CVC3: SAT::CNF_Manager Class Reference

CNF_Manager::CNF_Manager	(	CVC3::TheoremManager *	tm,
		CVC3::Statistics &	statistics,
		bool	minimizeClauses
	)

Definition at line 35 of file cnf_manager.cpp.

References createProofRules(), d_rules, d_varInfo, d_vc, and CVC3::CLFlags::setFlag().

CNF_Manager::~CNF_Manager ( )

Definition at line 57 of file cnf_manager.cpp.

References d_rules, and d_vc.

CNF_Rules * CNF_Manager::createProofRules ( CVC3::TheoremManager * tm ) [private]

Definition at line 38 of file cnf_theorem_producer.cpp.

Referenced by CNF_Manager().

void CNF_Manager::registerAtom	(	const CVC3::Expr &	e,
		const CVC3::Theorem &	thm
	)			`[private]`

Register a new atomic formula.

Definition at line 64 of file cnf_manager.cpp.

References d_cnfCallback, DebugAssert, CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isUserRegisteredAtom(), and SAT::CNF_Manager::CNFCallback::registerAtom().

Referenced by translateExprRec().

Lit CNF_Manager::translateExprRec	(	const CVC3::Expr &	e,
		CNF_Formula &	cnf,
		const CVC3::Theorem &	thmIn
	)			`[private]`

Recursively translate e into cnf.

A non-context dependent cache, d_cnfVars is used to remember translations of expressions. A context-dependent attribute, isTranslated, is used to remember whether an expression has been translated in the current context

Definition at line 128 of file cnf_manager.cpp.

References SAT::CNF_Formula::addLiteral(), CVC3::AND, CVC3::Expr::begin(), d_bottomScope, d_cnfVars, d_translateQueueThms, d_translateQueueVars, d_varInfo, DebugAssert, CVC3::Expr::end(), getCNFLit(), SAT::Lit::getFalse(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), SAT::Lit::getTrue(), SAT::Lit::getVar(), CVC3::IFF, CVC3::IMPLIES, CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), SAT::Lit::isNull(), CVC3::Expr::isTranslated(), CVC3::Expr::isTrue(), SAT::Lit::isVar(), CVC3::ITE, SAT::CNF_Formula::newClause(), CVC3::OR, registerAtom(), replaceITErec(), CVC3::Expr::setTranslated(), and CVC3::XOR.

Referenced by translateExpr().

Theorem CNF_Manager::replaceITErec	(	const CVC3::Expr &	e,
		Var	v,
		bool	translateOnly
	)			`[private]`

Recursively traverse an expression with an embedded term ITE.

Term ITE's are handled by introducing a skolem variable for the ITE term and then adding new constraints describing the ITE in terms of the new variable.

Definition at line 71 of file cnf_manager.cpp.

References d_commonRules, d_iteMap, d_rules, d_translateQueueFlags, d_translateQueueThms, d_translateQueueVars, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::CommonProofRules::iffMP(), CVC3::CNF_Rules::ifLiftRule(), CVC3::Expr::isAtomic(), CVC3::ITE, CVC3::CommonProofRules::reflexivityRule(), CVC3::CommonProofRules::substitutivityRule(), CVC3::CommonProofRules::symmetryRule(), and CVC3::CommonProofRules::varIntroSkolem().

Referenced by translateExprRec().

Lit CNF_Manager::translateExpr	(	const CVC3::Theorem &	thmIn,
		CNF_Formula &	cnf
	)			`[private]`

Recursively translate e into cnf.

Call translateExprRec. If additional expressions are queued up, translate them too, until none are left.

Definition at line 341 of file cnf_manager.cpp.

