CVC3
Public Member Functions | Private Attributes

CVC3::CNF_TheoremProducer Class Reference

#include <cnf_theorem_producer.h>

Inherits CVC3::CNF_Rules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::CNF_TheoremProducer:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Attributes


Detailed Description

Definition at line 31 of file cnf_theorem_producer.h.


Constructor & Destructor Documentation

CVC3::CNF_TheoremProducer::CNF_TheoremProducer ( TheoremManager tm,
const CLFlags flags 
) [inline]

Definition at line 38 of file cnf_theorem_producer.h.

CVC3::CNF_TheoremProducer::~CNF_TheoremProducer ( ) [inline]

Definition at line 41 of file cnf_theorem_producer.h.


Member Function Documentation

void CNF_TheoremProducer::getSmartClauses ( const Theorem thm,
std::vector< Theorem > &  clauses 
)
void CNF_TheoremProducer::learnedClauses ( const Theorem thm,
std::vector< Theorem > &  ,
bool  newLemma 
) [virtual]

Learned clause rule:

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

.

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

Implements CVC3::CNF_Rules.

Definition at line 106 of file cnf_theorem_producer.cpp.

References DebugAssert, std::endl(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), IF_DEBUG, CVC3::Expr::isFalse(), and OR.

Theorem CNF_TheoremProducer::CNFAddUnit ( const Theorem thm) [virtual]
Theorem CNF_TheoremProducer::CNFConvert ( const Expr e,
const Theorem thm 
) [virtual]
Theorem CNF_TheoremProducer::ifLiftRule ( const Expr e,
int  itePos 
) [virtual]
Theorem CNF_TheoremProducer::CNFtranslate ( const Expr before,
const Expr after,
std::string  reason,
int  pos,
const std::vector< Theorem > &  thms 
) [virtual]

Implements CVC3::CNF_Rules.

Definition at line 246 of file cnf_theorem_producer.cpp.

Theorem CNF_TheoremProducer::CNFITEtranslate ( const Expr before,
const std::vector< Expr > &  after,
const std::vector< Theorem > &  thms,
int  pos 
) [virtual]

Implements CVC3::CNF_Rules.

Definition at line 271 of file cnf_theorem_producer.cpp.

References DebugAssert, and CVC3::Expr::iteExpr().


Member Data Documentation

Definition at line 34 of file cnf_theorem_producer.h.

Definition at line 35 of file cnf_theorem_producer.h.


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