CVC3
Public Member Functions | List of all members
CVC3::BitvectorProofRules Class Referenceabstract

#include <bitvector_proof_rules.h>

Inherited by CVC3::BitvectorTheoremProducer.

Collaboration diagram for CVC3::BitvectorProofRules:
Collaboration graph

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])
 
virtual Theorem bitBlastDisEqnRule (const Theorem &e, const Expr &f)=0
 t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i])
 
virtual Theorem signExtendRule (const Expr &e)=0
 sign extend the input SX(e) appropriately
 
virtual Theorem padBVLTRule (const Expr &e, int len)=0
 Pad the kids of BVLT/BVLE to make their length equal.
 
virtual Theorem padBVSLTRule (const Expr &e, int len)=0
 Sign Extend the kids of BVSLT/BVSLE to make their length equal.
 
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)
 
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
 
virtual Theorem bitExtractRewrite (const Expr &x)=0
 t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])
 
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.
 
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)
 
virtual Theorem eqToBits (const Theorem &eq)=0
 |- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
 
virtual Theorem leftShiftToConcat (const Expr &e)=0
 t<<n = c @ 0bin00...00, takes e == (t<<n)
 
virtual Theorem constWidthLeftShiftToConcat (const Expr &e)=0
 t<<n = c @ 0bin00...00, takes e == (t<<n)
 
virtual Theorem rightShiftToConcat (const Expr &e)=0
 t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
 
virtual Theorem bvshlToConcat (const Expr &e)=0
 BVSHL(t,c) = t[n-c,0] @ 0bin00...00.
 
virtual Theorem bvshlSplit (const Expr &e)=0
 BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
 
virtual Theorem bvlshrToConcat (const Expr &e)=0
 BVLSHR(t,c) = 0bin00...00 @ t[n-1,c].
 
virtual Theorem bvShiftZero (const Expr &e)=0
 Any shift over a zero = 0.
 
virtual Theorem bvashrToConcat (const Expr &e)=0
 BVASHR(t,c) = SX(t[n-1,c], n-1)
 
virtual Theorem rewriteXNOR (const Expr &e)=0
 a XNOR b <=> (~a & ~b) | (a & b)
 
virtual Theorem rewriteNAND (const Expr &e)=0
 a NAND b <=> ~(a & b)
 
virtual Theorem rewriteNOR (const Expr &e)=0
 a NOR b <=> ~(a | b)
 
virtual Theorem rewriteBVCOMP (const Expr &e)=0
 BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
 
virtual Theorem rewriteBVSub (const Expr &e)=0
 a - b <=> a + (-b)
 
virtual Theorem constMultToPlus (const Expr &e)=0
 k*t = BVPLUS(n, <sum of shifts of t>) – translation of k*t to BVPLUS
 
virtual Theorem bvplusZeroConcatRule (const Expr &e)=0
 0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
 
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)
 
virtual Theorem padBVMult (const Expr &e)=0
 Make args the same length as the result (zero-extend)
 
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
 
