CVC3  2.4.1
Classes | Public Member Functions | Private Member Functions | Private Attributes | List of all members
SAT::CNF_Manager Class Reference

#include <cnf_manager.h>

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. More...
 
void setBottomScope (int scope)
 Set scope for translation. More...
 
unsigned numVars ()
 Return the number of variables being managed. More...
 
unsigned numFanins (Var c)
 Return number of fanins for CNF node c. More...
 
Lit getFanin (Var c, unsigned i)
 Returns the ith fanin of c. More...
 
unsigned numFanouts (Var c)
 Return number of fanins for c. More...
 
Lit getFanout (Var c, unsigned i)
 Returns the ith fanout of c. More...
 
const CVC3::ExprconcreteVar (Var v)
 Convert a CNF literal to an Expr literal. More...
 
CVC3::Expr concreteLit (Lit l, bool checkTranslated=true)
 Convert a CNF literal to an Expr literal. More...
 
Lit getCNFLit (const CVC3::Expr &e)
 Look up the CNF literal for an Expr. More...
 
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. More...
 
Lit addAssumption (const CVC3::Theorem &thm, CNF_Formula &cnf)
 Given thm of form A |- B, convert B to CNF and add it to cnf. More...
 
Lit addLemma (CVC3::Theorem thm, CNF_Formula &cnf)
 Convert thm to CNF and add it to the current formula. More...
 

Private Member Functions

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

Private Attributes

CVC3::ValidityCheckerd_vc
 For clause minimization. More...
 
bool d_minimizeClauses
 Whether to use brute-force clause minimization. More...
 
CVC3::CommonProofRulesd_commonRules
 Common proof rules. More...
 
CVC3::CNF_Rulesd_rules
 Rules for manipulating CNF. More...
 
std::vector< Varinfod_varInfo
 vector that maps a variable index to information for that variable More...
 
CVC3::ExprHashMap< Vard_cnfVars
 Map from Exprs to Vars representing those Exprs. More...
 
CVC3::ExprHashMap< CVC3::Theoremd_iteMap
 Cached translation of term-ite-containing expressions. More...
 
int d_clauseIdNext
 Map of possibly useful lemmas. More...
 
int d_bottomScope
 Whether expr has already been translated. More...
 
std::deque< CVC3::Theoremd_translateQueueThms
 Queue of theorems to translate. More...
 
std::deque< Vard_translateQueueVars
 Queue of fanouts corresponding to thms to translate. More...
 
std::deque< bool > d_translateQueueFlags
 Whether thm to translate is "translate only". More...
 
CVC3::Statisticsd_statistics
 Reference to statistics object. More...
 
const CVC3::CLFlagsd_flags
 Reference to command-line flags. More...
 
const CVC3::Exprd_nullExpr
 Reference to null Expr. More...
 
CNFCallbackd_cnfCallback
 Instance of CNF_CallBack: must be registered. More...
 

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
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
Theorem CNF_Manager::replaceITErec ( const CVC3::Expr e,
Var  v,
bool  translateOnly 
)
private
Lit CNF_Manager::translateExpr ( const CVC3::Theorem thmIn,
CNF_Formula cnf 
)
private
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, 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 
)
void CNF_Manager::convertLemma ( const CVC3::Theorem thm,
CNF_Formula cnf 
)
Lit CNF_Manager::addAssumption ( const CVC3::Theorem thm,
CNF_Formula cnf 
)
Lit CNF_Manager::addLemma ( CVC3::Theorem  thm,
CNF_Formula cnf 
)

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

Parameters
thmshould be of form A |- B where A is a set of literals.
cnfthe 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.

Definition at line 93 of file cnf_manager.h.

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

std::deque<bool> SAT::CNF_Manager::d_translateQueueFlags
private

Whether thm to translate is "translate only".

Definition at line 96 of file cnf_manager.h.

Referenced by replaceITErec(), and translateExpr().

CVC3::Statistics& SAT::CNF_Manager::d_statistics
private

Reference to statistics object.

Definition at line 99 of file cnf_manager.h.

const CVC3::CLFlags& SAT::CNF_Manager::d_flags
private

Reference to command-line flags.

Definition at line 102 of file cnf_manager.h.

Referenced by addAssumption(), and translateExprRec().

const CVC3::Expr& SAT::CNF_Manager::d_nullExpr
private

Reference to null Expr.

Definition at line 105 of file cnf_manager.h.

Referenced by concreteLit(), and concreteVar().

CNFCallback* SAT::CNF_Manager::d_cnfCallback
private

Instance of CNF_CallBack: must be registered.

Definition at line 120 of file cnf_manager.h.

Referenced by registerAtom(), and registerCNFCallback().


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