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