CVC3::BitvectorProofRules Class Reference

#include <bitvector_proof_rules.h>

Inheritance diagram for CVC3::BitvectorProofRules:

[legend]List of all members.

Public Member Functions

virtual ~BitvectorProofRules ()
virtual Theorem bitvectorFalseRule (const Theorem &thm)=0
virtual Theorem bitvectorTrueRule (const Theorem &thm)=0
virtual Theorem bitBlastEqnRule (const Expr &e, const Expr &f)=0
t1=t2 ==> AND_i(t1[i:i] = t2[i:i])
virtual Theorem bitBlastDisEqnRule (const Theorem &e, const Expr &f)=0
t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i])
virtual Theorem signExtendRule (const Expr &e)=0
sign extend the input SX(e) appropriately
virtual Theorem padBVLTRule (const Expr &e, int len)=0
Pad the kids of BVLT/BVLE to make their length equal.
virtual Theorem padBVSLTRule (const Expr &e, int len)=0
Sign Extend the kids of BVSLT/BVSLE to make their length equal.
virtual Theorem signBVLTRule (const Expr &e, const Theorem &topBit0, const Theorem &topBit1)=0
virtual Theorem notBVLTRule (const Expr &e, int Kind)=0
virtual Theorem lhsEqRhsIneqn (const Expr &e, int kind)=0
if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
virtual Theorem zeroLeq (const Expr &e)=0
virtual Theorem bvConstIneqn (const Expr &e, int kind)=0
virtual Theorem generalIneqn (const Expr &e, const Theorem &e0, const Theorem &e1, int kind)=0
virtual Theorem bitExtractToExtract (const Theorem &thm)=0
t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0
virtual Theorem bitExtractRewrite (const Expr &x)=0
t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])
virtual Theorem bitExtractConstant (const Expr &x, int i)=0
virtual Theorem bitExtractConcatenation (const Expr &x, int i)=0
virtual Theorem bitExtractConstBVMult (const Expr &t, int i)=0
virtual Theorem bitExtractBVMult (const Expr &t, int i)=0
virtual Theorem bitExtractExtraction (const Expr &x, int i)=0
virtual Theorem bitExtractBVPlus (const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i)=0
virtual Theorem bitExtractBVPlusPreComputed (const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed)=0
virtual Theorem bvPlusAssociativityRule (const Expr &bvPlusTerm)=0
virtual Theorem bitExtractNot (const Expr &x, int i)=0
virtual Theorem bitExtractAnd (const Expr &x, int i)=0
virtual Theorem bitExtractOr (const Expr &x, int i)=0
virtual Theorem bitExtractFixedLeftShift (const Expr &x, int i)=0
virtual Theorem bitExtractFixedRightShift (const Expr &x, int i)=0
virtual Theorem zeroPaddingRule (const Expr &e, int r)=0
virtual Theorem bitExtractSXRule (const Expr &e, int i)=0
virtual Theorem eqConst (const Expr &e)=0
c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
virtual Theorem eqToBits (const Theorem &eq)=0
|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
virtual Theorem leftShiftToConcat (const Expr &e)=0
t<<n = c @ 0bin00...00, takes e == (t<<n)
virtual Theorem constWidthLeftShiftToConcat (const Expr &e)=0
t<<n = c @ 0bin00...00, takes e == (t<<n)
virtual Theorem rightShiftToConcat (const Expr &e)=0
t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
virtual Theorem rewriteXOR (const Expr &e)=0
a XOR b <=> (a & ~b) | (~a & b)
virtual Theorem rewriteXNOR (const Expr &e)=0
a XNOR b <=> (~a & ~b) | (a & b)
virtual Theorem rewriteNAND (const Expr &e)=0
a NAND b <=> ~(a & b)
virtual Theorem rewriteNOR (const Expr &e)=0
a NOR b <=> ~(a | b)
virtual Theorem rewriteBVSub (const Expr &e)=0
a - b <=> a + (-b)
virtual Theorem constMultToPlus (const Expr &e)=0
k*t = BVPLUS(n, <sum of shifts of t>) -- translation of k*t to BVPLUS
virtual Theorem bvplusZeroConcatRule (const Expr &e)=0
0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
virtual Theorem zeroCoeffBVMult (const Expr &e)=0
virtual Theorem oneCoeffBVMult (const Expr &e)=0
virtual Theorem flipBVMult (const Expr &e)=0
virtual Theorem padBVPlus (const Expr &e)=0
Make args the same length as the result (zero-extend).
virtual Theorem padBVMult (const Expr &e)=0
Make args the same length as the result (zero-extend).
virtual Theorem bvConstMultAssocRule (const Expr &e)=0
virtual Theorem bvMultAssocRule (const Expr &e)=0
virtual Theorem bvMultDistRule (const Expr &e)=0
virtual Theorem flattenBVPlus (const Expr &e)=0
virtual Theorem combineLikeTermsRule (const Expr &e)=0
virtual Theorem lhsMinusRhsRule (const Expr &e)=0
virtual Theorem extractBVMult (const Expr &e)=0
(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n
virtual Theorem extractBVPlus (const Expr &e)=0
(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n
virtual Theorem iteExtractRule (const Expr &e)=0
ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
virtual Theorem iteBVnegRule (const Expr &e)=0
~ite(c,t1,t2) <=> ite(c,~t1,~t2)
virtual Theorem bvuminusBVConst (const Expr &e)=0
virtual Theorem bvuminusBVMult (const Expr &e)=0
virtual Theorem bvuminusBVUminus (const Expr &e)=0
virtual Theorem bvuminusVar (const Expr &e)=0
virtual Theorem bvmultBVUminus (const Expr &e)=0
virtual Theorem bvuminusToBVPlus (const Expr &e)=0
-t <==> ~t+1
virtual Theorem bvuminusBVPlus (const Expr &e)=0
-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
virtual Theorem extractConst (const Expr &e)=0
c1[i:j] = c (extraction from a constant bitvector)
virtual Theorem extractWhole (const Expr &e)=0
t[n-1:0] = t for n-bit t
virtual Theorem extractExtract (const Expr &e)=0
t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)
virtual Theorem extractConcat (const Expr &e)=0
(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
virtual Theorem extractAnd (const Expr &e)=0
(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)
virtual Theorem extractOr (const Expr &e)=0
(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)
virtual Theorem extractNeg (const Expr &e)=0
(~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
virtual Theorem extractBitwise (const Expr &e, int kind, const std::string &name)=0
Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j].
virtual Theorem negConst (const Expr &e)=0
~c1 = c (bit-wise negation of a constant bitvector)
virtual Theorem negConcat (const Expr &e)=0
~(t1@...@tn) = (~t1)@...@(~tn) -- push negation through concat
virtual Theorem negNeg (const Expr &e)=0
~(~t) = t -- eliminate double negation
virtual Theorem negBVand (const Expr &e)=0
~(t1 & t2) <=> ~t1 | ~t2 -- DeMorgan's Laws
virtual Theorem negBVor (const Expr &e)=0
~(t1 | t2) <=> ~t1 & ~t2 -- DeMorgan's Laws
virtual Theorem negBVxor (const Expr &e)=0
~(t1 xor t2) = ~t1 xor t2
virtual Theorem negBVxnor (const Expr &e)=0
~(t1 xnor t2) = t1 xor t2
virtual Theorem andConst (const Expr &e, const std::vector< int > &idxs)=0
c1&c2&t = c&t -- compute bit-wise AND of constant bitvector arguments
virtual Theorem andZero (const Expr &e, int idx)=0
0bin0...0 & t = 0bin0...0 -- bit-wise AND with zero bitvector
virtual Theorem andOne (const Expr &e, const std::vector< int > idxs)=0
0bin1...1 & t = t -- bit-wise AND with bitvector of 1's
virtual Theorem andConcat (const Expr &e, int idx)=0
... & (t1@...@tk) & ... = (...& t1 &...)@...@(...& tk &...)
virtual Theorem andFlatten (const Expr &e)=0
(t1 & (t2 & t3) & t4) = t1 & t2 & t3 & t4 -- flatten bit-wise AND
virtual Theorem orConst (const Expr &e, const std::vector< int > &idxs)=0
c1|c2|t = c|t -- compute bit-wise OR of constant bitvector arguments
virtual Theorem orOne (const Expr &e, int idx)=0
0bin1...1 | t = 0bin1...1 -- bit-wise OR with bitvector of 1's
virtual Theorem orZero (const Expr &e, const std::vector< int > idxs)=0
0bin0...0 | t = t -- bit-wise OR with bitvector of 0's
virtual Theorem orConcat (const Expr &e, int idx)=0
... | (t1@...@tk) | ... = (...| t1 |...)@...@(...| tk |...)
virtual Theorem orFlatten (const Expr &e)=0
(t1 | (t2 | t3) | t4) = t1 | t2 | t3 | t4 -- flatten bit-wise OR
virtual Theorem concatConst (const Expr &e)=0
c1@c2@...@cn = c (concatenation of constant bitvectors)
virtual Theorem concatFlatten (const Expr &e)=0
Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w.
virtual Theorem concatMergeExtract (const Expr &e)=0
Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0].
virtual Theorem bvplusConst (const Expr &e)=0
BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors).
virtual Theorem bvmultConst (const Expr &e)=0
n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant)
virtual Theorem typePredBit (const Expr &e)=0
|- t=0 OR t=1 for any 1-bit bitvector t
virtual Theorem expandTypePred (const Theorem &tp)=0
Expand the type predicate wrapper (compute the actual type predicate).

