CVC3  2.4.1
cnf_manager.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file cnf_manager.h
4  *\brief Manager for conversion to and traversal of CNF formulas
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Thu Dec 15 13:53:16 2005
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__cnf_manager_h_
22 #define _cvc3__include__cnf_manager_h_
23 
24 #include "cnf.h"
25 #include "expr.h"
26 #include "expr_map.h"
27 #include "cdmap.h"
28 #include "statistics.h"
29 
30 namespace CVC3 {
31 
32 class CommonProofRules;
33 class CNF_Rules;
34 class ValidityChecker;
35 class Statistics;
36 
37 }
38 
39 namespace SAT {
40 
41 class CNF_Manager {
42 
43  //! For clause minimization
45 
46  //! Whether to use brute-force clause minimization
48 
49  //! Common proof rules
51 
52  //! Rules for manipulating CNF
54 
55  //! Information kept for each CNF variable
56  struct Varinfo {
58  std::vector<Lit> fanins;
59  std::vector<Var> fanouts;
60  };
61 
62  //! vector that maps a variable index to information for that variable
63  std::vector<Varinfo> d_varInfo;
64 
65  //! Map from Exprs to Vars representing those Exprs
67 
68  //! Cached translation of term-ite-containing expressions
70 
71  //! Map of possibly useful lemmas
72  // CVC3::ExprMap<int> d_usefulLemmas;
73 
74  //! Maps a clause id to the theorem justifying that clause
75  /*! Note that clauses created by simple CNF translation are not given id's.
76  * This is because theorems for these clauses can be created lazily later. */
77  // CVC3::CDMap<int, CVC3::Theorem> d_theorems;
78  // CVC3::CDMap<int, CVC3::Theorem> d_theorems;
79 
80  //! Next clause id
82 
83  //! Whether expr has already been translated
84  // CVC3::CDMap<CVC3::Expr, bool> d_translated;
85 
86  //! Bottom scope in which translation is valid
88 
89  //! Queue of theorems to translate
90  std::deque<CVC3::Theorem> d_translateQueueThms;
91 
92  //! Queue of fanouts corresponding to thms to translate
93  std::deque<Var> d_translateQueueVars;
94 
95  //! Whether thm to translate is "translate only"
96  std::deque<bool> d_translateQueueFlags;
97 
98  //! Reference to statistics object
100 
101  //! Reference to command-line flags
103 
104  //! Reference to null Expr
106 
107 public:
108  //! Abstract class for callbacks
109  class CNFCallback {
110  public:
112  virtual ~CNFCallback() {}
113  //! Register an atom
114  virtual void registerAtom(const CVC3::Expr& e,
115  const CVC3::Theorem& thm) = 0;
116  };
117 
118 private:
119  //! Instance of CNF_CallBack: must be registered
121 
123 
124  //! Register a new atomic formula
125  void registerAtom(const CVC3::Expr& e, const CVC3::Theorem& thm);
126 
127  //! Return the expr corresponding to the literal unless the expr is TRUE of FALSE
128  CVC3::Expr concreteExpr(const CVC3::Expr& e, const Lit& literal);
129 
130  //! Return the theorem if e is not as concreteExpr(e).
132 
133  //! Recursively translate e into cnf
134  /*! A non-context dependent cache, d_cnfVars is used to remember translations
135  * of expressions. A context-dependent attribute, isTranslated, is used to
136  * remember whether an expression has been translated in the current context */
138  const CVC3::Theorem& thmIn);
139 
140  //! Recursively traverse an expression with an embedded term ITE
141  /*! Term ITE's are handled by introducing a skolem variable for the ITE term
142  * and then adding new constraints describing the ITE in terms of the new variable.
143  */
144  CVC3::Theorem replaceITErec(const CVC3::Expr& e, Var v, bool translateOnly);
145 
146  //! Recursively translate e into cnf
147  /*! Call translateExprRec. If additional expressions are queued up,
148  * translate them too, until none are left. */
149  Lit translateExpr(const CVC3::Theorem& thmIn, CNF_Formula& cnf);
150 
151 // bool isTranslated(const CVC3::Expr& e)
152 // { CVC3::CDMap<CVC3::Expr, bool>::iterator i = d_translated.find(e);
153 // return i != d_translated.end() && (*i).second; }
154 // void setTranslated(const CVC3::Expr& e)
155 // { DebugAssert(!isTranslated(e),"already set");
156 // d_translated.insert(e, true, d_bottomScope); }
157 // void clearTranslated(const CVC3::Expr& e)
158 // { d_translated.insert(e, false, d_bottomScope); }
159 
160 public:
162  const CVC3::CLFlags& flags);
163  ~CNF_Manager();
164 
165  //! Register CNF callback
166  void registerCNFCallback(CNFCallback* cnfCallback)
167  { d_cnfCallback = cnfCallback; }
168 
169  //! Set scope for translation
170  void setBottomScope(int scope) { d_bottomScope = scope; }
171 
172  //! Return the number of variables being managed
173  unsigned numVars() { return d_varInfo.size(); }
174 
175  //! Return number of fanins for CNF node c
176  /*! A CNF node x is a fanin of CNF node y if the expr for x is a child of the
177  * expr for y or if y is an ITE leaf and x is a new CNF node obtained by
178  * translating the ITE leaf y.
179  * \sa isITELeaf()
180  */
181  unsigned numFanins(Var c) {
182  if (!c.isVar()) return 0;
183  if (unsigned(c) >= d_varInfo.size()) return 0;
184  return d_varInfo[c].fanins.size();
185  }
186 
187  //! Returns the ith fanin of c.
188  Lit getFanin(Var c, unsigned i) {
189  DebugAssert(i < numFanins(c), "attempt to access unknown fanin");
190  return d_varInfo[c].fanins[i];
191  }
192 
193  //! Return number of fanins for c
194  /*! x is a fanout of y if y is a fanin of x
195  * \sa numFanins
196  */
197  unsigned numFanouts(Var c) {
198  if (!c.isVar()) return 0;
199  if (unsigned(c) >= d_varInfo.size()) return 0;
200  return d_varInfo[c].fanouts.size();
201  }
202 
203  //! Returns the ith fanout of c.
204  Lit getFanout(Var c, unsigned i) {
205  DebugAssert(i < numFanouts(c), "attempt to access unknown fanin");
206  return Lit(d_varInfo[c].fanouts[i]);
207  }
208 
209  //! Convert a CNF literal to an Expr literal
210  /*! Returns a NULL Expr if there is no corresponding Expr for l
211  */
213  if (v.isNull()) return d_nullExpr;
214  if (unsigned(v) >= d_varInfo.size() ||
215  (!d_varInfo[v].expr.isTranslated()))
216  return d_nullExpr;
217  return d_varInfo[v].expr;
218  }
219 
220  //! Convert a CNF literal to an Expr literal
221  /*! Returns a NULL Expr if there is no corresponding Expr for l
222  */
223  CVC3::Expr concreteLit(Lit l, bool checkTranslated = true) {
224  if (l.isNull()) return d_nullExpr;
225  bool inverted = !l.isPositive();
226  int index = l.getVar();
227  if ((unsigned)index >= d_varInfo.size() ||
228  (checkTranslated && !d_varInfo[index].expr.isTranslated()))
229  return d_nullExpr;
230  return inverted ? !d_varInfo[index].expr : d_varInfo[index].expr;
231  }
232 
233  //! Look up the CNF literal for an Expr
234  /*! Returns a NULL Lit if there is no corresponding CNF literal for e
235  */
237  if (e.isFalse()) return Lit::getFalse();
238  if (e.isTrue()) return Lit::getTrue();
239  if (e.isNot()) return !getCNFLit(e[0]);
241  if (!e.isTranslated() || i == d_cnfVars.end()) return Lit();
242  return Lit((*i).second);
243  }
244 
245  void cons(unsigned lb, unsigned ub, const CVC3::Expr& e2, std::vector<unsigned>& newLits);
246 
247  //! Convert thm A |- B (A is a set of literals) into one or more clauses
248  /*! cnf should be empty -- it will be filled with the result */
249  void convertLemma(const CVC3::Theorem& thm, CNF_Formula& cnf);
250 
251  //! Given thm of form A |- B, convert B to CNF and add it to cnf
252  /*! Returns Lit corresponding to the root of the expression that was
253  * translated. */
254  Lit addAssumption(const CVC3::Theorem& thm, CNF_Formula& cnf);
255 
256  //! Convert thm to CNF and add it to the current formula
257  /*! \param thm should be of form A |- B where A is a set of literals.
258  * \param cnf the new clauses are added to cnf.
259  * Returns Lit corresponding to the root of the expression that was
260  * translated. */
262 
263 };
264 
265 }
266 
267 #endif
Basic classes for reasoning about formulas in CNF.
static Lit getTrue()
Definition: cnf.h:60
std::deque< bool > d_translateQueueFlags
Whether thm to translate is "translate only".
Definition: cnf_manager.h:96
void registerCNFCallback(CNFCallback *cnfCallback)
Register CNF callback.
Definition: cnf_manager.h:166
Data structure of expressions in CVC3.
Definition: expr.h:133
bool isTrue() const
Definition: expr.h:356
unsigned numVars()
Return the number of variables being managed.
Definition: cnf_manager.h:173
std::vector< Varinfo > d_varInfo
vector that maps a variable index to information for that variable
Definition: cnf_manager.h:63
API to the CNF proof rules.
Definition: cnf_rules.h:34
Lit getFanout(Var c, unsigned i)
Returns the ith fanout of c.
Definition: cnf_manager.h:204
Lit translateExpr(const CVC3::Theorem &thmIn, CNF_Formula &cnf)
Recursively translate e into cnf.
bool isFalse() const
Definition: expr.h:355
bool isTranslated() const
Definition: expr.h:1370
bool isNull() const
Definition: cnf.h:63
std::deque< CVC3::Theorem > d_translateQueueThms
Queue of theorems to translate.
Definition: cnf_manager.h:90
virtual void registerAtom(const CVC3::Expr &e, const CVC3::Theorem &thm)=0
Register an atom.
Lit translateExprRec(const CVC3::Expr &e, CNF_Formula &cnf, const CVC3::Theorem &thmIn)
Recursively translate e into cnf.
#define DebugAssert(cond, str)
Definition: debug.h:408
void registerAtom(const CVC3::Expr &e, const CVC3::Theorem &thm)
Register a new atomic formula.
Definition: cnf_manager.cpp:67
int d_clauseIdNext
Map of possibly useful lemmas.
Definition: cnf_manager.h:81
Lit getCNFLit(const CVC3::Expr &e)
Look up the CNF literal for an Expr.
Definition: cnf_manager.h:236
CVC3::ExprHashMap< CVC3::Theorem > d_iteMap
Cached translation of term-ite-containing expressions.
Definition: cnf_manager.h:69
Description: Counters and flags for collecting run-time statistics.
static Lit getFalse()
Definition: cnf.h:61
CVC3::Theorem replaceITErec(const CVC3::Expr &e, Var v, bool translateOnly)
Recursively traverse an expression with an embedded term ITE.
Definition: cnf_manager.cpp:74
void cons(unsigned lb, unsigned ub, const CVC3::Expr &e2, std::vector< unsigned > &newLits)
bool isNot() const
Definition: expr.h:420
Lit getFanin(Var c, unsigned i)
Returns the ith fanin of c.
Definition: cnf_manager.h:188
Information kept for each CNF variable.
Definition: cnf_manager.h:56
CNFCallback * d_cnfCallback
Instance of CNF_CallBack: must be registered.
Definition: cnf_manager.h:120
CVC3::Theorem concreteThm(const CVC3::Expr &e)
Return the theorem if e is not as concreteExpr(e).
unsigned numFanins(Var c)
Return number of fanins for CNF node c.
Definition: cnf_manager.h:181
CVC3::ExprHashMap< Var > d_cnfVars
Map from Exprs to Vars representing those Exprs.
Definition: cnf_manager.h:66
bool isVar() const
Definition: cnf.h:45
std::deque< Var > d_translateQueueVars
Queue of fanouts corresponding to thms to translate.
Definition: cnf_manager.h:93
CVC3::Statistics & d_statistics
Reference to statistics object.
Definition: cnf_manager.h:99
Definition: cnf.h:51
CVC3::CNF_Rules * createProofRules(CVC3::TheoremManager *tm, const CVC3::CLFlags &)
Generic API for a validity checker.
Definition: vc.h:92
CVC3::ValidityChecker * d_vc
For clause minimization.
Definition: cnf_manager.h:44
Abstract class for callbacks.
Definition: cnf_manager.h:109
CVC3::CommonProofRules * d_commonRules
Common proof rules.
Definition: cnf_manager.h:50
CVC3::Expr concreteLit(Lit l, bool checkTranslated=true)
Convert a CNF literal to an Expr literal.
Definition: cnf_manager.h:223
unsigned numFanouts(Var c)
Return number of fanins for c.
Definition: cnf_manager.h:197
bool d_minimizeClauses
Whether to use brute-force clause minimization.
Definition: cnf_manager.h:47
Var getVar() const
Definition: cnf.h:70
const CVC3::CLFlags & d_flags
Reference to command-line flags.
Definition: cnf_manager.h:102
Definition of the API to expression package. See class Expr for details.
bool isNull() const
Definition: cnf.h:42
CNF_Manager(CVC3::TheoremManager *tm, CVC3::Statistics &statistics, const CVC3::CLFlags &flags)
Definition: cnf_manager.cpp:35
std::vector< Lit > fanins
Definition: cnf_manager.h:58
CVC3::Expr concreteExpr(const CVC3::Expr &e, const Lit &literal)
Return the expr corresponding to the literal unless the expr is TRUE of FALSE.
void setBottomScope(int scope)
Set scope for translation.
Definition: cnf_manager.h:170
int d_bottomScope
Whether expr has already been translated.
Definition: cnf_manager.h:87
void convertLemma(const CVC3::Theorem &thm, CNF_Formula &cnf)
Convert thm A |- B (A is a set of literals) into one or more clauses.
bool isPositive() const
Definition: cnf.h:64
const CVC3::Expr & d_nullExpr
Reference to null Expr.
Definition: cnf_manager.h:105
CVC3::CNF_Rules * d_rules
Rules for manipulating CNF.
Definition: cnf_manager.h:53
const CVC3::Expr & concreteVar(Var v)
Convert a CNF literal to an Expr literal.
Definition: cnf_manager.h:212
Lit addAssumption(const CVC3::Theorem &thm, CNF_Formula &cnf)
Given thm of form A |- B, convert B to CNF and add it to cnf.
Definition: cnf.h:34
std::vector< Var > fanouts
Definition: cnf_manager.h:59
Lit addLemma(CVC3::Theorem thm, CNF_Formula &cnf)
Convert thm to CNF and add it to the current formula.