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
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
CDList< Expr > d_sharedSubtermsList
Backtracking database of subterms of shared terms.
int check_linear(const Expr &e)
int getFixedRightShiftParam(const Expr &e)
Expr newBVSLTExpr(const Expr &t1, const Expr &t2)
Data structure of expressions in CVC3.
Definition: expr.h:133
BitvectorProofRules * d_rules
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Theorem rewriteBV(const Theorem &t, ExprMap< Theorem > &cache, int n=1)
StatCounter d_bvBitBlastEq
counts bitblasted equalities
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Expr newBVXnorExpr(const Expr &t1, const Expr &t2)
ExprStream & printSmtLibShared(ExprStream &os, const Expr &e)
Expr multiply_coeff(Rational mult_inv, const Expr &e)
Expr newBVExtractExpr(const Expr &e, int hi, int low)
hi and low are bit indices
TheoryBitvector(TheoryCore *core)
int d_maxLength
Max size of any bitvector we've seen.
Expr newBVUDivExpr(const Expr &t1, const Expr &t2)
StatCounter d_bvAssertDiseq
counts asserted disequalities
CDMap< Expr, Theorem > d_bitvecCache
Cache for storing the results of the bitBlastTerm function.
CDO< unsigned int > d_bb_index
Index to current position in d_bitblast.
const Expr & getTypePredExpr(const Expr &tp)
Expr newBVIndexExpr(int kind, const Expr &t1, int len)
StatCounter d_bvDelayEq
counts delayed asserted equalities
int getExtractHi(const Expr &e)
Expr newBVSLEExpr(const Expr &t1, const Expr &t2)
Expr newBVNorExpr(const Expr &t1, const Expr &t2)
Theorem pushNegationRec(const Expr &e)
MS C++ specific settings.
Definition: type.h:42
Base class for theories.
Definition: theory.h:64
bool canSolveFor(const Expr &term, const Expr &e)
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
Expr newBVOneString(int r)
produces a string of 1's of length bvLength
Expr newConcatExpr(const Expr &t1, const Expr &t2)
Type getTypePredType(const Expr &tp)
bool isTermIn(const Expr &e1, const Expr &e2)
Expr newSXExpr(const Expr &t1, int len)
int getBVPlusParam(const Expr &e)
Expr newBitvectorTypePred(const Type &t, const Expr &e)
int countTermIn(const Expr &term, const Expr &e)
int getSXIndex(const Expr &e)
Theorem simplifyPendingEq(const Theorem &thm, int maxEffort)
CDO< unsigned int > d_eq_index
Index to current position in d_eqPending.
Description: Counters and flags for collecting run-time statistics.
Expr newFixedLeftShiftExpr(const Expr &t1, int r)
size_t d_bvConstExprIndex
MemoryManager index for BVConstExpr subclass.
StatCounter d_bvBitBlastDiseq
counts bitblasted disequalities
const Expr & bvOne() const
Return cached constant 0bin1.
Expr newBVSDivExpr(const Expr &t1, const Expr &t2)
Expr signed_newBVConstExpr(Rational c, int bv_size)
Theorem updateSubterms(const Expr &d)
Expr newBVOrExpr(const Expr &t1, const Expr &t2)
CDList< Theorem > d_eqPending
Backtracking queue for unsolved equalities.
Expr newBVNegExpr(const Expr &t1)
const bool * d_boolExtractCacheFlag
bool extract cache flag
const Expr & getExpr() const
Definition: type.h:52
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
void checkType(const Expr &e)
Check that e is a valid Type expr.
int getBitvectorTypeParam(const Expr &e)
Theorem generalBitBlast(const Theorem &thm)
Theorem pushNegation(const Expr &e)
virtual Theorem simplifyOp(const Expr &e)
Top down simplifier.
ExprMap< Theorem > d_pushNegCache
Cache for pushNegation(). it is ok that this is cache is.
Expr newBVConstExpr(const std::string &s, int base=2)
Theorem rewriteBV(const Theorem &t, int n=1)
Expr newBVURemExpr(const Expr &t1, const Expr &t2)
CDMap< Expr, Expr > d_sharedSubterms
Backtracking database of subterms of shared terms.
Expr newBVMultExpr(int bvLength, const Expr &t1, const Expr &t2)
Expr newFixedConstWidthLeftShiftExpr(const Expr &t1, int r)
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Expr d_bvOne
Constant 1-bit bit-vector 0bin0.
Expr newBVLEExpr(const Expr &t1, const Expr &t2)
StatCounter d_bvDelayDiseq
counts delayed asserted disequalities
Expr newBVLTExpr(const Expr &t1, const Expr &t2)
StatCounter d_bvTypePreds
counts type predicates
ExprMap< Expr > d_bvPlusCarryCacheRightBV
Theorem solve(const Theorem &e)
An optional solver.
BitvectorProofRules * createProofRules()
Rational multiplicative_inverse(Rational r, int n_bits)
Expr newBVNandExpr(const Expr &t1, const Expr &t2)
Expr newBVUminusExpr(const Expr &t1)
Expr newBVPlusPadExpr(int bvLength, const std::vector< Expr > &k)
pads children and then builds plus expr
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
int getBVIndex(const Expr &e)
Expr newBVSubExpr(const Expr &t1, const Expr &t2)
const Expr & getRHS() const
Definition: theorem.cpp:246
const bool * d_bv32Flag
flag which indicates that all arithmetic is 32 bit with no overflow
Theorem bitBlastIneqn(const Expr &e)
function which implements the DP strtagey to bitblast Inequations
int getBitvectorTypeParam(const Type &t)
Expr newBVMultPadExpr(int bvLength, const Expr &t1, const Expr &t2)
int min(std::vector< Rational > list)
Expr newRatExpr(const Rational &r)
Definition: expr_manager.h:471
int getBoolExtractIndex(const Expr &e)
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
Theorem rewriteBV(const Expr &e, ExprMap< Theorem > &cache, int n=1)
Internal rewrite method for constants.
CDO< unsigned > d_index1
Used in checkSat.
int getFixedLeftShiftParam(const Expr &e)
Expr rat(const Rational &r)
const bool * d_booleanRWFlag
boolean on the fly rewrite flag
ExprMap< Expr > d_bvPlusCarryCacheLeftBV
bool getBVConstValue(const Expr &e, int i)
CDList< Theorem > d_eq
Backtracking queue for equalities.
StatCounter d_bvAssertEq
counts asserted equalities
Rational Odd_coeff(const Expr &e)
Expr newBVPlusExpr(int numbits, const Expr &k1, const Expr &k2)
'numbits' is the number of bits in the result
Theorem rewriteBoolean(const Expr &e)
rewrite input boolean expression e to a simpler form
unsigned getBVConstSize(const Expr &e)
Theorem rewriteAtomic(const Expr &e)
Theory-specific rewrites for atomic formulas.
int getBVMultParam(const Expr &e)
bool isLinearTerm(const Expr &e)
CDO< unsigned > d_index2
Expr d_bvZero
Constant 1-bit bit-vector 0bin0.
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Expr newFixedRightShiftExpr(const Expr &t1, int r)
Expr newBoolExtractExpr(const Expr &t1, int r)
const Expr & bvZero() const
Return cached constant 0bin0.
Expr pad(int len, const Expr &e)
pads e to be of length len
int BVSize(const Expr &e)
Return the number of bits in the bitvector expression.
void assertTypePred(const Expr &e, const Theorem &pred)
Receives all the type predicates for the types of the given theory.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Theorem bitBlastDisEqn(const Theorem &notE)
bitblast disequation
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
CDList< Theorem > d_bitblast
Backtracking queue for all other assertions.
Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
StatCounter d_bvDelayTypePreds
counts delayed type predicates
Expr newBVSRemExpr(const Expr &t1, const Expr &t2)
void extract_vars(const Expr &e, std::vector< Expr > &vars)
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Rational computeNegBVConst(const Expr &e)
computes the integer value of ~c+1 or BVUMINUS(c)
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Expr newBVXorExpr(const Expr &t1, const Expr &t2)
Expr newBVZeroString(int r)
produces a string of 0's of length bvLength
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
Expr newBVCompExpr(const Expr &t1, const Expr &t2)
Rational computeBVConst(const Expr &e)
computes the integer value of a bitvector constant
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Expr newBVAndExpr(const Expr &t1, const Expr &t2)
Theorem bitBlastTerm(const Expr &t, int bitPosition)
functions which implement the DP strategy for bitblasting
Theorem bitBlastEqn(const Expr &e)
functions which implement the DP strategy for bitblasting
std::vector< Theorem > additionalRewriteConstraints
Expr newBVSModExpr(const Expr &t1, const Expr &t2)
void computeType(const Expr &e)
Compute and store the type of e.
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
int getExtractLow(const Expr &e)
bool comparebv(const Expr &e1, const Expr &e2)