Detailed Description

Definition at line 33 of file bitvector_proof_rules.h.

Constructor & Destructor Documentation

virtual CVC3::BitvectorProofRules::~BitvectorProofRules ( ) [inline, virtual]

Definition at line 36 of file bitvector_proof_rules.h.

Member Function Documentation

virtual Theorem CVC3::BitvectorProofRules::bitvectorFalseRule ( const Theorem & thm ) [pure virtual]

Parameters:

thm

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

Returns:: (e1=e2)<=>false

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastEqn().

virtual Theorem CVC3::BitvectorProofRules::bitvectorTrueRule ( const Theorem & thm ) [pure virtual]

Parameters:

thm

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

Returns:: (e1!=e2)<=>true

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastDisEqn().

virtual Theorem CVC3::BitvectorProofRules::bitBlastEqnRule	(	const Expr &	e,
		const Expr &	f
	)			`[pure virtual]`

t1=t2 ==> AND_i(t1[i:i] = t2[i:i])

Parameters:

	e	is a Expr(t1=t2)
	f	is the resulting expression AND_i(t1[i:i] = t2[i:i]) is passed to the rule for efficiency.

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastEqn().

virtual Theorem CVC3::BitvectorProofRules::bitBlastDisEqnRule	(	const Theorem &	e,
		const Expr &	f
	)			`[pure virtual]`

