CVC3  2.4.1
theory_bitvector.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_bitvector.cpp
4  *
5  * Author: Vijay Ganesh.
6  *
7  * Created: Wed May 5 16:16:59 PST 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 
22 #include "theory_bitvector.h"
23 #include "bitvector_proof_rules.h"
24 #include "bitvector_exception.h"
25 #include "typecheck_exception.h"
26 #include "parser_exception.h"
27 #include "smtlib_exception.h"
28 #include "bitvector_expr_value.h"
29 #include "command_line_flags.h"
30 
31 
32 #define HASH_VALUE_ZERO 380
33 #define HASH_VALUE_ONE 450
34 
35 
36 using namespace std;
37 using namespace CVC3;
38 
39 
40 ///////////////////////////////////////////////////////////////////////////////
41 // TheoryBitvector Private Methods //
42 ///////////////////////////////////////////////////////////////////////////////
43 
44 
45 int TheoryBitvector::BVSize(const Expr& e)
46 {
47  Type tp(getBaseType(e));
49  "BVSize: e = "+e.toString());
50  return getBitvectorTypeParam(tp);
51 }
52 
53 
54 //! Converts e into a BITVECTOR of length 'len'
55 /*!
56  * \param len is the desired length of the resulting bitvector
57  * \param e is the original bitvector of arbitrary length
58  */
59 Expr TheoryBitvector::pad(int len, const Expr& e)
60 {
61  DebugAssert(len >=0,
62  "TheoryBitvector::newBVPlusExpr:"
63  "padding length must be a non-negative integer: "+
64  int2string(len));
66  "TheoryBitvector::newBVPlusExpr:"
67  "input must be a BITVECTOR: " + e.toString());
68 
69  int size = BVSize(e);
70  Expr res;
71  if(size == len)
72  res = e;
73  else if (len < size)
74  res = newBVExtractExpr(e,len-1,0);
75  else {
76  // size < len
77  Expr zero = newBVZeroString(len-size);
78  res = newConcatExpr(zero,e);
79  }
80  return res;
81 }
82 
83 
84 // Bit-blasting methods
85 
86 
87 //! accepts a bitvector equation t1 = t2.
88 /*! \return a rewrite theorem which is a conjunction of equivalences
89  * over the bits of t1,t2 respectively.
90  */
91 Theorem TheoryBitvector::bitBlastEqn(const Expr& e)
92 {
93  TRACE("bitvector", "bitBlastEqn(", e.toString(), ") {");
94  d_bvBitBlastEq++;
95 
96  DebugAssert(e.isEq(),
97  "TheoryBitvector::bitBlastEqn:"
98  "expecting an equation" + e.toString());
99  const Expr& leftBV = e[0];
100  const Expr& rightBV = e[1];
101  IF_DEBUG(const Type& leftType = getBaseType(leftBV);)
102  IF_DEBUG(const Type& rightType = getBaseType(rightBV);)
103  DebugAssert(BITVECTOR == leftType.getExpr().getOpKind() &&
104  BITVECTOR == rightType.getExpr().getOpKind(),
105  "TheoryBitvector::bitBlastEqn:"
106  "lhs & rhs must be bitvectors");
107  DebugAssert(BVSize(leftBV) == BVSize(rightBV),
108  "TheoryBitvector::bitBlastEqn:\n e = "
109  +e.toString());
110 
111  Theorem result = reflexivityRule(e);
112  Theorem bitBlastLeftThm;
113  Theorem bitBlastRightThm;
114  std::vector<Theorem> substThms;
115  std::vector<Theorem> leftBVrightBVThms;
116  int bvLength = BVSize(leftBV);
117  int bitPosition = 0;
118  Theorem thm0;
119 
120  for(; bitPosition < bvLength; ++bitPosition) {
121  //bitBlastLeftThm is the theorem 'leftBV[bitPosition] <==> phi'
122  bitBlastLeftThm = bitBlastTerm(leftBV, bitPosition);
123  //bitBlastRightThm is the theorem 'rightBV[bitPosition] <==> theta'
124  bitBlastRightThm = bitBlastTerm(rightBV, bitPosition);
125  //collect the two theorems created above in the vector
126  //leftBVrightBVthms.
127  leftBVrightBVThms.push_back(bitBlastLeftThm);
128  leftBVrightBVThms.push_back(bitBlastRightThm);
129  //construct (leftBV[bitPosition] <==> rightBV[bitPosition])
130  //<====> phi <==> theta
131  //and store in the vector substThms.
132  Theorem thm = substitutivityRule(IFF, leftBVrightBVThms);
133  thm = transitivityRule(thm, rewriteBoolean(thm.getRHS()));
134  leftBVrightBVThms.clear();
135  substThms.push_back(thm);
136  //if phi <==> theta is false, then stop bitblasting. immediately
137  //exit and return false.
138  if(thm.getRHS().isFalse())
139  return transitivityRule(result,
140  d_rules->bitvectorFalseRule(thm));
141  }
142  // AND_0^bvLength(leftBV[bitPosition] <==> rightBV[bitPosition]) <====>
143  // AND_0^bvLength(phi <==> theta)
144  Theorem thm = substitutivityRule(AND, substThms);
145  // AND_0^bvLength(leftBV[bitPosition] <==> rightBV[bitPosition]) <====>
146  // rewriteBoolean(AND_0^bvLength(phi <==> theta))
147  thm = transitivityRule(thm, rewriteBoolean(thm.getRHS()));
148  //call trusted rule for bitblasting equations.
149  result = d_rules->bitBlastEqnRule(e, thm.getLHS());
150  result = transitivityRule(result, thm);
151  TRACE("bitvector", "bitBlastEqn => ", result.toString(), " }");
152  return result;
153 }
154 
155 
156 //! accepts a bitvector equation t1 != t2.
157 /*! \return a rewrite theorem which is a conjunction of
158  * (dis)-equivalences over the bits of t1,t2 respectively.
159  *
160  * A separate rule for disequations for efficiency sake. Obvious
161  * implementation using rule for equations and rule for NOT, is not
162  * efficient.
163  */
164 Theorem TheoryBitvector::bitBlastDisEqn(const Theorem& notE)
165 {
166  TRACE("bitvector", "bitBlastDisEqn(", notE, ") {");
167  IF_DEBUG(debugger.counter("bit-blasted diseq")++);
168  //stat counter
169  d_bvBitBlastDiseq++;
170 
171  DebugAssert(notE.getExpr().isNot() && (notE.getExpr())[0].isEq(),
172  "TheoryBitvector::bitBlastDisEqn:"
173  "expecting an equation" + notE.getExpr().toString());
174  //e is the equation
175  const Expr& e = (notE.getExpr())[0];
176  const Expr& leftBV = e[0];
177  const Expr& rightBV = e[1];
178  IF_DEBUG(Type leftType = leftBV.getType());
179  IF_DEBUG(debugger.counter("bit-blasted diseq bits")+=
180  BVSize(leftBV));
181  IF_DEBUG(Type rightType = rightBV.getType());
182  DebugAssert(BITVECTOR == leftType.getExpr().getOpKind() &&
183  BITVECTOR == rightType.getExpr().getOpKind(),
184  "TheoryBitvector::bitBlastDisEqn:"
185  "lhs & rhs must be bitvectors");
186  DebugAssert(BVSize(leftBV) == BVSize(rightBV),
187  "TheoryBitvector::bitBlastDisEqn: e = "
188  +e.toString());
189  Theorem bitBlastLeftThm;
190  Theorem bitBlastRightThm;
191  std::vector<Theorem> substThms;
192  std::vector<Theorem> leftBVrightBVThms;
193  int bvLength = BVSize(leftBV);
194  int bitPosition = 0;
195  for(; bitPosition < bvLength; bitPosition = bitPosition+1) {
196  //bitBlastLeftThm is the theorem '~leftBV[bitPosition] <==> ~phi'
197  bitBlastLeftThm =
198  getCommonRules()->iffContrapositive(bitBlastTerm(leftBV, bitPosition));
199  //bitBlastRightThm is the theorem 'rightBV[bitPosition] <==> theta'
200  bitBlastRightThm = bitBlastTerm(rightBV, bitPosition);
201  //collect the two theorems created above in the vector leftBVrightBVthms.
202  leftBVrightBVThms.push_back(bitBlastLeftThm);
203  leftBVrightBVThms.push_back(bitBlastRightThm);
204  //construct (~leftBV[bitPosition] <==> rightBV[bitPosition])
205  //<====> ~phi <==> theta
206  //and store in the vector substThms.
207  //recall that (p <=/=> q) is same as (~p <==> q)
208  Theorem thm = substitutivityRule(IFF, leftBVrightBVThms);
209  thm = transitivityRule(thm, rewriteBoolean(thm.getRHS()));
210  leftBVrightBVThms.clear();
211  substThms.push_back(thm);
212 
213  //if phi <==> theta is the True theorem, then stop bitblasting. immediately
214  //exit and return t1!=t2 <=> true.
215  if(thm.getRHS().isTrue())
216  return d_rules->bitvectorTrueRule(thm);
217  }
218 
219  // OR_0^bvLength(~leftBV[bitPosition] <==> rightBV[bitPosition]) <====>
220  // OR_0^bvLength(~phi <==> theta)
221  Theorem thm1 = substitutivityRule(OR, substThms);
222  // Call trusted rule for bitblasting disequations.
223  Theorem result = d_rules->bitBlastDisEqnRule(notE, thm1.getLHS());
224  Theorem thm2 = transitivityRule(thm1, rewriteBoolean(thm1.getRHS()));
225  result = iffMP(result, thm2);
226  TRACE("bitvector", "bitBlastDisEqn => ", result.toString(), " }");
227  return result;
228 }
229 
230 
231 /*! \param e has the form e1 pred e2, where pred is < or <=.
232  *
233  * if e1,e2 are constants, determine bv2int(e1) pred bv2int(e2).
234  *
235  * most significant bit of ei is denoted by msb(ei)
236  *
237  * \return \f$(msb(e1)\ pred\ msb(e2)) \vee
238  * (msb(e1)=msb(e2) \wedge e1[n-2:0]\ pred\ e2[n-2:0])\f$
239  */
240 Theorem TheoryBitvector::bitBlastIneqn(const Expr& e)
241 {
242  TRACE("bitvector", "bitBlastIneqn(", e.toString(), ") {");
243 
244  DebugAssert(BVLT == e.getOpKind() ||
245  BVLE == e.getOpKind(),
246  "TheoryBitvector::bitBlastIneqn: "
247  "input e must be BVLT/BVLE: e = " + e.toString());
248  DebugAssert(e.arity() == 2,
249  "TheoryBitvector::bitBlastIneqn: "
250  "arity of e must be 2: e = " + e.toString());
251  Expr lhs = e[0];
252  Expr rhs = e[1];
253  int e0len = BVSize(lhs);
254  DebugAssert(e0len == BVSize(rhs), "Expected sizes to match");
255 
256  int kind = e.getOpKind();
257  Theorem res;
258  if(lhs == rhs) {
259  res = d_rules->lhsEqRhsIneqn(e, kind);
260  }
261  else if (lhs.getKind() == BVCONST && rhs.getKind() == BVCONST) {
262  res = d_rules->bvConstIneqn(e, kind);
263  } else {
264  Theorem lhs_i = bitBlastTerm(lhs, e0len-1);
265  Theorem rhs_i = bitBlastTerm(rhs, e0len-1);
266  res = d_rules->generalIneqn(e, lhs_i, rhs_i, kind);
267 
268  //check if output is TRUE or FALSE theorem, and then simply return
269  Theorem output = rewriteBoolean(res.getRHS());
270  if (output.getRHS().isBoolConst()) {
271  res = transitivityRule(res, output);
272  }
273  else if (e0len > 1) {
274  // Copy by value, since 'res' will be changing
275  Expr resRHS = res.getRHS();
276  // resRHS is of the form (\alpha or (\beta and \gamma))
277  // where \gamma is an inequality
278  DebugAssert(resRHS.getKind() == OR && resRHS.arity() == 2 &&
279  resRHS[1].getKind() == AND && resRHS[1].arity() == 2,
280  "Unexpected structure");
281 
282  vector<unsigned> changed;
283  vector<Theorem> thms;
284 
285  // \gamma <=> \gamma'
286  Theorem thm = bitBlastIneqn(resRHS[1][1]);
287 
288  // (\beta and \gamma) <=> (\beta and \gamma')
289  changed.push_back(1);
290  thms.push_back(thm);
291  thm = substitutivityRule(resRHS[1], changed, thms);
292 
293  // (\alpha or (\beta and \gamma)) <=> (\alpha or (\beta and \gamma'))
294  // 'changed' is the same, only update thms[0]
295  thms[0] = thm;
296  thm = substitutivityRule(resRHS, changed, thms);
297  res = transitivityRule(res, thm);
298  /*
299 
300  //resRHS can be of the form (\beta and \gamma) or
301  //resRHS can be of the form (\alpha or \gamma) or
302  //resRHS can be of the form (\gamma)
303  // Our mission is to bitblast \gamma and insert it back to the formula
304  switch(resRHS.getOpKind()) {
305  case OR:
306  if(resRHS[1].isAnd()) { // (\alpha or (\beta and \gamma))
307  break;
308  }
309  // (\alpha or \gamma) - fall through (same as the AND case)
310  case AND: { // (\beta and \gamma)
311  changed.push_back(1);
312  gamma = resRHS[1];
313  // \gamma <=> \gamma'
314  gammaThm = rewriteBV(gamma,2);
315  //\gamma' <=> \gamma"
316  Theorem thm3 = bitBlastIneqn(gammaThm.getRHS());
317  //Theorem thm3 = bitBlastIneqn(gamma);
318  //\gamma <=> \gamma' <=> \gamma"
319  thm3 = transitivityRule(gammaThm, thm3);
320  thms.push_back(thm3);
321  // (\beta and \gamma) <=> (\beta and \gamma")
322  thm3 = substitutivityRule(resRHS,changed,thms);
323  res = transitivityRule(res, thm3);
324  break;
325  }
326  default: // (\gamma)
327  IF_DEBUG(gamma = resRHS;)
328  // \gamma <=> \gamma'
329  gammaThm = rewriteBV(resRHS,2);
330  //\gamma' <=> \gamma"
331  Theorem thm3 = bitBlastIneqn(gammaThm.getRHS());
332  //Theorem thm3 = bitBlastIneqn(gamma);
333  //\gamma <=> \gamma' <=> \gamma"
334  thm3 = transitivityRule(gammaThm, thm3);
335  res = transitivityRule(res, thm3);
336  break;
337  }
338 
339  DebugAssert(kind == gamma.getOpKind(),
340  "TheoryBitvector::bitBlastIneqn: "
341  "gamma must be a BVLT/BVLE. gamma = " +
342  gamma.toString());
343  */
344  }
345  }
346  TRACE("bitvector", "bitBlastIneqn => ", res.toString(), " }");
347  return res;
348 }
349 
350 
351 /*! The invariant maintained by this function is: accepts a bitvector
352  * term, t,and a bitPosition, i. returns a formula over the set of
353  * propositional variables defined using BOOLEXTRACT of bitvector
354  * variables in t at the position i.
355  *
356  * \return Theorem(BOOLEXTRACT(t, bitPosition) <=> phi), where phi is
357  * a Boolean formula over the individual bits of bit-vector variables.
358  */
359 Theorem TheoryBitvector::bitBlastTerm(const Expr& t, int bitPosition)
360 {
361  TRACE("bitvector", "bitBlastTerm(", t, ", " + int2string(bitPosition) + ") {");
362 
363  IF_DEBUG(Type type = t.getType();)
364  DebugAssert(BITVECTOR == type.getExpr().getOpKind(), "TheoryBitvector::bitBlastTerm: The type of input to bitBlastTerm must be BITVECTOR.\n t = " +t.toString());
365  DebugAssert(bitPosition >= 0, "TheoryBitvector::bitBlastTerm: illegal bitExtraction attempted.\n bitPosition = " + int2string(bitPosition));
366 
367  Theorem result;
368 
369  // Check the cache
370  Expr t_i = newBoolExtractExpr(t, bitPosition);
371  CDMap<Expr,Theorem>::iterator it = d_bitvecCache.find(t_i);
372  if (it != d_bitvecCache.end()) {
373  result = (*it).second;
374  TRACE("bitvector", "bitBlastTerm[cached] => ", result, " }");
375  DebugAssert(t_i == result.getLHS(), "TheoryBitvector::bitBlastTerm: created wrong theorem" + result.toString() + t_i.toString());
376  return result;
377  }
378 
379  // Construct the theorem t[bitPosition] <=> \theta_i and put it into
380  // d_bitvecCache
381  switch(t.getOpKind()) {
382  case BVCONST:
383  result = d_rules->bitExtractConstant(t, bitPosition);
384  break;
385  case CONCAT:
386  {
387  Theorem thm = d_rules->bitExtractConcatenation(t, bitPosition);
388  const Expr& boolExtractTerm = thm.getRHS();
389  DebugAssert(BOOLEXTRACT == boolExtractTerm.getOpKind(), "TheoryBitvector::bitBlastTerm: recursion: term must be bool_extract");
390  const Expr& term = boolExtractTerm[0];
391  int bitPos = getBoolExtractIndex(boolExtractTerm);
392  TRACE("bitvector", "term for bitblastTerm recursion:(", term.toString(), ")");
393  result = transitivityRule(thm, bitBlastTerm(term, bitPos));
394  break;
395  }
396  case EXTRACT:
397  {
398  Theorem thm = d_rules->bitExtractExtraction(t, bitPosition);
399  const Expr& boolExtractTerm = thm.getRHS();
400  DebugAssert(BOOLEXTRACT == boolExtractTerm.getOpKind(), "TheoryBitvector::bitBlastTerm: recursion: term must be bool_extract");
401  const Expr& term = boolExtractTerm[0];
402  int bitPos = getBoolExtractIndex(boolExtractTerm);
403  TRACE("bitvector", "term for bitblastTerm recursion:(", term, ")");
404  result = transitivityRule(thm, bitBlastTerm(term, bitPos));
405  break;
406  }
408  {
409  result = d_rules->bitExtractFixedLeftShift(t, bitPosition);
410  const Expr& extractTerm = result.getRHS();
411  if(BOOLEXTRACT == extractTerm.getOpKind())
412  result = transitivityRule(result, bitBlastTerm(extractTerm[0], getBoolExtractIndex(extractTerm)));
413  break;
414  }
415  case BVSHL:
416  {
417  // BOOLEXTRACT(bvshl(t,x),i) <=> ((x = 0) AND BOOLEXTRACT(t,i)) OR
418  // ((x = 1) AND BOOLEXTRACT(t,i-1)) OR ...
419  // ((x = i) AND BOOLEXTRACT(t,0))
420  Theorem thm = d_rules->bitExtractBVSHL(t, bitPosition);
421  // bitblast the equations and extractions
422  vector<Theorem> thms, thms0;
423  int bvsize = BVSize(t);
424  for (int i = 0; i <= bitPosition; ++i) {
425  thms0.push_back(bitBlastEqn(t[1].eqExpr(newBVConstExpr(i, bvsize))));
426  thms0.push_back(bitBlastTerm(t[0], bitPosition-i));
427  thms.push_back(substitutivityRule(AND, thms0));
428  thms0.clear();
429  }
430  // Put it all together
431  if (thms.size() == 1) {
432  result = transitivityRule(thm, thms[0]);
433  }
434  else {
435  Theorem thm2 = substitutivityRule(OR, thms);
436  result = transitivityRule(thm, thm2);
437  }
438  break;
439  }
440  case BVLSHR:
441  {
442  // BOOLEXTRACT(bvlshr(t,x),i) <=> ((x = 0) AND BOOLEXTRACT(t,i)) OR
443  // ((x = 1) AND BOOLEXTRACT(t,i+1)) OR ...
444  // ((x = n-1-i) AND BOOLEXTRACT(t,n-1))
445  Theorem thm = d_rules->bitExtractBVLSHR(t, bitPosition);
446  // bitblast the equations and extractions
447  vector<Theorem> thms, thms0;
448  int bvsize = BVSize(t);
449  for (int i = 0; i <= bvsize-1-bitPosition; ++i) {
450  thms0.push_back(bitBlastEqn(t[1].eqExpr(newBVConstExpr(i, bvsize))));
451  thms0.push_back(bitBlastTerm(t[0], bitPosition+i));
452  thms.push_back(substitutivityRule(AND, thms0));
453  thms0.clear();
454  }
455  // Put it all together
456  if (thms.size() == 1) {
457  result = transitivityRule(thm, thms[0]);
458  }
459  else {
460  Theorem thm2 = substitutivityRule(OR, thms);
461  result = transitivityRule(thm, thm2);
462  }
463  break;
464  }
465  case BVASHR:
466  {
467  // BOOLEXTRACT(bvlshr(t,x),i) <=> ((x = 0) AND BOOLEXTRACT(t,i)) OR
468  // ((x = 1) AND BOOLEXTRACT(t,i+1)) OR ...
469  // ((x >= n-1-i) AND BOOLEXTRACT(t,n-1))
470  Theorem thm = d_rules->bitExtractBVASHR(t, bitPosition);
471  // bitblast the equations and extractions
472  vector<Theorem> thms, thms0;
473  int bvsize = BVSize(t);
474  int i = 0;
475  for (; i < bvsize-1-bitPosition; ++i) {
476  thms0.push_back(bitBlastEqn(t[1].eqExpr(newBVConstExpr(i, bvsize))));
477  thms0.push_back(bitBlastTerm(t[0], bitPosition+i));
478  thms.push_back(substitutivityRule(AND, thms0));
479  thms0.clear();
480  }
481  Expr leExpr = newBVLEExpr(newBVConstExpr(i, bvsize), t[1]);
482  thms0.push_back(bitBlastIneqn(leExpr));
483  thms0.push_back(bitBlastTerm(t[0], bvsize-1));
484  thms.push_back(substitutivityRule(AND, thms0));
485  // Put it all together
486  if (thms.size() == 1) {
487  result = transitivityRule(thm, thms[0]);
488  }
489  else {
490  Theorem thm2 = substitutivityRule(OR, thms);
491  result = transitivityRule(thm, thm2);
492  }
493  break;
494  }
495  case BVOR:
496  case BVAND:
497  case BVXOR:
498  {
499  int kind = t.getOpKind();
500  int resKind = (kind == BVOR) ? OR :
501  kind == BVAND ? AND : XOR;
502  Theorem thm = d_rules->bitExtractBitwise(t, bitPosition, kind);
503  const Expr& phi = thm.getRHS();
504  DebugAssert(phi.getOpKind() == resKind && phi.arity() == t.arity(), "TheoryBitvector::bitBlastTerm: recursion:\n phi = " + phi.toString() + "\n t = " + t.toString());
505  vector<Theorem> substThms;
506  for(Expr::iterator i=phi.begin(), iend=phi.end(); i!=iend; ++i) {
507  DebugAssert(i->getOpKind() == BOOLEXTRACT, "Expected BOOLEXTRACT");
508  substThms.push_back(bitBlastTerm((*i)[0], getBoolExtractIndex(*i)));
509  }
510  result = transitivityRule(thm, substitutivityRule(resKind, substThms));
511  break;
512  }
513  case BVNEG:
514  {
515  Theorem thm = d_rules->bitExtractNot(t, bitPosition);
516  const Expr& extractTerm = thm.getRHS();
517  DebugAssert(NOT == extractTerm.getKind(), "TheoryBitvector::bitBlastTerm: recursion: term must be NOT");
518  const Expr& term0 = extractTerm[0];
519  DebugAssert(BOOLEXTRACT == term0.getOpKind(), "TheoryBitvector::bitBlastTerm: recursion:(terms must be BOOL-EXTRACT");
520  int bitPos0 = getBoolExtractIndex(term0);
521  std::vector<Theorem> res;
522  res.push_back(bitBlastTerm(term0[0], bitPos0));
523  result = transitivityRule(thm, substitutivityRule(NOT, res));
524  break;
525  }
526  case BVPLUS:
527  {
528  Theorem thm_binary;
529  if(t.arity() > 2) thm_binary = d_rules->bvPlusAssociativityRule(t);
530  else thm_binary = reflexivityRule(t);
531 
532  Expr bvPlusTerm = thm_binary.getRHS();
533 
534  // Get the bits of the right multiplicand
535  Expr b = bvPlusTerm[1];
536  vector<Theorem> b_bits(bitPosition + 1);
537  for (int bit = bitPosition; bit >= 0; -- bit)
538  b_bits[bit] = bitBlastTerm(b, bit);
539 
540  // The output of the bit-blasting
541  vector<Theorem> output_bits;
542 
543  // Get the bits of the left multiplicand
544  Expr a = bvPlusTerm[0];
545  vector<Theorem> a_bits(bitPosition + 1);
546  for (int bit = bitPosition; bit >= 0; -- bit)
547  a_bits[bit] = bitBlastTerm(a, bit);
548 
549  // Bit-blast them and get all the output bits (of this size)
550  d_rules->bitblastBVPlus(a_bits, b_bits, bvPlusTerm, output_bits);
551 
552  // Simplify all the resulting bit expressions and add them to the bit-blasting cache
553  Theorem thm;
554  for (int bit = 0; bit <= bitPosition; bit ++)
555  {
556  thm = output_bits[bit];
557 
558  Expr original_boolextract = newBoolExtractExpr(t, bit);
559  Expr boolextract = thm.getLHS();
560  Expr bitblasted = thm.getRHS();
561 
562  CDMap<Expr,Theorem>::iterator it = d_bitvecCache.find(boolextract);
563  if (it != d_bitvecCache.end())
564  continue;
565 
566  thm = d_bitvecCache[boolextract] = transitivityRule(thm, rewriteBoolean(thm.getRHS()));
567  if (boolextract != original_boolextract)
568  thm = d_bitvecCache[original_boolextract] = transitivityRule(substitutivityRule(original_boolextract, thm_binary), thm);
569  }
570 
571  // We are returning the last theorem
572  return thm;
573 
574  break;
575  }
576  case BVMULT: {
577 
578  Theorem thm;
579 
580  bool a_is_const = (BVCONST == t[0].getKind());
581 
582  // If a constant, rewrite using addition
583  if (a_is_const) {
584  thm = d_rules->bitExtractConstBVMult(t, bitPosition);
585  const Expr& boolExtractTerm = thm.getRHS();
586  const Expr& term = boolExtractTerm[0];
587  result = transitivityRule(thm, bitBlastTerm(term, bitPosition));
588  break;
589  }
590 
591  // Get the bits ot the right multiplicant
592  Expr b = t[1];
593  vector<Theorem> b_bits(bitPosition + 1);
594  for (int bit = bitPosition; bit >= 0; -- bit)
595  b_bits[bit] = bitBlastTerm(b, bit);
596 
597  // The output of the bitblasting
598  vector<Theorem> output_bits;
599 
600  // Get the bits of the left multiplicant
601  Expr a = t[0];
602  vector<Theorem> a_bits(bitPosition + 1);
603  for (int bit = bitPosition; bit >= 0; -- bit)
604  a_bits[bit] = bitBlastTerm(a, bit);
605 
606  // Bitblast them and get all the output bits (of this size)
607  d_rules->bitblastBVMult(a_bits, b_bits, t, output_bits);
608 
609  // Simplify all the resulting bit expressions and add them to the bitblasting cache
610  for (int bit = 0; bit <= bitPosition; bit ++)
611  {
612  thm = output_bits[bit];
613 
614  Expr boolextract = thm.getLHS();
615  Expr bitblasted = thm.getRHS();
616 
617  CDMap<Expr,Theorem>::iterator it = d_bitvecCache.find(boolextract);
618  if (it != d_bitvecCache.end())
619  continue;
620 
621  thm = d_bitvecCache[boolextract] = transitivityRule(thm, rewriteBoolean(thm.getRHS()));
622  // not allowed to use simplify in bitblasting
623  //theoryCore()->simplify(thm.getRHS()));
624  }
625 
626  // We are returning the last theorem
627  return thm;
628 
629  break;
630  }
631 // case BVMULT: {
632 //
633 // Theorem thm;
634 // if(BVCONST == t[0].getKind())
635 // thm = d_rules->bitExtractConstBVMult(t, bitPosition);
636 // else
637 // thm = d_rules->bitExtractBVMult(t, bitPosition);
638 // const Expr& boolExtractTerm = thm.getRHS();
639 // const Expr& term = boolExtractTerm[0];
640 // result = transitivityRule(thm, bitBlastTerm(term, bitPosition));
641 // break;
642 // }
643  default:
644  {
645  FatalAssert(theoryOf(t.getOpKind()) != this, "Unexpected operator in bitBlastTerm:" + t.toString());
646  //we have bitvector variable. check if the expr is indeed a BITVECTOR.
647  IF_DEBUG(Type type = t.getType();)
648  DebugAssert(BITVECTOR == (type.getExpr()).getOpKind(), "BitvectorTheoremProducer::bitBlastTerm: the type must be BITVECTOR");
649  //check if 0<= i < length of BITVECTOR
650  IF_DEBUG(int bvLength=BVSize(t);)
651  DebugAssert(0 <= bitPosition && bitPosition < bvLength, "BitvectorTheoremProducer::bitBlastTerm: the bitextract position must be legal");
652  TRACE("bitvector", "bitBlastTerm: blasting variables(", t, ")");
653  const Expr bitExtract = newBoolExtractExpr(t, bitPosition);
654  result = reflexivityRule(bitExtract);
655  TRACE("bitvector", "bitBlastTerm: blasting variables(", t, ")");
656  break;
657  }
658  }
659  DebugAssert(!result.isNull(), "TheoryBitvector::bitBlastTerm()");
660  Theorem simpThm = rewriteBoolean(result.getRHS());
661  // not allowed to use simplify in bitblasting
662  // theoryCore()->simplify(result.getRHS());
663  result = transitivityRule(result, simpThm);
664  d_bitvecCache[t_i] = result;
665  DebugAssert(t_i == result.getLHS(),
666  "TheoryBitvector::bitBlastTerm: "
667  "created wrong theorem.\n result = "
668  +result.toString()
669  +"\n t_i = "+t_i.toString());
670  TRACE("bitvector", "bitBlastTerm => ", result, " }");
671  return result;
672 }
673 
674 
675 // Rewriting methods
676 
677 
678 //! Check that all the kids of e are BVCONST
679 static bool constantKids(const Expr& e) {
680  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
681  if(!i->isRational() && i->getKind() != BVCONST) return false;
682  return true;
683 }
684 
685 
686 //! Search for all the BVCONST kids of e, and return their indices in idxs
687 static void constantKids(const Expr& e, vector<int>& idxs) {
688  for(int i=0, iend=e.arity(); i<iend; ++i)
689  if(e[i].getKind() == BVCONST) idxs.push_back(i);
690 }
691 
692 
693 // Recursively descend into the expression e, keeping track of whether
694 // we are under even or odd number of negations ('neg' == true means
695 // odd, the context is "negative").
696 // Produce a proof of e <==> e' or !e <==> e', depending on whether
697 // neg is false or true, respectively.
698 // This function must be called only from the pushNegation function
699 Theorem TheoryBitvector::pushNegationRec(const Expr& e)
700 {
701  TRACE("pushNegation", "pushNegationRec(", e,") {");
702  DebugAssert(e.getKind() == BVNEG, "Expected BVNEG in pushNegationRec");
703  ExprMap<Theorem>::iterator i = d_pushNegCache.find(e);
704  if(i != d_pushNegCache.end()) { // Found cached result
705  TRACE("TheoryBitvector::pushNegation",
706  "pushNegationRec [cached] => ", (*i).second, "}");
707  return (*i).second;
708  }
709  Theorem res(reflexivityRule(e));
710 
711  switch(e[0].getOpKind()) {
712  case BVCONST:
713  res = d_rules->negConst(e);
714  break;
715  case BVNEG:{
716  res = d_rules->negNeg(e);
717  break;
718  }
719  case BVAND: {
720  //demorgan's laws.
721  Theorem thm0 = d_rules->negBVand(e);
722  Expr ee = thm0.getRHS();
723  if (ee.arity() == 0) res = thm0;
724  else {
725  //process each negated kid
726  Op op = ee.getOp();
727  vector<Theorem> thms;
728  for(Expr::iterator i=ee.begin(), iend=ee.end(); i!=iend; ++i)
729  thms.push_back(pushNegationRec(*i));
730  res = substitutivityRule(op, thms);
731  res = transitivityRule(thm0, res);
732  }
733  break;
734  }
735  case BVOR: {
736  //demorgan's laws.
737  Theorem thm0 = d_rules->negBVor(e);
738  Expr ee = thm0.getRHS();
739  if (ee.arity() == 0) res = thm0;
740  else {
741  //process each negated kid
742  Op op = ee.getOp();
743  vector<Theorem> thms;
744  for(Expr::iterator i=ee.begin(), iend=ee.end(); i!=iend; ++i)
745  thms.push_back(pushNegationRec(*i));
746  res = substitutivityRule(op, thms);
747  res = transitivityRule(thm0, res);
748  }
749  break;
750  }
751  case BVXOR: {
752  res = d_rules->negBVxor(e);
753  Expr ee = res.getRHS();
754 
755  // only the first child is negated
756  Theorem thm0 = pushNegationRec(ee[0]);
757  if (!thm0.isRefl()) {
758  thm0 = substitutivityRule(ee, 0, thm0);
759  res = transitivityRule(res, thm0);
760  }
761  break;
762  }
763  case BVXNOR: {
764  res = d_rules->negBVxnor(e);
765  break;
766  }
767  case CONCAT: {
768  //demorgan's laws.
769  Theorem thm0 = d_rules->negConcat(e);
770  Expr ee = thm0.getRHS();
771  if (ee.arity() == 0) res = thm0;
772  else {
773  //process each negated kid
774  Op op = ee.getOp();
775  vector<Theorem> thms;
776  for(Expr::iterator i=ee.begin(), iend=ee.end(); i!=iend; ++i)
777  thms.push_back(pushNegationRec(*i));
778  res = substitutivityRule(op, thms);
779  res = transitivityRule(thm0, res);
780  }
781  break;
782  }
783  case BVPLUS:
784  // FIXME: Need to implement the following transformation:
785  // ~(x+y) <=> ~x+~y+1
786  // (because ~(x+y)+1= -(x+y) = -x-y = ~x+1+~y+1)
787  case BVMULT:
788  // FIXME: Need to implement the following transformation:
789  // ~(x*y) <=> (~x+1)*y-1
790  // [ where we prefer x to be constant/AND/OR/NEG and then
791  // BVPLUS, and only then everything else].
792  // (because ~(x*y)+1= -(x+y) = (-x)*y = (~x+1)*y)
793  default:
794  res = reflexivityRule(e);
795  break;
796  }
797  TRACE("TheoryBitvector::pushNegation", "pushNegationRec => ", res, "}");
798  d_pushNegCache[e] = res;
799  return res;
800 }
801 
802 
803 // We assume that the cache is initially empty
804 Theorem TheoryBitvector::pushNegation(const Expr& e) {
805  d_pushNegCache.clear();
806  DebugAssert(BVNEG == e.getOpKind(), "Expected BVNEG");
807  return pushNegationRec(e);
808 }
809 
810 
811 //! Top down simplifier
812 Theorem TheoryBitvector::simplifyOp(const Expr& e) {
813  if (e.arity() > 0) {
814  Expr ee(e);
815  Theorem thm0;
816  switch(e.getOpKind()) {
817  case BVNEG:
818  thm0 = pushNegation(e);
819  break;
820  case EXTRACT:
821  switch(e[0].getOpKind()) {
822  case BVPLUS:
823  thm0 = d_rules->extractBVPlus(e);
824  break;
825  case BVMULT:
826  thm0 = d_rules->extractBVMult(e);
827  break;
828  default:
829  thm0 = reflexivityRule(e);
830  break;
831  }
832  break;
833  case BVPLUS:
834  break;
835  case BVMULT:
836  // thm0 = d_rules->padBVMult(e);
837  break;
838  case CONCAT: // 0bin0_[k] @ BVPLUS(n, args) => BVPLUS(n+k, args)
839 // if(e.arity()==2 && e[0].getKind()==BVCONST && e[1].getOpKind()==BVPLUS
840 // && computeBVConst(e[0]) == 0) {
841 // thm0 = d_rules->bvplusZeroConcatRule(e);
842 // }
843  break;
844  case RIGHTSHIFT:
845  thm0 = d_rules->rightShiftToConcat(e);
846  break;
847  case LEFTSHIFT:
848  thm0 = d_rules->leftShiftToConcat(e);
849  break;
851  thm0 = d_rules->constWidthLeftShiftToConcat(e);
852  break;
853  default:
854  thm0 = reflexivityRule(e);
855  break;
856  }
857  vector<Theorem> newChildrenThm;
858  vector<unsigned> changed;
859  if(thm0.isNull()) thm0 = reflexivityRule(e);
860  ee = thm0.getRHS();
861  int ar = ee.arity();
862  for(int k = 0; k < ar; ++k) {
863  // Recursively simplify the kids
864  Theorem thm = simplify(ee[k]);
865  if (thm.getLHS() != thm.getRHS()) {
866  newChildrenThm.push_back(thm);
867  changed.push_back(k);
868  }
869  }
870  if(changed.size() > 0) {
871  Theorem thm1 = substitutivityRule(ee, changed, newChildrenThm);
872  return transitivityRule(thm0,thm1);
873  } else
874  return thm0;
875  }
876  return reflexivityRule(e);
877 }
878 
879 
880 // Theorem TheoryBitvector::rewriteConst(const Expr& e)
881 // {
882 // Theorem result = reflexivityRule(e);
883 // return result;
884 // }
885 
886 
887 Theorem TheoryBitvector::rewriteBV(const Expr& e, ExprMap<Theorem>& cache, int n)
888 {
889  TRACE("bitvector rewrite", "TheoryBitvector::rewriteBV(", e, ") {");
890 
891  if (n <= 0) return reflexivityRule(e);
892 
893  Theorem res;
894 
895  if(n >= 2) {
896  // rewrite children recursively
897  Theorem thm;
898  vector<Theorem> thms;
899  vector<unsigned> changed;
900  for(int i=0, iend=e.arity(); i<iend; ++i) {
901  thm = rewriteBV(e[i], cache, n-1);
902  if(thm.getLHS() != thm.getRHS()) {
903  thms.push_back(thm);
904  changed.push_back(i);
905  }
906  }
907  if(changed.size() > 0) {
908  thm = substitutivityRule(e, changed, thms);
909  return transitivityRule(thm, rewriteBV(thm.getRHS(), cache));
910  }
911  // else fall through
912  }
913 
914  // Check the cache
915  ExprMap<Theorem>::iterator it = cache.find(e);
916  if (it != cache.end()) {
917  res = (*it).second;
918  TRACE("bitvector rewrite", "TheoryBitvector::rewrite["+int2string(n)
919  +"][cached] => ", res.getExpr(), " }");
920  IF_DEBUG(debugger.counter("bv rewriteBV[n] cache hits")++;)
921  return res;
922  }
923 
924  // Main rewrites
925  switch(e.getOpKind()) {
926  case NOT:
927  switch (e[0].getKind()) {
928  case BVLT:
929  case BVLE:
930  res = d_rules->notBVLTRule(e);
931  if (!res.isRefl()) {
932  res = transitivityRule(res, simplify(res.getRHS()));
933  }
934  break;
935  case EQ:
936  if (BVSize(e[0][0]) == 1) {
937  res = d_rules->notBVEQ1Rule(e);
938  res = transitivityRule(res, simplify(res.getRHS()));
939  break;
940  }
941  break;
942  }
943  break;
944  case EQ:
945  {
946  // Canonise constant equations to true or false
947  if (e[0].getKind() == BVCONST && e[1].getKind() == BVCONST) {
948  res = d_rules->constEq(e);
949  } else
950  // If x_1 or x_2 = 0 then both have to be 0
951  if (e[0].getKind() == BVOR && e[1].getKind() == BVCONST && computeBVConst(e[1]) == 0) {
952  res = d_rules->zeroBVOR(e);
953  res = transitivityRule(res, simplify(res.getRHS()));
954  }
955  // if x_1 and x_2 = 1 then both have to be 1
956  else if (e[0].getKind() == BVAND && e[1].getKind() == BVCONST && computeBVConst(e[1]) == pow(BVSize(e[1]), (Unsigned)2) - 1) {
957  res = d_rules->oneBVAND(e);
958  res = transitivityRule(res, simplify(res.getRHS()));
959  }
960  // Solve
961  else {
962  res = d_rules->canonBVEQ(e);
963  if (!res.isRefl()) {
964  res = transitivityRule(res, simplify(res.getRHS()));
965  }
966  else e.setRewriteNormal();
967  }
968  break;
969  }
970  case BVCONST:
971  {
972  res = reflexivityRule(e);
973  break;
974  }
975  case CONCAT: {
976  // First, flatten concatenation
977  res = d_rules->concatFlatten(e);
978  TRACE("bitvector rewrite", "rewriteBV (CONCAT): flattened = ",
979  res.getRHS(), "");
980  // Search for adjacent constants and accumulate the vector of
981  // nested concatenations (@ t1 ... (@ c1 ... ck) ... tn), and the
982  // indices of constant concatenations in this new expression.
983  // We'll connect this term to 'e' by inverse of flattenning, and
984  // rewrite concatenations of constants into bitvector constants.
985  vector<unsigned> idxs;
986  vector<Expr> kids; // Kids of the new concatenation
987  vector<Theorem> thms; // Rewrites of constant concatenations
988  vector<Expr> nestedKids; // Kids of the current concatenation of constants
989  // res will be overwritten, using const Expr& may be dangerous
990  Expr e1 = res.getRHS();
991  for(int i=0, iend=e1.arity(); i<iend; ++i) {
992  TRACE("bitvector rewrite", "rewriteBV: e["+int2string(i)+"]=",
993  e1[i], "");
994  if(e1[i].getKind() == BVCONST) {
995  // INVARIANT: if it is the first constant in a batch,
996  // then nestedKids must be empty.
997  nestedKids.push_back(e1[i]);
998  TRACE("bitvector rewrite", "rewriteBV: queued up BVCONST: ",
999  e1[i], "");
1000  } else { // e1[i] is not a BVCONST
1001  if(nestedKids.size() > 0) { // This is the end of a batch
1002  if(nestedKids.size() >= 2) { // Create a nested const concat
1003  Expr cc = newConcatExpr(nestedKids);
1004  idxs.push_back(kids.size());
1005  kids.push_back(cc);
1006  thms.push_back(d_rules->concatConst(cc));
1007  TRACE("bitvector rewrite", "rewriteBV: wrapping ", cc, "");
1008  } else { // A single constant, add it as it is
1009  TRACE("bitvector rewrite", "rewriteBV: single const ",
1010  nestedKids[0], "");
1011  kids.push_back(nestedKids[0]);
1012  }
1013  nestedKids.clear();
1014  }
1015  // Add the current non-constant BV
1016  kids.push_back(e1[i]);
1017  }
1018  }
1019  // Handle the last BVCONST
1020  if(nestedKids.size() > 0) {
1021  if(nestedKids.size() >= 2) { // Create a nested const concat
1022  Expr cc = newConcatExpr(nestedKids);
1023  idxs.push_back(kids.size());
1024  kids.push_back(cc);
1025  thms.push_back(d_rules->concatConst(cc));
1026  TRACE("bitvector rewrite", "rewriteBV: wrapping ", cc, "");
1027  } else { // A single constant, add it as it is
1028  kids.push_back(nestedKids[0]);
1029  TRACE("bitvector rewrite", "rewriteBV: single const ",
1030  nestedKids[0], "");
1031  }
1032  nestedKids.clear();
1033  }
1034  // If there are any constants to merge, do the merging
1035  if(idxs.size() > 0) {
1036  // CONCAT with constants groupped
1037  if(kids.size() == 1) { // Special case: all elements are constants
1038  DebugAssert(thms.size() == 1, "TheoryBitvector::rewriteBV:\n"
1039  "case CONCAT: all constants. thms.size() == "
1040  +int2string(thms.size()));
1041  res = transitivityRule(res, thms[0]);
1042  } else {
1043  Expr ee = newConcatExpr(kids);
1044 
1045  Theorem constMerge = substitutivityRule(ee, idxs, thms);
1046  // The inverse flattening of ee
1047  Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee));
1048  // Putting it together: Theorem(e==e'), where e' has constants merged
1049  res = transitivityRule(res, unFlatten);
1050  res = transitivityRule(res, constMerge);
1051  }
1052  }
1053 
1054  // Now do a similar search for mergeable extractions
1055  idxs.clear();
1056  thms.clear();
1057  kids.clear();
1058  // nestedKids must already be empty
1059  DebugAssert(nestedKids.size() == 0,
1060  "rewriteBV() case CONCAT, end of const merge");
1061  Expr prevExpr; // Previous base of extraction (initially Null)
1062  // The first and the last bit in the batch of mergeable extractions
1063  int hi(-1), low(-1);
1064  // Refresh e1
1065  e1 = res.getRHS();
1066  for(int i=0, iend=e1.arity(); i<iend; ++i) {
1067  const Expr& ei = e1[i];
1068  if(ei.getOpKind() == EXTRACT) {
1069  if(nestedKids.size() > 0 && ei[0] == prevExpr
1070  && (low-1) == getExtractHi(ei)) {
1071  // Continue to accumulate the current batch
1072  nestedKids.push_back(ei);
1073  low = getExtractLow(ei);
1074  } else { // Start a new batch
1075  // First, check if there was a batch before that
1076  if(nestedKids.size() >= 2) { // Create a nested const concat
1077  Expr cc = newConcatExpr(nestedKids);
1078  idxs.push_back(kids.size());
1079  kids.push_back(cc);
1080  thms.push_back(d_rules->concatMergeExtract(cc));
1081  nestedKids.clear();
1082  } else if(nestedKids.size() == 1) {
1083  // A single extraction, add it as it is
1084  kids.push_back(nestedKids[0]);
1085  nestedKids.clear();
1086  }
1087  // Now, actually start a new batch
1088  nestedKids.push_back(ei);
1089  hi = getExtractHi(ei);
1090  low = getExtractLow(ei);
1091  prevExpr = ei[0];
1092  }
1093  } else { // e1[i] is not an EXTRACT
1094  if(nestedKids.size() >= 2) { // Create a nested const concat
1095  Expr cc = newConcatExpr(nestedKids);
1096  idxs.push_back(kids.size());
1097  kids.push_back(cc);
1098  thms.push_back(d_rules->concatMergeExtract(cc));
1099  } else if(nestedKids.size() == 1) {
1100  // A single extraction, add it as it is
1101  kids.push_back(nestedKids[0]);
1102  }
1103  nestedKids.clear();
1104  // Add the current non-EXTRACT BV
1105  kids.push_back(ei);
1106  }
1107  }
1108  // Handle the last batch of extractions
1109  if(nestedKids.size() >= 2) { // Create a nested const concat
1110  Expr cc = newConcatExpr(nestedKids);
1111  idxs.push_back(kids.size());
1112  kids.push_back(cc);
1113  // The extraction may include all the bits, we need to rewrite again
1114  thms.push_back(rewriteBV(d_rules->concatMergeExtract(cc), cache, 1));
1115  } else if(nestedKids.size() == 1) {
1116  // A single extraction, add it as it is
1117  kids.push_back(nestedKids[0]);
1118  }
1119  // If there are any extractions to merge, do the merging
1120  if(idxs.size() > 0) {
1121  // CONCAT with extractions groupped
1122  if(kids.size() == 1) { // Special case: all elements merge together
1123  DebugAssert(thms.size() == 1, "TheoryBitvector::rewriteBV:\n"
1124  "case CONCAT: all extracts merge. thms.size() == "
1125  +int2string(thms.size()));
1126  res = thms[0];
1127  } else {
1128  Expr ee = newConcatExpr(kids);
1129  Theorem extractMerge = substitutivityRule(ee, idxs, thms);
1130  // The inverse flattening of ee
1131  Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee));
1132  // Putting it together: Theorem(e==e'), where e' has extractions merged
1133  res = transitivityRule(res, unFlatten);
1134  res = transitivityRule(res, extractMerge);
1135  }
1136  }
1137  // Check for 0bin00 @ BVPLUS(n, ...). Most of the time, this
1138  // case will be handled during the top-down phase
1139  // (simplifyOp()), but not always.
1140 // Expr ee = res.getRHS();
1141 // if(ee.getOpKind()==CONCAT && ee.arity() == 2 && ee[0].getKind()==BVCONST
1142 // && ee[1].getOpKind()==BVPLUS && computeBVConst(ee[0]) == 0) {
1143 // // Push the concat down through BVPLUS
1144 // Theorem thm = d_rules->bvplusZeroConcatRule(ee);
1145 // if(thm.getLHS()!=thm.getRHS()) {
1146 // thm = transitivityRule(thm, d_rules->padBVPlus(thm.getRHS()));
1147 // // Kids may need to be rewritten again
1148 // res = rewriteBV(transitivityRule(res, thm), cache, 2);
1149 // }
1150 // }
1151  // Since we may have pulled subexpressions from more than one
1152  // level deep, we cannot guarantee that all the new kids are
1153  // fully simplified, and have to call simplify explicitly again.
1154  // Since this is potentially an expensive operation, we try to
1155  // minimize the need for it:
1156 
1157  // * check if the result has a find pointer (then kids don't
1158  // need to be simplified),
1159  // * check if any of the kids simplify (if not, don't bother).
1160  // If kids are already simplified, we'll hit the simplifier
1161  // cache. It's only expensive when kids do indeed simplify.
1162  if(!res.isRefl() && (theoryCore()->inUpdate() || !res.getRHS().hasFind())) {
1163  res = transitivityRule(res, simplify(res.getRHS()));
1164  }
1165  break;
1166  }
1167  case EXTRACT: {
1168  DebugAssert(e.arity() == 1, "TheoryBitvector::rewriteBV: e = "
1169  +e.toString());
1170  if(getExtractLow(e) == 0 && getExtractHi(e) == BVSize(e[0])-1)
1171  res = d_rules->extractWhole(e);
1172  else {
1173  switch(e[0].getOpKind()) {
1174  case BVCONST:
1175  res = d_rules->extractConst(e);
1176  break;
1177  case EXTRACT:
1178  res = d_rules->extractExtract(e);
1179  break;
1180  case CONCAT:
1181  // Push extraction through concat, and rewrite the kids
1182  res = rewriteBV(d_rules->extractConcat(e), cache, 2);
1183  break;
1184  case BVNEG:
1185  res = rewriteBV(d_rules->extractNeg(e), cache, 2);
1186  break;
1187  case BVAND:
1188  res = rewriteBV(d_rules->extractAnd(e), cache, 2);
1189  break;
1190  case BVOR:
1191  res = rewriteBV(d_rules->extractOr(e), cache, 2);
1192  break;
1193  case BVXOR:
1194  res =
1195  rewriteBV(d_rules->extractBitwise(e, BVXOR, "extract_bvxor"), cache, 2);
1196  break;
1197  case BVMULT: {
1198  const Expr& bvmult = e[0];
1199  int hiBit = getExtractHi(e);
1200  int bvmultLen = BVSize(bvmult);
1201  // Applicable if it changes anything
1202  if(hiBit+1 < bvmultLen) {
1203  res = d_rules->extractBVMult(e);
1204  res = rewriteBV(res, cache, 3);
1205  } else
1206  res = reflexivityRule(e);
1207  break;
1208  }
1209  case BVPLUS: {
1210  const Expr& bvplus = e[0];
1211  int hiBit = getExtractHi(e);
1212  int bvplusLen = BVSize(bvplus);
1213  if(hiBit+1 < bvplusLen) {
1214  res = d_rules->extractBVPlus(e);
1215  } else res = reflexivityRule(e);
1216  break;
1217  }
1218  default:
1219  res = reflexivityRule(e);
1220  break;
1221  }
1222  }
1223  if (!res.isRefl()) {
1224  res = transitivityRule(res, simplify(res.getRHS()));
1225  }
1226  break;
1227  }
1228  case BOOLEXTRACT: {
1229  Expr t(e);
1230  // Normal form: t[0] for 1-bit t, collapse t[i:i][0] into t[i]
1231  if(BVSize(e[0]) > 1) { // transform t[i] to t[i:i][0] and rewrite
1232  res = rewriteBV(d_rules->bitExtractRewrite(e), cache, 2);
1233  t = res.getRHS();
1234  }
1235  if(t.getOpKind() == BOOLEXTRACT && t[0].getOpKind() == EXTRACT) {
1236  // Collapse t[i:i][0] to t[i]
1237  int low = getExtractLow(t[0]);
1238  if(getExtractHi(t[0]) == low) {
1239  Theorem thm(d_rules->bitExtractRewrite
1240  (newBoolExtractExpr(t[0][0], low)));
1241  thm = symmetryRule(thm);
1242  res = (res.isNull())? thm : transitivityRule(res, thm);
1243  t = res.getRHS()[0];
1244  // Make sure t in the resulting t[i] is its own find pointer
1245  // (global invariant)
1246  if(t.hasFind()) {
1247  Theorem findThm = find(t);
1248  if(t != findThm.getRHS()) {
1249  vector<Theorem> thms;
1250  thms.push_back(findThm);
1251  thm = substitutivityRule(res.getRHS().getOp(), thms);
1252  res = transitivityRule(res, thm);
1253  }
1254  }
1255  }
1256  }
1257  if(!res.isNull()) t = res.getRHS();
1258  // Rewrite a constant extraction to TRUE or FALSE
1259  if(t.getOpKind() == BOOLEXTRACT && constantKids(t)) {
1260  Theorem thm = d_rules->bitExtractConstant(t[0], getBoolExtractIndex(t));
1261  res = (res.isNull())? thm : transitivityRule(res, thm);
1262  }
1263  break;
1264  }
1265  case LEFTSHIFT:
1266  if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) {
1267  res = d_rules->bvShiftZero(e);
1268  } else {
1269  res = d_rules->leftShiftToConcat(e);
1270  if (!res.isRefl()) {
1271  res = transitivityRule(res, simplify(res.getRHS()));
1272  }
1273  }
1274  break;
1275  case CONST_WIDTH_LEFTSHIFT:
1276  if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) {
1277  res = d_rules->bvShiftZero(e);
1278  } else {
1279  res = d_rules->constWidthLeftShiftToConcat(e);
1280  if (!res.isRefl()) {
1281  res = transitivityRule(res, simplify(res.getRHS()));
1282  }
1283  }
1284  break;
1285  case RIGHTSHIFT:
1286  if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) {
1287  res = d_rules->bvShiftZero(e);
1288  } else {
1289  res = d_rules->rightShiftToConcat(e);
1290  if (!res.isRefl()) {
1291  res = transitivityRule(res, simplify(res.getRHS()));
1292  }
1293  }
1294  break;
1295  case BVSHL:
1296  if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) {
1297  res = d_rules->bvShiftZero(e);
1298  } else
1299  if (e[1].getKind() == BVCONST) {
1300  res = d_rules->bvshlToConcat(e);
1301  res = transitivityRule(res, simplify(res.getRHS()));
1302  }
1303 // else {
1304 // res = d_rules->bvshlSplit(e);
1305 // res = transitivityRule(res, simplify(res.getRHS()));
1306 // }
1307  break;
1308  case BVLSHR:
1309  if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) {
1310  res = d_rules->bvShiftZero(e);
1311  } else
1312  if (e[1].getKind() == BVCONST) {
1313  res = d_rules->bvlshrToConcat(e);
1314  res = transitivityRule(res, simplify(res.getRHS()));
1315  }
1316  break;
1317  case BVASHR:
1318  if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) {
1319  res = d_rules->bvShiftZero(e);
1320  } else
1321  if (e[1].getKind() == BVCONST) {
1322  res = d_rules->bvashrToConcat(e);
1323  res = transitivityRule(res, simplify(res.getRHS()));
1324  }
1325  break;
1326  case SX: {
1327  res = d_rules->signExtendRule(e);
1328  res = transitivityRule(res, simplify(res.getRHS()));
1329  break;
1330  }
1331 
1332  case BVZEROEXTEND:
1333  res = d_rules->zeroExtendRule(e);
1334  res = transitivityRule(res, simplify(res.getRHS()));
1335  break;
1336 
1337  case BVREPEAT:
1338  res = d_rules->repeatRule(e);
1339  res = transitivityRule(res, simplify(res.getRHS()));
1340  break;
1341 
1342  case BVROTL:
1343  res = d_rules->rotlRule(e);
1344  res = transitivityRule(res, simplify(res.getRHS()));
1345  break;
1346 
1347  case BVROTR:
1348  res = d_rules->rotrRule(e);
1349  res = transitivityRule(res, simplify(res.getRHS()));
1350  break;
1351 
1352  case BVAND:
1353  case BVOR:
1354  case BVXOR:
1355  {
1356  int kind = e.getOpKind();
1357  // Flatten the bit-wise AND, eliminate duplicates, reorder terms
1358  res = d_rules->bitwiseFlatten(e, kind);
1359  Expr ee = res.getRHS();
1360  if (ee.getOpKind() != kind) break;
1361 
1362  // Search for constant bitvectors
1363  vector<int> idxs;
1364  constantKids(ee, idxs);
1365  int idx = -1;
1366 
1367  if(idxs.size() >= 2) {
1368  res = transitivityRule(res, d_rules->bitwiseConst(ee, idxs, kind));
1369  ee = res.getRHS();
1370  if (ee.getOpKind() != kind) break;
1371  idx = 0;
1372  }
1373  else if (idxs.size() == 1) {
1374  idx = idxs[0];
1375  }
1376 
1377  if (idx >= 0) {
1378  res = transitivityRule(res, d_rules->bitwiseConstElim(ee, idx, kind));
1379  ee = res.getRHS();
1380  }
1381  if (ee.getOpKind() == kind) {
1382  res = transitivityRule(res, d_rules->bitwiseConcat(ee, kind));
1383  }
1384  if (!res.isRefl()) {
1385  res = transitivityRule(res, simplify(res.getRHS()));
1386  }
1387  else {
1388  e.setRewriteNormal();
1389  }
1390  break;
1391  }
1392  case BVXNOR: {
1393  res = d_rules->rewriteXNOR(e);
1394  res = transitivityRule(res, simplify(res.getRHS()));
1395  break;
1396  }
1397  case BVNEG: {
1398  res = pushNegation(e);
1399  if (!res.isRefl()) {
1400  res = transitivityRule(res, simplify(res.getRHS()));
1401  }
1402  break;
1403  }
1404  case BVNAND: {
1405  res = d_rules->rewriteNAND(e);
1406  res = transitivityRule(res, simplify(res.getRHS()));
1407  break;
1408  }
1409  case BVNOR: {
1410  res = d_rules->rewriteNOR(e);
1411  res = transitivityRule(res, simplify(res.getRHS()));
1412  break;
1413  }
1414  case BVCOMP: {
1415  res = d_rules->rewriteBVCOMP(e);
1416  res = transitivityRule(res, simplify(res.getRHS()));
1417  break;
1418  }
1419  case BVUMINUS:
1420  {
1421  res = d_rules->canonBVUMinus( e );
1422  res = transitivityRule(res, simplify(res.getRHS()));
1423  break;
1424  }
1425  case BVPLUS:
1426  {
1427  res = d_rules->canonBVPlus(e );
1428  if (!res.isRefl()) {
1429  res = transitivityRule(res, simplify(res.getRHS()));
1430  }
1431  else e.setRewriteNormal();
1432  break;
1433  }
1434  case BVSUB: {
1435  res = d_rules->rewriteBVSub(e);
1436  res = transitivityRule(res, simplify(res.getRHS()));
1437  break;
1438  }
1439  case BVMULT:
1440  {
1441  res = d_rules->liftConcatBVMult(e);
1442  if (!res.isRefl()) {
1443  res = transitivityRule(res, simplify(res.getRHS()));
1444  }
1445  else {
1446  res = d_rules->canonBVMult( e );
1447  if (!res.isRefl())
1448  res = transitivityRule(res, simplify(res.getRHS()));
1449  else e.setRewriteNormal();
1450  }
1451  break;
1452  }
1453 
1454  case BVUDIV:
1455  {
1456  Expr a = e[0];
1457  Expr b = e[1];
1458 
1459  // Constant division
1460  if (a.getOpKind() == BVCONST && b.getOpKind() == BVCONST) {
1461  res = d_rules->bvUDivConst(e);
1462  break;
1463  }
1464 
1465  if (theoryCore()->okToEnqueue())
1466  {
1467  // get the full theorem
1468  // e = x/y
1469  // \exists div, mod: e = div & (y != 0 -> ...)
1470  // result is the equality
1471  // assert the additional conjunct
1472  Theorem fullTheorem = d_rules->bvUDivTheorem(e);
1473  // Skolemise the variables
1474  Theorem skolem_div = getCommonRules()->skolemize(fullTheorem);
1475  // Get the rewrite part
1476  res = getCommonRules()->andElim(skolem_div, 0);
1477  // Get the division part
1478  Theorem additionalConstraint = getCommonRules()->andElim(skolem_div, 1);
1479  // Enqueue the division part
1480  enqueueFact(additionalConstraint);
1481  res = transitivityRule(res, simplify(res.getRHS()));
1482  } else {
1483  res = reflexivityRule(e);
1484  }
1485  break;
1486  }
1487  case BVSDIV:
1488  res = d_rules->bvSDivRewrite(e);
1489  res = transitivityRule(res, simplify(res.getRHS()));
1490  break;
1491  case BVUREM:
1492  {
1493  Expr a = e[0];
1494  Expr b = e[1];
1495 
1496  // Constant division
1497  if (a.getOpKind() == BVCONST && b.getOpKind() == BVCONST) {
1498  res = d_rules->bvURemConst(e);
1499  break;
1500  }
1501 
1502  res = d_rules->bvURemRewrite(e);
1503  res = transitivityRule(res, theoryCore()->simplify(res.getRHS()));
1504 
1505  break;
1506  }
1507  case BVSREM:
1508  res = d_rules->bvSRemRewrite(e);
1509  res = transitivityRule(res, simplify(res.getRHS()));
1510  break;
1511  case BVSMOD:
1512  res = d_rules->bvSModRewrite(e);
1513  res = transitivityRule(res, simplify(res.getRHS()));
1514  break;
1515  case BVLT:
1516  case BVLE: {
1517  Expr lhs = e[0];
1518  Expr rhs = e[1];
1519  if (BVSize(lhs) != BVSize(rhs)) {
1520  res = d_rules->padBVLTRule(e, BVSize(lhs) > BVSize(rhs) ? BVSize(lhs) : BVSize(rhs));
1521  res = transitivityRule(res, simplify(res.getRHS()));
1522  }
1523  else {
1524  if(lhs == rhs)
1525  res = d_rules->lhsEqRhsIneqn(e, e.getOpKind());
1526  else if (BVCONST == lhs.getKind() && BVCONST == rhs.getKind())
1527  res = d_rules->bvConstIneqn(e, e.getOpKind());
1528  else if (e.getOpKind() == BVLE && BVCONST == lhs.getKind() && computeBVConst(lhs) == 0)
1529  res = d_rules->zeroLeq(e);
1530  }
1531  break;
1532  }
1533 
1534  case BVGT:
1535  case BVGE:
1536  FatalAssert(false, "Should be eliminated at parse-time");
1537  break;
1538 
1539  case BVSLT:
1540  case BVSLE:{
1541  /*! input: e0 <=(s) e1. output depends on whether the topbits(MSB) of
1542  * e0 and e1 are constants. If they are constants then optimizations
1543  * are done. In general, the following rule is implemented.
1544  * Step1:
1545  * e0 <=(s) e1
1546  * <==>
1547  * pad(e0) <=(s) pad(e1)
1548  * Step2:
1549  * pad(e0) <=(s) pad(e1)
1550  * <==>
1551  * (e0[n-1] AND NOT e1[n-1]) OR
1552  * (e0[n-1] = e1[n-1] AND e0[n-2:0] <= e1[n-2:0])
1553  */
1554  int e0len = BVSize(e[0]);
1555  int e1len = BVSize(e[1]);
1556  int bvlength = e0len>=e1len ? e0len : e1len;
1557  //e0 <=(s) e1 <=> signpad(e0) <=(s) signpad(e1)
1558 
1559  std::vector<Theorem> thms;
1560  std::vector<unsigned> changed;
1561 
1562  //e0 <= e1 <==> pad(e0) <= pad(e1)
1563  Theorem thm = d_rules->padBVSLTRule(e, bvlength);
1564  Expr paddedE = thm.getRHS();
1565 
1566  //the rest of the code simply normalizes pad(e0) and pad(e1)
1567  Theorem thm0 = d_rules->signExtendRule(paddedE[0]);
1568  Expr rhs0 = thm0.getRHS();
1569  thm0 = transitivityRule(thm0, rewriteBV(rhs0, cache));
1570  if(thm0.getLHS() != thm0.getRHS()) {
1571  thms.push_back(thm0);
1572  changed.push_back(0);
1573  }
1574 
1575  Theorem thm1 = d_rules->signExtendRule(paddedE[1]);
1576  Expr rhs1 = thm1.getRHS();
1577  thm1 = transitivityRule(thm1, rewriteBV(rhs1, cache));
1578  if(thm1.getLHS() != thm1.getRHS()) {
1579  thms.push_back(thm1);
1580  changed.push_back(1);
1581  }
1582 
1583  if(changed.size() > 0) {
1584  thm0 = substitutivityRule(paddedE,changed,thms);
1585  thm0 = transitivityRule(thm, thm0);
1586  }
1587  else
1588  thm0 = reflexivityRule(e);
1589 
1590  //signpad(e0) <= signpad(e1)
1591  Expr thm0RHS = thm0.getRHS();
1592  DebugAssert(thm0RHS.getOpKind() == BVSLT ||
1593  thm0RHS.getOpKind() == BVSLE,
1594  "TheoryBitvector::RewriteBV");
1595  //signpad(e0)[bvlength-1:bvlength-1]
1596  const Expr MSB0 = newBVExtractExpr(thm0RHS[0],bvlength-1,bvlength-1);
1597  //signpad(e1)[bvlength-1:bvlength-1]
1598  const Expr MSB1 = newBVExtractExpr(thm0RHS[1],bvlength-1,bvlength-1);
1599  //rewritten MSB0
1600  const Theorem topBit0 = rewriteBV(MSB0, cache, 2);
1601  //rewritten MSB1
1602  const Theorem topBit1 = rewriteBV(MSB1, cache, 2);
1603  //compute e0 <=(s) e1 <==> signpad(e0) <=(s) signpad(e1) <==>
1604  //output as given above
1605  thm1 = d_rules->signBVLTRule(thm0RHS, topBit0, topBit1);
1606  thm1 = transitivityRule(thm1,simplify(thm1.getRHS()));
1607  res = transitivityRule(thm0,thm1);
1608  break;
1609  }
1610  case BVSGT:
1611  case BVSGE:
1612  FatalAssert(false, "Should be eliminated at parse-time");
1613  break;
1614  default:
1615  res = reflexivityRule(e);
1616  break;
1617  }
1618 
1619  if (res.isNull()) res = reflexivityRule(e);
1620 
1621  // Update cache
1622  cache[e] = res;
1623 
1624  TRACE("bitvector rewrite", "TheoryBitvector::rewriteBV => ",
1625  res.getExpr(), " }");
1626 
1627  return res;
1628 }
1629 
1630 
1631 Theorem TheoryBitvector::rewriteBV(const Expr& e, int n)
1632 {
1633  ExprMap<Theorem> cache;
1634  return rewriteBV(e, cache, n);
1635 }
1636 
1637 
1638 Theorem TheoryBitvector::rewriteBoolean(const Expr& e)
1639 {
1640  Theorem thm;
1641  switch (e.getKind()) {
1642  case NOT:
1643  if (e[0].isTrue())
1644  thm = getCommonRules()->rewriteNotTrue(e);
1645  else if (e[0].isFalse())
1646  thm = getCommonRules()->rewriteNotFalse(e);
1647  else if (e[0].isNot())
1648  thm = getCommonRules()->rewriteNotNot(e);
1649  break;
1650  case IFF: {
1651  thm = getCommonRules()->rewriteIff(e);
1652  const Expr& rhs = thm.getRHS();
1653  // The only time we need to rewrite the result (rhs) is when
1654  // e==(FALSE<=>e1) or (e1<=>FALSE), so rhs==!e1.
1655  if (e != rhs && rhs.isNot())
1656  thm = transitivityRule(thm, rewriteBoolean(rhs));
1657  break;
1658  }
1659  case AND:{
1660  std::vector<Theorem> newK;
1661  std::vector<unsigned> changed;
1662  unsigned count(0);
1663  for(Expr::iterator ii=e.begin(),iiend=e.end();ii!=iiend;ii++,count++) {
1664  Theorem temp = rewriteBoolean(*ii);
1665  if(temp.getLHS() != temp.getRHS()) {
1666  newK.push_back(temp);
1667  changed.push_back(count);
1668  }
1669  }
1670  if(changed.size() > 0) {
1671  Theorem res = substitutivityRule(e,changed,newK);
1672  thm = transitivityRule(res, rewriteAnd(res.getRHS()));
1673  } else
1674  thm = rewriteAnd(e);
1675  }
1676  break;
1677  case OR:{
1678  std::vector<Theorem> newK;
1679  std::vector<unsigned> changed;
1680  unsigned count(0);
1681  for(Expr::iterator ii=e.begin(),iiend=e.end();ii!=iiend;ii++,count++) {
1682  Theorem temp = rewriteBoolean(*ii);
1683  if(temp.getLHS() != temp.getRHS()) {
1684  newK.push_back(temp);
1685  changed.push_back(count);
1686  }
1687  }
1688  if(changed.size() > 0) {
1689  Theorem res = substitutivityRule(e,changed,newK);
1690  thm = transitivityRule(res, rewriteOr(res.getRHS()));
1691  } else
1692  thm = rewriteOr(e);
1693  }
1694  break;
1695 
1696  default:
1697  break;
1698  }
1699  if(thm.isNull()) thm = reflexivityRule(e);
1700 
1701  return thm;
1702 }
1703 
1704 
1705 ///////////////////////////////////////////////////////////////////////////////
1706 // TheoryBitvector Public Methods //
1707 ///////////////////////////////////////////////////////////////////////////////
1708 TheoryBitvector::TheoryBitvector(TheoryCore* core)
1709  : Theory(core, "Bitvector"),
1710  d_bvDelayEq(core->getStatistics().counter("bv delayed assert eqs")),
1711  d_bvAssertEq(core->getStatistics().counter("bv eager assert eqs")),
1712  d_bvDelayDiseq(core->getStatistics().counter("bv delayed assert diseqs")),
1713  d_bvAssertDiseq(core->getStatistics().counter("bv eager assert diseqs")),
1714  d_bvTypePreds(core->getStatistics().counter("bv type preds enqueued")),
1715  d_bvDelayTypePreds(core->getStatistics().counter("bv type preds delayed")),
1716  d_bvBitBlastEq(core->getStatistics().counter("bv bitblast eqs")),
1717  d_bvBitBlastDiseq(core->getStatistics().counter("bv bitblast diseqs")),
1718  d_bv32Flag(&(core->getFlags()["bv32-flag"].getBool())),
1719  d_bitvecCache(core->getCM()->getCurrentContext()),
1720  d_eq(core->getCM()->getCurrentContext()),
1721  d_eqPending(core->getCM()->getCurrentContext()),
1722  d_eq_index(core->getCM()->getCurrentContext(), 0, 0),
1723  d_bitblast(core->getCM()->getCurrentContext()),
1724  d_bb_index(core->getCM()->getCurrentContext(), 0, 0),
1725  d_sharedSubterms(core->getCM()->getCurrentContext()),
1726  d_sharedSubtermsList(core->getCM()->getCurrentContext()),
1727  d_maxLength(0),
1728  d_index1(core->getCM()->getCurrentContext(), 0, 0),
1729  d_index2(core->getCM()->getCurrentContext(), 0, 0)
1730  // d_solvedEqSet(core->getCM()->getCurrentContext(), 0, 0)
1731 {
1732  getEM()->newKind(BITVECTOR, "_BITVECTOR", true);
1733  getEM()->newKind(BVCONST, "_BVCONST");
1734  getEM()->newKind(CONCAT, "_CONCAT");
1735  getEM()->newKind(EXTRACT, "_EXTRACT");
1736  getEM()->newKind(BOOLEXTRACT, "_BOOLEXTRACT");
1737  getEM()->newKind(LEFTSHIFT, "_LEFTSHIFT");
1738  getEM()->newKind(CONST_WIDTH_LEFTSHIFT, "_CONST_WIDTH_LEFTSHIFT");
1739  getEM()->newKind(RIGHTSHIFT, "_RIGHTSHIFT");
1740  getEM()->newKind(BVSHL, "_BVSHL");
1741  getEM()->newKind(BVLSHR, "_BVLSHR");
1742  getEM()->newKind(BVASHR, "_BVASHR");
1743  getEM()->newKind(SX,"_SX");
1744  getEM()->newKind(BVREPEAT,"_BVREPEAT");
1745  getEM()->newKind(BVZEROEXTEND,"_BVZEROEXTEND");
1746  getEM()->newKind(BVROTL,"_BVROTL");
1747  getEM()->newKind(BVROTR,"_BVROTR");
1748  getEM()->newKind(BVAND, "_BVAND");
1749  getEM()->newKind(BVOR, "_BVOR");
1750  getEM()->newKind(BVXOR, "_BVXOR");
1751  getEM()->newKind(BVXNOR, "_BVXNOR");
1752  getEM()->newKind(BVNEG, "_BVNEG");
1753  getEM()->newKind(BVNAND, "_BVNAND");
1754  getEM()->newKind(BVNOR, "_BVNOR");
1755  getEM()->newKind(BVCOMP, "_BVCOMP");
1756  getEM()->newKind(BVUMINUS, "_BVUMINUS");
1757  getEM()->newKind(BVPLUS, "_BVPLUS");
1758  getEM()->newKind(BVSUB, "_BVSUB");
1759  getEM()->newKind(BVMULT, "_BVMULT");
1760  getEM()->newKind(BVUDIV, "_BVUDIV");
1761  getEM()->newKind(BVSDIV, "_BVSDIV");
1762  getEM()->newKind(BVUREM, "_BVUREM");
1763  getEM()->newKind(BVSREM, "_BVSREM");
1764  getEM()->newKind(BVSMOD, "_BVSMOD");
1765  getEM()->newKind(BVLT, "_BVLT");
1766  getEM()->newKind(BVLE, "_BVLE");
1767  getEM()->newKind(BVGT, "_BVGT");
1768  getEM()->newKind(BVGE, "_BVGE");
1769  getEM()->newKind(BVSLT, "_BVSLT");
1770  getEM()->newKind(BVSLE, "_BVSLE");
1771  getEM()->newKind(BVSGT, "_BVSGT");
1772  getEM()->newKind(BVSGE, "_BVSGE");
1773  getEM()->newKind(INTTOBV, "_INTTOBV");
1774  getEM()->newKind(BVTOINT, "_BVTOINT");
1775  getEM()->newKind(BVTYPEPRED, "_BVTYPEPRED");
1776 
1777  std::vector<int> kinds;
1778  kinds.push_back(BITVECTOR);
1779  kinds.push_back(BVCONST);
1780  kinds.push_back(CONCAT);
1781  kinds.push_back(EXTRACT);
1782  kinds.push_back(BOOLEXTRACT);
1783  kinds.push_back(LEFTSHIFT);
1784  kinds.push_back(CONST_WIDTH_LEFTSHIFT);
1785  kinds.push_back(RIGHTSHIFT);
1786  kinds.push_back(BVSHL);
1787  kinds.push_back(BVLSHR);
1788  kinds.push_back(BVASHR);
1789  kinds.push_back(SX);
1790  kinds.push_back(BVREPEAT);
1791  kinds.push_back(BVZEROEXTEND);
1792  kinds.push_back(BVROTL);
1793  kinds.push_back(BVROTR);
1794  kinds.push_back(BVAND);
1795  kinds.push_back(BVOR);
1796  kinds.push_back(BVXOR);
1797  kinds.push_back(BVXNOR);
1798  kinds.push_back(BVNEG);
1799  kinds.push_back(BVNAND);
1800  kinds.push_back(BVNOR);
1801  kinds.push_back(BVCOMP);
1802  kinds.push_back(BVUMINUS);
1803  kinds.push_back(BVPLUS);
1804  kinds.push_back(BVSUB);
1805  kinds.push_back(BVMULT);
1806  kinds.push_back(BVUDIV);
1807  kinds.push_back(BVSDIV);
1808  kinds.push_back(BVUREM);
1809  kinds.push_back(BVSREM);
1810  kinds.push_back(BVSMOD);
1811  kinds.push_back(BVLT);
1812  kinds.push_back(BVLE);
1813  kinds.push_back(BVGT);
1814  kinds.push_back(BVGE);
1815  kinds.push_back(BVSLT);
1816  kinds.push_back(BVSLE);
1817  kinds.push_back(BVSGT);
1818  kinds.push_back(BVSGE);
1819  kinds.push_back(INTTOBV);
1820  kinds.push_back(BVTOINT);
1821  kinds.push_back(BVTYPEPRED);
1822 
1823  registerTheory(this, kinds);
1824 
1826 
1827  // Cache constants 0bin0 and 0bin1
1828  vector<bool> bits(1);
1829  bits[0]=false;
1830  d_bvZero = newBVConstExpr(bits);
1831  bits[0]=true;
1832  d_bvOne = newBVConstExpr(bits);
1833 
1834  // Instantiate the rules after all expression creation is
1835  // registered, since the constructor creates some bit-vector
1836  // expressions.
1838 }
1839 
1840 
1841 // Destructor: delete the proof rules class if it's present
1843  if(d_rules != NULL) delete d_rules;
1844 }
1845 
1846 
1847 // Main theory API
1848 
1849 
1851 {
1852 }
1853 
1854 
1855 /*Modified by Lorenzo PLatania*/
1856 
1857 // solvable fact (e.g. solvable equations) are added to d_eq CDList,
1858 // all the others have to be in a different CDList. If the equation is
1859 // solvable it comes here already solved. Should distinguish between
1860 // solved and not solved eqs
1862 {
1863  const Expr& expr = e.getExpr();
1864  TRACE("bvAssertFact", "TheoryBitvector::assertFact(", e.getExpr().toString(), ")");
1865  // cout<<"TheoryBitvector::assertFact, expr: "<<expr.toString()<<endl;
1866  // every time a new fact is added to the list the whole set may be
1867  // not in a solved form
1868 
1869  switch (expr.getOpKind()) {
1870 
1871  case BVTYPEPRED:
1872  assertTypePred(expr[0], e);
1873  break;
1874 
1875  case BOOLEXTRACT:
1876  // facts form the SAT solver are just ignored
1877  return;
1878 
1879  case NOT:
1880  // facts form the SAT solver are just ignored
1881  if (expr[0].getOpKind() == BOOLEXTRACT) return;
1882 
1883  if (expr[0].getOpKind() == BVTYPEPRED) {
1884  Expr tpExpr = getTypePredExpr(expr[0]);
1885  Theorem tpThm = typePred(tpExpr);
1886  DebugAssert(tpThm.getExpr() == expr[0], "Expected BVTYPEPRED theorem");
1887  setInconsistent(getCommonRules()->contradictionRule(tpThm, e));
1888  return;
1889  }
1890 
1891  DebugAssert(expr[0].isEq(), "Unexpected negation");
1892 
1893  d_bitblast.push_back(e);
1894  break;
1895 
1896  case EQ:
1897  // Updates are also ignored:
1898  // Note: this can only be true if this fact was asserted as a result of
1899  // assertEqualities. For BV theory, this should only be possible if
1900  // the update was made from our own theory, so we can ignore it.
1901  if (theoryCore()->inUpdate()) return;
1902 
1903  // If we have already started bitblasting, just store the eq in d_bitblast;
1904  // if we haven't yet bitblasted and expr is a solved linear equation then
1905  // we store it in d_eq CDList, otherwise we store it in d_eqPending
1906  if (d_bb_index != 0) {
1907  d_bitblast.push_back(e);
1908  }
1909  else if (isLeaf(expr[0]) && !isLeafIn(expr[0], expr[1])) {
1910  d_eq.push_back( e );
1911  }
1912  else {
1913  d_eqPending.push_back( e );
1914  }
1915  break;
1916 
1917  default:
1918  // if the fact is not an equation it will be bit-blasted
1919  d_bitblast.push_back( e );
1920  break;
1921  }
1922 }
1923 
1924 
1925 //TODO: can we get rid of this in exchange for a more general politeness-based sharing mechanism?
1926 void TheoryBitvector::assertTypePred(const Expr& e, const Theorem& pred) {
1927  // Ignore bitvector constants (they always satisfy type predicates)
1928  // and bitvector operators. When rewrites and updates are enabled.
1929  // their type predicates will be implicitly derived from the type
1930  // predicates of the arguments.
1931 
1932  if (theoryOf(e) == this) return;
1933  TRACE("bvAssertTypePred", "TheoryBitvector::assertTypePred(", e.toString(PRESENTATION_LANG), ")");
1934  addSharedTerm(e);
1935 }
1936 
1937 
1938 /*Beginning of Lorenzo PLatania's methods*/
1939 
1940 // evaluates the gcd of two integers using
1941 // Euclid algorithm
1942 // int TheoryBitvector::gcd(int c1, int c2)
1943 // {
1944 // if(c2==0)
1945 // return c1;
1946 // else
1947 // return gcd( c2, c1%c2);
1948 // }
1949 
1950 void TheoryBitvector::extract_vars(const Expr& e, vector<Expr>& result)
1951 {
1952  if (e.getOpKind() == BVMULT ) {
1953  extract_vars(e[0], result);
1954  extract_vars(e[1], result);
1955  }
1956  else {
1957  DebugAssert(e.getOpKind() != BVCONST &&
1958  e.getOpKind() != BVUMINUS &&
1959  e.getOpKind() != BVPLUS, "Unexpected structure");
1960  result.push_back(e);
1961  }
1962 }
1963 
1964 
1966 {
1967 
1968  // nothing to be done
1969  if( mult_inv == 1)
1970  return e;
1971  if(e.isEq())
1972  {
1973  Expr lhs = e[0];
1974  Expr rhs = e[1];
1975  Expr new_lhs = multiply_coeff( mult_inv, lhs);
1976  Expr new_rhs = multiply_coeff( mult_inv, rhs);
1977  Expr res(EQ, new_lhs, new_rhs);
1978  return res;
1979  }
1980  else
1981  {
1982  int kind = e.getOpKind();
1983  int size = BVSize(e);
1984  if( kind == BVMULT )
1985  {
1986 
1987  //lhs is like 'a_0*x_0'
1988  Rational new_coeff = mult_inv * computeBVConst( e[0] );
1989  Expr new_expr_coeff = newBVConstExpr( new_coeff, size);
1990  Expr BV_one = newBVConstExpr(1,size);
1991  if( new_expr_coeff == BV_one )
1992  {
1993  return e[1];
1994  }
1995  else
1996  {
1997  return newBVMultExpr( size, new_expr_coeff, e[1]);
1998  }
1999  }
2000  else
2001  if( kind == BVPLUS)
2002  {
2003 
2004  int expr_arity= e.arity();
2005  std::vector<Expr> tmp_list;
2006  for( int i = 0; i < expr_arity; ++i)
2007  {
2008  tmp_list.push_back(multiply_coeff( mult_inv, e[i]));
2009  }
2010 // Expr::iterator i = e.begin();
2011 // int index;
2012 // Expr::iterator end = e.end();
2013 // std::vector<Expr> tmp_list;
2014 // for( i = e.begin(), index=0; i!=end; ++i, ++index)
2015 // {
2016 // tmp_list.push_back(multiply_coeff( mult_inv, *i));
2017 // }
2018  return newBVPlusExpr(size, tmp_list);
2019  }
2020  else
2021  if( kind == BVCONST )
2022  {
2023 
2024  Rational new_const = mult_inv * computeBVConst(e);
2025  Expr res = newBVConstExpr( new_const, size);
2026  // cout<<res.toString()+"\n";
2027  return res;
2028  }
2029  else
2030  if( isLeaf( e ) )
2031  {
2032  //lhs is like 'x_0'
2033  // need to know the lenght of the var
2034  // L:: guess it is not correct, mult_inv * e
2035  Expr BV_mult_inv = newBVConstExpr( mult_inv, size);
2036  Expr new_var = newBVMultExpr( size, BV_mult_inv, e);
2037 
2038  return new_var;
2039  }
2040  else
2041  {
2042  return e;
2043  }
2044  }
2045 }
2046 
2047 // L::return the index of the minimum element returns -1 if the list
2048 // is empty assuming only non-negative elements to be sostituted with
2049 // some debug assertion. ***I guess n_bits can be just an integer, no
2050 // need to declare it as a Rational
2051 
2053 {
2054 
2055  // cout<<"TheoryBitvector::multiplicative_inverse: working on "<<r.toString()<<endl;
2056  Rational i=r;
2057  Rational max_val= pow( n_bits, (Rational) 2);
2058  while(r!=1)
2059  {
2060  r = ( r*r ) % max_val;
2061  i = ( i*r ) % max_val;
2062  }
2063  // cout<<"TheoryBitvector::multiplicative_inverse: result is "<<i.toString()<<endl;
2064  return i;
2065 }
2066 
2067 // int TheoryBitvector::min(std::vector<Rational> list)
2068 // {
2069 // int res = 0;
2070 // int i;
2071 // int size = list.size();
2072 // for(i = 0; i < size; ++i)
2073 // {
2074 // cout<<"list["<<i<<"]: "<<list[i]<<endl;
2075 // }
2076 // for(i = 1; i < size; ++i)
2077 // {
2078 // if(list[res]>list[i])
2079 // res=i;
2080 // cout<<"res: "<<res<<endl;
2081 // cout<<"min: "<<list[res]<<endl;
2082 // }
2083 
2084 // cout<<"min: "<<res<<endl;
2085 // return res;
2086 // }
2087 
2088 //***************************
2089 // ecco come fare il delete!
2090 //***************************
2091 
2092 // int main ()
2093 // {
2094 // unsigned int i;
2095 // deque<unsigned int> mydeque;
2096 
2097 // // set some values (from 1 to 10)
2098 // for (i=1; i<=10; i++) mydeque.push_back(i);
2099 
2100 // // erase the 6th element
2101 // mydeque.erase (mydeque.begin()+5);
2102 
2103 // // erase the first 3 elements:
2104 // mydeque.erase (mydeque.begin(),mydeque.begin()+3);
2105 
2106 // cout << "mydeque contains:";
2107 // for (i=0; i<mydeque.size(); i++)
2108 // cout << " " << mydeque[i];
2109 // cout << endl;
2110 
2111 // return 0;
2112 // }
2113 
2114 // use the method in rational.h
2115 // it uses std::vector<Rational> instead of std::deque<int>
2116 // int TheoryBitvector::gcd(std::deque<int> coeff_list)
2117 // {
2118 
2119 // cout<<"TheoryBitvector::gcd: begin\n";
2120 // for(unsigned int i=0; i<coeff_list.size(); ++i)
2121 // {
2122 // cout<<"coeff_list["<<i<<"]: "<<coeff_list[i]<<endl;
2123 // }
2124 // int gcd_list;
2125 // int min_index = min(coeff_list);
2126 // int min_coeff_1 = coeff_list[min_index];
2127 // cout<<"erasing element: "<<coeff_list[min_index];
2128 // coeff_list.erase( coeff_list.begin() + min_index );
2129 
2130 // while(coeff_list.size()>0)
2131 // {
2132 // min_index = min(coeff_list);
2133 // int min_coeff_2 = coeff_list[min_index];
2134 // cout<<"erasing element: "<<coeff_list[min_index];
2135 // coeff_list.erase( coeff_list.begin() + min_index );
2136 
2137 // // save one recursion
2138 // gcd_list = gcd( min_coeff_2, min_coeff_1);
2139 // cout<<"TheoryBitvector::gcd: erased min1\n";
2140 // min_coeff_1 = gcd_list;
2141 // }
2142 // cout<<"gcd_list: "<<gcd_list<<endl;
2143 // return gcd_list;
2144 // }
2145 
2146 // int TheoryBitvector::bv2int(const Expr& e)
2147 // {
2148 // int sum=0;
2149 // if(e.arity()==0 && ! e.isVar())
2150 // {
2151 // std::string tmp = e.toString();
2152 // int s_length = tmp.length();
2153 // int bit;
2154 // int exp;
2155 // // first 4 cells contains the bv prefix 0bin
2156 // // just discard them
2157 // for(int i=3; i < s_length; ++i)
2158 // {
2159 // if(tmp[i]=='1')
2160 // {
2161 // sum += (int)std::pow((float) 2, s_length - 1 - i);
2162 // }
2163 // }
2164 // }
2165 // else
2166 // {
2167 // cerr<<"error: non-constant to be converted\n";
2168 // }
2169 // return sum;
2170 // }
2171 
2172 // returning the position of the first odd coefficient found;
2173 // moreover, it multiplies a variable which does not appear in other
2174 // subterms. It assumes that the input expression has already been
2175 // canonized, so the lhs is a flat BVPLUS expression and the rhs is a
2176 // zero BVCONST
2177 
2179 {
2180  int bv_size = BVSize(e[0]);
2181  Expr bv_zero( newBVZeroString(bv_size));
2182 
2183  DebugAssert(e.getOpKind()==EQ && e[1] == bv_zero,
2184  "TheoryBitvector::Odd_coeff: the input expression has a non valid form ");
2185 
2186  Expr lhs = e[0];
2187  if( lhs.getOpKind() == BVMULT )
2188  {
2189  if( lhs[0].getOpKind() == BVCONST && computeBVConst( lhs[0]) % 2 != 0)
2190  return computeBVConst( lhs[0] );
2191  }
2192  else
2193  if( isLeaf( lhs))
2194  return 1;
2195  else
2196  if( lhs.getOpKind() == BVPLUS )
2197  {
2198  int lhs_arity = lhs.arity();
2199  // scanning lhs in order to find a good odd coefficient
2200  for( int i = 0; i < lhs_arity; ++i)
2201  {
2202  // checking that the subterm is a leaf
2203  if( isLeaf( lhs[i] ) )
2204  {
2205  // checking that the current subterm does not appear in other
2206  // subterms
2207  for( int j = 0; j < lhs_arity; ++j)
2208  if( j != i && !isLeafIn( lhs[i], lhs[j] ))
2209  return 1;
2210  }
2211  else
2212  if( lhs[i].getOpKind() == BVMULT)
2213  {
2214  // the subterm is a BVMULT with a odd coefficient
2215  if( lhs[i][0].getOpKind() == BVCONST && computeBVConst( lhs[i][0]) % 2 != 0)
2216  {
2217  // checking that the current subterm does not appear in other
2218  // subterms
2219  int flag = 0;
2220  for( int j = 0; j < lhs_arity; ++j)
2221  {
2222  // as we can solve also for non-leaf terms we use
2223  // isTermIn instead of isLeafIn
2224  if( j != i && isTermIn( lhs[i][1], lhs[j] ))
2225  flag = 1;
2226  }
2227  // if the leaf is not a subterm of other terms in the
2228  // current expression then we can solve for it
2229  if( flag == 0)
2230  return computeBVConst( lhs[i][0] );
2231  }
2232  }
2233  else
2234  // the subterm is a non-linear one
2235  if ( lhs[i].getOpKind() != BVCONST )
2236  {
2237  // checking that the current subterm does not appear in other
2238  // subterms
2239  for( int j = 0; j < lhs_arity; ++j)
2240  if( j != i && !isLeafIn( lhs[i][1], lhs[j] ))
2241  return 1;
2242  }
2243  else
2244  ;
2245  }
2246  }
2247  // no leaf found to solve for
2248  return 0;
2249 }
2250 
2252 {
2253  TRACE("bv_check_linear", "TheoryBitvector::check_linear(", e.toString(PRESENTATION_LANG), ")");
2254  // recursively check if the expression is linear
2255  if( e.isVar() || e.getOpKind() == BVCONST )
2256  return 1;
2257  else
2258  if( e.getOpKind() == BVPLUS )
2259  {
2260  int e_arity= e.arity();
2261  int flag = 1;
2262  for( int i=0; i < e_arity && flag == 1; ++i)
2263  {
2264  flag = check_linear( e[i]);
2265  }
2266  return flag;
2267  }
2268  else
2269  if( e.getOpKind() == BVMULT)
2270  {
2271  if( e[0].getOpKind() == BVCONST && e[1].isVar() )
2272  return 1;
2273  else
2274  return 0;
2275  }
2276  else
2277  if( e.getOpKind() == BVUMINUS)
2278  return check_linear( e[0]);
2279  else
2280  if( e.getOpKind() == EQ )
2281  return ( check_linear( e[0] ) && check_linear( e[1] ));
2282  else
2283  // all other operators are non-linear
2284  return 0;
2285 }
2286 
2287 // please check it is right. It is the same as Theory::isLeafIn but it
2288 // does not require e1 to be a leaf. In this way we can check for e1
2289 // to be a subterm of other expressions even if it is not a leaf,
2290 // i.e. a non-linear term
2291 bool TheoryBitvector::isTermIn(const Expr& e1, const Expr& e2)
2292 {
2293  if (e1 == e2) return true;
2294  if (theoryOf(e2) != this) return false;
2295  for(Expr::iterator i=e2.begin(), iend=e2.end(); i != iend; ++i)
2296  if (isTermIn(e1, *i)) return true;
2297  return false;
2298 }
2299 
2300 // checks whether e can be solved in term
2301 bool TheoryBitvector::canSolveFor( const Expr& term, const Expr& e )
2302 {
2303  DebugAssert( e.getOpKind() == EQ, "TheoryBitvector::canSolveFor, input 'e' must be an equation");
2304 
2305  // cout<<"TheoryBitvector::canSolveFor, term: "<<term.toString()<<endl;
2306  // the term has not a unary coefficient, so we did not multiply the
2307  // equation by its multiplicative inverse
2308  if( term.getOpKind() == BVMULT && term[0].getOpKind() == BVCONST)
2309  return 0;
2310  else
2311  if( isLeaf( term ) || !isLinearTerm( term))
2312  {
2313  int count = countTermIn( term, e);
2314  // cout<<"TheoryBitvector::canSolveFor, count for "<<term.toString()<<" is: "<<count<<endl;
2315  if( count == 1)
2316  return true;
2317  else
2318  return false;
2319  }
2320  else
2321  {
2322  DebugAssert( false, "TheoryBitvector::canSolveFor, input 'term' of not treated kind");
2323  return false;
2324  }
2325 }
2326 
2327 int TheoryBitvector::countTermIn( const Expr& term, const Expr& e)
2328 {
2329  // cout<<"TheoryBitvector::countTermIn, term: "<<term.toString()<<" e: "<<e.toString()<<endl;
2330  int e_arity = e.arity();
2331  int result = 0;
2332  // base cases recursion happen when e is a constant or a leaf
2333  if( e.getOpKind() == BVCONST )
2334  return 0;
2335  if( term == e )
2336  return 1;
2337 
2338  for( int i = 0; i < e_arity; ++i)
2339  {
2340  result += countTermIn( term, e[i]);
2341  }
2342  return result;
2343 }
2344 
2346 {
2347  if( isLeaf( e ) )
2348  return true;
2349  switch( e.getOpKind())
2350  {
2351  case BVPLUS:
2352  return true;
2353  case BVMULT:
2354  if( e[0].getOpKind() == BVCONST && isLinearTerm( e[1] ))
2355  return true;
2356  else
2357  return false;
2358  break;
2359  default:
2360  return false;
2361  }
2362 }
2363 
2364 
2365 // returns thm if no change
2367 {
2368  Expr e = thm.getExpr();
2369  DebugAssert(e.getKind() == EQ, "Expected EQ");
2370  Expr lhs = e[0];
2371  Expr rhs = e[1];
2372 
2373  Theorem thm2 = thm;
2374  if (!isLeaf(lhs)) {
2375  // Carefully simplify lhs:
2376  // We can't take find(lhs) because find(lhs) = find(rhs) and this would result in a trivially true equation.
2377  // So, take the find of the children instead.
2378  int ar = lhs.arity();
2379  vector<Theorem> newChildrenThm;
2380  vector<unsigned> changed;
2381  Theorem thm0;
2382  for (int k = 0; k < ar; ++k) {
2383  thm0 = find(lhs[k]);
2384  if (thm0.getLHS() != thm0.getRHS()) {
2385  newChildrenThm.push_back(thm0);
2386  changed.push_back(k);
2387  }
2388  }
2389  if(changed.size() > 0) {
2390  // lhs = updated_lhs
2391  thm0 = substitutivityRule(lhs, changed, newChildrenThm);
2392  // lhs = updated_and_rewritten_lhs
2393  thm0 = transitivityRule(thm0, rewrite(thm0.getRHS()));
2394  // updated_and_rewritten_lhs = rhs
2395  thm2 = transitivityRule(symmetryRule(thm0), thm);
2396  }
2397  }
2398  // updated_and_rewritten_lhs = find(rhs)
2399  thm2 = transitivityRule(thm2, find(rhs));
2400  // canonized EQ
2401  thm2 = iffMP(thm2, d_rules->canonBVEQ(thm2.getExpr(), maxEffort));
2402  if (thm2.isRewrite() && thm2.getRHS() == lhs && thm2.getLHS() == rhs) {
2403  thm2 = thm;
2404  }
2405  return thm2;
2406 }
2407 
2408 
2410 {
2411  // cout<<"TheoryBitvector::generalBitBlast, thm: "<<thm.toString()<<" to expr(): "<<thm.getExpr().toString()<<endl;
2412  Expr e = thm.getExpr();
2413  switch (e.getOpKind()) {
2414  case EQ: {
2415  Theorem thm2 = simplifyPendingEq(thm, 6);
2416  const Expr& e2 = thm2.getExpr();
2417  switch (e2.getKind()) {
2418  case TRUE_EXPR:
2419  case FALSE_EXPR:
2420  return thm2;
2421  case EQ:
2422  return iffMP(thm2, bitBlastEqn(thm2.getExpr()));
2423  case AND: {
2424  DebugAssert(e2.arity() == 2 && e2[0].getKind() == EQ && e2[1].getKind() == EQ,
2425  "Expected two equations");
2426  Theorem t1 = bitBlastEqn(e2[0]);
2427  Theorem t2 = bitBlastEqn(e2[1]);
2428  Theorem thm3 = substitutivityRule(e2, t1, t2);
2429  return iffMP(thm2, thm3);
2430  }
2431  default:
2432  FatalAssert(false, "Unexpected Expr");
2433  break;
2434  }
2435  break;
2436  }
2437  case BVLT:
2438  case BVLE: {
2439  // Carefully simplify
2440  int ar = e.arity();
2441  DebugAssert(ar == 2, "Expected arity 2");
2442  vector<Theorem> newChildrenThm;
2443  vector<unsigned> changed;
2444  Theorem thm0;
2445  for (int k = 0; k < ar; ++k) {
2446  thm0 = find(e[k]);
2447  if (thm0.getLHS() != thm0.getRHS()) {
2448  newChildrenThm.push_back(thm0);
2449  changed.push_back(k);
2450  }
2451  }
2452  if(changed.size() > 0) {
2453  // updated_e
2454  thm0 = iffMP(thm, substitutivityRule(e, changed, newChildrenThm));
2455  // updated_and_rewritten_e
2456  thm0 = iffMP(thm0, rewrite(thm0.getExpr()));
2457  if (thm0.getExpr().getOpKind() != e.getOpKind()) return thm0;
2458  return iffMP(thm0, bitBlastIneqn(thm0.getExpr()));
2459  }
2460  return iffMP(thm, bitBlastIneqn(e));
2461  }
2462  // a NOT should mean a disequality, as negation of inequalities
2463  // can be expressed as other inequalities.
2464  case NOT: {
2465  // Carefully simplify
2466  DebugAssert(e.arity() == 1, "Expected arity 1");
2467  DebugAssert(e[0].isEq(), "Expected disequality");
2468  DebugAssert(e[0].arity() == 2, "Expected arity 2");
2469  vector<Theorem> newChildrenThm;
2470  vector<unsigned> changed;
2471  Theorem thm0;
2472  for (int k = 0; k < 2; ++k) {
2473  thm0 = find(e[0][k]);
2474  if (thm0.getLHS() != thm0.getRHS()) {
2475  newChildrenThm.push_back(thm0);
2476  changed.push_back(k);
2477  }
2478  }
2479  if(changed.size() > 0) {
2480  // a = b <=> a' = b'
2481  thm0 = substitutivityRule(e[0], changed, newChildrenThm);
2482  }
2483  else thm0 = reflexivityRule(e[0]);
2484  // a = b <=> canonized EQ
2485  thm0 = transitivityRule(thm0, d_rules->canonBVEQ(thm0.getRHS(), 6));
2486  // NOT(canonized EQ)
2487  thm0 = iffMP(thm, substitutivityRule(e, thm0));
2488  if (thm0.getExpr()[0].isEq()) {
2489  return bitBlastDisEqn(thm0);
2490  }
2491  else return thm0;
2492  }
2493  default:
2494  FatalAssert(false, "TheoryBitvector::generalBitBlast: unknown expression kind");
2495  break;
2496  }
2497  return reflexivityRule( e );
2498 }
2499 /*End of Lorenzo PLatania's methods*/
2500 
2501 static Expr findAtom(const Expr& e)
2502 {
2503  if (e.isAbsAtomicFormula()) return e;
2504  for (int i = 0; i < e.arity(); ++i) {
2505  Expr e_i = findAtom(e[i]);
2506  if (!e_i.isNull()) return e_i;
2507  }
2508  return Expr();
2509 }
2510 
2511 
2512 bool TheoryBitvector::comparebv(const Expr& e1, const Expr& e2)
2513 {
2514  int size = BVSize(e1);
2515  FatalAssert(size == BVSize(e2), "expected same size");
2516  Theorem c1, c2;
2517  int idx1 = -1;
2518  vector<Theorem> thms1;
2519 
2520  if (d_bb_index == 0) {
2521  Expr splitter = e1.eqExpr(e2);
2522  Theorem thm = simplify(splitter);
2523  if (!thm.getRHS().isBoolConst()) {
2524  addSplitter(e1.eqExpr(e2));
2525  return true;
2526  }
2527  // Store a dummy theorem to indicate bitblasting has begun
2528  d_bb_index = 1;
2529  d_bitblast.push_back(getCommonRules()->trueTheorem());
2530  }
2531 
2532  for (int i = 0; i < size; ++i) {
2533  c1 = bitBlastTerm(e1, i);
2534  c1 = transitivityRule(c1, simplify(c1.getRHS()));
2535  c2 = bitBlastTerm(e2, i);
2536  c2 = transitivityRule(c2, simplify(c2.getRHS()));
2537  thms1.push_back(c1);
2538  if (!c1.getRHS().isBoolConst()) {
2539  if (idx1 == -1) idx1 = i;
2540  continue;
2541  }
2542  if (!c2.getRHS().isBoolConst()) {
2543  continue;
2544  }
2545  if (c1.getRHS() != c2.getRHS()) return false;
2546  }
2547  if (idx1 == -1) {
2548  // If e1 is known to be a constant, assert that
2549  DebugAssert(e1.getKind() != BVCONST, "Expected non-const");
2551  addSplitter(e1.eqExpr(e2));
2552  // enqueueFact(getCommonRules()->trueTheorem());
2553  return true;
2554  }
2555 
2556  Theorem thm = bitBlastEqn(e1.eqExpr(e2));
2557  thm = iffMP(thm, simplify(thm.getExpr()));
2558  if (!thm.getExpr().isTrue()) {
2559  enqueueFact(thm);
2560  return true;
2561  }
2562 
2563  // Nothing to assert from bitblasted equation. Best way to resolve this
2564  // problem is to split until the term can be equated with a bitvector
2565  // constant.
2566  Expr e = findAtom(thms1[idx1].getRHS());
2567  DebugAssert(!e.isNull(), "Expected atom");
2568  addSplitter(e);
2569  return true;
2570 }
2571 
2572 static bool bvdump = false;
2573 
2574 void TheoryBitvector::checkSat(bool fullEffort)
2575 {
2576  if(fullEffort) {
2577 
2578  for (unsigned i = 0; i < additionalRewriteConstraints.size(); i ++)
2581 
2582  if (bvdump) {
2583  CDList<Theorem>::const_iterator it_list=d_eq.begin();
2584  unsigned int i;
2585  for(i=0; i<d_eq.size(); ++i)
2586  {
2587  cout<<"d_eq [" << i << "]= "<< it_list[i].getExpr().toString() << endl;
2588  }
2589 
2590  it_list=d_eqPending.begin();
2591 
2592  for(i=0; i<d_eqPending.size(); ++i)
2593  {
2594  cout<<"d_eqPending [" << i << "]= "<< it_list[i].getExpr().toString() << endl;
2595  }
2596 
2597  it_list=d_bitblast.begin();
2598 
2599  for(i=0; i<d_bitblast.size(); ++i)
2600  {
2601  cout<<"d_bitblast [" << i << "]= "<< it_list[i].getExpr().toString() << endl;
2602  }
2603 
2604  if (d_eq.size() || d_eqPending.size() || d_bitblast.size()) cout << endl;
2605  }
2606 
2607  unsigned eq_list_size = d_eqPending.size();
2608  bool bitBlastEq = d_eq_index < eq_list_size;
2609  if (d_bb_index == 0 && bitBlastEq) {
2610  bitBlastEq = false;
2611  unsigned eqIdx = d_eq_index;
2612  for(; eqIdx < eq_list_size; ++eqIdx) {
2613  Expr eq = d_eqPending[eqIdx].getExpr();
2614  DebugAssert(eq[1] == newBVConstExpr(Rational(0), BVSize(eq[0])), "Expected 0 on rhs");
2615  Theorem thm = simplifyPendingEq(d_eqPending[eqIdx], 5);
2616  if (thm == d_eqPending[eqIdx]) {
2617  bitBlastEq = true;
2618  continue;
2619  }
2620  const Expr& e2 = thm.getExpr();
2621  switch (e2.getKind()) {
2622  case TRUE_EXPR:
2623  break;
2624  case FALSE_EXPR:
2625  enqueueFact(thm);
2626  return;
2627  case EQ:
2628  case AND:
2629  if (simplify(thm.getExpr()).getRHS() == trueExpr()) {
2630  bitBlastEq = true;
2631  break;
2632  }
2633  for (; d_eq_index < eqIdx; d_eq_index = d_eq_index + 1) {
2634  d_eqPending.push_back(d_eqPending[d_eq_index]);
2635  }
2636  d_eq_index = d_eq_index + 1;
2637  enqueueFact(thm);
2638  return;
2639  default:
2640  FatalAssert(false, "Unexpected expr");
2641  break;
2642  }
2643  }
2644  }
2645 
2646  // Bitblast any new formulas
2647  unsigned bb_list_size = d_bitblast.size();
2648  bool bbflag = d_bb_index < bb_list_size || bitBlastEq;
2649  if (bbflag) {
2650  for( ; d_bb_index < bb_list_size; d_bb_index = d_bb_index + 1) {
2651  Theorem bb_result = generalBitBlast( d_bitblast[ d_bb_index ]);
2652  enqueueFact( bb_result);
2653  }
2654  if (d_bb_index == 0) {
2655  // push dummy on the stack to indicate bitblasting has started
2656  d_bb_index = 1;
2657  d_bitblast.push_back(getCommonRules()->trueTheorem());
2658  }
2659  for( ; d_eq_index < eq_list_size; d_eq_index = d_eq_index + 1) {
2660  Theorem bb_result = generalBitBlast( d_eqPending[ d_eq_index ]);
2661  enqueueFact( bb_result);
2662  }
2663  // If newly bitblasted formulas, skip the shared term check
2664  return;
2665  }
2666  }
2667 }
2668 
2669 
2671 {
2672  ExprMap<Theorem> cache;
2673  return rewriteBV(e, cache);
2674 }
2675 
2676 
2678 {
2679  return reflexivityRule(e);
2680 }
2681 
2682 
2684 {
2685  int k(0), ar(e.arity());
2686  if( e.isTerm() ) {
2687  for ( ; k < ar; ++k) {
2688  e[k].addToNotify(this, e);
2689  }
2690  }
2691 }
2692 
2693 
2694 // Lorenzo's version
2695 void TheoryBitvector::update(const Theorem& e, const Expr& d) {
2696 
2697  if (inconsistent()) return;
2698  // cout<<"TheoryBitvector::update, theorem e:"<<e.toString()<<" expression d: "<<d.toString()<<endl;
2699  // Updating shared terms informations, code inherited from the old
2700  // version of the bitvector theory
2701 
2702  // Constants should never change their find pointers to non-constant
2703  // expressions
2705  "TheoryBitvector::update(e="+e.getExpr().toString()
2706  +", d="+d.toString());
2707  if (d.isNull()) {
2708  Expr lhs = e.getLHS();
2709  Expr rhs = e.getRHS();
2710  DebugAssert(d_sharedSubterms.find(lhs) != d_sharedSubterms.end(),
2711  "Expected lhs to be shared");
2713  if (it == d_sharedSubterms.end()) {
2714  addSharedTerm(rhs);
2715  }
2716  return;
2717  }
2718 // {
2719 // // found an equality between shared subterms!
2720 // bool changed = false;
2721 // if ((*it).second != lhs) {
2722 // lhs = (*it).second;
2723 // it = d_sharedSubterms.find(lhs);
2724 // DebugAssert(it != d_sharedSubterms.end() && (*it).second == lhs,
2725 // "Invariant violated in TheoryBitvector::update");
2726 // changed = true;
2727 // }
2728 // if ((*it2).second != rhs) {
2729 // rhs = (*it2).second;
2730 // it2 = d_sharedSubterms.find(rhs);
2731 // DebugAssert(it2 != d_sharedSubterms.end() && (*it2).second == rhs,
2732 // "Invariant violated in TheoryBitvector::update");
2733 // changed = true;
2734 // }
2735 // DebugAssert(findExpr(lhs) == e.getRHS() &&
2736 // findExpr(rhs) == e.getRHS(), "Unexpected value for finds");
2737 // // It may be needed to check whether the two terms are the
2738 // // same, in that case don't do anything
2739 // if (changed) {
2740 // Theorem thm = transitivityRule(find(lhs),symmetryRule(find(rhs)));
2741 // const Expr& expr = thm.getExpr();
2742 
2743 // if (d_bb_index == 0 &&
2744 // isLeaf(expr[0]) && !isLeafIn(expr[0], expr[1])) {
2745 // d_eq.push_back( thm );
2746 // }
2747 // else {
2748 // d_bitblast.push_back( thm );
2749 // }
2750 // }
2751 
2752 
2753 // // canonize and solve befor asserting it
2754 // // cout<<"TheoryBitvector::update, thm.getRHS(): "<<thm.getRHS()<<" thm.getLHS():"<<thm.getLHS()<<" thm.getExpr():"<<thm.getExpr()<<endl;
2755 // Theorem rwt_thm = rewrite( thm.getExpr() );
2756 // Theorem solved_thm = solve( rwt_thm);
2757 // assertFact( solved_thm );
2758  // assertFact( thm );
2759  // enqueueFact(iffMP(thm, bitBlastEqn(thm.getExpr())));
2760 // }
2761 // else
2762 // {
2763 // d_sharedSubterms[rhs] = (*it).second;
2764 // }
2765 // }
2766  // Propagate the "find" information to all the terms in the notify
2767  // list of d
2768 
2769  // if d has no find there is nothing to be updated
2770  if (!d.hasFind()) return;
2771 
2772  if (find(d).getRHS() == d) {
2773 // Theorem thm = updateSubterms(d);
2774 // TRACE("bvupdate", "TheoryArithOld::update(): thm = ", thm, "");
2775 // DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
2776 // +thm.getExpr().toString());
2777  Theorem thm = simplify(d);
2778  if (thm.getRHS().isAtomic()) {
2779  assertEqualities(thm);
2780  }
2781  else {
2782  // Simplify could introduce case splits in the expression. Handle this by renaminig
2783  Theorem renameTheorem = renameExpr(d);
2784  enqueueFact(transitivityRule(symmetryRule(renameTheorem), thm));
2785  assertEqualities(renameTheorem);
2786  }
2787  }
2788 }
2789 
2790 
2792 {
2793  // DebugAssert(canonRec(e).getRHS() == e, "canonSimp expects input to be canonized");
2794  int ar = e.arity();
2795  if (isLeaf(e)) return find(e);
2796  if (ar > 0) {
2797  vector<Theorem> newChildrenThm;
2798  vector<unsigned> changed;
2799  Theorem thm;
2800  for (int k = 0; k < ar; ++k) {
2801  thm = updateSubterms(e[k]);
2802  if (thm.getLHS() != thm.getRHS()) {
2803  newChildrenThm.push_back(thm);
2804  changed.push_back(k);
2805  }
2806  }
2807  if(changed.size() > 0) {
2808  thm = substitutivityRule(e, changed, newChildrenThm);
2809  thm = transitivityRule(thm, rewrite(thm.getRHS()));
2810  return transitivityRule(thm, find(thm.getRHS()));
2811  }
2812  else return find(e);
2813  }
2814  return find(e);
2815 }
2816 
2817 
2819 {
2820  DebugAssert(t.isRewrite() && t.getLHS().isTerm(), "");
2821  Expr e = t.getExpr();
2822 
2823  if (isLeaf(e[0]) && !isLeafIn(e[0], e[1])) {
2824  // already solved
2825  return t;
2826  }
2827  else if (isLeaf(e[1]) && !isLeafIn(e[1], e[0])) {
2828  return symmetryRule(t);
2829  }
2830  else if (e[0].getOpKind() == EXTRACT && isLeaf(e[0][0])) {
2831  bool solvedForm;
2832  Theorem thm;
2834  {
2835  thm = iffMP(t, d_rules->solveExtractOverlap(e));
2836  solvedForm = true;
2837  }
2838  else
2839  thm = d_rules->processExtract(t, solvedForm);
2840 
2841  thm = getCommonRules()->skolemize(thm);
2842 
2843  if (solvedForm) return thm;
2844  else {
2845  enqueueFact(getCommonRules()->andElim(thm, 1));
2846  return getCommonRules()->andElim(thm, 0);
2847  }
2848  }
2849  else if (e[1].getOpKind() == EXTRACT && isLeaf(e[1][0])) {
2850  bool solvedForm;
2852  if (solvedForm) return thm;
2853  else {
2854  enqueueFact(getCommonRules()->andElim(thm, 1));
2855  return getCommonRules()->andElim(thm, 0);
2856  }
2857  }
2858 
2859  IF_DEBUG(
2860  Theorem t2 = iffMP(t, d_rules->canonBVEQ(e));
2861  if (e[0] < e[1]) {
2862  DebugAssert(e[1].getOpKind() == BVCONST,
2863  "Should be only case when lhs < rhs");
2864  t2 = symmetryRule(t2);
2865  }
2866  DebugAssert(t2.getExpr() == e, "Expected no change");
2867  )
2868 
2869  if (e[0].getOpKind() == BVCONST) {
2870  DebugAssert(e[1].getOpKind() != BVCONST, "should not have const = const");
2871  return symmetryRule(t);
2872  }
2873  return t;
2874 }
2875 
2876 // // solving just linear equations; for everything else I just return
2877 // // the same expression
2878 // if( ! e.isEq())
2879 // {
2880 // return reflexivityRule( e );
2881 // }
2882 // //the search for the odd coefficient should also check that the
2883 // //multiplied term does not appear in other terms. The coefficient can
2884 // //also multiply a non-linear term
2885 
2886 
2887 // // L:: look for a odd coefficient, if one, then the eq is solvable
2888 // // and we can find the mult-inverse using Barrett-Dill-Levitt
2889 // Expr lhs = e[0];
2890 // Expr::iterator it = lhs.begin(), iend = lhs.end();
2891 // for (; it != iend; ++it) {
2892 // switch ((*it).getOpKind()) {
2893 // case BVCONST: continue;
2894 // case BVMULT: {
2895 // DebugAssert((*it).arity() == 2 &&
2896 // (*it)[0].getOpKind() == BVCONST &&
2897 // computeBVConst((*it)[0]) != 1, "Unexpected format");
2898 // continue
2899 // }
2900 
2901 // coefficient = Odd_coeff( e );
2902 // // Rational odd_coeff = anyOdd( coeff );
2903 // if( coefficient != 0)
2904 // {
2905 // // the equation is solvable
2906 // cout<<"Odd coefficient found => the equation is solvable\n";
2907 // if (coefficient != 1) {
2908 // Rational mult_inv = multiplicative_inverse( coefficient, BVSize(e[0]));
2909 // // multiply all the coefficients in the expression by the inverse
2910 // // Expr tmp_expr = e;
2911 // e = multiply_coeff( mult_inv, e);
2912 // // Expr isolated_expr = isolate_var( new_expr);
2913 // }
2914 
2915 // Theorem solved_th = d_rules->isolate_var( t, e);
2916 // cout<<"solved theorem: "<<solved_th.toString()<<endl;
2917 // cout<<"solved theorem expr: "<<solved_th.getExpr().toString()<<endl;
2918 
2919 // return iffMP( t, solved_th);
2920 // }
2921 // else
2922 // {
2923 // cout<<"Odd coefficient not found => the equation is not solvable\n";
2924 // Theorem thm = d_rules->MarkNonSolvableEq( e );
2925 // cout<<"TheoryBitvector::solve, input e: "<<e.toString()<<" thm: "<<thm.toString()<<endl;
2926 // return iffMP( t, thm);
2927 // //return reflexivityRule(e);
2928 // }
2929 //}
2930 
2931 
2933 {
2934  switch (e.getOpKind()) {
2935  case BITVECTOR:
2936  //TODO: check that this is a well-formed type
2937  break;
2938  default:
2939  FatalAssert(false, "Unexpected kind in TheoryBitvector::checkType"
2940  +getEM()->getKindName(e.getOpKind()));
2941  }
2942 }
2943 
2944 
2946  bool enumerate, bool computeSize)
2947 {
2948  FatalAssert(e.getKind() == BITVECTOR,
2949  "Unexpected kind in TheoryBitvector::finiteTypeInfo");
2950  if (enumerate || computeSize) {
2951  int bitwidth = getBitvectorTypeParam(e);
2952  Rational max_val = pow( bitwidth, (Rational) 2);
2953 
2954  if (enumerate) {
2955  if (n < max_val.getUnsigned()) {
2956  e = newBVConstExpr(n, bitwidth);
2957  }
2958  else e = Expr();
2959  }
2960 
2961  if (computeSize) {
2962  n = max_val.getUnsignedMP();
2963  }
2964  }
2965  return CARD_FINITE;
2966 }
2967 
2968 
2970 {
2971  if (e.isApply()) {
2972  switch(e.getOpKind()) {
2973  case BOOLEXTRACT: {
2974  if(!(1 == e.arity() &&
2975  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
2976  throw TypecheckException("Type Checking error:"\
2977  "attempted extraction from non-bitvector \n"+
2978  e.toString());
2979  int extractLength = getBoolExtractIndex(e);
2980  if(!(0 <= extractLength))
2981  throw TypecheckException("Type Checking error: \n"
2982  "attempted out of range extraction \n"+
2983  e.toString());
2984  e.setType(boolType());
2985  break;
2986  }
2987  case BVMULT:{
2988  if(!(2 == e.arity() &&
2989  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind() &&
2990  BITVECTOR == getBaseType(e[1]).getExpr().getOpKind()))
2991  throw TypecheckException
2992  ("Not a bit-vector expression in BVMULT:\n\n "
2993  +e.toString());
2994  int bvLen = getBVMultParam(e);
2995  Type bvType = newBitvectorType(bvLen);
2996  e.setType(bvType);
2997  break;
2998  }
2999  case EXTRACT:{
3000  if(!(1 == e.arity() &&
3001  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
3002  throw TypecheckException
3003  ("Not a bit-vector expression in bit-vector extraction:\n\n "
3004  + e.toString());
3005  int bvLength = BVSize(e[0]);
3006  int leftExtract = getExtractHi(e);
3007  int rightExtract = getExtractLow(e);
3008  if(!(0 <= rightExtract &&
3009  rightExtract <= leftExtract && leftExtract < bvLength))
3010  throw TypecheckException
3011  ("Wrong bounds in bit-vector extract:\n\n "+e.toString());
3012  int extractLength = leftExtract - rightExtract + 1;
3013  Type bvType = newBitvectorType(extractLength);
3014  e.setType(bvType);
3015  break;
3016  }
3017  case BVPLUS: {
3018  int bvPlusLength = getBVPlusParam(e);
3019  if(!(0 <= bvPlusLength))
3020  throw TypecheckException
3021  ("Bad bit-vector length specified in BVPLUS expression:\n\n "
3022  + e.toString());
3023  for(Expr::iterator i=e.begin(), iend=e.end(); i != iend; ++i) {
3024  if(BITVECTOR != getBaseType(*i).getExpr().getOpKind())
3025  throw TypecheckException
3026  ("Not a bit-vector expression in BVPLUS:\n\n "+e.toString());
3027  }
3028  Type bvType = newBitvectorType(bvPlusLength);
3029  e.setType(bvType);
3030  break;
3031  }
3032  case LEFTSHIFT: {
3033  if(!(1 == e.arity() &&
3034  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
3035  throw TypecheckException
3036  ("Not a bit-vector expression in bit-vector shift:\n\n "
3037  +e.toString());
3038  int bvLength = BVSize(e[0]);
3039  int shiftLength = getFixedLeftShiftParam(e);
3040  if(!(shiftLength >= 0))
3041  throw TypecheckException("Bad shift value in bit-vector shift:\n\n "
3042  +e.toString());
3043  int newLength = bvLength + shiftLength;
3044  Type bvType = newBitvectorType(newLength);
3045  e.setType(bvType);
3046  break;
3047  }
3048  case CONST_WIDTH_LEFTSHIFT: {
3049  if(!(1 == e.arity() &&
3050  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
3051  throw TypecheckException
3052  ("Not a bit-vector expression in bit-vector shift:\n\n "
3053  +e.toString());
3054  int bvLength = BVSize(e[0]);
3055  int shiftLength = getFixedLeftShiftParam(e);
3056  if(!(shiftLength >= 0))
3057  throw TypecheckException("Bad shift value in bit-vector shift:\n\n "
3058  +e.toString());
3059  Type bvType = newBitvectorType(bvLength);
3060  e.setType(bvType);
3061  break;
3062  }
3063  case RIGHTSHIFT: {
3064  if(!(1 == e.arity() &&
3065  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
3066  throw TypecheckException
3067  ("Not a bit-vector expression in bit-vector shift:\n\n "
3068  +e.toString());
3069  int bvLength = BVSize(e[0]);
3070  int shiftLength = getFixedRightShiftParam(e);
3071  if(!(shiftLength >= 0))
3072  throw TypecheckException("Bad shift value in bit-vector shift:\n\n "
3073  +e.toString());
3074  //int newLength = bvLength + shiftLength;
3075  Type bvType = newBitvectorType(bvLength);
3076  e.setType(bvType);
3077  break;
3078  }
3079  case BVTYPEPRED:
3080  e.setType(boolType());
3081  break;
3082  case SX: {
3083  if(!(1 == e.arity() &&
3084  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
3085  throw TypecheckException("Type Checking error:"\
3086  "non-bitvector \n"+ e.toString());
3087  int bvLength = getSXIndex(e);
3088  if(!(1 <= bvLength))
3089  throw TypecheckException("Type Checking error: \n"
3090  "out of range\n"+ e.toString());
3091  Type bvType = newBitvectorType(bvLength);
3092  e.setType(bvType);
3093  break;
3094  }
3095  case BVREPEAT: {
3096  if(!(1 == e.arity() &&
3097  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
3098  throw TypecheckException("Type Checking error:"\
3099  "non-bitvector \n"+ e.toString());
3100  int bvLength = getBVIndex(e) * BVSize(e[0]);
3101  if(!(1 <= bvLength))
3102  throw TypecheckException("Type Checking error: \n"
3103  "out of range\n"+ e.toString());
3104  Type bvType = newBitvectorType(bvLength);
3105  e.setType(bvType);
3106  break;
3107  }
3108  case BVZEROEXTEND: {
3109  if(!(1 == e.arity() &&
3110  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
3111  throw TypecheckException("Type Checking error:"\
3112  "non-bitvector \n"+ e.toString());
3113  int bvLength = getBVIndex(e) + BVSize(e[0]);
3114  if(!(1 <= bvLength))
3115  throw TypecheckException("Type Checking error: \n"
3116  "out of range\n"+ e.toString());
3117  Type bvType = newBitvectorType(bvLength);
3118  e.setType(bvType);
3119  break;
3120  }
3121  case BVROTL:
3122  case BVROTR: {
3123  if(!(1 == e.arity() &&
3124  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
3125  throw TypecheckException("Type Checking error:"\
3126  "non-bitvector \n"+ e.toString());
3127  e.setType(getBaseType(e[0]));
3128  break;
3129  }
3130  default:
3131  FatalAssert(false,
3132  "TheoryBitvector::computeType: unexpected kind in application" +
3133  int2string(e.getOpKind()));
3134  break;
3135  }
3136  }
3137  else {
3138  switch(e.getKind()) {
3139  case BOOLEXTRACT:
3140  case BVMULT:
3141  case EXTRACT:
3142  case BVPLUS:
3143  case LEFTSHIFT:
3144  case CONST_WIDTH_LEFTSHIFT:
3145  case RIGHTSHIFT:
3146  case BVTYPEPRED:
3147  case SX:
3148  case BVREPEAT:
3149  case BVZEROEXTEND:
3150  case BVROTL:
3151  case BVROTR:
3152  // These operators are handled above when applied to arguments, here we
3153  // are dealing with the operators themselves which are polymorphic, so
3154  // don't assign them a specific type.
3155  e.setType(Type::anyType(getEM()));
3156  break;
3157  case BVCONST: {
3158  Type bvType = newBitvectorType(getBVConstSize(e));
3159  e.setType(bvType);
3160  break;
3161  }
3162  case CONCAT: {
3163  if(e.arity() < 2)
3164  throw TypecheckException
3165  ("Concatenation must have at least 2 bit-vectors:\n\n "+e.toString());
3166 
3167  // Compute the total length of concatenation
3168  int bvLength(0);
3169  for(int i=0, iend=e.arity(); i<iend; ++i) {
3170  if(BITVECTOR != getBaseType(e[i]).getExpr().getOpKind())
3171  throw TypecheckException
3172  ("Not a bit-vector expression (child #"+int2string(i+1)
3173  +") in concatenation:\n\n "+e[i].toString()
3174  +"\n\nIn the expression:\n\n "+e.toString());
3175  bvLength += BVSize(e[i]);
3176  }
3177  Type bvType = newBitvectorType(bvLength);
3178  e.setType(bvType);
3179  break;
3180  }
3181  case BVAND:
3182  case BVOR:
3183  case BVXOR:
3184  case BVXNOR:
3185  {
3186  string kindStr((e.getOpKind()==BVAND)? "AND" :
3187  ((e.getOpKind()==BVOR)? "OR" :
3188  ((e.getOpKind()==BVXOR)? "BVXOR" : "BVXNOR")));
3189 
3190  if(e.arity() < 2)
3191  throw TypecheckException
3192  ("Bit-wise "+kindStr+" must have at least 2 bit-vectors:\n\n "
3193  +e.toString());
3194 
3195  int bvLength(0);
3196  bool first(true);
3197  for(int i=0, iend=e.arity(); i<iend; ++i) {
3198  if(BITVECTOR != getBaseType(e[i]).getExpr().getOpKind())
3199  throw TypecheckException
3200  ("Not a bit-vector expression (child #"+int2string(i+1)
3201  +") in bit-wise "+kindStr+":\n\n "+e[i].toString()
3202  +"\n\nIn the expression:\n\n "+e.toString());
3203  if(first) {
3204  bvLength = BVSize(e[i]);
3205  first=false;
3206  } else { // Check that the size is the same for all subsequent BVs
3207  if(BVSize(e[i]) != bvLength)
3208  throw TypecheckException
3209  ("Mismatched bit-vector size in bit-wise "+kindStr+" (child #"
3210  +int2string(i)+").\nExpected type: "
3211  +newBitvectorType(bvLength).toString()
3212  +"\nFound: "+e[i].getType().toString()
3213  +"\nIn the following expression:\n\n "+e.toString());
3214  }
3215  }
3216  e.setType(newBitvectorType(bvLength));
3217  break;
3218  }
3219  case BVNEG:{
3220  if(!(1 == e.arity() &&
3221  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
3222  throw TypecheckException
3223  ("Not a bit-vector expression in bit-wise negation:\n\n "
3224  + e.toString());
3225  e.setType(e[0].getType());
3226  break;
3227  }
3228  case BVNAND:
3229  case BVNOR:
3230  case BVCOMP:
3231  case BVSUB:
3232  case BVUDIV:
3233  case BVSDIV:
3234  case BVUREM:
3235  case BVSREM:
3236  case BVSMOD:
3237  case BVSHL:
3238  case BVASHR:
3239  case BVLSHR:
3240  if(!(2 == e.arity() &&
3241  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind() &&
3242  BITVECTOR == getBaseType(e[1]).getExpr().getOpKind()))
3243  throw TypecheckException
3244  ("Expressions must have arity=2, and"
3245  "each subterm must be a bitvector term:\n"
3246  "e = " +e.toString());
3247  if (BVSize(e[0]) != BVSize(e[1]))
3248  throw TypecheckException
3249  ("Expected args of same size:\n"
3250  "e = " +e.toString());
3251  if (e.getKind() == BVCOMP) {
3253  }
3254  else {
3255  e.setType(getBaseType(e[0]));
3256  }
3257  break;
3258  case BVUMINUS:{
3259  Type bvType(getBaseType(e[0]));
3260  if(!(1 == e.arity() &&
3261  BITVECTOR == bvType.getExpr().getOpKind()))
3262  throw TypecheckException
3263  ("Not a bit-vector expression in BVUMINUS:\n\n "
3264  +e.toString());
3265  e.setType(bvType);
3266  break;
3267  }
3268  case BVLT:
3269  case BVLE:
3270  case BVGT:
3271  case BVGE:
3272  case BVSLT:
3273  case BVSLE:
3274  case BVSGT:
3275  case BVSGE:
3276  if(!(2 == e.arity() &&
3277  BITVECTOR == getBaseType(e[0]).getExpr().getOpKind() &&
3278  BITVECTOR == getBaseType(e[1]).getExpr().getOpKind()))
3279  throw TypecheckException
3280  ("BVLT/BVLE expressions must have arity=2, and"
3281  "each subterm must be a bitvector term:\n"
3282  "e = " +e.toString());
3283  e.setType(boolType());
3284  break;
3285  default:
3286  FatalAssert(false,
3287  "TheoryBitvector::computeType: wrong input" +
3288  int2string(e.getOpKind()));
3289  break;
3290  }
3291  }
3292  TRACE("bitvector", "TheoryBitvector::computeType => ", e.getType(), " }");
3293 }
3294 
3295 
3296 void TheoryBitvector::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
3297  switch(e.getOpKind()) {
3298  case BVPLUS:
3299  case BVSUB:
3300  case BVUMINUS:
3301  case BVMULT:
3302  case LEFTSHIFT:
3303  case CONST_WIDTH_LEFTSHIFT:
3304  case RIGHTSHIFT:
3305  case BVOR:
3306  case BVAND:
3307  case BVXOR:
3308  case BVXNOR:
3309  case BVNAND:
3310  case BVNOR:
3311  case BVNEG:
3312  case CONCAT:
3313  case EXTRACT:
3314  case BVSLT:
3315  case BVSLE:
3316  case BVSGT:
3317  case BVSGE:
3318  case BVLT:
3319  case BVLE:
3320  case BVGT:
3321  case BVGE:
3322  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
3323  // getModelTerm(*i, v);
3324  v.push_back(*i);
3325  return;
3326  case BVCONST: // No model variables here
3327  return;
3328  default: break; // It's a variable; continue processing
3329  }
3330 
3331  Type tp(e.getType());
3332  switch(tp.getExpr().getOpKind()) {
3333  case BITVECTOR: {
3334  int n = getBitvectorTypeParam(tp);
3335  for(int i=0; i<n; i = i+1)
3336  v.push_back(newBoolExtractExpr(e, i));
3337  break;
3338  }
3339  default:
3340  v.push_back(e);
3341  }
3342 }
3343 
3344 
3345 void TheoryBitvector::computeModel(const Expr& e, std::vector<Expr>& v) {
3346  switch(e.getOpKind()) {
3347  case BVPLUS:
3348  case BVSUB:
3349  case BVUMINUS:
3350  case BVMULT:
3351  case LEFTSHIFT:
3352  case CONST_WIDTH_LEFTSHIFT:
3353  case RIGHTSHIFT:
3354  case BVOR:
3355  case BVAND:
3356  case BVXOR:
3357  case BVXNOR:
3358  case BVNAND:
3359  case BVNOR:
3360  case BVNEG:
3361  case CONCAT:
3362  case EXTRACT:
3363  case SX:
3364  case BVSLT:
3365  case BVSLE:
3366  case BVSGT:
3367  case BVSGE:
3368  case BVLT:
3369  case BVLE:
3370  case BVGT:
3371  case BVGE: {
3372  // More primitive vars are kids, and they should have been
3373  // assigned concrete values
3374  assignValue(simplify(e));
3375  v.push_back(e);
3376  return;
3377  }
3378  case BVCONST: // No model variables here
3379  return;
3380  default: break; // It's a variable; continue processing
3381  }
3382 
3383  Type tp(e.getType());
3384  switch(tp.getExpr().getOpKind()) {
3385  case BITVECTOR: {
3386  const Rational& n = getBitvectorTypeParam(tp);
3387  vector<bool> bits;
3388  // FIXME: generate concrete assignment from bits using proof
3389  // rules. For now, just create a new assignment.
3390  for(int i=0; i<n; i++) {
3392  DebugAssert(val.getRHS().isBoolConst(),
3393  "TheoryBitvector::computeModel: unassigned bit: "
3394  +val.getExpr().toString());
3395  bits.push_back(val.getRHS().isTrue());
3396  }
3397  Expr c(newBVConstExpr(bits));
3398  assignValue(e, c);
3399  v.push_back(e);
3400  break;
3401  }
3402  default:
3403  FatalAssert(false, "TheoryBitvector::computeModel[not BITVECTOR type]("
3404  +e.toString()+")");
3405  }
3406 }
3407 
3408 
3409 // TODO: get rid of this - don't need type predicates for bv's, just need to share the right terms
3410 Expr
3413  "TheoryBitvector::computeTypePred: t = "+t.toString());
3414 // switch(e.getKind()) {
3415 // case BVCONST:
3416 // return getEM()->trueExpr();
3417 // default:
3418  return e.getEM()->trueExpr();
3419 
3420  // return newBitvectorTypePred(t, e);
3421  // }
3422 }
3423 
3424 ///////////////////////////////////////////////////////////////////////////////
3425 // Pretty-printing //
3426 ///////////////////////////////////////////////////////////////////////////////
3427 
3428 ExprStream&
3430 
3431  d_theoryUsed = true;
3432  switch( e.getOpKind() ) {
3433 
3434  case CONCAT:
3435  if( e.arity() == 0 )
3436  throw SmtlibException("TheoryBitvector::print: CONCAT arity = 0");
3437  else if( e.arity() == 1 )
3438  os << e[0];
3439  else {
3440  int i;
3441  for( i = 0; i < e.arity(); ++i ) {
3442  if( (i + 1) == e.arity() ) {
3443  os << e[i];
3444  } else {
3445  os << "(concat" << space << push << e[i] << space << push;
3446  }
3447  }
3448  for( --i; i != 0; --i )
3449  os << push << ")";
3450  }
3451  break;
3452  case BVSHL:
3453  os << "(bvshl" << space << push << e[0] << space << push << e[1] << push
3454  << ")";
3455  break;
3456  case BVLSHR:
3457  os << "(bvlshr" << space << push << e[0] << space << push << e[1] << push
3458  << ")";
3459  break;
3460  case BVASHR:
3461  os << "(bvashr" << space << push << e[0] << space << push << e[1] << push
3462  << ")";
3463  break;
3464  case BVAND:
3465  if( e.arity() == 0 )
3466  throw SmtlibException("TheoryBitvector::print: BVAND arity = 0");
3467  else if( e.arity() == 1 )
3468  os << e[0];
3469  else {
3470  int i;
3471  for( i = 0; i < e.arity(); ++i ) {
3472  if( (i + 1) == e.arity() ) {
3473  os << e[i];
3474  } else {
3475  os << "(bvand" << space << push << e[i] << space << push;
3476  }
3477  }
3478  for( --i; i != 0; --i )
3479  os << push << ")";
3480  }
3481  break;
3482  case BVOR:
3483  if( e.arity() == 0 )
3484  throw SmtlibException("TheoryBitvector::print: BVAND arity = 0");
3485  else if( e.arity() == 1 )
3486  os << e[0];
3487  else {
3488  int i;
3489  for( i = 0; i < e.arity(); ++i ) {
3490  if( (i + 1) == e.arity() ) {
3491  os << e[i];
3492  } else {
3493  os << "(bvor" << space << push << e[i] << space << push;
3494  }
3495  }
3496  for( --i; i != 0; --i )
3497  os << push << ")";
3498  }
3499  break;
3500  case BVXOR:
3501  if( e.arity() == 0 )
3502  throw SmtlibException("TheoryBitvector::print: BVXOR arity = 0");
3503  else if( e.arity() == 1 )
3504  os << e[0];
3505  else {
3506  int i;
3507  for( i = 0; i < e.arity(); ++i ) {
3508  if( (i + 1) == e.arity() ) {
3509  os << e[i];
3510  } else {
3511  os << "(bvxor" << space << push << e[i] << space << push;
3512  }
3513  }
3514  for( --i; i != 0; --i )
3515  os << push << ")";
3516  }
3517  break;
3518  case BVXNOR:
3519  if( e.arity() == 0 )
3520  throw SmtlibException("TheoryBitvector::print: BVXNOR arity = 0");
3521  else if( e.arity() == 1 )
3522  os << e[0];
3523  else {
3524  int i;
3525  for( i = 0; i < e.arity(); ++i ) {
3526  if( (i + 1) == e.arity() ) {
3527  os << e[i];
3528  } else {
3529  os << "(bvxnor" << space << push << e[i] << space << push;
3530  }
3531  }
3532  for( --i; i != 0; --i )
3533  os << push << ")";
3534  }
3535  break;
3536  case BVNEG:
3537  os << "(bvnot" << space << push << e[0] << push << ")";
3538  break;
3539  case BVNAND:
3540  os << "(bvnand" << space << push << e[0] << space << push << e[1] << push
3541  << ")";
3542  break;
3543  case BVNOR:
3544  os << "(bvnor" << space << push << e[0] << space << push << e[1] << push
3545  << ")";
3546  break;
3547  case BVCOMP:
3548  os << "(bvcomp" << space << push << e[0] << space << push << e[1] << push
3549  << ")";
3550  break;
3551 
3552  case BVUMINUS:
3553  os << "(bvneg" << space << push << e[0] << push << ")";
3554  break;
3555  case BVPLUS: {
3556  DebugAssert(e.arity() > 0, "expected arity > 0 in BVPLUS");
3557  int length = getBVPlusParam(e);
3558  int i;
3559  for( i = 0; i < e.arity(); ++i ) {
3560  if( (i + 1) == e.arity() ) {
3561  os << pad(length, e[i]);
3562  } else {
3563  os << "(bvadd" << space << push << pad(length, e[i]) << space << push;
3564  }
3565  }
3566  for( --i; i != 0; --i )
3567  os << push << ")";
3568  }
3569  break;
3570  case BVSUB:
3571  os << "(bvsub" << space << push << e[0] << space << push << e[1] << push
3572  << ")";
3573  break;
3574  case BVMULT: {
3575  int length = getBVMultParam(e);
3576  os << "(bvmul" << space << push << pad(length, e[0]) << space << push
3577  << pad(length, e[1]) << push << ")";
3578  break;
3579  }
3580  case BVUDIV:
3581  os << "(bvudiv" << space << push << e[0] << space << push << e[1] << push
3582  << ")";
3583  break;
3584  case BVSDIV:
3585  os << "(bvsdiv" << space << push << e[0] << space << push << e[1] << push
3586  << ")";
3587  break;
3588  case BVUREM:
3589  os << "(bvurem" << space << push << e[0] << space << push << e[1] << push
3590  << ")";
3591  break;
3592  case BVSREM:
3593  os << "(bvsrem" << space << push << e[0] << space << push << e[1] << push
3594  << ")";
3595  break;
3596  case BVSMOD:
3597  os << "(bvsmod" << space << push << e[0] << space << push << e[1] << push
3598  << ")";
3599  break;
3600 
3601  case BVLT:
3602  os << "(bvult" << space << push << e[0] << space << push << e[1] << push
3603  << ")";
3604  break;
3605  case BVLE:
3606  os << "(bvule" << space << push << e[0] << space << push << e[1] << push
3607  << ")";
3608  break;
3609  case BVGT:
3610  os << "(bvugt" << space << push << e[0] << space << push << e[1] << push
3611  << ")";
3612  break;
3613  case BVGE:
3614  os << "(bvuge" << space << push << e[0] << space << push << e[1] << push
3615  << ")";
3616  break;
3617  case BVSLT:
3618  os << "(bvslt" << space << push << e[0] << space << push << e[1] << push
3619  << ")";
3620  break;
3621  case BVSLE:
3622  os << "(bvsle" << space << push << e[0] << space << push << e[1] << push
3623  << ")";
3624  break;
3625  case BVSGT:
3626  os << "(bvsgt" << space << push << e[0] << space << push << e[1] << push
3627  << ")";
3628  break;
3629  case BVSGE:
3630  os << "(bvsge" << space << push << e[0] << space << push << e[1] << push
3631  << ")";
3632  break;
3633 
3634  case INTTOBV:
3635  throw SmtlibException(
3636  "TheoryBitvector::print: INTTOBV, SMTLIB not supported");
3637  break;
3638  case BVTOINT:
3639  throw SmtlibException(
3640  "TheoryBitvector::print: BVTOINT, SMTLIB not supported");
3641  break;
3642 
3643  case BVTYPEPRED:
3644  throw SmtlibException(
3645  "TheoryBitvector::print: BVTYPEPRED, SMTLIB not supported");
3646  if( e.isApply() ) {
3647  os << "BVTYPEPRED[" << push << e.getOp().getExpr() << push << "," << pop
3648  << space << e[0] << push << "]";
3649  } else
3650  e.printAST(os);
3651  break;
3652 
3653  default:
3654  FatalAssert(false, "Unknown BV kind");
3655  e.printAST(os);
3656  break;
3657  }
3658  return os;
3659 }
3660 
3661 ExprStream&
3663  switch(os.lang()) {
3664  case PRESENTATION_LANG:
3665  switch(e.getOpKind()) {
3666 
3667  case BITVECTOR: //printing type expression
3668  os << "BITVECTOR(" << push
3669  << getBitvectorTypeParam(e) << push << ")";
3670  break;
3671 
3672  case BVCONST: {
3673  std::ostringstream ss;
3674  ss << "0bin";
3675  for(int i=(int)getBVConstSize(e)-1; i>=0; --i)
3676  ss << (getBVConstValue(e, i) ? "1" : "0");
3677  os << ss.str();
3678  break;
3679  }
3680 
3681  case CONCAT:
3682  if(e.arity() <= 1) e.printAST(os);
3683  else {
3684  os << "(" << push;
3685  bool first(true);
3686  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
3687  if(first) first=false;
3688  else os << space << "@" << space;
3689  os << (*i);
3690  }
3691  os << push << ")";
3692  }
3693  break;
3694  case EXTRACT:
3695  os << "(" << push << e[0] << push << ")" << pop << pop
3696  << "[" << push << getExtractHi(e) << ":";
3697  os << getExtractLow(e) << push << "]";
3698  break;
3699  case BOOLEXTRACT:
3700  os << "BOOLEXTRACT(" << push << e[0] << ","
3701  << getBoolExtractIndex(e) << push << ")";
3702  break;
3703 
3704  case LEFTSHIFT:
3705  os << "(" << push << e[0] << space << "<<" << space
3706  << getFixedLeftShiftParam(e) << push << ")";
3707  break;
3708  case CONST_WIDTH_LEFTSHIFT:
3709  os << "(" << push << e[0] << space << "<<" << space
3710  << getFixedLeftShiftParam(e) << push << ")";
3711  os << "[" << push << BVSize(e)-1 << ":0]";
3712  break;
3713  case RIGHTSHIFT:
3714  os << "(" << push << e[0] << space << ">>" << space
3715  << getFixedRightShiftParam(e) << push << ")";
3716  break;
3717  case BVSHL:
3718  os << "BVSHL(" << push << e[0] << "," << e[1] << push << ")";
3719  break;
3720  case BVLSHR:
3721  os << "BVLSHR(" << push << e[0] << "," << e[1] << push << ")";
3722  break;
3723  case BVASHR:
3724  os << "BVASHR(" << push << e[0] << "," << e[1] << push << ")";
3725  break;
3726  case BVZEROEXTEND:
3727  os << "BVZEROEXTEND(" << push << e[0] << "," << getBVIndex(e) << push << ")";
3728  break;
3729  case BVREPEAT:
3730  os << "BVREPEAT(" << push << e[0] << "," << getBVIndex(e) << push << ")";
3731  break;
3732  case BVROTL:
3733  os << "BVROTL(" << push << e[0] << "," << getBVIndex(e) << push << ")";
3734  break;
3735  case BVROTR:
3736  os << "BVROTR(" << push << e[0] << "," << getBVIndex(e) << push << ")";
3737  break;
3738  case SX:
3739  os << "SX(" << push << e[0] << ","
3740  << push << getSXIndex(e) << ")";
3741  break;
3742 
3743  case BVAND:
3744  if(e.arity() <= 1) e.printAST(os);
3745  else {
3746  os << "(" << push;
3747  bool first(true);
3748  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
3749  if(first) first=false;
3750  else os << space << "&" << space;
3751  os << (*i);
3752  }
3753  os << push << ")";
3754  }
3755  break;
3756  case BVOR:
3757  if(e.arity() <= 1) e.printAST(os);
3758  else {
3759  os << "(" << push;
3760  bool first(true);
3761  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
3762  if(first) first=false;
3763  else os << space << "|" << space;
3764  os << (*i);
3765  }
3766  os << push << ")";
3767  }
3768  break;
3769  case BVXOR:
3770  DebugAssert(e.arity() > 0, "TheoryBitvector::print: BVXOR arity <= 0");
3771  if (e.arity() == 1) os << e[0];
3772  else {
3773  int i;
3774  for(i = 0; i < e.arity(); ++i) {
3775  if ((i+1) == e.arity()) {
3776  os << e[i];
3777  }
3778  else {
3779  os << "BVXOR(" << push << e[i] << "," << push;
3780  }
3781  }
3782  for (--i; i != 0; --i) os << push << ")";
3783  }
3784  break;
3785  case BVXNOR:
3786  DebugAssert(e.arity() > 0, "TheoryBitvector::print: BVXNOR arity <= 0");
3787  if (e.arity() == 1) os << e[0];
3788  else {
3789  int i;
3790  for(i = 0; i < e.arity(); ++i) {
3791  if ((i+1) == e.arity()) {
3792  os << e[i];
3793  }
3794  else {
3795  os << "BVXNOR(" << push << e[i] << "," << push;
3796  }
3797  }
3798  for (--i; i != 0; --i) os << push << ")";
3799  }
3800  break;
3801  case BVNEG:
3802  os << "(~(" << push << e[0] << push << "))";
3803  break;
3804  case BVNAND:
3805  os << "BVNAND(" << push << e[0] << "," << e[1] << push << ")";
3806  break;
3807  case BVNOR:
3808  os << "BVNAND(" << push << e[0] << "," << e[1] << push << ")";
3809  break;
3810  case BVCOMP:
3811  os << "BVCOMP(" << push << e[0] << "," << e[1] << push << ")";
3812  break;
3813 
3814  case BVUMINUS:
3815  os << "BVUMINUS(" << push << e[0] << push << ")";
3816  break;
3817  case BVPLUS:
3818  os << "BVPLUS(" << push << getBVPlusParam(e);
3819  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
3820  os << push << "," << pop << space << (*i);
3821  }
3822  os << push << ")";
3823  break;
3824  case BVSUB:
3825  os << "BVSUB(" << push << BVSize(e) << "," << e[0] << "," << e[1] << push << ")";
3826  break;
3827  case BVMULT:
3828  os << "BVMULT(" << push << getBVMultParam(e) << "," << e[0] << "," << e[1]<<push<<")";
3829  break;
3830  case BVUDIV:
3831  os << "BVUDIV(" << push << e[0] << "," << e[1]<<push<<")";
3832  break;
3833  case BVSDIV:
3834  os << "BVSDIV(" << push << e[0] << "," << e[1]<<push<<")";
3835  break;
3836  case BVUREM:
3837  os << "BVUREM(" << push << e[0] << "," << e[1]<<push<<")";
3838  break;
3839  case BVSREM:
3840  os << "BVSREM(" << push << e[0] << "," << e[1]<<push<<")";
3841  break;
3842  case BVSMOD:
3843  os << "BVSMOD(" << push << e[0] << "," << e[1]<<push<<")";
3844  break;
3845  case BVLT:
3846  os << "BVLT(" << push << e[0] << "," << e[1] << push << ")";
3847  break;
3848  case BVLE:
3849  os << "BVLE(" << push << e[0] << "," << e[1] << push << ")";
3850  break;
3851  case BVGT:
3852  os << "BVGT(" << push << e[0] << "," << e[1] << push << ")";
3853  break;
3854  case BVGE:
3855  os << "BVGE(" << push << e[0] << "," << e[1] << push << ")";
3856  break;
3857  case BVSLT:
3858  os << "BVSLT(" << push << e[0] << "," << e[1] << push << ")";
3859  break;
3860  case BVSLE:
3861  os << "BVSLE(" << push << e[0] << "," << e[1] << push << ")";
3862  break;
3863  case BVSGT:
3864  os << "BVSGT(" << push << e[0] << "," << e[1] << push << ")";
3865  break;
3866  case BVSGE:
3867  os << "BVSGE(" << push << e[0] << "," << e[1] << push << ")";
3868  break;
3869 
3870  case INTTOBV:
3871  FatalAssert(false, "INTTOBV not implemented yet");
3872  break;
3873  case BVTOINT:
3874  FatalAssert(false, "BVTOINT not implemented yet");
3875  break;
3876 
3877  case BVTYPEPRED:
3878  if(e.isApply()) {
3879  os << "BVTYPEPRED[" << push << e.getOp().getExpr()
3880  << push << "," << pop << space << e[0]
3881  << push << "]";
3882  } else
3883  e.printAST(os);
3884  break;
3885 
3886  default:
3887  FatalAssert(false, "Unknown BV kind");
3888  e.printAST(os);
3889  break;
3890  }
3891  break;
3892 
3893  case SMTLIB_LANG:
3894  switch(e.getOpKind()) {
3895  case BITVECTOR: //printing type expression
3896  os << push << "BitVec[" << getBitvectorTypeParam(e) << "]";
3897  break;
3898 
3899  case BVCONST: {
3900  Rational r = computeBVConst(e);
3901  DebugAssert(r.isInteger() && r >= 0, "Expected non-negative integer");
3902  os << push << "bv" << r << "[" << BVSize(e) << "]";
3903  break;
3904  }
3905 
3906  case EXTRACT:
3907  os << push << "(extract[" << getExtractHi(e) << ":" << getExtractLow(e)
3908  << "]";
3909  os << space << push << e[0] << push << ")";
3910  break;
3911  case BOOLEXTRACT:
3912  os << "(=" << space << push << "(extract[" << getBoolExtractIndex(e) << ":"
3913  << getBoolExtractIndex(e) << "]";
3914  os << space << push << e[0] << push << ")" << space << "bit1" << push
3915  << ")";
3916  break;
3917 
3918  case LEFTSHIFT: {
3919  int bvLength = getFixedLeftShiftParam(e);
3920  if( bvLength != 0 ) {
3921  os << "(concat" << space << push << e[0] << space;
3922  os << push << "bv0[" << bvLength << "]" << push << ")";
3923  break;
3924  }
3925  // else fall-through
3926  }
3927  case CONST_WIDTH_LEFTSHIFT:
3928  os << "(bvshl" << space << push << e[0] << space << push << "bv"
3929  << getFixedLeftShiftParam(e) << "[" << BVSize(e[0]) << "]" << push
3930  << ")";
3931  break;
3932  case RIGHTSHIFT:
3933  os << "(bvlshr" << space << push << e[0] << space << push << "bv"
3934  << getFixedRightShiftParam(e) << "[" << BVSize(e[0]) << "]" << push
3935  << ")";
3936  break;
3937  case SX: {
3938  int extend = getSXIndex(e) - BVSize(e[0]);
3939  if( extend == 0 )
3940  os << e[0];
3941  else if( extend < 0 )
3942  throw SmtlibException(
3943  "TheoryBitvector::print: SX: extension is shorter than argument");
3944  else
3945  os << "(sign_extend[" << extend << "]" << space << push << e[0] << push
3946  << ")";
3947  break;
3948  }
3949  case BVREPEAT:
3950  os << "(repeat[" << getBVIndex(e) << "]" << space << push << e[0] << push
3951  << ")";
3952  break;
3953  case BVZEROEXTEND: {
3954  int extend = getBVIndex(e);
3955  if( extend == 0 )
3956  os << e[0];
3957  else if( extend < 0 )
3958  throw SmtlibException(
3959  "TheoryBitvector::print: ZEROEXTEND: extension is less than zero");
3960  else
3961  os << "(zero_extend[" << extend << "]" << space << push << e[0] << push
3962  << ")";
3963  break;
3964  }
3965  case BVROTL:
3966  os << "(rotate_left[" << getBVIndex(e) << "]" << space << push << e[0]
3967  << push << ")";
3968  break;
3969  case BVROTR:
3970  os << "(rotate_right[" << getBVIndex(e) << "]" << space << push << e[0]
3971  << push << ")";
3972  break;
3973 
3974  default:
3975  printSmtLibShared(os,e);
3976  }
3977  break;
3978 
3979  case SMTLIB_V2_LANG:
3980  switch(e.getOpKind()) {
3981  case BITVECTOR: //printing type expression
3982  os << push << "(_" << space << "BitVec" << space << getBitvectorTypeParam(e) << ")" << pop;
3983  break;
3984 
3985  case BVCONST: {
3986  Rational r = computeBVConst(e);
3987  DebugAssert(r.isInteger() && r >= 0, "Expected non-negative integer");
3988  os << push << "(_ bv" << r << space << BVSize(e) << ")";
3989  break;
3990  }
3991 
3992  case EXTRACT:
3993  os << push << "((_ extract" << space << getExtractHi(e) << space << getExtractLow(e)
3994  << ")";
3995  os << space << push << e[0] << push << ")";
3996  break;
3997 
3998  case BOOLEXTRACT:
3999  os << "(=" << space << push << "((_ extract" << getBoolExtractIndex(e) << space
4000  << getBoolExtractIndex(e) << ")";
4001  os << space << push << e[0] << push << ")" << space << "#b1" << push
4002  << ")";
4003  break;
4004 
4005  case LEFTSHIFT: {
4006  int bvLength = getFixedLeftShiftParam(e);
4007  if( bvLength != 0 ) {
4008  os << "(concat" << space << push << e[0] << space;
4009  os << push << "#b";
4010  for (int i = 0; i < bvLength; ++i) os << "0";
4011  os << push << ")";
4012  break;
4013  }
4014  // else fall-through
4015  }
4016  case CONST_WIDTH_LEFTSHIFT:
4017  os << "(bvshl" << space << push << e[0] << space << push;
4018  os << newBVConstExpr(getFixedLeftShiftParam(e), BVSize(e[0])) << push << ")";
4019  break;
4020  case RIGHTSHIFT:
4021  os << "(bvlshr" << space << push << e[0] << space << push;
4022  os << newBVConstExpr(getFixedRightShiftParam(e), BVSize(e[0])) << push << ")";
4023  break;
4024  case SX: {
4025  int extend = getSXIndex(e) - BVSize(e[0]);
4026  if( extend == 0 )
4027  os << e[0];
4028  else if( extend < 0 )
4029  throw SmtlibException(
4030  "TheoryBitvector::print: SX: extension is shorter than argument");
4031  else
4032  os << "((_ sign_extend" << space << extend << ")" << space << push << e[0] << push
4033  << ")";
4034  break;
4035  }
4036  case BVREPEAT:
4037  os << "((_ repeat" << space << getBVIndex(e) << ")" << space << push << e[0] << push
4038  << ")";
4039  break;
4040  case BVZEROEXTEND: {
4041  int extend = getBVIndex(e);
4042  if( extend == 0 )
4043  os << e[0];
4044  else if( extend < 0 )
4045  throw SmtlibException(
4046  "TheoryBitvector::print: ZEROEXTEND: extension is less than zero");
4047  else
4048  os << "((_ zero_extend" << space << extend << ")" << space << push << e[0] << push
4049  << ")";
4050  break;
4051  }
4052  case BVROTL:
4053  os << "((_ rotate_left" << space << getBVIndex(e) << ")" << space << push << e[0]
4054  << push << ")";
4055  break;
4056  case BVROTR:
4057  os << "((_ rotate_right" << space << getBVIndex(e) << ")" << space << push << e[0]
4058  << push << ")";
4059  break;
4060 
4061  default:
4062  printSmtLibShared(os,e);
4063  }
4064  break;
4065 
4066  default:
4067  switch(e.getOpKind()) {
4068  case BVCONST: {
4069  os << "0bin";
4070  for(int i=(int)getBVConstSize(e)-1; i>=0; --i)
4071  os << (getBVConstValue(e, i) ? "1" : "0");
4072  break;
4073  }
4074  default:
4075  e.printAST(os);
4076  break;
4077  }
4078  }
4079  return os;
4080 }
4081 
4082 
4083 ///////////////////////////////////////////////////////////////////////////////
4084 //parseExprOp:
4085 //translating special Exprs to regular EXPR??
4086 ///////////////////////////////////////////////////////////////////////////////
4088 {
4089  d_theoryUsed = true;
4090  TRACE("parser", "TheoryBitvector::parseExprOp(", e, ")");
4091 
4092  // If the expression is not a list, it must have been already
4093  // parsed, so just return it as is.
4094  if(RAW_LIST != e.getKind()) return e;
4095 
4096  if(!(e.arity() > 0))
4097  throw ParserException("TheoryBitvector::parseExprOp: wrong input:\n\n"
4098  +e.toString());
4099 
4100  const Expr& c1 = e[0][0];
4101  int kind = getEM()->getKind(c1.getString());
4102  switch(kind) {
4103 
4104  case BITVECTOR:
4105  if(!(e.arity() == 2))
4106  throw ParserException("TheoryBitvector::parseExprOp: BITVECTOR"
4107  "kind should have exactly 1 arg:\n\n"
4108  + e.toString());
4109  if(!(e[1].isRational() && e[1].getRational().isInteger()))
4110  throw ParserException("BITVECTOR TYPE must have an integer constant"
4111  "as its first argument:\n\n"
4112  +e.toString());
4113  if(!(e[1].getRational().getInt() >=0 ))
4114  throw ParserException("parameter must be an integer constant >= 0.\n"
4115  +e.toString());
4116  return newBitvectorTypeExpr(e[1].getRational().getInt());
4117  break;
4118 
4119  case BVCONST:
4120  if(!(e.arity() == 2 || e.arity() == 3))
4121  throw ParserException("TheoryBitvector::parseExprOp: BVCONST "
4122  "kind should have 1 or 2 args:\n\n"
4123  + e.toString());
4124  if(!(e[1].isRational() || e[1].isString()))
4125  throw ParserException("TheoryBitvector::parseExprOp: BVCONST "
4126  "kind should have arg of type Rational "
4127  "or String:\n\n" + e.toString());
4128  if(e[1].isRational()) { // ("BVCONST" value [bitwidth])
4129  if(e.arity()==3) {
4130  if(!e[2].isRational() || !e[2].getRational().isInteger())
4131  throw ParserException("TheoryBitvector::parseExprOp: BVCONST "
4132  "2nd argument must be an integer:\n\n"
4133  +e.toString());
4134  return newBVConstExpr(e[1].getRational(), e[2].getRational().getInt());
4135  } else
4136  return newBVConstExpr(e[1].getRational());
4137  } else if(e[1].isString()) { // ("BVCONST" string [base])
4138  if(e.arity() == 3) {
4139  if(!e[2].isRational() || !e[2].getRational().isInteger())
4140  throw ParserException("TheoryBitvector::parseExprOp: BVCONST "
4141  "2nd argument must be an integer:\n\n"
4142  +e.toString());
4143  return newBVConstExpr(e[1].getString(), e[2].getRational().getInt());
4144  } else
4145  return newBVConstExpr(e[1].getString());
4146  }
4147  break;
4148 
4149  case CONCAT: {
4150  if(!(e.arity() >= 3))
4151  throw ParserException("TheoryBitvector::parseExprOp: CONCAT"
4152  "kind should have at least 2 args:\n\n"
4153  + e.toString());
4154  vector<Expr> kids;
4155  Expr::iterator i=e.begin(), iend=e.end();
4156  DebugAssert(i!=iend, "TheoryBitvector::parseExprOp("+e.toString()+")");
4157  ++i; // Skip the first element - the operator name
4158  for(; i!=iend; ++i)
4159  kids.push_back(parseExpr(*i));
4160  return newConcatExpr(kids);
4161  break;
4162  }
4163  case EXTRACT: {
4164  if(!(e.arity() == 4))
4165  throw ParserException("TheoryBitvector::parseExprOp: EXTRACT"
4166  "kind should have exactly 3 arg:\n\n"
4167  + e.toString());
4168  if(!e[1].isRational() || !e[1].getRational().isInteger())
4169  throw ParserException("EXTRACT must have an integer constant as its "
4170  "1st argument:\n\n"
4171  +e.toString());
4172  if(!e[2].isRational() || !e[2].getRational().isInteger())
4173  throw ParserException("EXTRACT must have an integer constant as its "
4174  "2nd argument:\n\n"
4175  +e.toString());
4176  int hi = e[1].getRational().getInt();
4177  int lo = e[2].getRational().getInt();
4178  if(!(hi >= lo && lo >=0))
4179  throw ParserException("parameter must be an integer constant >= 0.\n"
4180  +e.toString());
4181 
4182  // Check for extract of left shift
4183  Expr arg = e[3];
4184  if (lo == 0 && arg.getKind() == RAW_LIST && arg[0].getKind() == ID &&
4185  getEM()->getKind(arg[0][0].getString()) == LEFTSHIFT) {
4186  if(!(arg.arity() == 3))
4187  throw ParserException("TheoryBitvector::parseExprOp: LEFTSHIFT"
4188  "kind should have exactly 2 arg:\n\n"
4189  + arg.toString());
4190  if(!arg[2].isRational() || !arg[2].getRational().isInteger())
4191  throw ParserException("LEFTSHIFT must have an integer constant as its "
4192  "2nd argument:\n\n"
4193  +arg.toString());
4194  if(!(arg[2].getRational().getInt() >=0 ))
4195  throw ParserException("parameter must be an integer constant >= 0.\n"
4196  +arg.toString());
4197  Expr ls_arg = parseExpr(arg[1]);
4198  if (BVSize(ls_arg) == hi + 1) {
4199  return newFixedConstWidthLeftShiftExpr(ls_arg, arg[2].getRational().getInt());
4200  }
4201  }
4202  return newBVExtractExpr(parseExpr(arg), hi, lo);
4203  break;
4204  }
4205  case BOOLEXTRACT:
4206  if(!(e.arity() == 3))
4207  throw ParserException("TheoryBitvector::parseExprOp: BOOLEXTRACT"
4208  "kind should have exactly 2 arg:\n\n"
4209  + e.toString());
4210  if(!e[2].isRational() || !e[2].getRational().isInteger())
4211  throw ParserException("BOOLEXTRACT must have an integer constant as its"
4212  " 2nd argument:\n\n"
4213  +e.toString());
4214  if(!(e[2].getRational().getInt() >=0 ))
4215  throw ParserException("parameter must be an integer constant >= 0.\n"
4216  +e.toString());
4217  return newBoolExtractExpr(parseExpr(e[1]), e[2].getRational().getInt());
4218  break;
4219 
4220  case LEFTSHIFT:
4221  if(!(e.arity() == 3))
4222  throw ParserException("TheoryBitvector::parseExprOp: LEFTSHIFT"
4223  "kind should have exactly 2 arg:\n\n"
4224  + e.toString());
4225  if(!e[2].isRational() || !e[2].getRational().isInteger())
4226  throw ParserException("LEFTSHIFT must have an integer constant as its "
4227  "2nd argument:\n\n"
4228  +e.toString());
4229  if(!(e[2].getRational().getInt() >=0 ))
4230  throw ParserException("parameter must be an integer constant >= 0.\n"
4231  +e.toString());
4232  return newFixedLeftShiftExpr(parseExpr(e[1]), e[2].getRational().getInt());
4233  break;
4234  case CONST_WIDTH_LEFTSHIFT:
4235  if(!(e.arity() == 3))
4236  throw ParserException("TheoryBitvector::parseExprOp: CONST_WIDTH_LEFTSHIFT"
4237  "kind should have exactly 2 arg:\n\n"
4238  + e.toString());
4239  if(!e[2].isRational() || !e[2].getRational().isInteger())
4240  throw ParserException("CONST_WIDTH_LEFTSHIFT must have an integer constant as its "
4241  "2nd argument:\n\n"
4242  +e.toString());
4243  if(!(e[2].getRational().getInt() >=0 ))
4244  throw ParserException("parameter must be an integer constant >= 0.\n"
4245  +e.toString());
4246  return newFixedConstWidthLeftShiftExpr(parseExpr(e[1]), e[2].getRational().getInt());
4247  break;
4248  case RIGHTSHIFT:
4249  if(!(e.arity() == 3))
4250  throw ParserException("TheoryBitvector::parseExprOp: RIGHTSHIFT"
4251  "kind should have exactly 2 arg:\n\n"
4252  + e.toString());
4253  if(!e[2].isRational() || !e[2].getRational().isInteger())
4254  throw ParserException("RIGHTSHIFT must have an integer constant as its "
4255  "2nd argument:\n\n"
4256  +e.toString());
4257  if(!(e[2].getRational().getInt() >=0 ))
4258  throw ParserException("parameter must be an integer constant >= 0.\n"
4259  +e.toString());
4260  return newFixedRightShiftExpr(parseExpr(e[1]), e[2].getRational().getInt());
4261  break;
4262  // BVSHL, BVLSHR, BVASHR handled with arith operators below
4263  case SX:
4264  // smtlib format interprets the integer argument as the number of bits to
4265  // extend, while CVC format interprets it as the new total size.
4266  // The smtlib parser inserts an extra argument "_smtlib" for this operator
4267  // so that we can distinguish the two cases here.
4268  if (e.arity() == 4 &&
4269  e[1].getKind() == ID &&
4270  e[1][0].getString() == "_smtlib") {
4271  if(!e[2].isRational() || !e[2].getRational().isInteger())
4272  throw ParserException("sign_extend must have an integer constant as its"
4273  " 1st argument:\n\n"
4274  +e.toString());
4275  if(!(e[2].getRational().getInt() >=0 ))
4276  throw ParserException("sign_extend must have an integer constant as its"
4277  " 1st argument >= 0:\n\n"
4278  +e.toString());
4279  Expr e3 = parseExpr(e[3]);
4280  return newSXExpr(e3, BVSize(e3) + e[2].getRational().getInt());
4281  }
4282  if(!(e.arity() == 3))
4283  throw ParserException("TheoryBitvector::parseExprOp: SX"
4284  "kind should have exactly 2 arg:\n\n"
4285  + e.toString());
4286  if(!e[2].isRational() || !e[2].getRational().isInteger())
4287  throw ParserException("SX must have an integer constant as its"
4288  " 2nd argument:\n\n"
4289  +e.toString());
4290  if(!(e[2].getRational().getInt() >=0 ))
4291  throw ParserException("SX must have an integer constant as its"
4292  " 2nd argument >= 0:\n\n"
4293  +e.toString());
4294  return newSXExpr(parseExpr(e[1]), e[2].getRational().getInt());
4295  break;
4296  case BVROTL:
4297  case BVROTR:
4298  case BVREPEAT:
4299  case BVZEROEXTEND:
4300  if(!(e.arity() == 3))
4301  throw ParserException("TheoryBitvector::parseExprOp:"
4302  "kind should have exactly 2 arg:\n\n"
4303  + e.toString());
4304  if(!e[1].isRational() || !e[1].getRational().isInteger())
4305  throw ParserException("BVIndexExpr must have an integer constant as its"
4306  " 1st argument:\n\n"
4307  +e.toString());
4308  if (kind == BVREPEAT && !(e[1].getRational().getInt() >0 ))
4309  throw ParserException("BVREPEAT must have an integer constant as its"
4310  " 1st argument > 0:\n\n"
4311  +e.toString());
4312  if(!(e[1].getRational().getInt() >=0 ))
4313  throw ParserException("BVIndexExpr must have an integer constant as its"
4314  " 1st argument >= 0:\n\n"
4315  +e.toString());
4316  return newBVIndexExpr(kind, parseExpr(e[2]), e[1].getRational().getInt());
4317  break;
4318 
4319  case BVAND: {
4320  if(!(e.arity() >= 3))
4321  throw ParserException("TheoryBitvector::parseExprOp: BVAND "
4322  "kind should have at least 2 arg:\n\n"
4323  + e.toString());
4324  vector<Expr> kids;
4325  for(int i=1, iend=e.arity(); i<iend; ++i)
4326  kids.push_back(parseExpr(e[i]));
4327  return newBVAndExpr(kids);
4328  break;
4329  }
4330  case BVOR: {
4331  if(!(e.arity() >= 3))
4332  throw ParserException("TheoryBitvector::parseExprOp: BVOR "
4333  "kind should have at least 2 arg:\n\n"
4334  + e.toString());
4335  vector<Expr> kids;
4336  for(int i=1, iend=e.arity(); i<iend; ++i)
4337  kids.push_back(parseExpr(e[i]));
4338  return newBVOrExpr(kids);
4339  break;
4340  }
4341  case BVXOR: {
4342  if(!(e.arity() == 3))
4343  throw ParserException("TheoryBitvector::parseExprOp: BVXOR "
4344  "kind should have exactly 2 arg:\n\n"
4345  + e.toString());
4346  return newBVXorExpr(parseExpr(e[1]), parseExpr(e[2]));
4347  break;
4348  }
4349  case BVXNOR: {
4350  if(!(e.arity() == 3))
4351  throw ParserException("TheoryBitvector::parseExprOp: BVXNOR"
4352  "kind should have exactly 2 arg:\n\n"
4353  + e.toString());
4354  return newBVXnorExpr(parseExpr(e[1]), parseExpr(e[2]));
4355  break;
4356  }
4357  case BVNEG:
4358  if(!(e.arity() == 2))
4359  throw ParserException("TheoryBitvector::parseExprOp: BVNEG"
4360  "kind should have exactly 1 arg:\n\n"
4361  + e.toString());
4362  return newBVNegExpr(parseExpr(e[1]));
4363  break;
4364  case BVNAND:
4365  if(!(e.arity() == 3))
4366  throw ParserException("TheoryBitvector::parseExprOp: BVNAND"
4367  "kind should have exactly 2 arg:\n\n"
4368  + e.toString());
4369  return newBVNandExpr(parseExpr(e[1]), parseExpr(e[2]));
4370  break;
4371  case BVNOR:
4372  if(!(e.arity() == 3))
4373  throw ParserException("TheoryBitvector::parseExprOp: BVNOR"
4374  "kind should have exactly 2 arg:\n\n"
4375  + e.toString());
4376  return newBVNorExpr(parseExpr(e[1]), parseExpr(e[2]));
4377  break;
4378  case BVCOMP: {
4379  if(!(e.arity() == 3))
4380  throw ParserException("TheoryBitvector::parseExprOp: BVXNOR"
4381  "kind should have exactly 2 arg:\n\n"
4382  + e.toString());
4383  return newBVCompExpr(parseExpr(e[1]), parseExpr(e[2]));
4384  break;
4385  }
4386 
4387  case BVUMINUS:
4388  if(!(e.arity() == 2))
4389  throw ParserException("TheoryBitvector::parseExprOp: BVUMINUS"
4390  "kind should have exactly 1 arg:\n\n"
4391  + e.toString());
4392  return newBVUminusExpr(parseExpr(e[1]));
4393  break;
4394  case BVPLUS: {
4395  vector<Expr> k;
4396  Expr::iterator i = e.begin(), iend=e.end();
4397  if (!e[1].isRational()) {
4398  int maxsize = 0;
4399  Expr child;
4400  // Parse the kids of e and push them into the vector 'k'
4401  for(++i; i!=iend; ++i) {
4402  child = parseExpr(*i);
4403  if (getBaseType(child).getExpr().getOpKind() != BITVECTOR) {
4404  throw ParserException("BVPLUS argument is not bitvector");
4405  }
4406  if (BVSize(child) > maxsize) maxsize = BVSize(child);
4407  k.push_back(child);
4408  }
4409  if (e.arity() == 1) return k[0];
4410  return newBVPlusPadExpr(maxsize, k);
4411  }
4412  else {
4413  if(!(e.arity() >= 4))
4414  throw ParserException("Expected at least 3 args in BVPLUS:\n\n"
4415  +e.toString());
4416  if(!e[1].isRational() || !e[1].getRational().isInteger())
4417  throw ParserException
4418  ("Expected integer constant in BVPLUS:\n\n"
4419  +e.toString());
4420  if(!(e[1].getRational().getInt() > 0))
4421  throw ParserException("parameter must be an integer constant > 0.\n"
4422  +e.toString());
4423  // Skip first two elements of the vector of kids in 'e'.
4424  // The first element is the kind, and the second is the
4425  // numOfBits of the bvplus operator.
4426  ++i;++i;
4427  Expr child;
4428  // Parse the kids of e and push them into the vector 'k'
4429  for(; i!=iend; ++i) {
4430  child = parseExpr(*i);
4431  if (getBaseType(child).getExpr().getOpKind() != BITVECTOR) {
4432  throw ParserException("BVPLUS argument is not bitvector");
4433  }
4434  k.push_back(child);
4435  }
4436  return newBVPlusPadExpr(e[1].getRational().getInt(), k);
4437  }
4438  break;
4439  }
4440  case BVSUB: {
4441  if (e.arity() == 3) {
4442  Expr summand1 = parseExpr(e[1]);
4443  Expr summand2 = parseExpr(e[2]);
4444  if (getBaseType(summand1).getExpr().getOpKind() != BITVECTOR
4445  || getBaseType(summand2).getExpr().getOpKind() != BITVECTOR) {
4446  throw ParserException("BVSUB argument is not bitvector");
4447  }
4448  if (BVSize(summand1) != BVSize(summand2)) {
4449  throw ParserException("BVSUB: expected same sized arguments"
4450  +e.toString());
4451  }
4452  return newBVSubExpr(summand1, summand2);
4453  }
4454  else if (e.arity() != 4)
4455  throw ParserException("BVSUB: wrong number of arguments:\n\n"
4456  +e.toString());
4457  if (!e[1].isRational() || !e[1].getRational().isInteger())
4458  throw ParserException("BVSUB: expected an integer constant as "
4459  "first argument:\n\n"
4460  +e.toString());
4461  if (!(e[1].getRational().getInt() > 0))
4462  throw ParserException("parameter must be an integer constant > 0.\n"
4463  +e.toString());
4464  int bvsublength = e[1].getRational().getInt();
4465  Expr summand1 = parseExpr(e[2]);
4466  Expr summand2 = parseExpr(e[3]);
4467  if (getBaseType(summand1).getExpr().getOpKind() != BITVECTOR
4468  || getBaseType(summand2).getExpr().getOpKind() != BITVECTOR) {
4469  throw ParserException("BVSUB argument is not bitvector");
4470  }
4471  summand1 = pad(bvsublength, summand1);
4472  summand2 = pad(bvsublength, summand2);
4473  return newBVSubExpr(summand1, summand2);
4474  break;
4475  }
4476  case BVMULT: {
4477  vector<Expr> k;
4478  Expr::iterator i = e.begin(), iend=e.end();
4479  if (!e[1].isRational()) {
4480  if (e.arity() != 3) {
4481  throw ParserException("TheoryBitvector::parseExprOp: BVMULT: "
4482  "expected exactly 2 args:\n\n"
4483  + e.toString());
4484  }
4485  int maxsize = 0;
4486  Expr child;
4487  // Parse the kids of e and push them into the vector 'k'
4488  for(++i; i!=iend; ++i) {
4489  child = parseExpr(*i);
4490  if (getBaseType(child).getExpr().getOpKind() != BITVECTOR) {
4491  throw ParserException("BVMULT argument is not bitvector");
4492  }
4493  if (BVSize(child) > maxsize) maxsize = BVSize(child);
4494  k.push_back(child);
4495  }
4496  if (e.arity() == 1) return k[0];
4497  return newBVMultPadExpr(maxsize, k[0], k[1]);
4498  }
4499  if(!(e.arity() == 4))
4500  throw ParserException("TheoryBitvector::parseExprOp: BVMULT: "
4501  "expected exactly 3 args:\n\n"
4502  + e.toString());
4503  if(!e[1].isRational() || !e[1].getRational().isInteger())
4504  throw ParserException("BVMULT: expected integer constant"
4505  "as first argument:\n\n"
4506  +e.toString());
4507  if(!(e[1].getRational().getInt() > 0))
4508  throw ParserException("parameter must be an integer constant > 0.\n"
4509  +e.toString());
4510  Expr a = parseExpr(e[2]);
4511  Expr b = parseExpr(e[3]);
4512  if (getBaseType(a).getExpr().getOpKind() != BITVECTOR
4513  || getBaseType(b).getExpr().getOpKind() != BITVECTOR) {
4514  throw ParserException("BVMULT argument is not bitvector");
4515  }
4516  return newBVMultPadExpr(e[1].getRational().getInt(),a,b);
4517  break;
4518  }
4519  case BVUDIV:
4520  case BVSDIV:
4521  case BVUREM:
4522  case BVSREM:
4523  case BVSMOD:
4524  case BVSHL:
4525  case BVASHR:
4526  case BVLSHR: {
4527  if(!(e.arity() == 3))
4528  throw ParserException("TheoryBitvector::parseExprOp:"
4529  "kind should have exactly 2 args:\n\n"
4530  + e.toString());
4531  Expr e1 = parseExpr(e[1]);
4532  Expr e2 = parseExpr(e[2]);
4533  if (e1.getType().getExpr().getOpKind() != BITVECTOR ||
4534  e2.getType().getExpr().getOpKind() != BITVECTOR)
4535  throw ParserException("TheoryBitvector::parseExprOp:"
4536  "Expected bitvector arguments:\n\n"
4537  + e.toString());
4538  if (BVSize(e1) != BVSize(e2))
4539  throw ParserException("TheoryBitvector::parseExprOp:"
4540  "Expected bitvectors of same size:\n\n"
4541  + e.toString());
4542  if (kind == BVSHL) {
4543  if (e2.getKind() == BVCONST)
4545  computeBVConst(e2).getInt());
4546  }
4547  else if (kind == BVLSHR) {
4548  if (e2.getKind() == BVCONST)
4549  return newFixedRightShiftExpr(e1, computeBVConst(e2).getInt());
4550  }
4551  return Expr(kind, e1, e2);
4552  break;
4553  }
4554 
4555  case BVLT:
4556  if(!(e.arity() == 3))
4557  throw ParserException("TheoryBitvector::parseExprOp: BVLT"
4558  "kind should have exactly 2 arg:\n\n"
4559  + e.toString());
4560  return newBVLTExpr(parseExpr(e[1]),parseExpr(e[2]));
4561  break;
4562  case BVLE:
4563  if(!(e.arity() == 3))
4564  throw ParserException("TheoryBitvector::parseExprOp: BVLE"
4565  "kind should have exactly 2 arg:\n\n"
4566  + e.toString());
4567  return newBVLEExpr(parseExpr(e[1]),parseExpr(e[2]));
4568  break;
4569  case BVGT:
4570  if(!(e.arity() == 3))
4571  throw ParserException("TheoryBitvector::parseExprOp: BVGT"
4572  "kind should have exactly 2 arg:\n\n"
4573  + e.toString());
4574  return newBVLTExpr(parseExpr(e[2]),parseExpr(e[1]));
4575  break;
4576  case BVGE:
4577  if(!(e.arity() == 3))
4578  throw ParserException("TheoryBitvector::parseExprOp: BVGE"
4579  "kind should have exactly 2 arg:\n\n"
4580  + e.toString());
4581  return newBVLEExpr(parseExpr(e[2]),parseExpr(e[1]));
4582  break;
4583  case BVSLT:
4584  if(!(e.arity() == 3))
4585  throw ParserException("TheoryBitvector::parseExprOp: BVLT"
4586  "kind should have exactly 2 arg:\n\n"
4587  + e.toString());
4588  return newBVSLTExpr(parseExpr(e[1]),parseExpr(e[2]));
4589  break;
4590  case BVSLE:
4591  if(!(e.arity() == 3))
4592  throw ParserException("TheoryBitvector::parseExprOp: BVLE"
4593  "kind should have exactly 2 arg:\n\n"
4594  + e.toString());
4595  return newBVSLEExpr(parseExpr(e[1]),parseExpr(e[2]));
4596  break;
4597  case BVSGT:
4598  if(!(e.arity() == 3))
4599  throw ParserException("TheoryBitvector::parseExprOp: BVGT"
4600  "kind should have exactly 2 arg:\n\n"
4601  + e.toString());
4602  return newBVSLTExpr(parseExpr(e[2]),parseExpr(e[1]));
4603  break;
4604  case BVSGE:
4605  if(!(e.arity() == 3))
4606  throw ParserException("TheoryBitvector::parseExprOp: BVGE"
4607  "kind should have exactly 2 arg:\n\n"
4608  + e.toString());
4609  return newBVSLEExpr(parseExpr(e[2]),parseExpr(e[1]));
4610  break;
4611 
4612  case INTTOBV:
4613  throw ParserException("INTTOBV not implemented");
4614  break;
4615  case BVTOINT:
4616  throw ParserException("BVTOINT not implemented");
4617  break;
4618 
4619  case BVTYPEPRED:
4620  throw ParserException("BVTYPEPRED is used internally");
4621  break;
4622 
4623  default:
4624  FatalAssert(false,
4625  "TheoryBitvector::parseExprOp: unrecognized input operator"
4626  +e.toString());
4627  break;
4628  }
4629  return e;
4630 }
4631 
4632 
4633 ///////////////////////////////////////////////////////////////////////////////
4634 //helper functions
4635 ///////////////////////////////////////////////////////////////////////////////
4636 
4637 
4639 {
4640  DebugAssert(bvLength > 0,
4641  "TheoryBitvector::newBitvectorTypeExpr:\n"
4642  "len of a BV must be a positive integer:\n bvlength = "+
4643  int2string(bvLength));
4644  if (bvLength > d_maxLength)
4645  d_maxLength = bvLength;
4646  return Expr(BITVECTOR, getEM()->newRatExpr(bvLength));
4647 }
4648 
4649 
4651 {
4652  return Expr(Expr(BVTYPEPRED, t.getExpr()).mkOp(), e);
4653 }
4654 
4655 
4657 {
4659  BITVECTOR == t2.getType().getExpr().getOpKind(),
4660  "TheoryBitvector::newBVAndExpr:"
4661  "inputs must have type BITVECTOR:\n t1 = " +
4662  t1.toString() + "\n t2 = " +t2.toString());
4663  DebugAssert(BVSize(t1) == BVSize(t2),
4664  "TheoryBitvector::bitwise operator"
4665  "inputs must have same length:\n t1 = " + t1.toString()
4666  + "\n t2 = " + t2.toString());
4667  return Expr(CVC3::BVAND, t1, t2);
4668 }
4669 
4670 
4671 Expr TheoryBitvector::newBVAndExpr(const vector<Expr>& kids)
4672 {
4673  DebugAssert(kids.size() >= 2,
4674  "TheoryBitvector::newBVAndExpr:"
4675  "# of subterms must be at least 2");
4676  for(unsigned int i=0; i<kids.size(); ++i) {
4677  DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
4678  "TheoryBitvector::newBVAndExpr:"
4679  "inputs must have type BITVECTOR:\n t1 = " +
4680  kids[i].toString());
4681  if(i < kids.size()-1) {
4682  DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]),
4683  "TheoryBitvector::bitwise operator"
4684  "inputs must have same length:\n t1 = " + kids[i].toString()
4685  + "\n t2 = " + kids[i+1].toString());
4686  }
4687  }
4688  return Expr(CVC3::BVAND, kids, getEM());
4689 }
4690 
4691 
4693 {
4695  BITVECTOR == t2.getType().getExpr().getOpKind(),
4696  "TheoryBitvector::newBVOrExpr: "
4697  "inputs must have type BITVECTOR:\n t1 = " +
4698  t1.toString() + "\n t2 = " +t2.toString());
4699  DebugAssert(BVSize(t1) == BVSize(t2),
4700  "TheoryBitvector::bitwise OR operator: "
4701  "inputs must have same length:\n t1 = " + t1.toString()
4702  + "\n t2 = " + t2.toString());
4703  return Expr(CVC3::BVOR, t1, t2);
4704 }
4705 
4706 
4707 Expr TheoryBitvector::newBVOrExpr(const vector<Expr>& kids)
4708 {
4709  DebugAssert(kids.size() >= 2,
4710  "TheoryBitvector::newBVOrExpr: "
4711  "# of subterms must be at least 2");
4712  for(unsigned int i=0; i<kids.size(); ++i) {
4713  DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
4714  "TheoryBitvector::newBVOrExpr: "
4715  "inputs must have type BITVECTOR:\n t1 = " +
4716  kids[i].toString());
4717  if(i < kids.size()-1) {
4718  DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]),
4719  "TheoryBitvector::bitwise operator"
4720  "inputs must have same length:\n t1 = " + kids[i].toString()
4721  + "\n t2 = " + kids[i+1].toString());
4722  }
4723  }
4724  return Expr(CVC3::BVOR, kids, getEM());
4725 }
4726 
4727 
4729 {
4731  BITVECTOR == t2.getType().getExpr().getOpKind(),
4732  "TheoryBitvector::newBVNandExpr:"
4733  "inputs must have type BITVECTOR:\n t1 = " +
4734  t1.toString() + "\n t2 = " +t2.toString());
4735  DebugAssert(BVSize(t1) == BVSize(t2),
4736  "TheoryBitvector::bitwise operator"
4737  "inputs must have same length:\n t1 = " + t1.toString()
4738  + "\n t2 = " + t2.toString());
4739  return Expr(CVC3::BVNAND, t1, t2);
4740 }
4741 
4742 
4744 {
4746  BITVECTOR == t2.getType().getExpr().getOpKind(),
4747  "TheoryBitvector::newBVNorExpr:"
4748  "inputs must have type BITVECTOR:\n t1 = " +
4749  t1.toString() + "\n t2 = " +t2.toString());
4750  DebugAssert(BVSize(t1) == BVSize(t2),
4751  "TheoryBitvector::bitwise operator"
4752  "inputs must have same length:\n t1 = " + t1.toString()
4753  + "\n t2 = " + t2.toString());
4754  return Expr(CVC3::BVNOR, t1, t2);
4755 }
4756 
4757 
4759 {
4761  BITVECTOR == t2.getType().getExpr().getOpKind(),
4762  "TheoryBitvector::newBVXorExpr:"
4763  "inputs must have type BITVECTOR:\n t1 = " +
4764  t1.toString() + "\n t2 = " +t2.toString());
4765  DebugAssert(BVSize(t1) == BVSize(t2),
4766  "TheoryBitvector::bitwise operator"
4767  "inputs must have same length:\n t1 = " + t1.toString()
4768  + "\n t2 = " + t2.toString());
4769  return Expr(CVC3::BVXOR, t1, t2);
4770 }
4771 
4772 
4773 Expr TheoryBitvector::newBVXorExpr(const vector<Expr>& kids)
4774 {
4775  DebugAssert(kids.size() >= 2,
4776  "TheoryBitvector::newBVXorExpr:"
4777  "# of subterms must be at least 2");
4778  for(unsigned int i=0; i<kids.size(); ++i) {
4779  DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
4780  "TheoryBitvector::newBVXorExpr:"
4781  "inputs must have type BITVECTOR:\n t1 = " +
4782  kids[i].toString());
4783  if(i < kids.size()-1) {
4784  DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]),
4785  "TheoryBitvector::bitwise operator"
4786  "inputs must have same length:\n t1 = " + kids[i].toString()
4787  + "\n t2 = " + kids[i+1].toString());
4788  }
4789  }
4790  return Expr(CVC3::BVXOR, kids, getEM());
4791 }
4792 
4793 
4795 {
4797  BITVECTOR == t2.getType().getExpr().getOpKind(),
4798  "TheoryBitvector::newBVXnorExpr:"
4799  "inputs must have type BITVECTOR:\n t1 = " +
4800  t1.toString() + "\n t2 = " +t2.toString());
4801  DebugAssert(BVSize(t1) == BVSize(t2),
4802  "TheoryBitvector::bitwise operator"
4803  "inputs must have same length:\n t1 = " + t1.toString()
4804  + "\n t2 = " + t2.toString());
4805  return Expr(CVC3::BVXNOR, t1, t2);
4806 }
4807 
4808 
4810 {
4812  BITVECTOR == t2.getType().getExpr().getOpKind(),
4813  "TheoryBitvector::newBVCompExpr:"
4814  "inputs must have type BITVECTOR:\n t1 = " +
4815  t1.toString() + "\n t2 = " +t2.toString());
4816  DebugAssert(BVSize(t1) == BVSize(t2),
4817  "TheoryBitvector::bitwise operator"
4818  "inputs must have same length:\n t1 = " + t1.toString()
4819  + "\n t2 = " + t2.toString());
4820  return Expr(CVC3::BVCOMP, t1, t2);
4821 }
4822 
4823 
4824 Expr TheoryBitvector::newBVXnorExpr(const vector<Expr>& kids)
4825 {
4826  DebugAssert(kids.size() >= 2,
4827  "TheoryBitvector::newBVXnorExpr:"
4828  "# of subterms must be at least 2");
4829  for(unsigned int i=0; i<kids.size(); ++i) {
4830  DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
4831  "TheoryBitvector::newBVXnorExpr:"
4832  "inputs must have type BITVECTOR:\n t1 = " +
4833  kids[i].toString());
4834  if(i < kids.size()-1) {
4835  DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]),
4836  "TheoryBitvector::bitwise operator"
4837  "inputs must have same length:\n t1 = " + kids[i].toString()
4838  + "\n t2 = " + kids[i+1].toString());
4839  }
4840  }
4841  return Expr(CVC3::BVXNOR, kids, getEM());
4842 }
4843 
4844 
4846 {
4848  BITVECTOR == t2.getType().getExpr().getOpKind(),
4849  "TheoryBitvector::newBVLTExpr:"
4850  "inputs must have type BITVECTOR:\n t1 = " +
4851  t1.toString() + "\n t2 = " +t2.toString());
4852  return Expr(CVC3::BVLT, t1, t2);
4853 }
4854 
4855 
4857 {
4859  BITVECTOR == t2.getType().getExpr().getOpKind(),
4860  "TheoryBitvector::newBVLEExpr:"
4861  "inputs must have type BITVECTOR:\n t1 = " +
4862  t1.toString() + "\n t2 = " +t2.toString());
4863  return Expr(CVC3::BVLE, t1, t2);
4864 }
4865 
4866 
4868 {
4869  DebugAssert(len >=0,
4870  " TheoryBitvector::newSXExpr:"
4871  "SX index must be a non-negative integer"+
4872  int2string(len));
4874  "TheoryBitvector::newSXExpr:"
4875  "inputs must have type BITVECTOR:\n t1 = " +
4876  t1.toString());
4877  if(len==0) return t1;
4878  return Expr(Expr(SX, getEM()->newRatExpr(len)).mkOp(), t1);
4879 }
4880 
4881 
4882 Expr TheoryBitvector::newBVIndexExpr(int kind, const Expr& t1, int len)
4883 {
4884  DebugAssert(kind != BVREPEAT || len > 0,
4885  "repeat requires index > 0");
4886  DebugAssert(len >=0,
4887  "TheoryBitvector::newBVIndexExpr:"
4888  "index must be a non-negative integer"+
4889  int2string(len));
4891  "TheoryBitvector::newBVIndexExpr:"
4892  "inputs must have type BITVECTOR:\n t1 = " +
4893  t1.toString());
4894  return Expr(Expr(kind, getEM()->newRatExpr(len)).mkOp(), t1);
4895 }
4896 
4897 
4899 {
4901  BITVECTOR == t2.getType().getExpr().getOpKind(),
4902  "TheoryBitvector::newBVSLTExpr:"
4903  "inputs must have type BITVECTOR:\n t1 = " +
4904  t1.toString() + "\n t2 = " +t2.toString());
4905  return Expr(CVC3::BVSLT, t1, t2);
4906 }
4907 
4908 
4910 {
4912  BITVECTOR == t2.getType().getExpr().getOpKind(),
4913  "TheoryBitvector::newBVSLEExpr:"
4914  "inputs must have type BITVECTOR:\n t1 = " +
4915  t1.toString() + "\n t2 = " +t2.toString());
4916  return Expr(CVC3::BVSLE, t1, t2);
4917 }
4918 
4919 
4921 {
4923  "TheoryBitvector::newBVNegExpr:"
4924  "inputs must have type BITVECTOR:\n t1 = " +
4925  t1.toString());
4926  return Expr(CVC3::BVNEG, t1);
4927 }
4928 
4929 
4931 {
4933  "TheoryBitvector::newBVNegExpr:"
4934  "inputs must have type BITVECTOR:\n t1 = " +
4935  t1.toString());
4936  return Expr(CVC3::BVUMINUS, t1);
4937 }
4938 
4939 
4941 {
4942  DebugAssert(index >=0,
4943  " TheoryBitvector::newBoolExtractExpr:"
4944  "bool_extract index must be a non-negative integer"+
4945  int2string(index));
4947  "TheoryBitvector::newBVBoolExtractExpr:"
4948  "inputs must have type BITVECTOR:\n t1 = " +
4949  t1.toString());
4950  return Expr(Expr(BOOLEXTRACT, getEM()->newRatExpr(index)).mkOp(), t1);
4951 }
4952 
4953 
4955 {
4956  DebugAssert(shiftLength >=0,
4957  " TheoryBitvector::newFixedleftshift:"
4958  "fixed_shift index must be a non-negative integer"+
4959  int2string(shiftLength));
4961  "TheoryBitvector::newBVFixedleftshiftExpr:"
4962  "inputs must have type BITVECTOR:\n t1 = " +
4963  t1.toString());
4964  return Expr(Expr(LEFTSHIFT, getEM()->newRatExpr(shiftLength)).mkOp(), t1);
4965 }
4966 
4967 
4969 {
4970  DebugAssert(shiftLength >=0,
4971  " TheoryBitvector::newFixedConstWidthLeftShift:"
4972  "fixed_shift index must be a non-negative integer"+
4973  int2string(shiftLength));
4975  "TheoryBitvector::newBVFixedleftshiftExpr:"
4976  "inputs must have type BITVECTOR:\n t1 = " +
4977  t1.toString());
4978  return Expr(Expr(CONST_WIDTH_LEFTSHIFT, getEM()->newRatExpr(shiftLength)).mkOp(), t1);
4979 }
4980 
4981 
4983 {
4984  DebugAssert(shiftLength >=0,
4985  " TheoryBitvector::newFixedRightShift:"
4986  "fixed_shift index must be a non-negative integer"+
4987  int2string(shiftLength));
4989  "TheoryBitvector::newBVFixedRightShiftExpr:"
4990  "inputs must have type BITVECTOR:\n t1 = " +
4991  t1.toString());
4992  if(shiftLength==0) return t1;
4993  return Expr(Expr(RIGHTSHIFT, getEM()->newRatExpr(shiftLength)).mkOp(), t1);
4994 }
4995 
4996 
4998 {
5000  BITVECTOR == t2.getType().getExpr().getOpKind(),
5001  "TheoryBitvector::newBVConcatExpr:"
5002  "inputs must have type BITVECTOR:\n t1 = " +
5003  t1.toString() + "\n t2 = " +t2.toString());
5004  return Expr(CONCAT, t1, t2);
5005 }
5006 
5007 
5009  const Expr& t3)
5010 {
5012  BITVECTOR == t2.getType().getExpr().getOpKind() &&
5013  BITVECTOR == t3.getType().getExpr().getOpKind(),
5014  "TheoryBitvector::newBVConcatExpr:"
5015  "inputs must have type BITVECTOR:\n t1 = " +
5016  t1.toString() +
5017  "\n t2 = " +t2.toString() +
5018  "\n t3 =" + t3.toString());
5019  return Expr(CONCAT, t1, t2, t3);
5020 }
5021 
5022 
5023 Expr TheoryBitvector::newConcatExpr(const vector<Expr>& kids)
5024 {
5025  DebugAssert(kids.size() >= 2,
5026  "TheoryBitvector::newBVConcatExpr:"
5027  "# of subterms must be at least 2");
5028  for(unsigned int i=0; i<kids.size(); ++i) {
5029  DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
5030  "TheoryBitvector::newBVConcatExpr:"
5031  "inputs must have type BITVECTOR:\n t1 = " +
5032  kids[i].toString());
5033  }
5034  return Expr(CONCAT, kids, getEM());
5035 }
5036 
5037 
5039  const Expr& t1, const Expr& t2)
5040 {
5041  DebugAssert(bvLength > 0,
5042  "TheoryBitvector::newBVmultExpr:"
5043  "bvLength must be an integer > 0: bvLength = " +
5044  int2string(bvLength));
5046  BITVECTOR == t2.getType().getExpr().getOpKind(),
5047  "TheoryBitvector::newBVmultExpr:"
5048  "inputs must have type BITVECTOR:\n t1 = " +
5049  t1.toString() + "\n t2 = " +t2.toString());
5050  DebugAssert(bvLength == BVSize(t1) &&
5051  bvLength == BVSize(t2), "Expected same length");
5052  return Expr(Expr(BVMULT, getEM()->newRatExpr(bvLength)).mkOp(), t1, t2);
5053 }
5054 
5055 
5056 Expr TheoryBitvector::newBVMultExpr(int bvLength, const vector<Expr>& kids)
5057 {
5058  DebugAssert(bvLength > 0,
5059  "TheoryBitvector::newBVmultExpr:"
5060  "bvLength must be an integer > 0: bvLength = " +
5061  int2string(bvLength));
5062  for(unsigned int i=0; i<kids.size(); ++i) {
5063  DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
5064  "TheoryBitvector::newBVPlusExpr:"
5065  "inputs must have type BITVECTOR:\n t1 = " +
5066  kids[i].toString());
5067  DebugAssert(BVSize(kids[i]) == bvLength, "Expected matching sizes");
5068  }
5069  return Expr(Expr(BVMULT, getEM()->newRatExpr(bvLength)).mkOp(), kids);
5070 }
5071 
5072 
5073 Expr TheoryBitvector::newBVMultPadExpr(int bvLength, const vector<Expr>& kids)
5074 {
5075  vector<Expr> newKids;
5076  for (unsigned i = 0; i < kids.size(); ++i) {
5077  newKids.push_back(pad(bvLength, kids[i]));
5078  }
5079  return newBVMultExpr(bvLength, newKids);
5080 }
5081 
5082 
5084  const Expr& t1, const Expr& t2)
5085 {
5086  return newBVMultExpr(bvLength, pad(bvLength, t1), pad(bvLength, t2));
5087 }
5088 
5090 {
5092  BITVECTOR == t2.getType().getExpr().getOpKind(),
5093  "TheoryBitvector::newBVUDivExpr:"
5094  "inputs must have type BITVECTOR:\n t1 = " +
5095  t1.toString() + "\n t2 = " +t2.toString());
5096  DebugAssert(BVSize(t2) == BVSize(t1), "Expected same length");
5097  return Expr(BVUDIV, t1, t2);
5098 }
5099 
5101 {
5103  BITVECTOR == t2.getType().getExpr().getOpKind(),
5104  "TheoryBitvector::newBVURemExpr:"
5105  "inputs must have type BITVECTOR:\n t1 = " +
5106  t1.toString() + "\n t2 = " +t2.toString());
5107  DebugAssert(BVSize(t2) == BVSize(t1), "Expected same length");
5108  return Expr(BVUREM, t1, t2);
5109 }
5110 
5112 {
5114  BITVECTOR == t2.getType().getExpr().getOpKind(),
5115  "TheoryBitvector::newBVSDivExpr:"
5116  "inputs must have type BITVECTOR:\n t1 = " +
5117  t1.toString() + "\n t2 = " +t2.toString());
5118  DebugAssert(BVSize(t1) == BVSize(t2), "Expected same length");
5119  return Expr(BVSDIV, t1, t2);
5120 }
5121 
5123 {
5125  BITVECTOR == t2.getType().getExpr().getOpKind(),
5126  "TheoryBitvector::newBVSRemExpr:"
5127  "inputs must have type BITVECTOR:\n t1 = " +
5128  t1.toString() + "\n t2 = " +t2.toString());
5129  DebugAssert(BVSize(t1) == BVSize(t2), "Expected same length");
5130  return Expr(BVSREM, t1, t2);
5131 }
5132 
5134 {
5136  BITVECTOR == t2.getType().getExpr().getOpKind(),
5137  "TheoryBitvector::newBVSModExpr:"
5138  "inputs must have type BITVECTOR:\n t1 = " +
5139  t1.toString() + "\n t2 = " +t2.toString());
5140  DebugAssert(BVSize(t1) == BVSize(t2), "Expected same length");
5141  return Expr(BVSMOD, t1, t2);
5142 }
5143 
5144 //! produces a string of 0's of length bvLength
5146 {
5147  DebugAssert(bvLength > 0,
5148  "TheoryBitvector::newBVZeroString:must be >= 0: "
5149  + int2string(bvLength));
5150  std::vector<bool> bits;
5151  for(int count=0; count < bvLength; count++) {
5152  bits.push_back(false);
5153  }
5154  return newBVConstExpr(bits);
5155 }
5156 
5157 
5158 //! produces a string of 1's of length bvLength
5160 {
5161  DebugAssert(bvLength > 0,
5162  "TheoryBitvector::newBVOneString:must be >= 0: "
5163  + int2string(bvLength));
5164  std::vector<bool> bits;
5165  for(int count=0; count < bvLength; count++) {
5166  bits.push_back(true);
5167  }
5168  return newBVConstExpr(bits);
5169 }
5170 
5171 
5172 Expr TheoryBitvector::newBVConstExpr(const vector<bool>& bits)
5173 {
5174  DebugAssert(bits.size() > 0,
5175  "TheoryBitvector::newBVConstExpr:"
5176  "size of bits should be > 0");
5177  BVConstExpr bv(getEM(), bits, d_bvConstExprIndex);
5178  return getEM()->newExpr(&bv);
5179 }
5180 
5181 
5183 {
5184  DebugAssert(r.isInteger(),
5185  "TheoryBitvector::newBVConstExpr: not an integer: "
5186  + r.toString());
5187  DebugAssert(bvLength > 0,
5188  "TheoryBitvector::newBVConstExpr: bvLength = "
5189  + int2string(bvLength));
5190  string s(r.toString(2));
5191  size_t strsize = s.size();
5192  size_t length = bvLength;
5193  Expr res;
5194  if(length > 0 && length != strsize) {
5195  //either (length > strsize) or (length < strsize)
5196  if(length < strsize) {
5197  s = s.substr((strsize-length), length);
5198  } else {
5199  string zeros("");
5200  for(size_t i=0, pad=length-strsize; i < pad; ++i)
5201  zeros += "0";
5202  s = zeros+s;
5203  }
5204 
5205  res = newBVConstExpr(s, 2);
5206  }
5207  else
5208  res = newBVConstExpr(s, 2);
5209 
5210  return res;
5211 }
5212 
5213 
5214 Expr TheoryBitvector::newBVConstExpr(const std::string& s, int base)
5215 {
5216  DebugAssert(s.size() > 0,
5217  "TheoryBitvector::newBVConstExpr:"
5218  "# of subterms must be at least 2");
5219  DebugAssert(base == 2 || base == 16,
5220  "TheoryBitvector::newBVConstExpr: base = "
5221  +int2string(base));
5222  //hexadecimal
5223  std::string str = s;
5224  if(16 == base) {
5225  Rational r(str, 16);
5226  return newBVConstExpr(r, str.size()*4);
5227  }
5228  else {
5229  BVConstExpr bv(getEM(), str, d_bvConstExprIndex);
5230  return getEM()->newExpr(&bv);
5231  }
5232 }
5233 
5234 
5235 Expr
5237 newBVExtractExpr(const Expr& e, int hi, int low)
5238 {
5239  DebugAssert(low>=0 && hi>=low,
5240  " TheoryBitvector::newBVExtractExpr: "
5241  "bad bv_extract indices: hi = "
5242  + int2string(hi)
5243  + ", low = "
5244  + int2string(low));
5245  if (e.getOpKind() == LEFTSHIFT &&
5246  hi == BVSize(e[0])-1 &&
5247  low == 0) {
5249  }
5251  "TheoryBitvector::newBVExtractExpr:"
5252  "inputs must have type BITVECTOR:\n e = " +
5253  e.toString());
5254  return Expr(Expr(EXTRACT,
5255  getEM()->newRatExpr(hi),
5256  getEM()->newRatExpr(low)).mkOp(), e);
5257 }
5258 
5259 
5261 {
5263  BITVECTOR == t2.getType().getExpr().getOpKind(),
5264  "TheoryBitvector::newBVSubExpr:"
5265  "inputs must have type BITVECTOR:\n t1 = " +
5266  t1.toString() + "\n t2 = " +t2.toString());
5267  DebugAssert(BVSize(t1) == BVSize(t2),
5268  "TheoryBitvector::newBVSubExpr"
5269  "inputs must have same length:\n t1 = " + t1.toString()
5270  + "\n t2 = " + t2.toString());
5271  return Expr(BVSUB, t1, t2);
5272 }
5273 
5274 
5275 Expr TheoryBitvector::newBVPlusExpr(int bvLength, const Expr& k1, const Expr& k2)
5276 {
5277  DebugAssert(bvLength > 0,
5278  " TheoryBitvector::newBVPlusExpr:"
5279  "bvplus length must be a positive integer: "+
5280  int2string(bvLength));
5282  "TheoryBitvector::newBVPlusExpr:"
5283  "inputs must have type BITVECTOR:\n t1 = " +
5284  k1.toString());
5285  DebugAssert(BVSize(k1) == bvLength, "Expected matching sizes");
5287  "TheoryBitvector::newBVPlusExpr:"
5288  "inputs must have type BITVECTOR:\n t1 = " +
5289  k2.toString());
5290  DebugAssert(BVSize(k2) == bvLength, "Expected matching sizes");
5291 
5292  return Expr(Expr(BVPLUS, getEM()->newRatExpr(bvLength)).mkOp(), k1, k2);
5293 }
5294 
5295 
5297  const vector<Expr>& k)
5298 {
5299  DebugAssert(bvLength > 0,
5300  " TheoryBitvector::newBVPlusExpr:"
5301  "bvplus length must be a positive integer: "+
5302  int2string(bvLength));
5303  DebugAssert(k.size() > 1,
5304  " TheoryBitvector::newBVPlusExpr:"
5305  " size of input vector must be greater than 0: ");
5306  for(unsigned int i=0; i<k.size(); ++i) {
5307  DebugAssert(BITVECTOR == k[i].getType().getExpr().getOpKind(),
5308  "TheoryBitvector::newBVPlusExpr:"
5309  "inputs must have type BITVECTOR:\n t1 = " +
5310  k[i].toString());
5311  DebugAssert(BVSize(k[i]) == bvLength, "Expected matching sizes");
5312  }
5313  return Expr(Expr(BVPLUS, getEM()->newRatExpr(bvLength)).mkOp(), k);
5314 }
5315 
5316 
5318  const vector<Expr>& k)
5319 {
5320  vector<Expr> newKids;
5321  for (unsigned i = 0; i < k.size(); ++i) {
5322  newKids.push_back(pad(bvLength, k[i]));
5323  }
5324  return newBVPlusExpr(bvLength, newKids);
5325 }
5326 
5327 
5328 // Accessors for expression parameters
5329 
5330 
5332 {
5333  DebugAssert(BITVECTOR == e.getKind(),
5334  "TheoryBitvector::getBitvectorTypeParam: wrong kind: " +
5335  e.toString());
5336  return e[0].getRational().getInt();
5337 }
5338 
5339 
5341 {
5342  DebugAssert(tp.getOpKind()==BVTYPEPRED && tp.isApply(),
5343  "TheoryBitvector::getTypePredType:\n tp = "+tp.toString());
5344  return Type(tp.getOpExpr()[0]);
5345 }
5346 
5347 
5349 {
5351  "TheoryBitvector::getTypePredType:\n tp = "+tp.toString());
5352  return tp[0];
5353 }
5354 
5355 
5357 {
5358  DebugAssert(BOOLEXTRACT == e.getOpKind() && e.isApply(),
5359  "TheoryBitvector::getBoolExtractIndex: wrong kind" +
5360  e.toString());
5361  return e.getOpExpr()[0].getRational().getInt();
5362 }
5363 
5364 
5366 {
5367  DebugAssert(SX == e.getOpKind() && e.isApply(),
5368  "TheoryBitvector::getSXIndex: wrong kind\n"+e.toString());
5369  return e.getOpExpr()[0].getRational().getInt();
5370 }
5371 
5372 
5374 {
5375  DebugAssert(e.isApply() &&
5376  (e.getOpKind() == BVREPEAT ||
5377  e.getOpKind() == BVROTL ||
5378  e.getOpKind() == BVROTR ||
5379  e.getOpKind() == BVZEROEXTEND),
5380  "TheoryBitvector::getBVIndex: wrong kind\n"+e.toString());
5381  return e.getOpExpr()[0].getRational().getInt();
5382 }
5383 
5384 
5386 {
5387  DebugAssert(e.isApply() &&
5388  (LEFTSHIFT == e.getOpKind() ||
5390  "TheoryBitvector::getFixedLeftShiftParam: wrong kind" +
5391  e.toString());
5392  return e.getOpExpr()[0].getRational().getInt();
5393 }
5394 
5395 
5397 {
5398  DebugAssert(RIGHTSHIFT == e.getOpKind() && e.isApply(),
5399  "TheoryBitvector::getFixedRightShiftParam: wrong kind" +
5400  e.toString());
5401  return e.getOpExpr()[0].getRational().getInt();
5402 }
5403 
5404 
5406 {
5407  DebugAssert(EXTRACT == e.getOpKind() && e.isApply(),
5408  "TheoryBitvector::getExtractLow: wrong kind" +
5409  e.toString());
5410  return e.getOpExpr()[1].getRational().getInt();
5411 }
5412 
5413 
5415 {
5416  DebugAssert(EXTRACT == e.getOpKind() && e.isApply(),
5417  "TheoryBitvector::getExtractHi: wrong kind" +
5418  e.toString());
5419  return e.getOpExpr()[0].getRational().getInt();
5420 }
5421 
5422 
5424 {
5425  DebugAssert(BVPLUS == e.getOpKind() && e.isApply(),
5426  "TheoryBitvector::getBVPlusParam: wrong kind" +
5427  e.toString(AST_LANG));
5428  return e.getOpExpr()[0].getRational().getInt();
5429 }
5430 
5432 {
5433  DebugAssert(BVMULT == e.getOpKind() && e.isApply(),
5434  "TheoryBitvector::getBVMultParam: wrong kind " +
5435  e.toString(AST_LANG));
5436  return e.getOpExpr()[0].getRational().getInt();
5437 }
5438 
5440 {
5441  DebugAssert(BVCONST == e.getKind(), "getBVConstSize called on non-bvconst");
5442  const BVConstExpr* bvc = dynamic_cast<const BVConstExpr*>(e.getExprValue());
5443  DebugAssert(bvc, "getBVConstSize: cast failed");
5444  return bvc->size();
5445 }
5446 
5447 
5449 {
5450  DebugAssert(BVCONST == e.getKind(), "getBVConstSize called on non-bvconst");
5451  const BVConstExpr* bvc = dynamic_cast<const BVConstExpr*>(e.getExprValue());
5452  DebugAssert(bvc, "getBVConstSize: cast failed");
5453  return bvc->getValue(i);
5454 }
5455 
5456 
5457 // as newBVConstExpr can not give the BV expr of a negative rational,
5458 // I use this wrapper to do that
5460 {
5461  if( c > 0)
5462  return newBVConstExpr( c, bv_size);
5463  else
5464  {
5465  c = -c;
5466  Expr tmp = newBVConstExpr( c, bv_size);
5467  Rational neg_tmp = computeNegBVConst( tmp );
5468  return newBVConstExpr( neg_tmp, bv_size );
5469  }
5470 }
5471 
5472 
5473 // Computes the integer value of a bitvector constant
5475 {
5476  DebugAssert(BVCONST == e.getKind(),
5477  "TheoryBitvector::computeBVConst:"
5478  "input must be a BITVECTOR CONST: " + e.toString());
5479  if(*d_bv32Flag) {
5480  int c(0);
5481  for(int j=(int)getBVConstSize(e)-1; j>=0; j--)
5482  c = 2*c + getBVConstValue(e, j) ? 1 : 0;
5483  Rational d(c);
5484  return d;
5485  } else {
5486  Rational c(0);
5487  for(int j=(int)getBVConstSize(e)-1; j>=0; j--)
5488  c = 2*c + (getBVConstValue(e, j) ? Rational(1) : Rational(0));
5489  return c;
5490  }
5491 }
5492 
5493 
5494 // Computes the integer value of ~c+1
5496 {
5497  DebugAssert(BVCONST == e.getKind(),
5498  "TheoryBitvector::computeBVConst:"
5499  "input must be a BITVECTOR CONST: " + e.toString());
5500  if(*d_bv32Flag) {
5501  int c(0);
5502  for(int j=(int)getBVConstSize(e)-1; j>=0; j--)
5503  c = 2*c + getBVConstValue(e, j) ? 0 : 1;
5504  Rational d(c+1);
5505  return d;
5506  } else {
5507  Rational c(0);
5508  for(int j=(int)getBVConstSize(e)-1; j>=0; j--)
5509  c = 2*c + (getBVConstValue(e, j) ? Rational(0) : Rational(1));
5510  return c+1;
5511  }
5512 }
5513 
5514 
5515 //////////////////////////////////////////////////////////////////////
5516 // class BVConstExpr methods
5517 /////////////////////////////////////////////////////////////////////
5518 
5519 
5520 //! Constructor
5521 BVConstExpr::BVConstExpr(ExprManager* em, std::string bvconst,
5522  size_t mmIndex, ExprIndex idx)
5523  : ExprValue(em, BVCONST, idx), d_MMIndex(mmIndex)
5524 {
5525  std::string::reverse_iterator i = bvconst.rbegin();
5526  std::string::reverse_iterator iend = bvconst.rend();
5527  DebugAssert(bvconst.size() > 0,
5528  "TheoryBitvector::newBVConstExpr:"
5529  "# of subterms must be at least 2");
5530 
5531  for(;i != iend; ++i) {
5532  TRACE("bitvector", "BVConstExpr: bit ", *i, "");
5533  if('0' == *i)
5534  d_bvconst.push_back(false);
5535  else {
5536  if('1' == *i)
5537  d_bvconst.push_back(true);
5538  else
5539  DebugAssert(false, "BVConstExpr: bad binary bit-vector: "
5540  + bvconst);
5541  }
5542  }
5543  TRACE("bitvector", "BVConstExpr: #bits ", d_bvconst.size(), "");
5544 }
5545 
5546 
5547 BVConstExpr::BVConstExpr(ExprManager* em, std::vector<bool> bvconst,
5548  size_t mmIndex, ExprIndex idx)
5549  : ExprValue(em, BVCONST, idx), d_bvconst(bvconst), d_MMIndex(mmIndex)
5550 {
5551  TRACE("bitvector", "BVConstExpr(vector<bool>): arg. size = ", bvconst.size(),
5552  ", d_bvconst.size = "+int2string(d_bvconst.size()));
5553 }
5554 
5555 
5557 {
5558  std::vector<bool>::const_iterator i = d_bvconst.begin();
5559  std::vector<bool>::const_iterator iend = d_bvconst.end();
5560  size_t hash_value = 0;
5561  hash_value = ExprValue::hash(BVCONST);
5562  for (;i != iend; i++)
5563  if(*i)
5564  hash_value = PRIME*hash_value + HASH_VALUE_ONE;
5565  else
5566  hash_value = PRIME*hash_value + HASH_VALUE_ZERO;
5567  return hash_value;
5568 }
5569 
5571 {
5572  // inline recursive computation for deeply nested bitvector Exprs
5573 
5574  vector<Expr> operatorStack;
5575  vector<Expr> operandStack;
5576  vector<int> childStack;
5577  Expr e2, tcc;
5578 
5579  operatorStack.push_back(e);
5580  childStack.push_back(0);
5581 
5582  while (!operatorStack.empty()) {
5583  DebugAssert(operatorStack.size() == childStack.size(), "Invariant violated");
5584 
5585  if (childStack.back() < operatorStack.back().arity()) {
5586 
5587  e2 = operatorStack.back()[childStack.back()++];
5588 
5589  if (e2.isVar()) {
5590  operandStack.push_back(trueExpr());
5591  }
5592  else {
5593  ExprMap<Expr>::iterator itccCache = theoryCore()->tccCache().find(e2);
5594  if (itccCache != theoryCore()->tccCache().end()) {
5595  operandStack.push_back((*itccCache).second);
5596  }
5597  else if (theoryOf(e2) == this) {
5598  if (e2.arity() == 0) {
5599  operandStack.push_back(trueExpr());
5600  }
5601  else {
5602  operatorStack.push_back(e2);
5603  childStack.push_back(0);
5604  }
5605  }
5606  else {
5607  operandStack.push_back(getTCC(e2));
5608  }
5609  }
5610  }
5611  else {
5612  e2 = operatorStack.back();
5613  operatorStack.pop_back();
5614  childStack.pop_back();
5615  vector<Expr> children;
5616  vector<Expr>::iterator childStart = operandStack.end() - (e2.arity());
5617  children.insert(children.begin(), childStart, operandStack.end());
5618  operandStack.erase(childStart, operandStack.end());
5619  tcc = (children.size() == 0) ? trueExpr() :
5620  (children.size() == 1) ? children[0] :
5621  getCommonRules()->rewriteAnd(andExpr(children)).getRHS();
5622  switch(e2.getKind()) {
5623  case BVUDIV:
5624  case BVSDIV:
5625  case BVUREM:
5626  case BVSREM:
5627  case BVSMOD: {
5628  DebugAssert(e2.arity() == 2, "");
5629  int size = BVSize(e2);
5630  tcc = getCommonRules()->rewriteAnd(tcc.andExpr(!(e2[1].eqExpr(newBVZeroString(size))))).getRHS();
5631  break;
5632  }
5633  default:
5634  break;
5635  }
5636  operandStack.push_back(tcc);
5637  theoryCore()->tccCache()[e2] = tcc;
5638  }
5639  }
5640  DebugAssert(childStack.empty(), "Invariant violated");
5641  DebugAssert(operandStack.size() == 1, "Expected single operand left");
5642  return operandStack.back();
5643 }