SAT::CNF_Manager Class Reference

#include <cnf_manager.h>

Collaboration diagram for SAT::CNF_Manager:

[legend]List of all members.

Public Member Functions

• CNF_Manager (CVCL::TheoremManager *tm)
• ~CNF_Manager ()
• void setBottomScope (int scope)

  Set scope for translation.
  

• unsigned numVars ()

  Return the number of variables being managed.
  

• unsigned numFanins (Lit c)

  Return number of fanins for CNF node c.
  

• Lit getFanin (Lit c, unsigned i)

  Returns the ith fanin of c.
  

• unsigned numFanouts (Lit c)

  Return number of fanins for c.
  

• Lit getFanout (Lit c, unsigned i)

  Returns the ith fanout of c.
  

• CVCL::Expr concreteLit (Lit l)

  Convert a CNF literal to an Expr literal.
  

• Lit getCNFLit (const CVCL::Expr &e)

  Look up the CNF literal for an Expr.
  

• void convertLemma (const CVCL::Theorem &thm, Clause &c)

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

• Lit addAssumption (const CVCL::Theorem &thm, CNF_Formula &cnf)

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

• Lit addLemma (const CVCL::Theorem &thm, CNF_Formula &cnf)

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

Private Member Functions

• CVCL::CNF_Rules * createProofRules (CVCL::TheoremManager *tm)
• Lit translateExprRec (const CVCL::Expr &e, CNF_Formula &cnf)

  Recursively translate e into cnf.
  

• CVCL::Theorem replaceITErec (const CVCL::Expr &e, Var v, bool translateOnly)

  Recursively traverse an expression with an embedded term ITE.
  

• Lit translateExpr (const CVCL::Expr &e, CNF_Formula &cnf)

  Recursively translate e into cnf.
  

Private Attributes

• CVCL::CommonProofRules * d_commonRules

  Common proof rules.
  

• CVCL::CNF_Rules * d_rules

  Rules for manipulating CNF.
  

• std::vector< Varinfo > d_varInfo

  vector that maps a variable index to information for that variable
  

• CVCL::ExprMap< Var > d_cnfVars

  Map from Exprs to Vars representing those Exprs.
  

• CVCL::ExprMap< CVCL::Theorem > d_iteMap

  Cached translation of term-ite-containing expressions.
  

• CVCL::CDMap< int, CVCL::Theorem > d_theorems

  Maps a clause id to the theorem justifying that clause.
  

• int d_clauseIdNext

  Next clause id.
  

• int d_bottomScope

  Bottom scope in which translation is valid.
  

• std::deque< CVCL::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".
  

Classes

• struct Varinfo

  Information kept for each CNF variable. More...
  

---

Detailed Description

Definition at line 46 of file cnf_manager.h.

---

Constructor & Destructor Documentation

CNF_Manager::CNF_Manager (  CVCL::TheoremManager *  tm  )

Definition at line 41 of file cnf_manager.cpp. References createProofRules(), d_rules, and d_varInfo.

CNF_Manager::~CNF_Manager (   )

Definition at line 55 of file cnf_manager.cpp. References d_rules.

---

Member Function Documentation

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

Definition at line 46 of file cnf_theorem_producer.cpp. Referenced by CNF_Manager().

Lit CNF_Manager::translateExprRec (  const CVCL::Expr &  e, CNF_Formula &  cnf )  [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 118 of file cnf_manager.cpp. References SAT::CNF_Formula::addLiteral(), CVCL::AND, CVCL::Expr::begin(), d_bottomScope, d_cnfVars, d_translateQueueThms, d_translateQueueVars, d_varInfo, CVCL::Expr::end(), CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), getCNFLit(), SAT::Lit::getFalse(), CVCL::Expr::getKind(), CVCL::Theorem::getRHS(), SAT::Lit::getTrue(), SAT::Lit::getVar(), CVCL::IFF, CVCL::IMPLIES, CVCL::Expr::isAbsAtomicFormula(), CVCL::Expr::isFalse(), CVCL::Expr::isNot(), SAT::Lit::isNull(), CVCL::Expr::isTranslated(), CVCL::Expr::isTrue(), SAT::Lit::isVar(), CVCL::ITE, SAT::CNF_Formula::newClause(), CVCL::OR, replaceITErec(), CVCL::Expr::setTranslated(), and CVCL::XOR. Referenced by translateExpr().