t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i])

Parameters:

	e	is a Theorem(t1/=t2)
	f	is the resulting expression OR_i(NOT t1[i]<=>t2[i]), passed to the rule for efficiency.

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastDisEqn().

virtual Theorem CVC3::BitvectorProofRules::signExtendRule ( const Expr & e ) [pure virtual]

sign extend the input SX(e) appropriately

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV(), and CVC3::TheoryBitvector::signExtendBVLT().

virtual Theorem CVC3::BitvectorProofRules::padBVLTRule	(	const Expr &	e,
		int	len
	)			`[pure virtual]`

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastIneqn(), and CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::padBVSLTRule	(	const Expr &	e,
		int	len
	)			`[pure virtual]`

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::signExtendBVLT().

virtual Theorem CVC3::BitvectorProofRules::signBVLTRule	(	const Expr &	e,
		const Theorem &	topBit0,
		const Theorem &	topBit1
	)			`[pure 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])

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::notBVLTRule	(	const Expr &	e,
		int	Kind
	)			`[pure 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])

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::lhsEqRhsIneqn	(	const Expr &	e,
		int	kind
	)			`[pure virtual]`

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastIneqn(), and CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::zeroLeq ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::bvConstIneqn	(	const Expr &	e,
		int	kind
	)			`[pure virtual]`

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastIneqn(), and CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::generalIneqn	(	const Expr &	e,
		const Theorem &	e0,
		const Theorem &	e1,
		int	kind
	)			`[pure virtual]`

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastIneqn().

virtual Theorem CVC3::BitvectorProofRules::bitExtractToExtract ( const Theorem & thm ) [pure virtual]

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

Parameters:

thm

is a Theorem(t[i]) or Theorem(NOT t[i]), where t[i] is BOOLEXTRACT(t, i).

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bitExtractRewrite ( const Expr & x ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::bitExtractConstant	(	const Expr &	x,
		int	i
	)			`[pure virtual]`

Parameters:

	x	is bitvector constant
	i	is extracted bitposition

Returns:

$\frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{TRUE}}$

, if bitposition has a 1;

$\frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}}$

, if the bitposition has a 0

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryBitvector::rewriteBV(), and CVC3::TheoryBitvector::rewriteConst().

virtual Theorem CVC3::BitvectorProofRules::bitExtractConcatenation	(	const Expr &	x,
		int	i
	)			`[pure virtual]`

Parameters:

	x	is bitvector binary concatenation
	i	is extracted bitposition

Returns:

$\frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]}$

, where

