Public Member Functions | Private Member Functions | Private Attributes

CVC3::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 CVC3::BitvectorTheoremProducer:
CVC3::BitvectorProofRules CVC3::TheoremProducer

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


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 41 of file bitvector_theorem_producer.h.


Constructor & Destructor Documentation

BitvectorTheoremProducer::BitvectorTheoremProducer ( TheoryBitvector theoryBitvector  ) 

Constructor: constructs an instance of bitvector DP.

Definition at line 50 of file bitvector_theorem_producer.cpp.

References d_bvOne, d_bvZero, d_theoryBitvector, and CVC3::TheoryBitvector::newBVConstExpr().

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

Definition at line 90 of file bitvector_theorem_producer.h.


Member Function Documentation

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

Return cached constant 0bin0.

Definition at line 50 of file bitvector_theorem_producer.h.

References d_bvZero.

Referenced by bitExtractToExtract(), expandTypePred(), signBVLTRule(), and typePredBit().

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

Return cached constant 0bin1.

Definition at line 52 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 3723 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::begin(), CVC3::BVCONST, CVC3::BVMULT, CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::clear(), collectOneTermOfPlus(), CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Expr::end(), CVC3::Expr::getOpKind(), and CVC3::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 3692 of file bitvector_theorem_producer.cpp.

References d_theoryBitvector, CVC3::ExprMap< Data >::empty(), CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Theorem::getRHS(), CVC3::TheoryBitvector::newBVNegExpr(), and CVC3::TheoryBitvector::pushNegationRec().

Referenced by collectLikeTermsOfPlus().

void BitvectorTheoremProducer::createNewPlusCollection ( const Expr e,
const ExprMap< Rational > &  likeTerms,
Rational plusConstant,
std::vector< Expr > &  result 
) [private]
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 3845 of file bitvector_theorem_producer.cpp.

References d_theoryBitvector, CVC3::TheoryBitvector::newBVPlusExpr(), and CVC3::TheoryBitvector::newBVZeroString().

Referenced by combineLikeTermsRule().

Theorem BitvectorTheoremProducer::bitBlastEqnRule ( const Expr e,
const Expr f 
)
Theorem BitvectorTheoremProducer::signBVLTRule ( const Expr e,
const Theorem topBit0,
const Theorem topBit1 
)

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

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] = e1[n-1] AND e0[n-2:0] <= e1[n-2:0])

Definition at line 437 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::BITVECTOR, bvOne(), CVC3::TheoryBitvector::BVSize(), CVC3::BVSLE, CVC3::BVSLT, bvZero(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Theory::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractConstant ( const Expr x,
int  i 
)
Theorem BitvectorTheoremProducer::bitExtractConcatenation ( const Expr x,
int  i 
)
Theorem BitvectorTheoremProducer::bitExtractBVPlus ( const std::vector< Theorem > &  t1,
const std::vector< Theorem > &  t2,
const Expr bvPlusTerm,
int  i 
)
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

Definition at line 1256 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVPLUS, CHECK_PROOFS, CHECK_SOUND, computeCarry(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::Expr::getOpKind(), CVC3::Expr::iffExpr(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvPlusAssociativityRule ( const Expr bvPlusTerm  ) 
Theorem BitvectorTheoremProducer::zeroPaddingRule ( const Expr e,
int  r 
)
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)

Definition at line 1470 of file bitvector_theorem_producer.cpp.

References CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Expr BitvectorTheoremProducer::pad ( int  len,
const Expr e 
)

converts e to a bitvector of length rat

Converts e into a BVVECTOR of bvLength 'len'.

Parameters:
len is the desired bvLength of the resulting bitvector
e is the original bitvector of arbitrary bvLength

Definition at line 3424 of file bitvector_theorem_producer.cpp.

References CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), d_theoryBitvector, DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), and CVC3::Expr::toString().

Referenced by bvUDivTheorem(), oneCoeffBVMult(), padBVLTRule(), padBVMult(), and padBVPlus().

Theorem BitvectorTheoremProducer::bvuminusBVPlus ( const Expr e  ) 
Theorem BitvectorTheoremProducer::extractAnd ( const Expr e  ) 

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

Definition at line 2571 of file bitvector_theorem_producer.cpp.

References CVC3::BVAND, and extractBitwise().

Theorem BitvectorTheoremProducer::extractOr ( const Expr e  ) 

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

Definition at line 2578 of file bitvector_theorem_producer.cpp.

References CVC3::BVOR, and extractBitwise().

Theorem BitvectorTheoremProducer::extractNeg ( const Expr e  ) 

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

Definition at line 2585 of file bitvector_theorem_producer.cpp.

References CVC3::BVNEG, and extractBitwise().

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 3160 of file bitvector_theorem_producer.cpp.

References CVC3::BVNEG, d_theoryBitvector, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getOpKind(), and CVC3::TheoryBitvector::newBVNegExpr().

Referenced by bitwiseFlatten().

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 1305 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), DebugAssert, and CVC3::orExpr().

