CVCL::BitvectorTheoremProducer Class Reference

This class implements proof rules for bitvector normalizers (concatenation normal form, bvplus normal form), bitblaster rules, other relevant rewrite rules for bv arithmetic and word-level operators. More...

#include <bitvector_theorem_producer.h>

Inheritance diagram for CVCL::BitvectorTheoremProducer:

[legend]Collaboration diagram for CVCL::BitvectorTheoremProducer:

[legend]List of all members.

Public Member Functions

BitvectorTheoremProducer (TheoryBitvector *theoryBitvector)
Constructor: constructs an instance of bitvector DP.
~BitvectorTheoremProducer ()
Theorem bitvectorFalseRule (const Theorem &thm)
Theorem bitvectorTrueRule (const Theorem &thm)
Theorem bitBlastEqnRule (const Expr &e, const Expr &f)
Theorem bitBlastDisEqnRule (const Theorem &e, const Expr &f)
Theorem signExtendRule (const Expr &e)
sign extend the input SX(e) appropriately
Theorem padBVLTRule (const Expr &e, int len)
Pad the kids of BVLT/BVLE to make their length equal.
Theorem padSBVLTRule (const Expr &e, int len)
Sign Extend the kids of SBVLT/SBVLE to make their length equal.
Theorem signBVLTRule (const Expr &e, const Theorem &topBit0, const Theorem &topBit1)
Theorem notBVLTRule (const Expr &e, int Kind)
Theorem lhsEqRhsIneqn (const Expr &e, int kind)
if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
Theorem bvConstIneqn (const Expr &e, int kind)
if indeed e[0] < e[1] then (e<==>true) else (e<==>false)
Theorem generalIneqn (const Expr &e, const Theorem &lhs_i, const Theorem &rhs_i, int kind)
Theorem bitExtractToExtract (const Theorem &thm)
t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0
Theorem bitExtractRewrite (const Expr &x)
t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])
Theorem bitExtractConstant (const Expr &x, int i)
Theorem bitExtractConcatenation (const Expr &x, int i)
Theorem bitExtractConstBVMult (const Expr &t, int i)
Theorem bitExtractBVMult (const Expr &t, int i)
Theorem bitExtractExtraction (const Expr &x, int i)
Theorem bitExtractBVPlus (const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i)
Theorem bitExtractBVPlusPreComputed (const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed)
Theorem bvPlusAssociativityRule (const Expr &bvPlusTerm)
Theorem bitExtractNot (const Expr &x, int i)
Theorem bitExtractBitwise (const Expr &x, int i, int kind)
Auxiliary function for bitExtractAnd() and bitExtractOr().
Theorem bitExtractAnd (const Expr &x, int i)
Theorem bitExtractOr (const Expr &x, int i)
Theorem bitExtractFixedLeftShift (const Expr &x, int i)
Theorem bitExtractFixedRightShift (const Expr &x, int i)
Theorem zeroPaddingRule (const Expr &e, int r)
Theorem bitExtractSXRule (const Expr &e, int i)
bitExtractSXRule
Theorem eqConst (const Expr &e)
c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
Theorem eqToBits (const Theorem &eq)
|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
Theorem leftShiftToConcat (const Expr &e)
t<<n = c @ 0bin00...00, takes e == (t<<n)
Theorem rightShiftToConcat (const Expr &e)
t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
Theorem constMultToPlus (const Expr &e)
k*t = BVPLUS(n, <sum of shifts of t>) -- translation of k*t to BVPLUS
Theorem bvplusZeroConcatRule (const Expr &e)
0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
Theorem zeroCoeffBVMult (const Expr &e)
Theorem oneCoeffBVMult (const Expr &e)
Theorem flipBVMult (const Expr &e)
t1*a <==> a*t1
Expr pad (int rat, const Expr &e)
converts e to a bitvector of length rat
Theorem padBVPlus (const Expr &e)
Pad the kids of BVMULT to make their bvLength = # of output-bits.
Theorem padBVMult (const Expr &e)
Pad the kids of BVMULT to make their bvLength = # of output-bits.
Theorem bvConstMultAssocRule (const Expr &e)
a*(b*t) <==> (a*b)*t, where a,b,t have same bvLength
Theorem bvMultAssocRule (const Expr &e)
(t1*t2)*t3 <==> t1*(t2*t3), where t1<t2<t3
Theorem bvMultDistRule (const Expr &e)
a*(t1+...+tn) <==> (a*t1+...+a*tn), where all kids are equibvLength
Theorem flattenBVPlus (const Expr &e)
input BVPLUS expression e.output e <==> e', where e' has no BVPLUS
Theorem combineLikeTermsRule (const Expr &e)
Theorem lhsMinusRhsRule (const Expr &e)
Theorem extractBVMult (const Expr &e)
(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n
Theorem extractBVPlus (const Expr &e)
(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n
Theorem iteExtractRule (const Expr &e)
ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
Theorem iteBVnegRule (const Expr &e)
~ite(c,t1,t2) <=> ite(c,~t1,~t2)
Theorem bvuminusBVConst (const Expr &e)
-0 <==> 0, -c <==> ~c+1
Theorem bvuminusBVMult (const Expr &e)
-(c*t)<=>(-c)*t; if -c==0 return e<=>0. if(-c==1) return e<=>t
Theorem bvuminusBVUminus (const Expr &e)
-(-e) <==> e
Theorem bvuminusVar (const Expr &e)
-v <==> -1*v
Theorem bvmultBVUminus (const Expr &e)
c*(-t) <==> (-c)*t
Theorem bvuminusToBVPlus (const Expr &e)
-t <==> ~t+1
Theorem bvuminusBVPlus (const Expr &e)
-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
Theorem extractConst (const Expr &e)
c1[i:j] = c (extraction from a constant bitvector)
Theorem extractWhole (const Expr &e)
t[n-1:0] = t for n-bit t
Theorem extractExtract (const Expr &e)
t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)
Theorem extractConcat (const Expr &e)
(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
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 extractAnd (const Expr &e)
(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)
Theorem extractOr (const Expr &e)
(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)
Theorem extractNeg (const Expr &e)
(~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
Theorem negConst (const Expr &e)
~c1 = c (bit-wise negation of a constant bitvector)
Theorem negConcat (const Expr &e)
~(t1@...@tn) = (~t1)@...@(~tn) -- push negation through concat
Theorem negNeg (const Expr &e)
~(~t) = t -- eliminate double negation
Theorem negBVand (const Expr &e)
~(t1 & t2) <=> ~t1 | ~t2 -- DeMorgan's Laws
Theorem negBVor (const Expr &e)
~(t1 | t2) <=> ~t1 & ~t2 -- DeMorgan's Laws
Theorem bitwiseConst (const Expr &e, const std::vector< int > &idxs, bool isAnd)
Auxiliary method for andConst() and orConst().
Theorem bitwiseConcat (const Expr &e, int idx, bool isAnd)
Auxiliary method for andConcat() and orConcat().
Theorem bitwiseFlatten (const Expr &e, bool isAnd)
Auxiliary method for andFlatten() and orFlatten().
Theorem andConst (const Expr &e, const std::vector< int > &idxs)
c1&c2&t = c&t -- compute bit-wise AND of constant bitvector arguments
Theorem andZero (const Expr &e, int idx)
0bin0...0 & t = 0bin0...0 -- bit-wise AND with zero bitvector
Theorem andOne (const Expr &e, const std::vector< int > idxs)
0bin1...1 & t = t -- bit-wise AND with bitvector of 1's
Theorem andConcat (const Expr &e, int idx)
... & (t1@...@tk) & ... = (...& t1 &...)@...@(...& tk &...)
Theorem andFlatten (const Expr &e)
(t1 & (t2 & t3) & t4) = t1 & t2 & t3 & t4 -- flatten bit-wise AND
Theorem orConst (const Expr &e, const std::vector< int > &idxs)
c1|c2|t = c|t -- compute bit-wise OR of constant bitvector arguments
Theorem orOne (const Expr &e, int idx)
0bin1...1 | t = 0bin1...1 -- bit-wise OR with bitvector of 1's
Theorem orZero (const Expr &e, const std::vector< int > idxs)
0bin0...0 | t = t -- bit-wise OR with bitvector of 0's
Theorem orConcat (const Expr &e, int idx)
... | (t1@...@tk) | ... = (...| t1 |...)@...@(...| tk |...)
Theorem orFlatten (const Expr &e)
(t1 | (t2 | t3) | t4) = t1 | t2 | t3 | t4 -- flatten bit-wise OR
int sameKidCheck (const Expr &e, ExprMap< int > &likeTerms)
Theorem concatConst (const Expr &e)
c1@c2@...@cn = c (concatenation of constant bitvectors)
Theorem concatFlatten (const Expr &e)
Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w.
Theorem concatMergeExtract (const Expr &e)
Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0].
Theorem bvplusConst (const Expr &e)
BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors).
Theorem bvmultConst (const Expr &e)
n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant)
Theorem typePredBit (const Expr &e)
|- t=0 OR t=1 for any 1-bit bitvector t
Theorem expandTypePred (const Theorem &tp)
Expand the type predicate wrapper (compute the actual type predicate).
Expr rat (const Rational &r)
Expr computeCarry (const std::vector< Theorem > &t1BitExtractThms, const std::vector< Theorem > &t2BitExtractThms, int bitPos)
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