$0 \geq i \geq n-1$

, another case of boolextract over concatenation is:

$\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]}$

, where

$n \geq i \geq m+n-1$

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractConstBVMult	(	const Expr &	t,
		int	i
	)			`[pure virtual]`

Parameters:

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

Returns:: bitblast of BVMULT

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractBVMult	(	const Expr &	t,
		int	i
	)			`[pure virtual]`

Parameters:

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

Returns:: bitblast of BVMULT

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractExtraction	(	const Expr &	x,
		int	i
	)			`[pure virtual]`

Parameters:

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

Returns:

$\frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]}$

, where

$0 \geq j \geq k < n, 0 \geq i < k-j$

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

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

Parameters:

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

Returns:

The base case is:

$\frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]}$

, when

$0 < i \leq n-1$

, we have

$\frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i] \oplus c(t,q,i)}$

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractBVPlusPreComputed	(	const Theorem &	t1_i,
		const Theorem &	t2_i,
		const Expr &	bvPlusTerm,
		int	bitPos,
		int	precomputed
	)			`[pure virtual]`

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvPlusAssociativityRule ( const Expr & bvPlusTerm ) [pure 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.

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractNot	(	const Expr &	x,
		int	i
	)			`[pure virtual]`

Parameters:

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

Returns:

$\frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])}$

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractAnd	(	const Expr &	x,
		int	i
	)			`[pure virtual]`

Parameters:

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

Returns:

$\frac{}{(t_{[n]} \& q_{[n]})[i] \iff (t_{[n]}[i] \wedge q_{[n]}[i])}$

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractOr	(	const Expr &	x,
		int	i
	)			`[pure virtual]`

Parameters:

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

Returns:

$\frac{}{(t_{[n]} \mid q_{[n]})[i] \iff (t_{[n]}[i] \vee q_{[n]}[i])}$

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractFixedLeftShift	(	const Expr &	x,
		int	i
	)			`[pure virtual]`

Parameters:

: input1 is bitvector FIXED SHIFT

$e_{[n]} \ll k$

: input2 is extracted bitposition

Returns:

$\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}}$

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

