| d_checkProofs | CVCL::TheoremProducer | [protected] |
| d_em | CVCL::TheoremProducer | [protected] |
| d_hole | CVCL::TheoremProducer | [protected] |
| d_pfOp | CVCL::TheoremProducer | [protected] |
| d_theoryRecords | CVCL::RecordsTheoremProducer | [private] |
| d_tm | CVCL::TheoremProducer | [protected] |
| expandEq(const Theorem &eqThrm) | CVCL::RecordsTheoremProducer | [virtual] |
| expandNeq(const Theorem &neqThrm) | CVCL::RecordsTheoremProducer | [virtual] |
| expandRecord(const Expr &e) | CVCL::RecordsTheoremProducer | [virtual] |
| expandTuple(const Expr &e) | CVCL::RecordsTheoremProducer | [virtual] |
| getField(const Expr &e, int i) | CVCL::RecordsTheoremProducer | [inline] |
| getField(const Expr &e) | CVCL::RecordsTheoremProducer | [inline] |
| getFieldIndex(const Expr &e, const std::string &field) | CVCL::RecordsTheoremProducer | [inline] |
| getFields(const Expr &r) | CVCL::RecordsTheoremProducer | [inline] |
| getIndex(const Expr &e) | CVCL::RecordsTheoremProducer | [inline] |
| isRecordAccess(const Expr &e) | CVCL::RecordsTheoremProducer | [inline] |
| isRecordType(const Expr &e) | CVCL::RecordsTheoremProducer | [inline] |
| isRecordType(const Type &t) | CVCL::RecordsTheoremProducer | [inline] |
| isTupleAccess(const Expr &e) | CVCL::RecordsTheoremProducer | [inline] |
| newAssumption(const Expr &thm, const Proof &pf, int scope=-1) | CVCL::TheoremProducer | [inline, protected] |
| newLabel(const Expr &e) | CVCL::TheoremProducer | |
| newPf(const std::string &name) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end) | CVCL::TheoremProducer | |
| newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Expr > &args) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, const std::vector< Expr > &args) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Expr > &args, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs) | CVCL::TheoremProducer | |
| newPf(const Proof &label, const Expr &frm, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const Proof &label, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf) | CVCL::TheoremProducer | |
| newPf(const std::vector< Proof > &labels, const Proof &pf) | CVCL::TheoremProducer | |
| newReflTheorem(const Expr &e, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVCL::TheoremProducer | [inline, protected] |
| recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &kids) | CVCL::RecordsTheoremProducer | [inline] |
| recordExpr(const std::vector< Expr > &fields, const std::vector< Expr > &kids) | CVCL::RecordsTheoremProducer | [inline] |
| recordSelect(const Expr &r, const std::string &field) | CVCL::RecordsTheoremProducer | [inline] |
| RecordsTheoremProducer(TheoremManager *tm, TheoryRecords *t) | CVCL::RecordsTheoremProducer | [inline] |
| recordType(const std::vector< std::string > &fields, const std::vector< Type > &types) | CVCL::RecordsTheoremProducer | [inline] |
| recordType(const std::vector< std::string > &fields, const std::vector< Expr > &types) | CVCL::RecordsTheoremProducer | [inline] |
| recordUpdate(const Expr &r, const std::string &field, const Expr &val) | CVCL::RecordsTheoremProducer | [inline] |
| rewriteLitSelect(const Expr &e) | CVCL::RecordsTheoremProducer | [virtual] |
| rewriteLitUpdate(const Expr &e) | CVCL::RecordsTheoremProducer | [virtual] |
| rewriteUpdateSelect(const Expr &e) | CVCL::RecordsTheoremProducer | [virtual] |
| soundError(const std::string &file, int line, const std::string &cond, const std::string &msg) | CVCL::TheoremProducer | [protected] |
| TheoremProducer(TheoremManager *tm) | CVCL::TheoremProducer | |
| tupleExpr(const std::vector< Expr > &kids) | CVCL::RecordsTheoremProducer | [inline] |
| tupleSelect(const Expr &tup, int i) | CVCL::RecordsTheoremProducer | [inline] |
| tupleType(const std::vector< Type > &types) | CVCL::RecordsTheoremProducer | [inline] |
| tupleType(const std::vector< Expr > &types) | CVCL::RecordsTheoremProducer | [inline] |
| tupleUpdate(const Expr &tup, int i, const Expr &val) | CVCL::RecordsTheoremProducer | [inline] |
| withAssumptions() | CVCL::TheoremProducer | [inline] |
| withProof() | CVCL::TheoremProducer | [inline] |
| ~RecordsProofRules() | CVCL::RecordsProofRules | [inline, virtual] |
| ~TheoremProducer() | CVCL::TheoremProducer | [inline, virtual] |
