CVC3
2.4.1
|
#include <bitvector_proof_rules.h>
Public Member Functions | |
virtual | ~BitvectorProofRules () |
virtual Theorem | bitvectorFalseRule (const Theorem &thm)=0 |
virtual Theorem | bitvectorTrueRule (const Theorem &thm)=0 |
virtual Theorem | bitBlastEqnRule (const Expr &e, const Expr &f)=0 |
t1=t2 ==> AND_i(t1[i:i] = t2[i:i]) More... | |
virtual Theorem | bitBlastDisEqnRule (const Theorem &e, const Expr &f)=0 |
t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i]) More... | |
virtual Theorem | signExtendRule (const Expr &e)=0 |
sign extend the input SX(e) appropriately More... | |
virtual Theorem | padBVLTRule (const Expr &e, int len)=0 |
Pad the kids of BVLT/BVLE to make their length equal. More... | |
virtual Theorem | padBVSLTRule (const Expr &e, int len)=0 |
Sign Extend the kids of BVSLT/BVSLE to make their length equal. More... | |
virtual Theorem | signBVLTRule (const Expr &e, const Theorem &topBit0, const Theorem &topBit1)=0 |
virtual Theorem | notBVEQ1Rule (const Expr &e)=0 |
virtual Theorem | notBVLTRule (const Expr &e)=0 |
virtual Theorem | lhsEqRhsIneqn (const Expr &e, int kind)=0 |
if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true) More... | |
virtual Theorem | zeroLeq (const Expr &e)=0 |
virtual Theorem | bvConstIneqn (const Expr &e, int kind)=0 |
virtual Theorem | generalIneqn (const Expr &e, const Theorem &e0, const Theorem &e1, int kind)=0 |
virtual Theorem | bitExtractAllToConstEq (std::vector< Theorem > &thms)=0 |
virtual Theorem | bitExtractToExtract (const Theorem &thm)=0 |
t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0 More... | |
virtual Theorem | bitExtractRewrite (const Expr &x)=0 |
t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i]) More... | |
virtual Theorem | bitExtractConstant (const Expr &x, int i)=0 |
virtual Theorem | bitExtractConcatenation (const Expr &x, int i)=0 |
virtual Theorem | bitExtractConstBVMult (const Expr &t, int i)=0 |
virtual Theorem | bitExtractBVMult (const Expr &t, int i)=0 |
virtual Theorem | bitExtractExtraction (const Expr &x, int i)=0 |
virtual Theorem | bitExtractBVPlus (const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i)=0 |
virtual Theorem | bitExtractBVPlusPreComputed (const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed)=0 |
virtual Theorem | bvPlusAssociativityRule (const Expr &bvPlusTerm)=0 |
virtual Theorem | bitExtractNot (const Expr &x, int i)=0 |
virtual Theorem | bitExtractBitwise (const Expr &x, int i, int kind)=0 |
Extract from bitwise AND, OR, or XOR. More... | |
virtual Theorem | bitExtractFixedLeftShift (const Expr &x, int i)=0 |
virtual Theorem | bitExtractFixedRightShift (const Expr &x, int i)=0 |
virtual Theorem | bitExtractBVSHL (const Expr &x, int i)=0 |
virtual Theorem | bitExtractBVLSHR (const Expr &x, int i)=0 |
virtual Theorem | bitExtractBVASHR (const Expr &x, int i)=0 |
virtual Theorem | zeroPaddingRule (const Expr &e, int r)=0 |
virtual Theorem | bitExtractSXRule (const Expr &e, int i)=0 |
virtual Theorem | eqConst (const Expr &e)=0 |
c1=c2 <=> TRUE/FALSE (equality of constant bitvectors) More... | |
virtual Theorem | eqToBits (const Theorem &eq)=0 |
|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits More... | |
virtual Theorem | leftShiftToConcat (const Expr &e)=0 |
t<<n = c @ 0bin00...00, takes e == (t<<n) More... | |
virtual Theorem | constWidthLeftShiftToConcat (const Expr &e)=0 |
t<<n = c @ 0bin00...00, takes e == (t<<n) More... | |
virtual Theorem | rightShiftToConcat (const Expr &e)=0 |
t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n) More... | |
virtual Theorem | bvshlToConcat (const Expr &e)=0 |
BVSHL(t,c) = t[n-c,0] @ 0bin00...00. More... | |
virtual Theorem | bvshlSplit (const Expr &e)=0 |
BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ... More... | |
virtual Theorem | bvlshrToConcat (const Expr &e)=0 |
BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]. More... | |
virtual Theorem | bvShiftZero (const Expr &e)=0 |
Any shift over a zero = 0. More... | |
virtual Theorem | bvashrToConcat (const Expr &e)=0 |
BVASHR(t,c) = SX(t[n-1,c], n-1) More... | |
virtual Theorem | rewriteXNOR (const Expr &e)=0 |
a XNOR b <=> (~a & ~b) | (a & b) More... | |
virtual Theorem | rewriteNAND (const Expr &e)=0 |
a NAND b <=> ~(a & b) More... | |
virtual Theorem | rewriteNOR (const Expr &e)=0 |
a NOR b <=> ~(a | b) More... | |
virtual Theorem | rewriteBVCOMP (const Expr &e)=0 |
BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0) More... | |
virtual Theorem | rewriteBVSub (const Expr &e)=0 |
a - b <=> a + (-b) More... | |
virtual Theorem | constMultToPlus (const Expr &e)=0 |
k*t = BVPLUS(n, <sum of shifts of t>) – translation of k*t to BVPLUS More... | |
virtual Theorem | bvplusZeroConcatRule (const Expr &e)=0 |
0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args) More... | |
virtual Theorem | zeroCoeffBVMult (const Expr &e)=0 |
virtual Theorem | oneCoeffBVMult (const Expr &e)=0 |
virtual Theorem | flipBVMult (const Expr &e)=0 |
virtual Theorem | padBVPlus (const Expr &e)=0 |
Make args the same length as the result (zero-extend) More... | |
virtual Theorem | padBVMult (const Expr &e)=0 |
Make args the same length as the result (zero-extend) More... | |
virtual Theorem | bvConstMultAssocRule (const Expr &e)=0 |
virtual Theorem | bvMultAssocRule (const Expr &e)=0 |
virtual Theorem | bvMultDistRule (const Expr &e)=0 |
virtual Theorem | flattenBVPlus (const Expr &e)=0 |
virtual Theorem | combineLikeTermsRule (const Expr &e)=0 |
virtual Theorem | lhsMinusRhsRule (const Expr &e)=0 |
virtual Theorem | extractBVMult (const Expr &e)=0 |
(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n More... | |
virtual Theorem | extractBVPlus (const Expr &e)=0 |
(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n More... | |
virtual Theorem | iteExtractRule (const Expr &e)=0 |
ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j]) More... | |
virtual Theorem | iteBVnegRule (const Expr &e)=0 |
~ite(c,t1,t2) <=> ite(c,~t1,~t2) More... | |
virtual Theorem | bvuminusBVConst (const Expr &e)=0 |
virtual Theorem | bvuminusBVMult (const Expr &e)=0 |
virtual Theorem | bvuminusBVUminus (const Expr &e)=0 |
virtual Theorem | bvuminusVar (const Expr &e)=0 |
virtual Theorem | bvmultBVUminus (const Expr &e)=0 |
virtual Theorem | bvuminusToBVPlus (const Expr &e)=0 |
-t <==> ~t+1 More... | |
virtual Theorem | bvuminusBVPlus (const Expr &e)=0 |
-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn)) More... | |
virtual Theorem | extractConst (const Expr &e)=0 |
c1[i:j] = c (extraction from a constant bitvector) More... | |
virtual Theorem | extractWhole (const Expr &e)=0 |
t[n-1:0] = t for n-bit t More... | |
virtual Theorem | extractExtract (const Expr &e)=0 |
t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction) More... | |
virtual Theorem | extractConcat (const Expr &e)=0 |
(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat) More... | |
virtual Theorem | extractAnd (const Expr &e)=0 |
(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR) More... | |
virtual Theorem | extractOr (const Expr &e)=0 |
(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND) More... | |
virtual Theorem | extractNeg (const Expr &e)=0 |
(~t)[i:j] = ~(t[i:j]) (push extraction through NEG) More... | |
virtual Theorem | extractBitwise (const Expr &e, int kind, const std::string &name)=0 |
Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j]. More... | |
virtual Theorem | negConst (const Expr &e)=0 |
~c1 = c (bit-wise negation of a constant bitvector) More... | |
virtual Theorem | negConcat (const Expr &e)=0 |
~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat More... | |
virtual Theorem | negNeg (const Expr &e)=0 |
~(~t) = t – eliminate double negation More... | |
virtual Theorem | negElim (const Expr &e)=0 |
~t = -1*t + 1 – eliminate negation More... | |
virtual Theorem | negBVand (const Expr &e)=0 |
~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws More... | |
virtual Theorem | negBVor (const Expr &e)=0 |
~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws More... | |
virtual Theorem | negBVxor (const Expr &e)=0 |
~(t1 xor t2) = ~t1 xor t2 More... | |
virtual Theorem | negBVxnor (const Expr &e)=0 |
~(t1 xnor t2) = t1 xor t2 More... | |
virtual Theorem | bitwiseConst (const Expr &e, const std::vector< int > &idxs, int kind)=0 |
Combine constants in bitwise AND, OR, XOR. More... | |
virtual Theorem | bitwiseConcat (const Expr &e, int kind)=0 |
Lifts concatenation above bitwise operators. More... | |
virtual Theorem | bitwiseFlatten (const Expr &e, int kind)=0 |
Flatten bitwise operation. More... | |
virtual Theorem | bitwiseConstElim (const Expr &e, int idx, int kind)=0 |
Simplify bitwise operator containing a constant child. More... | |
virtual Theorem | concatConst (const Expr &e)=0 |
c1@c2@...@cn = c (concatenation of constant bitvectors) More... | |
virtual Theorem | concatFlatten (const Expr &e)=0 |
Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w. More... | |
virtual Theorem | concatMergeExtract (const Expr &e)=0 |
Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0]. More... | |
virtual Theorem | bvplusConst (const Expr &e)=0 |
BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors) More... | |
virtual Theorem | bvmultConst (const Expr &e)=0 |
n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant) More... | |
virtual Theorem | typePredBit (const Expr &e)=0 |
|- t=0 OR t=1 for any 1-bit bitvector t More... | |
virtual Theorem | expandTypePred (const Theorem &tp)=0 |
Expand the type predicate wrapper (compute the actual type predicate) More... | |
virtual Theorem | isolate_var (const Expr &e)=0 |
isolate a variable with coefficient = 1 on the Lhs of an More... | |
virtual Theorem | liftConcatBVMult (const Expr &e)=0 |
virtual Theorem | canonBVMult (const Expr &e)=0 |
canonize BVMult expressions in order to get one coefficient More... | |
virtual Theorem | liftConcatBVPlus (const Expr &e)=0 |
virtual Theorem | canonBVPlus (const Expr &e)=0 |
canonize BVPlus expressions in order to get just one More... | |
virtual Theorem | canonBVUMinus (const Expr &e)=0 |
virtual Theorem | processExtract (const Theorem &e, bool &solvedForm)=0 |
virtual Theorem | canonBVEQ (const Expr &e, int maxEffort=3)=0 |
virtual Theorem | distributive_rule (const Expr &e)=0 |
apply the distributive rule on the BVMULT expression e More... | |
virtual Theorem | BVMult_order_subterms (const Expr &e)=0 |
virtual Theorem | MarkNonSolvableEq (const Expr &e)=0 |
virtual Theorem | zeroExtendRule (const Expr &e)=0 |
virtual Theorem | repeatRule (const Expr &e)=0 |
virtual Theorem | rotlRule (const Expr &e)=0 |
virtual Theorem | rotrRule (const Expr &e)=0 |
virtual Theorem | bvUDivConst (const Expr &divExpr)=0 |
virtual Theorem | bvUDivTheorem (const Expr &divExpr)=0 |
virtual Theorem | bvURemConst (const Expr &remExpr)=0 |
virtual Theorem | bvURemRewrite (const Expr &divExpr)=0 |
virtual Theorem | bvSDivRewrite (const Expr &sDivExpr)=0 |
virtual Theorem | bvSRemRewrite (const Expr &sRemExpr)=0 |
virtual Theorem | bvSModRewrite (const Expr &sModExpr)=0 |
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)=0 |
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)=0 |
virtual Theorem | zeroBVOR (const Expr &orEqZero)=0 |
virtual Theorem | oneBVAND (const Expr &andEqOne)=0 |
virtual Theorem | constEq (const Expr &eq)=0 |
virtual bool | solveExtractOverlapApplies (const Expr &eq)=0 |
virtual Theorem | solveExtractOverlap (const Expr &eq)=0 |
Definition at line 33 of file bitvector_proof_rules.h.
|
inlinevirtual |
Definition at line 36 of file bitvector_proof_rules.h.
thm | input theorem: (e1[i]<=>e2[i])<=>false |
Implemented in CVC3::BitvectorTheoremProducer.
thm | input theorem: (~e1[i]<=>e2[i])<=>true |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
t1=t2 ==> AND_i(t1[i:i] = t2[i:i])
e | is a Expr(t1=t2) |
f | is the resulting expression AND_i(t1[i:i] = t2[i:i]) is passed to the rule for efficiency. |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i])
e | is a Theorem(t1/=t2) |
f | is the resulting expression OR_i(NOT t1[i]<=>t2[i]), passed to the rule for efficiency. |
Implemented in CVC3::BitvectorTheoremProducer.
sign extend the input SX(e) appropriately
Implemented in CVC3::BitvectorTheoremProducer.
Pad the kids of BVLT/BVLE to make their length equal.
Implemented in CVC3::BitvectorTheoremProducer.
Sign Extend the kids of BVSLT/BVSLE to make their length equal.
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
input: e0 <=(s) e1. output depends on whether the topbits(MSB) of e0 and e1 are constants. If they are constants then optimizations are done, otherwise the following rule is implemented.
e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0])
Implemented in CVC3::BitvectorTheoremProducer.
NOT(e[0][0] = e[0][1]) <==> e[0][0] = ~e[0][1]
Implemented in CVC3::BitvectorTheoremProducer.
NOT(e[0][0] < e[0][1]) <==> (e[0][1] <= e[0][0]), NOT(e[0][0] <= e[0][1]) <==> (e[0][1] < e[0][0])
Implemented in CVC3::BitvectorTheoremProducer.
if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Implemented in CVC3::BitvectorTheoremProducer.
Referenced by CVC3::TheoryBitvector::comparebv().
t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0
thm | is a Theorem(t[i]) or Theorem(NOT t[i]), where t[i] is BOOLEXTRACT(t, i). |
Implemented in CVC3::BitvectorTheoremProducer.
t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
x | is bitvector constant |
i | is extracted bitposition |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
x | is bitvector binary concatenation |
i | is extracted bitposition |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
t | is bitvector binary BVMULT. x[0] must be BVCONST |
i | is extracted bitposition |
Implemented in CVC3::BitvectorTheoremProducer.
t | : input1 is bitvector binary BVMULT. t[0] must not be BVCONST |
i | : input2 is extracted bitposition |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
x | is bitvector extraction e[k:j] |
i | is extracted bitposition |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
t1 | is vector of bitblasts of t, from bit i-1 to 0 |
t2 | is vector of bitblasts of q, from bit i-1 to 0 |
bvPlusTerm | is BVPLUS term: BVPLUS(n,t,q) |
i | is extracted bitposition |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
bvPlusTerm | : input1 is bvPlusTerm, a BVPLUS term with arity > 2 |
Implemented in CVC3::BitvectorTheoremProducer.
x | : input1 is bitwise NEGATION |
i | : input2 is extracted bitposition |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Extract from bitwise AND, OR, or XOR.
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
x | : input1 is bitvector FIXED SHIFT
|
i | : input2 is extracted bitposition |
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
e | : input1 is bitvector term |
r | : input2 is extracted bitposition |
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
Implemented in CVC3::BitvectorTheoremProducer.
|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
Implemented in CVC3::BitvectorTheoremProducer.
t<<n = c @ 0bin00...00, takes e == (t<<n)
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
t<<n = c @ 0bin00...00, takes e == (t<<n)
Implemented in CVC3::BitvectorTheoremProducer.
t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
Implemented in CVC3::BitvectorTheoremProducer.
BVSHL(t,c) = t[n-c,0] @ 0bin00...00.
Implemented in CVC3::BitvectorTheoremProducer.
BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
Implemented in CVC3::BitvectorTheoremProducer.
BVLSHR(t,c) = 0bin00...00 @ t[n-1,c].
Implemented in CVC3::BitvectorTheoremProducer.
Any shift over a zero = 0.
Implemented in CVC3::BitvectorTheoremProducer.
BVASHR(t,c) = SX(t[n-1,c], n-1)
Implemented in CVC3::BitvectorTheoremProducer.
a XNOR b <=> (~a & ~b) | (a & b)
Implemented in CVC3::BitvectorTheoremProducer.
a NAND b <=> ~(a & b)
Implemented in CVC3::BitvectorTheoremProducer.
a NOR b <=> ~(a | b)
Implemented in CVC3::BitvectorTheoremProducer.
BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
Implemented in CVC3::BitvectorTheoremProducer.
a - b <=> a + (-b)
Implemented in CVC3::BitvectorTheoremProducer.
k*t = BVPLUS(n, <sum of shifts of t>) – translation of k*t to BVPLUS
If k = 2^m, return k*t = t@0...0
Implemented in CVC3::BitvectorTheoremProducer.
0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
provided that m+ceil(log2(l)) <= n, where k is the size of the 0bin0...0, m is the max. length of each argument, and l is the number of arguments.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Make args the same length as the result (zero-extend)
Implemented in CVC3::BitvectorTheoremProducer.
Make args the same length as the result (zero-extend)
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n
Implemented in CVC3::BitvectorTheoremProducer.
(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n
Implemented in CVC3::BitvectorTheoremProducer.
ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
Implemented in CVC3::BitvectorTheoremProducer.
~ite(c,t1,t2) <=> ite(c,~t1,~t2)
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
-t <==> ~t+1
Implemented in CVC3::BitvectorTheoremProducer.
-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
Implemented in CVC3::BitvectorTheoremProducer.
c1[i:j] = c (extraction from a constant bitvector)
Implemented in CVC3::BitvectorTheoremProducer.
t[n-1:0] = t for n-bit t
Implemented in CVC3::BitvectorTheoremProducer.
t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)
Implemented in CVC3::BitvectorTheoremProducer.
(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
Implemented in CVC3::BitvectorTheoremProducer.
(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)
Implemented in CVC3::BitvectorTheoremProducer.
(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)
Implemented in CVC3::BitvectorTheoremProducer.
(~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j].
Implemented in CVC3::BitvectorTheoremProducer.
~c1 = c (bit-wise negation of a constant bitvector)
Implemented in CVC3::BitvectorTheoremProducer.
~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat
Implemented in CVC3::BitvectorTheoremProducer.
~(~t) = t – eliminate double negation
Implemented in CVC3::BitvectorTheoremProducer.
~t = -1*t + 1 – eliminate negation
Implemented in CVC3::BitvectorTheoremProducer.
~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws
Implemented in CVC3::BitvectorTheoremProducer.
~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws
Implemented in CVC3::BitvectorTheoremProducer.
~(t1 xor t2) = ~t1 xor t2
Implemented in CVC3::BitvectorTheoremProducer.
~(t1 xnor t2) = t1 xor t2
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Combine constants in bitwise AND, OR, XOR.
Implemented in CVC3::BitvectorTheoremProducer.
Lifts concatenation above bitwise operators.
Implemented in CVC3::BitvectorTheoremProducer.
Flatten bitwise operation.
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Simplify bitwise operator containing a constant child.
e | is the bit-wise expr |
idx | is the index of the constant bitvector |
kind | is the kind of e |
Implemented in CVC3::BitvectorTheoremProducer.
c1@c2@...@cn = c (concatenation of constant bitvectors)
Implemented in CVC3::BitvectorTheoremProducer.
Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w.
Implemented in CVC3::BitvectorTheoremProducer.
Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0].
Implemented in CVC3::BitvectorTheoremProducer.
BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)
Implemented in CVC3::BitvectorTheoremProducer.
n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant)
Implemented in CVC3::BitvectorTheoremProducer.
|- t=0 OR t=1 for any 1-bit bitvector t
Implemented in CVC3::BitvectorTheoremProducer.
Expand the type predicate wrapper (compute the actual type predicate)
Implemented in CVC3::BitvectorTheoremProducer.
isolate a variable with coefficient = 1 on the Lhs of an
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
canonize BVMult expressions in order to get one coefficient
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
canonize BVPlus expressions in order to get just one
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Implemented in CVC3::BitvectorTheoremProducer.
Referenced by CVC3::TheoryBitvector::solve().
|
pure virtual |
Implemented in CVC3::BitvectorTheoremProducer.
Referenced by CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryBitvector::simplifyPendingEq(), and CVC3::TheoryBitvector::solve().
apply the distributive rule on the BVMULT expression e
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Implemented in CVC3::BitvectorTheoremProducer.
Divide a with b unsigned and return the bit-vector constant result
Implemented in CVC3::BitvectorTheoremProducer.
Rewrite a/b with a fresh variable d and add the constraints to make it be a divider.
Implemented in CVC3::BitvectorTheoremProducer.
Divide a with b unsigned and return the bit-vector constant result
Implemented in CVC3::BitvectorTheoremProducer.
Rewrite ab in terms of a/b, i.e. a - a/b
Implemented in CVC3::BitvectorTheoremProducer.
Rewrite the signed divide in terms of the unsigned one.
Implemented in CVC3::BitvectorTheoremProducer.
Rewrite the signed remainder in terms of the unsigned one.
Implemented in CVC3::BitvectorTheoremProducer.
Rewrite the signed mod in terms of the unsigned one.
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Bit-blast the multiplication a_times_b given the bits in a_bits and b_bits. The resulting output bits will be in the vector output_bits. The return value is a theorem saying there is no overflow for this multiplication. (TODO, it's just an empty theorem for now).
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Bit-blast the sum a_times_b given the bits in a_bits and b_bits. The resulting output bits will be in the vector output_bits. The return value is a theorem saying there is no overflow for this sum. (TODO, it's just an empty theorem for now).
Implemented in CVC3::BitvectorTheoremProducer.
Equalities over constants go to true/false.
Implemented in CVC3::BitvectorTheoremProducer.
|
pure virtual |
Returns true if equation is of the form x[i:j] = x[k:l], where the extracted segments overlap, i.e. i > j >= k > l or k > i >= l > j.
Implemented in CVC3::BitvectorTheoremProducer.
Referenced by CVC3::TheoryBitvector::solve().
Returns the theorem that simplifies the equality of two overlapping extracts over the same term.
Implemented in CVC3::BitvectorTheoremProducer.
Referenced by CVC3::TheoryBitvector::solve().