CVC3
Public Member Functions | List of all members
CVC3::CNF_Rules Class Referenceabstract

API to the CNF proof rules. More...

#include <cnf_rules.h>

Inherited by CVC3::CNF_TheoremProducer.

Collaboration diagram for CVC3::CNF_Rules:
Collaboration graph

Public Member Functions

virtual ~CNF_Rules ()
 Destructor.
 
virtual void 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 ifLiftRule (const Expr &e, int itePos)=0
 |- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
 
virtual Theorem CNFAddUnit (const Theorem &thm)=0
 
virtual Theorem CNFConvert (const Expr &e, const Theorem &thm)=0
 
virtual Theorem CNFtranslate (const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)=0
 
virtual Theorem CNFITEtranslate (const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0
 

Detailed Description

API to the CNF proof rules.

Definition at line 34 of file cnf_rules.h.


The documentation for this class was generated from the following file: