CVCL::CNF_TheoremProducer

CVCL::CNF_TheoremProducer Class Reference

#include <cnf_theorem_producer.h>

Inheritance diagram for CVCL::CNF_TheoremProducer:

Inheritance graph

[legend]Collaboration diagram for CVCL::CNF_TheoremProducer:

Collaboration graph

[legend]List of all members.

Public Member Functions

CNF_TheoremProducer (TheoremManager *tm)
~CNF_TheoremProducer ()
Theorem learnedClause (const Theorem &thm)
Learned clause rule:
$\frac{A_1,\ldots,A_n\vdash B} {\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}$
.
Theorem ifLiftRule (const Expr &e, int itePos)
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))

Detailed Description

Definition at line 38 of file cnf_theorem_producer.h.

Constructor & Destructor Documentation

CVCL::CNF_TheoremProducer::CNF_TheoremProducer ( TheoremManager * tm ) [inline]

Definition at line 43 of file cnf_theorem_producer.h.

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

Definition at line 44 of file cnf_theorem_producer.h.

Member Function Documentation

Theorem CNF_TheoremProducer::learnedClause ( const Theorem & thm ) [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:

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

Implements CVCL::CNF_Rules.
Definition at line 56 of file cnf_theorem_producer.cpp.
References CVCL::debugger, std::endl(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLeafAssumptions(), CVCL::Debug::getOS(), CVCL::Theorem::getProof(), IF_DEBUG(), CVCL::Expr::isFalse(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::OR, CVCL::Debug::trace(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CNF_TheoremProducer::ifLiftRule ( const Expr & e,

int itePos

) [virtual]

|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))

Implements CVCL::CNF_Rules.
Definition at line 101 of file cnf_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::TheoremProducer::d_em, CVCL::Expr::getKids(), CVCL::Expr::getOp(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::Type::isBool(), CVCL::Expr::isITE(), CVCL::Expr::iteExpr(), CVCL::TheoremProducer::newPf(), CVCL::ExprManager::newRatExpr(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

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

Generated on Thu Apr 13 16:57:45 2006 for CVC Lite by

doxygen

1.4.4