| 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] |
| 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] |
| 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] |
| 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] |
| 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] |
| 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] |
| 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 | [inline, virtual] |