Theorem CNF_Manager::replaceITErec (  const CVCL::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 61 of file cnf_manager.cpp. References CVCL::Expr::begin(), d_commonRules, d_iteMap, d_rules, d_translateQueueFlags, d_translateQueueThms, d_translateQueueVars, CVCL::Expr::end(), CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::CommonProofRules::iffMP(), CVCL::CNF_Rules::ifLiftRule(), CVCL::Expr::isAtomic(), CVCL::Type::isBool(), CVCL::ITE, CVCL::CommonProofRules::reflexivityRule(), CVCL::CommonProofRules::substitutivityRule(), CVCL::CommonProofRules::symmetryRule(), and CVCL::CommonProofRules::varIntroSkolem(). Referenced by translateExprRec().

Lit CNF_Manager::translateExpr (  const CVCL::Expr &  e, 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 322 of file cnf_manager.cpp. References SAT::CNF_Formula::addLiteral(), d_clauseIdNext, d_theorems, d_translateQueueFlags, d_translateQueueThms, d_translateQueueVars, d_varInfo, SAT::CNF_Formula::getCurrentClause(), CVCL::Theorem::getExpr(), SAT::Lit::getVar(), CVCL::CDMap< Key, Data, HashFcn >::insert(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setId(), and translateExprRec(). Referenced by addAssumption(), and addLemma().

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

Set scope for translation. Definition at line 128 of file cnf_manager.h. References d_bottomScope. Referenced by CVCL::SearchSat::check().

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

Return the number of variables being managed. Definition at line 131 of file cnf_manager.h. References d_varInfo. Referenced by CVCL::SearchSat::addLemma(), and CVCL::SearchSat::check().

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 139 of file cnf_manager.h. References d_varInfo, SAT::Lit::getVar(), and SAT::Lit::isVar(). Referenced by CVCL::SearchSat::findSplitterRec(), and getFanin().

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

Returns the ith fanin of c. Definition at line 147 of file cnf_manager.h. References d_varInfo, SAT::Lit::getVar(), and numFanins(). Referenced by CVCL::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 156 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 164 of file cnf_manager.h. References d_varInfo, SAT::Lit::getVar(), and numFanouts().

CVCL::Expr SAT::CNF_Manager::concreteLit (  Lit  l  )  [inline]

Convert a CNF literal to an Expr literal. Returns a NULL Expr if there is no corresponding Expr for l Definition at line 172 of file cnf_manager.h. References d_varInfo, SAT::Lit::getVar(), SAT::Lit::isNull(), and SAT::Lit::isPositive(). Referenced by CVCL::SearchSat::addLemma(), CVCL::SearchSat::assertLit(), CVCL::SearchSat::check(), CVCL::SearchSat::checkJustified(), CVCL::SearchSat::findSplitterRec(), and CVCL::SearchSat::setJustified().

Lit SAT::CNF_Manager::getCNFLit (  const CVCL::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 184 of file cnf_manager.h. References d_cnfVars, CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), SAT::Lit::getFalse(), SAT::Lit::getTrue(), CVCL::Expr::isFalse(), CVCL::Expr::isNot(), CVCL::Expr::isTranslated(), and CVCL::Expr::isTrue(). Referenced by convertLemma(), CVCL::SearchSat::getImplication(), and translateExprRec().

void CNF_Manager::convertLemma (  const CVCL::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 352 of file cnf_manager.cpp. References SAT::Clause::addLiteral(), CVCL::Expr::begin(), d_clauseIdNext, d_rules, d_theorems, CVCL::Expr::end(), getCNFLit(), CVCL::Theorem::getExpr(), CVCL::CDMap< Key, Data, HashFcn >::insert(), SAT::Lit::isNull(), CVCL::Expr::isOr(), CVCL::CNF_Rules::learnedClause(), SAT::Clause::setId(), SAT::Clause::setUnit(), and SAT::Clause::size().

Lit CNF_Manager::addAssumption (  const CVCL::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 377 of file cnf_manager.cpp. References SAT::CNF_Formula::addLiteral(), d_clauseIdNext, d_theorems, SAT::CNF_Formula::getCurrentClause(), CVCL::Theorem::getExpr(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setId(), and translateExpr(). Referenced by CVCL::SearchSat::check().

Lit CNF_Manager::addLemma (  const CVCL::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 The new clauses are added to cnf. Returns Lit corresponding to the root of the expression that was translated. Definition at line 392 of file cnf_manager.cpp. References SAT::CNF_Formula::addLiteral(), d_clauseIdNext, d_rules, d_theorems, SAT::CNF_Formula::getCurrentClause(), CVCL::Theorem::getExpr(), CVCL::CDMap< Key, Data, HashFcn >::insert(), CVCL::CNF_Rules::learnedClause(), SAT::CNF_Formula::newClause(), SAT::CNF_Formula::registerUnit(), SAT::Clause::setId(), and translateExpr(). Referenced by CVCL::SearchSat::addLemma().

---

Member Data Documentation

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

Common proof rules. Definition at line 49 of file cnf_manager.h. Referenced by replaceITErec().

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

Rules for manipulating CNF. Definition at line 52 of file cnf_manager.h. Referenced by addLemma(), CNF_Manager(), convertLemma(), replaceITErec(), 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 62 of file cnf_manager.h. Referenced by CNF_Manager(), concreteLit(), getFanin(), getFanout(), numFanins(), numFanouts(), numVars(), translateExpr(), and translateExprRec().

CVCL::ExprMap<Var> SAT::CNF_Manager::d_cnfVars [private]

Map from Exprs to Vars representing those Exprs. Definition at line 65 of file cnf_manager.h. Referenced by getCNFLit(), and translateExprRec().

CVCL::ExprMap<CVCL::Theorem> SAT::CNF_Manager::d_iteMap [private]

Cached translation of term-ite-containing expressions. Definition at line 68 of file cnf_manager.h. Referenced by replaceITErec().

CVCL::CDMap<int, CVCL::Theorem> SAT::CNF_Manager::d_theorems [private]

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. Definition at line 73 of file cnf_manager.h. Referenced by addAssumption(), addLemma(), convertLemma(), and translateExpr().

int SAT::CNF_Manager::d_clauseIdNext [private]

Next clause id. Definition at line 76 of file cnf_manager.h. Referenced by addAssumption(), addLemma(), convertLemma(), and translateExpr().

int SAT::CNF_Manager::d_bottomScope [private]

Bottom scope in which translation is valid. Definition at line 82 of file cnf_manager.h. Referenced by setBottomScope(), and translateExprRec().

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

Queue of theorems to translate. Definition at line 85 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 88 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 91 of file cnf_manager.h. Referenced by replaceITErec(), and translateExpr().

---

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

• cnf_manager.h
• cnf_manager.cpp
• cnf_theorem_producer.cpp

---