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