Referenced by bitExtractBVPlus().

Expr BitvectorTheoremProducer::computeCarryPreComputed ( const Theorem t1_i,
const Theorem t2_i,
int  bitPos,
int  precomputedFlag 
)
Theorem BitvectorTheoremProducer::canonBVPlus ( const Expr e  )  [virtual]
Theorem BitvectorTheoremProducer::bitblastBVMult ( const std::vector< Theorem > &  a_bits,
const std::vector< Theorem > &  b_bits,
const Expr a_times_b,
std::vector< Theorem > &  output_bits 
) [virtual]
Theorem BitvectorTheoremProducer::bitblastBVPlus ( const std::vector< Theorem > &  a_bits,
const std::vector< Theorem > &  b_bits,
const Expr a_plus_b,
std::vector< Theorem > &  output_bits 
) [virtual]
bool BitvectorTheoremProducer::solveExtractOverlapApplies ( const Expr eq  ) 

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.

Definition at line 6687 of file bitvector_theorem_producer.cpp.

References d_theoryBitvector, CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), and CVC3::TheoryBitvector::getExtractLow().

Referenced by solveExtractOverlap().


Member Data Documentation

Definition at line 44 of file bitvector_theorem_producer.h.

Referenced by bitblastBVMult(), bitblastBVPlus(), bitBlastDisEqnRule(), bitBlastEqnRule(), bitExtractAllToConstEq(), bitExtractBitwise(), bitExtractBVASHR(), bitExtractBVLSHR(), bitExtractBVMult(), bitExtractBVPlus(), bitExtractBVPlusPreComputed(), bitExtractBVSHL(), bitExtractConcatenation(), bitExtractConstant(), bitExtractConstBVMult(), bitExtractExtraction(), bitExtractFixedLeftShift(), bitExtractFixedRightShift(), bitExtractNot(), bitExtractRewrite(), bitExtractSXRule(), bitExtractToExtract(), bitvectorFalseRule(), BitvectorTheoremProducer(), bitvectorTrueRule(), bitwiseConcat(), bitwiseConst(), bitwiseConstElim(), bitwiseFlatten(), buildPlusTerm(), bvashrToConcat(), bvConstIneqn(), bvConstMultAssocRule(), bvlshrToConcat(), BVMult_order_subterms(), bvMultAssocRule(), bvmultBVUminus(), bvmultConst(), bvMultDistRule(), bvPlusAssociativityRule(), bvplusConst(), bvplusZeroConcatRule(), bvSDivRewrite(), bvShiftZero(), bvshlSplit(), bvshlToConcat(), bvSModRewrite(), bvSRemRewrite(), bvUDivConst(), bvUDivTheorem(), bvuminusBVConst(), bvuminusBVMult(), bvuminusToBVPlus(), bvuminusVar(), bvURemConst(), bvURemRewrite(), canonBVEQ(), canonBVMult(), canonBVPlus(), canonBVUMinus(), chopConcat(), collectLikeTermsOfPlus(), collectOneTermOfPlus(), combineLikeTermsRule(), computeCarryPreComputed(), concatConst(), concatMergeExtract(), constEq(), constMultToPlus(), constWidthLeftShiftToConcat(), createNewPlusCollection(), distributive_rule(), eqConst(), eqToBits(), expandTypePred(), extractBitwise(), extractBVMult(), extractBVPlus(), extractConcat(), extractConst(), extractExtract(), extractWhole(), flattenBVPlus(), flipBVMult(), generalIneqn(), getPlusTerms(), isolate_var(), iteBVnegRule(), iteExtractRule(), leftShiftToConcat(), lhsEqRhsIneqn(), lhsMinusRhsRule(), liftConcatBVMult(), liftConcatBVPlus(), MarkNonSolvableEq(), negBVand(), negBVor(), negBVxnor(), negBVxor(), negConcat(), negConst(), negElim(), notBVEQ1Rule(), notBVLTRule(), okToSplit(), oneBVAND(), oneCoeffBVMult(), pad(), padBVLTRule(), padBVMult(), padBVPlus(), padBVSLTRule(), processExtract(), repeatRule(), rewriteBVCOMP(), rewriteBVSub(), rewriteNAND(), rewriteNOR(), rewriteXNOR(), rightShiftToConcat(), rotlRule(), rotrRule(), sameKidCheck(), signBVLTRule(), signExtendRule(), solveExtractOverlap(), solveExtractOverlapApplies(), sumNormalizedElements(), typePredBit(), zeroBVOR(), zeroCoeffBVMult(), zeroExtendRule(), zeroLeq(), and zeroPaddingRule().

Constant 1-bit bit-vector 0bin0.

instance of bitvector DP

Definition at line 46 of file bitvector_theorem_producer.h.

Referenced by BitvectorTheoremProducer(), and bvZero().

Constant 1-bit bit-vector 0bin1.

Definition at line 48 of file bitvector_theorem_producer.h.

Referenced by BitvectorTheoremProducer(), and bvOne().


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