CVC3
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>

Inherits CVC3::BitvectorProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::BitvectorTheoremProducer:
Collaboration graph
[legend]

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().

void BitvectorTheoremProducer::getPlusTerms ( const Expr e,
Rational known_term,
ExprMap< Rational > &  sumHashMap 
) [private]
Expr BitvectorTheoremProducer::buildPlusTerm ( int  bv_size,
Rational known_term,
ExprMap< Rational > &  sumHashMap 
) [private]
Expr BitvectorTheoremProducer::chopConcat ( int  bv_size,
Rational  c,
std::vector< Expr > &  concatKids 
) [private]
bool BitvectorTheoremProducer::okToSplit ( const Expr e) [private]
Theorem BitvectorTheoremProducer::bitvectorFalseRule ( const Theorem thm) [virtual]
Theorem BitvectorTheoremProducer::bitvectorTrueRule ( const Theorem thm) [virtual]
Theorem BitvectorTheoremProducer::bitBlastEqnRule ( const Expr e,
const Expr f 
) [virtual]
Theorem BitvectorTheoremProducer::bitBlastDisEqnRule ( const Theorem e,
const Expr f 
) [virtual]
Theorem BitvectorTheoremProducer::signExtendRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::padBVLTRule ( const Expr e,
int  len 
) [virtual]
Theorem BitvectorTheoremProducer::padBVSLTRule ( const Expr e,
int  len 
) [virtual]
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])

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

Implements CVC3::BitvectorProofRules.

