CVC3::CommonTheoremProducer Member List

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

ackermann(const Expr &e1, const Expr &e2)CVC3::CommonTheoremProducer [virtual]
andElim(const Theorem &e, int i)CVC3::CommonTheoremProducer [virtual]
andIntro(const Theorem &e1, const Theorem &e2)CVC3::CommonTheoremProducer [virtual]
andIntro(const std::vector< Theorem > &es)CVC3::CommonTheoremProducer [virtual]
assumpRule(const Expr &a, int scope=-1)CVC3::CommonTheoremProducer [virtual]
clearSkolemAxioms()CVC3::CommonTheoremProducer [inline, virtual]
CommonTheoremProducer(TheoremManager *tm)CVC3::CommonTheoremProducer
contradictionRule(const Theorem &e, const Theorem &not_e)CVC3::CommonTheoremProducer [virtual]
d_checkProofsCVC3::TheoremProducer [protected]
d_emCVC3::TheoremProducer [protected]
d_holeCVC3::TheoremProducer [protected]
d_pfOpCVC3::TheoremProducer [protected]
d_skolem_axiomsCVC3::CommonTheoremProducer [private]
d_skolemized_thmsCVC3::CommonTheoremProducer [private]
d_skolemVarsCVC3::CommonTheoremProducer [private]
d_tmCVC3::TheoremProducer [protected]
excludedMiddle(const Expr &e)CVC3::CommonTheoremProducer [virtual]
findITE(const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart)CVC3::CommonTheoremProducer [private]
getSkolemAxioms()CVC3::CommonTheoremProducer [inline, virtual]
iffContrapositive(const Theorem &thm)CVC3::CommonTheoremProducer [virtual]
iffFalseElim(const Theorem &e)CVC3::CommonTheoremProducer [virtual]
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVC3::CommonTheoremProducer [virtual]
iffNotFalse(const Theorem &e)CVC3::CommonTheoremProducer [virtual]
iffTrue(const Theorem &e)CVC3::CommonTheoremProducer [virtual]
iffTrueElim(const Theorem &e)CVC3::CommonTheoremProducer [virtual]
implContrapositive(const Theorem &thm)CVC3::CommonTheoremProducer [virtual]
implIntro(const Theorem &phi, const std::vector< Expr > &assump)CVC3::CommonTheoremProducer [virtual]
implIntro3(const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)CVC3::CommonTheoremProducer [virtual]
implMP(const Theorem &e1, const Theorem &e1_impl_e2)CVC3::CommonTheoremProducer [virtual]
liftOneITE(const Expr &e)CVC3::CommonTheoremProducer [virtual]
newAssumption(const Expr &thm, const Proof &pf, int scope=-1)CVC3::TheoremProducer [inline, protected]
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::TheoremProducer [inline, protected]
newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducer [inline, protected]
newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducer [inline, protected]
newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducer [inline, protected]
newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducer [inline, protected]
notNotElim(const Theorem &e)CVC3::CommonTheoremProducer [virtual]
notToIff(const Theorem &not_e)CVC3::CommonTheoremProducer [virtual]
queryTCC(const Theorem &phi, const Theorem &D_phi)CVC3::CommonTheoremProducer [virtual]
reflexivityRule(const Expr &a)CVC3::CommonTheoremProducer [virtual]
rewriteAnd(const Expr &e)CVC3::CommonTheoremProducer [virtual]
rewriteAnd(const Theorem &e)CVC3::CommonTheoremProducer [virtual]
rewriteIff(const Expr &e)CVC3::CommonTheoremProducer [virtual]
rewriteIteFalse(const Expr &e)CVC3::CommonTheoremProducer [virtual]
rewriteIteSame(const Expr &e)CVC3::CommonTheoremProducer [virtual]
rewriteIteTrue(const Expr &e)CVC3::CommonTheoremProducer [virtual]
rewriteNotExists(const Expr &existsExpr)CVC3::CommonTheoremProducer [virtual]
rewriteNotFalse(const Expr &e)CVC3::CommonTheoremProducer [virtual]
rewriteNotForall(const Expr &forallExpr)CVC3::CommonTheoremProducer [virtual]
rewriteNotNot(const Expr &e)CVC3::CommonTheoremProducer [virtual]
rewriteNotTrue(const Expr &e)CVC3::CommonTheoremProducer [virtual]
rewriteOr(const Expr &e)CVC3::CommonTheoremProducer [virtual]
rewriteOr(const Theorem &e)CVC3::CommonTheoremProducer [virtual]
rewriteReflexivity(const Expr &t)CVC3::CommonTheoremProducer [virtual]
rewriteUsingSymmetry(const Expr &a1_eq_a2)CVC3::CommonTheoremProducer [virtual]
skolemize(const Expr &e)CVC3::CommonTheoremProducer [virtual]
skolemize(const Theorem &thm)CVC3::CommonTheoremProducer [virtual]
skolemizeRewrite(const Expr &e)CVC3::CommonTheoremProducer [virtual]
skolemizeRewriteVar(const Expr &e)CVC3::CommonTheoremProducer [virtual]
soundError(const std::string &file, int line, const std::string &cond, const std::string &msg)CVC3::TheoremProducer [protected]
substitutivityRule(const Expr &e, const Theorem &thm)CVC3::CommonTheoremProducer [virtual]
substitutivityRule(const Expr &e, const Theorem &thm1, const Theorem &thm2)CVC3::CommonTheoremProducer [virtual]
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)CVC3::CommonTheoremProducer [virtual]
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)CVC3::CommonTheoremProducer [virtual]
substitutivityRule(const Expr &e, const int changed, const Theorem &thm)CVC3::CommonTheoremProducer [virtual]
symmetryRule(const Theorem &a1_eq_a2)CVC3::CommonTheoremProducer [virtual]
TheoremProducer(TheoremManager *tm)CVC3::TheoremProducer
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVC3::CommonTheoremProducer [virtual]
trueTheorem()CVC3::CommonTheoremProducer [virtual]
varIntroRule(const Expr &e)CVC3::CommonTheoremProducer [virtual]
varIntroSkolem(const Expr &e)CVC3::CommonTheoremProducer [virtual]
withAssumptions()CVC3::TheoremProducer [inline]
withProof()CVC3::TheoremProducer [inline]
xorToIff(const Expr &e)CVC3::CommonTheoremProducer [virtual]
~CommonProofRules()CVC3::CommonProofRules [inline, virtual]
~CommonTheoremProducer()CVC3::CommonTheoremProducer [inline, virtual]
~TheoremProducer()CVC3::TheoremProducer [inline, virtual]


Generated on Wed Nov 18 16:18:01 2009 for CVC3 by  doxygen 1.5.2