22 #ifndef _cvc3__bitvector_theorem_producer_h_
23 #define _cvc3__bitvector_theorem_producer_h_
30 class TheoryBitvector;
74 std::vector<Expr> & result);
80 const std::vector<Expr>& elements);
176 const Theorem& rhs_i,
int kind);
248 const std::vector<Theorem>& t2,
249 const Expr& bvPlusTerm,
int i);
253 const Expr& bvPlusTerm,
504 const std::vector<Theorem>& t2BitExtractThms,
510 int precomputedFlag);
601 const std::vector<Theorem>& b_bits,
602 const Expr& a_times_b,
603 std::vector<Theorem>& output_bits);
612 const std::vector<Theorem>& b_bits,
613 const Expr& a_plus_b,
614 std::vector<Theorem>& output_bits);
TheoryBitvector * d_theoryBitvector
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.
virtual Theorem bvUDivTheorem(const Expr &divExpr)
const Expr & bvZero() const
Return cached constant 0bin0.
Theorem combineLikeTermsRule(const Expr &e)
~BitvectorTheoremProducer()
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 zeroCoeffBVMult(const Expr &e)
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
bool okToSplit(const Expr &e)
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 lhsMinusRhsRule(const Expr &e)
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)
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 solveExtractOverlap(const Expr &eq)
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)
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
bool solveExtractOverlapApplies(const Expr &eq)
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)
Theorem notBVEQ1Rule(const Expr &e)
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 notBVLTRule(const Expr &e)
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)
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 oneCoeffBVMult(const Expr &e)
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].