References SAT::CNF_Formula::addLiteral(), d_clauseIdNext, d_translateQueueFlags, d_translateQueueThms, d_translateQueueVars, d_varInfo, FatalAssert, SAT::CNF_Formula::getCurrentClause(), CVC3::Theorem::getExpr(), SAT::Lit::getVar(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setId(), and translateExprRec().

Referenced by addAssumption(), and addLemma().

void SAT::CNF_Manager::registerCNFCallback ( CNFCallback * cnfCallback ) [inline]

Register CNF callback.

Definition at line 149 of file cnf_manager.h.

References d_cnfCallback.

Referenced by CVC3::SearchSat::SearchSat().

void SAT::CNF_Manager::setBottomScope ( int scope ) [inline]

Set scope for translation.

Definition at line 153 of file cnf_manager.h.

References d_bottomScope.

Referenced by CVC3::SearchSat::check().

unsigned SAT::CNF_Manager::numVars ( ) [inline]

Return the number of variables being managed.

Definition at line 156 of file cnf_manager.h.

References d_varInfo.

Referenced by CVC3::SearchSat::getNewClauses(), and CVC3::SearchSat::newUserAssumptionInt().

unsigned SAT::CNF_Manager::numFanins ( Lit c ) [inline]

Return number of fanins for CNF node c.

A CNF node x is a fanin of CNF node y if the expr for x is a child of the expr for y or if y is an ITE leaf and x is a new CNF node obtained by translating the ITE leaf y.

See also:: isITELeaf()

Definition at line 164 of file cnf_manager.h.

References d_varInfo, SAT::Lit::getVar(), and SAT::Lit::isVar().

Referenced by CVC3::SearchSat::findSplitterRec(), and getFanin().

Lit SAT::CNF_Manager::getFanin	(	Lit	c,
		unsigned	i
	)			`[inline]`

Returns the ith fanin of c.

Definition at line 172 of file cnf_manager.h.

References d_varInfo, DebugAssert, SAT::Lit::getVar(), and numFanins().

Referenced by CVC3::SearchSat::findSplitterRec().

unsigned SAT::CNF_Manager::numFanouts ( Lit c ) [inline]

Return number of fanins for c.

x is a fanout of y if y is a fanin of x

See also:: numFanins

Definition at line 181 of file cnf_manager.h.

References d_varInfo, SAT::Lit::getVar(), and SAT::Lit::isVar().

Referenced by getFanout().

Lit SAT::CNF_Manager::getFanout	(	Lit	c,
		unsigned	i
	)			`[inline]`

Returns the ith fanout of c.

Definition at line 189 of file cnf_manager.h.

References d_varInfo, DebugAssert, SAT::Lit::getVar(), and numFanouts().

CVC3::Expr SAT::CNF_Manager::concreteLit	(	Lit	l,
		bool	checkTranslated = `true`
	)			`[inline]`

Convert a CNF literal to an Expr literal.

Returns a NULL Expr if there is no corresponding Expr for l

Definition at line 197 of file cnf_manager.h.

References d_varInfo, SAT::Lit::getVar(), SAT::Lit::isNull(), and SAT::Lit::isPositive().

Referenced by CVC3::SearchSat::assertLit(), CVC3::SearchSat::checkJustified(), CVC3::SearchSat::findSplitterRec(), CVC3::SearchSat::getExplanation(), and CVC3::SearchSat::setJustified().

Lit SAT::CNF_Manager::getCNFLit ( const CVC3::Expr & e ) [inline]

Look up the CNF literal for an Expr.

Returns a NULL Lit if there is no corresponding CNF literal for e

Definition at line 210 of file cnf_manager.h.

References d_cnfVars, SAT::Lit::getFalse(), SAT::Lit::getTrue(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Expr::isTranslated(), and CVC3::Expr::isTrue().

Referenced by convertLemma(), CVC3::SearchSat::getImplication(), and translateExprRec().

void CNF_Manager::cons	(	unsigned	lb,
		unsigned	ub,
		const CVC3::Expr &	e2,
		std::vector< unsigned > &	newLits
	)

Definition at line 372 of file cnf_manager.cpp.

References CVC3::ValidityChecker::assertFormula(), d_vc, CVC3::ValidityChecker::falseExpr(), CVC3::Expr::negate(), CVC3::ValidityChecker::pop(), CVC3::ValidityChecker::push(), CVC3::ValidityChecker::query(), and CVC3::VALID.

Referenced by convertLemma().

void CNF_Manager::convertLemma	(	const CVC3::Theorem &	thm,
		Clause &	c
	)

Convert thm A |- B (A is a set of literals) into a clause ~A \/ B.

c should be an empty clause that will be filled with the result

Definition at line 415 of file cnf_manager.cpp.

References SAT::Clause::addLiteral(), CVC3::Expr::arity(), CVC3::Expr::begin(), cons(), CVC3::Statistics::counter(), d_clauseIdNext, d_minimizeClauses, d_rules, d_statistics, d_vc, DebugAssert, CVC3::Expr::end(), FatalAssert, getCNFLit(), CVC3::Theorem::getExpr(), IF_DEBUG, CVC3::ValidityChecker::importExpr(), SAT::Lit::isNull(), CVC3::Expr::isOr(), CVC3::CNF_Rules::learnedClause(), CVC3::OR, CVC3::ValidityChecker::pop(), CVC3::ValidityChecker::push(), CVC3::ValidityChecker::query(), CVC3::ValidityChecker::scopeLevel(), SAT::Clause::setId(), SAT::Clause::setUnit(), SAT::Clause::size(), and CVC3::VALID.

Referenced by CVC3::SearchSat::checkConsistent(), and CVC3::SearchSat::getExplanation().

Lit CNF_Manager::addAssumption	(	const CVC3::Theorem &	thm,
		CNF_Formula &	cnf
	)

Given thm of form A |- B, convert B to CNF and add it to cnf.

Returns Lit corresponding to the root of the expression that was translated.

Definition at line 469 of file cnf_manager.cpp.

References SAT::CNF_Formula::addLiteral(), d_clauseIdNext, FatalAssert, SAT::CNF_Formula::getCurrentClause(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setId(), and translateExpr().

Referenced by CVC3::SearchSat::assertLit(), and CVC3::SearchSat::newUserAssumptionInt().

Lit CNF_Manager::addLemma	(	const CVC3::Theorem &	thm,
		CNF_Formula &	cnf
	)

Convert thm to CNF and add it to the current formula.

Parameters:

	thm	should be of form A \|- B where A is a set of literals.
	cnf	the new clauses are added to cnf. Returns Lit corresponding to the root of the expression that was translated.

Definition at line 484 of file cnf_manager.cpp.

References SAT::CNF_Formula::addLiteral(), d_clauseIdNext, d_rules, FatalAssert, SAT::CNF_Formula::getCurrentClause(), CVC3::CNF_Rules::learnedClause(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setId(), and translateExpr().

Referenced by CVC3::SearchSat::getNewClauses().

CVC3::ValidityChecker* SAT::CNF_Manager::d_vc [private]

For clause minimization.

Definition at line 44 of file cnf_manager.h.

Referenced by CNF_Manager(), cons(), convertLemma(), and ~CNF_Manager().

bool SAT::CNF_Manager::d_minimizeClauses [private]

Whether to use brute-force clause minimization.

Definition at line 47 of file cnf_manager.h.

Referenced by convertLemma().

CVC3::CommonProofRules* SAT::CNF_Manager::d_commonRules [private]