CVC3
2.4.1
|
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>
Public Member Functions | |
BitvectorTheoremProducer (TheoryBitvector *theoryBitvector) | |
Constructor: constructs an instance of bitvector DP. More... | |
~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 More... | |
Theorem | padBVLTRule (const Expr &e, int len) |
Pad the kids of BVLT/BVLE to make their length equal. More... | |
Theorem | padBVSLTRule (const Expr &e, int len) |
Sign Extend the kids of BVSLT/BVSLE to make their length equal. More... | |
Theorem | signBVLTRule (const Expr &e, const Theorem &topBit0, const Theorem &topBit1) |
Theorem | notBVEQ1Rule (const Expr &e) |
Theorem | notBVLTRule (const Expr &e) |
Theorem | lhsEqRhsIneqn (const Expr &e, int kind) |
if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true) More... | |
Theorem | zeroLeq (const Expr &e) |
|= 0 <= foo <-> TRUE More... | |
Theorem | bvConstIneqn (const Expr &e, int kind) |
if indeed e[0] < e[1] then (e<==>true) else (e<==>false) More... | |
Theorem | generalIneqn (const Expr &e, const Theorem &lhs_i, const Theorem &rhs_i, int kind) |
Theorem | bitExtractAllToConstEq (std::vector< Theorem > &thms) |
Theorem | bitExtractToExtract (const Theorem &thm) |
t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0 More... | |
Theorem | bitExtractRewrite (const Expr &x) |
t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i]) More... | |
Theorem | bitExtractConstant (const Expr &x, int i) |
Theorem | bitExtractConcatenation (const Expr &x, int i) |
Theorem | bitExtractConstBVMult (const Expr &t, int i) |
Theorem | bitExtractBVMult (const Expr &t, int i) |
Theorem | bitExtractExtraction (const Expr &x, int i) |
Theorem | bitExtractBVPlus (const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i) |
Theorem | bitExtractBVPlusPreComputed (const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed) |
Theorem | bvPlusAssociativityRule (const Expr &bvPlusTerm) |
Theorem | bitExtractNot (const Expr &x, int i) |
Theorem | bitExtractBitwise (const Expr &x, int i, int kind) |
Extract from bitwise AND, OR, or XOR. More... | |
Theorem | bitExtractFixedLeftShift (const Expr &x, int i) |
Theorem | bitExtractFixedRightShift (const Expr &x, int i) |
Theorem | bitExtractBVSHL (const Expr &x, int i) |
Theorem | bitExtractBVLSHR (const Expr &x, int i) |
Theorem | bitExtractBVASHR (const Expr &x, int i) |
Theorem | zeroPaddingRule (const Expr &e, int r) |
Theorem | bitExtractSXRule (const Expr &e, int i) |
bitExtractSXRule More... | |
Theorem | eqConst (const Expr &e) |
c1=c2 <=> TRUE/FALSE (equality of constant bitvectors) More... | |
Theorem | eqToBits (const Theorem &eq) |
|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits More... | |
Theorem | leftShiftToConcat (const Expr &e) |
t<<n = c @ 0bin00...00, takes e == (t<<n) More... | |
Theorem | constWidthLeftShiftToConcat (const Expr &e) |
t<<n = c @ 0bin00...00, takes e == (t<<n) More... | |
Theorem | rightShiftToConcat (const Expr &e) |
t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n) More... | |
Theorem | bvshlToConcat (const Expr &e) |
BVSHL(t,c) = t[n-c,0] @ 0bin00...00. More... | |
Theorem | bvshlSplit (const Expr &e) |
BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ... More... | |
Theorem | bvlshrToConcat (const Expr &e) |
BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]. More... | |
Theorem | bvShiftZero (const Expr &e) |
All shifts over a 0 constant = 0. More... | |
Theorem | bvashrToConcat (const Expr &e) |
BVASHR(t,c) = SX(t[n-1,c], n-1) More... | |
Theorem | rewriteXNOR (const Expr &e) |
a XNOR b <=> (~a & ~b) | (a & b) More... | |
Theorem | rewriteNAND (const Expr &e) |
a NAND b <=> ~(a & b) More... | |
Theorem | rewriteNOR (const Expr &e) |
a NOR b <=> ~(a | b) More... | |
Theorem | rewriteBVCOMP (const Expr &e) |
BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0) More... | |
Theorem | rewriteBVSub (const Expr &e) |
a - b <=> a + (-b) More... | |
Theorem | constMultToPlus (const Expr &e) |
k*t = BVPLUS(n, <sum of shifts of t>) – translation of k*t to BVPLUS More... | |
Theorem | bvplusZeroConcatRule (const Expr &e) |
0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args) More... | |
Theorem | zeroCoeffBVMult (const Expr &e) |
Theorem | oneCoeffBVMult (const Expr &e) |
Theorem | flipBVMult (const Expr &e) |
t1*a <==> a*t1 More... | |
Expr | pad (int rat, const Expr &e) |
converts e to a bitvector of length rat More... | |
Theorem | padBVPlus (const Expr &e) |
Pad the kids of BVMULT to make their bvLength = # of output-bits. More... | |
Theorem | padBVMult (const Expr &e) |
Pad the kids of BVMULT to make their bvLength = # of output-bits. More... | |
Theorem | bvConstMultAssocRule (const Expr &e) |
a*(b*t) <==> (a*b)*t, where a,b,t have same bvLength More... | |
Theorem | bvMultAssocRule (const Expr &e) |
(t1*t2)*t3 <==> t1*(t2*t3), where t1<t2<t3 More... | |
Theorem | bvMultDistRule (const Expr &e) |
a*(t1+...+tn) <==> (a*t1+...+a*tn), where all kids are equibvLength More... | |
Theorem | flattenBVPlus (const Expr &e) |
input BVPLUS expression e.output e <==> e', where e' has no BVPLUS More... | |
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 More... | |
Theorem | extractBVPlus (const Expr &e) |
(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n More... | |
Theorem | iteExtractRule (const Expr &e) |
ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j]) More... | |
Theorem | iteBVnegRule (const Expr &e) |
~ite(c,t1,t2) <=> ite(c,~t1,~t2) More... | |
Theorem | bvuminusBVConst (const Expr &e) |
-0 <==> 0, -c <==> ~c+1 More... | |
Theorem | bvuminusBVMult (const Expr &e) |
-(c*t)<=>(-c)*t; if -c==0 return e<=>0. if(-c==1) return e<=>t More... | |
Theorem | bvuminusBVUminus (const Expr &e) |
-(-e) <==> e More... | |
Theorem | bvuminusVar (const Expr &e) |
-v <==> -1*v More... | |
Theorem | bvmultBVUminus (const Expr &e) |
c*(-t) <==> (-c)*t More... | |
Theorem | bvuminusToBVPlus (const Expr &e) |
-t <==> ~t+1 More... | |
Theorem | bvuminusBVPlus (const Expr &e) |
-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn)) More... | |
Theorem | extractConst (const Expr &e) |
c1[i:j] = c (extraction from a constant bitvector) More... | |
Theorem | extractWhole (const Expr &e) |
t[n-1:0] = t for n-bit t More... | |
Theorem | extractExtract (const Expr &e) |
t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction) More... | |
Theorem | extractConcat (const Expr &e) |
(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat) More... | |
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]. More... | |
Theorem | extractAnd (const Expr &e) |
(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR) More... | |
Theorem | extractOr (const Expr &e) |
(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND) More... | |
Theorem | extractNeg (const Expr &e) |
(~t)[i:j] = ~(t[i:j]) (push extraction through NEG) More... | |
Theorem | negConst (const Expr &e) |
~c1 = c (bit-wise negation of a constant bitvector) More... | |
Theorem | negConcat (const Expr &e) |
~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat More... | |
Theorem | negNeg (const Expr &e) |
~(~t) = t – eliminate double negation More... | |
Theorem | negElim (const Expr &e) |
~t = -1*t + 1 – eliminate negation More... | |
Theorem | negBVand (const Expr &e) |
~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws More... | |
Theorem | negBVor (const Expr &e) |
~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws More... | |
Theorem | negBVxor (const Expr &e) |
~(t1 xor t2) = ~t1 xor t2 More... | |
Theorem | negBVxnor (const Expr &e) |
~(t1 xnor t2) = t1 xor t2 More... | |
Theorem | bitwiseConst (const Expr &e, const std::vector< int > &idxs, int kind) |
Combine constants in bitwise AND, OR, XOR. More... | |
Theorem | bitwiseConcat (const Expr &e, int kind) |
Lifts concatenation above bitwise operators. More... | |
Theorem | bitwiseFlatten (const Expr &e, int kind) |
Flatten bitwise operation. More... | |
Theorem | bitwiseConstElim (const Expr &e, int idx, int kind) |
Simplify bitwise operator containing a constant child. More... | |
int | sameKidCheck (const Expr &e, ExprMap< int > &likeTerms) |
Theorem | concatConst (const Expr &e) |
c1@c2@...@cn = c (concatenation of constant bitvectors) More... | |
Theorem | concatFlatten (const Expr &e) |
Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w. More... | |
Theorem | concatMergeExtract (const Expr &e) |
Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0]. More... | |
Theorem | bvplusConst (const Expr &e) |
BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors) More... | |
Theorem | bvmultConst (const Expr &e) |
n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant) More... | |
Theorem | typePredBit (const Expr &e) |
|- t=0 OR t=1 for any 1-bit bitvector t More... | |
Theorem | expandTypePred (const Theorem &tp) |
Expand the type predicate wrapper (compute the actual type predicate) More... | |
Expr | rat (const Rational &r) |
Create Expr from Rational (for convenience) More... | |
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 More... | |
virtual Theorem | isolate_var (const Expr &e) |
isolate a variable with coefficient = 1 on the Lhs of an More... | |
virtual Theorem | liftConcatBVMult (const Expr &e) |
virtual Theorem | canonBVMult (const Expr &e) |
canonize BVMult expressions in order to get one coefficient More... | |
virtual Theorem | liftConcatBVPlus (const Expr &e) |
virtual Theorem | canonBVPlus (const Expr &e) |
canonize BVPlus expressions in order to get just one More... | |
virtual Theorem | canonBVUMinus (const Expr &e) |
canonize BVMinus expressions: push the minus to the leafs in More... | |
virtual Theorem | processExtract (const Theorem &e, bool &solvedForm) |
virtual Theorem | canonBVEQ (const Expr &e, int maxEffort=3) |
virtual Theorem | distributive_rule (const Expr &e) |
apply the distributive rule on the BVMULT expression e More... | |
virtual Theorem | BVMult_order_subterms (const Expr &e) |
virtual Theorem | MarkNonSolvableEq (const Expr &e) |
virtual Theorem | zeroExtendRule (const Expr &e) |
BVZEROEXTEND(e, i) = zeroString @ e. More... | |
virtual Theorem | repeatRule (const Expr &e) |
BVREPEAT(e, i) = e @ e @ ... @ e. More... | |
virtual Theorem | rotlRule (const Expr &e) |
BVROTL(e, i) = a[n-i-1:0] @ a[n-1:n-i]. More... | |
virtual Theorem | rotrRule (const Expr &e) |
BVROTR(e, i) = a[i-1:0] @ a[n-1:i]. More... | |
virtual Theorem | bvUDivConst (const Expr &divExpr) |
virtual Theorem | bvUDivTheorem (const Expr &divExpr) |
virtual Theorem | bvURemConst (const Expr &remExpr) |
virtual Theorem | bvURemRewrite (const Expr &remExpr) |
virtual Theorem | bitblastBVMult (const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_times_b, std::vector< Theorem > &output_bits) |
virtual Theorem | bitblastBVPlus (const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_plus_b, std::vector< Theorem > &output_bits) |
virtual Theorem | bvSDivRewrite (const Expr &sDivExpr) |
virtual Theorem | bvSRemRewrite (const Expr &sRemExpr) |
virtual Theorem | bvSModRewrite (const Expr &sModExpr) |
virtual Theorem | zeroBVOR (const Expr &orEqZero) |
virtual Theorem | oneBVAND (const Expr &andEqOne) |
virtual Theorem | constEq (const Expr &eq) |
bool | solveExtractOverlapApplies (const Expr &eq) |
Theorem | solveExtractOverlap (const Expr &eq) |
![]() | |
virtual | ~BitvectorProofRules () |
![]() | |
TheoremProducer (TheoremManager *tm) | |
virtual | ~TheoremProducer () |
bool | withProof () |
Testing whether to generate proofs. More... | |
bool | withAssumptions () |
Testing whether to generate assumptions. More... | |
Proof | newLabel (const Expr &e) |
Create a new proof label (bound variable) for an assumption (formula) More... | |
Proof | newPf (const std::string &name) |
Proof | newPf (const std::string &name, const Expr &e) |
Proof | newPf (const std::string &name, const Proof &pf) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2) |
Proof | newPf (const std::string &name, const Expr &e, const Proof &pf) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf) |
Proof | newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end) |
Proof | newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end) |
Proof | newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const std::vector< Expr > &args) |
Proof | newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args) |
Proof | newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf) |
Proof | newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs) |
Proof | newPf (const Proof &label, const Expr &frm, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label formula proof) More... | |
Proof | newPf (const Proof &label, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label proof). More... | |
Proof | newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf) |
Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf) More... | |
Proof | newPf (const std::vector< Proof > &labels, const Proof &pf) |
Private Member Functions | |
const Expr & | bvZero () const |
Return cached constant 0bin0. More... | |
const Expr & | bvOne () const |
Return cached constant 0bin1. More... | |
void | collectLikeTermsOfPlus (const Expr &e, ExprMap< Rational > &likeTerms, Rational &plusConstant) |
void | collectOneTermOfPlus (const Rational &coefficient, const Expr &var, ExprMap< Rational > &likeTerms, Rational &plusConstant) |
void | createNewPlusCollection (const Expr &e, const ExprMap< Rational > &likeTerms, Rational &plusConstant, std::vector< Expr > &result) |
Expr | sumNormalizedElements (int bvplusLength, const std::vector< Expr > &elements) |
void | getPlusTerms (const Expr &e, Rational &known_term, ExprMap< Rational > &sumHashMap) |
Expr | buildPlusTerm (int bv_size, Rational &known_term, ExprMap< Rational > &sumHashMap) |
Expr | chopConcat (int bv_size, Rational c, std::vector< Expr > &concatKids) |
bool | okToSplit (const Expr &e) |
Private Attributes | |
TheoryBitvector * | d_theoryBitvector |
Expr | d_bvZero |
Constant 1-bit bit-vector 0bin0. More... | |
Expr | d_bvOne |
Constant 1-bit bit-vector 0bin1. More... | |
Additional Inherited Members | |
![]() | |
Theorem | newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf) |
Create a new theorem. See also newRWTheorem() and newReflTheorem() More... | |
Theorem | newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
Create a rewrite theorem: lhs = rhs. More... | |
Theorem | newReflTheorem (const Expr &e) |
Create a reflexivity theorem. More... | |
Theorem | newAssumption (const Expr &thm, const Proof &pf, int scope=-1) |
Theorem3 | newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf) |
Theorem3 | newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
void | soundError (const std::string &file, int line, const std::string &cond, const std::string &msg) |
![]() | |
TheoremManager * | d_tm |
ExprManager * | d_em |
const bool * | d_checkProofs |
Op | d_pfOp |
Expr | d_hole |
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.
BitvectorTheoremProducer::BitvectorTheoremProducer | ( | TheoryBitvector * | theoryBitvector) |
Constructor: constructs an instance of bitvector DP.
Definition at line 50 of file bitvector_theorem_producer.cpp.
References d_bvOne, d_bvZero, d_theoryBitvector, and CVC3::TheoryBitvector::newBVConstExpr().
|
inline |
Definition at line 90 of file bitvector_theorem_producer.h.
|
inlineprivate |
Return cached constant 0bin0.
Definition at line 50 of file bitvector_theorem_producer.h.
References d_bvZero.
Referenced by bitExtractToExtract(), expandTypePred(), signBVLTRule(), and typePredBit().
|
inlineprivate |
Return cached constant 0bin1.
Definition at line 52 of file bitvector_theorem_producer.h.
References d_bvOne.
Referenced by bitExtractToExtract(), expandTypePred(), signBVLTRule(), and typePredBit().
|
private |
Collect all of: a*x1+b*x1 + c*x2-x2 + d*x3 + ~x3 + ~x4 +e into (a+b, x1) , (c-1 , x2), (d-1, x3), (-1, x4) and the constant e-2. The constant is calculated from the formula -x = ~x+1 (or -x-1=~x).
Definition at line 3723 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::begin(), CVC3::BVCONST, CVC3::BVMULT, CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::clear(), collectOneTermOfPlus(), CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Expr::end(), CVC3::Expr::getOpKind(), and CVC3::Expr::toString().
Referenced by combineLikeTermsRule().
|
private |
Collect a single coefficient*var pair into likeTerms. Update the counter of likeTerms[var] += coefficient. Potentially update the constant additive plusConstant.
Definition at line 3692 of file bitvector_theorem_producer.cpp.
References d_theoryBitvector, CVC3::ExprMap< Data >::empty(), CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Theorem::getRHS(), CVC3::TheoryBitvector::newBVNegExpr(), and CVC3::TheoryBitvector::pushNegationRec().
Referenced by collectLikeTermsOfPlus().
|
private |
Create a vector which will form the next PVPLUS. Use the colleciton of likeTerms, and the constant additive plusConstant
Definition at line 3785 of file bitvector_theorem_producer.cpp.
References CVC3::ExprMap< Data >::begin(), CVC3::BITVECTOR, boundedModulo(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::ExprMap< Data >::end(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::pushNegationRec(), and CVC3::Expr::toString().
Referenced by combineLikeTermsRule().
|
private |
Create expression by applying plus to all elements. All elements should be normalized and ready. If there are too few elements, a non BVPLUS expression will be created.
Definition at line 3845 of file bitvector_theorem_producer.cpp.
References d_theoryBitvector, CVC3::TheoryBitvector::newBVPlusExpr(), and CVC3::TheoryBitvector::newBVZeroString().
Referenced by combineLikeTermsRule().
|
private |
Definition at line 5020 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::BVNEG, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, concatConst(), d_theoryBitvector, DebugAssert, CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), and CVC3::pow().
Referenced by canonBVEQ(), canonBVMult(), canonBVPlus(), chopConcat(), and rewriteBVSub().
|
private |
Definition at line 5298 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::BVCONST, CVC3::BVNEG, CVC3::TheoryBitvector::BVSize(), chopConcat(), CVC3::CONCAT, d_theoryBitvector, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVMultPadExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), and CVC3::pow().
Referenced by canonBVEQ(), canonBVMult(), canonBVPlus(), chopConcat(), and rewriteBVSub().
|
private |
Definition at line 5169 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), buildPlusTerm(), CVC3::BVCONST, CVC3::TheoryBitvector::BVSize(), CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, d_theoryBitvector, DebugAssert, CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), getPlusTerms(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), and CVC3::pow().
Referenced by buildPlusTerm().
|
private |
Definition at line 5657 of file bitvector_theorem_producer.cpp.
References CVC3::BVAND, CVC3::BVASHR, CVC3::BVCONST, CVC3::BVLSHR, CVC3::BVMULT, CVC3::BVNEG, CVC3::BVOR, CVC3::BVPLUS, CVC3::BVSDIV, CVC3::BVSHL, CVC3::BVSMOD, CVC3::BVSREM, CVC3::BVUDIV, CVC3::BVUREM, CVC3::BVXOR, d_theoryBitvector, CVC3::EXTRACT, FatalAssert, CVC3::Expr::getOpKind(), and CVC3::Theory::isLeaf().
Referenced by canonBVEQ().
thm | input theorem: (e1[i]<=>e2[i])<=>false |
Implements CVC3::BitvectorProofRules.
Definition at line 66 of file bitvector_theorem_producer.cpp.
References CVC3::BOOLEXTRACT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
thm | input theorem: (~e1[i]<=>e2[i])<=>true |
Implements CVC3::BitvectorProofRules.
Definition at line 104 of file bitvector_theorem_producer.cpp.
References CVC3::BOOLEXTRACT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isIff(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), NOT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
e | input equation: e1=e2 over bitvector terms |
f | formula over the bits of bitvector variables in e: |
Implements CVC3::BitvectorProofRules.
Definition at line 142 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BOOLEXTRACT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Expr::isAnd(), CVC3::Expr::isEq(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
e | : input disequality: e1 != e2 over bitvector terms |
f | : formula over the bits of bitvector variables in e: |
Implements CVC3::BitvectorProofRules.
Definition at line 225 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BOOLEXTRACT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Expr::isIff(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
sign extend the input SX(e) appropriately
signExtendRule: pads the input e with topBit to length len
Implements CVC3::BitvectorProofRules.
Definition at line 339 of file bitvector_theorem_producer.cpp.
References CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::SX, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by bitExtractSXRule().
Pad the kids of BVLT/BVLE to make their length equal.
Pad the kids of BVLT/BVLE to make their bvLength equal.
Implements CVC3::BitvectorProofRules.
Definition at line 305 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVLE, CVC3::BVLT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Sign Extend the kids of BVSLT/BVSLE to make their length equal.
Pad the kids of SIGN BVLT/SIGN BVLE to make their bvLength equal.
Implements CVC3::BitvectorProofRules.
Definition at line 397 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVSLE, CVC3::BVSLT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoryBitvector::newSXExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|
virtual |
input: e0 <=(s) e1. output depends on whether the topbits(MSB) of e0 and e1 are constants. If they are constants then optimizations are done, otherwise the following rule is implemented.
e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0])
input: e0 <=(s) e1. output depends on whether the topbits(MSB) of e0 and e1 are constants. If they are constants then optimizations are done, otherwise the following rule is implemented.
e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR (e0[n-1] = e1[n-1] AND e0[n-2:0] <= e1[n-2:0])
Implements CVC3::BitvectorProofRules.
Definition at line 437 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVCONST, bvOne(), CVC3::TheoryBitvector::BVSize(), CVC3::BVSLE, CVC3::BVSLT, bvZero(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Theory::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
NOT(e[0][0] = e[0][1]) <==> e[0][0] = ~e[0][1]
Implements CVC3::BitvectorProofRules.
Definition at line 606 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), EQ, CVC3::Expr::eqExpr(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), NOT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
NOT(e[0][0] < e[0][1]) <==> (e[0][1] <= e[0][0]), NOT(e[0][0] <= e[0][1]) <==> (e[0][1] < e[0][0])
Implements CVC3::BitvectorProofRules.
Definition at line 631 of file bitvector_theorem_producer.cpp.
References CVC3::BVLE, CVC3::BVLT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), NOT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
Implements CVC3::BitvectorProofRules.
Definition at line 658 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVLE, CVC3::BVLT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
|= 0 <= foo <-> TRUE
Implements CVC3::BitvectorProofRules.
Definition at line 686 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVLE, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
if indeed e[0] < e[1] then (e<==>true) else (e<==>false)
Implements CVC3::BitvectorProofRules.
Definition at line 704 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVLE, CVC3::BVLT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::BitvectorProofRules.
Definition at line 762 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BOOLEXTRACT, CVC3::BVLE, CVC3::BVLT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::Expr::isFalse(), CVC3::Expr::isNull(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTrue(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::toString(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 895 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BOOLEXTRACT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Expr::getKind(), IFF, CVC3::Expr::isBoolConst(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0
Implements CVC3::BitvectorProofRules.
Definition at line 927 of file bitvector_theorem_producer.cpp.
References CVC3::BOOLEXTRACT, bvOne(), bvZero(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Theorem::getExpr(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::Expr::isNot(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i])
Implements CVC3::BitvectorProofRules.
Definition at line 948 of file bitvector_theorem_producer.cpp.
References CVC3::BOOLEXTRACT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
x | : input1 is bitvector constant |
i | : input2 is extracted bitposition |
Implements CVC3::BitvectorProofRules.
Definition at line 977 of file bitvector_theorem_producer.cpp.
References CVC3::BVCONST, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), TRACE, CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
x | : input1 is bitvector binary concatenation |
i | : input2 is extracted bitposition |
Implements CVC3::BitvectorProofRules.
Definition at line 1017 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Theory::getBaseType(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
t | : input1 is bitvector binary BVMULT. x[0] must be BVCONST |
i | : input2 is extracted bitposition |
Implements CVC3::BitvectorProofRules.
Definition at line 1074 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
t | : input1 is bitvector binary BVMULT. t[0] must not be BVCONST |
i | : input2 is extracted bitposition |
Implements CVC3::BitvectorProofRules.
Definition at line 1141 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), TRACE, CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
x | : input1 is bitvector extraction [k:j] |
i | : input2 is extracted bitposition |
Implements CVC3::BitvectorProofRules.
Definition at line 1206 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::Type::getExpr(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
|
virtual |
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 |
Implements CVC3::BitvectorProofRules.
Definition at line 1256 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVPLUS, CHECK_PROOFS, CHECK_SOUND, computeCarry(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::Expr::getOpKind(), CVC3::Expr::iffExpr(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::BitvectorProofRules.
Definition at line 1337 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BOOLEXTRACT, CVC3::BVPLUS, CHECK_PROOFS, CHECK_SOUND, computeCarryPreComputed(), d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::iffExpr(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Theorem::toString(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
bvPlusTerm | : input1 is bvPlusTerm, a BVPLUS term with arity > 2 |
Implements CVC3::BitvectorProofRules.
Definition at line 1497 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
x | : input1 is bitwise NEGATION |
i | : input2 is extracted bitposition |
Implements CVC3::BitvectorProofRules.
Definition at line 1539 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVNEG, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
Extract from bitwise AND, OR, or XOR.
Implements CVC3::BitvectorProofRules.
Definition at line 1575 of file bitvector_theorem_producer.cpp.
References AND, CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BITVECTOR, CVC3::BVAND, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Theory::getEM(), CVC3::Type::getExpr(), CVC3::ExprManager::getKindName(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), OR, rat(), CVC3::Type::toString(), CVC3::Theorem::toString(), CVC3::Expr::toString(), TRACE, CVC3::TheoremProducer::withProof(), and XOR.
x | : input1 is bitvector FIXED SHIFT
|
i | : input2 is extracted bitposition |
Implements CVC3::BitvectorProofRules.
Definition at line 1619 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONST_WIDTH_LEFTSHIFT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Type::getExpr(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::LEFTSHIFT, CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 1668 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Type::getExpr(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::RIGHTSHIFT, CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 1721 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVSHL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), OR, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 1775 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVLSHR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), OR, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 1829 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVASHR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), OR, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
e | : input1 is bitvector term |
r | : input2 is extracted bitposition |
Implements CVC3::BitvectorProofRules.
Definition at line 1470 of file bitvector_theorem_producer.cpp.
References CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
bitExtractSXRule
Implements CVC3::BitvectorProofRules.
Definition at line 380 of file bitvector_theorem_producer.cpp.
References d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theorem::getRHS(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), signExtendRule(), and CVC3::TheoremProducer::withProof().
c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
Implements CVC3::BitvectorProofRules.
Definition at line 1893 of file bitvector_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Expr::isEq(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
|- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
Implements CVC3::BitvectorProofRules.
Definition at line 1911 of file bitvector_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Theorem::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().
t<<n = c @ 0bin00...00, takes e == (t<<n)
t<<n = c @ 0bin00...00, takes e == (t<<n)
Implements CVC3::BitvectorProofRules.
Definition at line 1944 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::Expr::getOpKind(), CVC3::LEFTSHIFT, CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
t<<n = c @ 0bin00...00, takes e == (t<<n)
t<<n = c @ 0bin00...00, takes e == (t<<n)
Implements CVC3::BitvectorProofRules.
Definition at line 1968 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONST_WIDTH_LEFTSHIFT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
t>>m = 0bin00...00 @ t[bvLength-1:m], takes e == (t>>n)
Implements CVC3::BitvectorProofRules.
Definition at line 2001 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::RIGHTSHIFT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
BVSHL(t,c) = t[n-c,0] @ 0bin00...00.
BVSHL(t,c) = t[n-c,0] @ 0bin00...00.
Implements CVC3::BitvectorProofRules.
Definition at line 2033 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVSHL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Rational::getInt(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
Implements CVC3::BitvectorProofRules.
Definition at line 2068 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVSHL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
BVLSHR(t,c) = 0bin00...00 @ t[n-1,c].
BVLSHR(t,c) = 0bin00...00 @ t[n-1,c].
Implements CVC3::BitvectorProofRules.
Definition at line 2107 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVLSHR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Rational::getInt(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
All shifts over a 0 constant = 0.
Implements CVC3::BitvectorProofRules.
Definition at line 2135 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVASHR, CVC3::BVCONST, CVC3::BVLSHR, CVC3::BVSHL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONST_WIDTH_LEFTSHIFT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::LEFTSHIFT, CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::RIGHTSHIFT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
BVASHR(t,c) = SX(t[n-1,c], n-1)
Implements CVC3::BitvectorProofRules.
Definition at line 2155 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVASHR, CVC3::BVCONST, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Rational::getInt(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoryBitvector::newSXExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
a XNOR b <=> (~a & ~b) | (a & b)
Implements CVC3::BitvectorProofRules.
Definition at line 2181 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVXNOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
a NAND b <=> ~(a & b)
Implements CVC3::BitvectorProofRules.
Definition at line 2196 of file bitvector_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::BVNAND, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
a NOR b <=> ~(a | b)
Implements CVC3::BitvectorProofRules.
Definition at line 2211 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVNOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), and CVC3::TheoremProducer::withProof().
BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
Implements CVC3::BitvectorProofRules.
Definition at line 2226 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCOMP, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getKind(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
a - b <=> a + (-b)
Implements CVC3::BitvectorProofRules.
Definition at line 2241 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), buildPlusTerm(), CVC3::TheoryBitvector::BVSize(), CVC3::BVSUB, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), getPlusTerms(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
k*t = BVPLUS(n, <sum of shifts of t>) – translation of k*t to BVPLUS
If k = 2^m, return k*t = t@0...0
Implements CVC3::BitvectorProofRules.
Definition at line 2270 of file bitvector_theorem_producer.cpp.
References CVC3::abs(), CVC3::Expr::arity(), CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::Expr::getRational(), CVC3::Rational::isInteger(), CVC3::Expr::isRational(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
where k is the size of the 0bin0...0
Implements CVC3::BitvectorProofRules.
Definition at line 2318 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVCONST, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 3356 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 3378 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
t1*a <==> a*t1
Implements CVC3::BitvectorProofRules.
Definition at line 3403 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
converts e to a bitvector of length rat
Converts e into a BVVECTOR of bvLength 'len'.
len | is the desired bvLength of the resulting bitvector |
e | is the original bitvector of arbitrary bvLength |
Definition at line 3424 of file bitvector_theorem_producer.cpp.
References CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), d_theoryBitvector, DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), and CVC3::Expr::toString().
Referenced by bvUDivTheorem(), oneCoeffBVMult(), padBVLTRule(), padBVMult(), and padBVPlus().
Pad the kids of BVMULT to make their bvLength = # of output-bits.
Implements CVC3::BitvectorProofRules.
Definition at line 3449 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Pad the kids of BVMULT to make their bvLength = # of output-bits.
Implements CVC3::BitvectorProofRules.
Definition at line 3479 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
a*(b*t) <==> (a*b)*t, where a,b,t have same bvLength
Implements CVC3::BitvectorProofRules.
Definition at line 3503 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
(t1*t2)*t3 <==> t1*(t2*t3), where t1<t2<t3
Implements CVC3::BitvectorProofRules.
Definition at line 3541 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
a*(t1+...+tn) <==> (a*t1+...+a*tn), where all kids are equibvLength
Implements CVC3::BitvectorProofRules.
Definition at line 3615 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
input BVPLUS expression e.output e <==> e', where e' has no BVPLUS
Implements CVC3::BitvectorProofRules.
Definition at line 3655 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 3865 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, collectLikeTermsOfPlus(), createNewPlusCollection(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), sumNormalizedElements(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 3916 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), EQ, CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
(x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n
Implements CVC3::BitvectorProofRules.
Definition at line 4209 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVMultPadExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
(x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n
Implements CVC3::BitvectorProofRules.
Definition at line 4241 of file bitvector_theorem_producer.cpp.
References CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVPlusPadExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
Implements CVC3::BitvectorProofRules.
Definition at line 2591 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), ITE, CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
~ite(c,t1,t2) <=> ite(c,~t1,~t2)
Implements CVC3::BitvectorProofRules.
Definition at line 2627 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), ITE, CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
-0 <==> 0, -c <==> ~c+1
Implements CVC3::BitvectorProofRules.
Definition at line 4011 of file bitvector_theorem_producer.cpp.
References CVC3::BVCONST, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::TheoryBitvector::computeNegBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
-(c*t)<=>(-c)*t; if -c==0 return e<=>0. if(-c==1) return e<=>t
Implements CVC3::BitvectorProofRules.
Definition at line 4038 of file bitvector_theorem_producer.cpp.
References CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeNegBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
-(-e) <==> e
Implements CVC3::BitvectorProofRules.
Definition at line 4084 of file bitvector_theorem_producer.cpp.
References CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
-v <==> -1*v
Implements CVC3::BitvectorProofRules.
Definition at line 4105 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
c*(-t) <==> (-c)*t
Implements CVC3::BitvectorProofRules.
Definition at line 4128 of file bitvector_theorem_producer.cpp.
References CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeNegBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
-t <==> ~t+1
generic rule used for bitblasting step. -e <==> ~e+1
Implements CVC3::BitvectorProofRules.
Definition at line 3989 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
-(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
Implements CVC3::BitvectorProofRules.
Definition at line 4174 of file bitvector_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
c1[i:j] = c (extraction from a constant bitvector)
Implements CVC3::BitvectorProofRules.
Definition at line 2365 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getBVConstValue(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
t[n-1:0] = t for n-bit t
Implements CVC3::BitvectorProofRules.
Definition at line 2397 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction)
Implements CVC3::BitvectorProofRules.
Definition at line 2421 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
(t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
Implements CVC3::BitvectorProofRules.
Definition at line 2465 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::EXTRACT, CVC3::Theorem::getExpr(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
|
virtual |
Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j].
Implements CVC3::BitvectorProofRules.
Definition at line 2532 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVAND, CVC3::BVNEG, CVC3::BVOR, CVC3::BVXNOR, CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::EXTRACT, CVC3::Theory::getEM(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::ExprManager::getKindName(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by extractAnd(), extractNeg(), and extractOr().
(t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR)
Implements CVC3::BitvectorProofRules.
Definition at line 2571 of file bitvector_theorem_producer.cpp.
References CVC3::BVAND, and extractBitwise().
(t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND)
Implements CVC3::BitvectorProofRules.
Definition at line 2578 of file bitvector_theorem_producer.cpp.
References CVC3::BVOR, and extractBitwise().
(~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
Implements CVC3::BitvectorProofRules.
Definition at line 2585 of file bitvector_theorem_producer.cpp.
References CVC3::BVNEG, and extractBitwise().
~c1 = c (bit-wise negation of a constant bitvector)
Implements CVC3::BitvectorProofRules.
Definition at line 2655 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
~(t1@...@tn) = (~t1)@...@(~tn) – push negation through concat
Implements CVC3::BitvectorProofRules.
Definition at line 2678 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
~(~t) = t – eliminate double negation
Implements CVC3::BitvectorProofRules.
Definition at line 2703 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
~t = -1*t + 1 – eliminate negation
Implements CVC3::BitvectorProofRules.
Definition at line 2719 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVNEG, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
~(t1 & t2) <=> ~t1 | ~t2 – DeMorgan's Laws
~(t1 & t2) = ~t1 | ~t2 – DeMorgan's Laws
Implements CVC3::BitvectorProofRules.
Definition at line 2744 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVAND, CVC3::BVNEG, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
~(t1 | t2) <=> ~t1 & ~t2 – DeMorgan's Laws
~(t1 | t2) = ~t1 & ~t2 – DeMorgan's Laws
Implements CVC3::BitvectorProofRules.
Definition at line 2766 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVNEG, CVC3::BVOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
~(t1 xor t2) = ~t1 xor t2
Implements CVC3::BitvectorProofRules.
Definition at line 2789 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVNEG, CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
~(t1 xnor t2) = t1 xor t2
Implements CVC3::BitvectorProofRules.
Definition at line 2815 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVNEG, CVC3::BVXNOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|
virtual |
Combine constants in bitwise AND, OR, XOR.
c1 op c2 = c – bit-wise AND, OR, XOR of constant bitvectors
Implements CVC3::BitvectorProofRules.
Definition at line 2842 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVAND, CVC3::BVCONST, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), RAW_LIST, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Lifts concatenation above bitwise operators.
Implements CVC3::BitvectorProofRules.
Definition at line 2922 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Flatten bitwise operation.
Implements CVC3::BitvectorProofRules.
Definition at line 2970 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CVC3::BVAND, CVC3::BVNEG, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprMap< Data >::erase(), CVC3::Expr::getOpKind(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), sameKidCheck(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Simplify bitwise operator containing a constant child.
e | is the bit-wise expr |
idx | is the index of the constant bitvector |
kind | is the kind of e |
Implements CVC3::BitvectorProofRules.
Definition at line 3068 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVAND, CVC3::BVCONST, CVC3::BVOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
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
Definition at line 3160 of file bitvector_theorem_producer.cpp.
References CVC3::BVNEG, d_theoryBitvector, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getOpKind(), and CVC3::TheoryBitvector::newBVNegExpr().
Referenced by bitwiseFlatten().
c1@c2@...@cn = c (concatenation of constant bitvectors)
Implements CVC3::BitvectorProofRules.
Definition at line 3195 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by getPlusTerms().
Flatten one level of nested concatenation, e.g.: x@(y@z)@w = x@y@z@w.
Implements CVC3::BitvectorProofRules.
Definition at line 3217 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0].
Implements CVC3::BitvectorProofRules.
Definition at line 3239 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors)
Implements CVC3::BitvectorProofRules.
Definition at line 3290 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::begin(), CVC3::BVPLUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::Expr::getOpKind(), CVC3::int2string(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Rational::toString(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
n*c1 = c, where n >= 0 (multiplication of a constant bitvector by a non-negative constant)
c0*c1 = c, multiplication of two BVCONST
Implements CVC3::BitvectorProofRules.
Definition at line 3329 of file bitvector_theorem_producer.cpp.
References CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), constantKids(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|- t=0 OR t=1 for any 1-bit bitvector t
Implements CVC3::BitvectorProofRules.
Definition at line 4277 of file bitvector_theorem_producer.cpp.
References CVC3::BITVECTOR, bvOne(), CVC3::TheoryBitvector::BVSize(), bvZero(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Expand the type predicate wrapper (compute the actual type predicate)
Implements CVC3::BitvectorProofRules.
Definition at line 4294 of file bitvector_theorem_producer.cpp.
References CVC3::andExpr(), bvOne(), CVC3::BVTYPEPRED, bvZero(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Theory::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::TheoryBitvector::getTypePredExpr(), CVC3::TheoryBitvector::getTypePredType(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), NOT, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Create Expr from Rational (for convenience)
Definition at line 486 of file bitvector_theorem_producer.h.
References CVC3::TheoremProducer::d_em, and CVC3::ExprManager::newRatExpr().
Referenced by bitblastBVMult(), bitblastBVPlus(), bitExtractBitwise(), bitExtractBVASHR(), bitExtractBVLSHR(), bitExtractBVMult(), bitExtractBVPlus(), bitExtractBVPlusPreComputed(), bitExtractBVSHL(), bitExtractConcatenation(), bitExtractConstant(), bitExtractConstBVMult(), bitExtractExtraction(), bitExtractFixedLeftShift(), bitExtractFixedRightShift(), bitExtractNot(), bitExtractSXRule(), bitwiseConcat(), bitwiseConst(), bitwiseConstElim(), computeCarryPreComputed(), constMultToPlus(), and zeroPaddingRule().
Expr BitvectorTheoremProducer::computeCarry | ( | const std::vector< Theorem > & | t1BitExtractThms, |
const std::vector< Theorem > & | t2BitExtractThms, | ||
int | bitPos | ||
) |
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 |
Definition at line 1305 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::andExpr(), DebugAssert, and CVC3::orExpr().
Referenced by bitExtractBVPlus().
Expr BitvectorTheoremProducer::computeCarryPreComputed | ( | const Theorem & | t1_i, |
const Theorem & | t2_i, | ||
int | bitPos, | ||
int | precomputedFlag | ||
) |
compute carryout of the current bits and cache them, and return
Definition at line 1406 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CVC3::TheoryBitvector::d_bvPlusCarryCacheLeftBV, CVC3::TheoryBitvector::d_bvPlusCarryCacheRightBV, d_theoryBitvector, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::ExprMap< Data >::insert(), CVC3::Expr::orExpr(), CVC3::orExpr(), and rat().
Referenced by bitExtractBVPlusPreComputed().
isolate a variable with coefficient = 1 on the Lhs of an
Implements CVC3::BitvectorProofRules.
Definition at line 4371 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), EQ, CVC3::Expr::getOpKind(), CVC3::Expr::isEq(), CVC3::Theory::isLeaf(), CVC3::Theory::isLeafIn(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), and CVC3::Expr::toString().
Implements CVC3::BitvectorProofRules.
Definition at line 4687 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultPadExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
canonize BVMult expressions in order to get one coefficient
Implements CVC3::BitvectorProofRules.
Definition at line 4770 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), buildPlusTerm(), CVC3::BVCONST, CVC3::BVMULT, BVMult_order_subterms(), CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, DebugAssert, distributive_rule(), CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), getPlusTerms(), CVC3::Theorem::getRHS(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 4924 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), CVC3::CONCAT, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
canonize BVPlus expressions in order to get just one
L:: to store the sum of the coefficients for each var
Implements CVC3::BitvectorProofRules.
Definition at line 5559 of file bitvector_theorem_producer.cpp.
References buildPlusTerm(), CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), getPlusTerms(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
canonize BVMinus expressions: push the minus to the leafs in
Implements CVC3::BitvectorProofRules.
Definition at line 5587 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), CVC3::BVUMINUS, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 5609 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, DebugAssert, EQ, CVC3::Expr::eqExpr(), EXISTS, CVC3::EXTRACT, CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), CVC3::Theory::isLeaf(), CVC3::Theory::isLeafIn(), CVC3::TheoryBitvector::newBitvectorType(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
Implements CVC3::BitvectorProofRules.
Definition at line 5692 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CVC3::BITVECTOR, buildPlusTerm(), CVC3::TheoryBitvector::BVSize(), CVC3::BVXOR, CHECK_PROOFS, CHECK_SOUND, CVC3::CONCAT, d_theoryBitvector, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), EQ, CVC3::Expr::eqExpr(), CVC3::EXTRACT, CVC3::Theory::falseExpr(), FatalAssert, CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::getOpKind(), getPlusTerms(), CVC3::Theory::isLeaf(), CVC3::Theory::isLeafIn(), CVC3::Expr::isNull(), CVC3::TheoryBitvector::multiplicative_inverse(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVMultPadExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newReflTheorem(), CVC3::TheoremProducer::newRWTheorem(), okToSplit(), CVC3::TheoryBitvector::pad(), CVC3::pow(), CVC3::Expr::toString(), TRACE, CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
apply the distributive rule on the BVMULT expression e
Implements CVC3::BitvectorProofRules.
Definition at line 4882 of file bitvector_theorem_producer.cpp.
References CVC3::BVMULT, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by canonBVMult().
Implements CVC3::BitvectorProofRules.
Definition at line 4619 of file bitvector_theorem_producer.cpp.
References CVC3::ExprMap< Data >::begin(), CVC3::BVCONST, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::count(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::TheoryBitvector::extract_vars(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by canonBVMult().
Implements CVC3::BitvectorProofRules.
Definition at line 4343 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), EQ, CVC3::Expr::isEq(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::reflexivityRule(), and CVC3::Expr::toString().
BVZEROEXTEND(e, i) = zeroString @ e.
Implements CVC3::BitvectorProofRules.
Definition at line 6081 of file bitvector_theorem_producer.cpp.
References CVC3::BITVECTOR, CVC3::BVZEROEXTEND, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
BVREPEAT(e, i) = e @ e @ ... @ e.
Implements CVC3::BitvectorProofRules.
Definition at line 6109 of file bitvector_theorem_producer.cpp.
References CVC3::BITVECTOR, CVC3::BVREPEAT, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
BVROTL(e, i) = a[n-i-1:0] @ a[n-1:n-i].
Implements CVC3::BitvectorProofRules.
Definition at line 6142 of file bitvector_theorem_producer.cpp.
References CVC3::BITVECTOR, CVC3::BVROTL, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
BVROTR(e, i) = a[i-1:0] @ a[n-1:i].
Implements CVC3::BitvectorProofRules.
Definition at line 6173 of file bitvector_theorem_producer.cpp.
References CVC3::BITVECTOR, CVC3::BVROTR, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::getBVIndex(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Divide a with b unsigned and return the bit-vector constant result
Implements CVC3::BitvectorProofRules.
Definition at line 6243 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::newVar(), and CVC3::TheoremProducer::withProof().
Rewrite x/y to
Implements CVC3::BitvectorProofRules.
Definition at line 6272 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CVC3::andExpr(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVUDIV, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), EXISTS, CVC3::Theory::getEM(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::impExpr(), CVC3::Expr::negate(), CVC3::ExprManager::newBoundVarExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), pad(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Compute the remainder
Implements CVC3::BitvectorProofRules.
Definition at line 6201 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::newVar(), and CVC3::TheoremProducer::withProof().
Rewrite ab in terms of a/b, i.e. a - a/b
Implements CVC3::BitvectorProofRules.
Definition at line 6229 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUDivExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
|
virtual |
Bit-blast the multiplication a_times_b given the bits in a_bits and b_bits. The resulting output bits will be in the vector output_bits. The return value is a theorem saying there is no overflow for this multiplication. (TODO, it's just an empty theorem for now).
Implements CVC3::BitvectorProofRules.
Definition at line 6324 of file bitvector_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVMULT, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::orExpr(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|
virtual |
Bit-blast the sum a_plus_b given the bits in a_bits and b_bits. The resulting output bits will be in the vector output_bits. The return value is a theorem saying there is no overflow for this sum. (TODO, it's just an empty theorem for now).
Implements CVC3::BitvectorProofRules.
Definition at line 6407 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::BITVECTOR, CVC3::BVPLUS, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Type::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Rewrite the signed divide in terms of the unsigned one.
Implements CVC3::BitvectorProofRules.
Definition at line 6462 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CVC3::BITVECTOR, CVC3::BVSDIV, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVUDivExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Rewrite the signed remainder in terms of the unsigned one.
Implements CVC3::BitvectorProofRules.
Definition at line 6518 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVSREM, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVURemExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Rewrite the signed mod in terms of the unsigned one.
Implements CVC3::BitvectorProofRules.
Definition at line 6574 of file bitvector_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CVC3::BITVECTOR, CVC3::TheoryBitvector::BVSize(), CVC3::BVSMOD, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::iteExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVURemExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Rewrite
into
.
Implements CVC3::BitvectorProofRules.
Definition at line 6631 of file bitvector_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::BVCONST, CVC3::BVOR, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::isEq(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Rewrite
into
.
Implements CVC3::BitvectorProofRules.
Definition at line 6653 of file bitvector_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::BVAND, CVC3::BVCONST, CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoryBitvector::computeBVConst(), d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::isEq(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Equalities over constants go to true/false.
Implements CVC3::BitvectorProofRules.
Definition at line 6675 of file bitvector_theorem_producer.cpp.
References CVC3::BVCONST, CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::Expr::isEq(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
|
virtual |
Returns true if equation is of the form x[i:j] = x[k:l], where the extracted segments overlap, i.e. i > j >= k > l or k > i >= l > j.
Implements CVC3::BitvectorProofRules.
Definition at line 6691 of file bitvector_theorem_producer.cpp.
References d_theoryBitvector, CVC3::EXTRACT, CVC3::TheoryBitvector::getExtractHi(), and CVC3::TheoryBitvector::getExtractLow().
Referenced by solveExtractOverlap().
Returns the theorem that simplifies the equality of two overlapping extracts over the same term.
Implements CVC3::BitvectorProofRules.
Definition at line 6713 of file bitvector_theorem_producer.cpp.
References CVC3::TheoryBitvector::BVSize(), CHECK_PROOFS, CHECK_SOUND, d_theoryBitvector, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), EXISTS, CVC3::Theory::getEM(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::Expr::iffExpr(), CVC3::TheoryBitvector::newBitvectorType(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), solveExtractOverlapApplies(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|
private |
Definition at line 44 of file bitvector_theorem_producer.h.
Referenced by bitblastBVMult(), bitblastBVPlus(), bitBlastDisEqnRule(), bitBlastEqnRule(), bitExtractAllToConstEq(), bitExtractBitwise(), bitExtractBVASHR(), bitExtractBVLSHR(), bitExtractBVMult(), bitExtractBVPlus(), bitExtractBVPlusPreComputed(), bitExtractBVSHL(), bitExtractConcatenation(), bitExtractConstant(), bitExtractConstBVMult(), bitExtractExtraction(), bitExtractFixedLeftShift(), bitExtractFixedRightShift(), bitExtractNot(), bitExtractRewrite(), bitExtractSXRule(), bitExtractToExtract(), bitvectorFalseRule(), BitvectorTheoremProducer(), bitvectorTrueRule(), bitwiseConcat(), bitwiseConst(), bitwiseConstElim(), bitwiseFlatten(), buildPlusTerm(), bvashrToConcat(), bvConstIneqn(), bvConstMultAssocRule(), bvlshrToConcat(), BVMult_order_subterms(), bvMultAssocRule(), bvmultBVUminus(), bvmultConst(), bvMultDistRule(), bvPlusAssociativityRule(), bvplusConst(), bvplusZeroConcatRule(), bvSDivRewrite(), bvShiftZero(), bvshlSplit(), bvshlToConcat(), bvSModRewrite(), bvSRemRewrite(), bvUDivConst(), bvUDivTheorem(), bvuminusBVConst(), bvuminusBVMult(), bvuminusToBVPlus(), bvuminusVar(), bvURemConst(), bvURemRewrite(), canonBVEQ(), canonBVMult(), canonBVPlus(), canonBVUMinus(), chopConcat(), collectLikeTermsOfPlus(), collectOneTermOfPlus(), combineLikeTermsRule(), computeCarryPreComputed(), concatConst(), concatMergeExtract(), constEq(), constMultToPlus(), constWidthLeftShiftToConcat(), createNewPlusCollection(), distributive_rule(), eqConst(), eqToBits(), expandTypePred(), extractBitwise(), extractBVMult(), extractBVPlus(), extractConcat(), extractConst(), extractExtract(), extractWhole(), flattenBVPlus(), flipBVMult(), generalIneqn(), getPlusTerms(), isolate_var(), iteBVnegRule(), iteExtractRule(), leftShiftToConcat(), lhsEqRhsIneqn(), lhsMinusRhsRule(), liftConcatBVMult(), liftConcatBVPlus(), MarkNonSolvableEq(), negBVand(), negBVor(), negBVxnor(), negBVxor(), negConcat(), negConst(), negElim(), notBVEQ1Rule(), notBVLTRule(), okToSplit(), oneBVAND(), oneCoeffBVMult(), pad(), padBVLTRule(), padBVMult(), padBVPlus(), padBVSLTRule(), processExtract(), repeatRule(), rewriteBVCOMP(), rewriteBVSub(), rewriteNAND(), rewriteNOR(), rewriteXNOR(), rightShiftToConcat(), rotlRule(), rotrRule(), sameKidCheck(), signBVLTRule(), signExtendRule(), solveExtractOverlap(), solveExtractOverlapApplies(), sumNormalizedElements(), typePredBit(), zeroBVOR(), zeroCoeffBVMult(), zeroExtendRule(), zeroLeq(), and zeroPaddingRule().
|
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().
|
private |
Constant 1-bit bit-vector 0bin1.
Definition at line 48 of file bitvector_theorem_producer.h.
Referenced by BitvectorTheoremProducer(), and bvOne().