CVC3
2.4.1
|
#include <cnf_theorem_producer.h>
Public Member Functions | |
CNF_TheoremProducer (TheoremManager *tm, const CLFlags &flags) | |
~CNF_TheoremProducer () | |
void | getSmartClauses (const Theorem &thm, std::vector< Theorem > &clauses) |
void | learnedClauses (const Theorem &thm, std::vector< Theorem > &clauses, bool newLemma) |
Learned clause rule:
| |
Theorem | CNFAddUnit (const Theorem &thm) |
Theorem | CNFConvert (const Expr &e, const Theorem &thm) |
Theorem | ifLiftRule (const Expr &e, int itePos) |
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _)) | |
Theorem | CNFtranslate (const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms) |
Theorem | CNFITEtranslate (const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos) |
![]() | |
virtual | ~CNF_Rules () |
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 | |
const CLFlags & | d_flags |
const bool & | d_smartClauses |
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 31 of file cnf_theorem_producer.h.
|
inline |
Definition at line 38 of file cnf_theorem_producer.h.
|
inline |
Definition at line 41 of file cnf_theorem_producer.h.
Definition at line 49 of file cnf_theorem_producer.cpp.
References CVC3::Theorem::clearAllFlags(), FatalAssert, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), CVC3::Theorem::GetSatAssumptions(), CVC3::Expr::isFalse(), OR, and CVC3::Theorem::setQuantLevel().
|
virtual |
Learned clause rule:
.
\param thm is the theorem
Each
and
should be literals
can also be
Implements CVC3::CNF_Rules.
Definition at line 106 of file cnf_theorem_producer.cpp.
References DebugAssert, std::endl(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), IF_DEBUG, CVC3::Expr::isFalse(), and OR.
Implements CVC3::CNF_Rules.
Definition at line 311 of file cnf_theorem_producer.cpp.
References CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), and CVC3::Theorem::getProof().
Implements CVC3::CNF_Rules.
Definition at line 321 of file cnf_theorem_producer.cpp.
References DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), and CVC3::Expr::isOr().
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
Implements CVC3::CNF_Rules.
Definition at line 208 of file cnf_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getKids(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Expr::iteExpr(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::CNF_Rules.
Definition at line 246 of file cnf_theorem_producer.cpp.
|
virtual |
Implements CVC3::CNF_Rules.
Definition at line 271 of file cnf_theorem_producer.cpp.
References DebugAssert, and CVC3::Expr::iteExpr().
|
private |
Definition at line 34 of file cnf_theorem_producer.h.
|
private |
Definition at line 35 of file cnf_theorem_producer.h.