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:

[legend]

Collaboration diagram for CVC3::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 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)

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

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

---

Constructor & Destructor Documentation

BitvectorTheoremProducer::BitvectorTheoremProducer

(

TheoryBitvector *

theoryBitvector

)

Constructor: constructs an instance of bitvector DP.

Definition at line 49 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 3722 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 3691 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]

Create a vector which will form the next PVPLUS. Use the colleciton of likeTerms, and the constant additive plusConstant

Definition at line 3784 of file bitvector_theorem_producer.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::BITVECTOR, boundedModulo(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::ExprMap< Data >::end(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::pushNegationRec(), and CVC3::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 3844 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]

Definition at line 5019 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::BVNEG, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, concatConst(), d_theoryBitvector, DebugAssert, CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), and CVC3::pow().

Referenced by canonBVEQ(), canonBVMult(), canonBVPlus(), chopConcat(), and rewriteBVSub().

Expr BitvectorTheoremProducer::buildPlusTerm	(	int	bv_size,
		Rational &	known_term,
		ExprMap< Rational > &	sumHashMap
	)			[private]

Definition at line 5297 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::BVCONST, CVC3::BVNEG, CVC3::TheoryBitvector::BVSize(), chopConcat(), CVC3::CONCAT, d_theoryBitvector, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVMultPadExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), and CVC3::pow().

Referenced by canonBVEQ(), canonBVMult(), canonBVPlus(), chopConcat(), and rewriteBVSub().

Expr BitvectorTheoremProducer::chopConcat	(	int	bv_size,
		Rational	c,
		std::vector< Expr > &	concatKids
	)			[private]

Definition at line 5168 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), buildPlusTerm(), CVC3::BVCONST, CVC3::TheoryBitvector::BVSize(), CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, d_theoryBitvector, DebugAssert, CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), getPlusTerms(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), and CVC3::pow().

Referenced by buildPlusTerm().

bool BitvectorTheoremProducer::okToSplit

(

const Expr &

e

)

[private]

Definition at line 5656 of file bitvector_theorem_producer.cpp.

References CVC3::BVAND, CVC3::BVASHR, CVC3::BVCONST, CVC3::BVLSHR, CVC3::BVMULT, CVC3::BVNEG, CVC3::BVOR, CVC3::BVPLUS, CVC3::BVSDIV, CVC3::BVSHL, CVC3::BVSMOD, CVC3::BVSREM, CVC3::BVUDIV, CVC3::BVUREM, CVC3::BVXOR, d_theoryBitvector, CVC3::EXTRACT, FatalAssert, CVC3::Expr::getOpKind(), and CVC3::Theory::isLeaf().

Referenced by canonBVEQ().

Theorem BitvectorTheoremProducer::bitvectorFalseRule

(

const Theorem &

thm

)

[virtual]

Parameters:

thm

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

Returns:

(e1=e2)<=>false

Implements CVC3::BitvectorProofRules.

Definition at line 65 of file bitvector_theorem_producer.cpp.

References CVC3::BOOLEXTRACT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitvectorTrueRule

(

const Theorem &

thm

)

[virtual]

Parameters:

thm

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

Returns:

(e1!=e2)<=>true

Implements CVC3::BitvectorProofRules.

Definition at line 103 of file bitvector_theorem_producer.cpp.

