| addPairToArithOrder(const Expr &smaller, const Expr &bigger) | CVC3::VCL | [virtual] |
| andExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| andExpr(const std::vector< Expr > &children) | CVC3::VCL | [virtual] |
| arrayType(const Type &typeIndex, const Type &typeData) | CVC3::VCL | [virtual] |
| assertFormula(const Expr &e) | CVC3::VCL | [virtual] |
| bitvecType(int n) | CVC3::VCL | [virtual] |
| boolType() | CVC3::VCL | [virtual] |
| boundVarExpr(const std::string &name, const std::string &uid, const Type &type) | CVC3::VCL | [virtual] |
| checkContinue() | CVC3::VCL | [virtual] |
| checkTCC(const Expr &tcc) | CVC3::VCL | [private] |
| checkUnsat(const Expr &e) | CVC3::VCL | [virtual] |
| cmdsFromString(const std::string &s, InputLanguage lang) | CVC3::VCL | [virtual] |
| computeBVConst(const Expr &e) | CVC3::VCL | [virtual] |
| core() | CVC3::VCL | |
| create(const CLFlags &flags) | CVC3::ValidityChecker | [static] |
| create() | CVC3::ValidityChecker | [static] |
| createFlags() | CVC3::ValidityChecker | [static] |
| createOp(const std::string &name, const Type &type) | CVC3::VCL | [virtual] |
| createOp(const std::string &name, const Type &type, const Expr &def) | CVC3::VCL | [virtual] |
| createType(const std::string &typeName) | CVC3::VCL | [virtual] |
| createType(const std::string &typeName, const Type &def) | CVC3::VCL | [virtual] |
| d_batchedAssertions | CVC3::VCL | [private] |
| d_batchedAssertionsIdx | CVC3::VCL | [private] |
| d_cm | CVC3::VCL | [private] |
| d_dump | CVC3::VCL | [private] |
| d_em | CVC3::VCL | [private] |
| d_flags | CVC3::VCL | [private] |
| d_lastClosure | CVC3::VCL | [private] |
| d_lastQuery | CVC3::VCL | [private] |
| d_lastQueryTCC | CVC3::VCL | [private] |
| d_nextIdx | CVC3::VCL | [private] |
| d_se | CVC3::VCL | [private] |
| d_stackLevel | CVC3::VCL | [private] |
| d_statistics | CVC3::VCL | [private] |
| d_theories | CVC3::VCL | [private] |
| d_theoryArith | CVC3::VCL | [private] |
| d_theoryArray | CVC3::VCL | [private] |
| d_theoryBitvector | CVC3::VCL | [private] |
| d_theoryCore | CVC3::VCL | [private] |
| d_theoryDatatype | CVC3::VCL | [private] |
| d_theoryQuant | CVC3::VCL | [private] |
| d_theoryRecords | CVC3::VCL | [private] |
| d_theorySimulate | CVC3::VCL | [private] |
| d_theoryUF | CVC3::VCL | [private] |
| d_tm | CVC3::VCL | [private] |
| d_translator | CVC3::VCL | [private] |
| d_userAssertions | CVC3::VCL | [private] |
| dataType(const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types) | CVC3::VCL | [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) | CVC3::VCL | [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) | CVC3::VCL | [virtual] |
| datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args) | CVC3::VCL | [virtual] |
| datatypeSelExpr(const std::string &selector, const Expr &arg) | CVC3::VCL | [virtual] |
| datatypeTestExpr(const std::string &constructor, const Expr &arg) | CVC3::VCL | [virtual] |
| deriveClosure(const Theorem3 &thm) | CVC3::VCL | [private] |
| destroy(void) | CVC3::VCL | [private] |
| distinctExpr(const std::vector< Expr > &children) | CVC3::VCL | [virtual] |
| divideExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| eqExpr(const Expr &child0, const Expr &child1) | CVC3::VCL | [virtual] |
| existsExpr(const std::vector< Expr > &vars, const Expr &body) | CVC3::VCL | [virtual] |
| exprFromString(const std::string &s) | CVC3::VCL | [virtual] |
| falseExpr() | CVC3::VCL | [virtual] |
| forallExpr(const std::vector< Expr > &vars, const Expr &body) | CVC3::VCL | [virtual] |
| forallExpr(const std::vector< Expr > &vars, const Expr &body, const Expr &trigger) | CVC3::VCL | [virtual] |
| forallExpr(const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers) | CVC3::VCL | [virtual] |
| forallExpr(const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers) | CVC3::VCL | [virtual] |
| funExpr(const Op &op, const Expr &child) | CVC3::VCL | [virtual] |
| funExpr(const Op &op, const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| funExpr(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2) | CVC3::VCL | [virtual] |
| funExpr(const Op &op, const std::vector< Expr > &children) | CVC3::VCL | [virtual] |
| funType(const Type &typeDom, const Type &typeRan) | CVC3::VCL | [virtual] |
| funType(const std::vector< Type > &typeDom, const Type &typeRan) | CVC3::VCL | [virtual] |
| geExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| getAssumptions(const Assumptions &a, std::vector< Expr > &assumptions) | CVC3::VCL | [private] |
| getAssumptions(std::vector< Expr > &assumptions) | CVC3::VCL | [virtual] |
| getAssumptionsRec(const Theorem &thm, std::set< UserAssertion > &assumptions, bool addTCCs) | CVC3::VCL | [private] |
| getAssumptionsTCC(std::vector< Expr > &assumptions) | CVC3::VCL | [virtual] |
| getAssumptionsUsed(std::vector< Expr > &assumptions) | CVC3::VCL | [virtual] |
| getBaseType(const Expr &e) | CVC3::VCL | [virtual] |
| getBaseType(const Type &e) | CVC3::VCL | [virtual] |
| getClosure() | CVC3::VCL | [virtual] |
| getConcreteModel(ExprMap< Expr > &m) | CVC3::VCL | [virtual] |
| getCounterExample(std::vector< Expr > &assumptions, bool inOrder) | CVC3::VCL | [virtual] |
| getCurrentContext() | CVC3::VCL | [virtual] |
| getEM() | CVC3::VCL | [inline, virtual] |
| getFlags() const | CVC3::VCL | [inline, virtual] |
| getImpliedLiteral() | CVC3::VCL | [virtual] |
| getInternalAssumptions(std::vector< Expr > &assumptions) | CVC3::VCL | [virtual] |
| getMemory(int verbosity=0) | CVC3::VCL | |
| getProof() | CVC3::VCL | [virtual] |
| getProofClosure() | CVC3::VCL | [virtual] |
| getProofQuery() | CVC3::VCL | [virtual] |
| getProofTCC() | CVC3::VCL | [virtual] |
| getStatistics() | CVC3::VCL | [inline, virtual] |
| getTCC() | CVC3::VCL | [virtual] |
| getType(const Expr &e) | CVC3::VCL | [virtual] |
| getTypePred(const Type &t, const Expr &e) | CVC3::VCL | [virtual] |
| getUserAssumptions(std::vector< Expr > &assumptions) | CVC3::VCL | [virtual] |
| gtExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| idExpr(const std::string &name) | CVC3::VCL | [virtual] |
| iffExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| impliesExpr(const Expr &hyp, const Expr &conc) | CVC3::VCL | [virtual] |
| importExpr(const Expr &e) | CVC3::VCL | [virtual] |
| importType(const Type &t) | CVC3::VCL | [virtual] |
| incomplete() | CVC3::VCL | [virtual] |
| incomplete(std::vector< std::string > &reasons) | CVC3::VCL | [virtual] |
| inconsistent(std::vector< Expr > &assumptions) | CVC3::VCL | [virtual] |
| inconsistent() | CVC3::VCL | [virtual] |
| init(void) | CVC3::VCL | [private] |
| intType() | CVC3::VCL | [virtual] |
| iteExpr(const Expr &ifpart, const Expr &thenpart, const Expr &elsepart) | CVC3::VCL | [virtual] |
| lambdaExpr(const std::vector< Expr > &vars, const Expr &body) | CVC3::VCL | [virtual] |
| leExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| listExpr(const std::vector< Expr > &kids) | CVC3::VCL | [virtual] |
| listExpr(const Expr &e1) | CVC3::VCL | [virtual] |
| listExpr(const Expr &e1, const Expr &e2) | CVC3::VCL | [virtual] |
| listExpr(const Expr &e1, const Expr &e2, const Expr &e3) | CVC3::VCL | [virtual] |
| listExpr(const std::string &op, const std::vector< Expr > &kids) | CVC3::VCL | [virtual] |
| listExpr(const std::string &op, const Expr &e1) | CVC3::VCL | [virtual] |
| listExpr(const std::string &op, const Expr &e1, const Expr &e2) | CVC3::VCL | [virtual] |
| listExpr(const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3) | CVC3::VCL | [virtual] |
| loadFile(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false) | CVC3::VCL | [virtual] |
| loadFile(std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false) | CVC3::VCL | [virtual] |
| lookupOp(const std::string &name, Type *type) | CVC3::VCL | [virtual] |
| lookupType(const std::string &typeName) | CVC3::VCL | [virtual] |
| lookupVar(const std::string &name, Type *type) | CVC3::VCL | [virtual] |
| ltExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| minusExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| multExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| newBVAndExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVAndExpr(const std::vector< Expr > &kids) | CVC3::VCL | [virtual] |
| newBVCompExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVConstExpr(const std::string &s, int base) | CVC3::VCL | [virtual] |
| newBVConstExpr(const std::vector< bool > &bits) | CVC3::VCL | [virtual] |
| newBVConstExpr(const Rational &r, int len) | CVC3::VCL | [virtual] |
| newBVExtractExpr(const Expr &e, int hi, int low) | CVC3::VCL | [virtual] |
| newBVLEExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVLTExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVMultExpr(int numbits, const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVNandExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVNegExpr(const Expr &t1) | CVC3::VCL | [virtual] |
| newBVNorExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVOrExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVOrExpr(const std::vector< Expr > &kids) | CVC3::VCL | [virtual] |
| newBVPlusExpr(int numbits, const std::vector< Expr > &k) | CVC3::VCL | [virtual] |
| newBVPlusExpr(int numbits, const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVSDivExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVSLEExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVSLTExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVSModExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVSRemExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVSubExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVUDivExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVUminusExpr(const Expr &t1) | CVC3::VCL | [virtual] |
| newBVURemExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVXnorExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVXnorExpr(const std::vector< Expr > &kids) | CVC3::VCL | [virtual] |
| newBVXorExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newBVXorExpr(const std::vector< Expr > &kids) | CVC3::VCL | [virtual] |
| newConcatExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | [virtual] |
| newConcatExpr(const std::vector< Expr > &kids) | CVC3::VCL | [virtual] |
| newFixedConstWidthLeftShiftExpr(const Expr &t1, int r) | CVC3::VCL | [virtual] |
| newFixedLeftShiftExpr(const Expr &t1, int r) | CVC3::VCL | [virtual] |
| newFixedRightShiftExpr(const Expr &t1, int r) | CVC3::VCL | [virtual] |
| newSXExpr(const Expr &t1, int len) | CVC3::VCL | [virtual] |
| notExpr(const Expr &child) | CVC3::VCL | [virtual] |
| orExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| orExpr(const std::vector< Expr > &children) | CVC3::VCL | [virtual] |
| parseExpr(const Expr &e) | CVC3::VCL | [virtual] |
| parseType(const Expr &e) | CVC3::VCL | [virtual] |
| plusExpr(const Expr &left, const Expr &right) | CVC3::VCL | [virtual] |
| plusExpr(const std::vector< Expr > &children) | CVC3::VCL | [virtual] |
| pop() | CVC3::VCL | [virtual] |
| popScope() | CVC3::VCL | [virtual] |
| popto(int stackLevel) | CVC3::VCL | [virtual] |
| poptoScope(int scopeLevel) | CVC3::VCL | [virtual] |
| powExpr(const Expr &x, const Expr &n) | CVC3::VCL | [virtual] |
| printExpr(const Expr &e) | CVC3::VCL | [virtual] |
| printExpr(const Expr &e, std::ostream &os) | CVC3::VCL | [virtual] |
| printStatistics() | CVC3::VCL | [inline, virtual] |
| push() | CVC3::VCL | [virtual] |
| pushScope() | CVC3::VCL | [virtual] |
| query(const Expr &e) | CVC3::VCL | [virtual] |
| ratExpr(int n, int d) | CVC3::VCL | [virtual] |
| ratExpr(const std::string &n, const std::string &d, int base) | CVC3::VCL | [virtual] |
| ratExpr(const std::string &n, int base) | CVC3::VCL | [virtual] |
| readExpr(const Expr &array, const Expr &index) | CVC3::VCL | [virtual] |
| realType() | CVC3::VCL | [virtual] |
| recordExpr(const std::string &field, const Expr &expr) | CVC3::VCL | [virtual] |
| recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1) | CVC3::VCL | [virtual] |
| recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2) | CVC3::VCL | [virtual] |
| recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &exprs) | CVC3::VCL | [virtual] |
| recordType(const std::string &field, const Type &type) | CVC3::VCL | [virtual] |
| recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1) | CVC3::VCL | [virtual] |
| recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2) | CVC3::VCL | [virtual] |
| recordType(const std::vector< std::string > &fields, const std::vector< Type > &types) | CVC3::VCL | [virtual] |
| recSelectExpr(const Expr &record, const std::string &field) | CVC3::VCL | [virtual] |
| recUpdateExpr(const Expr &record, const std::string &field, const Expr &newValue) | CVC3::VCL | [virtual] |
| registerAtom(const Expr &e) | CVC3::VCL | [virtual] |
| reprocessFlags() | CVC3::VCL | [virtual] |
| reset() | CVC3::VCL | [virtual] |
| restart(const Expr &e) | CVC3::VCL | [virtual] |
| returnFromCheck() | CVC3::VCL | [virtual] |
| scopeLevel() | CVC3::VCL | [virtual] |
| setMultiTrigger(const Expr &e, const std::vector< Expr > &multiTrigger) | CVC3::VCL | [virtual] |
| setResourceLimit(unsigned limit) | CVC3::VCL | [virtual] |
| setTimeLimit(unsigned limit) | CVC3::VCL | [virtual] |
| setTrigger(const Expr &e, const Expr &trigger) | CVC3::VCL | [virtual] |
| setTriggers(const Expr &e, const std::vector< std::vector< Expr > > &triggers) | CVC3::VCL | [virtual] |
| setTriggers(const Expr &e, const std::vector< Expr > &triggers) | CVC3::VCL | [virtual] |
| simplify(const Expr &e) | CVC3::VCL | [virtual] |
| simplifyThm(const Expr &e) | CVC3::VCL | |
| simulateExpr(const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n) | CVC3::VCL | [virtual] |
| stackLevel() | CVC3::VCL | [virtual] |
| stringExpr(const std::string &str) | CVC3::VCL | [virtual] |
| subrangeType(const Expr &l, const Expr &r) | CVC3::VCL | [virtual] |
| subtypeType(const Expr &pred, const Expr &witness) | CVC3::VCL | [virtual] |
| transClosure(const Op &op) | CVC3::VCL | [virtual] |
| trueExpr() | CVC3::VCL | [virtual] |
| tryModelGeneration() | CVC3::VCL | [virtual] |
| tupleExpr(const std::vector< Expr > &exprs) | CVC3::VCL | [virtual] |
| tupleSelectExpr(const Expr &tuple, int index) | CVC3::VCL | [virtual] |
| tupleType(const Type &type0, const Type &type1) | CVC3::VCL | [virtual] |
| tupleType(const Type &type0, const Type &type1, const Type &type2) | CVC3::VCL | [virtual] |
| tupleType(const std::vector< Type > &types) | CVC3::VCL | [virtual] |
| tupleUpdateExpr(const Expr &tuple, int index, const Expr &newValue) | CVC3::VCL | [virtual] |
| uminusExpr(const Expr &child) | CVC3::VCL | [virtual] |
| ValidityChecker() | CVC3::ValidityChecker | [inline] |
| value(const Expr &e) | CVC3::VCL | [virtual] |
| varExpr(const std::string &name, const Type &type) | CVC3::VCL | [virtual] |
| varExpr(const std::string &name, const Type &type, const Expr &def) | CVC3::VCL | [virtual] |
| VCL(const CLFlags &flags) | CVC3::VCL | |
| writeExpr(const Expr &array, const Expr &index, const Expr &newValue) | CVC3::VCL | [virtual] |
| ~ValidityChecker() | CVC3::ValidityChecker | [inline, virtual] |
| ~VCL() | CVC3::VCL | |