Definition at line 437 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVCONST, 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::notBVEQ1Rule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::notBVLTRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::lhsEqRhsIneqn ( const Expr e,
int  kind 
) [virtual]
Theorem BitvectorTheoremProducer::zeroLeq ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvConstIneqn ( const Expr e,
int  kind 
) [virtual]
Theorem BitvectorTheoremProducer::generalIneqn ( const Expr e,
const Theorem lhs_i,
const Theorem rhs_i,
int  kind 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractAllToConstEq ( std::vector< Theorem > &  thms) [virtual]
Theorem BitvectorTheoremProducer::bitExtractToExtract ( const Theorem thm) [virtual]
Theorem BitvectorTheoremProducer::bitExtractRewrite ( const Expr x) [virtual]
Theorem BitvectorTheoremProducer::bitExtractConstant ( const Expr x,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractConcatenation ( const Expr x,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractConstBVMult ( const Expr t,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractBVMult ( const Expr t,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractExtraction ( const Expr x,
int  i 
) [virtual]
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 CVC3::BitvectorProofRules.

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(), TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractBVPlusPreComputed ( const Theorem t1_i,
const Theorem t2_i,
const Expr bvPlusTerm,
int  bitPos,
int  precomputed 
) [virtual]
Theorem BitvectorTheoremProducer::bvPlusAssociativityRule ( const Expr bvPlusTerm) [virtual]
Theorem BitvectorTheoremProducer::bitExtractNot ( const Expr x,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractBitwise ( const Expr x,
int  i,
int  kind 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractFixedLeftShift ( const Expr x,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractFixedRightShift ( const Expr x,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractBVSHL ( const Expr x,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractBVLSHR ( const Expr x,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::bitExtractBVASHR ( const Expr x,
int  i 
) [virtual]
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 CVC3::BitvectorProofRules.

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().

Theorem BitvectorTheoremProducer::bitExtractSXRule ( const Expr e,
int  i 
) [virtual]
Theorem BitvectorTheoremProducer::eqConst ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::eqToBits ( const Theorem eq) [virtual]
Theorem BitvectorTheoremProducer::leftShiftToConcat ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::constWidthLeftShiftToConcat ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::rightShiftToConcat ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvshlToConcat ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvshlSplit ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvlshrToConcat ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvShiftZero ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvashrToConcat ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::rewriteXNOR ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::rewriteNAND ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::rewriteNOR ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::rewriteBVCOMP ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::rewriteBVSub ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::constMultToPlus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvplusZeroConcatRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::zeroCoeffBVMult ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::oneCoeffBVMult ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::flipBVMult ( const Expr e) [virtual]
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:
lenis the desired bvLength of the resulting bitvector
eis 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::padBVPlus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::padBVMult ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvConstMultAssocRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvMultAssocRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvMultDistRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::flattenBVPlus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::combineLikeTermsRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::lhsMinusRhsRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::extractBVMult ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::extractBVPlus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::iteExtractRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::iteBVnegRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvuminusBVConst ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvuminusBVMult ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvuminusBVUminus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvuminusVar ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvmultBVUminus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvuminusToBVPlus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvuminusBVPlus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::extractConst ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::extractWhole ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::extractExtract ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::extractConcat ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::extractBitwise ( const Expr e,
int  kind,
const std::string &  name 
) [virtual]
Theorem BitvectorTheoremProducer::extractAnd ( const Expr e) [virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2571 of file bitvector_theorem_producer.cpp.

References CVC3::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 CVC3::BitvectorProofRules.

Definition at line 2578 of file bitvector_theorem_producer.cpp.

References CVC3::BVOR, and extractBitwise().

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 2585 of file bitvector_theorem_producer.cpp.

References CVC3::BVNEG, and extractBitwise().

Theorem BitvectorTheoremProducer::negConst ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::negConcat ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::negNeg ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::negElim ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::negBVand ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::negBVor ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::negBVxor ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::negBVxnor ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bitwiseConst ( const Expr e,
const std::vector< int > &  idxs,
int  kind 
) [virtual]
Theorem BitvectorTheoremProducer::bitwiseConcat ( const Expr e,
int  kind 
) [virtual]
Theorem BitvectorTheoremProducer::bitwiseFlatten ( const Expr e,
int  kind 
) [virtual]
Theorem BitvectorTheoremProducer::bitwiseConstElim ( const Expr e,
int  idx,
int  kind 
) [virtual]
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().

Theorem BitvectorTheoremProducer::concatConst ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::concatFlatten ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::concatMergeExtract ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvplusConst ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvmultConst ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::typePredBit ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::expandTypePred ( const Theorem tp) [virtual]
Expr CVC3::BitvectorTheoremProducer::rat ( const Rational r) [inline]
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::isolate_var ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::liftConcatBVMult ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::canonBVMult ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::liftConcatBVPlus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::canonBVPlus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::canonBVUMinus ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::processExtract ( const Theorem e,
bool &  solvedForm 
) [virtual]
Theorem BitvectorTheoremProducer::canonBVEQ ( const Expr e,
int  maxEffort = 3 
) [virtual]
Theorem BitvectorTheoremProducer::distributive_rule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::BVMult_order_subterms ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::MarkNonSolvableEq ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::zeroExtendRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::repeatRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::rotlRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::rotrRule ( const Expr e) [virtual]
Theorem BitvectorTheoremProducer::bvUDivConst ( const Expr divExpr) [virtual]
Theorem BitvectorTheoremProducer::bvUDivTheorem ( const Expr divExpr) [virtual]
Theorem BitvectorTheoremProducer::bvURemConst ( const Expr remExpr) [virtual]
Theorem BitvectorTheoremProducer::bvURemRewrite ( const Expr remExpr) [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]
Theorem BitvectorTheoremProducer::bvSDivRewrite ( const Expr sDivExpr) [virtual]
Theorem BitvectorTheoremProducer::bvSRemRewrite ( const Expr sRemExpr) [virtual]
Theorem BitvectorTheoremProducer::bvSModRewrite ( const Expr sModExpr) [virtual]
Theorem BitvectorTheoremProducer::zeroBVOR ( const Expr orEqZero) [virtual]
Theorem BitvectorTheoremProducer::oneBVAND ( const Expr andEqOne) [virtual]
Theorem BitvectorTheoremProducer::constEq ( const Expr eq) [virtual]
bool BitvectorTheoremProducer::solveExtractOverlapApplies ( const Expr eq) [virtual]

Returns true if equation is of the form x[i:j] = x[k:l], where the extracted segments overlap, i.e. i > j >= k > l or k > i >= l > j.

Implements CVC3::BitvectorProofRules.

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().

Theorem BitvectorTheoremProducer::solveExtractOverlap ( const Expr eq) [virtual]

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: