CVC3  2.4.1
bitvector_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file bitvector_theorem_producer.h
4  * \brief TRUSTED implementation of bitvector proof rules
5  *
6  * Author: Vijay Ganesh
7  *
8  * Created: Wed May 5 16:10:28 PST 2004
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__bitvector_theorem_producer_h_
23 #define _cvc3__bitvector_theorem_producer_h_
24 
25 #include "bitvector_proof_rules.h"
26 #include "theorem_producer.h"
27 
28 namespace CVC3 {
29 
30  class TheoryBitvector;
31 
32  /*! @brief This class implements proof rules for bitvector
33  * normalizers (concatenation normal form, bvplus normal form),
34  * bitblaster rules, other relevant rewrite rules for bv arithmetic
35  * and word-level operators
36  */
37  /*!
38  Author: Vijay Ganesh, May-August, 2004
39 
40  */
42  public BitvectorProofRules, public TheoremProducer {
43  private:
44  TheoryBitvector* d_theoryBitvector; //! instance of bitvector DP
45  //! Constant 1-bit bit-vector 0bin0
47  //! Constant 1-bit bit-vector 0bin1
49  //! Return cached constant 0bin0
50  const Expr& bvZero() const { return d_bvZero; }
51  //! Return cached constant 0bin1
52  const Expr& bvOne() const { return d_bvOne; }
53 
54  //! Collect all of: a*x1+b*x1 + c*x2-x2 + d*x3 + ~x3 + ~x4 +e into
55  //! (a+b, x1) , (c-1 , x2), (d-1, x3), (-1, x4) and the constant e-2.
56  //! The constant is calculated from the formula -x = ~x+1 (or -x-1=~x).
57  void collectLikeTermsOfPlus(const Expr& e,
58  ExprMap<Rational> & likeTerms,
59  Rational & plusConstant);
60 
61  //! Collect a single coefficient*var pair into likeTerms.
62  //! Update the counter of likeTerms[var] += coefficient.
63  //! Potentially update the constant additive plusConstant.
64  void collectOneTermOfPlus(const Rational & coefficient,
65  const Expr& var,
66  ExprMap<Rational> & likeTerms,
67  Rational & plusConstant);
68 
69  //! Create a vector which will form the next PVPLUS.
70  //! Use the colleciton of likeTerms, and the constant additive plusConstant
71  void createNewPlusCollection(const Expr & e,
72  const ExprMap<Rational> & likeTerms,
73  Rational & plusConstant,
74  std::vector<Expr> & result);
75 
76  //! Create expression by applying plus to all elements.
77  //! All elements should be normalized and ready.
78  //! If there are too few elements, a non BVPLUS expression will be created.
79  Expr sumNormalizedElements(int bvplusLength,
80  const std::vector<Expr>& elements);
81 
82  void getPlusTerms(const Expr& e, Rational& known_term, ExprMap<Rational>& sumHashMap);
83  Expr buildPlusTerm(int bv_size, Rational& known_term, ExprMap<Rational>& sumHashMap);
84  Expr chopConcat(int bv_size, Rational c, std::vector<Expr>& concatKids);
85  bool okToSplit(const Expr& e);
86 
87  public:
88  //! Constructor: constructs an instance of bitvector DP
89  BitvectorTheoremProducer(TheoryBitvector* theoryBitvector);
91 
92  //ExprMap<Expr> d_bvPlusCarryCacheLeftBV;
93  //ExprMap<Expr> d_bvPlusCarryCacheRightBV;
94 
95  ////////////////////////////////////////////////////////////////////
96  // Partial Canonization rules
97  ////////////////////////////////////////////////////////////////////
98 
99  ////////////////////////////////////////////////////////////////////
100  // Bitblasting rules for equations
101  ////////////////////////////////////////////////////////////////////
102 
103  /*! \param thm input theorem: (e1[i]<=>e2[i])<=>false
104  *
105  * \result (e1=e2)<=>false
106  */
107  Theorem bitvectorFalseRule(const Theorem& thm);
108 
109  /*! \param thm input theorem: (~e1[i]<=>e2[i])<=>true
110  *
111  * \result (e1!=e2)<=>true
112  */
113  Theorem bitvectorTrueRule(const Theorem& thm);
114 
115  /*! \param e input equation: e1=e2 over bitvector terms
116  * \param f formula over the bits of bitvector variables in e:
117  *
118  * \result \f[\frac{e_1 = e_2}{\bigwedge_{i=1}^n (e_{1}[i]
119  * \iff e_{2}[i]) } \f] where each of \f[ e_{1}[i], e{2}[i] \f] denotes a
120  * formula over variables in \f[ e_{1}, e_{2} \f] respectively
121  */
122  Theorem bitBlastEqnRule(const Expr& e, const Expr& f);
123 
124  /*! \param e : input disequality: e1 != e2 over bitvector terms
125  * \param f : formula over the bits of bitvector variables in e:
126  *
127  * \result \f[\frac{e_1 \not = e_2}{\bigwedge_{i=1}^n ((\neg e_{1}[i])
128  * \iff e_{2}[i]) } \f] where each of \f[ e_{1}[i], e{2}[i] \f] denotes a
129  * formula over variables in \f[ e_{1}, e_{2} \f] respectively
130  */
131  Theorem bitBlastDisEqnRule(const Theorem& e, const Expr& f);
132 
133 
134  ////////////////////////////////////////////////////////////////////
135  // Bitblasting and rewrite rules for Inequations
136  ////////////////////////////////////////////////////////////////////
137 
138  //! sign extend the input SX(e) appropriately
139  Theorem signExtendRule(const Expr& e);
140 
141  //! Pad the kids of BVLT/BVLE to make their length equal
142  Theorem padBVLTRule(const Expr& e, int len);
143 
144  //! Sign Extend the kids of BVSLT/BVSLE to make their length equal
145  Theorem padBVSLTRule(const Expr& e, int len);
146 
147  /*! input: e0 <=(s) e1. output depends on whether the topbits(MSB) of
148  * e0 and e1 are constants. If they are constants then optimizations
149  * are done, otherwise the following rule is implemented.
150  *
151  * e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR
152  * (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR
153  * (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0])
154  */
155  Theorem signBVLTRule(const Expr& e,
156  const Theorem& topBit0,
157  const Theorem& topBit1);
158 
159  /*! NOT(e[0][0] = e[0][1]) <==> e[0][0] = ~e[0][1]
160  */
161  Theorem notBVEQ1Rule(const Expr& e);
162 
163  /*! NOT(e[0][0] < e[0][1]) <==> (e[0][1] <= e[0][0]),
164  * NOT(e[0][0] <= e[0][1]) <==> (e[0][1] < e[0][0])
165  */
166  Theorem notBVLTRule(const Expr& e);
167 
168  //! if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
169  Theorem lhsEqRhsIneqn(const Expr& e, int kind);
170 
171  Theorem zeroLeq(const Expr& e);
172  Theorem bvConstIneqn(const Expr& e, int kind);
173 
174  Theorem generalIneqn(const Expr& e,
175  const Theorem& lhs_i,
176  const Theorem& rhs_i, int kind);
177 
178  ////////////////////////////////////////////////////////////////////
179  // Bitblasting rules for terms
180  ////////////////////////////////////////////////////////////////////
181 
182  // Input: |- BOOLEXTRACT(a,0) <=> bc_0, ... BOOLEXTRACT(a,n-1) <=> bc_(n-1)
183  // where each bc_0 is TRUE or FALSE
184  // Output: |- a = c
185  // where c is an n-bit constant made from the values bc_0..bc_(n-1)
186  Theorem bitExtractAllToConstEq(std::vector<Theorem>& thms);
187  //! t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0
188  Theorem bitExtractToExtract(const Theorem& thm);
189  //! t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])
190  Theorem bitExtractRewrite(const Expr& x);
191 
192  /*! \param x : input1 is bitvector constant
193  * \param i : input2 is extracted bitposition
194  *
195  * \result \f[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff
196  * \mathrm{TRUE}} \f], if bitposition has a 1; \f[
197  * \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}} \f], if
198  * the bitposition has a 0
199  */
200  Theorem bitExtractConstant(const Expr & x, int i);
201 
202  /*! \param x : input1 is bitvector binary concatenation
203  * \param i : input2 is extracted bitposition
204  *
205  * \result \f[ \frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]}
206  * \f], where \f[ 0 \geq i \geq n-1 \f], another case of
207  * boolextract over concatenation is:
208  * \f[\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]} \f],
209  * where \f[ n \geq i \geq m+n-1 \f]
210  */
211  Theorem bitExtractConcatenation(const Expr & x, int i);
212 
213  /*! \param t : input1 is bitvector binary BVMULT. x[0] must be BVCONST
214  * \param i : input2 is extracted bitposition
215  *
216  * \result bitblast of BVMULT
217  */
218  Theorem bitExtractConstBVMult(const Expr& t, int i);
219 
220  /*! \param t : input1 is bitvector binary BVMULT. t[0] must not be BVCONST
221  * \param i : input2 is extracted bitposition
222  *
223  * \result bitblast of BVMULT
224  */
225  Theorem bitExtractBVMult(const Expr& t, int i);
226 
227  /*! \param x : input1 is bitvector extraction [k:j]
228  * \param i : input2 is extracted bitposition
229  *
230  * \result \f[ \frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]}
231  * \f], where \f[ 0 \geq j \geq k < n, 0 \geq i < k-j \f]
232  */
233  Theorem bitExtractExtraction(const Expr & x, int i);
234 
235  /*! \param t1 : input1 is vector of bitblasts of t, from bit i-1 to 0
236  * \param t2 : input2 is vector of bitblasts of q, from bit i-1 to 0
237  * \param bvPlusTerm : input3 is BVPLUS term: BVPLUS(n,t,q)
238  * \param i : input4 is extracted bitposition
239  *
240  * \result The base case is: \f[
241  * \frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]}
242  * \f], when \f[ 0 < i \leq n-1 \f], we have \f[
243  * \frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i]
244  * \oplus c(t,q,i)} \f], where c(t,q,i) is the carry generated
245  * by the addition of bits from 0 to i-1
246  */
247  Theorem bitExtractBVPlus(const std::vector<Theorem>& t1,
248  const std::vector<Theorem>& t2,
249  const Expr& bvPlusTerm, int i);
250 
252  const Theorem& t2_i,
253  const Expr& bvPlusTerm,
254  int bitPos,
255  int precomputed);
256 
257  /*! \param bvPlusTerm : input1 is bvPlusTerm, a BVPLUS term with
258  * arity > 2
259  *
260  * \result : output is iff-Theorem: bvPlusTerm <==> outputTerm,
261  * where outputTerm is an equivalent BINARY bvplus.
262  */
263  Theorem bvPlusAssociativityRule(const Expr& bvPlusTerm);
264 
265  /*! \param x : input1 is bitwise NEGATION
266  * \param i : input2 is extracted bitposition
267  *
268  * \result \f[ \frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])}
269  * \f]
270  */
271  Theorem bitExtractNot(const Expr & x, int i);
272 
273  //! Extract from bitwise AND, OR, or XOR
274  Theorem bitExtractBitwise(const Expr& x, int i, int kind);
275 
276  /*! \param x : input1 is bitvector FIXED SHIFT \f[ e_{[n]} \ll k \f]
277  * \param i : input2 is extracted bitposition
278  *
279  * \result \f[\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}}
280  * \f], if 0 <= i < k. however, if k <= i < n then, result is
281  * \f[\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]} \f]
282  */
283  Theorem bitExtractFixedLeftShift(const Expr & x, int i);
284 
285  Theorem bitExtractFixedRightShift(const Expr & x, int i);
286 
287  // BOOLEXTRACT(bvshl(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
288  // ((s = 1) AND BOOLEXTRACT(t,i-1)) OR ...
289  // ((s = i) AND BOOLEXTRACT(t,0))
290  Theorem bitExtractBVSHL(const Expr & x, int i);
291 
292  // BOOLEXTRACT(bvlshr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
293  // ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...
294  // ((s = n-1-i) AND BOOLEXTRACT(t,n-1))
295  Theorem bitExtractBVLSHR(const Expr & x, int i);
296 
297  // BOOLEXTRACT(bvashr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
298  // ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...
299  // ((s >= n-1-i) AND BOOLEXTRACT(t,n-1))
300  Theorem bitExtractBVASHR(const Expr & x, int i);
301 
302  /*! \param e : input1 is bitvector term
303  * \param r : input2 is extracted bitposition
304  *
305  * \result we check if r > bvlength(e). if yes, then return
306  * BOOLEXTRACT(e,r) <==> FALSE; else raise soundness
307  * exception. (Note: this rule is used in BVPLUS bitblast
308  * function)
309  */
310  Theorem zeroPaddingRule(const Expr& e, int r);
311 
312  Theorem bitExtractSXRule(const Expr& e, int i);
313 
314  //! c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
315  Theorem eqConst(const Expr& e);
316  //! |- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
317  Theorem eqToBits(const Theorem& eq);
318  //! t<<n = c @ 0bin00...00, takes e == (t<<n)
319  Theorem leftShiftToConcat(const Expr& e);
320  //! t<<n = c @ 0bin00...00, takes e == (t<<n)
322  //! t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
323  Theorem rightShiftToConcat(const Expr& e);
324  //! BVSHL(t,c) = t[n-c,0] @ 0bin00...00
325  Theorem bvshlToConcat(const Expr& e);
326  //! BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
327  Theorem bvshlSplit(const Expr& e);
328  //! BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]
329  Theorem bvlshrToConcat(const Expr& e);
330  //! All shifts over a 0 constant = 0
331  Theorem bvShiftZero(const Expr& e);
332  //! BVASHR(t,c) = SX(t[n-1,c], n-1)
333  Theorem bvashrToConcat(const Expr& e);
334  //! a XNOR b <=> (~a & ~b) | (a & b)
335  Theorem rewriteXNOR(const Expr& e);
336  //! a NAND b <=> ~(a & b)
337  Theorem rewriteNAND(const Expr& e);
338  //! a NOR b <=> ~(a | b)
339  Theorem rewriteNOR(const Expr& e);
340  //! BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
341  Theorem rewriteBVCOMP(const Expr& e);
342  //! a - b <=> a + (-b)
343  Theorem rewriteBVSub(const Expr& e);
344  //! k*t = BVPLUS(n, <sum of shifts of t>) -- translation of k*t to BVPLUS
345  /*! If k = 2^m, return k*t = t\@0...0 */
346  Theorem constMultToPlus(const Expr& e);
347  //! 0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
348  /*! where k is the size of the 0bin0...0 */
350 
351 
352  ///////////////////////////////////////////////////////////////////
353  ///// Bvplus Normal Form rules
354  ///////////////////////////////////////////////////////////////////
355  Theorem zeroCoeffBVMult(const Expr& e);
356  Theorem oneCoeffBVMult(const Expr& e);
357  Theorem flipBVMult(const Expr& e);
358  //! converts e to a bitvector of length rat
359  Expr pad(int rat, const Expr& e);
360  Theorem padBVPlus(const Expr& e);
361  Theorem padBVMult(const Expr& e);
363  Theorem bvMultAssocRule(const Expr& e);
364  Theorem bvMultDistRule(const Expr& e);
365  Theorem flattenBVPlus(const Expr& e);
367  Theorem lhsMinusRhsRule(const Expr& e);
368  Theorem extractBVMult(const Expr& e);
369  Theorem extractBVPlus(const Expr& e);
370  //! ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
371  Theorem iteExtractRule(const Expr& e);
372  //! ~ite(c,t1,t2) <=> ite(c,~t1,~t2)
373  Theorem iteBVnegRule(const Expr& e);
374 
375  Theorem bvuminusBVConst(const Expr& e);
376  Theorem bvuminusBVMult(const Expr& e);
377  Theorem bvuminusBVUminus(const Expr& e);
378  Theorem bvuminusVar(const Expr& e);
379  Theorem bvmultBVUminus(const Expr& e);
380  //! -t <==> ~t+1
381  Theorem bvuminusToBVPlus(const Expr& e);
382  //! -(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
383  Theorem bvuminusBVPlus(const Expr& e);
384 
385 
386  ///////////////////////////////////////////////////////////////////
387  ///// Concatenation Normal Form rules
388  ///////////////////////////////////////////////////////////////////
389 
390  // Extraction rules
391 
392  //! c1[i:j] = c (extraction from a constant bitvector)
393  Theorem extractConst(const Expr& e);
394  //! t[n-1:0] = t for n-bit t
395  Theorem extractWhole(const Expr& e);
396  //! t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)
397  Theorem extractExtract(const Expr& e);
398  //! (t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
399  Theorem extractConcat(const Expr& e);
400 
401  //! Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j]
402  Theorem extractBitwise(const Expr& e, int kind, const std::string& name);
403  //! (t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)
404  Theorem extractAnd(const Expr& e);
405  //! (t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)
406  Theorem extractOr(const Expr& e);
407  //! (~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
408  Theorem extractNeg(const Expr& e);
409 
410  // Negation rules
411 
412  //! ~c1 = c (bit-wise negation of a constant bitvector)
413  Theorem negConst(const Expr& e);
414  //! ~(t1\@...\@tn) = (~t1)\@...\@(~tn) -- push negation through concat
415  Theorem negConcat(const Expr& e);
416  //! ~(~t) = t -- eliminate double negation
417  Theorem negNeg(const Expr& e);
418  //! ~t = -1*t + 1 -- eliminate negation
419  Theorem negElim(const Expr& e);
420  //! ~(t1 & t2) <=> ~t1 | ~t2 -- DeMorgan's Laws
421  Theorem negBVand(const Expr& e);
422  //! ~(t1 | t2) <=> ~t1 & ~t2 -- DeMorgan's Laws
423  Theorem negBVor(const Expr& e);
424  //! ~(t1 xor t2) = ~t1 xor t2
425  Theorem negBVxor(const Expr& e);
426  //! ~(t1 xnor t2) = t1 xor t2
427  Theorem negBVxnor(const Expr& e);
428 
429  // Bit-wise rules
430  //! Combine constants in bitwise AND, OR, XOR
431  Theorem bitwiseConst(const Expr& e, const std::vector<int>& idxs,
432  int kind);
433  //! Lifts concatenation above bitwise operators.
434  Theorem bitwiseConcat(const Expr& e, int kind);
435  //! Flatten bitwise operation
436  Theorem bitwiseFlatten(const Expr& e, int kind);
437  //! Simplify bitwise operator containing a constant child
438  /*! \param e is the bit-wise expr
439  * \param idx is the index of the constant bitvector
440  * \param kind is the kind of e
441  */
442  Theorem bitwiseConstElim(const Expr& e, int idx, int kind);
443 
444  /*! checks if e is already present in likeTerms without conflicts.
445  * if yes return 1, else{ if conflict return -1 else return 0 }
446  * we have conflict if
447  * 1. the kind of e is BVNEG,
448  * and e[0] is already present in likeTerms
449  * 2. ~e is present in likeTerms already
450  */
451  int sameKidCheck(const Expr& e, ExprMap<int>& likeTerms);
452 
453  // Concatenation rules
454 
455  //! c1\@c2\@...\@cn = c (concatenation of constant bitvectors)
456  Theorem concatConst(const Expr& e);
457  //! Flatten one level of nested concatenation, e.g.: x\@(y\@z)\@w = x\@y\@z\@w
458  Theorem concatFlatten(const Expr& e);
459  //! Merge n-ary concat. of adjacent extractions: x[15:8]\@x[7:0] = x[15:0]
460  Theorem concatMergeExtract(const Expr& e);
461 
462  ///////////////////////////////////////////////////////////////////
463  ///// Modulo arithmetic rules
464  ///////////////////////////////////////////////////////////////////
465 
466  //! BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)
467  Theorem bvplusConst(const Expr& e);
468  /*! @brief n*c1 = c, where n >= 0 (multiplication of a constant
469  * bitvector by a non-negative constant) */
470  Theorem bvmultConst(const Expr& e);
471 
472  ///////////////////////////////////////////////////////////////////
473  ///// Type predicate rules
474  ///////////////////////////////////////////////////////////////////
475 
476  //! |- t=0 OR t=1 for any 1-bit bitvector t
477  Theorem typePredBit(const Expr& e);
478 
479  //! Expand the type predicate wrapper (compute the actual type predicate)
480  Theorem expandTypePred(const Theorem& tp);
481 
482  ////////////////////////////////////////////////////////////////////
483  // Helper functions
484  ////////////////////////////////////////////////////////////////////
485  //! Create Expr from Rational (for convenience)
486  Expr rat(const Rational& r) { return d_em->newRatExpr(r); }
487  /*! \param t1BitExtractThms : input1 is vector of bitblasts of t1,
488  * from bit i-1 to 0
489  *
490  * \param t2BitExtractThms : input2 is vector of bitblasts of t2,
491  * from bit i-1 to 0
492  *
493  * \param bitPos : input3 is extracted * bitposition
494  *
495  * \result is the expression \f$t1[0] \wedge t2[0]\f$ if
496  * bitPos=0. this function is recursive; if bitPos > 0 then the
497  * output expression is
498  * \f[ (t1[i-1] \wedge t2[i-1])
499  * \vee (t1[i-1] \wedge computeCarry(t1,t2,i-1))
500  * \vee (t2[i-1] \wedge computeCarry(t1,t2,i-1))
501  * \f]
502  */
503  Expr computeCarry(const std::vector<Theorem>& t1BitExtractThms,
504  const std::vector<Theorem>& t2BitExtractThms,
505  int bitPos);
506 
508  const Theorem& t2_i,
509  int bitPos,
510  int precomputedFlag);
511 
512  /*Beginning of Lorenzo PLatania's methods*/
513 
514  // virtual Theorem multiply_coeff( Rational mult_inv, const Expr& e);
515  //! isolate a variable with coefficient = 1 on the Lhs of an
516  //equality expression
517  virtual Theorem isolate_var(const Expr& e);
518 
519  // BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)
520  // where n = BVSize(b), a != 0
521  virtual Theorem liftConcatBVMult(const Expr& e);
522 
523  //! canonize BVMult expressions in order to get one coefficient
524  //multiplying the variable(s) in the expression
525  virtual Theorem canonBVMult( const Expr& e );
526 
527  // BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)
528  // where n = BVSize(b)
529  virtual Theorem liftConcatBVPlus(const Expr& e);
530 
531  //! canonize BVPlus expressions in order to get just one
532  //coefficient multiplying each variable in the expression
533  virtual Theorem canonBVPlus( const Expr& e );
534 
535  //! canonize BVMinus expressions: push the minus to the leafs in
536  //BVPLUS expr; simplify minus in BVMULT and BVMINUS expr
537  virtual Theorem canonBVUMinus( const Expr& e );
538 
539  // Input: t[hi:lo] = rhs
540  // if t appears as leaf in rhs, then:
541  // t[hi:lo] = rhs |- Exists x,y,z. (t = x @ y @ z AND y = rhs), solvedForm = false
542  // else
543  // t[hi:lo] = rhs |- Exists x,y,z. (t = x @ rhs @ z AND y = rhs), solvedForm = true
544  virtual Theorem processExtract(const Theorem& e, bool& solvedForm);
545 
546  // normalizes equation
547  virtual Theorem canonBVEQ( const Expr& e, int maxEffort = 3 );
548 
549  //! apply the distributive rule on the BVMULT expression e
550  virtual Theorem distributive_rule( const Expr& e );
551  // virtual Theorem BVMultConstTerm( const Expr& e1, const Expr& e2);
552  // recursively reorder subterms in a BVMULT term
553  virtual Theorem BVMult_order_subterms( const Expr& e);
554 
555  // rewrites the equation in the form 0 = Expr
556  // this is needed for TheoryBitvector::solve
557  virtual Theorem MarkNonSolvableEq( const Expr& e);
558  /*End of Lorenzo PLatania's methods*/
559 
560  // rewrite BVZEROEXTEND into CONCAT
561  virtual Theorem zeroExtendRule(const Expr& e);
562 
563  // rewrite BVREPEAT into CONCAT
564  virtual Theorem repeatRule(const Expr& e);
565 
566  // rewrite BVROTL into CONCAT
567  virtual Theorem rotlRule(const Expr& e);
568  // rewrite BVROTR into CONCAT
569  virtual Theorem rotrRule(const Expr& e);
570 
571  // Dejan: Division rewrites
572 
573  /**
574  * Divide a with b unsigned and return the bit-vector constant result
575  */
576  virtual Theorem bvUDivConst(const Expr& divExpr);
577 
578  /**
579  * Rewrite x/y to
580  * \f[\exists s: s = x/y \wedge (y \neq 0 \implies x = y * s + m \wedge 0 <= m < y)\f]
581  */
582  virtual Theorem bvUDivTheorem(const Expr& divExpr);
583 
584  /**
585  * Compute the remainder
586  */
587  virtual Theorem bvURemConst(const Expr& remExpr);
588 
589  /**
590  * Rewrite a%b in terms of a/b, i.e. a - a/b
591  */
592  virtual Theorem bvURemRewrite(const Expr& remExpr);
593 
594  /**
595  * Bit-blast the multiplication a_times_b given the bits in a_bits and b_bits.
596  * The resulting output bits will be in the vector output_bits. The return value
597  * is a theorem saying there is no overflow for this multiplication. (TODO, it's
598  * just an empty theorem for now).
599  */
600  virtual Theorem bitblastBVMult(const std::vector<Theorem>& a_bits,
601  const std::vector<Theorem>& b_bits,
602  const Expr& a_times_b,
603  std::vector<Theorem>& output_bits);
604 
605  /**
606  * Bit-blast the sum a_plus_b given the bits in a_bits and b_bits.
607  * The resulting output bits will be in the vector output_bits. The return value
608  * is a theorem saying there is no overflow for this sum. (TODO, it's
609  * just an empty theorem for now).
610  */
611  virtual Theorem bitblastBVPlus(const std::vector<Theorem>& a_bits,
612  const std::vector<Theorem>& b_bits,
613  const Expr& a_plus_b,
614  std::vector<Theorem>& output_bits);
615 
616  /**
617  * Rewrite the signed divide in terms of the unsigned one.
618  */
619  virtual Theorem bvSDivRewrite(const Expr& sDivExpr);
620 
621  /**
622  * Rewrite the signed remainder in terms of the unsigned one.
623  */
624  virtual Theorem bvSRemRewrite(const Expr& sRemExpr);
625 
626  /**
627  * Rewrite the signed mod in terms of the unsigned one.
628  */
629  virtual Theorem bvSModRewrite(const Expr& sModExpr);
630 
631  /**
632  * Rewrite \f[x_1 \vee x_2 \vee \ldots \vee x_n = 0\f] into
633  * \f[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\f].
634  */
635  virtual Theorem zeroBVOR(const Expr& orEqZero);
636 
637  /**
638  * Rewrite \f[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\f] into
639  * \f[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\f].
640  */
641  virtual Theorem oneBVAND(const Expr& andEqOne);
642 
643  /**
644  * Equalities over constants go to true/false.
645  */
646  virtual Theorem constEq(const Expr& eq);
647 
648  /**
649  * Returns true if equation is of the form x[i:j] = x[k:l], where the
650  * extracted segments overlap, i.e. i > j >= k > l or k > i >= l > j.
651  */
652  bool solveExtractOverlapApplies(const Expr& eq);
653 
654  /**
655  * Returns the theorem that simplifies the equality of two overlapping
656  * extracts over the same term.
657  */
658  Theorem solveExtractOverlap(const Expr& eq);
659 
660 
661 }; // end of class BitvectorTheoremProducer
662 } // end of name-space CVC3
663 
664 
665 #endif
666 
Theorem bitExtractBVSHL(const Expr &x, int i)
Theorem bitExtractToExtract(const Theorem &thm)
t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0
Theorem expandTypePred(const Theorem &tp)
Expand the type predicate wrapper (compute the actual type predicate)
Expr sumNormalizedElements(int bvplusLength, const std::vector< Expr > &elements)
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem bvUDivTheorem(const Expr &divExpr)
const Expr & bvZero() const
Return cached constant 0bin0.
Theorem extractExtract(const Expr &e)
t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)
Theorem bvMultDistRule(const Expr &e)
a*(t1+...+tn) <==> (a*t1+...+a*tn), where all kids are equibvLength
Theorem bitExtractBVLSHR(const Expr &x, int i)
Theorem bvshlToConcat(const Expr &e)
BVSHL(t,c) = t[n-c,0] @ 0bin00...00.
Theorem bvshlSplit(const Expr &e)
BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
Theorem bitExtractFixedLeftShift(const Expr &x, int i)
Expr computeCarryPreComputed(const Theorem &t1_i, const Theorem &t2_i, int bitPos, int precomputedFlag)
compute carryout of the current bits and cache them, and return
Theorem bitExtractRewrite(const Expr &x)
t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])
Theorem bitExtractNot(const Expr &x, int i)
Theorem flattenBVPlus(const Expr &e)
input BVPLUS expression e.output e <==> e', where e' has no BVPLUS
virtual Theorem bitblastBVMult(const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_times_b, std::vector< Theorem > &output_bits)
Theorem iteExtractRule(const Expr &e)
ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
Expr chopConcat(int bv_size, Rational c, std::vector< Expr > &concatKids)
Theorem bitExtractFixedRightShift(const Expr &x, int i)
Theorem negBVxor(const Expr &e)
~(t1 xor t2) = ~t1 xor t2
void createNewPlusCollection(const Expr &e, const ExprMap< Rational > &likeTerms, Rational &plusConstant, std::vector< Expr > &result)
virtual Theorem BVMult_order_subterms(const Expr &e)
Theorem bitvectorFalseRule(const Theorem &thm)
Theorem bitBlastDisEqnRule(const Theorem &e, const Expr &f)
virtual Theorem bvUDivConst(const Expr &divExpr)
Theorem bvmultBVUminus(const Expr &e)
c*(-t) <==> (-c)*t
Theorem constMultToPlus(const Expr &e)
k*t = BVPLUS(n, ) – translation of k*t to BVPLUS
Theorem zeroLeq(const Expr &e)
|= 0 <= foo <-> TRUE
Theorem bvuminusBVUminus(const Expr &e)
-(-e) <==> e
Expr d_bvZero
Constant 1-bit bit-vector 0bin0.
Expr computeCarry(const std::vector< Theorem > &t1BitExtractThms, const std::vector< Theorem > &t2BitExtractThms, int bitPos)
Theorem bvmultConst(const Expr &e)
n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant) ...
Theorem bitExtractSXRule(const Expr &e, int i)
bitExtractSXRule
Theorem eqConst(const Expr &e)
c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
virtual Theorem bvSRemRewrite(const Expr &sRemExpr)
Theorem padBVMult(const Expr &e)
Pad the kids of BVMULT to make their bvLength = # of output-bits.
Theorem typePredBit(const Expr &e)
|- t=0 OR t=1 for any 1-bit bitvector t
Theorem rewriteXNOR(const Expr &e)
a XNOR b <=> (~a & ~b) | (a & b)
Theorem bitvectorTrueRule(const Theorem &thm)
virtual Theorem bvSDivRewrite(const Expr &sDivExpr)
Theorem lhsEqRhsIneqn(const Expr &e, int kind)
if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
void getPlusTerms(const Expr &e, Rational &known_term, ExprMap< Rational > &sumHashMap)
Theorem bitExtractConcatenation(const Expr &x, int i)
Theorem bitwiseFlatten(const Expr &e, int kind)
Flatten bitwise operation.
const Expr & bvOne() const
Return cached constant 0bin1.
Theorem negConst(const Expr &e)
~c1 = c (bit-wise negation of a constant bitvector)
virtual Theorem liftConcatBVPlus(const Expr &e)
virtual Theorem constEq(const Expr &eq)
virtual Theorem liftConcatBVMult(const Expr &e)
Theorem bvPlusAssociativityRule(const Expr &bvPlusTerm)
Theorem extractNeg(const Expr &e)
(~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
virtual Theorem processExtract(const Theorem &e, bool &solvedForm)
Theorem bitBlastEqnRule(const Expr &e, const Expr &f)
Theorem negBVand(const Expr &e)
~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws
Theorem bitExtractBVMult(const Expr &t, int i)
Theorem bvlshrToConcat(const Expr &e)
BVLSHR(t,c) = 0bin00...00 @ t[n-1,c].
Theorem bvuminusBVPlus(const Expr &e)
-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
Theorem negConcat(const Expr &e)
~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat
Theorem eqToBits(const Theorem &eq)
|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
Theorem bvuminusBVConst(const Expr &e)
-0 <==> 0, -c <==> ~c+1
Theorem bitwiseConcat(const Expr &e, int kind)
Lifts concatenation above bitwise operators.
Theorem bvShiftZero(const Expr &e)
All shifts over a 0 constant = 0.
Theorem bitExtractBitwise(const Expr &x, int i, int kind)
Extract from bitwise AND, OR, or XOR.
virtual Theorem bitblastBVPlus(const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_plus_b, std::vector< Theorem > &output_bits)
virtual Theorem canonBVMult(const Expr &e)
canonize BVMult expressions in order to get one coefficient
Theorem bitExtractExtraction(const Expr &x, int i)
Theorem rightShiftToConcat(const Expr &e)
t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
Theorem bvConstIneqn(const Expr &e, int kind)
if indeed e[0] < e[1] then (e<==>true) else (e<==>false)
Theorem constWidthLeftShiftToConcat(const Expr &e)
Expr pad(int rat, const Expr &e)
converts e to a bitvector of length rat
virtual Theorem bvURemRewrite(const Expr &remExpr)
Arithmetic proof rules.
virtual Theorem zeroExtendRule(const Expr &e)
BVZEROEXTEND(e, i) = zeroString @ e.
Theorem rewriteBVCOMP(const Expr &e)
BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
Theorem bvplusZeroConcatRule(const Expr &e)
0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
Theorem bitExtractConstBVMult(const Expr &t, int i)
void collectLikeTermsOfPlus(const Expr &e, ExprMap< Rational > &likeTerms, Rational &plusConstant)
Theorem negBVxnor(const Expr &e)
~(t1 xnor t2) = t1 xor t2
Theorem bitExtractBVPlus(const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i)
Theorem bvplusConst(const Expr &e)
BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)
Theorem negBVor(const Expr &e)
~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws
Theorem extractConst(const Expr &e)
c1[i:j] = c (extraction from a constant bitvector)
Theorem bitwiseConst(const Expr &e, const std::vector< int > &idxs, int kind)
Combine constants in bitwise AND, OR, XOR.
virtual Theorem distributive_rule(const Expr &e)
apply the distributive rule on the BVMULT expression e
Theorem bitExtractBVASHR(const Expr &x, int i)
Theorem extractAnd(const Expr &e)
(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)
void collectOneTermOfPlus(const Rational &coefficient, const Expr &var, ExprMap< Rational > &likeTerms, Rational &plusConstant)
Expr newRatExpr(const Rational &r)
Definition: expr_manager.h:471
Theorem bvuminusBVMult(const Expr &e)
-(c*t)<=>(-c)*t; if -c==0 return e<=>0. if(-c==1) return e<=>t
Theorem flipBVMult(const Expr &e)
t1*a <==> a*t1
Theorem padBVPlus(const Expr &e)
Pad the kids of BVMULT to make their bvLength = # of output-bits.
Expr rat(const Rational &r)
Create Expr from Rational (for convenience)
Theorem leftShiftToConcat(const Expr &e)
Theorem rewriteNAND(const Expr &e)
a NAND b <=> ~(a & b)
Theorem bitExtractAllToConstEq(std::vector< Theorem > &thms)
Theorem bvConstMultAssocRule(const Expr &e)
a*(b*t) <==> (a*b)*t, where a,b,t have same bvLength
int sameKidCheck(const Expr &e, ExprMap< int > &likeTerms)
Theorem negElim(const Expr &e)
~t = -1*t + 1 – eliminate negation
virtual Theorem bvSModRewrite(const Expr &sModExpr)
Expr buildPlusTerm(int bv_size, Rational &known_term, ExprMap< Rational > &sumHashMap)
Expr d_bvOne
Constant 1-bit bit-vector 0bin1.
virtual Theorem canonBVEQ(const Expr &e, int maxEffort=3)
virtual Theorem MarkNonSolvableEq(const Expr &e)
Theorem extractBVPlus(const Expr &e)
(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n
Theorem extractBitwise(const Expr &e, int kind, const std::string &name)
Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j].
Theorem negNeg(const Expr &e)
~(~t) = t – eliminate double negation
Theorem padBVLTRule(const Expr &e, int len)
Pad the kids of BVLT/BVLE to make their length equal.
virtual Theorem oneBVAND(const Expr &andEqOne)
virtual Theorem zeroBVOR(const Expr &orEqZero)
Theorem bitwiseConstElim(const Expr &e, int idx, int kind)
Simplify bitwise operator containing a constant child.
virtual Theorem canonBVUMinus(const Expr &e)
canonize BVMinus expressions: push the minus to the leafs in
Theorem signExtendRule(const Expr &e)
sign extend the input SX(e) appropriately
Theorem extractConcat(const Expr &e)
(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
Theorem rewriteNOR(const Expr &e)
a NOR b <=> ~(a | b)
Theorem generalIneqn(const Expr &e, const Theorem &lhs_i, const Theorem &rhs_i, int kind)
virtual Theorem repeatRule(const Expr &e)
BVREPEAT(e, i) = e @ e @ ... @ e.
virtual Theorem rotlRule(const Expr &e)
BVROTL(e, i) = a[n-i-1:0] @ a[n-1:n-i].
Theorem zeroPaddingRule(const Expr &e, int r)
Theorem extractOr(const Expr &e)
(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)
Theorem extractWhole(const Expr &e)
t[n-1:0] = t for n-bit t
Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
Theorem concatMergeExtract(const Expr &e)
Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0].
Theorem rewriteBVSub(const Expr &e)
a - b <=> a + (-b)
Theorem concatFlatten(const Expr &e)
Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w.
Theorem bvashrToConcat(const Expr &e)
BVASHR(t,c) = SX(t[n-1,c], n-1)
Definition: expr.cpp:35
This class implements proof rules for bitvector normalizers (concatenation normal form...
Theorem padBVSLTRule(const Expr &e, int len)
Sign Extend the kids of BVSLT/BVSLE to make their length equal.
Theorem bvuminusToBVPlus(const Expr &e)
-t <==> ~t+1
Theorem iteBVnegRule(const Expr &e)
~ite(c,t1,t2) <=> ite(c,~t1,~t2)
Theorem bitExtractBVPlusPreComputed(const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed)
BitvectorTheoremProducer(TheoryBitvector *theoryBitvector)
Constructor: constructs an instance of bitvector DP.
Theorem bvuminusVar(const Expr &e)
-v <==> -1*v
Theorem concatConst(const Expr &e)
c1@c2@...@cn = c (concatenation of constant bitvectors)
virtual Theorem canonBVPlus(const Expr &e)
canonize BVPlus expressions in order to get just one
Theorem bitExtractConstant(const Expr &x, int i)
virtual Theorem bvURemConst(const Expr &remExpr)
Theorem bvMultAssocRule(const Expr &e)
(t1*t2)*t3 <==> t1*(t2*t3), where t1
Theorem extractBVMult(const Expr &e)
(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n
Theorem signBVLTRule(const Expr &e, const Theorem &topBit0, const Theorem &topBit1)
virtual Theorem isolate_var(const Expr &e)
isolate a variable with coefficient = 1 on the Lhs of an
virtual Theorem rotrRule(const Expr &e)
BVROTR(e, i) = a[i-1:0] @ a[n-1:i].