30 #ifndef _cvc3__common_theorem_producer_h_
31 #define _cvc3__common_theorem_producer_h_
64 const std::vector<Expr>& assump,
65 const std::vector<Theorem>& tccs);
79 const std::vector<Theorem>& thms);
81 const std::vector<unsigned>& changed,
82 const std::vector<Theorem>& thms);
Theorem liftOneITE(const Expr &e)
Theorem notNotElim(const Theorem &e)
Theorem iffTrue(const Theorem &e)
Data structure of expressions in CVC3.
Theorem rewriteOr(const Expr &e)
==> OR(e1,...,en) IFF [simplified expr]
Theorem rewriteIteSame(const Expr &e)
==> ITE(c, e, e) == e
Theorem rewriteIteTrue(const Expr &e)
==> ITE(TRUE, e1, e2) == e1
void findITE(const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart)
Helper function for liftOneITE.
Theorem trueTheorem()
==> TRUE
Theorem excludedMiddle(const Expr &e)
std::vector< Theorem > & getSkolemAxioms()
Theorem3 implIntro3(const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)
3-valued implication introduction rule:
Theorem skolemizeRewrite(const Expr &e)
Theorem rewriteNotExists(const Expr &existsExpr)
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Theorem rewriteNotTrue(const Expr &e)
==> NOT TRUE IFF FALSE
Theorem reflexivityRule(const Expr &a)
Theorem ackermann(const Expr &e1, const Expr &e2)
Theorem varIntroRule(const Expr &e)
|- EXISTS x. e = x
Theorem rewriteReflexivity(const Expr &t)
==> (a == a) IFF TRUE
Theorem iffNotFalse(const Theorem &e)
Theorem contradictionRule(const Theorem &e, const Theorem ¬_e)
Theorem iffTrueElim(const Theorem &e)
std::vector< Theorem > d_skolem_axioms
CommonTheoremProducer(TheoremManager *tm)
Theorem3 queryTCC(const Theorem &phi, const Theorem &D_phi)
Convert 2-valued formula to 3-valued by discharging its TCC ( ): .
virtual ~CommonTheoremProducer()
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
Theorem varIntroSkolem(const Expr &e)
Retrun a theorem "|- e = v" for a new Skolem constant v.
Theorem andIntro(const Theorem &e1, const Theorem &e2)
e1, e2 ==> AND(e1, e2)
Theorem rewriteNotFalse(const Expr &e)
==> NOT FALSE IFF TRUE
Theorem andElim(const Theorem &e, int i)
Theorem rewriteIteFalse(const Expr &e)
==> ITE(FALSE, e1, e2) == e2
Theorem implMP(const Theorem &e1, const Theorem &e1_impl_e2)
Theorem substitutivityRule(const Expr &e, const Theorem &thm)
Optimized case for expr with one child.
Expr skolemize(const Expr &e)
Theorem rewriteNotForall(const Expr &forallExpr)
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
CDMap< Expr, Theorem > d_skolemized_thms
Theorem skolemizeRewriteVar(const Expr &e)
Special version of skolemizeRewrite for "EXISTS x. t = x".
CDMap< Expr, Theorem > d_skolemVars
Mapping of e to "|- e = v" for fresh Skolem vars v.
Theorem iffFalseElim(const Theorem &e)
Theorem xorToIff(const Expr &e)
Theorem symmetryRule(const Theorem &a1_eq_a2)
(same for IFF)
Theorem assumpRule(const Expr &a, int scope=-1)
Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(same for IFF)
Theorem implIntro(const Theorem &phi, const std::vector< Expr > &assump)
Implication introduction rule: .
Theorem rewriteIff(const Expr &e)
==> (e1 <=> e2) <=> [simplified expr]
Theorem implContrapositive(const Theorem &thm)
e1 => e2 ==> ~e2 => ~e1
Theorem notToIff(const Theorem ¬_e)
Theorem rewriteNotNot(const Expr &e)
==> NOT NOT e IFF e, takes !!e
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
Theorem iffContrapositive(const Theorem &thm)
e1 <=> e2 ==> ~e1 <=> ~e2