22 #ifndef _cvc3__core_proof_rules_h_
23 #define _cvc3__core_proof_rules_h_
virtual Theorem ifLiftUnaryRule(const Expr &e)=0
|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
Data structure of expressions in CVC3.
virtual Theorem OrToIte(const Expr &e)=0
==> Or(e) == ITE(e[1], TRUE, e[0])
virtual Theorem rewriteIteToIff(const Expr &e)=0
==> ITE(a, b, !b) IFF IFF(a, b)
virtual Theorem rewriteIteThen(const Expr &e, const Theorem &thenThm)=0
a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
virtual Theorem dummyTheorem(const Expr &e)=0
Temporary cheat for building theorems.
virtual Theorem IffToIte(const Expr &e)=0
==> IFF(a,b) == ITE(a, b, !b)
virtual Theorem rewriteIteCond(const Expr &e)=0
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
virtual Theorem rewriteIteBool(const Expr &c, const Expr &e1, const Expr &e2)=0
==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)
virtual Theorem rewriteIteToAnd(const Expr &e)=0
==> ITE(a, b, FALSE) IFF AND(a, b)
virtual Theorem NotToIte(const Expr ¬_e)=0
==> NOT(e) == ITE(e, FALSE, TRUE)
virtual Theorem andDistributivityRule(const Expr &e)=0
|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
virtual ~CoreProofRules()
Destructor.
virtual Theorem rewriteIteToOr(const Expr &e)=0
==> ITE(a, TRUE, b) IFF OR(a, b)
virtual Theorem ImpToIte(const Expr &e)=0
==> IMPLIES(a,b) == ITE(a, b, TRUE)
virtual Theorem orDistributivityRule(const Expr &e)=0
|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
virtual Theorem rewriteIteToNot(const Expr &e)=0
==> ITE(e, FALSE, TRUE) IFF NOT(e)
virtual Theorem rewriteNotIff(const Expr &e)=0
==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
virtual Theorem rewriteIteToImp(const Expr &e)=0
==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
virtual Theorem typePred(const Expr &e)=0
e: T ==> |- typePred_T(e) [deriving the type predicate of e]
virtual Theorem rewriteAndSubterms(const Expr &e, int idx)=0
(a & b) <=> a & b[a/true]; takes the index of a
virtual Theorem rewriteNotOr(const Expr &e)=0
==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
virtual Theorem rewriteNotAnd(const Expr &e)=0
==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
virtual Theorem rewriteDistinct(const Expr &e)=0
==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
virtual Theorem rewriteLetDecl(const Expr &e)=0
Replace LETDECL with its definition.
virtual Theorem iffOrDistrib(const Expr &iff)=0
((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
virtual Theorem rewriteIteElse(const Expr &e, const Theorem &elseThm)=0
!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
virtual Theorem rewriteNotIte(const Expr &e)=0
==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
virtual Theorem AndToIte(const Expr &e)=0
==> And(e) == ITE(e[1], e[0], FALSE)
virtual Theorem rewriteOrSubterms(const Expr &e, int idx)=0
(a | b) <=> a | b[a/false]; takes the index of a
virtual Theorem iffAndDistrib(const Expr &iff)=0
((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'
virtual Theorem rewriteImplies(const Expr &e)=0
==> IMPLIES(e1,e2) IFF OR(!e1, e2)