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