CVC3
|
#include <core_theorem_producer.h>
Inherits CVC3::CoreProofRules, and CVC3::TheoremProducer.
Public Member Functions | |
CoreTheoremProducer (TheoremManager *tm, TheoryCore *core) | |
virtual | ~CoreTheoremProducer () |
Theorem | typePred (const Expr &e) |
e: T ==> |- typePred_T(e) [deriving the type predicate of e] | |
Theorem | rewriteLetDecl (const Expr &e) |
Replace LETDECL with its definition. | |
Theorem | rewriteNotAnd (const Expr &e) |
==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...) | |
Theorem | rewriteNotOr (const Expr &e) |
==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...) | |
Theorem | rewriteNotIff (const Expr &e) |
==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2) | |
Theorem | rewriteNotIte (const Expr &e) |
==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c) | |
Theorem | rewriteIteThen (const Expr &e, const Theorem &thenThm) |
a |- b == d ==> ITE(a, b, c) == ITE(a, d, c) | |
Theorem | rewriteIteElse (const Expr &e, const Theorem &elseThm) |
!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d) | |
Theorem | rewriteIteBool (const Expr &c, const Expr &e1, const Expr &e2) |
==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2) | |
Theorem | orDistributivityRule (const Expr &e) |
|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn) | |
Theorem | andDistributivityRule (const Expr &e) |
|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn) | |
Theorem | rewriteImplies (const Expr &e) |
==> IMPLIES(e1,e2) IFF OR(!e1, e2) | |
Theorem | rewriteDistinct (const Expr &e) |
==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j]) | |
Theorem | NotToIte (const Expr ¬_e) |
==> NOT(e) == ITE(e, FALSE, TRUE) | |
Theorem | OrToIte (const Expr &e) |
==> Or(e) == ITE(e[1], TRUE, e[0]) | |
Theorem | AndToIte (const Expr &e) |
==> And(e) == ITE(e[1], e[0], FALSE) | |
Theorem | IffToIte (const Expr &e) |
==> IFF(a,b) == ITE(a, b, !b) | |
Theorem | ImpToIte (const Expr &e) |
==> IMPLIES(a,b) == ITE(a, b, TRUE) | |
Theorem | rewriteIteToNot (const Expr &e) |
==> ITE(e, FALSE, TRUE) IFF NOT(e) | |
Theorem | rewriteIteToOr (const Expr &e) |
==> ITE(a, TRUE, b) IFF OR(a, b) | |
Theorem | rewriteIteToAnd (const Expr &e) |
==> ITE(a, b, FALSE) IFF AND(a, b) | |
Theorem | rewriteIteToIff (const Expr &e) |
==> ITE(a, b, !b) IFF IFF(a, b) | |
Theorem | rewriteIteToImp (const Expr &e) |
==> ITE(a, b, TRUE) IFF IMPLIES(a, b) | |
Theorem | rewriteIteCond (const Expr &e) |
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE)) | |
Theorem | ifLiftUnaryRule (const Expr &e) |
|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b)) | |
Theorem | iffOrDistrib (const Expr &iff) |
((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff' | |
Theorem | iffAndDistrib (const Expr &iff) |
((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff' | |
Theorem | rewriteAndSubterms (const Expr &e, int idx) |
(a & b) <=> a & b[a/true]; takes the index of a | |
Theorem | rewriteOrSubterms (const Expr &e, int idx) |
(a | b) <=> a | b[a/false]; takes the index of a | |
Theorem | dummyTheorem (const Expr &e) |
Temporary cheat for building theorems. | |
![]() | |
virtual | ~CoreProofRules () |
Destructor. | |
![]() | |
TheoremProducer (TheoremManager *tm) | |
virtual | ~TheoremProducer () |
bool | withProof () |
Testing whether to generate proofs. | |
bool | withAssumptions () |
Testing whether to generate assumptions. | |
Proof | newLabel (const Expr &e) |
Create a new proof label (bound variable) for an assumption (formula) | |
Proof | newPf (const std::string &name) |
Proof | newPf (const std::string &name, const Expr &e) |
Proof | newPf (const std::string &name, const Proof &pf) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2) |
Proof | newPf (const std::string &name, const Expr &e, const Proof &pf) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf) |
Proof | newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end) |
Proof | newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end) |
Proof | newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const std::vector< Expr > &args) |
Proof | newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args) |
Proof | newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf) |
Proof | newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs) |
Proof | newPf (const Proof &label, const Expr &frm, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label formula proof) | |
Proof | newPf (const Proof &label, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label proof). | |
Proof | newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf) |
Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf) | |
Proof | newPf (const std::vector< Proof > &labels, const Proof &pf) |
Private Attributes | |
TheoryCore * | d_core |
pointer to theory core | |
Additional Inherited Members | |
![]() | |
Theorem | newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf) |
Create a new theorem. See also newRWTheorem() and newReflTheorem() | |
Theorem | newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
Create a rewrite theorem: lhs = rhs. | |
Theorem | newReflTheorem (const Expr &e) |
Create a reflexivity theorem. | |
Theorem | newAssumption (const Expr &thm, const Proof &pf, int scope=-1) |
Theorem3 | newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf) |
Theorem3 | newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
void | soundError (const std::string &file, int line, const std::string &cond, const std::string &msg) |
![]() | |
TheoremManager * | d_tm |
ExprManager * | d_em |
const bool * | d_checkProofs |
Op | d_pfOp |
Expr | d_hole |
Definition at line 40 of file core_theorem_producer.h.
|
inline |
Definition at line 46 of file core_theorem_producer.h.
|
inlinevirtual |
Definition at line 48 of file core_theorem_producer.h.
e: T ==> |- typePred_T(e) [deriving the type predicate of e]
Implements CVC3::CoreProofRules.
Definition at line 52 of file core_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), and CVC3::Expr::getType().
Replace LETDECL with its definition.
Used only in TheoryCore
Implements CVC3::CoreProofRules.
Definition at line 64 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), LETDECL, and CVC3::Expr::toString().
==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
Implements CVC3::CoreProofRules.
Definition at line 75 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isAnd(), CVC3::Expr::isNot(), CVC3::orExpr(), and CVC3::Expr::toString().
==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
Implements CVC3::CoreProofRules.
Definition at line 93 of file core_theorem_producer.cpp.
References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), and CVC3::Expr::toString().
==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
Implements CVC3::CoreProofRules.
Definition at line 110 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isIff(), and CVC3::Expr::isNot().
==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
Implements CVC3::CoreProofRules.
Definition at line 123 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), and CVC3::Expr::isNot().
a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
Implements CVC3::CoreProofRules.
Definition at line 136 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::Theorem::isRewrite(), and CVC3::Expr::toString().
!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
Implements CVC3::CoreProofRules.
Definition at line 161 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::Theorem::isRewrite(), and CVC3::Expr::toString().
|
virtual |
==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)
Implements CVC3::CoreProofRules.
Definition at line 186 of file core_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::iteExpr(), CVC3::Expr::orExpr(), and CVC3::Expr::toString().
|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
Implements CVC3::CoreProofRules.
Definition at line 202 of file core_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isAnd(), CVC3::Expr::isOr(), CVC3::orExpr(), and CVC3::Expr::toString().
|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
Implements CVC3::CoreProofRules.
Definition at line 245 of file core_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isAnd(), CVC3::Expr::isOr(), CVC3::Expr::orExpr(), and CVC3::Expr::toString().
==> IMPLIES(e1,e2) IFF OR(!e1, e2)
Implements CVC3::CoreProofRules.
Definition at line 285 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), and CVC3::Expr::isImpl().
==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
Implements CVC3::CoreProofRules.
Definition at line 297 of file core_theorem_producer.cpp.
References AND, CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, DISTINCT, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getEM(), CVC3::Expr::getKind(), and CVC3::ExprManager::trueExpr().
==> NOT(e) == ITE(e, FALSE, TRUE)
Implements CVC3::CoreProofRules.
Definition at line 328 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::Type::isBool(), and CVC3::Expr::isNot().
==> Or(e) == ITE(e[1], TRUE, e[0])
Implements CVC3::CoreProofRules.
Definition at line 345 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Type::isNull(), CVC3::Expr::isOr(), CVC3::Expr::iteExpr(), and CVC3::Expr::toString().
==> And(e) == ITE(e[1], e[0], FALSE)
Implements CVC3::CoreProofRules.
Definition at line 383 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Expr::isAnd(), CVC3::Type::isNull(), CVC3::Expr::iteExpr(), and CVC3::Expr::toString().
==> IFF(a,b) == ITE(a, b, !b)
Implements CVC3::CoreProofRules.
Definition at line 423 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isIff(), and CVC3::Expr::toString().
==> IMPLIES(a,b) == ITE(a, b, TRUE)
Implements CVC3::CoreProofRules.
Definition at line 439 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isImpl(), and CVC3::Expr::toString().
==> ITE(e, FALSE, TRUE) IFF NOT(e)
Implements CVC3::CoreProofRules.
Definition at line 455 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isFalse(), CVC3::Expr::isITE(), CVC3::Expr::isTrue(), and CVC3::Expr::toString().
==> ITE(a, TRUE, b) IFF OR(a, b)
Implements CVC3::CoreProofRules.
Definition at line 467 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::isTrue(), and CVC3::Expr::toString().
==> ITE(a, b, FALSE) IFF AND(a, b)
Implements CVC3::CoreProofRules.
Definition at line 479 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isFalse(), CVC3::Expr::isITE(), and CVC3::Expr::toString().
==> ITE(a, b, !b) IFF IFF(a, b)
Implements CVC3::CoreProofRules.
Definition at line 491 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::negate(), and CVC3::Expr::toString().
==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
Implements CVC3::CoreProofRules.
Definition at line 503 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::isTrue(), and CVC3::Expr::toString().
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
Implements CVC3::CoreProofRules.
Definition at line 516 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), and CVC3::Expr::toString().
|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
Implements CVC3::CoreProofRules.
Definition at line 588 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Expr::iteExpr(), and CVC3::Expr::toString().
((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
Implements CVC3::CoreProofRules.
Definition at line 543 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::iffExpr(), CVC3::Expr::isIff(), and CVC3::Expr::toString().
((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'
Implements CVC3::CoreProofRules.
Definition at line 565 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::iffExpr(), CVC3::Expr::isIff(), and CVC3::Expr::toString().
(a & b) <=> a & b[a/true]; takes the index of a
and rewrites all the other conjuncts.
Implements CVC3::CoreProofRules.
Definition at line 621 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOp(), CVC3::ExprHashMap< Data >::insert(), CVC3::int2string(), CVC3::Expr::isAnd(), and CVC3::Expr::toString().
(a | b) <=> a | b[a/false]; takes the index of a
and rewrites all the other disjuncts.
Implements CVC3::CoreProofRules.
Definition at line 647 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOp(), CVC3::ExprHashMap< Data >::insert(), CVC3::int2string(), CVC3::Expr::isOr(), and CVC3::Expr::toString().
Temporary cheat for building theorems.
Implements CVC3::CoreProofRules.
Definition at line 670 of file core_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump().
|
private |
pointer to theory core
Definition at line 43 of file core_theorem_producer.h.