22 #ifndef _cvc3__bitvector_proof_rules_h_
23 #define _cvc3__bitvector_proof_rules_h_
116 const Theorem& e1,
int kind) = 0;
195 const std::vector<Theorem>& t2,
196 const Expr& bvPlusTerm,
int i) = 0;
201 const Expr& bvPlusTerm,
203 int precomputed) = 0;
369 int kind,
const std::string& name) = 0;
392 const std::vector<int>& idxs,
527 const std::vector<Theorem>& b_bits,
528 const Expr& a_times_b,
529 std::vector<Theorem>& output_bits) = 0;
538 const std::vector<Theorem>& b_bits,
539 const Expr& a_plus_b,
540 std::vector<Theorem>& output_bits) = 0;
virtual Theorem bvConstMultAssocRule(const Expr &e)=0
virtual Theorem iteExtractRule(const Expr &e)=0
ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
virtual Theorem bitwiseFlatten(const Expr &e, int kind)=0
Flatten bitwise operation.
virtual Theorem bvuminusToBVPlus(const Expr &e)=0
-t <==> ~t+1
virtual Theorem rewriteXNOR(const Expr &e)=0
a XNOR b <=> (~a & ~b) | (a & b)
virtual Theorem bitExtractBVSHL(const Expr &x, int i)=0
virtual Theorem bitExtractConstBVMult(const Expr &t, int i)=0
Data structure of expressions in CVC3.
virtual Theorem bitExtractBVASHR(const Expr &x, int i)=0
virtual Theorem bitExtractBVPlusPreComputed(const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed)=0
virtual Theorem bitExtractBitwise(const Expr &x, int i, int kind)=0
Extract from bitwise AND, OR, or XOR.
virtual Theorem extractBVPlus(const Expr &e)=0
(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n
virtual Theorem bitExtractAllToConstEq(std::vector< Theorem > &thms)=0
virtual Theorem bitExtractBVPlus(const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i)=0
virtual Theorem bvshlSplit(const Expr &e)=0
BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
virtual Theorem bitExtractSXRule(const Expr &e, int i)=0
virtual Theorem bitExtractBVLSHR(const Expr &x, int i)=0
virtual Theorem concatMergeExtract(const Expr &e)=0
Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0].
virtual Theorem distributive_rule(const Expr &e)=0
apply the distributive rule on the BVMULT expression e
virtual ~BitvectorProofRules()
virtual Theorem bitwiseConstElim(const Expr &e, int idx, int kind)=0
Simplify bitwise operator containing a constant child.
virtual Theorem typePredBit(const Expr &e)=0
|- t=0 OR t=1 for any 1-bit bitvector t
virtual Theorem bvuminusVar(const Expr &e)=0
virtual Theorem negNeg(const Expr &e)=0
~(~t) = t – eliminate double negation
virtual Theorem bvuminusBVUminus(const Expr &e)=0
virtual Theorem MarkNonSolvableEq(const Expr &e)=0
virtual Theorem bvlshrToConcat(const Expr &e)=0
BVLSHR(t,c) = 0bin00...00 @ t[n-1,c].
virtual Theorem negConcat(const Expr &e)=0
~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat
virtual Theorem liftConcatBVPlus(const Expr &e)=0
virtual Theorem rotlRule(const Expr &e)=0
virtual Theorem flipBVMult(const Expr &e)=0
virtual Theorem bvshlToConcat(const Expr &e)=0
BVSHL(t,c) = t[n-c,0] @ 0bin00...00.
virtual Theorem notBVEQ1Rule(const Expr &e)=0
virtual Theorem negBVand(const Expr &e)=0
~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws
virtual Theorem padBVLTRule(const Expr &e, int len)=0
Pad the kids of BVLT/BVLE to make their length equal.
virtual Theorem extractExtract(const Expr &e)=0
t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)
virtual Theorem bitExtractFixedRightShift(const Expr &x, int i)=0
virtual Theorem negElim(const Expr &e)=0
~t = -1*t + 1 – eliminate negation
virtual Theorem negBVor(const Expr &e)=0
~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws
virtual Theorem expandTypePred(const Theorem &tp)=0
Expand the type predicate wrapper (compute the actual type predicate)
virtual Theorem zeroLeq(const Expr &e)=0
virtual Theorem bvuminusBVConst(const Expr &e)=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 isolate_var(const Expr &e)=0
isolate a variable with coefficient = 1 on the Lhs of an
virtual Theorem bvUDivConst(const Expr &divExpr)=0
virtual Theorem iteBVnegRule(const Expr &e)=0
~ite(c,t1,t2) <=> ite(c,~t1,~t2)
virtual Theorem extractWhole(const Expr &e)=0
t[n-1:0] = t for n-bit t
virtual Theorem rotrRule(const Expr &e)=0
virtual Theorem bvuminusBVPlus(const Expr &e)=0
-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
virtual Theorem eqConst(const Expr &e)=0
c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
virtual Theorem rightShiftToConcat(const Expr &e)=0
t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
virtual Theorem canonBVEQ(const Expr &e, int maxEffort=3)=0
virtual Theorem generalIneqn(const Expr &e, const Theorem &e0, const Theorem &e1, int kind)=0
virtual Theorem bvmultBVUminus(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)
virtual Theorem extractNeg(const Expr &e)=0
(~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
virtual Theorem zeroPaddingRule(const Expr &e, int r)=0
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].
virtual Theorem extractOr(const Expr &e)=0
(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)
virtual Theorem eqToBits(const Theorem &eq)=0
|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
virtual Theorem bitExtractConstant(const Expr &x, int i)=0
virtual Theorem bitExtractToExtract(const Theorem &thm)=0
t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0
virtual Theorem oneBVAND(const Expr &andEqOne)=0
virtual Theorem bitBlastDisEqnRule(const Theorem &e, const Expr &f)=0
t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i])
virtual Theorem bvSDivRewrite(const Expr &sDivExpr)=0
virtual Theorem bitExtractNot(const Expr &x, int i)=0
virtual Theorem rewriteNAND(const Expr &e)=0
a NAND b <=> ~(a & b)
virtual Theorem bitExtractFixedLeftShift(const Expr &x, int i)=0
virtual Theorem padBVPlus(const Expr &e)=0
Make args the same length as the result (zero-extend)
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 signExtendRule(const Expr &e)=0
sign extend the input SX(e) appropriately
virtual Theorem notBVLTRule(const Expr &e)=0
virtual Theorem canonBVPlus(const Expr &e)=0
canonize BVPlus expressions in order to get just one
virtual Theorem zeroBVOR(const Expr &orEqZero)=0
virtual Theorem zeroExtendRule(const Expr &e)=0
virtual Theorem negConst(const Expr &e)=0
~c1 = c (bit-wise negation of a constant bitvector)
virtual Theorem bitwiseConcat(const Expr &e, int kind)=0
Lifts concatenation above bitwise operators.
virtual Theorem signBVLTRule(const Expr &e, const Theorem &topBit0, const Theorem &topBit1)=0
virtual Theorem extractConcat(const Expr &e)=0
(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
virtual Theorem combineLikeTermsRule(const Expr &e)=0
virtual Theorem constWidthLeftShiftToConcat(const Expr &e)=0
t<
virtual Theorem canonBVMult(const Expr &e)=0
canonize BVMult expressions in order to get one coefficient
virtual Theorem solveExtractOverlap(const Expr &eq)=0
virtual Theorem bvMultAssocRule(const Expr &e)=0
virtual Theorem padBVMult(const Expr &e)=0
Make args the same length as the result (zero-extend)
virtual Theorem bvURemConst(const Expr &remExpr)=0
virtual Theorem zeroCoeffBVMult(const Expr &e)=0
virtual Theorem bitBlastEqnRule(const Expr &e, const Expr &f)=0
t1=t2 ==> AND_i(t1[i:i] = t2[i:i])
virtual Theorem bvConstIneqn(const Expr &e, int kind)=0
virtual Theorem oneCoeffBVMult(const Expr &e)=0
virtual Theorem bitExtractConcatenation(const Expr &x, int i)=0
virtual Theorem rewriteBVCOMP(const Expr &e)=0
BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
virtual Theorem concatFlatten(const Expr &e)=0
Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w.
virtual Theorem flattenBVPlus(const Expr &e)=0
virtual Theorem bitExtractRewrite(const Expr &x)=0
t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])
virtual bool solveExtractOverlapApplies(const Expr &eq)=0
virtual Theorem lhsMinusRhsRule(const Expr &e)=0
virtual Theorem canonBVUMinus(const Expr &e)=0
virtual Theorem liftConcatBVMult(const Expr &e)=0
virtual Theorem constMultToPlus(const Expr &e)=0
k*t = BVPLUS(n, ) – translation of k*t to BVPLUS
virtual Theorem negBVxnor(const Expr &e)=0
~(t1 xnor t2) = t1 xor t2
virtual Theorem BVMult_order_subterms(const Expr &e)=0
virtual Theorem rewriteBVSub(const Expr &e)=0
a - b <=> a + (-b)
virtual Theorem bvmultConst(const Expr &e)=0
n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant) ...
virtual Theorem bitExtractBVMult(const Expr &t, int i)=0
virtual Theorem negBVxor(const Expr &e)=0
~(t1 xor t2) = ~t1 xor t2
virtual Theorem extractConst(const Expr &e)=0
c1[i:j] = c (extraction from a constant bitvector)
virtual Theorem bvplusZeroConcatRule(const Expr &e)=0
0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
virtual Theorem bvashrToConcat(const Expr &e)=0
BVASHR(t,c) = SX(t[n-1,c], n-1)
virtual Theorem bvPlusAssociativityRule(const Expr &bvPlusTerm)=0
virtual Theorem bitExtractExtraction(const Expr &x, int i)=0
virtual Theorem concatConst(const Expr &e)=0
c1@c2@...@cn = c (concatenation of constant bitvectors)
virtual Theorem processExtract(const Theorem &e, bool &solvedForm)=0
virtual Theorem bvuminusBVMult(const Expr &e)=0
virtual Theorem bvShiftZero(const Expr &e)=0
Any shift over a zero = 0.
virtual Theorem padBVSLTRule(const Expr &e, int len)=0
Sign Extend the kids of BVSLT/BVSLE to make their length equal.
virtual Theorem bvplusConst(const Expr &e)=0
BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)
virtual Theorem bitvectorFalseRule(const Theorem &thm)=0
virtual Theorem bvSRemRewrite(const Expr &sRemExpr)=0
virtual Theorem constEq(const Expr &eq)=0
virtual Theorem bitvectorTrueRule(const Theorem &thm)=0
virtual Theorem bvURemRewrite(const Expr &divExpr)=0
virtual Theorem bvUDivTheorem(const Expr &divExpr)=0
virtual Theorem bitwiseConst(const Expr &e, const std::vector< int > &idxs, int kind)=0
Combine constants in bitwise AND, OR, XOR.
virtual Theorem repeatRule(const Expr &e)=0
virtual Theorem extractAnd(const Expr &e)=0
(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)
virtual Theorem leftShiftToConcat(const Expr &e)=0
t<
virtual Theorem extractBVMult(const Expr &e)=0
(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n
virtual Theorem rewriteNOR(const Expr &e)=0
a NOR b <=> ~(a | b)
virtual Theorem bvSModRewrite(const Expr &sModExpr)=0
virtual Theorem bvMultDistRule(const Expr &e)=0