CVC3::CNF_TheoremProducer Class Reference

#include <cnf_theorem_producer.h>

Inheritance diagram for CVC3::CNF_TheoremProducer:

[legend]

Collaboration diagram for CVC3::CNF_TheoremProducer:

[legend]

List of all members.

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}$
.
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, _))
Theorem CNFtranslate (const Expr &before, const Expr &after, std::string reason, int pos)
Theorem CNFITEtranslate (const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)

Private Attributes

const CLFlags & d_flags
const bool & d_smartClauses

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
	)

Definition at line 49 of file cnf_theorem_producer.cpp.

References CVC3::Theorem::clearAllFlags(), CVC3::Assumptions::emptyAssump(), FatalAssert, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), CVC3::Theorem::GetSatAssumptions(), CVC3::Expr::isFalse(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::OR, CVC3::Theorem::setQuantLevel(), and CVC3::TheoremProducer::withProof().

Referenced by learnedClauses().

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:

thm

is the theorem $A_1,\ldots,A_n\vdash B$ Each $A_i$

and

should be literals $B$

can also be $\mathrm{FALSE}$

Implements CVC3::CNF_Rules.

Definition at line 97 of file cnf_theorem_producer.cpp.

References d_smartClauses, DebugAssert, CVC3::Assumptions::emptyAssump(), std::endl(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), getSmartClauses(), IF_DEBUG, CVC3::Expr::isFalse(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::OR, and CVC3::TheoremProducer::withProof().

Theorem CNF_TheoremProducer::CNFAddUnit ( const Theorem & thm ) [virtual]

Implements CVC3::CNF_Rules.

Definition at line 295 of file cnf_theorem_producer.cpp.

References CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

Theorem CNF_TheoremProducer::CNFConvert	(	const Expr &	e,
		const Theorem &	thm
	)			`[virtual]`

Implements CVC3::CNF_Rules.

Definition at line 305 of file cnf_theorem_producer.cpp.

References DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), 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 199 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::int2string(), 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().

Theorem CNF_TheoremProducer::CNFtranslate	(	const Expr &	before,
		const Expr &	after,
		std::string	reason,
		int	pos
	)			`[virtual]`

Implements CVC3::CNF_Rules.

Definition at line 237 of file cnf_theorem_producer.cpp.

References CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::ExprManager::newStringExpr(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

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 255 of file cnf_theorem_producer.cpp.

References CVC3::TheoremProducer::d_em, DebugAssert, CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

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.

Referenced by learnedClauses().

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