CVC3::BitvectorTheoremProducer Class Reference

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

#include <bitvector_theorem_producer.h>

Inheritance diagram for CVC3::BitvectorTheoremProducer:

[legend]Collaboration diagram for CVC3::BitvectorTheoremProducer:

[legend]List of all members.

Public Member Functions

• BitvectorTheoremProducer (TheoryBitvector *theoryBitvector)

  Constructor: constructs an instance of bitvector DP.
  

• ~BitvectorTheoremProducer ()
• Theorem bitvectorFalseRule (const Theorem &thm)
• Theorem bitvectorTrueRule (const Theorem &thm)
• Theorem bitBlastEqnRule (const Expr &e, const Expr &f)
• Theorem bitBlastDisEqnRule (const Theorem &e, const Expr &f)
• Theorem signExtendRule (const Expr &e)

  sign extend the input SX(e) appropriately
  

• Theorem padBVLTRule (const Expr &e, int len)

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

• Theorem padBVSLTRule (const Expr &e, int len)

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

• Theorem signBVLTRule (const Expr &e, const Theorem &topBit0, const Theorem &topBit1)
• Theorem notBVLTRule (const Expr &e, int Kind)
• 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 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)

  Auxiliary function for bitExtractAnd() and bitExtractOr().
  

• Theorem bitExtractAnd (const Expr &x, int i)
• Theorem bitExtractOr (const Expr &x, int i)
• Theorem bitExtractFixedLeftShift (const Expr &x, int i)
• Theorem bitExtractFixedRightShift (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 rewriteXOR (const Expr &e)

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

• 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 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 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, bool isAnd)

  Auxiliary method for andConst() and orConst().
  

• Theorem bitwiseConcat (const Expr &e, int idx, bool isAnd)

  Auxiliary method for andConcat() and orConcat().
  

• Theorem bitwiseFlatten (const Expr &e, bool isAnd)

  Auxiliary method for andFlatten() and orFlatten().
  

• Theorem andConst (const Expr &e, const std::vector< int > &idxs)

  c1&c2&t = c&t -- compute bit-wise AND of constant bitvector arguments
  

• Theorem andZero (const Expr &e, int idx)

  0bin0...0 & t = 0bin0...0 -- bit-wise AND with zero bitvector
  

• Theorem andOne (const Expr &e, const std::vector< int > idxs)

  0bin1...1 & t = t -- bit-wise AND with bitvector of 1's
  

• Theorem andConcat (const Expr &e, int idx)

  ... & (t1@...@tk) & ... = (...& t1 &...)@...@(...& tk &...)
  

• Theorem andFlatten (const Expr &e)

  (t1 & (t2 & t3) & t4) = t1 & t2 & t3 & t4 -- flatten bit-wise AND
  

• Theorem orConst (const Expr &e, const std::vector< int > &idxs)

  c1|c2|t = c|t -- compute bit-wise OR of constant bitvector arguments
  

• Theorem orOne (const Expr &e, int idx)

  0bin1...1 | t = 0bin1...1 -- bit-wise OR with bitvector of 1's
  

• Theorem orZero (const Expr &e, const std::vector< int > idxs)

  0bin0...0 | t = t -- bit-wise OR with bitvector of 0's
  

• Theorem orConcat (const Expr &e, int idx)

  ... | (t1@...@tk) | ... = (...| t1 |...)@...@(...| tk |...)
  

• Theorem orFlatten (const Expr &e)

  (t1 | (t2 | t3) | t4) = t1 | t2 | t3 | t4 -- flatten bit-wise OR
  

• 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
  

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)

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

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

CVC3::BitvectorTheoremProducer::~BitvectorTheoremProducer

(

)

[inline]

Definition at line 84 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 3462 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(), 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 3432 of file bitvector_theorem_producer.cpp.

References d_theoryBitvector, CVC3::ExprMap< Data >::empty(), CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Theorem::getRHS(), 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 3524 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::Theorem::getRHS(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), 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 3584 of file bitvector_theorem_producer.cpp.

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

