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

API to the CNF proof rules. More...

#include <cnf_rules.h>

Inheritance diagram for CVC3::CNF_Rules:
CVC3::CNF_TheoremProducer

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: