CVC3::CNF_TheoremProducer

CVC3::CNF_TheoremProducer Class Reference

#include <cnf_theorem_producer.h>

Inheritance diagram for CVC3::CNF_TheoremProducer:

Inheritance graph

[legend]Collaboration diagram for CVC3::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 30 of file cnf_theorem_producer.h.

Constructor & Destructor Documentation

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

Definition at line 35 of file cnf_theorem_producer.h.

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

Definition at line 36 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$

$A_i$

and

$B$

should be literals $B$

$B$

can also be $\mathrm{FALSE}$

Implements CVC3::CNF_Rules.

Definition at line 48 of file cnf_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::debugger, CVC3::Assumptions::emptyAssump(), std::endl(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::Debug::getOS(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), IF_DEBUG, CVC3::Expr::isFalse(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::OR, CVC3::Debug::trace(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem CNF_TheoremProducer::ifLiftRule	(	const Expr &	e,
		int	itePos
	)			`[virtual]`

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

Implements CVC3::CNF_Rules.

Definition at line 95 of file cnf_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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

Generated on Tue Jul 3 14:40:22 2007 for CVC3 by

doxygen

1.5.1