Private Member Functions

const Expr & bvZero () const
Return cached constant 0bin0.
const Expr & bvOne () const
Return cached constant 0bin1.
void collectLikeTermsOfPlus (const Expr &e, ExprMap< Rational > &likeTerms, Rational &plusConstant)
void collectOneTermOfPlus (const Rational &coefficient, const Expr &var, ExprMap< Rational > &likeTerms, Rational &plusConstant)
void createNewPlusCollection (const Expr &e, const ExprMap< Rational > &likeTerms, Rational &plusConstant, std::vector< Expr > &result)
Expr sumNormalizedElements (int bvplusLength, const std::vector< Expr > &elements)

Private Attributes

TheoryBitvector * d_theoryBitvector
Expr d_bvZero
Constant 1-bit bit-vector 0bin0.
Expr d_bvOne
Constant 1-bit bit-vector 0bin1.

Detailed Description

This class implements proof rules for bitvector normalizers (concatenation normal form, bvplus normal form), bitblaster rules, other relevant rewrite rules for bv arithmetic and word-level operators.

Author: Vijay Ganesh, May-August, 2004

Definition at line 49 of file bitvector_theorem_producer.h.

Constructor & Destructor Documentation

BitvectorTheoremProducer::BitvectorTheoremProducer ( TheoryBitvector * theoryBitvector )

Constructor: constructs an instance of bitvector DP.

Definition at line 56 of file bitvector_theorem_producer.cpp.
References d_bvOne, d_bvZero, d_theoryBitvector, and CVCL::TheoryBitvector::newBVConstExpr().

CVCL::BitvectorTheoremProducer::~BitvectorTheoremProducer ( ) [inline]

Definition at line 92 of file bitvector_theorem_producer.h.

Member Function Documentation

const Expr& CVCL::BitvectorTheoremProducer::bvZero ( ) const [inline, private]

Return cached constant 0bin0.

Definition at line 58 of file bitvector_theorem_producer.h.
References d_bvZero.
Referenced by bitExtractToExtract(), expandTypePred(), signBVLTRule(), and typePredBit().

const Expr& CVCL::BitvectorTheoremProducer::bvOne ( ) const [inline, private]

Return cached constant 0bin1.

Definition at line 60 of file bitvector_theorem_producer.h.
References d_bvOne.
Referenced by bitExtractToExtract(), expandTypePred(), signBVLTRule(), and typePredBit().

void BitvectorTheoremProducer::collectLikeTermsOfPlus ( const Expr & e,

ExprMap< Rational > & likeTerms,

Rational & plusConstant

) [private]

Collect all of: a*x1+b*x1 + c*x2-x2 + d*x3 + ~x3 + ~x4 +e into (a+b, x1) , (c-1 , x2), (d-1, x3), (-1, x4) and the constant e-2. The constant is calculated from the formula -x = ~x+1 (or -x-1=~x).
Definition at line 3362 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::begin(), CVCL::BVCONST, CVCL::BVMULT, CVCL::BVUMINUS, CVCL::ExprMap< Data >::clear(), collectOneTermOfPlus(), CVCL::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVCL::Expr::end(), CVCL::Expr::getOpKind(), and CVCL::Expr::toString().
Referenced by combineLikeTermsRule().

void BitvectorTheoremProducer::collectOneTermOfPlus ( const Rational & coefficient,

const Expr & var,

ExprMap< Rational > & likeTerms,

Rational & plusConstant

) [private]

