CVC3
2.4.1
|
#include <core_proof_rules.h>
Public Member Functions | |
virtual | ~CoreProofRules () |
Destructor. | |
virtual Theorem | typePred (const Expr &e)=0 |
e: T ==> |- typePred_T(e) [deriving the type predicate of e] | |
virtual Theorem | rewriteLetDecl (const Expr &e)=0 |
Replace LETDECL with its definition. | |
virtual Theorem | rewriteNotAnd (const Expr &e)=0 |
==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...) | |
virtual Theorem | rewriteNotOr (const Expr &e)=0 |
==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...) | |
virtual Theorem | rewriteNotIff (const Expr &e)=0 |
==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2) | |
virtual Theorem | rewriteNotIte (const Expr &e)=0 |
==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c) | |
virtual Theorem | rewriteIteThen (const Expr &e, const Theorem &thenThm)=0 |
a |- b == d ==> ITE(a, b, c) == ITE(a, d, c) | |
virtual Theorem | rewriteIteElse (const Expr &e, const Theorem &elseThm)=0 |
!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d) | |
virtual Theorem | rewriteIteBool (const Expr &c, const Expr &e1, const Expr &e2)=0 |
==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2) | |
virtual Theorem | orDistributivityRule (const Expr &e)=0 |
|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn) | |
virtual Theorem | andDistributivityRule (const Expr &e)=0 |
|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn) | |
virtual Theorem | rewriteImplies (const Expr &e)=0 |
==> IMPLIES(e1,e2) IFF OR(!e1, e2) | |
virtual Theorem | rewriteDistinct (const Expr &e)=0 |
==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j]) | |
virtual Theorem | NotToIte (const Expr ¬_e)=0 |
==> NOT(e) == ITE(e, FALSE, TRUE) | |
virtual Theorem | OrToIte (const Expr &e)=0 |
==> Or(e) == ITE(e[1], TRUE, e[0]) | |
virtual Theorem | AndToIte (const Expr &e)=0 |
==> And(e) == ITE(e[1], e[0], FALSE) | |
virtual Theorem | IffToIte (const Expr &e)=0 |
==> IFF(a,b) == ITE(a, b, !b) | |
virtual Theorem | ImpToIte (const Expr &e)=0 |
==> IMPLIES(a,b) == ITE(a, b, TRUE) | |
virtual Theorem | rewriteIteToNot (const Expr &e)=0 |
==> ITE(e, FALSE, TRUE) IFF NOT(e) | |
virtual Theorem | rewriteIteToOr (const Expr &e)=0 |
==> ITE(a, TRUE, b) IFF OR(a, b) | |
virtual Theorem | rewriteIteToAnd (const Expr &e)=0 |
==> ITE(a, b, FALSE) IFF AND(a, b) | |
virtual Theorem | rewriteIteToIff (const Expr &e)=0 |
==> ITE(a, b, !b) IFF IFF(a, b) | |
virtual Theorem | rewriteIteToImp (const Expr &e)=0 |
==> ITE(a, b, TRUE) IFF IMPLIES(a, b) | |
virtual Theorem | rewriteIteCond (const Expr &e)=0 |
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE)) | |
virtual Theorem | ifLiftUnaryRule (const Expr &e)=0 |
|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b)) | |
virtual Theorem | iffOrDistrib (const Expr &iff)=0 |
((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff' | |
virtual Theorem | iffAndDistrib (const Expr &iff)=0 |
((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff' | |
virtual Theorem | rewriteAndSubterms (const Expr &e, int idx)=0 |
(a & b) <=> a & b[a/true]; takes the index of a | |
virtual Theorem | rewriteOrSubterms (const Expr &e, int idx)=0 |
(a | b) <=> a | b[a/false]; takes the index of a | |
virtual Theorem | dummyTheorem (const Expr &e)=0 |
Temporary cheat for building theorems. |
Definition at line 34 of file core_proof_rules.h.
|
inlinevirtual |
Destructor.
Definition at line 37 of file core_proof_rules.h.
e: T ==> |- typePred_T(e) [deriving the type predicate of e]
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::setupTerm(), and CVC3::TheoryCore::typePred().
Replace LETDECL with its definition.
Used only in TheoryCore
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), and CVC3::TheoryCore::rewrite().
==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::ExprTransform::pushNegation1(), and CVC3::ExprTransform::pushNegationRec().
==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::ExprTransform::pushNegation1(), and CVC3::ExprTransform::pushNegationRec().
==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
Implemented in CVC3::CoreTheoremProducer.
==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::ExprTransform::pushNegation1(), and CVC3::ExprTransform::pushNegationRec().
|
pure virtual |
a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::ExprTransform::newPPrec().
|
pure virtual |
!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::ExprTransform::newPPrec().
|
pure virtual |
==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)
Implemented in CVC3::CoreTheoremProducer.
|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
Implemented in CVC3::CoreTheoremProducer.
|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
Implemented in CVC3::CoreTheoremProducer.
==> IMPLIES(e1,e2) IFF OR(!e1, e2)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryCore::rewrite(), and CVC3::TheoryCore::simplifyOp().
==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite().
==> NOT(e) == ITE(e, FALSE, TRUE)
Implemented in CVC3::CoreTheoremProducer.
==> Or(e) == ITE(e[1], TRUE, e[0])
Implemented in CVC3::CoreTheoremProducer.
==> And(e) == ITE(e[1], e[0], FALSE)
Implemented in CVC3::CoreTheoremProducer.
==> IFF(a,b) == ITE(a, b, !b)
Implemented in CVC3::CoreTheoremProducer.
==> IMPLIES(a,b) == ITE(a, b, TRUE)
Implemented in CVC3::CoreTheoremProducer.
==> ITE(e, FALSE, TRUE) IFF NOT(e)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite().
==> ITE(a, TRUE, b) IFF OR(a, b)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite().
==> ITE(a, b, FALSE) IFF AND(a, b)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite().
==> ITE(a, b, !b) IFF IFF(a, b)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite().
==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite().
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite(), and CVC3::ExprTransform::simplifyWithCare().
|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
Implemented in CVC3::CoreTheoremProducer.
((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
Implemented in CVC3::CoreTheoremProducer.
((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'
Implemented in CVC3::CoreTheoremProducer.
(a & b) <=> a & b[a/true]; takes the index of a
and rewrites all the other conjuncts.
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite().
(a | b) <=> a | b[a/false]; takes the index of a
and rewrites all the other disjuncts.
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite().
Temporary cheat for building theorems.
Implemented in CVC3::CoreTheoremProducer.
Referenced by CVC3::ExprTransform::simplifyWithCare().