CVC3  2.4.1
theory_bitvector.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_bitvector.h
4  *
5  * Author: Vijay Ganesh
6  *
7  * Created: Wed May 05 18:34:55 PDT 2004
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__theory_bitvector_h_
22 #define _cvc3__include__theory_bitvector_h_
23 
24 #include "theory_core.h"
25 #include "statistics.h"
26 
27 namespace CVC3 {
28 
29  class VCL;
30  class BitvectorProofRules;
31 
32  typedef enum { //some new BV kinds
33  // New constants
34  BVCONST = 80,
35 
36  BITVECTOR = 8000,
37 
41 
48  SX,
53 
62 
72 
81 
82  INTTOBV, // Not implemented yet
83  BVTOINT, // Not implemented yet
84  // A wrapper for delaying the construction of type predicates
86  } BVKinds;
87 
88 /*****************************************************************************/
89 /*!
90  *\class TheoryBitvector
91  *\ingroup Theories
92  *\brief Theory of bitvectors of known length \
93  * (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
94  *
95  * Author: Vijay Ganesh
96  *
97  * Created:Wed May 5 15:35:07 PDT 2004
98  */
99 /*****************************************************************************/
100 class TheoryBitvector :public Theory {
102  //! MemoryManager index for BVConstExpr subclass
107 
108  //! counts delayed asserted equalities
110  //! counts asserted equalities
112  //! counts delayed asserted disequalities
114  //! counts asserted disequalities
116  //! counts type predicates
118  //! counts delayed type predicates
120  //! counts bitblasted equalities
122  //! counts bitblasted disequalities
124 
125  //! boolean on the fly rewrite flag
126  const bool* d_booleanRWFlag;
127  //! bool extract cache flag
129  //! flag which indicates that all arithmetic is 32 bit with no overflow
130  const bool* d_bv32Flag;
131 
132  //! Cache for storing the results of the bitBlastTerm function
134 
135  //! Cache for pushNegation(). it is ok that this is cache is
136  //ExprMap. it is cleared for each call of pushNegation. Does not add
137  //value across calls of pushNegation
139 
140  //! Backtracking queue for equalities
142  //! Backtracking queue for unsolved equalities
144  //! Index to current position in d_eqPending
146  //! Backtracking queue for all other assertions
148  //! Index to current position in d_bitblast
150  //! Backtracking database of subterms of shared terms
152  //! Backtracking database of subterms of shared terms
154 
155  //! Constant 1-bit bit-vector 0bin0
157  //! Constant 1-bit bit-vector 0bin0
159  //! Return cached constant 0bin0
160  const Expr& bvZero() const { return d_bvZero; }
161  //! Return cached constant 0bin1
162  const Expr& bvOne() const { return d_bvOne; }
163 
164  //! Max size of any bitvector we've seen
166 
167  //! Used in checkSat
170 
171  //! functions which implement the DP strategy for bitblasting
172  Theorem bitBlastEqn(const Expr& e);
173  //! bitblast disequation
174  Theorem bitBlastDisEqn(const Theorem& notE);
175  //! function which implements the DP strtagey to bitblast Inequations
176  Theorem bitBlastIneqn(const Expr& e);
177  //! functions which implement the DP strategy for bitblasting
178  Theorem bitBlastTerm(const Expr& t, int bitPosition);
179 
180 // //! strategy fucntions for BVPLUS NORMAL FORM
181 // Theorem padBVPlus(const Expr& e);
182 // //! strategy fucntions for BVPLUS NORMAL FORM
183 // Theorem flattenBVPlus(const Expr& e);
184 
185 // //! Implementation of the concatenation normal form
186 // Theorem normalizeConcat(const Expr& e, bool useFind);
187 // //! Implementation of the n-bit arithmetic normal form
188 // Theorem normalizeBVArith(const Expr& e, bool useFind);
189 // //! Helper method for composing normalizations
190 // Theorem normalizeConcat(const Theorem& t, bool useFind) {
191 // return transitivityRule(t, normalizeConcat(t.getRHS(), useFind));
192 // }
193 // //! Helper method for composing normalizations
194 // Theorem normalizeBVArith(const Theorem& t, bool useFind) {
195 // return transitivityRule(t, normalizeBVArith(t.getRHS(), useFind));
196 // }
197 
198 // Theorem signExtendBVLT(const Expr& e, int len, bool useFind);
199 
200  public:
201  Theorem pushNegationRec(const Expr& e);
202  private:
203  Theorem pushNegation(const Expr& e);
204 
205  //! Top down simplifier
206  virtual Theorem simplifyOp(const Expr& e);
207 
208  //! Internal rewrite method for constants
209  // Theorem rewriteConst(const Expr& e);
210 
211  //! Main rewrite method (implements the actual rewrites)
212  Theorem rewriteBV(const Expr& e, ExprMap<Theorem>& cache, int n = 1);
213 
214  //! Rewrite children 'n' levels down (n==1 means "only the top level")
215  Theorem rewriteBV(const Expr& e, int n = 1);
216 
217  // Shortcuts for theorems
218  Theorem rewriteBV(const Theorem& t, ExprMap<Theorem>& cache, int n = 1) {
219  return transitivityRule(t, rewriteBV(t.getRHS(), cache, n));
220  }
221  Theorem rewriteBV(const Theorem& t, int n = 1) {
222  return transitivityRule(t, rewriteBV(t.getRHS(), n));
223  }
224 
225  //! rewrite input boolean expression e to a simpler form
226  Theorem rewriteBoolean(const Expr& e);
227 
228 /*Beginning of Lorenzo PLatania's methods*/
229 
230  Expr multiply_coeff( Rational mult_inv, const Expr& e);
231 
232  // extract the min value from a Rational list
233  int min(std::vector<Rational> list);
234 
235  // evaluates the gcd of two integer coefficients
236  // int gcd(int c1, int c2);
237 
238  // converts a bv constant to an integer
239  // int bv2int(const Expr& e);
240 
241  // return the odd coefficient of a leaf for which we can solve the
242  // equation, or zero if no one has been found
243  Rational Odd_coeff( const Expr& e );
244 
245 
246 
247  // returns 1 if e is a linear term
248  int check_linear( const Expr &e );
249 
250  bool isTermIn(const Expr& e1, const Expr& e2);
251 
252  Theorem updateSubterms( const Expr& d );
253 
254  // returns how many times "term" appears in "e"
255  int countTermIn( const Expr& term, const Expr& e);
256 
257  Theorem simplifyPendingEq(const Theorem& thm, int maxEffort);
258  Theorem generalBitBlast( const Theorem& thm );
259 /*End of Lorenzo PLatania's methods*/
260 
262 
263 public:
266 
269 
270  // Trusted method that creates the proof rules class (used in constructor).
271  // Implemented in bitvector_theorem_producer.cpp
273 
274  // Theory interface
275  void addSharedTerm(const Expr& e);
276  void assertFact(const Theorem& e);
277  void assertTypePred(const Expr& e, const Theorem& pred);
278  void checkSat(bool fullEffort);
279  Theorem rewrite(const Expr& e);
280  Theorem rewriteAtomic(const Expr& e);
281  void setup(const Expr& e);
282  void update(const Theorem& e, const Expr& d);
283  Theorem solve(const Theorem& e);
284  void checkType(const Expr& e);
286  bool enumerate, bool computeSize);
287  void computeType(const Expr& e);
288  void computeModelTerm(const Expr& e, std::vector<Expr>& v);
289  void computeModel(const Expr& e, std::vector<Expr>& vars);
290  Expr computeTypePred(const Type& t, const Expr& e);
291  Expr computeTCC(const Expr& e);
292  ExprStream& print(ExprStream& os, const Expr& e);
293  Expr parseExprOp(const Expr& e);
294 
295  //helper functions
296 
297  //! Return the number of bits in the bitvector expression
298  int BVSize(const Expr& e);
299 
300  Expr rat(const Rational& r) { return getEM()->newRatExpr(r); }
301  //!pads e to be of length len
302  Expr pad(int len, const Expr& e);
303 
304  bool comparebv(const Expr& e1, const Expr& e2);
305 
306  //helper functions: functions to construct exprs
308  { return newBitvectorTypeExpr(i); }
309  Expr newBitvectorTypePred(const Type& t, const Expr& e);
310  Expr newBitvectorTypeExpr(int i);
311 
312  Expr newBVAndExpr(const Expr& t1, const Expr& t2);
313  Expr newBVAndExpr(const std::vector<Expr>& kids);
314 
315  Expr newBVOrExpr(const Expr& t1, const Expr& t2);
316  Expr newBVOrExpr(const std::vector<Expr>& kids);
317 
318  Expr newBVXorExpr(const Expr& t1, const Expr& t2);
319  Expr newBVXorExpr(const std::vector<Expr>& kids);
320 
321  Expr newBVXnorExpr(const Expr& t1, const Expr& t2);
322  Expr newBVXnorExpr(const std::vector<Expr>& kids);
323 
324  Expr newBVNandExpr(const Expr& t1, const Expr& t2);
325  Expr newBVNorExpr(const Expr& t1, const Expr& t2);
326  Expr newBVCompExpr(const Expr& t1, const Expr& t2);
327 
328  Expr newBVLTExpr(const Expr& t1, const Expr& t2);
329  Expr newBVLEExpr(const Expr& t1, const Expr& t2);
330  Expr newSXExpr(const Expr& t1, int len);
331  Expr newBVIndexExpr(int kind, const Expr& t1, int len);
332  Expr newBVSLTExpr(const Expr& t1, const Expr& t2);
333  Expr newBVSLEExpr(const Expr& t1, const Expr& t2);
334 
335  Expr newBVNegExpr(const Expr& t1);
336  Expr newBVUminusExpr(const Expr& t1);
337  Expr newBoolExtractExpr(const Expr& t1, int r);
338  Expr newFixedLeftShiftExpr(const Expr& t1, int r);
339  Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r);
340  Expr newFixedRightShiftExpr(const Expr& t1, int r);
341  Expr newConcatExpr(const Expr& t1, const Expr& t2);
342  Expr newConcatExpr(const Expr& t1, const Expr& t2, const Expr& t3);
343  Expr newConcatExpr(const std::vector<Expr>& kids);
344  Expr newBVConstExpr(const std::string& s, int base = 2);
345  Expr newBVConstExpr(const std::vector<bool>& bits);
346  // Lorenzo's wrapper
347  // as computeBVConst can not give the BV expr of a negative rational,
348  // I use this wrapper to do that
349  Expr signed_newBVConstExpr( Rational c, int bv_size);
350  // end of Lorenzo's wrapper
351 
352  // Construct BVCONST of length 'len', or the min. needed length when len=0.
353  Expr newBVConstExpr(const Rational& r, int len = 0);
354  Expr newBVZeroString(int r);
355  Expr newBVOneString(int r);
356  //! hi and low are bit indices
357  Expr newBVExtractExpr(const Expr& e,
358  int hi, int low);
359  Expr newBVSubExpr(const Expr& t1, const Expr& t2);
360  //! 'numbits' is the number of bits in the result
361  Expr newBVPlusExpr(int numbits, const Expr& k1, const Expr& k2);
362  //! 'numbits' is the number of bits in the result
363  Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k);
364  //! pads children and then builds plus expr
365  Expr newBVPlusPadExpr(int bvLength, const std::vector<Expr>& k);
366  Expr newBVMultExpr(int bvLength,
367  const Expr& t1, const Expr& t2);
368  Expr newBVMultExpr(int bvLength, const std::vector<Expr>& kids);
369  Expr newBVMultPadExpr(int bvLength,
370  const Expr& t1, const Expr& t2);
371  Expr newBVMultPadExpr(int bvLength, const std::vector<Expr>& kids);
372  Expr newBVUDivExpr(const Expr& t1, const Expr& t2);
373  Expr newBVURemExpr(const Expr& t1, const Expr& t2);
374  Expr newBVSDivExpr(const Expr& t1, const Expr& t2);
375  Expr newBVSRemExpr(const Expr& t1, const Expr& t2);
376  Expr newBVSModExpr(const Expr& t1, const Expr& t2);
377 
378  // Accessors for expression parameters
379  int getBitvectorTypeParam(const Expr& e);
381  { return getBitvectorTypeParam(t.getExpr()); }
382  Type getTypePredType(const Expr& tp);
383  const Expr& getTypePredExpr(const Expr& tp);
384  int getSXIndex(const Expr& e);
385  int getBVIndex(const Expr& e);
386  int getBoolExtractIndex(const Expr& e);
387  int getFixedLeftShiftParam(const Expr& e);
388  int getFixedRightShiftParam(const Expr& e);
389  int getExtractHi(const Expr& e);
390  int getExtractLow(const Expr& e);
391  int getBVPlusParam(const Expr& e);
392  int getBVMultParam(const Expr& e);
393 
394  unsigned getBVConstSize(const Expr& e);
395  bool getBVConstValue(const Expr& e, int i);
396  //!computes the integer value of a bitvector constant
397  Rational computeBVConst(const Expr& e);
398  //!computes the integer value of ~c+1 or BVUMINUS(c)
399  Rational computeNegBVConst(const Expr& e);
400 
401  int getMaxSize() { return d_maxLength; }
402 
403 /*Beginning of Lorenzo PLatania's public methods*/
404 
405  bool isLinearTerm( const Expr& e );
406  void extract_vars( const Expr& e, std::vector<Expr>& vars );
407  // checks whether e can be solved in term
408  bool canSolveFor( const Expr& term, const Expr& e );
409 
410  // evaluates the multipicative inverse
412 
413 
414  /*End of Lorenzo PLatania's public methods*/
415 
416  std::vector<Theorem> additionalRewriteConstraints;
417 
418 }; //end of class TheoryBitvector
419 
420 
421 }//end of namespace CVC3
422 #endif