References CVC3::BOOLEXTRACT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isIff(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::NOT, CVC3::Expr::toString(), and CVC3::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:

where each of

denotes a formula over variables in

respectively

Implements CVC3::BitvectorProofRules.

Definition at line 141 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BOOLEXTRACT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Expr::isAnd(), CVC3::Expr::isEq(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::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:

where each of

denotes a formula over variables in

respectively

Implements CVC3::BitvectorProofRules.

Definition at line 224 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BOOLEXTRACT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Expr::isIff(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::Theorem::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::signExtendRule

(

const Expr &

e

)

[virtual]

sign extend the input SX(e) appropriately

signExtendRule: pads the input e with topBit to length len

Implements CVC3::BitvectorProofRules.

Definition at line 338 of file bitvector_theorem_producer.cpp.

References CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::SX, CVC3::Expr::toString(), and CVC3::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.

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

Implements CVC3::BitvectorProofRules.

Definition at line 304 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVLE, CVC3::BVLT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::padBVSLTRule	(	const Expr &	e,
		int	len
	)			[virtual]

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 396 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVSLE, CVC3::BVSLT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoryBitvector::newSXExpr(), CVC3::Expr::toString(), and CVC3::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])

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 605 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::Expr::eqExpr(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::NOT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::notBVLTRule

(

const Expr &

e

)

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

Definition at line 630 of file bitvector_theorem_producer.cpp.

References CVC3::BVLE, CVC3::BVLT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::NOT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::lhsEqRhsIneqn	(	const Expr &	e,
		int	kind
	)			[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 657 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVLE, CVC3::BVLT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::zeroLeq

(

const Expr &

e

)

[virtual]

|= 0 <= foo <-> TRUE

Implements CVC3::BitvectorProofRules.

Definition at line 685 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVLE, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvConstIneqn	(	const Expr &	e,
		int	kind
	)			[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 703 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVLE, CVC3::BVLT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::generalIneqn	(	const Expr &	e,
		const Theorem &	lhs_i,
		const Theorem &	rhs_i,
		int	kind
	)			[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 761 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BOOLEXTRACT, CVC3::BVLE, CVC3::BVLT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::Expr::isFalse(), CVC3::Expr::isNull(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTrue(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::toString(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractAllToConstEq

(

std::vector< Theorem > &

thms

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 894 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BOOLEXTRACT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Expr::getKind(), CVC3::IFF, CVC3::Expr::isBoolConst(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractToExtract

(

const Theorem &

thm

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 926 of file bitvector_theorem_producer.cpp.

References CVC3::BOOLEXTRACT, bvOne(), bvZero(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Theorem::getExpr(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::Expr::isNot(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractRewrite

(

const Expr &

x

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 947 of file bitvector_theorem_producer.cpp.

References CVC3::BOOLEXTRACT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractConstant	(	const Expr &	x,
		int	i
	)			[virtual]

Parameters:

	x	: input1 is bitvector constant
	i	: input2 is extracted bitposition

Returns:

, if bitposition has a 1;

, if the bitposition has a 0

Implements CVC3::BitvectorProofRules.

Definition at line 976 of file bitvector_theorem_producer.cpp.

References CVC3::BVCONST, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractConcatenation	(	const Expr &	x,
		int	i
	)			[virtual]

Parameters:

	x	: input1 is bitvector binary concatenation
	i	: input2 is extracted bitposition

Returns:

, where

, another case of boolextract over concatenation is:

, where

Implements CVC3::BitvectorProofRules.

Definition at line 1016 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Theory::getBaseType(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::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 CVC3::BitvectorProofRules.

Definition at line 1073 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::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 CVC3::BitvectorProofRules.

Definition at line 1140 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::Theory::trueExpr(), and CVC3::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:

, where

Implements CVC3::BitvectorProofRules.

Definition at line 1205 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::Type::getExpr(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::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:

, when

, we have

, 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 1255 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::bitExtractBVPlusPreComputed	(	const Theorem &	t1_i,
		const Theorem &	t2_i,
		const Expr &	bvPlusTerm,
		int	bitPos,
		int	precomputed
	)			[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 1336 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BOOLEXTRACT, CVC3::BVPLUS, CHECK_PROOFS, CHECK_SOUND, computeCarryPreComputed(), d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::iffExpr(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Theorem::toString(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::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 CVC3::BitvectorProofRules.

Definition at line 1496 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractNot	(	const Expr &	x,
		int	i
	)			[virtual]

Parameters:

	x	: input1 is bitwise NEGATION
	i	: input2 is extracted bitposition

Returns:

Implements CVC3::BitvectorProofRules.

Definition at line 1538 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::bitExtractBitwise	(	const Expr &	x,
		int	i,
		int	kind
	)			[virtual]

Extract from bitwise AND, OR, or XOR.

Implements CVC3::BitvectorProofRules.

Definition at line 1574 of file bitvector_theorem_producer.cpp.

References CVC3::AND, CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BITVECTOR, CVC3::BVAND, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Theory::getEM(), CVC3::Type::getExpr(), CVC3::ExprManager::getKindName(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::OR, rat(), CVC3::Theorem::toString(), CVC3::Type::toString(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::TheoremProducer::withProof(), and CVC3::XOR.

Theorem BitvectorTheoremProducer::bitExtractFixedLeftShift	(	const Expr &	x,
		int	i
	)			[virtual]

Parameters:

	x	: input1 is bitvector FIXED SHIFT
	i	: input2 is extracted bitposition

Returns:

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

Implements CVC3::BitvectorProofRules.

Definition at line 1618 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::bitExtractFixedRightShift	(	const Expr &	x,
		int	i
	)			[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 1667 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::bitExtractBVSHL	(	const Expr &	x,
		int	i
	)			[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 1720 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVSHL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::OR, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractBVLSHR	(	const Expr &	x,
		int	i
	)			[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 1774 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVLSHR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::OR, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractBVASHR	(	const Expr &	x,
		int	i
	)			[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 1828 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVASHR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::OR, rat(), CVC3::Expr::toString(), and CVC3::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 CVC3::BitvectorProofRules.

Definition at line 1469 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]

bitExtractSXRule

Implements CVC3::BitvectorProofRules.

Definition at line 379 of file bitvector_theorem_producer.cpp.

References d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theorem::getRHS(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), signExtendRule(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::eqConst

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 1892 of file bitvector_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Expr::isEq(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::eqToBits

(

const Theorem &

eq

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 1910 of file bitvector_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theory::getBaseType(), CVC3::Theorem::getExpr(), CVC3::Type::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::leftShiftToConcat

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 1943 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::Expr::getOpKind(), CVC3::LEFTSHIFT, CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::constWidthLeftShiftToConcat

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 1967 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONST_WIDTH_LEFTSHIFT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::rightShiftToConcat

(

const Expr &

e

)

[virtual]

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 2000 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::RIGHTSHIFT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvshlToConcat

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2032 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVSHL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Rational::getInt(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvshlSplit

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2067 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVSHL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvlshrToConcat

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2106 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVLSHR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Rational::getInt(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvShiftZero

(

const Expr &

e

)

[virtual]

All shifts over a 0 constant = 0.

Implements CVC3::BitvectorProofRules.

Definition at line 2134 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVASHR, CVC3::BVCONST, CVC3::BVLSHR, CVC3::BVSHL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONST_WIDTH_LEFTSHIFT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::LEFTSHIFT, CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::RIGHTSHIFT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvashrToConcat

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2154 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVASHR, CVC3::BVCONST, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Rational::getInt(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoryBitvector::newSXExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::rewriteXNOR

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2180 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVXNOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::rewriteNAND

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2195 of file bitvector_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::BVNAND, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::rewriteNOR

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2210 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVNOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::rewriteBVCOMP

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2225 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCOMP, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getKind(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::rewriteBVSub

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2240 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), buildPlusTerm(), CVC3::TheoryBitvector::BVSize(), CVC3::BVSUB, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), getPlusTerms(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::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

If k = 2^m, return k*t = t...0

Implements CVC3::BitvectorProofRules.

Definition at line 2269 of file bitvector_theorem_producer.cpp.

References CVC3::abs(), CVC3::Expr::arity(), CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::Expr::getRational(), CVC3::Rational::isInteger(), CVC3::Expr::isRational(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::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 CVC3::BitvectorProofRules.

Definition at line 2317 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVCONST, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::zeroCoeffBVMult

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 3355 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::oneCoeffBVMult

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 3377 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::flipBVMult

(

const Expr &

e

)

[virtual]

t1*a <==> a*t1

Implements CVC3::BitvectorProofRules.

Definition at line 3402 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), 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 3423 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]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3448 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::padBVMult

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3478 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvConstMultAssocRule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3502 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvMultAssocRule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3540 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvMultDistRule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3614 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::flattenBVPlus

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3654 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::combineLikeTermsRule

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 3864 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, collectLikeTermsOfPlus(), createNewPlusCollection(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), sumNormalizedElements(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::lhsMinusRhsRule

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 3915 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::EQ, CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractBVMult

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 4208 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVMultPadExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractBVPlus

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 4240 of file bitvector_theorem_producer.cpp.

References CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVPlusPadExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::iteExtractRule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2590 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::ITE, CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::iteBVnegRule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2626 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::ITE, CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusBVConst

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 4010 of file bitvector_theorem_producer.cpp.

References CVC3::BVCONST, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::TheoryBitvector::computeNegBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::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 CVC3::BitvectorProofRules.

Definition at line 4037 of file bitvector_theorem_producer.cpp.

References CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeNegBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusBVUminus

(

const Expr &

e

)

[virtual]

-(-e) <==> e

Implements CVC3::BitvectorProofRules.

Definition at line 4083 of file bitvector_theorem_producer.cpp.

References CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusVar

(

const Expr &

e

)

[virtual]

-v <==> -1*v

Implements CVC3::BitvectorProofRules.

Definition at line 4104 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvmultBVUminus

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 4127 of file bitvector_theorem_producer.cpp.

References CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeNegBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusToBVPlus

(

const Expr &

e

)

[virtual]

-t <==> ~t+1

generic rule used for bitblasting step. -e <==> ~e+1

Implements CVC3::BitvectorProofRules.

Definition at line 3988 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvuminusBVPlus

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 4173 of file bitvector_theorem_producer.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractConst

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2364 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getBVConstValue(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractWhole

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2396 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractExtract

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2420 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractConcat

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2464 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::EXTRACT, CVC3::Theorem::getExpr(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

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

Definition at line 2531 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVAND, CVC3::BVNEG, CVC3::BVOR, CVC3::BVXNOR, CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::EXTRACT, CVC3::Theory::getEM(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::ExprManager::getKindName(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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

Definition at line 2570 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 2577 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 2584 of file bitvector_theorem_producer.cpp.

References CVC3::BVNEG, and extractBitwise().

Theorem BitvectorTheoremProducer::negConst

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2654 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negConcat

(

const Expr &

e

)

[virtual]

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 2677 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negNeg

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2702 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negElim

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2718 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVNEG, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negBVand

(

const Expr &

e

)

[virtual]

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 2743 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVAND, CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negBVor

(

const Expr &

e

)

[virtual]

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 2765 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVNEG, CVC3::BVOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negBVxor

(

const Expr &

e

)

[virtual]

~(t1 xor t2) = ~t1 xor t2

Implements CVC3::BitvectorProofRules.

Definition at line 2788 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVNEG, CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::negBVxnor

(

const Expr &

e

)

[virtual]

~(t1 xnor t2) = t1 xor t2

Implements CVC3::BitvectorProofRules.

Definition at line 2814 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVNEG, CVC3::BVXNOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitwiseConst	(	const Expr &	e,
		const std::vector< int > &	idxs,
		int	kind
	)			[virtual]

Combine constants in bitwise AND, OR, XOR.

c1 op c2 = c -- bit-wise AND, OR, XOR of constant bitvectors

Implements CVC3::BitvectorProofRules.

Definition at line 2841 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVAND, CVC3::BVCONST, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::RAW_LIST, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitwiseConcat	(	const Expr &	e,
		int	kind
	)			[virtual]

Lifts concatenation above bitwise operators.

Implements CVC3::BitvectorProofRules.

Definition at line 2921 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitwiseFlatten	(	const Expr &	e,
		int	kind
	)			[virtual]

Flatten bitwise operation.

Implements CVC3::BitvectorProofRules.

Definition at line 2969 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CVC3::BVAND, CVC3::BVNEG, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprMap< Data >::erase(), CVC3::Expr::getOpKind(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), sameKidCheck(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitwiseConstElim	(	const Expr &	e,
		int	idx,
		int	kind
	)			[virtual]

Simplify bitwise operator containing a constant child.

Parameters:

	e	is the bit-wise expr
	idx	is the index of the constant bitvector
	kind	is the kind of e

Implements CVC3::BitvectorProofRules.

Definition at line 3067 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVAND, CVC3::BVCONST, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 3194 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by getPlusTerms().

Theorem BitvectorTheoremProducer::concatFlatten

(

const Expr &

e

)

[virtual]

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 3216 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::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].

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

Implements CVC3::BitvectorProofRules.

Definition at line 3238 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvplusConst

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3289 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::begin(), CVC3::BVPLUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Rational::toString(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::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)

c0*c1 = c, multiplication of two BVCONST

Implements CVC3::BitvectorProofRules.

Definition at line 3328 of file bitvector_theorem_producer.cpp.

References CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::typePredBit

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 4276 of file bitvector_theorem_producer.cpp.

References CVC3::BITVECTOR, bvOne(), CVC3::TheoryBitvector::BVSize(), bvZero(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::expandTypePred

(

const Theorem &

tp

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 4293 of file bitvector_theorem_producer.cpp.

References CVC3::andExpr(), bvOne(), CVC3::BVTYPEPRED, bvZero(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Theory::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::TheoryBitvector::getTypePredExpr(), CVC3::TheoryBitvector::getTypePredType(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::NOT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Expr CVC3::BitvectorTheoremProducer::rat

(

const Rational &

r

)

[inline]

Create Expr from Rational (for convenience)

Definition at line 486 of file bitvector_theorem_producer.h.

References CVC3::TheoremProducer::d_em, and CVC3::ExprManager::newRatExpr().

Referenced by bitblastBVMult(), bitblastBVPlus(), bitExtractBitwise(), bitExtractBVASHR(), bitExtractBVLSHR(), bitExtractBVMult(), bitExtractBVPlus(), bitExtractBVPlusPreComputed(), bitExtractBVSHL(), bitExtractConcatenation(), bitExtractConstant(), bitExtractConstBVMult(), bitExtractExtraction(), bitExtractFixedLeftShift(), bitExtractFixedRightShift(), bitExtractNot(), bitExtractSXRule(), bitwiseConcat(), bitwiseConst(), bitwiseConstElim(), computeCarryPreComputed(), constMultToPlus(), 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 if bitPos=0. this function is recursive; if bitPos > 0 then the output expression is

Definition at line 1304 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
	)

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

Definition at line 1405 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), CVC3::TheoryBitvector::d_bvPlusCarryCacheLeftBV, CVC3::TheoryBitvector::d_bvPlusCarryCacheRightBV, d_theoryBitvector, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::ExprMap< Data >::insert(), CVC3::orExpr(), CVC3::Expr::orExpr(), and rat().

Referenced by bitExtractBVPlusPreComputed().

Theorem BitvectorTheoremProducer::isolate_var

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 4370 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::Expr::getOpKind(), CVC3::Expr::isEq(), CVC3::Theory::isLeaf(), CVC3::Theory::isLeafIn(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), and CVC3::Expr::toString().

Theorem BitvectorTheoremProducer::liftConcatBVMult

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 4686 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultPadExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::canonBVMult

(

const Expr &

e

)

[virtual]

canonize BVMult expressions in order to get one coefficient

Implements CVC3::BitvectorProofRules.

Definition at line 4769 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), buildPlusTerm(), CVC3::BVCONST, CVC3::BVMULT, BVMult_order_subterms(), CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, DebugAssert, distributive_rule(), CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), getPlusTerms(), CVC3::Theorem::getRHS(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::liftConcatBVPlus

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 4923 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::canonBVPlus

(

const Expr &

e

)

[virtual]

canonize BVPlus expressions in order to get just one

L:: to store the sum of the coefficients for each var

Implements CVC3::BitvectorProofRules.

Definition at line 5558 of file bitvector_theorem_producer.cpp.

References buildPlusTerm(), CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), getPlusTerms(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::canonBVUMinus

(

const Expr &

e

)

[virtual]

canonize BVMinus expressions: push the minus to the leafs in

Implements CVC3::BitvectorProofRules.

Definition at line 5586 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::processExtract	(	const Theorem &	e,
		bool &	solvedForm
	)			[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 5608 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::EQ, CVC3::Expr::eqExpr(), CVC3::EXISTS, CVC3::EXTRACT, CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::Theory::isLeaf(), CVC3::Theory::isLeafIn(), CVC3::TheoryBitvector::newBitvectorType(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::canonBVEQ	(	const Expr &	e,
		int	maxEffort = 3
	)			[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 5691 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CVC3::BITVECTOR, buildPlusTerm(), CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::EQ, CVC3::Expr::eqExpr(), CVC3::EXTRACT, CVC3::Theory::falseExpr(), FatalAssert, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), getPlusTerms(), CVC3::Theory::isLeaf(), CVC3::Theory::isLeafIn(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::multiplicative_inverse(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVMultPadExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newReflTheorem(), CVC3::TheoremProducer::newRWTheorem(), okToSplit(), CVC3::TheoryBitvector::pad(), CVC3::pow(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::distributive_rule

(

const Expr &

e

)

[virtual]

apply the distributive rule on the BVMULT expression e

Implements CVC3::BitvectorProofRules.

Definition at line 4881 of file bitvector_theorem_producer.cpp.

References CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by canonBVMult().

Theorem BitvectorTheoremProducer::BVMult_order_subterms

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 4618 of file bitvector_theorem_producer.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::count(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::TheoryBitvector::extract_vars(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by canonBVMult().

Theorem BitvectorTheoremProducer::MarkNonSolvableEq

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 4342 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::Expr::isEq(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::reflexivityRule(), and CVC3::Expr::toString().

Theorem BitvectorTheoremProducer::zeroExtendRule

(

const Expr &

e

)

[virtual]

BVZEROEXTEND(e, i) = zeroString @ e.

Implements CVC3::BitvectorProofRules.

Definition at line 6080 of file bitvector_theorem_producer.cpp.

References CVC3::BITVECTOR, CVC3::BVZEROEXTEND, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::repeatRule

(

const Expr &

e

)

[virtual]

BVREPEAT(e, i) = e @ e @ ... @ e.

Implements CVC3::BitvectorProofRules.

Definition at line 6108 of file bitvector_theorem_producer.cpp.

References CVC3::BITVECTOR, CVC3::BVREPEAT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::rotlRule

(

const Expr &

e

)

[virtual]

BVROTL(e, i) = a[n-i-1:0] @ a[n-1:n-i].

Implements CVC3::BitvectorProofRules.

Definition at line 6141 of file bitvector_theorem_producer.cpp.

References CVC3::BITVECTOR, CVC3::BVROTL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::rotrRule

(

const Expr &

e

)

[virtual]

BVROTR(e, i) = a[i-1:0] @ a[n-1:i].

Implements CVC3::BitvectorProofRules.

Definition at line 6172 of file bitvector_theorem_producer.cpp.

References CVC3::BITVECTOR, CVC3::BVROTR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvUDivConst

(

const Expr &

divExpr

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 6242 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::newVar(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvUDivTheorem

(

const Expr &

divExpr

)

[virtual]

Rewrite x/y to s: s = x/y (y 0 x = y * s + m & 0 <= m < y)

Implements CVC3::BitvectorProofRules.

Definition at line 6271 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), CVC3::andExpr(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVUDIV, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::EXISTS, CVC3::Theory::getEM(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::ExprManager::newBoundVarExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvURemConst

(

const Expr &

remExpr

)

[virtual]

Compute the remainder

Implements CVC3::BitvectorProofRules.

Definition at line 6200 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::newVar(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvURemRewrite

(

const Expr &

remExpr

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 6228 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUDivExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

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

References CVC3::Expr::andExpr(), 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::Expr::iffExpr(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), CVC3::Expr::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]

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

Implements CVC3::BitvectorProofRules.

Definition at line 6406 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::bvSDivRewrite

(

const Expr &

sDivExpr

)

[virtual]

Rewrite the signed divide in terms of the unsigned one.

Implements CVC3::BitvectorProofRules.

Definition at line 6461 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), CVC3::BITVECTOR, CVC3::BVSDIV, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVUDivExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvSRemRewrite

(

const Expr &

sRemExpr

)

[virtual]

Rewrite the signed remainder in terms of the unsigned one.

Implements CVC3::BitvectorProofRules.

Definition at line 6517 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVSREM, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVURemExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvSModRewrite

(

const Expr &

sModExpr

)

[virtual]

Rewrite the signed mod in terms of the unsigned one.

Implements CVC3::BitvectorProofRules.

Definition at line 6573 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVSMOD, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVURemExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::zeroBVOR

(

const Expr &

orEqZero

)

[virtual]

Rewrite x_1 x_2 x_n = 0 into x_1 = 0 x_2 = 0 x_n = 0.

Implements CVC3::BitvectorProofRules.

Definition at line 6626 of file bitvector_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVOR, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::isEq(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::oneBVAND

(

const Expr &

andEqOne

)

[virtual]

Rewrite x_1 x_2 x_n = 1^n into x_1 = 1^n x_2 = 1^n x_n = 1^n.

Implements CVC3::BitvectorProofRules.

Definition at line 6648 of file bitvector_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::BVAND, CVC3::BVCONST, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::isEq(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::constEq

(

const Expr &

eq

)

[virtual]

Equalities over constants go to true/false.

Implements CVC3::BitvectorProofRules.

Definition at line 6670 of file bitvector_theorem_producer.cpp.

References CVC3::BVCONST, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Expr::isEq(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 6708 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::EXISTS, CVC3::Theory::getEM(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::iffExpr(), CVC3::TheoryBitvector::newBitvectorType(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), solveExtractOverlapApplies(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

---

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:

• bitvector_theorem_producer.h
• bitvector_theorem_producer.cpp