#include <cnf_manager.h>

Collaboration diagram for SAT::CNF_Manager:

[legend]

List of all members.

Classes

class CNFCallback
Abstract class for callbacks. More...
struct Varinfo
Information kept for each CNF variable. More...

Public Member Functions

CNF_Manager (CVC3::TheoremManager *tm, CVC3::Statistics &statistics, const CVC3::CLFlags &flags)
~CNF_Manager ()
void registerCNFCallback (CNFCallback *cnfCallback)
Register CNF callback.
void setBottomScope (int scope)
Set scope for translation.
unsigned numVars ()
Return the number of variables being managed.
unsigned numFanins (Var c)
Return number of fanins for CNF node c.
Lit getFanin (Var c, unsigned i)
Returns the ith fanin of c.
unsigned numFanouts (Var c)
Return number of fanins for c.
Lit getFanout (Var c, unsigned i)
Returns the ith fanout of c.
const CVC3::Expr & concreteVar (Var v)
Convert a CNF literal to an Expr literal.
CVC3::Expr concreteLit (Lit l, bool checkTranslated=true)
Convert a CNF literal to an Expr literal.
Lit getCNFLit (const CVC3::Expr &e)
Look up the CNF literal for an Expr.
void cons (unsigned lb, unsigned ub, const CVC3::Expr &e2, std::vector< unsigned > &newLits)
void convertLemma (const CVC3::Theorem &thm, CNF_Formula &cnf)
Convert thm A |- B (A is a set of literals) into one or more clauses.
Lit addAssumption (const CVC3::Theorem &thm, CNF_Formula &cnf)
Given thm of form A |- B, convert B to CNF and add it to cnf.
Lit addLemma (CVC3::Theorem thm, CNF_Formula &cnf)
Convert thm to CNF and add it to the current formula.

Private Member Functions

CVC3::CNF_Rules * createProofRules (CVC3::TheoremManager *tm, const CVC3::CLFlags &)
void registerAtom (const CVC3::Expr &e, const CVC3::Theorem &thm)
Register a new atomic formula.
CVC3::Expr concreteExpr (const CVC3::Expr &e, const Lit &literal)
Return the expr corresponding to the literal unless the expr is TRUE of FALSE.
CVC3::Theorem concreteThm (const CVC3::Expr &e)
Return the theorem if e is not as concreteExpr(e).
Lit translateExprRec (const CVC3::Expr &e, CNF_Formula &cnf, const CVC3::Theorem &thmIn)
Recursively translate e into cnf.
CVC3::Theorem replaceITErec (const CVC3::Expr &e, Var v, bool translateOnly)
Recursively traverse an expression with an embedded term ITE.
Lit translateExpr (const CVC3::Theorem &thmIn, CNF_Formula &cnf)
Recursively translate e into cnf.

Private Attributes

CVC3::ValidityChecker * d_vc
For clause minimization.
bool d_minimizeClauses
Whether to use brute-force clause minimization.
CVC3::CommonProofRules * d_commonRules
Common proof rules.
CVC3::CNF_Rules * d_rules
Rules for manipulating CNF.
std::vector< Varinfo > d_varInfo
vector that maps a variable index to information for that variable
CVC3::ExprHashMap< Var > d_cnfVars
Map from Exprs to Vars representing those Exprs.
CVC3::ExprHashMap< CVC3::Theorem > d_iteMap
Cached translation of term-ite-containing expressions.
int d_clauseIdNext
Map of possibly useful lemmas.
int d_bottomScope
Whether expr has already been translated.
std::deque< CVC3::Theorem > d_translateQueueThms
Queue of theorems to translate.
std::deque< Var > d_translateQueueVars
Queue of fanouts corresponding to thms to translate.
std::deque< bool > d_translateQueueFlags
Whether thm to translate is "translate only".
CVC3::Statistics & d_statistics
Reference to statistics object.
const CVC3::CLFlags & d_flags
Reference to command-line flags.
const CVC3::Expr & d_nullExpr
Reference to null Expr.
CNFCallback * d_cnfCallback
Instance of CNF_CallBack: must be registered.

Detailed Description

Definition at line 41 of file cnf_manager.h.

Constructor & Destructor Documentation

CNF_Manager::CNF_Manager	(	CVC3::TheoremManager *	tm,
		CVC3::Statistics &	statistics,
		const CVC3::CLFlags &	flags
	)

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 60 of file cnf_manager.cpp.