Collect a single coefficient*var pair into likeTerms. Update the counter of likeTerms[var] += coefficient. Potentially update the constant additive plusConstant.
Definition at line 3332 of file bitvector_theorem_producer.cpp.
References d_theoryBitvector, CVCL::ExprMap< Data >::empty(), CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), CVCL::Theorem::getRHS(), and CVCL::TheoryBitvector::pushNegationRec().
Referenced by collectLikeTermsOfPlus().

void BitvectorTheoremProducer::createNewPlusCollection ( const Expr & e,

const ExprMap< Rational > & likeTerms,

Rational & plusConstant,

std::vector< Expr > & result

) [private]

Create a vector which will form the next PVPLUS. Use the colleciton of likeTerms, and the constant additive plusConstant
Definition at line 3424 of file bitvector_theorem_producer.cpp.
References CVCL::ExprMap< Data >::begin(), CVCL::BITVECTOR, boundedModulo(), CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::ExprMap< Data >::end(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::pushNegationRec(), and CVCL::Expr::toString().
Referenced by combineLikeTermsRule().

Expr BitvectorTheoremProducer::sumNormalizedElements ( int bvplusLength,

const std::vector< Expr > & elements

) [private]

Create expression by applying plus to all elements. All elements should be normalized and ready. If there are too few elements, a non BVPLUS expression will be created.
Definition at line 3484 of file bitvector_theorem_producer.cpp.
References d_theoryBitvector, CVCL::TheoryBitvector::newBVPlusExpr(), and CVCL::TheoryBitvector::newBVZeroString().
Referenced by combineLikeTermsRule().

Theorem BitvectorTheoremProducer::bitvectorFalseRule ( const Theorem & thm ) [virtual]

Parameters:

thm input theorem: (e1[i]<=>e2[i])<=>false

Returns:
(e1=e2)<=>false

Implements CVCL::BitvectorProofRules.
Definition at line 71 of file bitvector_theorem_producer.cpp.
References CVCL::BOOLEXTRACT, d_theoryBitvector, CVCL::Expr::eqExpr(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::Theorem::getExpr(), CVCL::Expr::iffExpr(), CVCL::Expr::isIff(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitvectorTrueRule ( const Theorem & thm ) [virtual]

Parameters:

thm input theorem: (~e1[i]<=>e2[i])<=>true

Returns:
(e1!=e2)<=>true

Implements CVCL::BitvectorProofRules.
Definition at line 105 of file bitvector_theorem_producer.cpp.
References CVCL::BOOLEXTRACT, d_theoryBitvector, CVCL::Expr::eqExpr(), CVCL::Theorem::getAssumptionsCopy(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::iffExpr(), CVCL::Expr::isIff(), CVCL::Expr::negate(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::NOT, CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitBlastEqnRule ( const Expr & e,

const Expr & f

) [virtual]

Parameters:

e input equation: e1=e2 over bitvector terms

f formula over the bits of bitvector variables in e:

Returns:
$\frac{e_1 = e_2}{\bigwedge_{i=1}^n (e_{1}[i] \iff e_{2}[i]) }$
where each of
$e_{1}[i], e{2}[i]$
denotes a formula over variables in
$e_{1}, e_{2}$
respectively

Implements CVCL::BitvectorProofRules.
Definition at line 144 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BOOLEXTRACT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::Expr::isAnd(), CVCL::Expr::isEq(), CVCL::Expr::isIff(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitBlastDisEqnRule ( const Theorem & e,

const Expr & f

) [virtual]

Parameters:

e : input disequality: e1 != e2 over bitvector terms

f : formula over the bits of bitvector variables in e:

Returns:
$\frac{e_1 \not = e_2}{\bigwedge_{i=1}^n ((\neg e_{1}[i]) \iff e_{2}[i]) }$
where each of
$e_{1}[i], e{2}[i]$
denotes a formula over variables in
$e_{1}, e_{2}$
respectively

Implements CVCL::BitvectorProofRules.
Definition at line 228 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BOOLEXTRACT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Theorem::getAssumptionsCopy(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::Type::getExpr(), CVCL::Theorem::getExpr(), CVCL::Expr::getOpKind(), CVCL::Theorem::getProof(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::Expr::isEq(), CVCL::Expr::isIff(), CVCL::Expr::isNot(), CVCL::Expr::isOr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::Theorem::toString(), CVCL::TRACE, CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::signExtendRule ( const Expr & e ) [virtual]

sign extend the input SX(e) appropriately

Implements CVCL::BitvectorProofRules.
Definition at line 346 of file bitvector_theorem_producer.cpp.
References CVCL::BITVECTOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::SX, CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().
Referenced by bitExtractSXRule().

Theorem BitvectorTheoremProducer::padBVLTRule ( const Expr & e,

int len

) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 311 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVLE, CVCL::BVLT, d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoryBitvector::newBVLEExpr(), CVCL::TheoryBitvector::newBVLTExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), pad(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::padSBVLTRule ( const Expr & e,

int len

) [virtual]

Sign Extend the kids of SBVLT/SBVLE to make their length equal.

Implements CVCL::BitvectorProofRules.
Definition at line 406 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::TheoryBitvector::newSBVLEExpr(), CVCL::TheoryBitvector::newSBVLTExpr(), CVCL::TheoryBitvector::newSXExpr(), CVCL::SBVLE, CVCL::SBVLT, CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::signBVLTRule ( const Expr & e,

const Theorem & topBit0,

const Theorem & topBit1

) [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])
Implements CVCL::BitvectorProofRules.
Definition at line 448 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::andExpr(), CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVCONST, bvOne(), CVCL::TheoryBitvector::BVSize(), bvZero(), CVCL::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVCL::Expr::eqExpr(), CVCL::Theory::falseExpr(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVLEExpr(), CVCL::TheoryBitvector::newBVLTExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::orExpr(), CVCL::SBVLE, CVCL::SBVLT, CVCL::Expr::toString(), CVCL::Theory::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::notBVLTRule ( const Expr & e,

int Kind

) [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])
Implements CVCL::BitvectorProofRules.
Definition at line 627 of file bitvector_theorem_producer.cpp.
References CVCL::BVLE, CVCL::BVLT, d_theoryBitvector, CVCL::Expr::getKind(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVLEExpr(), CVCL::TheoryBitvector::newBVLTExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::NOT, CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::lhsEqRhsIneqn ( const Expr & e,

int kind

) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 658 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVLE, CVCL::BVLT, d_theoryBitvector, CVCL::Theory::falseExpr(), CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::Theory::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvConstIneqn ( const Expr & e,

int kind

) [virtual]

if indeed e[0] < e[1] then (e<==>true) else (e<==>false)

Implements CVCL::BitvectorProofRules.
Definition at line 686 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVCONST, CVCL::BVLE, CVCL::BVLT, CVCL::TheoryBitvector::BVSize(), CVCL::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVCL::Theory::falseExpr(), CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::Theory::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::generalIneqn ( const Expr & e,

const Theorem & lhs_i,

const Theorem & rhs_i,

int kind

) [virtual]

Implements CVCL::BitvectorProofRules.
Definition at line 735 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::andExpr(), CVCL::Expr::arity(), CVCL::BOOLEXTRACT, CVCL::BVLE, CVCL::BVLT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Theory::falseExpr(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Expr::iffExpr(), CVCL::Type::isBool(), CVCL::Expr::isFalse(), CVCL::Expr::isNull(), CVCL::Theorem::isRewrite(), CVCL::Expr::isTrue(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVLEExpr(), CVCL::TheoryBitvector::newBVLTExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::notExpr(), CVCL::Expr::orExpr(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::Theory::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractToExtract ( const Theorem & thm ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 877 of file bitvector_theorem_producer.cpp.
References CVCL::BOOLEXTRACT, bvOne(), bvZero(), d_theoryBitvector, CVCL::Theorem::getAssumptionsCopy(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::Theorem::getExpr(), CVCL::Expr::getOpKind(), CVCL::Theorem::getProof(), CVCL::Expr::isNot(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractRewrite ( const Expr & x ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 901 of file bitvector_theorem_producer.cpp.
References CVCL::BOOLEXTRACT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractConstant ( const Expr & x,

int i

) [virtual]

Parameters:

x : input1 is bitvector constant

i : input2 is 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

Implements CVCL::BitvectorProofRules.
Definition at line 930 of file bitvector_theorem_producer.cpp.
References CVCL::BVCONST, d_theoryBitvector, CVCL::Theory::falseExpr(), CVCL::TheoryBitvector::getBVConstValue(), CVCL::Expr::getKind(), CVCL::int2string(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::TRACE, CVCL::Theory::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractConcatenation ( const Expr & x,

int i

) [virtual]

Parameters:

x : input1 is bitvector binary concatenation

i : input2 is 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$

Implements CVCL::BitvectorProofRules.
Definition at line 968 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::TheoryBitvector::BVSize(), CVCL::CONCAT, d_theoryBitvector, CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::Expr::isNull(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractConstBVMult ( const Expr & t,

int i

) [virtual]

Parameters:

t : input1 is bitvector binary BVMULT. x[0] must be BVCONST

i : input2 is extracted bitposition

Returns:
bitblast of BVMULT

Implements CVCL::BitvectorProofRules.
Definition at line 1023 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVCONST, CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::TheoryBitvector::getBVConstValue(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::mult(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoryBitvector::newBVZeroString(), CVCL::TheoryBitvector::newFixedLeftShiftExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), pad(), rat(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractBVMult ( const Expr & t,

int i

) [virtual]

Parameters:

t : input1 is bitvector binary BVMULT. t[0] must not be BVCONST

i : input2 is extracted bitposition

Returns:
bitblast of BVMULT

Implements CVCL::BitvectorProofRules.
Definition at line 1090 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVCONST, CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::Expr::iffExpr(), CVCL::int2string(), CVCL::Expr::iteExpr(), CVCL::mult(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoryBitvector::newBVZeroString(), CVCL::TheoryBitvector::newFixedLeftShiftExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::Theory::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractExtraction ( const Expr & x,

int i

) [virtual]

Parameters:

x : input1 is bitvector extraction [k:j]

i : input2 is 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$

Implements CVCL::BitvectorProofRules.
Definition at line 1153 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::EXTRACT, CVCL::Type::getExpr(), CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractBVPlus ( const std::vector< Theorem > & t1,

const std::vector< Theorem > & t2,

const Expr & bvPlusTerm,

int i

) [virtual]

Parameters:

t1 : input1 is vector of bitblasts of t, from bit i-1 to 0

t2 : input2 is vector of bitblasts of q, from bit i-1 to 0

bvPlusTerm : input3 is BVPLUS term: BVPLUS(n,t,q)

i : input4 is 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

Implements CVCL::BitvectorProofRules.
Definition at line 1205 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVPLUS, computeCarry(), d_theoryBitvector, CVCL::TheoryBitvector::getBVPlusParam(), CVCL::Expr::getOpKind(), CVCL::Expr::iffExpr(), CVCL::int2string(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractBVPlusPreComputed ( const Theorem & t1_i,

const Theorem & t2_i,

const Expr & bvPlusTerm,

int bitPos,

int precomputed

) [virtual]

Implements CVCL::BitvectorProofRules.
Definition at line 1306 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BOOLEXTRACT, CVCL::BVPLUS, computeCarryPreComputed(), d_theoryBitvector, CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::TheoryBitvector::getBVPlusParam(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::iffExpr(), CVCL::int2string(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvPlusAssociativityRule ( const Expr & bvPlusTerm ) [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.

Implements CVCL::BitvectorProofRules.
Definition at line 1468 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVPLUS, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Type::getExpr(), CVCL::Expr::getKids(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractNot ( const Expr & x,

int i

) [virtual]

Parameters:

x : input1 is bitwise NEGATION

i : input2 is extracted bitposition

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

Implements CVCL::BitvectorProofRules.
Definition at line 1511 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVNEG, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractBitwise ( const Expr & x,

int i,

int kind

)

Auxiliary function for bitExtractAnd() and bitExtractOr().

Definition at line 1548 of file bitvector_theorem_producer.cpp.
References CVCL::andExpr(), CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BITVECTOR, CVCL::BVAND, CVCL::BVOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::end(), CVCL::Theory::getEM(), CVCL::Type::getExpr(), CVCL::ExprManager::getKindName(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::orExpr(), rat(), CVCL::Theorem::toString(), CVCL::Type::toString(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().
Referenced by bitExtractAnd(), and bitExtractOr().

Theorem BitvectorTheoremProducer::bitExtractAnd ( const Expr & x,

int i

) [virtual]

Parameters:

x : input1 is bitwise AND

i : input2 is extracted bitposition

Returns:
$\frac{}{(t_{[n]} \& q_{[n]})[i] \iff (t_{[n]}[i] \wedge q_{[n]}[i])}$

Implements CVCL::BitvectorProofRules.
Definition at line 1593 of file bitvector_theorem_producer.cpp.
References bitExtractBitwise(), and CVCL::BVAND.

Theorem BitvectorTheoremProducer::bitExtractOr ( const Expr & x,

int i

) [virtual]

Parameters:

x : input1 is bitwise OR

i : input2 is extracted bitposition

Returns:
$\frac{}{(t_{[n]} \mid q_{[n]})[i] \iff (t_{[n]}[i] \vee q_{[n]}[i])}$

Implements CVCL::BitvectorProofRules.
Definition at line 1599 of file bitvector_theorem_producer.cpp.
References bitExtractBitwise(), and CVCL::BVOR.

Theorem BitvectorTheoremProducer::bitExtractFixedLeftShift ( const Expr & x,

int i

) [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]}$

Implements CVCL::BitvectorProofRules.
Definition at line 1604 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Theory::falseExpr(), CVCL::Type::getExpr(), CVCL::TheoryBitvector::getFixedLeftShiftParam(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::LEFTSHIFT, CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractFixedRightShift ( const Expr & x,

int i

) [virtual]

Implements CVCL::BitvectorProofRules.
Definition at line 1653 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Theory::falseExpr(), CVCL::Type::getExpr(), CVCL::TheoryBitvector::getFixedRightShiftParam(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::RIGHTSHIFT, CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::zeroPaddingRule ( const Expr & e,

int r

) [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)

Implements CVCL::BitvectorProofRules.
Definition at line 1440 of file bitvector_theorem_producer.cpp.
References CVCL::BITVECTOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Theory::falseExpr(), CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractSXRule ( const Expr & e,

int i

) [virtual]

bitExtractSXRule

Implements CVCL::BitvectorProofRules.
Definition at line 388 of file bitvector_theorem_producer.cpp.
References d_theoryBitvector, CVCL::Theorem::getRHS(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), signExtendRule(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::eqConst ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 1713 of file bitvector_theorem_producer.cpp.
References constantKids(), d_theoryBitvector, CVCL::Theory::falseExpr(), CVCL::Expr::isEq(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::Theory::trueExpr(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::eqToBits ( const Theorem & eq ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 1732 of file bitvector_theorem_producer.cpp.
References CVCL::andExpr(), CVCL::BITVECTOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::eqExpr(), CVCL::Theorem::getAssumptionsCopy(), CVCL::Theory::getBaseType(), CVCL::Theorem::getExpr(), CVCL::Type::getExpr(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Theorem::isRewrite(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::leftShiftToConcat ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 1768 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), d_theoryBitvector, CVCL::TheoryBitvector::getFixedLeftShiftParam(), CVCL::Expr::getOpKind(), CVCL::LEFTSHIFT, CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::rightShiftToConcat ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 1795 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::TheoryBitvector::getFixedRightShiftParam(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVZeroString(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::RIGHTSHIFT, CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::constMultToPlus ( const Expr & e ) [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
Implements CVCL::BitvectorProofRules.
Definition at line 1830 of file bitvector_theorem_producer.cpp.
References CVCL::abs(), CVCL::Expr::arity(), CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Rational::isInteger(), CVCL::Expr::isRational(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoryBitvector::newFixedLeftShiftExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvplusZeroConcatRule ( const Expr & e ) [virtual]

0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
where k is the size of the 0bin0...0
Implements CVCL::BitvectorProofRules.
Definition at line 1879 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVCONST, CVCL::BVPLUS, CVCL::TheoryBitvector::BVSize(), CVCL::TheoryBitvector::computeBVConst(), CVCL::CONCAT, d_theoryBitvector, CVCL::Expr::end(), CVCL::TheoryBitvector::getBVPlusParam(), CVCL::Expr::getKids(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Theory::reflexivityRule(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::zeroCoeffBVMult ( const Expr & e ) [virtual]

Implements CVCL::BitvectorProofRules.
Definition at line 2987 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVCONST, CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), CVCL::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVZeroString(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::oneCoeffBVMult ( const Expr & e ) [virtual]

Implements CVCL::BitvectorProofRules.
Definition at line 3010 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVCONST, CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), CVCL::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), pad(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::flipBVMult ( const Expr & e ) [virtual]

t1*a <==> a*t1

Implements CVCL::BitvectorProofRules.
Definition at line 3036 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Expr BitvectorTheoremProducer::pad ( int len,

const Expr & e

)

converts e to a bitvector of length rat

Parameters:

len is the desired bvLength of the resulting bitvector

e is the original bitvector of arbitrary bvLength

Definition at line 3058 of file bitvector_theorem_producer.cpp.
References CVCL::BITVECTOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVZeroString(), CVCL::TheoryBitvector::newConcatExpr(), and CVCL::Expr::toString().
Referenced by bitExtractConstBVMult(), oneCoeffBVMult(), padBVLTRule(), padBVMult(), and padBVPlus().

Theorem BitvectorTheoremProducer::padBVPlus ( const Expr & e ) [virtual]

Pad the kids of BVMULT to make their bvLength = # of output-bits.

Implements CVCL::BitvectorProofRules.
Definition at line 3083 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVMULT, CVCL::BVPLUS, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::end(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), pad(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::padBVMult ( const Expr & e ) [virtual]

Pad the kids of BVMULT to make their bvLength = # of output-bits.

Implements CVCL::BitvectorProofRules.
Definition at line 3114 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), pad(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvConstMultAssocRule ( const Expr & e ) [virtual]

a*(b*t) <==> (a*b)*t, where a,b,t have same bvLength

Implements CVCL::BitvectorProofRules.
Definition at line 3139 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVCONST, CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), CVCL::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvMultAssocRule ( const Expr & e ) [virtual]

(t1*t2)*t3 <==> t1*(t2*t3), where t1<t2<t3

Implements CVCL::BitvectorProofRules.
Definition at line 3178 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVCONST, CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvMultDistRule ( const Expr & e ) [virtual]

a*(t1+...+tn) <==> (a*t1+...+a*tn), where all kids are equibvLength

Implements CVCL::BitvectorProofRules.
Definition at line 3253 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVMULT, CVCL::BVPLUS, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::end(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::flattenBVPlus ( const Expr & e ) [virtual]

input BVPLUS expression e.output e <==> e', where e' has no BVPLUS

Implements CVCL::BitvectorProofRules.
Definition at line 3294 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVPLUS, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::combineLikeTermsRule ( const Expr & e ) [virtual]

Implements CVCL::BitvectorProofRules.
Definition at line 3504 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVMULT, CVCL::BVPLUS, CVCL::TheoryBitvector::BVSize(), collectLikeTermsOfPlus(), createNewPlusCollection(), d_theoryBitvector, CVCL::Expr::end(), CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), sumNormalizedElements(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::lhsMinusRhsRule ( const Expr & e ) [virtual]

Implements CVCL::BitvectorProofRules.
Definition at line 3556 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVPLUS, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::end(), CVCL::EQ, CVCL::Expr::getKids(), CVCL::Expr::getKind(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoryBitvector::newBVUminusExpr(), CVCL::TheoryBitvector::newBVZeroString(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::uminus(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractBVMult ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 3857 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::EXTRACT, CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractBVPlus ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 3890 of file bitvector_theorem_producer.cpp.
References CVCL::BVPLUS, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::EXTRACT, CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::Expr::getKids(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Theory::reflexivityRule(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::iteExtractRule ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2157 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::EXTRACT, CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::Expr::getOpKind(), CVCL::ITE, CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::iteBVnegRule ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2194 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVNEG, d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::ITE, CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusBVConst ( const Expr & e ) [virtual]

-0 <==> 0, -c <==> ~c+1

Implements CVCL::BitvectorProofRules.
Definition at line 3653 of file bitvector_theorem_producer.cpp.
References CVCL::BVCONST, CVCL::TheoryBitvector::BVSize(), CVCL::BVUMINUS, CVCL::TheoryBitvector::computeBVConst(), CVCL::TheoryBitvector::computeNegBVConst(), d_theoryBitvector, CVCL::Expr::getKind(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusBVMult ( const Expr & e ) [virtual]

-(c*t)<=>(-c)*t; if -c==0 return e<=>0. if(-c==1) return e<=>t

Implements CVCL::BitvectorProofRules.
Definition at line 3681 of file bitvector_theorem_producer.cpp.
References CVCL::BVCONST, CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), CVCL::BVUMINUS, CVCL::TheoryBitvector::computeNegBVConst(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::newBVZeroString(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusBVUminus ( const Expr & e ) [virtual]

-(-e) <==> e

Implements CVCL::BitvectorProofRules.
Definition at line 3728 of file bitvector_theorem_producer.cpp.
References CVCL::BVUMINUS, CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusVar ( const Expr & e ) [virtual]

-v <==> -1*v

Implements CVCL::BitvectorProofRules.
Definition at line 3750 of file bitvector_theorem_producer.cpp.
References CVCL::TheoryBitvector::BVSize(), CVCL::BVUMINUS, d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvmultBVUminus ( const Expr & e ) [virtual]

c*(-t) <==> (-c)*t

Implements CVCL::BitvectorProofRules.
Definition at line 3774 of file bitvector_theorem_producer.cpp.
References CVCL::BVCONST, CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), CVCL::BVUMINUS, CVCL::TheoryBitvector::computeNegBVConst(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::newBVZeroString(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusToBVPlus ( const Expr & e ) [virtual]

-t <==> ~t+1

Implements CVCL::BitvectorProofRules.
Definition at line 3630 of file bitvector_theorem_producer.cpp.
References CVCL::TheoryBitvector::BVSize(), CVCL::BVUMINUS, d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusBVPlus ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 3821 of file bitvector_theorem_producer.cpp.
References CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractConst ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 1926 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), constantKids(), d_theoryBitvector, CVCL::EXTRACT, CVCL::TheoryBitvector::getBVConstValue(), CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractWhole ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 1959 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::EXTRACT, CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractExtract ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 1984 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), d_theoryBitvector, CVCL::EXTRACT, CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractConcat ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2029 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::TheoryBitvector::BVSize(), CVCL::CONCAT, d_theoryBitvector, CVCL::Expr::end(), CVCL::EXTRACT, CVCL::Theorem::getExpr(), CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem CVCL::BitvectorTheoremProducer::extractBitwise ( const Expr & e,

int kind,

const std::string & name

) [virtual]

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

Implements CVCL::BitvectorProofRules.
Referenced by extractAnd(), extractNeg(), and extractOr().

Theorem BitvectorTheoremProducer::extractAnd ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2137 of file bitvector_theorem_producer.cpp.
References CVCL::BVAND, and extractBitwise().

Theorem BitvectorTheoremProducer::extractOr ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2144 of file bitvector_theorem_producer.cpp.
References CVCL::BVOR, and extractBitwise().

Theorem BitvectorTheoremProducer::extractNeg ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2151 of file bitvector_theorem_producer.cpp.
References CVCL::BVNEG, and extractBitwise().

Theorem BitvectorTheoremProducer::negConst ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2223 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVNEG, constantKids(), d_theoryBitvector, CVCL::TheoryBitvector::getBVConstSize(), CVCL::TheoryBitvector::getBVConstValue(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negConcat ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2247 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVNEG, CVCL::CONCAT, d_theoryBitvector, CVCL::Expr::end(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negNeg ( const Expr & e ) [virtual]

~(~t) = t -- eliminate double negation

Implements CVCL::BitvectorProofRules.
Definition at line 2273 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVNEG, CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negBVand ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2290 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVAND, CVCL::BVNEG, d_theoryBitvector, CVCL::Expr::end(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoryBitvector::newBVOrExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negBVor ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2313 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVNEG, CVCL::BVOR, d_theoryBitvector, CVCL::Expr::end(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVAndExpr(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitwiseConst ( const Expr & e,

const std::vector< int > & idxs,

bool isAnd

)

Auxiliary method for andConst() and orConst().
c1&c2 = c (bit-wise AND constant bitvectors) c1 op c2 = c -- bit-wise AND and OR of constant bitvectors
Definition at line 2337 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVAND, CVCL::BVCONST, CVCL::BVOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::TheoryBitvector::getBVConstSize(), CVCL::TheoryBitvector::getBVConstValue(), CVCL::Expr::getKind(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoryBitvector::newBVAndExpr(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newBVOrExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::RAW_LIST, CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().
Referenced by andConst(), and orConst().

Theorem BitvectorTheoremProducer::bitwiseConcat ( const Expr & e,

int idx,

bool isAnd

)

Auxiliary method for andConcat() and orConcat().
Lifts concatenation to the top of bit-wise AND. Takes the bit-wise AND expression 'e' and the index 'i' of the concatenation.
Definition at line 2419 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVAND, CVCL::BVOR, CVCL::TheoryBitvector::BVSize(), CVCL::CONCAT, d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoryBitvector::newBVAndExpr(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVOrExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().
Referenced by andConcat(), and orConcat().

Theorem BitvectorTheoremProducer::bitwiseFlatten ( const Expr & e,

bool isAnd

)

Auxiliary method for andFlatten() and orFlatten().

Definition at line 2471 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BVAND, CVCL::BVOR, CVCL::TheoryBitvector::BVSize(), d_theoryBitvector, CVCL::Expr::end(), CVCL::Expr::getOp(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVOneString(), CVCL::TheoryBitvector::newBVZeroString(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), sameKidCheck(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().
Referenced by andFlatten(), and orFlatten().

Theorem BitvectorTheoremProducer::andConst ( const Expr & e,

const std::vector< int > & idxs

) [virtual]

c1&c2&t = c&t -- compute bit-wise AND of constant bitvector arguments

Parameters:

e is the bit-wise AND expression;

idxs are the indices of the constant bitvectors. There must be at least constant expressions in this rule.

Returns:
Theorem(e==e'), where e' is either a constant bitvector, or is a bit-wise AND with a single constant bitvector in e'[0].

Implements CVCL::BitvectorProofRules.
Definition at line 2548 of file bitvector_theorem_producer.cpp.
References bitwiseConst().

Theorem BitvectorTheoremProducer::andZero ( const Expr & e,

int idx

) [virtual]

0bin0...0 & t = 0bin0...0 -- bit-wise AND with zero bitvector

Parameters:

e is the bit-wise AND expr

idx is the index of the zero bitvector

Implements CVCL::BitvectorProofRules.
Definition at line 2558 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVAND, CVCL::BVCONST, CVCL::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CVCL::BitvectorTheoremProducer::andOne ( const Expr & e,

const std::vector< int > idxs

) [virtual]

0bin1...1 & t = t -- bit-wise AND with bitvector of 1's

Parameters:

e is the bit-wise AND expr

idxs is a vector of indices of the bitvectors of 1's which will be dropped

Implements CVCL::BitvectorProofRules.

Theorem BitvectorTheoremProducer::andConcat ( const Expr & e,

int idx

) [virtual]

... & (t1@...@tk) & ... = (...& t1 &...)@...@(...& tk &...)
Lifts concatenation to the top of bit-wise AND. Takes the bit-wise AND expression 'e' and the index 'i' of the concatenation.
Implements CVCL::BitvectorProofRules.
Definition at line 2639 of file bitvector_theorem_producer.cpp.
References bitwiseConcat().

Theorem BitvectorTheoremProducer::andFlatten ( const Expr & e ) [virtual]

(t1 & (t2 & t3) & t4) = t1 & t2 & t3 & t4 -- flatten bit-wise AND
Also reorders the terms according to a fixed total ordering
Implements CVCL::BitvectorProofRules.
Definition at line 2647 of file bitvector_theorem_producer.cpp.
References bitwiseFlatten().

Theorem BitvectorTheoremProducer::orConst ( const Expr & e,

const std::vector< int > & idxs

) [virtual]

c1|c2|t = c|t -- compute bit-wise OR of constant bitvector arguments

Parameters:

e is the bit-wise OR expression;

idxs are the indices of the constant bitvectors. There must be at least constant expressions in this rule.

Returns:
Theorem(e==e'), where e' is either a constant bitvector, or is a bit-wise OR with a single constant bitvector in e'[0].

Implements CVCL::BitvectorProofRules.
Definition at line 2654 of file bitvector_theorem_producer.cpp.
References bitwiseConst().

Theorem BitvectorTheoremProducer::orOne ( const Expr & e,

int idx

) [virtual]

0bin1...1 | t = 0bin1...1 -- bit-wise OR with bitvector of 1's

Parameters:

e is the bit-wise OR expr

idx is the index of the bitvector of 1's

Implements CVCL::BitvectorProofRules.
Definition at line 2665 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::BVCONST, CVCL::BVOR, d_theoryBitvector, CVCL::TheoryBitvector::getBVConstSize(), CVCL::TheoryBitvector::getBVConstValue(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), rat(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem CVCL::BitvectorTheoremProducer::orZero ( const Expr & e,

const std::vector< int > idxs

) [virtual]

0bin0...0 | t = t -- bit-wise OR with bitvector of 0's

Parameters:

e is the bit-wise OR expr

idxs is a vector of indices of the bitvectors of 0's which will be dropped

Implements CVCL::BitvectorProofRules.

Theorem BitvectorTheoremProducer::orConcat ( const Expr & e,

int idx

) [virtual]

... | (t1@...@tk) | ... = (...| t1 |...)@...@(...| tk |...)
Lifts concatenation to the top of bit-wise OR. Takes the bit-wise OR expression 'e' and the index 'i' of the concatenation.
Implements CVCL::BitvectorProofRules.
Definition at line 2806 of file bitvector_theorem_producer.cpp.
References bitwiseConcat().

Theorem BitvectorTheoremProducer::orFlatten ( const Expr & e ) [virtual]

(t1 | (t2 | t3) | t4) = t1 | t2 | t3 | t4 -- flatten bit-wise OR
Also reorders the terms according to a fixed total ordering
Implements CVCL::BitvectorProofRules.
Definition at line 2814 of file bitvector_theorem_producer.cpp.
References bitwiseFlatten().

int BitvectorTheoremProducer::sameKidCheck ( const Expr & e,

ExprMap< int > & likeTerms

)

checks if e is already present in likeTerms without conflicts. if yes return 1, else{ if conflict return -1 else return 0 } we have conflict if 1. the kind of e is BVNEG, and e[0] is already present in likeTerms 2. ~e is present in likeTerms already
Definition at line 2749 of file bitvector_theorem_producer.cpp.
References CVCL::BVNEG, d_theoryBitvector, CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), CVCL::Expr::getOpKind(), and CVCL::TheoryBitvector::newBVNegExpr().
Referenced by bitwiseFlatten().

Theorem BitvectorTheoremProducer::concatConst ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2821 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::CONCAT, constantKids(), d_theoryBitvector, CVCL::TheoryBitvector::getBVConstSize(), CVCL::TheoryBitvector::getBVConstValue(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::concatFlatten ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2844 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::CONCAT, CVCL::Expr::end(), CVCL::Expr::getOp(), CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::concatMergeExtract ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2867 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::arity(), CVCL::CONCAT, d_theoryBitvector, CVCL::EXTRACT, CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvplusConst ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2919 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::begin(), CVCL::BVPLUS, CVCL::TheoryBitvector::computeBVConst(), constantKids(), d_theoryBitvector, CVCL::Expr::end(), CVCL::floor(), CVCL::TheoryBitvector::getBVPlusParam(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::mod(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Rational::toString(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvmultConst ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 2959 of file bitvector_theorem_producer.cpp.
References CVCL::BVMULT, CVCL::TheoryBitvector::BVSize(), CVCL::TheoryBitvector::computeBVConst(), constantKids(), d_theoryBitvector, CVCL::floor(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::mod(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::typePredBit ( const Expr & e ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 3927 of file bitvector_theorem_producer.cpp.
References CVCL::BITVECTOR, bvOne(), CVCL::TheoryBitvector::BVSize(), bvZero(), d_theoryBitvector, CVCL::Expr::eqExpr(), CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::expandTypePred ( const Theorem & tp ) [virtual]

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

Implements CVCL::BitvectorProofRules.
Definition at line 3945 of file bitvector_theorem_producer.cpp.
References CVCL::andExpr(), bvOne(), CVCL::BVTYPEPRED, bvZero(), d_theoryBitvector, CVCL::Expr::eqExpr(), CVCL::Theory::falseExpr(), CVCL::Theorem::getAssumptionsCopy(), CVCL::TheoryBitvector::getBitvectorTypeParam(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Expr::getOpKind(), CVCL::Theorem::getProof(), CVCL::TheoryBitvector::getTypePredExpr(), CVCL::TheoryBitvector::getTypePredType(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::NOT, CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Expr CVCL::BitvectorTheoremProducer::rat ( const Rational & r ) [inline]

Create Expr from Rational (for convenience)
Definition at line 503 of file bitvector_theorem_producer.h.
References CVCL::TheoremProducer::d_em, and CVCL::ExprManager::newRatExpr().
Referenced by andZero(), bitExtractBitwise(), bitExtractBVMult(), bitExtractBVPlus(), bitExtractBVPlusPreComputed(), bitExtractConcatenation(), bitExtractConstant(), bitExtractConstBVMult(), bitExtractExtraction(), bitExtractFixedLeftShift(), bitExtractFixedRightShift(), bitExtractNot(), bitExtractSXRule(), bitwiseConcat(), bitwiseConst(), computeCarryPreComputed(), constMultToPlus(), orOne(), and zeroPaddingRule().

Expr BitvectorTheoremProducer::computeCarry ( const std::vector< Theorem > & t1BitExtractThms,

const std::vector< Theorem > & t2BitExtractThms,

int bitPos

)

Parameters:

t1BitExtractThms : input1 is vector of bitblasts of t1, from bit i-1 to 0

t2BitExtractThms : input2 is vector of bitblasts of t2, from bit i-1 to 0

bitPos : input3 is extracted * bitposition

Returns:
is the expression $t1[0] \wedge t2[0]$ if bitPos=0. this function is recursive; if bitPos > 0 then the output expression is
$(t1[i-1] \wedge t2[i-1]) \vee (t1[i-1] \wedge computeCarry(t1,t2,i-1)) \vee (t2[i-1] \wedge computeCarry(t1,t2,i-1))$

Definition at line 1274 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::andExpr(), and CVCL::orExpr().
Referenced by bitExtractBVPlus().

Expr BitvectorTheoremProducer::computeCarryPreComputed ( const Theorem & t1_i,

const Theorem & t2_i,

int bitPos,

int precomputedFlag

)

compute carryout of the current bits and cache them, and return

Definition at line 1376 of file bitvector_theorem_producer.cpp.
References CVCL::Expr::andExpr(), CVCL::TheoryBitvector::d_bvPlusCarryCacheLeftBV, CVCL::TheoryBitvector::d_bvPlusCarryCacheRightBV, d_theoryBitvector, CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::ExprMap< Data >::insert(), CVCL::Expr::orExpr(), and rat().
Referenced by bitExtractBVPlusPreComputed().

Member Data Documentation

TheoryBitvector* CVCL::BitvectorTheoremProducer::d_theoryBitvector [private]

Definition at line 52 of file bitvector_theorem_producer.h.
Referenced by andZero(), bitBlastDisEqnRule(), bitBlastEqnRule(), bitExtractBitwise(), bitExtractBVMult(), bitExtractBVPlus(), bitExtractBVPlusPreComputed(), bitExtractConcatenation(), bitExtractConstant(), bitExtractConstBVMult(), bitExtractExtraction(), bitExtractFixedLeftShift(), bitExtractFixedRightShift(), bitExtractNot(), bitExtractRewrite(), bitExtractSXRule(), bitExtractToExtract(), bitvectorFalseRule(), BitvectorTheoremProducer(), bitvectorTrueRule(), bitwiseConcat(), bitwiseConst(), bitwiseFlatten(), bvConstIneqn(), bvConstMultAssocRule(), bvMultAssocRule(), bvmultBVUminus(), bvmultConst(), bvMultDistRule(), bvPlusAssociativityRule(), bvplusConst(), bvplusZeroConcatRule(), bvuminusBVConst(), bvuminusBVMult(), bvuminusToBVPlus(), bvuminusVar(), collectLikeTermsOfPlus(), collectOneTermOfPlus(), combineLikeTermsRule(), computeCarryPreComputed(), concatConst(), concatMergeExtract(), constMultToPlus(), createNewPlusCollection(), eqConst(), eqToBits(), expandTypePred(), extractBVMult(), extractBVPlus(), extractConcat(), extractConst(), extractExtract(), extractWhole(), flattenBVPlus(), flipBVMult(), generalIneqn(), iteBVnegRule(), iteExtractRule(), leftShiftToConcat(), lhsEqRhsIneqn(), lhsMinusRhsRule(), negBVand(), negBVor(), negConcat(), negConst(), notBVLTRule(), oneCoeffBVMult(), orOne(), pad(), padBVLTRule(), padBVMult(), padBVPlus(), padSBVLTRule(), rightShiftToConcat(), sameKidCheck(), signBVLTRule(), signExtendRule(), sumNormalizedElements(), typePredBit(), zeroCoeffBVMult(), and zeroPaddingRule().

Expr CVCL::BitvectorTheoremProducer::d_bvZero [private]

Constant 1-bit bit-vector 0bin0.
instance of bitvector DP
Definition at line 54 of file bitvector_theorem_producer.h.
Referenced by BitvectorTheoremProducer(), and bvZero().

Expr CVCL::BitvectorTheoremProducer::d_bvOne [private]

Constant 1-bit bit-vector 0bin1.

Definition at line 56 of file bitvector_theorem_producer.h.
Referenced by BitvectorTheoremProducer(), and bvOne().

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

Generated on Thu Apr 13 16:57:46 2006 for CVC Lite by

1.4.4