CVC3
bitvector_proof_rules.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file bitvector_proof_rules.h
4  * \brief Arithmetic proof rules
5  *
6  * Author: Vijay Ganesh.
7  *
8  * Created:Wed May 5 15:47: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_proof_rules_h_
23 #define _cvc3__bitvector_proof_rules_h_
24 
25 #include <string>
26 #include <vector>
27 
28 namespace CVC3 {
29 
30  class Expr;
31  class Theorem;
32 
34  public:
35  // Destructor
36  virtual ~BitvectorProofRules() { }
37 
38  ////////////////////////////////////////////////////////////////////
39  // Bitblasting rules for equations
40  ////////////////////////////////////////////////////////////////////
41 
42  /*! \param thm input theorem: (e1[i]<=>e2[i])<=>false
43  *
44  * \result (e1=e2)<=>false
45  */
46  virtual Theorem bitvectorFalseRule(const Theorem& thm) = 0;
47 
48  /*! \param thm input theorem: (~e1[i]<=>e2[i])<=>true
49  *
50  * \result (e1!=e2)<=>true
51  */
52  virtual Theorem bitvectorTrueRule(const Theorem& thm) = 0;
53 
54 
55  //! t1=t2 ==> AND_i(t1[i:i] = t2[i:i])
56  /*!
57  * \param e is a Expr(t1=t2)
58  *
59  * \param f is the resulting expression AND_i(t1[i:i] = t2[i:i])
60  * is passed to the rule for efficiency.
61  */
62  virtual Theorem bitBlastEqnRule(const Expr& e, const Expr& f) = 0;
63  //! t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i])
64  /*!
65  * \param e is a Theorem(t1/=t2)
66  *
67  * \param f is the resulting expression OR_i(NOT t1[i]<=>t2[i]),
68  * passed to the rule for efficiency.
69  */
70  virtual Theorem bitBlastDisEqnRule(const Theorem& e, const Expr& f) = 0;
71 
72 
73  ////////////////////////////////////////////////////////////////////
74  // Bitblasting and rewrite rules for Inequations
75  ////////////////////////////////////////////////////////////////////
76 
77  //! sign extend the input SX(e) appropriately
78  virtual Theorem signExtendRule(const Expr& e) = 0;
79 
80  //! Pad the kids of BVLT/BVLE to make their length equal
81  virtual Theorem padBVLTRule(const Expr& e, int len) = 0;
82 
83  //! Sign Extend the kids of BVSLT/BVSLE to make their length equal
84  virtual Theorem padBVSLTRule(const Expr& e, int len) = 0;
85 
86  /*! input: e0 <=(s) e1. output depends on whether the topbits(MSB) of
87  * e0 and e1 are constants. If they are constants then optimizations
88  * are done, otherwise the following rule is implemented.
89  *
90  * e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR
91  * (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR
92  * (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0])
93  */
94  virtual Theorem signBVLTRule(const Expr& e,
95  const Theorem& topBit0,
96  const Theorem& topBit1) = 0;
97 
98  /*! NOT(e[0][0] = e[0][1]) <==> e[0][0] = ~e[0][1]
99  */
100  virtual Theorem notBVEQ1Rule(const Expr& e) = 0;
101 
102  /*! NOT(e[0][0] < e[0][1]) <==> (e[0][1] <= e[0][0]),
103  * NOT(e[0][0] <= e[0][1]) <==> (e[0][1] < e[0][0])
104  */
105  virtual Theorem notBVLTRule(const Expr& e) = 0;
106 
107  //! if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
108  virtual Theorem lhsEqRhsIneqn(const Expr& e, int kind) = 0;
109 
110 
111  virtual Theorem zeroLeq(const Expr& e) = 0;
112  virtual Theorem bvConstIneqn(const Expr& e, int kind) = 0;
113 
114  virtual Theorem generalIneqn(const Expr& e,
115  const Theorem& e0,
116  const Theorem& e1, int kind) = 0;
117 
118 
119  ////////////////////////////////////////////////////////////////////
120  // Bitblast rules for terms
121  ////////////////////////////////////////////////////////////////////
122 
123  // Input: |- BOOLEXTRACT(a,0) <=> bc_0, ... BOOLEXTRACT(a,n-1) <=> bc_(n-1)
124  // where each bc_0 is TRUE or FALSE
125  // Output: |- a = c
126  // where c is an n-bit constant made from the values bc_0..bc_(n-1)
127  virtual Theorem bitExtractAllToConstEq(std::vector<Theorem>& thms) = 0;
128 
129  //! t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0
130  /*! \param thm is a Theorem(t[i]) or Theorem(NOT t[i]), where t[i]
131  * is BOOLEXTRACT(t, i).
132  */
133  virtual Theorem bitExtractToExtract(const Theorem& thm) = 0;
134 
135  //! t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])
136  virtual Theorem bitExtractRewrite(const Expr& x) = 0;
137 
138  /*! \param x is bitvector constant
139  * \param i is extracted bitposition
140  *
141  * \result \f[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff
142  * \mathrm{TRUE}} \f], if bitposition has a 1; \f[
143  * \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}} \f], if
144  * the bitposition has a 0
145  */
146  virtual Theorem bitExtractConstant(const Expr & x, int i)= 0;
147 
148  /*! \param x is bitvector binary concatenation
149  * \param i is extracted bitposition
150  *
151  * \result \f[ \frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]}
152  * \f], where \f[ 0 \geq i \geq n-1 \f], another case of
153  * boolextract over concatenation is:
154  * \f[\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]} \f],
155  * where \f[ n \geq i \geq m+n-1 \f]
156  */
157  virtual Theorem bitExtractConcatenation(const Expr & x,
158  int i)= 0;
159 
160  /*! \param t is bitvector binary BVMULT. x[0] must be BVCONST
161  * \param i is extracted bitposition
162  *
163  * \result bitblast of BVMULT
164  */
165  virtual Theorem bitExtractConstBVMult(const Expr& t, int i)= 0;
166 
167  /*! \param t : input1 is bitvector binary BVMULT. t[0] must not be BVCONST
168  * \param i : input2 is extracted bitposition
169  *
170  * \result bitblast of BVMULT
171  */
172  virtual Theorem bitExtractBVMult(const Expr& t, int i) = 0;
173 
174  /*! \param x is bitvector extraction e[k:j]
175  * \param i is extracted bitposition
176  *
177  * \result \f[ \frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]}
178  * \f], where \f[ 0 \geq j \geq k < n, 0 \geq i < k-j \f]
179  */
180  virtual Theorem bitExtractExtraction(const Expr & x, int i)= 0;
181 
182  /*! \param t1 is vector of bitblasts of t, from bit i-1 to 0
183  * \param t2 is vector of bitblasts of q, from bit i-1 to 0
184  * \param bvPlusTerm is BVPLUS term: BVPLUS(n,t,q)
185  * \param i is extracted bitposition
186  *
187  * \result The base case is: \f[
188  * \frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]}
189  * \f], when \f[ 0 < i \leq n-1 \f], we have \f[
190  * \frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i]
191  * \oplus c(t,q,i)} \f], where c(t,q,i) is the carry generated
192  * by the addition of bits from 0 to i-1
193  */
194  virtual Theorem bitExtractBVPlus(const std::vector<Theorem>& t1,
195  const std::vector<Theorem>& t2,
196  const Expr& bvPlusTerm, int i) = 0;
197 
198 
199  virtual Theorem bitExtractBVPlusPreComputed(const Theorem& t1_i,
200  const Theorem& t2_i,
201  const Expr& bvPlusTerm,
202  int bitPos,
203  int precomputed) = 0;
204 
205 
206  /*! \param bvPlusTerm : input1 is bvPlusTerm, a BVPLUS term with
207  * arity > 2
208  *
209  * \result : output is iff-Theorem: bvPlusTerm <==> outputTerm,
210  * where outputTerm is an equivalent BINARY bvplus.
211  */
212  virtual Theorem bvPlusAssociativityRule(const Expr& bvPlusTerm)= 0;
213 
214  /*! \param x : input1 is bitwise NEGATION
215  * \param i : input2 is extracted bitposition
216  *
217  * \result \f[ \frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])}
218  * \f]
219  */
220  virtual Theorem bitExtractNot(const Expr & x, int i)= 0;
221 
222  //! Extract from bitwise AND, OR, or XOR
223  virtual Theorem bitExtractBitwise(const Expr & x, int i, int kind)= 0;
224 
225  /*! \param x : input1 is bitvector FIXED SHIFT \f[ e_{[n]} \ll k \f]
226  * \param i : input2 is extracted bitposition
227  *
228  * \result \f[\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}}
229  * \f], if 0 <= i < k. however, if k <= i < n then, result is
230  * \f[\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]} \f]
231  */
232  virtual Theorem bitExtractFixedLeftShift(const Expr & x,
233  int i)= 0;
234 
235  virtual Theorem bitExtractFixedRightShift(const Expr & x,
236  int i)= 0;
237  // BOOLEXTRACT(bvshl(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
238  // ((s = 1) AND BOOLEXTRACT(t,i-1)) OR ...
239  // ((s = i) AND BOOLEXTRACT(t,0))
240  virtual Theorem bitExtractBVSHL(const Expr & x, int i) = 0;
241 
242  // BOOLEXTRACT(bvlshr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
243  // ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...
244  // ((s = n-1-i) AND BOOLEXTRACT(t,n-1))
245  virtual Theorem bitExtractBVLSHR(const Expr & x, int i) = 0;
246 
247  // BOOLEXTRACT(bvashr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
248  // ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...
249  // ((s >= n-1-i) AND BOOLEXTRACT(t,n-1))
250  virtual Theorem bitExtractBVASHR(const Expr & x, int i) = 0;
251 
252  /*! \param e : input1 is bitvector term
253  * \param r : input2 is extracted bitposition
254  *
255  * \result we check if r > bvlength(e). if yes, then return
256  * BOOLEXTRACT(e,r) <==> FALSE; else raise soundness
257  * exception. (Note: this rule is used in BVPLUS bitblast
258  * function)
259  */
260  virtual Theorem zeroPaddingRule(const Expr& e, int r)= 0;
261 
262 
263  virtual Theorem bitExtractSXRule(const Expr& e, int i) = 0;
264 
265  ///////////////////////////////////////////////////////////////////
266  ///// Special case rewrite rules
267  ///////////////////////////////////////////////////////////////////
268 
269  //! c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
270  virtual Theorem eqConst(const Expr& e) = 0;
271  //! |- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
272  virtual Theorem eqToBits(const Theorem& eq) = 0;
273  //! t<<n = c @ 0bin00...00, takes e == (t<<n)
274  virtual Theorem leftShiftToConcat(const Expr& e) = 0;
275  //! t<<n = c @ 0bin00...00, takes e == (t<<n)
276  virtual Theorem constWidthLeftShiftToConcat(const Expr& e) = 0;
277  //! t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
278  virtual Theorem rightShiftToConcat(const Expr& e) = 0;
279  //! BVSHL(t,c) = t[n-c,0] @ 0bin00...00
280  virtual Theorem bvshlToConcat(const Expr& e) = 0;
281  //! BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
282  virtual Theorem bvshlSplit(const Expr& e) = 0;
283  //! BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]
284  virtual Theorem bvlshrToConcat(const Expr& e) = 0;
285  //! Any shift over a zero = 0
286  virtual Theorem bvShiftZero(const Expr& e) = 0;
287  //! BVASHR(t,c) = SX(t[n-1,c], n-1)
288  virtual Theorem bvashrToConcat(const Expr& e) = 0;
289  //! a XNOR b <=> (~a & ~b) | (a & b)
290  virtual Theorem rewriteXNOR(const Expr& e) = 0;
291  //! a NAND b <=> ~(a & b)
292  virtual Theorem rewriteNAND(const Expr& e) = 0;
293  //! a NOR b <=> ~(a | b)
294  virtual Theorem rewriteNOR(const Expr& e) = 0;
295  //! BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
296  virtual Theorem rewriteBVCOMP(const Expr& e) = 0;
297  //! a - b <=> a + (-b)
298  virtual Theorem rewriteBVSub(const Expr& e) = 0;
299  //! k*t = BVPLUS(n, <sum of shifts of t>) -- translation of k*t to BVPLUS
300  /*! If k = 2^m, return k*t = t\@0...0 */
301  virtual Theorem constMultToPlus(const Expr& e) = 0;
302  //! 0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
303  /*! provided that m+ceil(log2(l)) <= n, where k is the size of the
304  * 0bin0...0, m is the max. length of each argument, and l is the
305  * number of arguments.
306  */
307  virtual Theorem bvplusZeroConcatRule(const Expr& e) = 0;
308 
309 
310  ///////////////////////////////////////////////////////////////////
311  ///// Bvplus Normal Form rules
312  ///////////////////////////////////////////////////////////////////
313  virtual Theorem zeroCoeffBVMult(const Expr& e)=0;
314  virtual Theorem oneCoeffBVMult(const Expr& e)=0;
315  virtual Theorem flipBVMult(const Expr& e) = 0;
316  //! Make args the same length as the result (zero-extend)
317  virtual Theorem padBVPlus(const Expr& e) = 0;
318  //! Make args the same length as the result (zero-extend)
319  virtual Theorem padBVMult(const Expr& e) = 0;
320  virtual Theorem bvConstMultAssocRule(const Expr& e) = 0;
321  virtual Theorem bvMultAssocRule(const Expr& e) = 0;
322  virtual Theorem bvMultDistRule(const Expr& e) = 0;
323  virtual Theorem flattenBVPlus(const Expr& e) = 0;
324  virtual Theorem combineLikeTermsRule(const Expr& e) = 0;
325  virtual Theorem lhsMinusRhsRule(const Expr& e) = 0;
326  //! (x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n
327  virtual Theorem extractBVMult(const Expr& e) = 0;
328  //! (x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n
329  virtual Theorem extractBVPlus(const Expr& e) = 0;
330  //! ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
331  virtual Theorem iteExtractRule(const Expr& e) = 0;
332  //! ~ite(c,t1,t2) <=> ite(c,~t1,~t2)
333  virtual Theorem iteBVnegRule(const Expr& e) = 0;
334 
335  virtual Theorem bvuminusBVConst(const Expr& e) = 0;
336  virtual Theorem bvuminusBVMult(const Expr& e) = 0;
337  virtual Theorem bvuminusBVUminus(const Expr& e) = 0;
338  virtual Theorem bvuminusVar(const Expr& e) = 0;
339  virtual Theorem bvmultBVUminus(const Expr& e) = 0;
340  //! -t <==> ~t+1
341  virtual Theorem bvuminusToBVPlus(const Expr& e) = 0;
342  //! -(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
343  virtual Theorem bvuminusBVPlus(const Expr& e) = 0;
344 
345 
346 
347  ///////////////////////////////////////////////////////////////////
348  ///// Concatenation Normal Form rules
349  ///////////////////////////////////////////////////////////////////
350 
351  // Extraction rules
352 
353  //! c1[i:j] = c (extraction from a constant bitvector)
354  virtual Theorem extractConst(const Expr& e) = 0;
355  //! t[n-1:0] = t for n-bit t
356  virtual Theorem extractWhole(const Expr& e) = 0;
357  //! t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)
358  virtual Theorem extractExtract(const Expr& e) = 0;
359  //! (t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
360  virtual Theorem extractConcat(const Expr& e) = 0;
361  //! (t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)
362  virtual Theorem extractAnd(const Expr& e) = 0;
363  //! (t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)
364  virtual Theorem extractOr(const Expr& e) = 0;
365  //! (~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
366  virtual Theorem extractNeg(const Expr& e) = 0;
367  //! Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j]
368  virtual Theorem extractBitwise(const Expr& e,
369  int kind, const std::string& name) = 0;
370 
371  // Negation rules
372 
373  //! ~c1 = c (bit-wise negation of a constant bitvector)
374  virtual Theorem negConst(const Expr& e) = 0;
375  //! ~(t1\@...\@tn) = (~t1)\@...\@(~tn) -- push negation through concat
376  virtual Theorem negConcat(const Expr& e) = 0;
377  //! ~(~t) = t -- eliminate double negation
378  virtual Theorem negNeg(const Expr& e) = 0;
379  //! ~t = -1*t + 1 -- eliminate negation
380  virtual Theorem negElim(const Expr& e) = 0;
381  //! ~(t1 & t2) <=> ~t1 | ~t2 -- DeMorgan's Laws
382  virtual Theorem negBVand(const Expr& e) = 0;
383  //! ~(t1 | t2) <=> ~t1 & ~t2 -- DeMorgan's Laws
384  virtual Theorem negBVor(const Expr& e) = 0;
385  //! ~(t1 xor t2) = ~t1 xor t2
386  virtual Theorem negBVxor(const Expr& e) = 0;
387  //! ~(t1 xnor t2) = t1 xor t2
388  virtual Theorem negBVxnor(const Expr& e) = 0;
389 
390  //! Combine constants in bitwise AND, OR, XOR
391  virtual Theorem bitwiseConst(const Expr& e,
392  const std::vector<int>& idxs,
393  int kind) = 0;
394  //! Lifts concatenation above bitwise operators.
395  virtual Theorem bitwiseConcat(const Expr& e, int kind) = 0;
396  //! Flatten bitwise operation
397  virtual Theorem bitwiseFlatten(const Expr& e, int kind) = 0;
398  //! Simplify bitwise operator containing a constant child
399  /*! \param e is the bit-wise expr
400  * \param idx is the index of the constant bitvector
401  * \param kind is the kind of e
402  */
403  virtual Theorem bitwiseConstElim(const Expr& e, int idx, int kind) = 0;
404 
405  // Concatenation rules
406 
407  //! c1\@c2\@...\@cn = c (concatenation of constant bitvectors)
408  virtual Theorem concatConst(const Expr& e) = 0;
409  //! Flatten one level of nested concatenation, e.g.: x\@(y\@z)\@w = x\@y\@z\@w
410  virtual Theorem concatFlatten(const Expr& e) = 0;
411  //! Merge n-ary concat. of adjacent extractions: x[15:8]\@x[7:0] = x[15:0]
412  virtual Theorem concatMergeExtract(const Expr& e) = 0;
413 
414  ///////////////////////////////////////////////////////////////////
415  ///// Modulo arithmetic rules
416  ///////////////////////////////////////////////////////////////////
417 
418  //! BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)
419  virtual Theorem bvplusConst(const Expr& e) = 0;
420  /*! @brief n*c1 = c, where n >= 0 (multiplication of a constant
421  * bitvector by a non-negative constant) */
422  virtual Theorem bvmultConst(const Expr& e) = 0;
423 
424  ///////////////////////////////////////////////////////////////////
425  ///// Type predicate rules
426  ///////////////////////////////////////////////////////////////////
427 
428  //! |- t=0 OR t=1 for any 1-bit bitvector t
429  virtual Theorem typePredBit(const Expr& e) = 0;
430  //! Expand the type predicate wrapper (compute the actual type predicate)
431  virtual Theorem expandTypePred(const Theorem& tp) = 0;
432 
433  /*Beginning of Lorenzo PLatania's methods*/
434 
435  // virtual Theorem multiply_coeff( Rational mult_inv, const Expr& e)=0;
436 
437  //! isolate a variable with coefficient = 1 on the Lhs of an
438  //equality expression
439  virtual Theorem isolate_var(const Expr& e)=0;
440 
441  // BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)
442  // where n = BVSize(b), a != 0
443  virtual Theorem liftConcatBVMult(const Expr& e)=0;
444 
445  //! canonize BVMult expressions in order to get one coefficient
446  //multiplying the variable(s) in the expression
447  virtual Theorem canonBVMult( const Expr& e )=0;
448 
449  // BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)
450  // where n = BVSize(b)
451  virtual Theorem liftConcatBVPlus(const Expr& e)=0;
452 
453  //! canonize BVPlus expressions in order to get just one
454  //coefficient multiplying each variable in the expression
455  virtual Theorem canonBVPlus( const Expr& e )=0;
456  virtual Theorem canonBVUMinus( const Expr& e )=0;
457  // Input: t[hi:lo] = rhs
458  // if t appears as leaf in rhs, then:
459  // t[hi:lo] = rhs |- Exists x,y,z. (t = x @ y @ z AND y = rhs), solvedForm = false
460  // else
461  // t[hi:lo] = rhs |- Exists x,y,z. (t = x @ rhs @ z AND y = rhs), solvedForm = true
462  virtual Theorem processExtract(const Theorem& e, bool& solvedForm)=0;
463  // normalizes equation
464  virtual Theorem canonBVEQ( const Expr& e, int maxEffort = 3 )=0;
465 
466  //! apply the distributive rule on the BVMULT expression e
467  virtual Theorem distributive_rule( const Expr& e )=0;
468  // virtual Theorem BVMultConstTerm( const Expr& e1, const Expr& e2)=0;
469  // recursively reorder subterms in a BVMULT term
470  virtual Theorem BVMult_order_subterms( const Expr& e ) = 0;
471  // rewrites the equation in the form 0 = Expr
472  // this is needed for TheoryBitvector::solve
473  virtual Theorem MarkNonSolvableEq( const Expr& e) = 0;
474  /*End of Lorenzo PLatania's methods*/
475 
476  // rewrite BVZEROEXTEND into CONCAT
477  virtual Theorem zeroExtendRule(const Expr& e) = 0;
478  // rewrite BVREPEAT into CONCAT
479  virtual Theorem repeatRule(const Expr& e) = 0;
480  // rewrite BVROTL into CONCAT
481  virtual Theorem rotlRule(const Expr& e) = 0;
482  // rewrite BVROTR into CONCAT
483  virtual Theorem rotrRule(const Expr& e) = 0;
484 
485  /**
486  * Divide a with b unsigned and return the bit-vector constant result
487  */
488  virtual Theorem bvUDivConst(const Expr& divExpr) = 0;
489 
490  /**
491  * Rewrite a/b with a fresh variable d and add the constraints to make it be a divider.
492  */
493  virtual Theorem bvUDivTheorem(const Expr& divExpr) = 0;
494 
495  /**
496  * Divide a with b unsigned and return the bit-vector constant result
497  */
498  virtual Theorem bvURemConst(const Expr& remExpr) = 0;
499 
500  /**
501  * Rewrite a%b in terms of a/b, i.e. a - a/b
502  */
503  virtual Theorem bvURemRewrite(const Expr& divExpr) = 0;
504 
505  /**
506  * Rewrite the signed divide in terms of the unsigned one.
507  */
508  virtual Theorem bvSDivRewrite(const Expr& sDivExpr) = 0;
509 
510  /**
511  * Rewrite the signed remainder in terms of the unsigned one.
512  */
513  virtual Theorem bvSRemRewrite(const Expr& sRemExpr) = 0;
514 
515  /**
516  * Rewrite the signed mod in terms of the unsigned one.
517  */
518  virtual Theorem bvSModRewrite(const Expr& sModExpr) = 0;
519 
520  /**
521  * Bit-blast the multiplication a_times_b given the bits in a_bits and b_bits.
522  * The resulting output bits will be in the vector output_bits. The return value
523  * is a theorem saying there is no overflow for this multiplication. (TODO, it's
524  * just an empty theorem for now).
525  */
526  virtual Theorem bitblastBVMult(const std::vector<Theorem>& a_bits,
527  const std::vector<Theorem>& b_bits,
528  const Expr& a_times_b,
529  std::vector<Theorem>& output_bits) = 0;
530 
531  /**
532  * Bit-blast the sum a_times_b given the bits in a_bits and b_bits.
533  * The resulting output bits will be in the vector output_bits. The return value
534  * is a theorem saying there is no overflow for this sum. (TODO, it's
535  * just an empty theorem for now).
536  */
537  virtual Theorem bitblastBVPlus(const std::vector<Theorem>& a_bits,
538  const std::vector<Theorem>& b_bits,
539  const Expr& a_plus_b,
540  std::vector<Theorem>& output_bits) = 0;
541 
542  /**
543  * Rewrite \f[x_1 \vee x_2 \vee \ldots \vee x_n = 0\f] into
544  * \f[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\f].
545  */
546  virtual Theorem zeroBVOR(const Expr& orEqZero) = 0;
547 
548  /**
549  * Rewrite \f[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\f] into
550  * \f[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\f].
551  */
552  virtual Theorem oneBVAND(const Expr& andEqOne) = 0;
553 
554  /**
555  * Equalities over constants go to true/false.
556  */
557  virtual Theorem constEq(const Expr& eq) = 0;
558 
559  /**
560  * Returns true if equation is of the form x[i:j] = x[k:l], where the
561  * extracted segments overlap, i.e. i > j >= k > l or k > i >= l > j.
562  */
563  virtual bool solveExtractOverlapApplies(const Expr& eq) = 0;
564 
565  /**
566  * Returns the theorem that simplifies the equality of two overlapping
567  * extracts over the same term.
568  */
569  virtual Theorem solveExtractOverlap(const Expr& eq) = 0;
570 
571  }; // end of class BitvectorProofRules
572 } // end of name-space CVC3
573 
574 #endif