| andExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| andExpr(const std::vector< Expr > &children) | CVCL::VCL | [private, virtual] |
| arrayType(const Type &typeIndex, const Type &typeData) | CVCL::VCL | [private, virtual] |
| assertFormula(const Expr &e) | CVCL::VCL | [private, virtual] |
| boolType() | CVCL::VCL | [private, virtual] |
| boundVarExpr(const std::string &name, const std::string &uid, const Type &type) | CVCL::VCL | [private, virtual] |
| checkContinue() | CVCL::VCL | [private, virtual] |
| checkUnsat(const Expr &e) | CVCL::VCL | [private, virtual] |
| create(const CLFlags &flags) | CVCL::ValidityChecker | [static] |
| create() | CVCL::ValidityChecker | [static] |
| createFlags() | CVCL::ValidityChecker | [static] |
| createOp(const std::string &name, const Type &type) | CVCL::VCL | [private, virtual] |
| createOp(const std::string &name, const Type &type, const Expr &def) | CVCL::VCL | [private, virtual] |
| createType(const std::string &typeName) | CVCL::VCL | [private, virtual] |
| createType(const std::string &typeName, const Type &def) | CVCL::VCL | [private, virtual] |
| d_cm | CVCL::VCL | [private] |
| d_dump | CVCL::VCL | [private] |
| d_dumpFileOpen | CVCL::VCL | [private] |
| d_em | CVCL::VCL | [private] |
| d_flags | CVCL::VCL | [private] |
| d_lastClosure | CVCL::VCL | [private] |
| d_lastQuery | CVCL::VCL | [private] |
| d_lastQueryTCC | CVCL::VCL | [private] |
| d_nextIdx | CVCL::VCL | [private] |
| d_osdump | CVCL::VCL | [private] |
| d_osdumpFile | CVCL::VCL | [private] |
| d_osdumpTranslate | CVCL::VCL | [private] |
| d_osdumpTranslateFile | CVCL::VCL | [private] |
| d_scopeStack | CVCL::VCL | [private] |
| d_se | CVCL::VCL | [private] |
| d_statistics | CVCL::VCL | [private] |
| d_theories | CVCL::VCL | [private] |
| d_theoryArith | CVCL::VCL | [private] |
| d_theoryArray | CVCL::VCL | [private] |
| d_theoryBitvector | CVCL::VCL | [private] |
| d_theoryCore | CVCL::VCL | [private] |
| d_theoryDatatype | CVCL::VCL | [private] |
| d_theoryQuant | CVCL::VCL | [private] |
| d_theoryRecords | CVCL::VCL | [private] |
| d_theorySimulate | CVCL::VCL | [private] |
| d_theoryUF | CVCL::VCL | [private] |
| d_tm | CVCL::VCL | [private] |
| d_tmpFile | CVCL::VCL | [private] |
| d_translate | CVCL::VCL | [private] |
| d_translateFileOpen | CVCL::VCL | [private] |
| d_translator | CVCL::VCL | [private] |
| d_userAssertions | CVCL::VCL | [private] |
| d_vars | CVCL::VCL | [private] |
| dataType(const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types) | CVCL::VCL | [private, 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) | CVCL::VCL | [private, 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) | CVCL::VCL | [private, virtual] |
| datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args) | CVCL::VCL | [private, virtual] |
| datatypeSelExpr(const std::string &selector, const Expr &arg) | CVCL::VCL | [private, virtual] |
| datatypeTestExpr(const std::string &constructor, const Expr &arg) | CVCL::VCL | [private, virtual] |
| deriveClosure(const Theorem3 &thm) | CVCL::VCL | [private] |
| divideExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| eqExpr(const Expr &child0, const Expr &child1) | CVCL::VCL | [private, virtual] |
| existsExpr(const std::vector< Expr > &vars, const Expr &body) | CVCL::VCL | [private, virtual] |
| falseExpr() | CVCL::VCL | [private, virtual] |
| forallExpr(const std::vector< Expr > &vars, const Expr &body) | CVCL::VCL | [private, virtual] |
| funExpr(const Op &op, const Expr &child) | CVCL::VCL | [private, virtual] |
| funExpr(const Op &op, const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| funExpr(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2) | CVCL::VCL | [private, virtual] |
| funExpr(const Op &op, const std::vector< Expr > &children) | CVCL::VCL | [private, virtual] |
| funType(const Type &typeDom, const Type &typeRan) | CVCL::VCL | [private, virtual] |
| funType(const std::vector< Type > &typeDom, const Type &typeRan) | CVCL::VCL | [private, virtual] |
| geExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| getAssumptions(const Assumptions &a, std::vector< Expr > &assumptions) | CVCL::VCL | [private] |
| getAssumptions(std::vector< Expr > &assumptions) | CVCL::VCL | [private, virtual] |
| getAssumptionsRec(const Theorem &thm, std::set< UserAssertion > &assumptions, bool addTCCs) | CVCL::VCL | [private] |
| getAssumptionsTCC(std::vector< Expr > &assumptions) | CVCL::VCL | [private, virtual] |
| getAssumptionsUsed(std::vector< Expr > &assumptions) | CVCL::VCL | [private, virtual] |
| getBaseType(const Expr &e) | CVCL::VCL | [private, virtual] |
| getBaseType(const Type &e) | CVCL::VCL | [private, virtual] |
| getClosure() | CVCL::VCL | [private, virtual] |
| getConcreteModel(ExprMap< Expr > &m) | CVCL::VCL | [private, virtual] |
| getCounterExample(std::vector< Expr > &assertions, bool inOrder) | CVCL::VCL | [private, virtual] |
| getCurrentContext() | CVCL::VCL | [private, virtual] |
| getEM() | CVCL::VCL | [inline, private, virtual] |
| getFlags() const | CVCL::VCL | [inline, private, virtual] |
| getImpliedLiteral() | CVCL::VCL | [private, virtual] |
| getInternalAssumptions(std::vector< Expr > &assumptions) | CVCL::VCL | [private, virtual] |
| getProof() | CVCL::VCL | [private, virtual] |
| getProofClosure() | CVCL::VCL | [private, virtual] |
| getProofTCC() | CVCL::VCL | [private, virtual] |
| getStatistics() | CVCL::VCL | [inline, private, virtual] |
| getTCC() | CVCL::VCL | [private, virtual] |
| getType(const Expr &e) | CVCL::VCL | [private, virtual] |
| getTypePred(const Type &t, const Expr &e) | CVCL::VCL | [private, virtual] |
| getUserAssumptions(std::vector< Expr > &assumptions) | CVCL::VCL | [private, virtual] |
| gtExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| idExpr(const std::string &name) | CVCL::VCL | [private, virtual] |
| iffExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| impliesExpr(const Expr &hyp, const Expr &conc) | CVCL::VCL | [private, virtual] |
| importExpr(const Expr &e) | CVCL::VCL | [private, virtual] |
| importType(const Type &t) | CVCL::VCL | [private, virtual] |
| incomplete() | CVCL::VCL | [private, virtual] |
| incomplete(std::vector< std::string > &reasons) | CVCL::VCL | [private, virtual] |
| inconsistent(std::vector< Expr > &assumptions) | CVCL::VCL | [private, virtual] |
| intType() | CVCL::VCL | [private, virtual] |
| iteExpr(const Expr &ifpart, const Expr &thenpart, const Expr &elsepart) | CVCL::VCL | [private, virtual] |
| lambdaExpr(const std::vector< Expr > &vars, const Expr &body) | CVCL::VCL | [private, virtual] |
| leExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| listExpr(const std::vector< Expr > &kids) | CVCL::VCL | [private, virtual] |
| listExpr(const Expr &e1) | CVCL::VCL | [private, virtual] |
| listExpr(const Expr &e1, const Expr &e2) | CVCL::VCL | [private, virtual] |
| listExpr(const Expr &e1, const Expr &e2, const Expr &e3) | CVCL::VCL | [private, virtual] |
| listExpr(const std::string &op, const std::vector< Expr > &kids) | CVCL::VCL | [private, virtual] |
| listExpr(const std::string &op, const Expr &e1) | CVCL::VCL | [private, virtual] |
| listExpr(const std::string &op, const Expr &e1, const Expr &e2) | CVCL::VCL | [private, virtual] |
| listExpr(const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3) | CVCL::VCL | [private, virtual] |
| loadFile(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false) | CVCL::VCL | [private, virtual] |
| loadFile(std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false) | CVCL::VCL | [private, virtual] |
| lookupType(const std::string &typeName) | CVCL::VCL | [private, virtual] |
| lookupVar(const std::string &name, Type *type) | CVCL::VCL | [private, virtual] |
| ltExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| minusExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| multExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| notExpr(const Expr &child) | CVCL::VCL | [private, virtual] |
| orExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| orExpr(const std::vector< Expr > &children) | CVCL::VCL | [private, virtual] |
| parseExpr(const Expr &e) | CVCL::VCL | [private, virtual] |
| parseType(const Expr &e) | CVCL::VCL | [private, virtual] |
| plusExpr(const Expr &left, const Expr &right) | CVCL::VCL | [private, virtual] |
| pop() | CVCL::VCL | [private, virtual] |
| popScope() | CVCL::VCL | [private, virtual] |
| popto(int stackLevel) | CVCL::VCL | [private, virtual] |
| poptoScope(int scopeLevel) | CVCL::VCL | [private, virtual] |
| powExpr(const Expr &x, const Expr &n) | CVCL::VCL | [private, virtual] |
| printExpr(const Expr &e) | CVCL::VCL | [private, virtual] |
| printExpr(const Expr &e, std::ostream &os) | CVCL::VCL | [private, virtual] |
| printStatistics() | CVCL::VCL | [inline, private, virtual] |
| printV(const Expr &e) | CVCL::VCL | [private, virtual] |
| push() | CVCL::VCL | [private, virtual] |
| pushScope() | CVCL::VCL | [private, virtual] |
| query(const Expr &e, bool isTCC=false) | CVCL::VCL | [private, virtual] |
| ratExpr(int n, int d) | CVCL::VCL | [private, virtual] |
| ratExpr(const std::string &n, const std::string &d, int base) | CVCL::VCL | [private, virtual] |
| ratExpr(const std::string &n, int base) | CVCL::VCL | [private, virtual] |
| readExpr(const Expr &array, const Expr &index) | CVCL::VCL | [private, virtual] |
| realType() | CVCL::VCL | [private, virtual] |
| recordExpr(const std::string &field, const Expr &expr) | CVCL::VCL | [private, virtual] |
| recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1) | CVCL::VCL | [private, virtual] |
| recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2) | CVCL::VCL | [private, virtual] |
| recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &exprs) | CVCL::VCL | [private, virtual] |
| recordType(const std::string &field, const Type &type) | CVCL::VCL | [private, virtual] |
| recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1) | CVCL::VCL | [private, virtual] |
| recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2) | CVCL::VCL | [private, virtual] |
| recordType(const std::vector< std::string > &fields, const std::vector< Type > &types) | CVCL::VCL | [private, virtual] |
| recSelectExpr(const Expr &record, const std::string &field) | CVCL::VCL | [private, virtual] |
| recUpdateExpr(const Expr &record, const std::string &field, const Expr &newValue) | CVCL::VCL | [private, virtual] |
| registerAtom(const Expr &e) | CVCL::VCL | [private, virtual] |
| reprocessFlags() | CVCL::VCL | [private, virtual] |
| restart(const Expr &e) | CVCL::VCL | [private, virtual] |
| returnFromCheck() | CVCL::VCL | [private, virtual] |
| scopeLevel() | CVCL::VCL | [private, virtual] |
| setResourceLimit(unsigned limit) | CVCL::VCL | [private, virtual] |
| simplify(const Expr &e) | CVCL::VCL | [private, virtual] |
| simplifyThm(const Expr &e) | CVCL::VCL | [private, virtual] |
| simplifyThm2(const Expr &e) | CVCL::VCL | [private, virtual] |
| simulateExpr(const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n) | CVCL::VCL | [private, virtual] |
| stackLevel() | CVCL::VCL | [private, virtual] |
| stringExpr(const std::string &str) | CVCL::VCL | [private, virtual] |
| subrangeType(const Expr &l, const Expr &r) | CVCL::VCL | [private, virtual] |
| subtypeType(const Expr &pred) | CVCL::VCL | [private, virtual] |
| trueExpr() | CVCL::VCL | [private, virtual] |
| tupleExpr(const std::vector< Expr > &exprs) | CVCL::VCL | [private, virtual] |
| tupleSelectExpr(const Expr &tuple, int index) | CVCL::VCL | [private, virtual] |
| tupleType(const Type &type0, const Type &type1) | CVCL::VCL | [private, virtual] |
| tupleType(const Type &type0, const Type &type1, const Type &type2) | CVCL::VCL | [private, virtual] |
| tupleType(const std::vector< Type > &types) | CVCL::VCL | [private, virtual] |
| tupleUpdateExpr(const Expr &tuple, int index, const Expr &newValue) | CVCL::VCL | [private, virtual] |
| uminusExpr(const Expr &child) | CVCL::VCL | [private, virtual] |
| ValidityChecker() | CVCL::ValidityChecker | [inline] |
| varExpr(const std::string &name, const Type &type) | CVCL::VCL | [private, virtual] |
| varExpr(const std::string &name, const Type &type, const Expr &def) | CVCL::VCL | [private, virtual] |
| writeExpr(const Expr &array, const Expr &index, const Expr &newValue) | CVCL::VCL | [private, virtual] |
| ~ValidityChecker() | CVCL::ValidityChecker | [inline, virtual] |
| ~VCL | CVCL::VCL | [private] |