virtual Theorem extractBVPlus (const Expr &e)=0
 (x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n
 
virtual Theorem iteExtractRule (const Expr &e)=0
 ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
 
virtual Theorem iteBVnegRule (const Expr &e)=0
 ~ite(c,t1,t2) <=> ite(c,~t1,~t2)
 
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
 
virtual Theorem bvuminusBVPlus (const Expr &e)=0
 -(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
 
virtual Theorem extractConst (const Expr &e)=0
 c1[i:j] = c (extraction from a constant bitvector)
 
virtual Theorem extractWhole (const Expr &e)=0
 t[n-1:0] = t for n-bit t
 
virtual Theorem extractExtract (const Expr &e)=0
 t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)
 
virtual Theorem extractConcat (const Expr &e)=0
 (t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
 
virtual Theorem extractAnd (const Expr &e)=0
 (t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)
 
virtual Theorem extractOr (const Expr &e)=0
 (t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)
 
virtual Theorem extractNeg (const Expr &e)=0
 (~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
 
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 negConst (const Expr &e)=0
 ~c1 = c (bit-wise negation of a constant bitvector)
 
virtual Theorem negConcat (const Expr &e)=0
 ~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat
 
virtual Theorem negNeg (const Expr &e)=0
 ~(~t) = t – eliminate double negation
 
virtual Theorem negElim (const Expr &e)=0
 ~t = -1*t + 1 – eliminate negation
 
virtual Theorem negBVand (const Expr &e)=0
 ~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws
 
virtual Theorem negBVor (const Expr &e)=0
 ~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws
 
virtual Theorem negBVxor (const Expr &e)=0
 ~(t1 xor t2) = ~t1 xor t2
 
virtual Theorem negBVxnor (const Expr &e)=0
 ~(t1 xnor t2) = t1 xor t2
 
virtual Theorem bitwiseConst (const Expr &e, const std::vector< int > &idxs, int kind)=0
 Combine constants in bitwise AND, OR, XOR.
 
virtual Theorem bitwiseConcat (const Expr &e, int kind)=0
 Lifts concatenation above bitwise operators.
 
virtual Theorem bitwiseFlatten (const Expr &e, int kind)=0
 Flatten bitwise operation.
 
virtual Theorem bitwiseConstElim (const Expr &e, int idx, int kind)=0
 Simplify bitwise operator containing a constant child.
 
virtual Theorem concatConst (const Expr &e)=0
 c1@c2@...@cn = c (concatenation of constant bitvectors)
 
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 concatMergeExtract (const Expr &e)=0
 Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0].
 
virtual Theorem bvplusConst (const Expr &e)=0
 BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)
 
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 typePredBit (const Expr &e)=0
 |- t=0 OR t=1 for any 1-bit bitvector t
 
virtual Theorem expandTypePred (const Theorem &tp)=0
 Expand the type predicate wrapper (compute the actual type predicate)
 
virtual Theorem isolate_var (const Expr &e)=0
 isolate a variable with coefficient = 1 on the Lhs of an
 
virtual Theorem liftConcatBVMult (const Expr &e)=0
 
virtual Theorem canonBVMult (const Expr &e)=0
 canonize BVMult expressions in order to get one coefficient
 
virtual Theorem liftConcatBVPlus (const Expr &e)=0
 
virtual Theorem canonBVPlus (const Expr &e)=0
 canonize BVPlus expressions in order to get just one
 
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
 
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
 

Detailed Description

Definition at line 33 of file bitvector_proof_rules.h.

Constructor & Destructor Documentation

virtual CVC3::BitvectorProofRules::~BitvectorProofRules ( )
inlinevirtual

Definition at line 36 of file bitvector_proof_rules.h.

Member Function Documentation

virtual Theorem CVC3::BitvectorProofRules::bitvectorFalseRule ( const Theorem thm)
pure virtual
Parameters
thminput theorem: (e1[i]<=>e2[i])<=>false
   \result (e1=e2)<=>false

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitvectorTrueRule ( const Theorem thm)
pure virtual
Parameters
thminput theorem: (~e1[i]<=>e2[i])<=>true
   \result (e1!=e2)<=>true

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitBlastEqnRule ( const Expr e,
const Expr f 
)
pure virtual

t1=t2 ==> AND_i(t1[i:i] = t2[i:i])

Parameters
eis a Expr(t1=t2)
fis the resulting expression AND_i(t1[i:i] = t2[i:i]) is passed to the rule for efficiency.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitBlastDisEqnRule ( const Theorem e,
const Expr f 
)
pure virtual

t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i])

Parameters
eis a Theorem(t1/=t2)
fis the resulting expression OR_i(NOT t1[i]<=>t2[i]), passed to the rule for efficiency.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::signExtendRule ( const Expr e)
pure virtual

sign extend the input SX(e) appropriately

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::padBVLTRule ( const Expr e,
int  len 
)
pure virtual

Pad the kids of BVLT/BVLE to make their length equal.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::padBVSLTRule ( const Expr e,
int  len 
)
pure virtual

Sign Extend the kids of BVSLT/BVSLE to make their length equal.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::signBVLTRule ( const Expr e,
const Theorem topBit0,
const Theorem topBit1 
)
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.

virtual Theorem CVC3::BitvectorProofRules::notBVEQ1Rule ( const Expr e)
pure virtual

NOT(e[0][0] = e[0][1]) <==> e[0][0] = ~e[0][1]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::notBVLTRule ( const Expr e)
pure virtual

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.

virtual Theorem CVC3::BitvectorProofRules::lhsEqRhsIneqn ( const Expr e,
int  kind 
)
pure virtual