Referenced by combineLikeTermsRule().

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

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

Theorem BitvectorTheoremProducer::bitBlastEqnRule	(	const Expr &	e,
		const Expr &	f
	)			[virtual]

Parameters:

	e	input equation: e1=e2 over bitvector terms
	f	formula over the bits of bitvector variables in e:

Returns:

where each of

denotes a formula over variables in

respectively

Implements CVC3::BitvectorProofRules.

Definition at line 130 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::Expr::isAnd(), CVC3::Expr::isEq(), 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 213 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::Expr::isNot(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::Theorem::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::signExtendRule

(

const Expr &

e

)

[virtual]

sign extend the input SX(e) appropriately

Implements CVC3::BitvectorProofRules.

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

Implements CVC3::BitvectorProofRules.

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

Implements CVC3::BitvectorProofRules.

Definition at line 385 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::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])

Implements CVC3::BitvectorProofRules.

Definition at line 425 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::notBVLTRule	(	const Expr &	e,
		int	Kind
	)			[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 595 of file bitvector_theorem_producer.cpp.

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

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

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

Implements CVC3::BitvectorProofRules.

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

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVLE, CHECK_PROOFS, CHECK_SOUND, CVC3::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 671 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 719 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), 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::Theorem::isRewrite(), CVC3::Expr::isTrue(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::notExpr(), CVC3::Expr::orExpr(), CVC3::Theorem::toString(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), 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 860 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 881 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::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 909 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::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::TRACE, CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

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

Parameters:

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

Returns:

, where

, another case of boolextract over concatenation is:

, where

Implements CVC3::BitvectorProofRules.

Definition at line 946 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::Expr::isNull(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractConstBVMult	(	const Expr &	t,
		int	i
	)			[virtual]

Parameters:

	t	: input1 is bitvector binary BVMULT. x[0] must be BVCONST
	i	: input2 is extracted bitposition

Returns:

bitblast of BVMULT

Implements CVC3::BitvectorProofRules.

Definition at line 1000 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::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), pad(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractBVMult	(	const Expr &	t,
		int	i
	)			[virtual]

Parameters:

	t	: input1 is bitvector binary BVMULT. t[0] must not be BVCONST
	i	: input2 is extracted bitposition

Returns:

bitblast of BVMULT

Implements CVC3::BitvectorProofRules.

Definition at line 1066 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::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

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

Parameters:

	x	: input1 is bitvector extraction [k:j]
	i	: input2 is extracted bitposition

Returns:

, where

Implements CVC3::BitvectorProofRules.

Definition at line 1128 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::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bitExtractBVPlus	(	const std::vector< Theorem > &	t1,
		const std::vector< Theorem > &	t2,
		const Expr &	bvPlusTerm,
		int	i
	)			[virtual]

Parameters:

	t1	: input1 is vector of bitblasts of t, from bit i-1 to 0
	t2	: input2 is vector of bitblasts of q, from bit i-1 to 0
	bvPlusTerm	: input3 is BVPLUS term: BVPLUS(n,t,q)
	i	: input4 is extracted bitposition

Returns:

The base case is:

, when

, we have

, where c(t,q,i) is the carry generated by the addition of bits from 0 to i-1

Implements CVC3::BitvectorProofRules.

Definition at line 1179 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::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

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

Implements CVC3::BitvectorProofRules.

Definition at line 1279 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::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Theorem::toString(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvPlusAssociativityRule

(

const Expr &

bvPlusTerm

)

[virtual]

Parameters:

bvPlusTerm

: input1 is bvPlusTerm, a BVPLUS term with arity > 2

Returns:

: output is iff-Theorem: bvPlusTerm <==> outputTerm, where outputTerm is an equivalent BINARY bvplus.

Implements CVC3::BitvectorProofRules.

Definition at line 1439 of file bitvector_theorem_producer.cpp.

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

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

Parameters:

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

Returns:

Implements CVC3::BitvectorProofRules.

Definition at line 1481 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::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

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

Auxiliary function for bitExtractAnd() and bitExtractOr().

Definition at line 1517 of file bitvector_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BITVECTOR, CVC3::BVAND, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), 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::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), rat(), CVC3::Theorem::toString(), CVC3::Type::toString(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Referenced by bitExtractAnd(), and bitExtractOr().

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

Parameters:

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

Returns:

Implements CVC3::BitvectorProofRules.

Definition at line 1561 of file bitvector_theorem_producer.cpp.

References bitExtractBitwise(), and CVC3::BVAND.

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

Parameters:

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

Returns:

Implements CVC3::BitvectorProofRules.

Definition at line 1567 of file bitvector_theorem_producer.cpp.

References bitExtractBitwise(), and CVC3::BVOR.

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 1572 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::LEFTSHIFT, CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

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

Implements CVC3::BitvectorProofRules.

Definition at line 1621 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::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::RIGHTSHIFT, CVC3::Expr::toString(), CVC3::TRACE, 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 1412 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::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 368 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 1680 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 1698 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::leftShiftToConcat

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 1731 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::constWidthLeftShiftToConcat

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

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

Implements CVC3::BitvectorProofRules.

Definition at line 1787 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::rewriteXOR

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 1819 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::rewriteXNOR

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 1838 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::newBVAndExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVOrExpr(), 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 1857 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 1872 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::rewriteBVSub

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 1887 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::TheoryBitvector::BVSize(), CVC3::BVSUB, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), 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 1910 of file bitvector_theorem_producer.cpp.

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

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

Theorem BitvectorTheoremProducer::zeroCoeffBVMult

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 3096 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 3118 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 3143 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

Parameters:

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

Definition at line 3164 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::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), and CVC3::Expr::toString().