References d_rules, and d_vc.

Member Function Documentation

CNF_Rules * CNF_Manager::createProofRules	(	CVC3::TheoremManager *	tm,
		const CVC3::CLFlags &	flags
	)		`[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 67 of file cnf_manager.cpp.

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

Referenced by translateExprRec().

Expr CNF_Manager::concreteExpr	(	const CVC3::Expr &	e,
		const Lit &	literal
	)		`[private]`

Return the expr corresponding to the literal unless the expr is TRUE of FALSE.

Definition at line 131 of file cnf_manager.cpp.

References concreteLit(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), and CVC3::Expr::isTrue().

Referenced by translateExprRec().

Theorem CNF_Manager::concreteThm ( const CVC3::Expr & e ) [private]

Return the theorem if e is not as concreteExpr(e).

Definition at line 139 of file cnf_manager.cpp.

References d_commonRules, d_iteMap, CVC3::Theorem::isNull(), and CVC3::CommonProofRules::reflexivityRule().

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 147 of file cnf_manager.cpp.

References SAT::CNF_Formula::addLiteral(), AND, CVC3::Expr::begin(), CVC3::CNF_Rules::CNFITEtranslate(), CVC3::CNF_Rules::CNFtranslate(), concreteExpr(), concreteThm(), d_bottomScope, d_cnfVars, d_commonRules, d_flags, d_iteMap, d_rules, d_translateQueueThms, d_translateQueueVars, d_varInfo, DebugAssert, CVC3::Expr::end(), CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), getCNFLit(), SAT::CNF_Formula::getCurrentClause(), SAT::Lit::getFalse(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), SAT::Lit::getTrue(), SAT::Lit::getVar(), IFF, CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), IMPLIES, CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::isEq(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), SAT::Lit::isNull(), CVC3::Theorem::isNull(), CVC3::Expr::isTranslated(), CVC3::Expr::isTrue(), SAT::Lit::isVar(), ITE, MiniSat::left(), SAT::CNF_Formula::newClause(), OR, CVC3::CommonProofRules::reflexivityRule(), registerAtom(), replaceITErec(), MiniSat::right(), SAT::Clause::setClauseTheorem(), CVC3::Expr::setTranslated(), XOR, and CVC3::Expr::xorExpr().

Referenced by addAssumption(), and 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 74 of file cnf_manager.cpp.

References CVC3::Expr::begin(), d_commonRules, d_iteMap, d_rules, d_translateQueueFlags, d_translateQueueThms, d_translateQueueVars, DebugAssert, CVC3::Expr::end(), CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::CommonProofRules::iffMP(), CVC3::CNF_Rules::ifLiftRule(), CVC3::Expr::isAtomic(), CVC3::Type::isBool(), CVC3::Theorem::isRefl(), 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 510 of file cnf_manager.cpp.

References SAT::CNF_Formula::addLiteral(), CVC3::CNF_Rules::CNFAddUnit(), d_rules, d_translateQueueFlags, d_translateQueueThms, d_translateQueueVars, d_varInfo, SAT::CNF_Formula::getCurrentClause(), CVC3::Theorem::getExpr(), SAT::Lit::getVar(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setClauseTheorem(), and translateExprRec().

Referenced by addAssumption(), and addLemma().

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

Register CNF callback.

Definition at line 166 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 170 of file cnf_manager.h.

References d_bottomScope.

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

Return the number of variables being managed.

Definition at line 173 of file cnf_manager.h.

References d_varInfo.

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

unsigned SAT::CNF_Manager::numFanins ( Var 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 181 of file cnf_manager.h.

References d_varInfo, and SAT::Var::isVar().

Referenced by getFanin().

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

Returns the ith fanin of c.

Definition at line 188 of file cnf_manager.h.

References d_varInfo, DebugAssert, and numFanins().

unsigned SAT::CNF_Manager::numFanouts ( Var 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 197 of file cnf_manager.h.

References d_varInfo, and SAT::Var::isVar().

Referenced by getFanout().

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

Returns the ith fanout of c.

Definition at line 204 of file cnf_manager.h.

References d_varInfo, DebugAssert, and numFanouts().

const CVC3::Expr& SAT::CNF_Manager::concreteVar ( Var v ) [inline]

Convert a CNF literal to an Expr literal.

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

Definition at line 212 of file cnf_manager.h.

References d_nullExpr, d_varInfo, and SAT::Var::isNull().

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 223 of file cnf_manager.h.

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

Referenced by CVC3::SearchSat::checkJustified(), concreteExpr(), generateSatProof(), 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 236 of file cnf_manager.h.

References d_cnfVars, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), SAT::Lit::getFalse(), SAT::Lit::getTrue(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Expr::isTranslated(), and CVC3::Expr::isTrue().

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

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

Definition at line 550 of file cnf_manager.cpp.

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

void CNF_Manager::convertLemma	(	const CVC3::Theorem &	thm,
		CNF_Formula &	cnf
	)

Convert thm A |- B (A is a set of literals) into one or more clauses.

cnf should be empty -- it will be filled with the result

Definition at line 593 of file cnf_manager.cpp.

References SAT::CNF_Formula::addLiteral(), CVC3::Expr::begin(), CVC3::CNF_Rules::CNFAddUnit(), CVC3::CNF_Rules::CNFConvert(), d_rules, DebugAssert, SAT::CNF_Formula::empty(), CVC3::Expr::end(), getCNFLit(), SAT::CNF_Formula::getCurrentClause(), SAT::Lit::isNull(), CVC3::Expr::isOr(), CVC3::CNF_Rules::learnedClauses(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), and SAT::Clause::setClauseTheorem().

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 623 of file cnf_manager.cpp.

References SAT::CNF_Formula::addLiteral(), CVC3::Expr::arity(), CVC3::CNF_Rules::CNFAddUnit(), d_flags, d_rules, DebugAssert, SAT::CNF_Formula::getCurrentClause(), CVC3::Theorem::getExpr(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Expr::isTrue(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setClauseTheorem(), CVC3::Expr::toString(), translateExpr(), and translateExprRec().

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

Lit CNF_Manager::addLemma	(	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 674 of file cnf_manager.cpp.

References SAT::CNF_Formula::addLiteral(), CVC3::CNF_Rules::CNFAddUnit(), d_rules, DebugAssert, SAT::CNF_Formula::getCurrentClause(), CVC3::CNF_Rules::learnedClauses(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setClauseTheorem(), and translateExpr().

Member Data Documentation

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(), 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.

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

Common proof rules.

Definition at line 50 of file cnf_manager.h.

Referenced by concreteThm(), replaceITErec(), and translateExprRec().

CVC3::CNF_Rules* SAT::CNF_Manager::d_rules [private]

Rules for manipulating CNF.

Definition at line 53 of file cnf_manager.h.

Referenced by addAssumption(), addLemma(), CNF_Manager(), convertLemma(), replaceITErec(), translateExpr(), translateExprRec(), and ~CNF_Manager().

std::vector<Varinfo> SAT::CNF_Manager::d_varInfo [private]

vector that maps a variable index to information for that variable

Definition at line 63 of file cnf_manager.h.

Referenced by CNF_Manager(), concreteLit(), concreteVar(), getFanin(), getFanout(), numFanins(), numFanouts(), numVars(), translateExpr(), and translateExprRec().

CVC3::ExprHashMap<Var> SAT::CNF_Manager::d_cnfVars [private]

Map from Exprs to Vars representing those Exprs.

Definition at line 66 of file cnf_manager.h.

Referenced by getCNFLit(), and translateExprRec().

CVC3::ExprHashMap<CVC3::Theorem> SAT::CNF_Manager::d_iteMap [private]

Cached translation of term-ite-containing expressions.

Definition at line 69 of file cnf_manager.h.

Referenced by concreteThm(), replaceITErec(), and translateExprRec().

int SAT::CNF_Manager::d_clauseIdNext [private]

Map of possibly useful lemmas.

Maps a clause id to the theorem justifying that clause

Note that clauses created by simple CNF translation are not given id's. This is because theorems for these clauses can be created lazily later. Next clause id

Definition at line 81 of file cnf_manager.h.

int SAT::CNF_Manager::d_bottomScope [private]

Whether expr has already been translated.

Bottom scope in which translation is valid

Definition at line 87 of file cnf_manager.h.

Referenced by setBottomScope(), and translateExprRec().

std::deque<CVC3::Theorem> SAT::CNF_Manager::d_translateQueueThms [private]

Queue of theorems to translate.

Definition at line 90 of file cnf_manager.h.

Referenced by replaceITErec(), translateExpr(), and translateExprRec().

std::deque<Var> SAT::CNF_Manager::d_translateQueueVars [private]

Queue of fanouts corresponding to thms to translate.