$\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]}$

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractFixedRightShift	(	const Expr &	x,
		int	i
	)			`[pure virtual]`

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::zeroPaddingRule	(	const Expr &	e,
		int	r
	)			`[pure 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)

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::bitBlastTerm().

virtual Theorem CVC3::BitvectorProofRules::bitExtractSXRule	(	const Expr &	e,
		int	i
	)			`[pure virtual]`

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::eqConst ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryBitvector::rewriteConst(), and CVC3::TheoryBitvector::solve().

virtual Theorem CVC3::BitvectorProofRules::eqToBits ( const Theorem & eq ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::leftShiftToConcat ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV(), and CVC3::TheoryBitvector::simplifyOp().

virtual Theorem CVC3::BitvectorProofRules::constWidthLeftShiftToConcat ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV(), and CVC3::TheoryBitvector::simplifyOp().

virtual Theorem CVC3::BitvectorProofRules::rightShiftToConcat ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV(), and CVC3::TheoryBitvector::simplifyOp().

virtual Theorem CVC3::BitvectorProofRules::rewriteXOR ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::rewriteXNOR ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::rewriteNAND ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::rewriteNOR ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::rewriteBVSub ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::constMultToPlus ( const Expr & e ) [pure 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

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvplusZeroConcatRule ( const Expr & e ) [pure virtual]

0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)

provided that m+ceil(log2(l)) <= n, where k is the size of the 0bin0...0, m is the max. length of each argument, and l is the number of arguments.

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), and CVC3::TheoryBitvector::simplifyOp().

virtual Theorem CVC3::BitvectorProofRules::zeroCoeffBVMult ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith().

virtual Theorem CVC3::BitvectorProofRules::oneCoeffBVMult ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith().

virtual Theorem CVC3::BitvectorProofRules::flipBVMult ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith().

virtual Theorem CVC3::BitvectorProofRules::padBVPlus ( const Expr & e ) [pure virtual]

Make args the same length as the result (zero-extend).

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith(), and CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::padBVMult ( const Expr & e ) [pure virtual]

Make args the same length as the result (zero-extend).

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith().

virtual Theorem CVC3::BitvectorProofRules::bvConstMultAssocRule ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith().

virtual Theorem CVC3::BitvectorProofRules::bvMultAssocRule ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvMultDistRule ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith().

virtual Theorem CVC3::BitvectorProofRules::flattenBVPlus ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::flattenBVPlus().

virtual Theorem CVC3::BitvectorProofRules::combineLikeTermsRule ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith().

virtual Theorem CVC3::BitvectorProofRules::lhsMinusRhsRule ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteBV().

virtual Theorem CVC3::BitvectorProofRules::extractBVMult ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), and CVC3::TheoryBitvector::simplifyOp().

virtual Theorem CVC3::BitvectorProofRules::extractBVPlus ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), and CVC3::TheoryBitvector::simplifyOp().

virtual Theorem CVC3::BitvectorProofRules::iteExtractRule ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::iteBVnegRule ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvuminusBVConst ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvuminusBVMult ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvuminusBVUminus ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvuminusVar ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvmultBVUminus ( const Expr & e ) [pure virtual]

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::bvuminusToBVPlus ( const Expr & e ) [pure virtual]

-t <==> ~t+1

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith().

virtual Theorem CVC3::BitvectorProofRules::bvuminusBVPlus ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::extractConst ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), and CVC3::TheoryBitvector::rewriteConst().

virtual Theorem CVC3::BitvectorProofRules::extractWhole ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::extractExtract ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::extractConcat ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::extractAnd ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::extractOr ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::extractNeg ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::extractBitwise	(	const Expr &	e,
		int	kind,
		const std::string &	name
	)			`[pure virtual]`

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::negConst ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryBitvector::pushNegationRec(), and CVC3::TheoryBitvector::rewriteConst().

virtual Theorem CVC3::BitvectorProofRules::negConcat ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), and CVC3::TheoryBitvector::pushNegationRec().

virtual Theorem CVC3::BitvectorProofRules::negNeg ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), and CVC3::TheoryBitvector::pushNegationRec().

virtual Theorem CVC3::BitvectorProofRules::negBVand ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::pushNegationRec().

virtual Theorem CVC3::BitvectorProofRules::negBVor ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::pushNegationRec().

virtual Theorem CVC3::BitvectorProofRules::negBVxor ( const Expr & e ) [pure virtual]

~(t1 xor t2) = ~t1 xor t2

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::pushNegationRec().

virtual Theorem CVC3::BitvectorProofRules::negBVxnor ( const Expr & e ) [pure virtual]

~(t1 xnor t2) = t1 xor t2

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::pushNegationRec().

virtual Theorem CVC3::BitvectorProofRules::andConst	(	const Expr &	e,
		const std::vector< int > &	idxs
	)			`[pure 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].

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), and CVC3::TheoryBitvector::rewriteConst().

virtual Theorem CVC3::BitvectorProofRules::andZero	(	const Expr &	e,
		int	idx
	)			`[pure 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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::andOne	(	const Expr &	e,
		const std::vector< int >	idxs
	)			`[pure 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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::andConcat	(	const Expr &	e,
		int	idx
	)			`[pure 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.

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::andFlatten ( const Expr & e ) [pure virtual]

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

Also reorders the terms according to a fixed total ordering

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::orConst	(	const Expr &	e,
		const std::vector< int > &	idxs
	)			`[pure 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].

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), and CVC3::TheoryBitvector::rewriteConst().

virtual Theorem CVC3::BitvectorProofRules::orOne	(	const Expr &	e,
		int	idx
	)			`[pure 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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::orZero	(	const Expr &	e,
		const std::vector< int >	idxs
	)			`[pure 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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::orConcat	(	const Expr &	e,
		int	idx
	)			`[pure 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.

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::orFlatten ( const Expr & e ) [pure virtual]

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

Also reorders the terms according to a fixed total ordering

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::concatConst ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat(), and CVC3::TheoryBitvector::rewriteConst().

virtual Theorem CVC3::BitvectorProofRules::concatFlatten ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::concatMergeExtract ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeConcat().

virtual Theorem CVC3::BitvectorProofRules::bvplusConst ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::rewriteConst().

virtual Theorem CVC3::BitvectorProofRules::bvmultConst ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

Referenced by CVC3::TheoryBitvector::normalizeBVArith(), and CVC3::TheoryBitvector::rewriteConst().

virtual Theorem CVC3::BitvectorProofRules::typePredBit ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

virtual Theorem CVC3::BitvectorProofRules::expandTypePred ( const Theorem & tp ) [pure virtual]

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

Implemented in CVC3::BitvectorTheoremProducer.

The documentation for this class was generated from the following file:

bitvector_proof_rules.h

Generated on Tue Jul 3 14:41:38 2007 for CVC3 by

1.5.1