if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::zeroLeq ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvConstIneqn ( const Expr e,
int  kind 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::generalIneqn ( const Expr e,
const Theorem e0,
const Theorem e1,
int  kind 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bitExtractAllToConstEq ( std::vector< Theorem > &  thms)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bitExtractToExtract ( const Theorem thm)
pure virtual

t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0

Parameters
thmis a Theorem(t[i]) or Theorem(NOT t[i]), where t[i] is BOOLEXTRACT(t, i).

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractRewrite ( const Expr x)
pure virtual

t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractConstant ( const Expr x,
int  i 
)
pure virtual
Parameters
xis bitvector constant
iis extracted bitposition
Returns

\[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{TRUE}} \]

, if bitposition has a 1;

\[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}} \]

, if the bitposition has a 0

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractConcatenation ( const Expr x,
int  i 
)
pure virtual
Parameters
xis bitvector binary concatenation
iis extracted bitposition
Returns

\[ \frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]} \]

, where

\[ 0 \geq i \geq n-1 \]

, another case of boolextract over concatenation is:

\[\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]} \]

, where

\[ n \geq i \geq m+n-1 \]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractConstBVMult ( const Expr t,
int  i 
)
pure virtual
Parameters
tis bitvector binary BVMULT. x[0] must be BVCONST
iis extracted bitposition
Returns
bitblast of BVMULT

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractBVMult ( const Expr t,
int  i 
)
pure virtual
Parameters
t: input1 is bitvector binary BVMULT. t[0] must not be BVCONST
i: input2 is extracted bitposition
Returns
bitblast of BVMULT

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractExtraction ( const Expr x,
int  i 
)
pure virtual
Parameters
xis bitvector extraction e[k:j]
iis extracted bitposition
Returns

\[ \frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]} \]

, where

\[ 0 \geq j \geq k < n, 0 \geq i < k-j \]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractBVPlus ( const std::vector< Theorem > &  t1,
const std::vector< Theorem > &  t2,
const Expr bvPlusTerm,
int  i 
)
pure virtual
Parameters
t1is vector of bitblasts of t, from bit i-1 to 0
t2is vector of bitblasts of q, from bit i-1 to 0
bvPlusTermis BVPLUS term: BVPLUS(n,t,q)
iis extracted bitposition
Returns
The base case is:

\[ \frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]} \]

, when

\[ 0 < i \leq n-1 \]

, we have

\[ \frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i] \oplus c(t,q,i)} \]

, where c(t,q,i) is the carry generated by the addition of bits from 0 to i-1

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractBVPlusPreComputed ( const Theorem t1_i,
const Theorem t2_i,
const Expr bvPlusTerm,
int  bitPos,
int  precomputed 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvPlusAssociativityRule ( const Expr bvPlusTerm)
pure virtual
Parameters
bvPlusTerm: input1 is bvPlusTerm, a BVPLUS term with arity > 2
Returns
: output is iff-Theorem: bvPlusTerm <==> outputTerm, where outputTerm is an equivalent BINARY bvplus.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractNot ( const Expr x,
int  i 
)
pure virtual
Parameters
x: input1 is bitwise NEGATION
i: input2 is extracted bitposition
Returns

\[ \frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])} \]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractBitwise ( const Expr x,
int  i,
int  kind 
)
pure virtual

Extract from bitwise AND, OR, or XOR.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractFixedLeftShift ( const Expr x,
int  i 
)
pure virtual
Parameters
x: input1 is bitvector FIXED SHIFT

\[ e_{[n]} \ll k \]

i: input2 is extracted bitposition
Returns

\[\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}} \]

, if 0 <= i < k. however, if k <= i < n then, result is

