CVC3: CVC3::CNF_Rules Class Reference

API to the CNF proof rules. More...

#include <cnf_rules.h>

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

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: