CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | List of all members
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

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 padBVSLTRule (const Expr &e, int len)
 Sign Extend the kids of BVSLT/BVSLE to make their length equal.
Theorem signBVLTRule (const Expr &e, const Theorem &topBit0, const Theorem &topBit1)
Theorem notBVEQ1Rule (const Expr &e)
Theorem notBVLTRule (const Expr &e)
Theorem lhsEqRhsIneqn (const Expr &e, int kind)
 if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
Theorem zeroLeq (const Expr &e)
 |= 0 <= foo <-> 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 bitExtractAllToConstEq (std::vector< Theorem > &thms)
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)
 Extract from bitwise AND, OR, or XOR.
Theorem bitExtractFixedLeftShift (const Expr &x, int i)
Theorem bitExtractFixedRightShift (const Expr &x, int i)
Theorem bitExtractBVSHL (const Expr &x, int i)
Theorem bitExtractBVLSHR (const Expr &x, int i)
Theorem bitExtractBVASHR (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 constWidthLeftShiftToConcat (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 bvshlToConcat (const Expr &e)
 BVSHL(t,c) = t[n-c,0] @ 0bin00...00.
Theorem bvshlSplit (const Expr &e)
 BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
Theorem bvlshrToConcat (const Expr &e)
 BVLSHR(t,c) = 0bin00...00 @ t[n-1,c].
Theorem bvShiftZero (const Expr &e)
 All shifts over a 0 constant = 0.
Theorem bvashrToConcat (const Expr &e)
 BVASHR(t,c) = SX(t[n-1,c], n-1)
Theorem rewriteXNOR (const Expr &e)
 a XNOR b <=> (~a & ~b) | (a & b)
Theorem rewriteNAND (const Expr &e)
 a NAND b <=> ~(a & b)
Theorem rewriteNOR (const Expr &e)
 a NOR b <=> ~(a | b)
Theorem rewriteBVCOMP (const Expr &e)
 BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
Theorem rewriteBVSub (const Expr &e)
 a - b <=> a + (-b)
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 negElim (const Expr &e)
 ~t = -1*t + 1 – eliminate 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 negBVxor (const Expr &e)
 ~(t1 xor t2) = ~t1 xor t2
Theorem negBVxnor (const Expr &e)
 ~(t1 xnor t2) = t1 xor t2
Theorem bitwiseConst (const Expr &e, const std::vector< int > &idxs, int kind)
 Combine constants in bitwise AND, OR, XOR.
Theorem bitwiseConcat (const Expr &e, int kind)
 Lifts concatenation above bitwise operators.
Theorem bitwiseFlatten (const Expr &e, int kind)
 Flatten bitwise operation.
Theorem bitwiseConstElim (const Expr &e, int idx, int kind)
 Simplify bitwise operator containing a constant child.
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
virtual Theorem isolate_var (const Expr &e)
 isolate a variable with coefficient = 1 on the Lhs of an
virtual Theorem liftConcatBVMult (const Expr &e)
virtual Theorem canonBVMult (const Expr &e)
 canonize BVMult expressions in order to get one coefficient
virtual Theorem liftConcatBVPlus (const Expr &e)
virtual Theorem canonBVPlus (const Expr &e)
 canonize BVPlus expressions in order to get just one
virtual Theorem canonBVUMinus (const Expr &e)
 canonize BVMinus expressions: push the minus to the leafs in
virtual Theorem processExtract (const Theorem &e, bool &solvedForm)
virtual Theorem canonBVEQ (const Expr &e, int maxEffort=3)
virtual Theorem distributive_rule (const Expr &e)
 apply the distributive rule on the BVMULT expression e
virtual Theorem BVMult_order_subterms (const Expr &e)
virtual Theorem MarkNonSolvableEq (const Expr &e)
virtual Theorem zeroExtendRule (const Expr &e)
 BVZEROEXTEND(e, i) = zeroString @ e.
virtual Theorem repeatRule (const Expr &e)
 BVREPEAT(e, i) = e @ e @ ... @ e.
virtual Theorem rotlRule (const Expr &e)
 BVROTL(e, i) = a[n-i-1:0] @ a[n-1:n-i].
virtual Theorem rotrRule (const Expr &e)
 BVROTR(e, i) = a[i-1:0] @ a[n-1:i].
virtual Theorem bvUDivConst (const Expr &divExpr)
virtual Theorem bvUDivTheorem (const Expr &divExpr)
virtual Theorem bvURemConst (const Expr &remExpr)
virtual Theorem bvURemRewrite (const Expr &remExpr)
virtual Theorem bitblastBVMult (const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_times_b, std::vector< Theorem > &output_bits)
virtual Theorem bitblastBVPlus (const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_plus_b, std::vector< Theorem > &output_bits)
virtual Theorem bvSDivRewrite (const Expr &sDivExpr)
virtual Theorem bvSRemRewrite (const Expr &sRemExpr)
virtual Theorem bvSModRewrite (const Expr &sModExpr)
virtual Theorem zeroBVOR (const Expr &orEqZero)
virtual Theorem oneBVAND (const Expr &andEqOne)
virtual Theorem constEq (const Expr &eq)
bool solveExtractOverlapApplies (const Expr &eq)
Theorem solveExtractOverlap (const Expr &eq)
- Public Member Functions inherited from CVC3::BitvectorProofRules
virtual ~BitvectorProofRules ()
- Public Member Functions inherited from CVC3::TheoremProducer
 TheoremProducer (TheoremManager *tm)
virtual ~TheoremProducer ()
bool withProof ()
 Testing whether to generate proofs.
bool withAssumptions ()
 Testing whether to generate assumptions.
Proof newLabel (const Expr &e)
 Create a new proof label (bound variable) for an assumption (formula)
Proof newPf (const std::string &name)
Proof newPf (const std::string &name, const Expr &e)
Proof newPf (const std::string &name, const Proof &pf)
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2)
Proof newPf (const std::string &name, const Expr &e, const Proof &pf)
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end)
Proof newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)
Proof newPf (const std::string &name, const std::vector< Expr > &args)
Proof newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args)
Proof newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs)
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)
Proof newPf (const std::string &name, const std::vector< Proof > &pfs)
Proof newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf)
Proof newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)
Proof newPf (const Proof &label, const Expr &frm, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label formula proof)
Proof newPf (const Proof &label, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label proof).
Proof newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)
 Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf)