\[\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]} \]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractFixedRightShift ( const Expr x,
int  i 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bitExtractBVSHL ( const Expr x,
int  i 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bitExtractBVLSHR ( const Expr x,
int  i 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bitExtractBVASHR ( const Expr x,
int  i 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::zeroPaddingRule ( const Expr e,
int  r 
)
pure virtual
Parameters
e: input1 is bitvector term
r: input2 is extracted bitposition
Returns
we check if r > bvlength(e). if yes, then return BOOLEXTRACT(e,r) <==> FALSE; else raise soundness exception. (Note: this rule is used in BVPLUS bitblast function)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractSXRule ( const Expr e,
int  i 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::eqConst ( const Expr e)
pure virtual

c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::eqToBits ( const Theorem eq)
pure virtual

|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::leftShiftToConcat ( const Expr e)
pure virtual

t<<n = c @ 0bin00...00, takes e == (t<<n)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::constWidthLeftShiftToConcat ( const Expr e)
pure virtual

t<<n = c @ 0bin00...00, takes e == (t<<n)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::rightShiftToConcat ( const Expr e)
pure virtual

t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvshlToConcat ( const Expr e)
pure virtual

BVSHL(t,c) = t[n-c,0] @ 0bin00...00.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvshlSplit ( const Expr e)
pure virtual

BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvlshrToConcat ( const Expr e)
pure virtual

BVLSHR(t,c) = 0bin00...00 @ t[n-1,c].

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvShiftZero ( const Expr e)
pure virtual

Any shift over a zero = 0.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvashrToConcat ( const Expr e)
pure virtual

BVASHR(t,c) = SX(t[n-1,c], n-1)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::rewriteXNOR ( const Expr e)
pure virtual

a XNOR b <=> (~a & ~b) | (a & b)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::rewriteNAND ( const Expr e)
pure virtual

a NAND b <=> ~(a & b)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::rewriteNOR ( const Expr e)
pure virtual

a NOR b <=> ~(a | b)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::rewriteBVCOMP ( const Expr e)
pure virtual

BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::rewriteBVSub ( const Expr e)
pure virtual

a - b <=> a + (-b)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::constMultToPlus ( const Expr e)
pure virtual

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.

virtual Theorem CVC3::BitvectorProofRules::bvplusZeroConcatRule ( const Expr e)
pure virtual

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.

virtual Theorem CVC3::BitvectorProofRules::zeroCoeffBVMult ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::oneCoeffBVMult ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::flipBVMult ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::padBVPlus ( const Expr e)
pure virtual

Make args the same length as the result (zero-extend)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::padBVMult ( const Expr e)
pure virtual

Make args the same length as the result (zero-extend)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvConstMultAssocRule ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvMultAssocRule ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvMultDistRule ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::flattenBVPlus ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::combineLikeTermsRule ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::lhsMinusRhsRule ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::extractBVMult ( const Expr e)
pure virtual

(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractBVPlus ( const Expr e)
pure virtual

(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::iteExtractRule ( const Expr e)
pure virtual

ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::iteBVnegRule ( const Expr e)
pure virtual

~ite(c,t1,t2) <=> ite(c,~t1,~t2)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvuminusBVConst ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvuminusBVMult ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvuminusBVUminus ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvuminusVar ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvmultBVUminus ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvuminusToBVPlus ( const Expr e)
pure virtual

-t <==> ~t+1

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvuminusBVPlus ( const Expr e)
pure virtual

-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractConst ( const Expr e)
pure virtual

c1[i:j] = c (extraction from a constant bitvector)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractWhole ( const Expr e)
pure virtual

t[n-1:0] = t for n-bit t

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractExtract ( const Expr e)
pure virtual

t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractConcat ( const Expr e)
pure virtual

(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractAnd ( const Expr e)
pure virtual

(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractOr ( const Expr e)
pure virtual

(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractNeg ( const Expr e)
pure virtual

(~t)[i:j] = ~(t[i:j]) (push extraction through NEG)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractBitwise ( const Expr e,
int  kind,
const std::string &  name 
)
pure virtual

Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j].

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::negConst ( const Expr e)
pure virtual

~c1 = c (bit-wise negation of a constant bitvector)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::negConcat ( const Expr e)
pure virtual

~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::negNeg ( const Expr e)
pure virtual

~(~t) = t – eliminate double negation

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::negElim ( const Expr e)
pure virtual

~t = -1*t + 1 – eliminate negation

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::negBVand ( const Expr e)
pure virtual

~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::negBVor ( const Expr e)
pure virtual

~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::negBVxor ( const Expr e)
pure virtual

~(t1 xor t2) = ~t1 xor t2

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::negBVxnor ( const Expr e)
pure virtual

~(t1 xnor t2) = t1 xor t2

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitwiseConst ( const Expr e,
const std::vector< int > &  idxs,
int  kind 
)
pure virtual

Combine constants in bitwise AND, OR, XOR.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitwiseConcat ( const Expr e,
int  kind 
)
pure virtual

Lifts concatenation above bitwise operators.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitwiseFlatten ( const Expr e,
int  kind 
)
pure virtual

Flatten bitwise operation.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitwiseConstElim ( const Expr e,
int  idx,
int  kind 
)
pure virtual

Simplify bitwise operator containing a constant child.

Parameters
eis the bit-wise expr
idxis the index of the constant bitvector
kindis the kind of e

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::concatConst ( const Expr e)
pure virtual

c1@c2@...@cn = c (concatenation of constant bitvectors)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::concatFlatten ( const Expr e)
pure virtual

Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::concatMergeExtract ( const Expr e)
pure virtual

Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0].

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvplusConst ( const Expr e)
pure virtual

BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvmultConst ( const Expr e)
pure virtual

n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::typePredBit ( const Expr e)
pure virtual

|- t=0 OR t=1 for any 1-bit bitvector t

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::expandTypePred ( const Theorem tp)
pure virtual

Expand the type predicate wrapper (compute the actual type predicate)

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::isolate_var ( const Expr e)
pure virtual

isolate a variable with coefficient = 1 on the Lhs of an

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::liftConcatBVMult ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::canonBVMult ( const Expr e)
pure virtual

canonize BVMult expressions in order to get one coefficient

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::liftConcatBVPlus ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::canonBVPlus ( const Expr e)
pure virtual

canonize BVPlus expressions in order to get just one

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::canonBVUMinus ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::processExtract ( const Theorem e,
bool &  solvedForm 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::canonBVEQ ( const Expr e,
int  maxEffort = 3 
)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::distributive_rule ( const Expr e)
pure virtual

apply the distributive rule on the BVMULT expression e

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::BVMult_order_subterms ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::MarkNonSolvableEq ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::zeroExtendRule ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::repeatRule ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::rotlRule ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::rotrRule ( const Expr e)
pure virtual
virtual Theorem CVC3::BitvectorProofRules::bvUDivConst ( const Expr divExpr)
pure virtual

Divide a with b unsigned and return the bit-vector constant result

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvUDivTheorem ( const Expr divExpr)
pure virtual

Rewrite a/b with a fresh variable d and add the constraints to make it be a divider.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvURemConst ( const Expr remExpr)
pure virtual

Divide a with b unsigned and return the bit-vector constant result

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvURemRewrite ( const Expr divExpr)
pure virtual

Rewrite ab in terms of a/b, i.e. a - a/b

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvSDivRewrite ( const Expr sDivExpr)
pure virtual

Rewrite the signed divide in terms of the unsigned one.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvSRemRewrite ( const Expr sRemExpr)
pure virtual

Rewrite the signed remainder in terms of the unsigned one.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvSModRewrite ( const Expr sModExpr)
pure virtual

Rewrite the signed mod in terms of the unsigned one.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitblastBVMult ( const std::vector< Theorem > &  a_bits,
const std::vector< Theorem > &  b_bits,
const Expr a_times_b,
std::vector< Theorem > &  output_bits 
)
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.

virtual Theorem CVC3::BitvectorProofRules::bitblastBVPlus ( const std::vector< Theorem > &  a_bits,
const std::vector< Theorem > &  b_bits,
const Expr a_plus_b,
std::vector< Theorem > &  output_bits 
)
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.

virtual Theorem CVC3::BitvectorProofRules::zeroBVOR ( const Expr orEqZero)
pure virtual

Rewrite

\[x_1 \vee x_2 \vee \ldots \vee x_n = 0\]

into

\[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\]

.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::oneBVAND ( const Expr andEqOne)
pure virtual

Rewrite

\[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\]

into

\[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\]

.

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::constEq ( const Expr eq)
pure virtual

Equalities over constants go to true/false.

Implemented in CVC3::BitvectorTheoremProducer.

virtual bool CVC3::BitvectorProofRules::solveExtractOverlapApplies ( const Expr eq)
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().

virtual Theorem CVC3::BitvectorProofRules::solveExtractOverlap ( const Expr eq)
pure virtual

Returns the theorem that simplifies the equality of two overlapping extracts over the same term.

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::solve().


The documentation for this class was generated from the following file: