CVC3
CVC3::RecordsTheoremProducer Member List

This is the complete list of members for CVC3::RecordsTheoremProducer, including all inherited members.

d_checkProofsCVC3::TheoremProducerprotected
d_emCVC3::TheoremProducerprotected
d_holeCVC3::TheoremProducerprotected
d_pfOpCVC3::TheoremProducerprotected
d_theoryRecordsCVC3::RecordsTheoremProducerprivate
d_tmCVC3::TheoremProducerprotected
expandEq(const Theorem &eqThrm)CVC3::RecordsTheoremProducervirtual
expandNeq(const Theorem &neqThrm)CVC3::RecordsTheoremProducervirtual
expandRecord(const Expr &e)CVC3::RecordsTheoremProducervirtual
expandTuple(const Expr &e)CVC3::RecordsTheoremProducervirtual
getField(const Expr &e, int i)CVC3::RecordsTheoremProducerinline
getField(const Expr &e)CVC3::RecordsTheoremProducerinline
getFieldIndex(const Expr &e, const std::string &field)CVC3::RecordsTheoremProducerinline
getFields(const Expr &r)CVC3::RecordsTheoremProducerinline
getIndex(const Expr &e)CVC3::RecordsTheoremProducerinline
isRecordAccess(const Expr &e)CVC3::RecordsTheoremProducerinline
isRecordType(const Expr &e)CVC3::RecordsTheoremProducerinline
isRecordType(const Type &t)CVC3::RecordsTheoremProducerinline
isTupleAccess(const Expr &e)CVC3::RecordsTheoremProducerinline
newAssumption(const Expr &thm, const Proof &pf, int scope=-1)CVC3::TheoremProducerinlineprotected
newLabel(const Expr &e)CVC3::TheoremProducer
newPf(const std::string &name)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e)CVC3::TheoremProducer
newPf(const std::string &name, const Proof &pf)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e1, const Expr &e2)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e, const Proof &pf)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)CVC3::TheoremProducer
newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)CVC3::TheoremProducer
newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const std::string &name, const std::vector< Expr > &args)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e, const std::vector< Expr > &args)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const std::string &name, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const std::string &name, const std::vector< Expr > &args, const Proof &pf)CVC3::TheoremProducer
newPf(const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const Proof &label, const Expr &frm, const Proof &pf)CVC3::TheoremProducer
newPf(const Proof &label, const Proof &pf)CVC3::TheoremProducer
newPf(const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)CVC3::TheoremProducer
newPf(const std::vector< Proof > &labels, const Proof &pf)CVC3::TheoremProducer
newReflTheorem(const Expr &e)CVC3::TheoremProducerinlineprotected
newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &kids)CVC3::RecordsTheoremProducerinline
recordExpr(const std::vector< Expr > &fields, const std::vector< Expr > &kids)CVC3::RecordsTheoremProducerinline
recordSelect(const Expr &r, const std::string &field)CVC3::RecordsTheoremProducerinline
RecordsTheoremProducer(TheoremManager *tm, TheoryRecords *t)CVC3::RecordsTheoremProducerinline
recordType(const std::vector< std::string > &fields, const std::vector< Type > &types)CVC3::RecordsTheoremProducerinline
recordType(const std::vector< std::string > &fields, const std::vector< Expr > &types)CVC3::RecordsTheoremProducerinline
recordUpdate(const Expr &r, const std::string &field, const Expr &val)CVC3::RecordsTheoremProducerinline
rewriteLitSelect(const Expr &e)CVC3::RecordsTheoremProducervirtual
rewriteLitUpdate(const Expr &e)CVC3::RecordsTheoremProducervirtual
rewriteUpdateSelect(const Expr &e)CVC3::RecordsTheoremProducervirtual
soundError(const std::string &file, int line, const std::string &cond, const std::string &msg)CVC3::TheoremProducerprotected
TheoremProducer(TheoremManager *tm)CVC3::TheoremProducer
tupleExpr(const std::vector< Expr > &kids)CVC3::RecordsTheoremProducerinline
tupleSelect(const Expr &tup, int i)CVC3::RecordsTheoremProducerinline
tupleType(const std::vector< Type > &types)CVC3::RecordsTheoremProducerinline
tupleType(const std::vector< Expr > &types)CVC3::RecordsTheoremProducerinline
tupleUpdate(const Expr &tup, int i, const Expr &val)CVC3::RecordsTheoremProducerinline
withAssumptions()CVC3::TheoremProducerinline
withProof()CVC3::TheoremProducerinline
~RecordsProofRules()CVC3::RecordsProofRulesinlinevirtual
~TheoremProducer()CVC3::TheoremProducerinlinevirtual