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