CVC3  2.4.1
Public Member Functions | Private Attributes | List of all members
CVC3::CNF_TheoremProducer Class Reference

#include <cnf_theorem_producer.h>

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

Public Member Functions

 CNF_TheoremProducer (TheoremManager *tm, const CLFlags &flags)
 
 ~CNF_TheoremProducer ()
 
void getSmartClauses (const Theorem &thm, std::vector< Theorem > &clauses)
 
void learnedClauses (const Theorem &thm, std::vector< Theorem > &clauses, bool newLemma)
 Learned clause rule:

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

. More...

 
Theorem CNFAddUnit (const Theorem &thm)
 
Theorem CNFConvert (const Expr &e, const Theorem &thm)
 
Theorem ifLiftRule (const Expr &e, int itePos)
 |- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _)) More...
 
Theorem CNFtranslate (const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)
 
Theorem CNFITEtranslate (const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)
 
- Public Member Functions inherited from CVC3::CNF_Rules
virtual ~CNF_Rules ()
 Destructor. More...
 
- Public Member Functions inherited from CVC3::TheoremProducer
 TheoremProducer (TheoremManager *tm)
 
virtual ~TheoremProducer ()
 
bool withProof ()
 Testing whether to generate proofs. More...
 
bool withAssumptions ()
 Testing whether to generate assumptions. More...
 
Proof newLabel (const Expr &e)
 Create a new proof label (bound variable) for an assumption (formula) More...
 
Proof newPf (const std::string &name)
 
Proof newPf (const std::string &name, const Expr &e)
 
Proof newPf (const std::string &name, const Proof &pf)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2)
 
Proof newPf (const std::string &name, const Expr &e, const Proof &pf)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)
 
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end)
 
Proof newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)
 
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args)
 
Proof newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args)
 
Proof newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)
 
Proof newPf (const Proof &label, const Expr &frm, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label formula proof) More...
 
Proof newPf (const Proof &label, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label proof). More...
 
Proof newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)
 Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf) More...
 
Proof newPf (const std::vector< Proof > &labels, const Proof &pf)
 

Private Attributes

const CLFlagsd_flags
 
const bool & d_smartClauses
 

Additional Inherited Members

- Protected Member Functions inherited from CVC3::TheoremProducer
Theorem newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf)
 Create a new theorem. See also newRWTheorem() and newReflTheorem() More...
 
Theorem newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 Create a rewrite theorem: lhs = rhs. More...
 
Theorem newReflTheorem (const Expr &e)
 Create a reflexivity theorem. More...
 
Theorem newAssumption (const Expr &thm, const Proof &pf, int scope=-1)
 
Theorem3 newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf)
 
Theorem3 newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 
void soundError (const std::string &file, int line, const std::string &cond, const std::string &msg)
 
- Protected Attributes inherited from CVC3::TheoremProducer
TheoremManagerd_tm
 
ExprManagerd_em
 
const bool * d_checkProofs
 
Op d_pfOp
 
Expr d_hole
 

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

const CLFlags& CVC3::CNF_TheoremProducer::d_flags
private

Definition at line 34 of file cnf_theorem_producer.h.

const bool& CVC3::CNF_TheoremProducer::d_smartClauses
private

Definition at line 35 of file cnf_theorem_producer.h.


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