|
CVC3
|
This is the complete list of members for CVC3::ValidityChecker, including all inherited members.
| addPairToArithOrder(const Expr &smaller, const Expr &bigger)=0 | CVC3::ValidityChecker | pure virtual |
| andExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| andExpr(const std::vector< Expr > &children)=0 | CVC3::ValidityChecker | pure virtual |
| arrayType(const Type &typeIndex, const Type &typeData)=0 | CVC3::ValidityChecker | pure virtual |
| assertFormula(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| bitvecType(int n)=0 | CVC3::ValidityChecker | pure virtual |
| boolType()=0 | CVC3::ValidityChecker | pure virtual |
| boundVarExpr(const std::string &name, const std::string &uid, const Type &type)=0 | CVC3::ValidityChecker | pure virtual |
| checkContinue()=0 | CVC3::ValidityChecker | pure virtual |
| checkUnsat(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| cmdsFromString(const std::string &s, InputLanguage lang=PRESENTATION_LANG)=0 | CVC3::ValidityChecker | pure virtual |
| computeBVConst(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| create(const CLFlags &flags) | CVC3::ValidityChecker | static |
| create() | CVC3::ValidityChecker | static |
| createFlags() | CVC3::ValidityChecker | static |
| createOp(const std::string &name, const Type &type)=0 | CVC3::ValidityChecker | pure virtual |
| createOp(const std::string &name, const Type &type, const Expr &def)=0 | CVC3::ValidityChecker | pure virtual |
| createType(const std::string &typeName)=0 | CVC3::ValidityChecker | pure virtual |
| createType(const std::string &typeName, const Type &def)=0 | CVC3::ValidityChecker | pure virtual |
| dataType(const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types)=0 | CVC3::ValidityChecker | pure virtual |
| dataType(const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types)=0 | CVC3::ValidityChecker | pure virtual |
| dataType(const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< Expr > > > &types, std::vector< Type > &returnTypes)=0 | CVC3::ValidityChecker | pure virtual |
| datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args)=0 | CVC3::ValidityChecker | pure virtual |
| datatypeSelExpr(const std::string &selector, const Expr &arg)=0 | CVC3::ValidityChecker | pure virtual |
| datatypeTestExpr(const std::string &constructor, const Expr &arg)=0 | CVC3::ValidityChecker | pure virtual |
| distinctExpr(const std::vector< Expr > &children)=0 | CVC3::ValidityChecker | pure virtual |
| divideExpr(const Expr &numerator, const Expr &denominator)=0 | CVC3::ValidityChecker | pure virtual |
| eqExpr(const Expr &child0, const Expr &child1)=0 | CVC3::ValidityChecker | pure virtual |
| existsExpr(const std::vector< Expr > &vars, const Expr &body)=0 | CVC3::ValidityChecker | pure virtual |
| exprFromString(const std::string &e)=0 | CVC3::ValidityChecker | pure virtual |
| falseExpr()=0 | CVC3::ValidityChecker | pure virtual |
| forallExpr(const std::vector< Expr > &vars, const Expr &body)=0 | CVC3::ValidityChecker | pure virtual |
| forallExpr(const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)=0 | CVC3::ValidityChecker | pure virtual |
| forallExpr(const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)=0 | CVC3::ValidityChecker | pure virtual |
| forallExpr(const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers)=0 | CVC3::ValidityChecker | pure virtual |
| funExpr(const Op &op, const Expr &child)=0 | CVC3::ValidityChecker | pure virtual |
| funExpr(const Op &op, const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| funExpr(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)=0 | CVC3::ValidityChecker | pure virtual |
| funExpr(const Op &op, const std::vector< Expr > &children)=0 | CVC3::ValidityChecker | pure virtual |
| funType(const Type &typeDom, const Type &typeRan)=0 | CVC3::ValidityChecker | pure virtual |
| funType(const std::vector< Type > &typeDom, const Type &typeRan)=0 | CVC3::ValidityChecker | pure virtual |
| geExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| getAssignment()=0 | CVC3::ValidityChecker | pure virtual |
| getAssumptions(std::vector< Expr > &assumptions)=0 | CVC3::ValidityChecker | pure virtual |
| getAssumptionsTCC(std::vector< Expr > &assumptions)=0 | CVC3::ValidityChecker | pure virtual |
| getAssumptionsUsed(std::vector< Expr > &assumptions)=0 | CVC3::ValidityChecker | pure virtual |
| getBaseType(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| getBaseType(const Type &t)=0 | CVC3::ValidityChecker | pure virtual |
| getClosure()=0 | CVC3::ValidityChecker | pure virtual |
| getConcreteModel(ExprMap< Expr > &m)=0 | CVC3::ValidityChecker | pure virtual |
| getCounterExample(std::vector< Expr > &assumptions, bool inOrder=true)=0 | CVC3::ValidityChecker | pure virtual |
| getCurrentContext()=0 | CVC3::ValidityChecker | pure virtual |
| getEM()=0 | CVC3::ValidityChecker | pure virtual |
| getFlags() const =0 | CVC3::ValidityChecker | pure virtual |
| getImpliedLiteral()=0 | CVC3::ValidityChecker | pure virtual |
| getInternalAssumptions(std::vector< Expr > &assumptions)=0 | CVC3::ValidityChecker | pure virtual |
| getProof()=0 | CVC3::ValidityChecker | pure virtual |
| getProofClosure()=0 | CVC3::ValidityChecker | pure virtual |
| getProofQuery()=0 | CVC3::ValidityChecker | pure virtual |
| getProofTCC()=0 | CVC3::ValidityChecker | pure virtual |
| getStatistics()=0 | CVC3::ValidityChecker | pure virtual |
| getTCC()=0 | CVC3::ValidityChecker | pure virtual |
| getType(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| getTypePred(const Type &t, const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| getUserAssumptions(std::vector< Expr > &assumptions)=0 | CVC3::ValidityChecker | pure virtual |
| getValue(Expr e)=0 | CVC3::ValidityChecker | pure virtual |
| gtExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| idExpr(const std::string &name)=0 | CVC3::ValidityChecker | pure virtual |
| iffExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| impliesExpr(const Expr &hyp, const Expr &conc)=0 | CVC3::ValidityChecker | pure virtual |
| importExpr(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| importType(const Type &t)=0 | CVC3::ValidityChecker | pure virtual |
| incomplete()=0 | CVC3::ValidityChecker | pure virtual |
| incomplete(std::vector< std::string > &reasons)=0 | CVC3::ValidityChecker | pure virtual |
| inconsistent(std::vector< Expr > &assumptions)=0 | CVC3::ValidityChecker | pure virtual |
| inconsistent()=0 | CVC3::ValidityChecker | pure virtual |
| intType()=0 | CVC3::ValidityChecker | pure virtual |
| iteExpr(const Expr &ifpart, const Expr &thenpart, const Expr &elsepart)=0 | CVC3::ValidityChecker | pure virtual |
| lambdaExpr(const std::vector< Expr > &vars, const Expr &body)=0 | CVC3::ValidityChecker | pure virtual |
| leExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| listExpr(const std::vector< Expr > &kids)=0 | CVC3::ValidityChecker | pure virtual |
| listExpr(const Expr &e1)=0 | CVC3::ValidityChecker | pure virtual |
| listExpr(const Expr &e1, const Expr &e2)=0 | CVC3::ValidityChecker | pure virtual |
| listExpr(const Expr &e1, const Expr &e2, const Expr &e3)=0 | CVC3::ValidityChecker | pure virtual |
| listExpr(const std::string &op, const std::vector< Expr > &kids)=0 | CVC3::ValidityChecker | pure virtual |
| listExpr(const std::string &op, const Expr &e1)=0 | CVC3::ValidityChecker | pure virtual |
| listExpr(const std::string &op, const Expr &e1, const Expr &e2)=0 | CVC3::ValidityChecker | pure virtual |
| listExpr(const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3)=0 | CVC3::ValidityChecker | pure virtual |
| loadFile(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false)=0 | CVC3::ValidityChecker | pure virtual |
| loadFile(std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)=0 | CVC3::ValidityChecker | pure virtual |
| logAnnotation(const Expr &annot)=0 | CVC3::ValidityChecker | pure virtual |
| lookupOp(const std::string &name, Type *type)=0 | CVC3::ValidityChecker | pure virtual |
| lookupType(const std::string &typeName)=0 | CVC3::ValidityChecker | pure virtual |
| lookupVar(const std::string &name, Type *type)=0 | CVC3::ValidityChecker | pure virtual |
| ltExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| minusExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| multExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| newBVAndExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVAndExpr(const std::vector< Expr > &kids)=0 | CVC3::ValidityChecker | pure virtual |
| newBVASHR(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVCompExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVConstExpr(const std::string &s, int base=2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVConstExpr(const std::vector< bool > &bits)=0 | CVC3::ValidityChecker | pure virtual |
| newBVConstExpr(const Rational &r, int len=0)=0 | CVC3::ValidityChecker | pure virtual |
| newBVExtractExpr(const Expr &e, int hi, int low)=0 | CVC3::ValidityChecker | pure virtual |
| newBVLEExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVLSHR(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVLTExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVMultExpr(int numbits, const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVNandExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVNegExpr(const Expr &t1)=0 | CVC3::ValidityChecker | pure virtual |
| newBVNorExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVOrExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVOrExpr(const std::vector< Expr > &kids)=0 | CVC3::ValidityChecker | pure virtual |
| newBVPlusExpr(int numbits, const std::vector< Expr > &k)=0 | CVC3::ValidityChecker | pure virtual |
| newBVPlusExpr(int numbits, const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVSDivExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVSHL(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVSLEExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVSLTExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVSModExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVSRemExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVSubExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVUDivExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVUminusExpr(const Expr &t1)=0 | CVC3::ValidityChecker | pure virtual |
| newBVURemExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVXnorExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVXnorExpr(const std::vector< Expr > &kids)=0 | CVC3::ValidityChecker | pure virtual |
| newBVXorExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newBVXorExpr(const std::vector< Expr > &kids)=0 | CVC3::ValidityChecker | pure virtual |
| newConcatExpr(const Expr &t1, const Expr &t2)=0 | CVC3::ValidityChecker | pure virtual |
| newConcatExpr(const std::vector< Expr > &kids)=0 | CVC3::ValidityChecker | pure virtual |
| newFixedConstWidthLeftShiftExpr(const Expr &t1, int r)=0 | CVC3::ValidityChecker | pure virtual |
| newFixedLeftShiftExpr(const Expr &t1, int r)=0 | CVC3::ValidityChecker | pure virtual |
| newFixedRightShiftExpr(const Expr &t1, int r)=0 | CVC3::ValidityChecker | pure virtual |
| newSXExpr(const Expr &t1, int len)=0 | CVC3::ValidityChecker | pure virtual |
| notExpr(const Expr &child)=0 | CVC3::ValidityChecker | pure virtual |
| orExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| orExpr(const std::vector< Expr > &children)=0 | CVC3::ValidityChecker | pure virtual |
| parseExpr(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| parseType(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| plusExpr(const Expr &left, const Expr &right)=0 | CVC3::ValidityChecker | pure virtual |
| plusExpr(const std::vector< Expr > &children)=0 | CVC3::ValidityChecker | pure virtual |
| pop()=0 | CVC3::ValidityChecker | pure virtual |
| popScope()=0 | CVC3::ValidityChecker | pure virtual |
| popto(int stackLevel)=0 | CVC3::ValidityChecker | pure virtual |
| poptoScope(int scopeLevel)=0 | CVC3::ValidityChecker | pure virtual |
| powExpr(const Expr &x, const Expr &n)=0 | CVC3::ValidityChecker | pure virtual |
| printExpr(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| printExpr(const Expr &e, std::ostream &os)=0 | CVC3::ValidityChecker | pure virtual |
| printStatistics()=0 | CVC3::ValidityChecker | pure virtual |
| push()=0 | CVC3::ValidityChecker | pure virtual |
| pushScope()=0 | CVC3::ValidityChecker | pure virtual |
| query(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| ratExpr(int n, int d=1)=0 | CVC3::ValidityChecker | pure virtual |
| ratExpr(const std::string &n, const std::string &d, int base)=0 | CVC3::ValidityChecker | pure virtual |
| ratExpr(const std::string &n, int base=10)=0 | CVC3::ValidityChecker | pure virtual |
| readExpr(const Expr &array, const Expr &index)=0 | CVC3::ValidityChecker | pure virtual |
| realType()=0 | CVC3::ValidityChecker | pure virtual |
| recordExpr(const std::string &field, const Expr &expr)=0 | CVC3::ValidityChecker | pure virtual |
| recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1)=0 | CVC3::ValidityChecker | pure virtual |
| recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2)=0 | CVC3::ValidityChecker | pure virtual |
| recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &exprs)=0 | CVC3::ValidityChecker | pure virtual |
| recordType(const std::string &field, const Type &type)=0 | CVC3::ValidityChecker | pure virtual |
| recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1)=0 | CVC3::ValidityChecker | pure virtual |
| recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2)=0 | CVC3::ValidityChecker | pure virtual |
| recordType(const std::vector< std::string > &fields, const std::vector< Type > &types)=0 | CVC3::ValidityChecker | pure virtual |
| recSelectExpr(const Expr &record, const std::string &field)=0 | CVC3::ValidityChecker | pure virtual |
| recUpdateExpr(const Expr &record, const std::string &field, const Expr &newValue)=0 | CVC3::ValidityChecker | pure virtual |
| registerAtom(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| reprocessFlags()=0 | CVC3::ValidityChecker | pure virtual |
| reset()=0 | CVC3::ValidityChecker | pure virtual |
| restart(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| returnFromCheck()=0 | CVC3::ValidityChecker | pure virtual |
| scopeLevel()=0 | CVC3::ValidityChecker | pure virtual |
| setMultiTrigger(const Expr &e, const std::vector< Expr > &multiTrigger)=0 | CVC3::ValidityChecker | pure virtual |
| setResourceLimit(unsigned limit)=0 | CVC3::ValidityChecker | pure virtual |
| setTimeLimit(unsigned limit)=0 | CVC3::ValidityChecker | pure virtual |
| setTrigger(const Expr &e, const Expr &trigger)=0 | CVC3::ValidityChecker | pure virtual |
| setTriggers(const Expr &e, const std::vector< std::vector< Expr > > &triggers)=0 | CVC3::ValidityChecker | pure virtual |
| setTriggers(const Expr &e, const std::vector< Expr > &triggers)=0 | CVC3::ValidityChecker | pure virtual |
| simplify(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| simulateExpr(const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n)=0 | CVC3::ValidityChecker | pure virtual |
| stackLevel()=0 | CVC3::ValidityChecker | pure virtual |
| stringExpr(const std::string &str)=0 | CVC3::ValidityChecker | pure virtual |
| subrangeType(const Expr &l, const Expr &r)=0 | CVC3::ValidityChecker | pure virtual |
| subtypeType(const Expr &pred, const Expr &witness)=0 | CVC3::ValidityChecker | pure virtual |
| transClosure(const Op &op)=0 | CVC3::ValidityChecker | pure virtual |
| trueExpr()=0 | CVC3::ValidityChecker | pure virtual |
| tryModelGeneration()=0 | CVC3::ValidityChecker | pure virtual |
| tupleExpr(const std::vector< Expr > &exprs)=0 | CVC3::ValidityChecker | pure virtual |
| tupleSelectExpr(const Expr &tuple, int index)=0 | CVC3::ValidityChecker | pure virtual |
| tupleType(const Type &type0, const Type &type1)=0 | CVC3::ValidityChecker | pure virtual |
| tupleType(const Type &type0, const Type &type1, const Type &type2)=0 | CVC3::ValidityChecker | pure virtual |
| tupleType(const std::vector< Type > &types)=0 | CVC3::ValidityChecker | pure virtual |
| tupleUpdateExpr(const Expr &tuple, int index, const Expr &newValue)=0 | CVC3::ValidityChecker | pure virtual |
| uminusExpr(const Expr &child)=0 | CVC3::ValidityChecker | pure virtual |
| ValidityChecker() | CVC3::ValidityChecker | inline |
| value(const Expr &e)=0 | CVC3::ValidityChecker | pure virtual |
| varExpr(const std::string &name, const Type &type)=0 | CVC3::ValidityChecker | pure virtual |
| varExpr(const std::string &name, const Type &type, const Expr &def)=0 | CVC3::ValidityChecker | pure virtual |
| writeExpr(const Expr &array, const Expr &index, const Expr &newValue)=0 | CVC3::ValidityChecker | pure virtual |
| ~ValidityChecker() | CVC3::ValidityChecker | inlinevirtual |
1.8.2