Referenced by bitExtractConstBVMult(), 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 3189 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 3219 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 3243 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 3281 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 3355 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 3395 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 3604 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::lhsMinusRhsRule

(

const Expr &

e

)

[virtual]

Implements CVC3::BitvectorProofRules.

Definition at line 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::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 3948 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::newBVMultExpr(), 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 3980 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::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), 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 2231 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::iteBVnegRule

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2267 of file bitvector_theorem_producer.cpp.

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

Theorem BitvectorTheoremProducer::bvuminusBVConst

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 3750 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 3777 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 3823 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 3844 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 3867 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

Implements CVC3::BitvectorProofRules.

Definition at line 3728 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 3913 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 2005 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 2037 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::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 2061 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::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractConcat

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2105 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::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::extractBitwise	(	const Expr &	e,
		int	kind,
		const std::string &	name
	)			[virtual]

Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j].

Implements CVC3::BitvectorProofRules.

Definition at line 2172 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 2211 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 2218 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 2225 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 2295 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 2318 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), 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 2343 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::negBVand

(

const Expr &

e

)

[virtual]

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

Implements CVC3::BitvectorProofRules.

Definition at line 2359 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::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

Implements CVC3::BitvectorProofRules.

Definition at line 2381 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::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 2404 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 2430 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,
		bool	isAnd
	)

Auxiliary method for andConst() and orConst().

c1&c2 = c (bit-wise AND constant bitvectors) c1 op c2 = c -- bit-wise AND and OR of constant bitvectors

Definition at line 2458 of file bitvector_theorem_producer.cpp.

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

Referenced by andConst(), and orConst().

Theorem BitvectorTheoremProducer::bitwiseConcat	(	const Expr &	e,
		int	idx,
		bool	isAnd
	)

Auxiliary method for andConcat() and orConcat().

Lifts concatenation to the top of bit-wise AND. Takes the bit-wise AND expression 'e' and the index 'i' of the concatenation.

Definition at line 2539 of file bitvector_theorem_producer.cpp.

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

Referenced by andConcat(), and orConcat().

Theorem BitvectorTheoremProducer::bitwiseFlatten	(	const Expr &	e,
		bool	isAnd
	)

Auxiliary method for andFlatten() and orFlatten().

