CVC3
Classes | Functions
Proof Rules for the Search Engines

Classes

class  CVC3::CNF_Rules
 API to the CNF proof rules. More...
 

Functions

virtual CVC3::CNF_Rules::~CNF_Rules ()
 Destructor.
 
virtual void CVC3::CNF_Rules::learnedClauses (const Theorem &thm, std::vector< Theorem > &, bool newLemma)=0
 Learned clause rule:

\[\frac{A_1,\ldots,A_n\vdash B} {\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}\]

.

 
virtual Theorem CVC3::CNF_Rules::ifLiftRule (const Expr &e, int itePos)=0
 |- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
 
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
 

Detailed Description

Function Documentation

virtual CVC3::CNF_Rules::~CNF_Rules ( )
inlinevirtual

Destructor.

Definition at line 40 of file cnf_rules.h.

virtual void CVC3::CNF_Rules::learnedClauses ( const Theorem thm,
std::vector< Theorem > &  ,
bool  newLemma 
)
pure virtual

Learned clause rule:

\[\frac{A_1,\ldots,A_n\vdash B} {\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}\]

.

 \param thm is the theorem

$ A_1,\ldots,A_n\vdash B$ Each $A_i$ and $B$ should be literals $B$ can also be $\mathrm{FALSE}$

Implemented in CVC3::CNF_TheoremProducer.

Referenced by SAT::CNF_Manager::addLemma(), and SAT::CNF_Manager::convertLemma().

virtual Theorem CVC3::CNF_Rules::ifLiftRule ( const Expr e,
int  itePos 
)
pure virtual

|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))

Implemented in CVC3::CNF_TheoremProducer.

Referenced by SAT::CNF_Manager::replaceITErec().

virtual Theorem CVC3::CNF_Rules::CNFAddUnit ( const Theorem thm)
pure virtual
virtual Theorem CVC3::CNF_Rules::CNFConvert ( const Expr e,
const Theorem thm 
)
pure virtual
virtual Theorem CVC3::CNF_Rules::CNFtranslate ( const Expr before,
const Expr after,
std::string  reason,
int  pos,
const std::vector< Theorem > &  thms 
)
pure virtual
virtual Theorem CVC3::CNF_Rules::CNFITEtranslate ( const Expr before,
const std::vector< Expr > &  after,
const std::vector< Theorem > &  thms,
int  pos 
)
pure virtual