CVC3::BitvectorTheoremProducer Class Reference

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

#include <bitvector_theorem_producer.h>

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

Collaboration diagram for CVC3::BitvectorTheoremProducer:

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

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

CVC3::BitvectorTheoremProducer::~BitvectorTheoremProducer

(

)

[inline]

Definition at line 90 of file bitvector_theorem_producer.h.

---

Member Function Documentation

const Expr& CVC3::BitvectorTheoremProducer::bvZero

(

)

const [inline, private]

Return cached constant 0bin0.

Definition at line 50 of file bitvector_theorem_producer.h.

References d_bvZero.

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

const Expr& CVC3::BitvectorTheoremProducer::bvOne

(

)

const [inline, private]

Return cached constant 0bin1.

Definition at line 52 of file bitvector_theorem_producer.h.

References d_bvOne.

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

void BitvectorTheoremProducer::collectLikeTermsOfPlus	(	const Expr &	e,
		ExprMap< Rational > &	likeTerms,
		Rational &	plusConstant
	)		[private]

Collect all of: a*x1+b*x1 + c*x2-x2 + d*x3 + ~x3 + ~x4 +e into (a+b, x1) , (c-1 , x2), (d-1, x3), (-1, x4) and the constant e-2. The constant is calculated from the formula -x = ~x+1 (or -x-1=~x).

Definition at line 3723 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::begin(), CVC3::BVCONST, CVC3::BVMULT, CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::clear(), collectOneTermOfPlus(), CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Expr::end(), CVC3::Expr::getOpKind(), and CVC3::Expr::toString().

Referenced by combineLikeTermsRule().

void BitvectorTheoremProducer::collectOneTermOfPlus	(	const Rational &	coefficient,
		const Expr &	var,
		ExprMap< Rational > &	likeTerms,
		Rational &	plusConstant
	)		[private]

Collect a single coefficient*var pair into likeTerms. Update the counter of likeTerms[var] += coefficient. Potentially update the constant additive plusConstant.

Definition at line 3692 of file bitvector_theorem_producer.cpp.

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

Referenced by collectLikeTermsOfPlus().

void BitvectorTheoremProducer::createNewPlusCollection	(	const Expr &	e,
		const ExprMap< Rational > &	likeTerms,
		Rational &	plusConstant,
		std::vector< Expr > &	result
	)		[private]

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

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

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

Referenced by combineLikeTermsRule().

void BitvectorTheoremProducer::getPlusTerms	(	const Expr &	e,
		Rational &	known_term,
		ExprMap< Rational > &	sumHashMap
	)		[private]

Definition at line 5020 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 5298 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 5169 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 5657 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 66 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 104 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(), 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 142 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 225 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(), 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 339 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 305 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 397 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 437 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::notBVEQ1Rule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 606 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), EQ, CVC3::Expr::eqExpr(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), 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 631 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(), 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 658 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 686 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 704 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 762 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 895 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BOOLEXTRACT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Expr::getKind(), 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 927 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 948 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 977 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(), 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 1017 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(), 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 1074 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(), 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 1141 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(), 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 1206 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(), 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 1256 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::bitExtractBVPlusPreComputed	(	const Theorem &	t1_i,
		const Theorem &	t2_i,
		const Expr &	bvPlusTerm,
		int	bitPos,
		int	precomputed
	)		[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 1337 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(), 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 1497 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(), 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 1539 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(), 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 1575 of file bitvector_theorem_producer.cpp.

References 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(), OR, rat(), CVC3::Theorem::toString(), CVC3::Type::toString(), CVC3::Expr::toString(), TRACE, CVC3::TheoremProducer::withProof(), and 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 1619 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(), TRACE, and CVC3::TheoremProducer::withProof().

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

Implements CVC3::BitvectorProofRules.

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 1721 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(), OR, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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

Implements CVC3::BitvectorProofRules.

Definition at line 1775 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(), OR, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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

Implements CVC3::BitvectorProofRules.

Definition at line 1829 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(), 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 1470 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::bitExtractSXRule	(	const Expr &	e,
		int	i
	)		[virtual]

bitExtractSXRule

Implements CVC3::BitvectorProofRules.

Definition at line 380 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 1893 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 1911 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)

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

Implements CVC3::BitvectorProofRules.

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

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

Implements CVC3::BitvectorProofRules.

Definition at line 1968 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 2001 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.

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

Implements CVC3::BitvectorProofRules.

Definition at line 2033 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 2068 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].

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

Implements CVC3::BitvectorProofRules.

Definition at line 2107 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 2135 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 2155 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 2181 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 2196 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 2211 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 2226 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 2241 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

Implements CVC3::BitvectorProofRules.

Definition at line 2270 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 2318 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(), TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::zeroCoeffBVMult

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 3356 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 3378 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 3403 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 3424 of file bitvector_theorem_producer.cpp.

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

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

Theorem BitvectorTheoremProducer::padBVPlus

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3449 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 3479 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 3503 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 3541 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 3615 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 3655 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 3865 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(), TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::lhsMinusRhsRule

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 3916 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(), 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 4209 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 4241 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 2591 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(), 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 2627 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(), 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 4011 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 4038 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 4084 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 4105 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 4128 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 3989 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 4174 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 2365 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 2397 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 2421 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)

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

Implements CVC3::BitvectorProofRules.

Definition at line 2465 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(), 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 2532 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 2571 of file bitvector_theorem_producer.cpp.

References CVC3::BVAND, and extractBitwise().

Theorem BitvectorTheoremProducer::extractOr

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2578 of file bitvector_theorem_producer.cpp.

References CVC3::BVOR, and extractBitwise().

Theorem BitvectorTheoremProducer::extractNeg

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2585 of file bitvector_theorem_producer.cpp.

References CVC3::BVNEG, and extractBitwise().

Theorem BitvectorTheoremProducer::negConst

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2655 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

Implements CVC3::BitvectorProofRules.

Definition at line 2678 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 2703 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 2719 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 2744 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 2766 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 2789 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 2815 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 2842 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(), 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 2922 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 2970 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 3068 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 3160 of file bitvector_theorem_producer.cpp.

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

Referenced by bitwiseFlatten().

Theorem BitvectorTheoremProducer::concatConst

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3195 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.

Implements CVC3::BitvectorProofRules.

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

Implements CVC3::BitvectorProofRules.

Definition at line 3239 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 3290 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(), 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 3329 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 4277 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 4294 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(), 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 1305 of file bitvector_theorem_producer.cpp.

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

Referenced by bitExtractBVPlus().

Expr BitvectorTheoremProducer::computeCarryPreComputed	(	const Theorem &	t1_i,
		const Theorem &	t2_i,
		int	bitPos,
		int	precomputedFlag
	)

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

Definition at line 1406 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 4371 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(), 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 4687 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 4770 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(), TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::liftConcatBVPlus

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 4924 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 5559 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(), 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 5587 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 5609 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, EQ, CVC3::Expr::eqExpr(), 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 5692 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(), 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(), 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 4882 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 4619 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 4343 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), 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 6081 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 6109 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 6142 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 6173 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 6243 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 6272 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(), EXISTS, CVC3::Theory::getEM(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::impExpr(), CVC3::Expr::negate(), 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 6201 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 6229 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 6324 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 6407 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 6462 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 6518 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 6574 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 6631 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 6653 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 6675 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 6691 of file bitvector_theorem_producer.cpp.

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

Referenced by solveExtractOverlap().

Theorem BitvectorTheoremProducer::solveExtractOverlap

(

const Expr &

eq

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 6713 of file bitvector_theorem_producer.cpp.

References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), 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