Definition at line 2590 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVAND, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), sameKidCheck(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by andFlatten(), and orFlatten().

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

c1&c2&t = c&t -- compute bit-wise AND of constant bitvector arguments

Parameters:

	e	is the bit-wise AND expression;
	idxs	are the indices of the constant bitvectors. There must be at least constant expressions in this rule.

Returns:

Theorem(e==e'), where e' is either a constant bitvector, or is a bit-wise AND with a single constant bitvector in e'[0].

Implements CVC3::BitvectorProofRules.

Definition at line 2666 of file bitvector_theorem_producer.cpp.

References bitwiseConst().

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

0bin0...0 & t = 0bin0...0 -- bit-wise AND with zero bitvector

Parameters:

	e	is the bit-wise AND expr
	idx	is the index of the zero bitvector

Implements CVC3::BitvectorProofRules.

Definition at line 2676 of file bitvector_theorem_producer.cpp.

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

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

0bin1...1 & t = t -- bit-wise AND with bitvector of 1's

Parameters:

	e	is the bit-wise AND expr
	idxs	is a vector of indices of the bitvectors of 1's which will be dropped

Implements CVC3::BitvectorProofRules.

Definition at line 2698 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVAND, CVC3::BVCONST, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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

... & (t1@...@tk) & ... = (...& t1 &...)@...@(...& tk &...)

Lifts concatenation to the top of bit-wise AND. Takes the bit-wise AND expression 'e' and the index 'i' of the concatenation.

Implements CVC3::BitvectorProofRules.

Definition at line 2755 of file bitvector_theorem_producer.cpp.

References bitwiseConcat().

Theorem BitvectorTheoremProducer::andFlatten

(

const Expr &

e

)

[virtual]

(t1 & (t2 & t3) & t4) = t1 & t2 & t3 & t4 -- flatten bit-wise AND

Also reorders the terms according to a fixed total ordering

Implements CVC3::BitvectorProofRules.

Definition at line 2763 of file bitvector_theorem_producer.cpp.

References bitwiseFlatten().

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

c1|c2|t = c|t -- compute bit-wise OR of constant bitvector arguments

Parameters:

	e	is the bit-wise OR expression;
	idxs	are the indices of the constant bitvectors. There must be at least constant expressions in this rule.

Returns:

Theorem(e==e'), where e' is either a constant bitvector, or is a bit-wise OR with a single constant bitvector in e'[0].

Implements CVC3::BitvectorProofRules.

Definition at line 2770 of file bitvector_theorem_producer.cpp.

References bitwiseConst().

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

0bin1...1 | t = 0bin1...1 -- bit-wise OR with bitvector of 1's

Parameters:

	e	is the bit-wise OR expr
	idx	is the index of the bitvector of 1's

Implements CVC3::BitvectorProofRules.

Definition at line 2781 of file bitvector_theorem_producer.cpp.

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

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

0bin0...0 | t = t -- bit-wise OR with bitvector of 0's

Parameters:

	e	is the bit-wise OR expr
	idxs	is a vector of indices of the bitvectors of 0's which will be dropped

Implements CVC3::BitvectorProofRules.

Definition at line 2811 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVOR, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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

... | (t1@...@tk) | ... = (...| t1 |...)@...@(...| tk |...)

Lifts concatenation to the top of bit-wise OR. Takes the bit-wise OR expression 'e' and the index 'i' of the concatenation.

Implements CVC3::BitvectorProofRules.

Definition at line 2920 of file bitvector_theorem_producer.cpp.

References bitwiseConcat().

Theorem BitvectorTheoremProducer::orFlatten

(

const Expr &

e

)

[virtual]

(t1 | (t2 | t3) | t4) = t1 | t2 | t3 | t4 -- flatten bit-wise OR

Also reorders the terms according to a fixed total ordering

Implements CVC3::BitvectorProofRules.

Definition at line 2928 of file bitvector_theorem_producer.cpp.

References bitwiseFlatten().

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

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 2957 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 2979 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::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 3030 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::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem BitvectorTheoremProducer::bvmultConst

(

const Expr &

e

)

[virtual]

n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant)

Implements CVC3::BitvectorProofRules.

Definition at line 3069 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 4016 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(), 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 4033 of file bitvector_theorem_producer.cpp.

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

Expr CVC3::BitvectorTheoremProducer::rat

(

const Rational &

r

)

[inline]

Create Expr from Rational (for convenience)

Definition at line 512 of file bitvector_theorem_producer.h.

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

Referenced by andOne(), andZero(), bitExtractBitwise(), bitExtractBVMult(), bitExtractBVPlus(), bitExtractBVPlusPreComputed(), bitExtractConcatenation(), bitExtractConstant(), bitExtractConstBVMult(), bitExtractExtraction(), bitExtractFixedLeftShift(), bitExtractFixedRightShift(), bitExtractNot(), bitExtractSXRule(), bitwiseConcat(), bitwiseConst(), computeCarryPreComputed(), constMultToPlus(), orOne(), orZero(), 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 1247 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 1348 of file bitvector_theorem_producer.cpp.

References CVC3::Expr::andExpr(), CVC3::TheoryBitvector::d_bvPlusCarryCacheLeftBV, CVC3::TheoryBitvector::d_bvPlusCarryCacheRightBV, d_theoryBitvector, DebugAssert, CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::orExpr(), CVC3::Expr::orExpr(), and rat().

Referenced by bitExtractBVPlusPreComputed().

---

Member Data Documentation

TheoryBitvector* CVC3::BitvectorTheoremProducer::d_theoryBitvector [private]

Definition at line 44 of file bitvector_theorem_producer.h.

Referenced by andOne(), andZero(), bitBlastDisEqnRule(), bitBlastEqnRule(), bitExtractBitwise(), bitExtractBVMult(), bitExtractBVPlus(), bitExtractBVPlusPreComputed(), bitExtractConcatenation(), bitExtractConstant(), bitExtractConstBVMult(), bitExtractExtraction(), bitExtractFixedLeftShift(), bitExtractFixedRightShift(), bitExtractNot(), bitExtractRewrite(), bitExtractSXRule(), bitExtractToExtract(), bitvectorFalseRule(), BitvectorTheoremProducer(), bitvectorTrueRule(), bitwiseConcat(), bitwiseConst(), bitwiseFlatten(), bvConstIneqn(), bvConstMultAssocRule(), bvMultAssocRule(), bvmultBVUminus(), bvmultConst(), bvMultDistRule(), bvPlusAssociativityRule(), bvplusConst(), bvplusZeroConcatRule(), bvuminusBVConst(), bvuminusBVMult(), bvuminusToBVPlus(), bvuminusVar(), collectLikeTermsOfPlus(), collectOneTermOfPlus(), combineLikeTermsRule(), computeCarryPreComputed(), concatConst(), concatMergeExtract(), constMultToPlus(), constWidthLeftShiftToConcat(), createNewPlusCollection(), eqConst(), eqToBits(), expandTypePred(), extractBitwise(), extractBVMult(), extractBVPlus(), extractConcat(), extractConst(), extractExtract(), extractWhole(), flattenBVPlus(), flipBVMult(), generalIneqn(), iteBVnegRule(), iteExtractRule(), leftShiftToConcat(), lhsEqRhsIneqn(), lhsMinusRhsRule(), negBVand(), negBVor(), negBVxnor(), negBVxor(), negConcat(), negConst(), notBVLTRule(), oneCoeffBVMult(), orOne(), orZero(), pad(), padBVLTRule(), padBVMult(), padBVPlus(), padBVSLTRule(), rewriteBVSub(), rewriteNAND(), rewriteNOR(), rewriteXNOR(), rewriteXOR(), rightShiftToConcat(), sameKidCheck(), signBVLTRule(), signExtendRule(), sumNormalizedElements(), typePredBit(), zeroCoeffBVMult(), 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

---