Proof newPf (const std::vector< Proof > &labels, const Proof &pf)

Private Member Functions

const ExprbvZero () const
 Return cached constant 0bin0.
const ExprbvOne () 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)
void getPlusTerms (const Expr &e, Rational &known_term, ExprMap< Rational > &sumHashMap)
Expr buildPlusTerm (int bv_size, Rational &known_term, ExprMap< Rational > &sumHashMap)
Expr chopConcat (int bv_size, Rational c, std::vector< Expr > &concatKids)
bool okToSplit (const Expr &e)

Private Attributes

TheoryBitvectord_theoryBitvector
Expr d_bvZero
 Constant 1-bit bit-vector 0bin0.
Expr d_bvOne
 Constant 1-bit bit-vector 0bin1.

Additional Inherited Members

- Protected Member Functions inherited from CVC3::TheoremProducer
Theorem newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf)
 Create a new theorem. See also newRWTheorem() and newReflTheorem()
Theorem newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 Create a rewrite theorem: lhs = rhs.
Theorem newReflTheorem (const Expr &e)
 Create a reflexivity theorem.
Theorem newAssumption (const Expr &thm, const Proof &pf, int scope=-1)
Theorem3 newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf)
Theorem3 newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
void soundError (const std::string &file, int line, const std::string &cond, const std::string &msg)
- Protected Attributes inherited from CVC3::TheoremProducer
TheoremManagerd_tm
ExprManagerd_em
const bool * d_checkProofs
Op d_pfOp
Expr d_hole

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
inlineprivate

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
inlineprivate

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

Bit-blast the multiplication a_times_b given the bits in a_bits and b_bits. The resulting output bits will be in the vector output_bits. The return value is a theorem saying there is no overflow for this multiplication. (TODO, it's just an empty theorem for now).

Implements CVC3::BitvectorProofRules.

Definition at line 6324 of file bitvector_theorem_producer.cpp.

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

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

TheoryBitvector* CVC3::BitvectorTheoremProducer::d_theoryBitvector
private

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

Expr CVC3::BitvectorTheoremProducer::d_bvZero
private

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

Expr CVC3::BitvectorTheoremProducer::d_bvOne
private

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: