Public Member Functions | Private Attributes

CVC3::CNF_TheoremProducer Class Reference

#include <cnf_theorem_producer.h>

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

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

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

Member Data Documentation

Definition at line 34 of file cnf_theorem_producer.h.

Definition at line 35 of file cnf_theorem_producer.h.

Referenced by learnedClauses().


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