CVC3
Classes | Public Member Functions | Private Member Functions | Private Attributes

SAT::CNF_Manager Class Reference

#include <cnf_manager.h>

Collaboration diagram for SAT::CNF_Manager:
Collaboration graph
[legend]

List of all members.

Classes

Public Member Functions

Private Member Functions

Private Attributes


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

For clause minimization.

Definition at line 44 of file cnf_manager.h.

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

Whether to use brute-force clause minimization.

Definition at line 47 of file cnf_manager.h.

Common proof rules.

Definition at line 50 of file cnf_manager.h.

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

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

Map from Exprs to Vars representing those Exprs.

Definition at line 66 of file cnf_manager.h.

Referenced by getCNFLit(), and translateExprRec().

Cached translation of term-ite-containing expressions.

Definition at line 69 of file cnf_manager.h.

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

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.

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

Queue of theorems to translate.

Definition at line 90 of file cnf_manager.h.

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

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

Reference to statistics object.

Definition at line 99 of file cnf_manager.h.

Reference to command-line flags.

Definition at line 102 of file cnf_manager.h.

Referenced by addAssumption(), and translateExprRec().

Reference to null Expr.

Definition at line 105 of file cnf_manager.h.

Referenced by concreteLit(), and concreteVar().

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: