CVC3
2.4.1
|
Classes | |
class | CVC3::CNF_Rules |
API to the CNF proof rules. More... | |
Functions | |
virtual | CVC3::CNF_Rules::~CNF_Rules () |
Destructor. More... | |
virtual void | CVC3::CNF_Rules::learnedClauses (const Theorem &thm, std::vector< Theorem > &, bool newLemma)=0 |
Learned clause rule:
. More... | |
virtual Theorem | CVC3::CNF_Rules::ifLiftRule (const Expr &e, int itePos)=0 |
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _)) More... | |
virtual Theorem | CVC3::CNF_Rules::CNFAddUnit (const Theorem &thm)=0 |
virtual Theorem | CVC3::CNF_Rules::CNFConvert (const Expr &e, const Theorem &thm)=0 |
virtual Theorem | CVC3::CNF_Rules::CNFtranslate (const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)=0 |
virtual Theorem | CVC3::CNF_Rules::CNFITEtranslate (const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0 |
|
inlinevirtual |
Destructor.
Definition at line 40 of file cnf_rules.h.
|
pure virtual |
Learned clause rule:
.
thm | is the theorem ![]() ![]() ![]() ![]() ![]() |
Implemented in CVC3::CNF_TheoremProducer.
Referenced by SAT::CNF_Manager::addLemma(), and SAT::CNF_Manager::convertLemma().
|
pure virtual |
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
Implemented in CVC3::CNF_TheoremProducer.
Referenced by SAT::CNF_Manager::replaceITErec().
|
pure virtual |
Implemented in CVC3::CNF_TheoremProducer.
Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), and SAT::CNF_Manager::translateExpr().
Implemented in CVC3::CNF_TheoremProducer.
Referenced by SAT::CNF_Manager::convertLemma().
|
pure virtual |
Implemented in CVC3::CNF_TheoremProducer.
Referenced by SAT::CNF_Manager::translateExprRec().
|
pure virtual |
Implemented in CVC3::CNF_TheoremProducer.
Referenced by SAT::CNF_Manager::translateExprRec().