CVCL::TheoryBitvector Class Reference
[Theories]

Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG). More...

#include <theory_bitvector.h>

Inheritance diagram for CVCL::TheoryBitvector:

[legend]Collaboration diagram for CVCL::TheoryBitvector:

[legend]List of all members.

Public Member Functions

• TheoryBitvector (TheoryCore *core)
• ~TheoryBitvector ()
• BitvectorProofRules * createProofRules ()
• Theorem pushNegationRec (const Expr &e, bool neg)
• void addSharedTerm (const Expr &e)

  Notify theory of a new shared term.
  

• void assertFact (const Theorem &e)

  Assert a new fact to the decision procedure.
  

• void assertTypePred (const Expr &e, const Theorem &pred)

  Receives all the type predicates for the types of the given theory.
  

• void checkSat (bool fullEffort)

  Check for satisfiability in the theory.
  

• Theorem rewrite (const Expr &e)

  Theory-specific rewrite rules.
  

• Theorem rewriteAux (const Expr &e)
• Theorem rewriteAtomic (const Expr &e)

  Theory-specific rewrites for atomic formulas.
  

• void setup (const Expr &e)

  Set up the term e for call-backs when e or its children change.
  

• void update (const Theorem &e, const Expr &d)

  Notify a theory of a new equality.
  

• Theorem solve (const Theorem &e)

  An optional solver.
  

• void checkType (const Expr &e)

  Check that e is a valid Type expr.
  

• void computeType (const Expr &e)

  Compute and store the type of e.
  

• void computeModelTerm (const Expr &e, std::vector< Expr > &v)

  Add variables from 'e' to 'v' for constructing a concrete model.
  

• void computeModel (const Expr &e, std::vector< Expr > &v)

  Compute the value of a compound variable from the more primitive ones.
  

• Expr computeTypePred (const Type &t, const Expr &e)

  Theory specific computation of the subtyping predicate for type t applied to the expression e.
  

• Expr computeTCC (const Expr &e)

  Compute and cache the TCC of e.
  

• ExprStream & print (ExprStream &os, const Expr &e)

  Theory-specific pretty-printing.
  

• Expr parseExprOp (const Expr &e)

  Theory-specific parsing implemented by the DP.
  

• Expr rat (const Rational &r)
• Expr pad (int len, const Expr &e)

  pads e to be of length len
  

• int BVSize (const Expr &e)

  Return the number of bits in the bitvector expression.
  

• Type newBitvectorType (int i)
• Expr newBitvectorTypePred (const Type &t, const Expr &e)
• Expr newBitvectorTypeExpr (int i)
• Expr newBVAndExpr (const Expr &t1, const Expr &t2)
• Expr newBVAndExpr (const std::vector< Expr > &kids)
• Expr newBVNandExpr (const Expr &t1, const Expr &t2)
• Expr newBVNandExpr (const std::vector< Expr > &kids)
• Expr newBVOrExpr (const Expr &t1, const Expr &t2)
• Expr newBVOrExpr (const std::vector< Expr > &kids)
• Expr newBVNorExpr (const Expr &t1, const Expr &t2)
• Expr newBVNorExpr (const std::vector< Expr > &kids)
• Expr newBVXorExpr (const Expr &t1, const Expr &t2)
• Expr newBVXorExpr (const std::vector< Expr > &kids)
• Expr newBVXnorExpr (const Expr &t1, const Expr &t2)
• Expr newBVXnorExpr (const std::vector< Expr > &kids)
• Expr newBVLTExpr (const Expr &t1, const Expr &t2)
• Expr newBVLEExpr (const Expr &t1, const Expr &t2)
• Expr newSXExpr (const Expr &t1, int len)
• Expr newSBVLTExpr (const Expr &t1, const Expr &t2)
• Expr newSBVLEExpr (const Expr &t1, const Expr &t2)
• Expr newBVNegExpr (const Expr &t1)
• Expr newBVUminusExpr (const Expr &t1)
• Expr newBoolExtractExpr (const Expr &t1, int r)
• Expr newFixedLeftShiftExpr (const Expr &t1, int r)
• Expr newFixedRightShiftExpr (const Expr &t1, int r)
• Expr newConcatExpr (const Expr &t1, const Expr &t2)
• Expr newConcatExpr (const Expr &t1, const Expr &t2, const Expr &t3)
• Expr newConcatExpr (const std::vector< Expr > &kids)
• Expr newBVConstExpr (const std::string &s, int base=2)
• Expr newBVConstExpr (const std::vector< bool > &bits)
• Expr newBVConstExpr (const Rational &r, int len=0)
• Expr newBVZeroString (int r)

  produces a string of 0's of length bvLength
  

• Expr newBVOneString (int r)

  produces a string of 1's of length bvLength
  

• Expr newBVExtractExpr (const Expr &e, int hi, int low)

  hi and low are bit indices
  

• Expr newBVPlusExpr (int numbits, const std::vector< Expr > &k)

  'numbits' is the number of bits in the result
  

• Expr newBVMultExpr (int bvLength, const Expr &t1, const Expr &t2)

  accepts an integer, r, and bitvector, t1, and returns r.t1
  

• int getBitvectorTypeParam (const Expr &e)
• int getBitvectorTypeParam (const Type &t)
• Type getTypePredType (const Expr &tp)
• const Expr & getTypePredExpr (const Expr &tp)
• int getSXIndex (const Expr &e)
• int getBoolExtractIndex (const Expr &e)
• int getFixedLeftShiftParam (const Expr &e)
• int getFixedRightShiftParam (const Expr &e)
• int getExtractHi (const Expr &e)
• int getExtractLow (const Expr &e)
• int getBVPlusParam (const Expr &e)
• int getBVMultParam (const Expr &e)
• unsigned getBVConstSize (const Expr &e)
• bool getBVConstValue (const Expr &e, int i)
• Rational computeBVConst (const Expr &e)

  computes the integer value of a bitvector constant
  

• Rational computeNegBVConst (const Expr &e)

  computes the integer value of ~c+1 or BVUMINUS(c)
  

Public Attributes

• ExprMap< Expr > d_bvPlusCarryCacheLeftBV
• ExprMap< Expr > d_bvPlusCarryCacheRightBV

Private Member Functions

• const Expr & bvZero () const

  Return cached constant 0bin0.
  

• const Expr & bvOne () const

  Return cached constant 0bin1.
  

• Theorem bitBlastEqn (const Expr &e)

  functions which implement the DP strategy for bitblasting
  

• Theorem bitBlastDisEqn (const Theorem &e)

  functions which implement the DP strategy for bitblasting
  

• Theorem bitBlastTerm (const Expr &t, int bitPosition, int preComputed)

  functions which implement the DP strategy for bitblasting
  

• Theorem TheoryBitvector::bitBlastIneqn (const Expr &e)

  function which implements the DP strtagey to bitblast Inequations
  

• Theorem combineLikeTerms (const Expr &e)

  strategy functions for BVPLUS_NORMAL_FORM
  

• Theorem padBVPlus (const Expr &e)

  strategy fucntions for BVPLUS NORMAL FORM
  

• Theorem flattenBVPlus (const Expr &e)

  strategy fucntions for BVPLUS NORMAL FORM
  

• Theorem normalizeConcat (const Expr &e, bool useFind)

  Implementation of the concatenation normal form.
  

• Theorem normalizeBVArith (const Expr &e, bool useFind)

  Implementation of the n-bit arithmetic normal form.
  

• Theorem normalizeConcat (const Theorem &t, bool useFind)

  Helper method for composing normalizations.
  

• Theorem normalizeBVArith (const Theorem &t, bool useFind)

  Helper method for composing normalizations.
  

• Theorem signExtendBVLT (const Expr &e, int len, bool useFind)

  signextend e0 <=(s) e1 appropriately, then normalize and return
  

• Theorem pushNegationRec (const Theorem &thm, bool neg)
• Theorem pushNegation (const Expr &e)
• virtual Theorem simplifyOp (const Expr &e)

  Top down simplifier.
  

• Theorem rewriteConst (const Expr &e)

  Internal rewrite method for constants.
  

• Theorem rewriteBV (const Expr &e, bool useFind)

  Internal rewrite method.
  

• Theorem rewriteBV (const Expr &e, int n, bool useFind)

  Rewrite children 'n' levels down (n==1 means "only the top level").
  

• Theorem rewriteBV (const Theorem &t, int n, bool useFind)

  Rewrite children 'n' levels down (n==1 means "only the top level").
  

• Theorem rewriteBV (const Expr &e, ExprMap< Theorem > &cache, bool useFind)

  Internal rewrite method (implements the actual rewrites).
  

• Theorem rewriteBV (const Expr &e, ExprMap< Theorem > &cache, int n, bool useFind)

  Rewrite children 'n' levels down (n==1 means "only the top level").
  

• Theorem rewriteBV (const Theorem &t, ExprMap< Theorem > &cache, int n, bool useFind)

  Rewrite children 'n' levels down (n==1 means "only the top level").
  

• Theorem rewriteBoolean (const Expr &e)

  rewrite input boolean expression e to a simpler form
  

• void collectSharedSubterms (const Expr &e)

  Collect subterms of shared terms.
  

• void setupExpr (const Expr &e)

  Setup the NotifyList mechanism for the Expr e.
  

Private Attributes

• BitvectorProofRules * d_rules
• size_t d_bvConstExprIndex

  MemoryManager index for BVConstExpr subclass.
  

• size_t d_bvPlusExprIndex
• size_t d_bvParameterExprIndex
• size_t d_bvTypePredExprIndex
• StatCounter d_bvDelayEq

  counts delayed asserted equalities
  

• StatCounter d_bvAssertEq

  counts asserted equalities
  

• StatCounter d_bvDelayDiseq

  counts delayed asserted disequalities
  

• StatCounter d_bvAssertDiseq

  counts asserted disequalities
  

• StatCounter d_bvTypePreds

  counts type predicates
  

• StatCounter d_bvDelayTypePreds

  counts delayed type predicates
  

• StatCounter d_bvBitBlastEq

  counts bitblasted equalities
  

• StatCounter d_bvBitBlastDiseq

  counts bitblasted disequalities
  

• const bool * d_simplifyFlag

  Command line flag: simplify bit-blasted expressions before enqueuing.
  

• const bool * d_booleanRWFlag

  boolean on the fly rewrite flag
  

• const bool * d_boolExtractCacheFlag

  bool extract cache flag
  

• const bool * d_bv32Flag

  flag which indicates that all arithmetic is 32 bit with no overflow
  

• const bool * d_rewriteFlag

  Command line flag: rewrite bitvector expressions.
  

• const bool * d_concatRewriteFlag

  Command line flag: concatenation normal form rewrite bitvector expressions.
  

• const bool * d_bvplusRewriteFlag

  Command line flag: bvplus normal form rewrite bitvector expressions.
  

• const bool * d_rwBitBlastFlag

  Commant line flag: rewrite while bit-blasting.
  

• const bool * d_cnfBitBlastFlag

  Commant line flag: bit-blast equalities in CNF converter.
  

• const bool * d_lhsMinusRhsFlag

  Command line flag: enable lhs-minus-rhs-rule for lhs=rhs.
  

• const bool * d_updateFlag

  Command line flag: update bitvector expressions on find pointer merges.
  

• const bool * d_setupFlag

  Command line flag: setup bitvector expressions for single bit changes.
  

• const bool * d_setupSharedFlag

  Command line flag: setup only shared subexpressions.
  

• const bool * d_pushNegationFlag

  Command line flag: enable pushnegation.
  

• CDMap< Expr, Theorem > d_bitvecCache

  Cache for storing the results of the bitBlastTerm function.
  

• ExprMap< Theorem > d_pushNegCache

  Cache for pushNegation(). it is ok that this is cache is.
  

• CDList< Theorem > d_eq

  Backtracking queue for equalities (to delay them till checkSat() call).
  

• CDO< size_t > d_eqIdx

  Pointer to the next unasserted equality in d_eq.
  

• CDO< size_t > d_eqBlastIdx

  Pointer to the next equality in d_eq which is not bit-blasted yet.
  

• CDList< Theorem > d_diseq

  Backtracking queue for disequalities (to delay them till checkSat() call).
  

• CDO< size_t > d_diseqIdx

  Pointer to the next unasserted disequality in d_diseq.
  

• CDMap< Expr, bool > d_staleDB

  Database of stale bit-expansions for update().
  

• CDList< Theorem > d_tccs

  Backtracking queue for TCCs on individual bits.
  

• CDO< size_t > d_tccsIdx

  Pointer to the next unasserted TCC in d_tccs.
  

• CDMap< Expr, bool > d_sharedSubterms

  Backtracking database of subterms of shared terms.
  

• CDMap< Expr, Theorem > d_typePredsCache

  Cache for typePredicates of non shared terms.
  

• Expr d_bvZero

  Constant 1-bit bit-vector 0bin0.
  

• Expr d_bvOne

  Constant 1-bit bit-vector 0bin0.
  

---

Detailed Description

Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG).

Author: Vijay Ganesh

Created:Wed May 5 15:35:07 PDT 2004

Definition at line 91 of file theory_bitvector.h.

---

Constructor & Destructor Documentation

TheoryBitvector::TheoryBitvector (  TheoryCore *  core  )

Definition at line 1974 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BOOLEXTRACT, CVCL::BVAND, CVCL::BVCONST, CVCL::BVGE, CVCL::BVGT, CVCL::BVLE, CVCL::BVLT, CVCL::BVMULT, CVCL::BVNAND, CVCL::BVNEG, CVCL::BVNOR, CVCL::BVOR, CVCL::BVPARAMOP, CVCL::BVPLUS, CVCL::BVSUB, CVCL::BVTOINT, CVCL::BVTYPEPRED, CVCL::BVUMINUS, CVCL::BVXNOR, CVCL::BVXOR, CVCL::CONCAT, createProofRules(), d_bvConstExprIndex, d_bvOne, d_bvZero, d_rules, CVCL::EXTRACT, CVCL::Theory::getEM(), CVCL::HEXBVCONST, CVCL::INTTOBV, CVCL::LEFTSHIFT, newBVConstExpr(), CVCL::ExprManager::newKind(), CVCL::ExprManager::registerSubclass(), CVCL::Theory::registerTheory(), CVCL::RIGHTSHIFT, CVCL::SBVGE, CVCL::SBVGT, CVCL::SBVLE, CVCL::SBVLT, CVCL::SX, and CVCL::VARSHIFT.

TheoryBitvector::~TheoryBitvector (   )

Definition at line 2099 of file theory_bitvector.cpp. References d_rules.

---

Member Function Documentation

const Expr& CVCL::TheoryBitvector::bvZero (   )  const [inline, private]

Return cached constant 0bin0. Definition at line 182 of file theory_bitvector.h. References d_bvZero.

const Expr& CVCL::TheoryBitvector::bvOne (   )  const [inline, private]

Return cached constant 0bin1. Definition at line 184 of file theory_bitvector.h. References d_bvOne.

Theorem TheoryBitvector::bitBlastEqn (  const Expr &  e  )  [private]

functions which implement the DP strategy for bitblasting Returns: a rewrite theorem which is a conjunction of equivalences over the bits of t1,t2 respectively. Definition at line 65 of file theory_bitvector.cpp. References CVCL::AND, CVCL::BitvectorProofRules::bitBlastEqnRule(), bitBlastTerm(), CVCL::BITVECTOR, CVCL::BitvectorProofRules::bitvectorFalseRule(), BVSize(), CVCL::ExprMap< Data >::clear(), CVCL::Debug::counter(), d_bvBitBlastEq, d_bvPlusCarryCacheLeftBV, d_bvPlusCarryCacheRightBV, d_rules, CVCL::debugger, CVCL::Theory::getBaseType(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), IF_DEBUG(), CVCL::IFF, CVCL::Expr::isEq(), CVCL::Expr::isFalse(), CVCL::Theory::reflexivityRule(), rewriteBoolean(), CVCL::Theory::substitutivityRule(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::Theory::transitivityRule(). Referenced by assertFact(), checkSat(), and rewriteAtomic().

Theorem TheoryBitvector::bitBlastDisEqn (  const Theorem &  notE  )  [private]

functions which implement the DP strategy for bitblasting Returns: a rewrite theorem which is a conjunction of (dis)-equivalences over the bits of t1,t2 respectively. A separate rule for disequations for efficiency sake. Obvious implementation using rule for equations and rule for NOT, is not efficient. Definition at line 145 of file theory_bitvector.cpp. References CVCL::BitvectorProofRules::bitBlastDisEqnRule(), bitBlastTerm(), CVCL::BITVECTOR, CVCL::BitvectorProofRules::bitvectorTrueRule(), BVSize(), CVCL::ExprMap< Data >::clear(), CVCL::Debug::counter(), d_bvBitBlastDiseq, d_bvPlusCarryCacheLeftBV, d_bvPlusCarryCacheRightBV, d_rules, CVCL::debugger, CVCL::Theory::getCommonRules(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), IF_DEBUG(), CVCL::IFF, CVCL::CommonProofRules::iffContrapositive(), CVCL::Theory::iffMP(), CVCL::Expr::isNot(), CVCL::Expr::isTrue(), CVCL::OR, rewriteBoolean(), CVCL::Theory::substitutivityRule(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::Theory::transitivityRule(). Referenced by assertFact(), and checkSat().

Theorem TheoryBitvector::bitBlastTerm (  const Expr &  t, int  bitPosition, int  preComputed )  [private]

functions which implement the DP strategy for bitblasting The invariant maintained by this function is: accepts a bitvector term, t,and a bitPosition, i. returns a formula over the set of propositional variables defined using BOOLEXTRACT of bitvector variables in t at the position i. Returns: Theorem(BOOLEXTRACT(t, bitPosition) <=> phi), where phi is a Boolean formula over the individual bits of bit-vector variables. Definition at line 365 of file theory_bitvector.cpp. References CVCL::AND, CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BitvectorProofRules::bitExtractAnd(), CVCL::BitvectorProofRules::bitExtractBVMult(), CVCL::BitvectorProofRules::bitExtractBVPlus(), CVCL::BitvectorProofRules::bitExtractBVPlusPreComputed(), CVCL::BitvectorProofRules::bitExtractConcatenation(), CVCL::BitvectorProofRules::bitExtractConstant(), CVCL::BitvectorProofRules::bitExtractConstBVMult(), CVCL::BitvectorProofRules::bitExtractExtraction(), CVCL::BitvectorProofRules::bitExtractFixedLeftShift(), CVCL::BitvectorProofRules::bitExtractFixedRightShift(), CVCL::BitvectorProofRules::bitExtractNot(), CVCL::BitvectorProofRules::bitExtractOr(), CVCL::BitvectorProofRules::bitExtractSXRule(), CVCL::BITVECTOR, CVCL::BOOLEXTRACT, CVCL::BVAND, CVCL::BVCONST, CVCL::BVMULT, CVCL::BVNEG, CVCL::BVOR, CVCL::BVPLUS, CVCL::BitvectorProofRules::bvPlusAssociativityRule(), BVSize(), CVCL::BVSUB, CVCL::BVUMINUS, CVCL::BitvectorProofRules::bvuminusToBVPlus(), CVCL::CONCAT, d_bitvecCache, d_rules, CVCL::Expr::end(), CVCL::CDMap< Key, Data, HashFcn >::end(), CVCL::EXTRACT, CVCL::CDMap< Key, Data, HashFcn >::find(), getBoolExtractIndex(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Expr::getOp(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), IF_DEBUG(), CVCL::int2string(), CVCL::Expr::isBoolConst(), CVCL::Theorem::isNull(), CVCL::LEFTSHIFT, newBoolExtractExpr(), CVCL::NOT, CVCL::OR, CVCL::Theory::reflexivityRule(), rewriteBoolean(), rewriteBV(), CVCL::RIGHTSHIFT, CVCL::Theory::substitutivityRule(), CVCL::SX, CVCL::Expr::toString(), CVCL::Theorem::toString(), CVCL::TRACE, CVCL::Theory::transitivityRule(), and CVCL::BitvectorProofRules::zeroPaddingRule(). Referenced by bitBlastDisEqn(), and bitBlastEqn().

Theorem CVCL::TheoryBitvector::TheoryBitvector::bitBlastIneqn (  const Expr &  e  )  [private]

function which implements the DP strtagey to bitblast Inequations

Theorem TheoryBitvector::combineLikeTerms (  const Expr &  e  )  [private]

strategy functions for BVPLUS_NORMAL_FORM Definition at line 1333 of file theory_bitvector.cpp. References CVCL::BitvectorProofRules::combineLikeTermsRule(), and d_rules. Referenced by normalizeBVArith().

Theorem TheoryBitvector::padBVPlus (  const Expr &  e  )  [private]

strategy fucntions for BVPLUS NORMAL FORM Definition at line 1338 of file theory_bitvector.cpp. References CVCL::BVPLUS, d_rules, CVCL::Theorem::getExpr(), CVCL::Expr::getOpKind(), CVCL::BitvectorProofRules::padBVPlus(), CVCL::Expr::toString(), and CVCL::TRACE. Referenced by normalizeBVArith(), normalizeConcat(), and simplifyOp().

Theorem TheoryBitvector::flattenBVPlus (  const Expr &  e  )  [private]

strategy fucntions for BVPLUS NORMAL FORM Definition at line 1364 of file theory_bitvector.cpp. References CVCL::Expr::begin(), CVCL::BVPLUS, d_rules, CVCL::Expr::end(), CVCL::BitvectorProofRules::flattenBVPlus(), CVCL::Expr::getOpKind(), CVCL::Theory::reflexivityRule(), and CVCL::Expr::toString(). Referenced by normalizeBVArith().

Theorem TheoryBitvector::normalizeConcat (  const Expr &  e, bool  useFind )  [private]

Implementation of the concatenation normal form. Definition at line 687 of file theory_bitvector.cpp. References CVCL::BitvectorProofRules::andConcat(), CVCL::BitvectorProofRules::andConst(), CVCL::BitvectorProofRules::andFlatten(), CVCL::BitvectorProofRules::andOne(), CVCL::BitvectorProofRules::andZero(), CVCL::Expr::arity(), CVCL::BVAND, CVCL::BVCONST, CVCL::BVMULT, CVCL::BVNEG, CVCL::BVOR, CVCL::BVPLUS, CVCL::BitvectorProofRules::bvplusZeroConcatRule(), BVSize(), CVCL::BVXOR, computeBVConst(), CVCL::CONCAT, CVCL::BitvectorProofRules::concatConst(), CVCL::BitvectorProofRules::concatFlatten(), CVCL::BitvectorProofRules::concatMergeExtract(), constantKids(), d_rules, CVCL::EXTRACT, CVCL::BitvectorProofRules::extractAnd(), CVCL::BitvectorProofRules::extractBitwise(), CVCL::BitvectorProofRules::extractBVMult(), CVCL::BitvectorProofRules::extractBVPlus(), CVCL::BitvectorProofRules::extractConcat(), CVCL::BitvectorProofRules::extractConst(), CVCL::BitvectorProofRules::extractExtract(), CVCL::BitvectorProofRules::extractNeg(), CVCL::BitvectorProofRules::extractOr(), CVCL::BitvectorProofRules::extractWhole(), getBVConstSize(), getBVConstValue(), CVCL::Theorem::getExpr(), getExtractHi(), getExtractLow(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::hasFind(), CVCL::int2string(), CVCL::BitvectorProofRules::negConcat(), CVCL::BitvectorProofRules::negConst(), CVCL::BitvectorProofRules::negNeg(), newConcatExpr(), CVCL::BitvectorProofRules::orConcat(), CVCL::BitvectorProofRules::orConst(), CVCL::BitvectorProofRules::orFlatten(), CVCL::BitvectorProofRules::orOne(), CVCL::BitvectorProofRules::orZero(), padBVPlus(), CVCL::Theory::reflexivityRule(), rewriteBV(), CVCL::Theory::rewriteCC(), CVCL::Theory::simplify(), CVCL::Theory::substitutivityRule(), CVCL::Theory::symmetryRule(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::Theory::transitivityRule(). Referenced by normalizeConcat(), and rewriteBV().

Theorem TheoryBitvector::normalizeBVArith (  const Expr &  e, bool  useFind )  [private]

Implementation of the n-bit arithmetic normal form. accepts an expression e, and returns a theorem e <==> BVPLUS_NORMAL_FORM(e) we always assume that kids of e are in bvplus normal form, and only the top-level needs normalization Definition at line 1189 of file theory_bitvector.cpp. References CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVCONST, CVCL::BitvectorProofRules::bvConstMultAssocRule(), CVCL::BVMULT, CVCL::BitvectorProofRules::bvmultConst(), CVCL::BitvectorProofRules::bvMultDistRule(), CVCL::BVPLUS, CVCL::BVUMINUS, CVCL::BitvectorProofRules::bvuminusToBVPlus(), combineLikeTerms(), computeBVConst(), constantKids(), d_rules, flattenBVPlus(), CVCL::BitvectorProofRules::flipBVMult(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::BitvectorProofRules::oneCoeffBVMult(), CVCL::BitvectorProofRules::padBVMult(), padBVPlus(), pushNegation(), CVCL::Theory::reflexivityRule(), rewriteBV(), CVCL::Theory::substitutivityRule(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::Theory::transitivityRule(), and CVCL::BitvectorProofRules::zeroCoeffBVMult(). Referenced by normalizeBVArith(), and rewriteBV().

Theorem CVCL::TheoryBitvector::normalizeConcat (  const Theorem &  t, bool  useFind )  [inline, private]

Helper method for composing normalizations. Definition at line 207 of file theory_bitvector.h. References CVCL::Theorem::getRHS(), normalizeConcat(), and CVCL::Theory::transitivityRule().

Theorem CVCL::TheoryBitvector::normalizeBVArith (  const Theorem &  t, bool  useFind )  [inline, private]

Helper method for composing normalizations. Definition at line 211 of file theory_bitvector.h. References CVCL::Theorem::getRHS(), normalizeBVArith(), and CVCL::Theory::transitivityRule().

Theorem TheoryBitvector::signExtendBVLT (  const Expr &  e, int  len, bool  useFind )  [private]

signextend e0 <=(s) e1 appropriately, then normalize and return Definition at line 1388 of file theory_bitvector.cpp. References d_rules, CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::BitvectorProofRules::padSBVLTRule(), CVCL::Theory::reflexivityRule(), rewriteBV(), CVCL::SBVLE, CVCL::SBVLT, CVCL::BitvectorProofRules::signExtendRule(), CVCL::Theory::substitutivityRule(), CVCL::Expr::toString(), and CVCL::Theory::transitivityRule(). Referenced by rewriteBV().

Theorem TheoryBitvector::pushNegationRec (  const Theorem &  thm, bool  neg )  [private]

Definition at line 1875 of file theory_bitvector.cpp. References CVCL::Theorem::getRHS(), CVCL::Expr::isNot(), CVCL::Theorem::isRewrite(), CVCL::Theorem::toString(), and CVCL::Theory::transitivityRule(). Referenced by CVCL::BitvectorTheoremProducer::collectOneTermOfPlus(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), pushNegation(), and pushNegationRec().

Theorem TheoryBitvector::pushNegation (  const Expr &  e  )  [private]

Definition at line 1890 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVNEG, CVCL::ExprMap< Data >::clear(), d_pushNegCache, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), pushNegationRec(), and CVCL::Theory::reflexivityRule(). Referenced by normalizeBVArith(), and simplifyOp().

Theorem TheoryBitvector::simplifyOp (  const Expr &  e  )  [private, virtual]

Top down simplifier. Reimplemented from CVCL::Theory. Definition at line 1903 of file theory_bitvector.cpp. References CVCL::Expr::arity(), CVCL::BVCONST, CVCL::BVMULT, CVCL::BVNEG, CVCL::BVPLUS, CVCL::BitvectorProofRules::bvplusZeroConcatRule(), computeBVConst(), CVCL::CONCAT, d_rules, CVCL::EXTRACT, CVCL::BitvectorProofRules::extractBVMult(), CVCL::BitvectorProofRules::extractBVPlus(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Theorem::isNull(), CVCL::LEFTSHIFT, CVCL::BitvectorProofRules::leftShiftToConcat(), CVCL::BitvectorProofRules::padBVMult(), padBVPlus(), CVCL::BitvectorProofRules::padBVPlus(), pushNegation(), CVCL::Theory::reflexivityRule(), CVCL::RIGHTSHIFT, CVCL::BitvectorProofRules::rightShiftToConcat(), CVCL::Theory::simplifyRec(), CVCL::Theory::substitutivityRule(), and CVCL::Theory::transitivityRule().

Theorem TheoryBitvector::rewriteConst (  const Expr &  e  )  [private]

Internal rewrite method for constants. Definition at line 1426 of file theory_bitvector.cpp. References CVCL::BitvectorProofRules::andConst(), CVCL::BitvectorProofRules::bitExtractConstant(), CVCL::BOOLEXTRACT, CVCL::BVAND, CVCL::BVMULT, CVCL::BitvectorProofRules::bvmultConst(), CVCL::BVNEG, CVCL::BVOR, CVCL::BVPLUS, CVCL::BitvectorProofRules::bvplusConst(), CVCL::CONCAT, CVCL::BitvectorProofRules::concatConst(), constantKids(), d_rules, CVCL::EQ, CVCL::BitvectorProofRules::eqConst(), CVCL::EXTRACT, CVCL::BitvectorProofRules::extractConst(), getBoolExtractIndex(), CVCL::Expr::getOpKind(), CVCL::BitvectorProofRules::negConst(), CVCL::BitvectorProofRules::orConst(), and CVCL::Theory::reflexivityRule(). Referenced by rewriteAux().

Theorem TheoryBitvector::rewriteBV (  const Expr &  e, bool  useFind )  [private]

Internal rewrite method. Definition at line 1478 of file theory_bitvector.cpp. Referenced by assertFact(), bitBlastTerm(), normalizeBVArith(), normalizeConcat(), parseExprOp(), rewriteAux(), rewriteBV(), and signExtendBVLT().

Theorem TheoryBitvector::rewriteBV (  const Expr &  e, int  n, bool  useFind )  [private]

Rewrite children 'n' levels down (n==1 means "only the top level"). Definition at line 1697 of file theory_bitvector.cpp. References rewriteBV().

Theorem CVCL::TheoryBitvector::rewriteBV (  const Theorem &  t, int  n, bool  useFind )  [inline, private]

Rewrite children 'n' levels down (n==1 means "only the top level"). Definition at line 231 of file theory_bitvector.h. References CVCL::Theorem::getRHS(), rewriteBV(), and CVCL::Theory::transitivityRule().

Theorem TheoryBitvector::rewriteBV (  const Expr &  e, ExprMap< Theorem > &  cache, bool  useFind )  [private]

Internal rewrite method (implements the actual rewrites). 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. In general, the following rule is implemented. Step1: e0 <=(s) e1 <==> pad(e0) <=(s) pad(e1) Step2: pad(e0) <=(s) pad(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]) Definition at line 1484 of file theory_bitvector.cpp. References CVCL::BitvectorProofRules::bitExtractConstant(), CVCL::BitvectorProofRules::bitExtractRewrite(), CVCL::BOOLEXTRACT, CVCL::BVAND, CVCL::BVCONST, CVCL::BitvectorProofRules::bvConstIneqn(), CVCL::BVLE, CVCL::BVLT, CVCL::BVMULT, CVCL::BVNEG, CVCL::BVOR, CVCL::BVPLUS, BVSize(), CVCL::BVUMINUS, CVCL::CONCAT, constantKids(), CVCL::Debug::counter(), d_lhsMinusRhsFlag, d_rules, CVCL::debugger, CVCL::ExprMap< Data >::end(), CVCL::EQ, CVCL::BitvectorProofRules::eqConst(), CVCL::EXTRACT, CVCL::Theory::find(), CVCL::ExprMap< Data >::find(), getBoolExtractIndex(), CVCL::Theorem::getExpr(), getExtractHi(), getExtractLow(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Expr::getOp(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::hasFind(), IF_DEBUG(), CVCL::Theorem::isNull(), CVCL::LEFTSHIFT, CVCL::BitvectorProofRules::leftShiftToConcat(), CVCL::BitvectorProofRules::lhsEqRhsIneqn(), CVCL::BitvectorProofRules::lhsMinusRhsRule(), newBoolExtractExpr(), newBVExtractExpr(), normalizeBVArith(), normalizeConcat(), CVCL::BitvectorProofRules::padBVLTRule(), CVCL::Theory::reflexivityRule(), rewriteBV(), CVCL::Theory::rewriteCC(), CVCL::RIGHTSHIFT, CVCL::BitvectorProofRules::rightShiftToConcat(), CVCL::SBVLE, CVCL::SBVLT, CVCL::BitvectorProofRules::signBVLTRule(), signExtendBVLT(), CVCL::BitvectorProofRules::signExtendRule(), CVCL::Theory::simplify(), CVCL::Theory::substitutivityRule(), CVCL::SX, CVCL::Theory::symmetryRule(), CVCL::TRACE, and CVCL::Theory::transitivityRule().

Theorem TheoryBitvector::rewriteBV (  const Expr &  e, ExprMap< Theorem > &  cache, int  n, bool  useFind )  [private]

Rewrite children 'n' levels down (n==1 means "only the top level"). Definition at line 1703 of file theory_bitvector.cpp. References CVCL::Expr::arity(), CVCL::Debug::counter(), CVCL::debugger, CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), IF_DEBUG(), CVCL::int2string(), CVCL::Theorem::isNull(), CVCL::Theory::reflexivityRule(), rewriteBV(), CVCL::Theory::substitutivityRule(), CVCL::TRACE, and CVCL::Theory::transitivityRule().

Theorem CVCL::TheoryBitvector::rewriteBV (  const Theorem &  t, ExprMap< Theorem > &  cache, int  n, bool  useFind )  [inline, private]

Rewrite children 'n' levels down (n==1 means "only the top level"). Definition at line 240 of file theory_bitvector.h. References CVCL::Theorem::getRHS(), rewriteBV(), and CVCL::Theory::transitivityRule().

Theorem CVCL::TheoryBitvector::rewriteBoolean (  const Expr &  e  )  [private]

rewrite input boolean expression e to a simpler form Definition at line 4258 of file theory_bitvector.cpp. References CVCL::AND, CVCL::Expr::begin(), d_booleanRWFlag, CVCL::Expr::end(), CVCL::Theory::getCommonRules(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::IFF, CVCL::Expr::isNot(), CVCL::Theorem::isNull(), CVCL::NOT, CVCL::OR, CVCL::Theory::reflexivityRule(), CVCL::Theory::rewriteAnd(), CVCL::CommonProofRules::rewriteIff(), CVCL::CommonProofRules::rewriteNotFalse(), CVCL::CommonProofRules::rewriteNotNot(), CVCL::CommonProofRules::rewriteNotTrue(), CVCL::Theory::rewriteOr(), CVCL::Theory::substitutivityRule(), and CVCL::Theory::transitivityRule(). Referenced by assertFact(), bitBlastDisEqn(), bitBlastEqn(), bitBlastTerm(), and checkSat().

void TheoryBitvector::collectSharedSubterms (  const Expr &  e  )  [private]

Collect subterms of shared terms. Definition at line 2105 of file theory_bitvector.cpp. References assertTypePred(), CVCL::Expr::begin(), CVCL::CDMap< Key, Data, HashFcn >::count(), CVCL::Debug::counter(), d_sharedSubterms, d_typePredsCache, CVCL::debugger, CVCL::Expr::end(), CVCL::Theorem::getExpr(), IF_DEBUG(), CVCL::Theory::isLeaf(), CVCL::Theory::setInconsistent(), setupExpr(), CVCL::Expr::toString(), and CVCL::TRACE. Referenced by addSharedTerm().

void TheoryBitvector::setupExpr (  const Expr &  e  )  [private]

Setup the NotifyList mechanism for the Expr e. Definition at line 2420 of file theory_bitvector.cpp. References CVCL::Expr::addToNotify(), CVCL::Expr::arity(), CVCL::BITVECTOR, CVCL::BVCONST, BVSize(), CVCL::CONCAT, CVCL::BitvectorProofRules::concatConst(), CVCL::BitvectorProofRules::concatMergeExtract(), constantKids(), CVCL::Debug::counter(), d_rules, CVCL::debugger, CVCL::Theory::enqueueFact(), CVCL::BitvectorProofRules::extractWhole(), CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::hasFind(), IF_DEBUG(), CVCL::int2string(), CVCL::Expr::isTerm(), newBVExtractExpr(), newConcatExpr(), rewriteAux(), CVCL::Expr::setFind(), CVCL::Theory::setupCC(), CVCL::TheoryCore::setupTerm(), CVCL::Theory::substitutivityRule(), CVCL::Theory::symmetryRule(), CVCL::Theory::theoryCore(), CVCL::TRACE, and CVCL::Theory::transitivityRule(). Referenced by collectSharedSubterms().

BitvectorProofRules * TheoryBitvector::createProofRules (   )

Definition at line 51 of file bitvector_theorem_producer.cpp. Referenced by TheoryBitvector().

Theorem TheoryBitvector::pushNegationRec (  const Expr &  e, bool  neg )

Definition at line 1756 of file theory_bitvector.cpp. References CVCL::Expr::arity(), CVCL::ExprMap< Data >::begin(), CVCL::Expr::begin(), CVCL::BVAND, CVCL::BVCONST, CVCL::BVMULT, CVCL::BVNEG, CVCL::BVOR, CVCL::BVPLUS, CVCL::CONCAT, d_pushNegCache, d_rules, CVCL::Expr::end(), CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), CVCL::Expr::getOp(), CVCL::Theorem::getRHS(), CVCL::BitvectorProofRules::negBVand(), CVCL::BitvectorProofRules::negBVor(), CVCL::BitvectorProofRules::negConcat(), CVCL::BitvectorProofRules::negConst(), CVCL::BitvectorProofRules::negNeg(), newBVNegExpr(), pushNegationRec(), CVCL::Theory::reflexivityRule(), rewriteAux(), CVCL::Theory::substitutivityRule(), CVCL::TRACE, and CVCL::Theory::transitivityRule().

void TheoryBitvector::addSharedTerm (  const Expr &  e  )  [virtual]

Notify theory of a new shared term. When a term e associated with theory i occurs as a child of an expression associated with theory j, the framework calls i->addSharedTerm(e) and j->addSharedTerm(e) Reimplemented from CVCL::Theory. Definition at line 2130 of file theory_bitvector.cpp. References collectSharedSubterms(), CVCL::Debug::counter(), CVCL::debugger, and IF_DEBUG().

void TheoryBitvector::assertFact (  const Theorem &  e  )  [virtual]

Assert a new fact to the decision procedure. Each fact that makes it into the core framework is assigned to exactly one theory: the theory associated with that fact. assertFact is called to inform the theory that a new fact has been assigned to the theory. Implements CVCL::Theory. Definition at line 2136 of file theory_bitvector.cpp. References bitBlastDisEqn(), bitBlastEqn(), CVCL::BitvectorProofRules::bitExtractToExtract(), CVCL::BOOLEXTRACT, CVCL::BVLE, CVCL::BVLT, BVSize(), CVCL::BVTYPEPRED, CVCL::Debug::counter(), d_booleanRWFlag, d_bvAssertDiseq, d_bvAssertEq, d_bvDelayDiseq, d_bvDelayEq, d_diseq, d_eq, d_rules, CVCL::debugger, CVCL::Theory::enqueueFact(), CVCL::EQ, CVCL::BitvectorProofRules::eqToBits(), CVCL::BitvectorProofRules::expandTypePred(), CVCL::Theory::getCommonRules(), CVCL::Theorem::getExpr(), CVCL::TheoryCore::getFlags(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), IF_DEBUG(), CVCL::Theory::iffMP(), CVCL::Theorem::isNull(), CVCL::Theorem::isRewrite(), CVCL::NOT, CVCL::BitvectorProofRules::notBVLTRule(), CVCL::CDList< T >::push_back(), rewriteBoolean(), rewriteBV(), CVCL::Theory::simplify(), CVCL::Theory::theoryCore(), and CVCL::TRACE.

void TheoryBitvector::assertTypePred (  const Expr &  e, const Theorem &  pred )  [virtual]

Receives all the type predicates for the types of the given theory. Type predicates may be expensive to enqueue eagerly, and DPs may choose to postpone them, or transform them to something more efficient. By default, the asserted type predicate is immediately enqueued as a new fact. Note: Used only by bitvector theory. Parameters: e  is the expression for which the type predicate is computed pred  is the predicate theorem P(e) Reimplemented from CVCL::Theory. Definition at line 2235 of file theory_bitvector.cpp. References CVCL::BOOLEXTRACT, CVCL::BVAND, CVCL::BVCONST, CVCL::BVGE, CVCL::BVGT, CVCL::BVLE, CVCL::BVLT, CVCL::BVMULT, CVCL::BVNAND, CVCL::BVNEG, CVCL::BVOR, CVCL::BVPLUS, CVCL::BVSUB, CVCL::BVUMINUS, CVCL::BVXNOR, CVCL::BVXOR, CVCL::CONCAT, CVCL::CDMap< Key, Data, HashFcn >::count(), d_bvDelayTypePreds, d_bvTypePreds, d_setupFlag, d_sharedSubterms, d_tccs, d_typePredsCache, d_updateFlag, CVCL::Theory::enqueueFact(), CVCL::EXTRACT, CVCL::TheoryCore::getFlags(), CVCL::Expr::getOpKind(), CVCL::LEFTSHIFT, CVCL::CDList< T >::push_back(), CVCL::RIGHTSHIFT, CVCL::SBVGE, CVCL::SBVGT, CVCL::SBVLE, CVCL::SBVLT, CVCL::SX, CVCL::Theory::theoryCore(), CVCL::Expr::toString(), and CVCL::TRACE. Referenced by collectSharedSubterms().

void TheoryBitvector::checkSat (  bool  fullEffort  )  [virtual]

Check for satisfiability in the theory. Parameters: fullEffort  when it is false, checkSat can do as much or as little work as it likes, though simple inferences and checks for consistency should be done to increase efficiency. If fullEffort is true, checkSat must check whether the set of facts given by assertFact together with the arrangement of shared terms (provided by addSharedTerm) induced by the global find database equivalence relation are satisfiable. If satisfiable, checkSat does nothing. If satisfiability can be acheived by merging some of the shared terms, a new fact must be enqueued using enqueueFact (this fact need not be a literal). If there is no way to make things satisfiable, setInconsistent must be called. Implements CVCL::Theory. Definition at line 2291 of file theory_bitvector.cpp. References bitBlastDisEqn(), bitBlastEqn(), CVCL::Debug::counter(), d_booleanRWFlag, d_bvTypePreds, d_diseq, d_diseqIdx, d_eq, d_eqBlastIdx, d_eqIdx, d_tccs, d_tccsIdx, CVCL::debugger, CVCL::Theory::enqueueFact(), CVCL::Theory::find(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Expr::getOp(), CVCL::Theorem::getRHS(), IF_DEBUG(), CVCL::Theory::iffMP(), CVCL::Expr::isTrue(), rewriteBoolean(), CVCL::Theory::simplify(), CVCL::CDList< T >::size(), and CVCL::Theory::substitutivityRule().

Theorem TheoryBitvector::rewrite (  const Expr &  e  )  [virtual]

Theory-specific rewrite rules. By default, rewrite just returns a reflexive theorem stating that the input expression is equivalent to itself. However, rewrite is allowed to return any theorem which describes how the input expression is equivalent to some new expression. rewrite should be used to perform simplifications, normalization, and any other preprocessing on theory-specific expressions that needs to be done. Reimplemented from CVCL::Theory. Definition at line 2362 of file theory_bitvector.cpp. References rewriteAux(). Referenced by parseExprOp().

Theorem TheoryBitvector::rewriteAux (  const Expr &  e  )

Definition at line 2367 of file theory_bitvector.cpp. References CVCL::Debug::counter(), CVCL::debugger, CVCL::Theory::find(), CVCL::Expr::hasFind(), IF_DEBUG(), rewriteBV(), rewriteConst(), and CVCL::Theory::transitivityRule(). Referenced by pushNegationRec(), rewrite(), setupExpr(), and update().

Theorem TheoryBitvector::rewriteAtomic (  const Expr &  e  )  [virtual]

Theory-specific rewrites for atomic formulas. The intended use is to convert complex atomic formulas into an equivalent Boolean combination of simpler formulas. Such conversion may be harmful for algebraic rewrites, and is not always desirable to have in rewrite() method. Note: Used only by bitvector theory and rewriteLiteral in core. However, if rewrite() alone cannot solve the problem, and the SAT solver needs to be envoked, these additional rewrites may ease the job for the SAT solver. Reimplemented from CVCL::Theory. Definition at line 2383 of file theory_bitvector.cpp. References bitBlastEqn(), CVCL::BVLE, CVCL::BVLT, d_cnfBitBlastFlag, CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::isEq(), CVCL::Theory::reflexivityRule(), CVCL::Theory::simplify(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::Theory::transitivityRule().

void TheoryBitvector::setup (  const Expr &  e  )  [virtual]

Set up the term e for call-backs when e or its children change. setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update. See also: update Reimplemented from CVCL::Theory. Definition at line 2403 of file theory_bitvector.cpp. References CVCL::Expr::addToNotify(), CVCL::Expr::arity(), CVCL::BVCONST, CVCL::CONCAT, d_setupSharedFlag, CVCL::Expr::getKind(), CVCL::Expr::getOpKind(), CVCL::int2string(), CVCL::Theory::setupCC(), and CVCL::TRACE.

void TheoryBitvector::update (  const Theorem &  e, const Expr &  d )  [virtual]

Notify a theory of a new equality. update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2. To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup. See also: setup Reimplemented from CVCL::Theory. Definition at line 2526 of file theory_bitvector.cpp. References CVCL::BVCONST, CVCL::CONCAT, CVCL::BitvectorProofRules::concatConst(), constantKids(), CVCL::CDMap< Key, Data, HashFcn >::count(), CVCL::Debug::counter(), d_rules, d_sharedSubterms, d_staleDB, CVCL::debugger, CVCL::Theory::enqueueEquality(), CVCL::Theory::enqueueFact(), CVCL::Theory::find(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::hasFind(), IF_DEBUG(), rewriteAux(), CVCL::Expr::setFind(), CVCL::TheoryCore::setupTerm(), CVCL::Theory::symmetryRule(), CVCL::Theory::theoryCore(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::Theory::transitivityRule(), CVCL::Theory::updateCC(), and CVCL::Theory::updateHelper().

Theorem TheoryBitvector::solve (  const Theorem &  e  )  [virtual]

An optional solver. The solve method can be used to implement a Shostak-style solver. Since solvers do not in general combine, the following technique is used. One theory is designated as the primary solver (in our case, it is the theory of arithmetic). For each equation that enters the core framework, the primary solver is called to ensure that the equation is in solved form with respect to the primary theory. After the primary solver, the solver for the theory associated with the equation is called. This solver can do whatever it likes, as long as the result is still in solved form with respect to the primary solver. This is a slight generalization of what is described in my (Clark)'s PhD thesis. Reimplemented from CVCL::Theory. Definition at line 2609 of file theory_bitvector.cpp. References CVCL::BVCONST, d_rules, CVCL::BitvectorProofRules::eqConst(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Theory::iffMP(), and CVCL::Theory::symmetryRule().

void TheoryBitvector::checkType (  const Expr &  e  )  [virtual]

Check that e is a valid Type expr. Reimplemented from CVCL::Theory. Definition at line 2626 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Theory::getEM(), and CVCL::Expr::getOpKind().

void TheoryBitvector::computeType (  const Expr &  e  )  [virtual]

Compute and store the type of e. Parameters: e  is the expression whose type is computed. This function computes the type of the top-level operator of e, and recurses into children using getType(), if necessary. Reimplemented from CVCL::Theory. Definition at line 2639 of file theory_bitvector.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BITVECTOR, CVCL::BOOLEXTRACT, CVCL::Theory::boolType(), CVCL::BVAND, CVCL::BVCONST, CVCL::BVLE, CVCL::BVLT, CVCL::BVMULT, CVCL::BVNEG, CVCL::BVOR, CVCL::BVPLUS, BVSize(), CVCL::BVTYPEPRED, CVCL::BVUMINUS, CVCL::CONCAT, CVCL::Expr::end(), CVCL::EXTRACT, CVCL::Theory::getBaseType(), getBoolExtractIndex(), getBVConstSize(), getBVMultParam(), getBVPlusParam(), CVCL::Type::getExpr(), getExtractHi(), getExtractLow(), getFixedLeftShiftParam(), getFixedRightShiftParam(), CVCL::Expr::getOpKind(), getSXIndex(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::LEFTSHIFT, newBitvectorType(), CVCL::RIGHTSHIFT, CVCL::SBVLE, CVCL::SBVLT, CVCL::Expr::setType(), CVCL::SX, CVCL::Type::toString(), CVCL::Expr::toString(), and CVCL::TRACE.

void TheoryBitvector::computeModelTerm (  const Expr &  e, std::vector< Expr > &  v )  [virtual]

Add variables from 'e' to 'v' for constructing a concrete model. If e is already of primitive type, do NOT add it to v. Reimplemented from CVCL::Theory. Definition at line 2848 of file theory_bitvector.cpp. References CVCL::Expr::begin(), CVCL::BITVECTOR, CVCL::BVAND, CVCL::BVCONST, CVCL::BVGE, CVCL::BVGT, CVCL::BVLE, CVCL::BVLT, CVCL::BVMULT, CVCL::BVNAND, CVCL::BVNEG, CVCL::BVNOR, CVCL::BVOR, CVCL::BVPLUS, CVCL::BVSUB, CVCL::BVTOINT, CVCL::BVUMINUS, CVCL::BVXNOR, CVCL::BVXOR, CVCL::CONCAT, CVCL::Expr::end(), CVCL::EXTRACT, getBitvectorTypeParam(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::HEXBVCONST, CVCL::INTTOBV, CVCL::LEFTSHIFT, newBoolExtractExpr(), CVCL::RIGHTSHIFT, CVCL::SBVGE, CVCL::SBVGT, CVCL::SBVLE, CVCL::SBVLT, and CVCL::VARSHIFT.

void TheoryBitvector::computeModel (  const Expr &  e, std::vector< Expr > &  v )  [virtual]

Compute the value of a compound variable from the more primitive ones. The more primitive variables for e are already assigned concrete values, and are available through getModelValue(). The new value for e must be assigned using assignValue() method. Parameters: e  is the compound type expression to assign a value; vars  are the variables actually assigned. Normally, 'e' is the only element of vars. However, e.g. in the case of uninterpreted functions, assigning 'f' means assigning all relevant applications of 'f' to constant values (f(0), f(5), etc.). Such applications might not be known before the model is constructed (they may be of the form f(x), f(y+z), etc., where x,y,z are still unassigned). Populating 'vars' is an opportunity for a DP to change the set of top-level "variables" to assign, if needed. In particular, it may drop 'e' from the model entirely, if it is already a concrete value by itself. Reimplemented from CVCL::Theory. Definition at line 2900 of file theory_bitvector.cpp. References CVCL::Theory::assignValue(), CVCL::BITVECTOR, CVCL::BVAND, CVCL::BVCONST, CVCL::BVGE, CVCL::BVGT, CVCL::BVLE, CVCL::BVLT, CVCL::BVMULT, CVCL::BVNAND, CVCL::BVNEG, CVCL::BVNOR, CVCL::BVOR, CVCL::BVPLUS, CVCL::BVSUB, CVCL::BVTOINT, CVCL::BVUMINUS, CVCL::BVXNOR, CVCL::BVXOR, CVCL::CONCAT, CVCL::EXTRACT, getBitvectorTypeParam(), CVCL::Theorem::getExpr(), CVCL::Type::getExpr(), CVCL::Theory::getModelValue(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::HEXBVCONST, CVCL::INTTOBV, CVCL::Expr::isBoolConst(), CVCL::Expr::isTrue(), CVCL::LEFTSHIFT, newBoolExtractExpr(), newBVConstExpr(), CVCL::RIGHTSHIFT, CVCL::SBVGE, CVCL::SBVGT, CVCL::SBVLE, CVCL::SBVLT, CVCL::Theory::simplify(), CVCL::SX, CVCL::Expr::toString(), and CVCL::VARSHIFT.

Expr TheoryBitvector::computeTypePred (  const Type &  t, const Expr &  e )  [virtual]

Theory specific computation of the subtyping predicate for type t applied to the expression e. By default returns true. Each theory needs to compute subtype predicates for the types associated with it. So, for example, the theory of records will take a record type [# f1: T1, f2: T2 #] and an expression e and will return the subtyping predicate for e, namely: computeTypePred(T1, e.f1) AND computeTypePred(T2, e.f2) Reimplemented from CVCL::Theory. Definition at line 2968 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), newBitvectorTypePred(), and CVCL::Type::toString().

Expr TheoryBitvector::computeTCC (  const Expr &  e  )  [virtual]

Compute and cache the TCC of e. Parameters: e  is an expression (term or formula). This function computes the TCC of e which is true iff the expression is defined. This function computes the TCC or predicate of the top-level operator of e, and recurses into children using getTCC(), if necessary. The default implementation is to compute TCCs recursively for all children, and return their conjunction. Reimplemented from CVCL::Theory. Definition at line 2981 of file theory_bitvector.cpp. References CVCL::Theory::computeTCC().

ExprStream & TheoryBitvector::print (  ExprStream &  os, const Expr &  e )  [virtual]

Theory-specific pretty-printing. By default, print the top node in AST, and resume pretty-printing the children. The same call e.print(os) can be used in DP-specific printers to use AST printing for the given node. In fact, it is strongly recommended to add e.print(os) as the default for all the cases/kinds that are not handled by the particular pretty-printer. Reimplemented from CVCL::Theory. Definition at line 2994 of file theory_bitvector.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BITVECTOR, CVCL::BOOLEXTRACT, CVCL::BVAND, CVCL::BVCONST, CVCL::BVLE, CVCL::BVLT, CVCL::BVMULT, CVCL::BVNEG, CVCL::BVOR, CVCL::BVPLUS, CVCL::BVSUB, CVCL::BVTOINT, CVCL::BVTYPEPRED, CVCL::BVUMINUS, CVCL::CONCAT, CVCL::Theory::d_theoryUsed, CVCL::Expr::end(), CVCL::EXTRACT, getBitvectorTypeParam(), getBoolExtractIndex(), getBVConstSize(), getBVConstValue(), getBVMultParam(), getBVPlusParam(), CVCL::Op::getExpr(), getExtractHi(), getExtractLow(), getFixedLeftShiftParam(), getFixedRightShiftParam(), CVCL::Expr::getOp(), CVCL::Expr::getOpKind(), getSXIndex(), CVCL::INTTOBV, CVCL::Expr::isApply(), CVCL::ExprStream::lang(), CVCL::LEFTSHIFT, CVCL::pop(), CVCL::PRESENTATION_LANG, CVCL::Expr::printAST(), CVCL::push(), CVCL::RIGHTSHIFT, CVCL::SBVLE, CVCL::SBVLT, CVCL::SMTLIB_LANG, CVCL::space(), and CVCL::SX.

Expr TheoryBitvector::parseExprOp (  const Expr &  e  )  [virtual]

Theory-specific parsing implemented by the DP. Reimplemented from CVCL::Theory. Definition at line 3144 of file theory_bitvector.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BITVECTOR, CVCL::BOOLEXTRACT, CVCL::BVAND, CVCL::BVCONST, CVCL::BVGE, CVCL::BVGT, CVCL::BVLE, CVCL::BVLT, CVCL::BVMULT, CVCL::BVNAND, CVCL::BVNEG, CVCL::BVNOR, CVCL::BVOR, CVCL::BVPLUS, CVCL::BVSUB, CVCL::BVUMINUS, CVCL::BVXNOR, CVCL::BVXOR, CVCL::CONCAT, CVCL::Expr::end(), CVCL::EXTRACT, CVCL::Theory::getEM(), CVCL::Rational::getInt(), CVCL::ExprManager::getKind(), CVCL::Expr::getKind(), CVCL::Expr::getRational(), CVCL::Theorem::getRHS(), CVCL::Expr::getString(), CVCL::HEXBVCONST, CVCL::int2string(), CVCL::Rational::isInteger(), CVCL::Expr::isRational(), CVCL::Expr::isString(), CVCL::LEFTSHIFT, newBitvectorTypeExpr(), newBoolExtractExpr(), newBVAndExpr(), newBVConstExpr(), newBVExtractExpr(), newBVLEExpr(), newBVLTExpr(), newBVMultExpr(), newBVNegExpr(), newBVOrExpr(), newBVPlusExpr(), newBVUminusExpr(), newConcatExpr(), newFixedLeftShiftExpr(), newFixedRightShiftExpr(), newSBVLEExpr(), newSBVLTExpr(), newSXExpr(), pad(), CVCL::Theory::parseExpr(), CVCL::RAW_LIST, rewrite(), rewriteBV(), CVCL::RIGHTSHIFT, CVCL::SBVGE, CVCL::SBVGT, CVCL::SBVLE, CVCL::SBVLT, CVCL::SX, CVCL::Expr::toString(), and CVCL::TRACE.

Expr CVCL::TheoryBitvector::rat (  const Rational &  r  )  [inline]

Definition at line 286 of file theory_bitvector.h. References CVCL::Theory::getEM(), and CVCL::ExprManager::newRatExpr().

Expr TheoryBitvector::pad (  int  len, const Expr &  e )

pads e to be of length len Parameters: len  is the desired length of the resulting bitvector e  is the original bitvector of arbitrary length Definition at line 4026 of file theory_bitvector.cpp. References CVCL::BITVECTOR, BVSize(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), newBVExtractExpr(), newBVZeroString(), newConcatExpr(), and CVCL::Expr::toString(). Referenced by newBVConstExpr(), and parseExprOp().

int TheoryBitvector::BVSize (  const Expr &  e  )

Return the number of bits in the bitvector expression. Definition at line 53 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Theory::getBaseType(), getBitvectorTypeParam(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), and CVCL::Expr::toString(). Referenced by assertFact(), bitBlastDisEqn(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), bitBlastEqn(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitExtractExtraction(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bitExtractNot(), CVCL::BitvectorTheoremProducer::bitExtractRewrite(), CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvMultAssocRule(), CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), CVCL::BitvectorTheoremProducer::bvuminusBVMult(), CVCL::BitvectorTheoremProducer::bvuminusToBVPlus(), CVCL::BitvectorTheoremProducer::bvuminusVar(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), computeType(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::extractWhole(), CVCL::BitvectorTheoremProducer::flattenBVPlus(), CVCL::BitvectorTheoremProducer::flipBVMult(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::BitvectorTheoremProducer::iteExtractRule(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), newBVAndExpr(), newBVNandExpr(), newBVNorExpr(), newBVOrExpr(), newBVXnorExpr(), newBVXorExpr(), normalizeConcat(), CVCL::BitvectorTheoremProducer::oneCoeffBVMult(), pad(), CVCL::BitvectorTheoremProducer::pad(), CVCL::BitvectorTheoremProducer::padBVMult(), CVCL::BitvectorTheoremProducer::padBVPlus(), rewriteBV(), CVCL::BitvectorTheoremProducer::rightShiftToConcat(), setupExpr(), CVCL::BitvectorTheoremProducer::signBVLTRule(), CVCL::BitvectorTheoremProducer::signExtendRule(), CVCL::BitvectorTheoremProducer::typePredBit(), CVCL::BitvectorTheoremProducer::zeroCoeffBVMult(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

Type CVCL::TheoryBitvector::newBitvectorType (  int  i  )  [inline]

Definition at line 294 of file theory_bitvector.h. References newBitvectorTypeExpr(). Referenced by computeType().

Expr TheoryBitvector::newBitvectorTypePred (  const Type &  t, const Expr &  e )

Definition at line 3525 of file theory_bitvector.cpp. References CVCL::BVTYPEPRED, and CVCL::Type::getExpr(). Referenced by computeTypePred().

Expr TheoryBitvector::newBitvectorTypeExpr (  int  i  )

Definition at line 3517 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Theory::getEM(), and CVCL::int2string(). Referenced by newBitvectorType(), and parseExprOp().

Expr TheoryBitvector::newBVAndExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3530 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVAND, BVSize(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::negBVor(), and parseExprOp().

Expr CVCL::TheoryBitvector::newBVAndExpr (  const std::vector< Expr > &  kids  )

Expr TheoryBitvector::newBVNandExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3595 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVNAND, BVSize(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString().

Expr CVCL::TheoryBitvector::newBVNandExpr (  const std::vector< Expr > &  kids  )

Expr TheoryBitvector::newBVOrExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3562 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVOR, BVSize(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::negBVand(), and parseExprOp().

Expr CVCL::TheoryBitvector::newBVOrExpr (  const std::vector< Expr > &  kids  )

Expr TheoryBitvector::newBVNorExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3627 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVNOR, BVSize(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString().

Expr CVCL::TheoryBitvector::newBVNorExpr (  const std::vector< Expr > &  kids  )

Expr TheoryBitvector::newBVXorExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3659 of file theory_bitvector.cpp. References CVCL::BITVECTOR, BVSize(), CVCL::BVXOR, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString().

Expr CVCL::TheoryBitvector::newBVXorExpr (  const std::vector< Expr > &  kids  )

Expr TheoryBitvector::newBVXnorExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3691 of file theory_bitvector.cpp. References CVCL::BITVECTOR, BVSize(), CVCL::BVXNOR, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString().

Expr CVCL::TheoryBitvector::newBVXnorExpr (  const std::vector< Expr > &  kids  )

Expr TheoryBitvector::newBVLTExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3723 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVLT, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::BitvectorTheoremProducer::notBVLTRule(), CVCL::BitvectorTheoremProducer::padBVLTRule(), parseExprOp(), and CVCL::BitvectorTheoremProducer::signBVLTRule().

Expr TheoryBitvector::newBVLEExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3732 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVLE, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::BitvectorTheoremProducer::notBVLTRule(), CVCL::BitvectorTheoremProducer::padBVLTRule(), parseExprOp(), and CVCL::BitvectorTheoremProducer::signBVLTRule().

Expr TheoryBitvector::newSXExpr (  const Expr &  t1, int  len )

Definition at line 3741 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Theory::getEM(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::SX, and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::padSBVLTRule(), and parseExprOp().

Expr TheoryBitvector::newSBVLTExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3754 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::SBVLT, and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::padSBVLTRule(), and parseExprOp().

Expr TheoryBitvector::newSBVLEExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3763 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::SBVLE, and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::padSBVLTRule(), and parseExprOp().

Expr TheoryBitvector::newBVNegExpr (  const Expr &  t1  )

Definition at line 3772 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVNEG, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bvuminusToBVPlus(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::BitvectorTheoremProducer::iteBVnegRule(), CVCL::BitvectorTheoremProducer::negBVand(), CVCL::BitvectorTheoremProducer::negBVor(), CVCL::BitvectorTheoremProducer::negConcat(), parseExprOp(), pushNegationRec(), and CVCL::BitvectorTheoremProducer::sameKidCheck().

Expr TheoryBitvector::newBVUminusExpr (  const Expr &  t1  )

Definition at line 3781 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVUMINUS, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), and parseExprOp().

Expr TheoryBitvector::newBoolExtractExpr (  const Expr &  t1, int  r )

Definition at line 3789 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BOOLEXTRACT, CVCL::Theory::getEM(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), and CVCL::Expr::toString(). Referenced by bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractBVPlus(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), CVCL::BitvectorTheoremProducer::bitExtractConstant(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitExtractExtraction(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bitExtractNot(), CVCL::BitvectorTheoremProducer::bitExtractRewrite(), CVCL::BitvectorTheoremProducer::bitExtractSXRule(), computeModel(), computeModelTerm(), parseExprOp(), rewriteBV(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

Expr TheoryBitvector::newFixedLeftShiftExpr (  const Expr &  t1, int  r )

Definition at line 3829 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Theory::getEM(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::LEFTSHIFT, and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::constMultToPlus(), and parseExprOp().

Expr TheoryBitvector::newFixedRightShiftExpr (  const Expr &  t1, int  r )

Definition at line 3842 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Theory::getEM(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), CVCL::RIGHTSHIFT, and CVCL::Expr::toString(). Referenced by parseExprOp().

Expr TheoryBitvector::newConcatExpr (  const Expr &  t1, const Expr &  t2 )

Definition at line 3855 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::CONCAT, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::leftShiftToConcat(), CVCL::BitvectorTheoremProducer::negConcat(), normalizeConcat(), pad(), CVCL::BitvectorTheoremProducer::pad(), parseExprOp(), CVCL::BitvectorTheoremProducer::rightShiftToConcat(), setupExpr(), and CVCL::BitvectorTheoremProducer::signExtendRule().

Expr TheoryBitvector::newConcatExpr (  const Expr &  t1, const Expr &  t2, const Expr &  t3 )

Definition at line 3864 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::CONCAT, CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), and CVCL::Expr::toString().

Expr CVCL::TheoryBitvector::newConcatExpr (  const std::vector< Expr > &  kids  )

Expr TheoryBitvector::newBVConstExpr (  const std::string &  s, int  base = 2 )

Definition at line 3965 of file theory_bitvector.cpp. References d_bvConstExprIndex, CVCL::Theory::getEM(), CVCL::int2string(), and CVCL::ExprManager::newExpr(). Referenced by CVCL::BitvectorTheoremProducer::BitvectorTheoremProducer(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), CVCL::BitvectorTheoremProducer::bvuminusBVMult(), CVCL::BitvectorTheoremProducer::bvuminusToBVPlus(), CVCL::BitvectorTheoremProducer::bvuminusVar(), computeModel(), CVCL::BitvectorTheoremProducer::concatConst(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::BitvectorTheoremProducer::extractConst(), CVCL::BitvectorTheoremProducer::leftShiftToConcat(), CVCL::BitvectorTheoremProducer::negConst(), newBVConstExpr(), newBVOneString(), newBVZeroString(), parseExprOp(), and TheoryBitvector().

Expr CVCL::TheoryBitvector::newBVConstExpr (  const std::vector< bool > &  bits  )

Expr TheoryBitvector::newBVConstExpr (  const Rational &  r, int  len = 0 )

Definition at line 3936 of file theory_bitvector.cpp. References CVCL::int2string(), CVCL::Rational::isInteger(), newBVConstExpr(), pad(), and CVCL::Rational::toString().

Expr TheoryBitvector::newBVZeroString (  int  r  )

produces a string of 0's of length bvLength Definition at line 3905 of file theory_bitvector.cpp. References CVCL::int2string(), and newBVConstExpr(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvuminusBVMult(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), pad(), CVCL::BitvectorTheoremProducer::pad(), CVCL::BitvectorTheoremProducer::rightShiftToConcat(), CVCL::BitvectorTheoremProducer::sumNormalizedElements(), and CVCL::BitvectorTheoremProducer::zeroCoeffBVMult().

Expr TheoryBitvector::newBVOneString (  int  r  )

produces a string of 1's of length bvLength Definition at line 3917 of file theory_bitvector.cpp. References CVCL::int2string(), and newBVConstExpr(). Referenced by CVCL::BitvectorTheoremProducer::bitwiseFlatten().

Expr TheoryBitvector::newBVExtractExpr (  const Expr &  e, int  hi, int  low )

hi and low are bit indices Definition at line 3986 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::EXTRACT, CVCL::Theory::getEM(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractRewrite(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::concatMergeExtract(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::extractExtract(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::BitvectorTheoremProducer::iteExtractRule(), pad(), CVCL::BitvectorTheoremProducer::pad(), parseExprOp(), rewriteBV(), CVCL::BitvectorTheoremProducer::rightShiftToConcat(), setupExpr(), CVCL::BitvectorTheoremProducer::signBVLTRule(), and CVCL::BitvectorTheoremProducer::signExtendRule().

Expr TheoryBitvector::newBVPlusExpr (  int  numbits, const std::vector< Expr > &  k )

'numbits' is the number of bits in the result Definition at line 4002 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVPLUS, CVCL::Theory::getEM(), and CVCL::int2string(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::BitvectorTheoremProducer::bvuminusToBVPlus(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::BitvectorTheoremProducer::flattenBVPlus(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::BitvectorTheoremProducer::padBVPlus(), parseExprOp(), and CVCL::BitvectorTheoremProducer::sumNormalizedElements().

Expr TheoryBitvector::newBVMultExpr (  int  bvLength, const Expr &  t1, const Expr &  t2 )

accepts an integer, r, and bitvector, t1, and returns r.t1 Definition at line 3890 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::BVMULT, CVCL::Theory::getEM(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::int2string(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvMultAssocRule(), CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvuminusBVMult(), CVCL::BitvectorTheoremProducer::bvuminusVar(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::flipBVMult(), CVCL::BitvectorTheoremProducer::padBVMult(), CVCL::BitvectorTheoremProducer::padBVPlus(), and parseExprOp().

int TheoryBitvector::getBitvectorTypeParam (  const Expr &  e  )

Definition at line 4051 of file theory_bitvector.cpp. References CVCL::BITVECTOR, CVCL::Rational::getInt(), CVCL::Expr::getKind(), CVCL::Expr::getRational(), and CVCL::Expr::toString(). Referenced by BVSize(), computeModel(), computeModelTerm(), CVCL::BitvectorTheoremProducer::expandTypePred(), getBitvectorTypeParam(), and print().

int CVCL::TheoryBitvector::getBitvectorTypeParam (  const Type &  t  )  [inline]

Definition at line 345 of file theory_bitvector.h. References getBitvectorTypeParam(), and CVCL::Type::getExpr().

Type TheoryBitvector::getTypePredType (  const Expr &  tp  )

Definition at line 4059 of file theory_bitvector.cpp. References CVCL::BVTYPEPRED, CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::expandTypePred().

const Expr & TheoryBitvector::getTypePredExpr (  const Expr &  tp  )

Definition at line 4066 of file theory_bitvector.cpp. References CVCL::BVTYPEPRED, CVCL::Expr::getOpKind(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::expandTypePred().

int TheoryBitvector::getSXIndex (  const Expr &  e  )

Definition at line 4079 of file theory_bitvector.cpp. References CVCL::Rational::getInt(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Expr::isApply(), CVCL::SX, and CVCL::Expr::toString(). Referenced by computeType(), and print().

int TheoryBitvector::getBoolExtractIndex (  const Expr &  e  )

Definition at line 4072 of file theory_bitvector.cpp. References CVCL::BOOLEXTRACT, CVCL::Rational::getInt(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Expr::isApply(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bitExtractRewrite(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitvectorFalseRule(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), computeType(), CVCL::BitvectorTheoremProducer::generalIneqn(), print(), rewriteBV(), and rewriteConst().

int TheoryBitvector::getFixedLeftShiftParam (  const Expr &  e  )

Definition at line 4085 of file theory_bitvector.cpp. References CVCL::Rational::getInt(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Expr::isApply(), CVCL::LEFTSHIFT, and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), computeType(), CVCL::BitvectorTheoremProducer::leftShiftToConcat(), and print().

int TheoryBitvector::getFixedRightShiftParam (  const Expr &  e  )

Definition at line 4093 of file theory_bitvector.cpp. References CVCL::Rational::getInt(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Expr::isApply(), CVCL::RIGHTSHIFT, and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), computeType(), print(), and CVCL::BitvectorTheoremProducer::rightShiftToConcat().

int TheoryBitvector::getExtractHi (  const Expr &  e  )

Definition at line 4107 of file theory_bitvector.cpp. References CVCL::EXTRACT, CVCL::Rational::getInt(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Expr::isApply(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractExtraction(), computeType(), CVCL::BitvectorTheoremProducer::concatMergeExtract(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::extractConst(), CVCL::BitvectorTheoremProducer::extractExtract(), CVCL::BitvectorTheoremProducer::extractWhole(), CVCL::BitvectorTheoremProducer::iteExtractRule(), normalizeConcat(), print(), and rewriteBV().

int TheoryBitvector::getExtractLow (  const Expr &  e  )

Definition at line 4100 of file theory_bitvector.cpp. References CVCL::EXTRACT, CVCL::Rational::getInt(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Expr::isApply(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractExtraction(), computeType(), CVCL::BitvectorTheoremProducer::concatMergeExtract(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::extractConst(), CVCL::BitvectorTheoremProducer::extractExtract(), CVCL::BitvectorTheoremProducer::extractWhole(), CVCL::BitvectorTheoremProducer::iteExtractRule(), normalizeConcat(), print(), and rewriteBV().

int TheoryBitvector::getBVPlusParam (  const Expr &  e  )

Definition at line 4114 of file theory_bitvector.cpp. References CVCL::BVPLUS, CVCL::Rational::getInt(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Expr::isApply(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractBVPlus(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), computeType(), and print().

int TheoryBitvector::getBVMultParam (  const Expr &  e  )

Definition at line 4122 of file theory_bitvector.cpp. References CVCL::AST_LANG, CVCL::BVMULT, CVCL::Rational::getInt(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Expr::isApply(), and CVCL::Expr::toString(). Referenced by computeType(), and print().

unsigned CVCL::TheoryBitvector::getBVConstSize (  const Expr &  e  )

Definition at line 4179 of file theory_bitvector.cpp. References CVCL::BVCONST, CVCL::Expr::getExprValue(), CVCL::Expr::getKind(), and CVCL::BVConstExpr::size(). Referenced by CVCL::BitvectorTheoremProducer::bitwiseConst(), computeBVConst(), computeNegBVConst(), computeType(), CVCL::BitvectorTheoremProducer::concatConst(), CVCL::BitvectorTheoremProducer::negConst(), normalizeConcat(), CVCL::BitvectorTheoremProducer::orOne(), and print().

bool CVCL::TheoryBitvector::getBVConstValue (  const Expr &  e, int  i )

Definition at line 4187 of file theory_bitvector.cpp. References CVCL::BVCONST, CVCL::Expr::getExprValue(), CVCL::Expr::getKind(), and CVCL::BVConstExpr::getValue(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractConstant(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitwiseConst(), computeBVConst(), computeNegBVConst(), CVCL::BitvectorTheoremProducer::concatConst(), CVCL::BitvectorTheoremProducer::extractConst(), CVCL::BitvectorTheoremProducer::negConst(), normalizeConcat(), CVCL::BitvectorTheoremProducer::orOne(), and print().

Rational CVCL::TheoryBitvector::computeBVConst (  const Expr &  e  )

computes the integer value of a bitvector constant Definition at line 4196 of file theory_bitvector.cpp. References CVCL::BVCONST, getBVConstSize(), getBVConstValue(), CVCL::Expr::getKind(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::andZero(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), CVCL::BitvectorTheoremProducer::collectLikeTermsOfPlus(), normalizeBVArith(), normalizeConcat(), CVCL::BitvectorTheoremProducer::oneCoeffBVMult(), CVCL::BitvectorTheoremProducer::signBVLTRule(), simplifyOp(), and CVCL::BitvectorTheoremProducer::zeroCoeffBVMult().

Rational CVCL::TheoryBitvector::computeNegBVConst (  const Expr &  e  )

computes the integer value of ~c+1 or BVUMINUS(c) Definition at line 4218 of file theory_bitvector.cpp. References CVCL::BVCONST, getBVConstSize(), getBVConstValue(), CVCL::Expr::getKind(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), and CVCL::BitvectorTheoremProducer::bvuminusBVMult().

---

Member Data Documentation

BitvectorProofRules* CVCL::TheoryBitvector::d_rules [private]

Definition at line 92 of file theory_bitvector.h. Referenced by assertFact(), bitBlastDisEqn(), bitBlastEqn(), bitBlastTerm(), combineLikeTerms(), flattenBVPlus(), normalizeBVArith(), normalizeConcat(), padBVPlus(), pushNegationRec(), rewriteBV(), rewriteConst(), setupExpr(), signExtendBVLT(), simplifyOp(), solve(), TheoryBitvector(), update(), and ~TheoryBitvector().

size_t CVCL::TheoryBitvector::d_bvConstExprIndex [private]

MemoryManager index for BVConstExpr subclass. Definition at line 94 of file theory_bitvector.h. Referenced by newBVConstExpr(), and TheoryBitvector().

size_t CVCL::TheoryBitvector::d_bvPlusExprIndex [private]

Definition at line 95 of file theory_bitvector.h.

size_t CVCL::TheoryBitvector::d_bvParameterExprIndex [private]

Definition at line 96 of file theory_bitvector.h.

size_t CVCL::TheoryBitvector::d_bvTypePredExprIndex [private]

Definition at line 97 of file theory_bitvector.h.

StatCounter CVCL::TheoryBitvector::d_bvDelayEq [private]

counts delayed asserted equalities Definition at line 100 of file theory_bitvector.h. Referenced by assertFact().

StatCounter CVCL::TheoryBitvector::d_bvAssertEq [private]

counts asserted equalities Definition at line 102 of file theory_bitvector.h. Referenced by assertFact().

StatCounter CVCL::TheoryBitvector::d_bvDelayDiseq [private]

counts delayed asserted disequalities Definition at line 104 of file theory_bitvector.h. Referenced by assertFact().

StatCounter CVCL::TheoryBitvector::d_bvAssertDiseq [private]

counts asserted disequalities Definition at line 106 of file theory_bitvector.h. Referenced by assertFact().

StatCounter CVCL::TheoryBitvector::d_bvTypePreds [private]

counts type predicates Definition at line 108 of file theory_bitvector.h. Referenced by assertTypePred(), and checkSat().

StatCounter CVCL::TheoryBitvector::d_bvDelayTypePreds [private]

counts delayed type predicates Definition at line 110 of file theory_bitvector.h. Referenced by assertTypePred().

StatCounter CVCL::TheoryBitvector::d_bvBitBlastEq [private]

counts bitblasted equalities Definition at line 112 of file theory_bitvector.h. Referenced by bitBlastEqn().

StatCounter CVCL::TheoryBitvector::d_bvBitBlastDiseq [private]

counts bitblasted disequalities Definition at line 114 of file theory_bitvector.h. Referenced by bitBlastDisEqn().

const bool* CVCL::TheoryBitvector::d_simplifyFlag [private]

Command line flag: simplify bit-blasted expressions before enqueuing. Definition at line 118 of file theory_bitvector.h.

const bool* CVCL::TheoryBitvector::d_booleanRWFlag [private]

boolean on the fly rewrite flag Definition at line 120 of file theory_bitvector.h. Referenced by assertFact(), checkSat(), and rewriteBoolean().

const bool* CVCL::TheoryBitvector::d_boolExtractCacheFlag [private]

bool extract cache flag Definition at line 122 of file theory_bitvector.h.

const bool* CVCL::TheoryBitvector::d_bv32Flag [private]

flag which indicates that all arithmetic is 32 bit with no overflow Definition at line 124 of file theory_bitvector.h.

const bool* CVCL::TheoryBitvector::d_rewriteFlag [private]

Command line flag: rewrite bitvector expressions. Definition at line 126 of file theory_bitvector.h.

const bool* CVCL::TheoryBitvector::d_concatRewriteFlag [private]

Command line flag: concatenation normal form rewrite bitvector expressions. Definition at line 128 of file theory_bitvector.h.

const bool* CVCL::TheoryBitvector::d_bvplusRewriteFlag [private]

Command line flag: bvplus normal form rewrite bitvector expressions. Definition at line 130 of file theory_bitvector.h.

const bool* CVCL::TheoryBitvector::d_rwBitBlastFlag [private]

Commant line flag: rewrite while bit-blasting. Definition at line 132 of file theory_bitvector.h.

const bool* CVCL::TheoryBitvector::d_cnfBitBlastFlag [private]

Commant line flag: bit-blast equalities in CNF converter. Definition at line 134 of file theory_bitvector.h. Referenced by rewriteAtomic().

const bool* CVCL::TheoryBitvector::d_lhsMinusRhsFlag [private]

Command line flag: enable lhs-minus-rhs-rule for lhs=rhs. Definition at line 136 of file theory_bitvector.h. Referenced by rewriteBV().

const bool* CVCL::TheoryBitvector::d_updateFlag [private]

Command line flag: update bitvector expressions on find pointer merges. Definition at line 138 of file theory_bitvector.h. Referenced by assertTypePred().

const bool* CVCL::TheoryBitvector::d_setupFlag [private]

Command line flag: setup bitvector expressions for single bit changes. Definition at line 140 of file theory_bitvector.h. Referenced by assertTypePred().

const bool* CVCL::TheoryBitvector::d_setupSharedFlag [private]

Command line flag: setup only shared subexpressions. Definition at line 142 of file theory_bitvector.h. Referenced by setup().

const bool* CVCL::TheoryBitvector::d_pushNegationFlag [private]

Command line flag: enable pushnegation. Definition at line 144 of file theory_bitvector.h.

CDMap<Expr,Theorem> CVCL::TheoryBitvector::d_bitvecCache [private]

Cache for storing the results of the bitBlastTerm function. Definition at line 147 of file theory_bitvector.h. Referenced by bitBlastTerm().

ExprMap<Theorem> CVCL::TheoryBitvector::d_pushNegCache [private]

Cache for pushNegation(). it is ok that this is cache is. Definition at line 152 of file theory_bitvector.h. Referenced by pushNegation(), and pushNegationRec().

CDList<Theorem> CVCL::TheoryBitvector::d_eq [private]

Backtracking queue for equalities (to delay them till checkSat() call). Definition at line 155 of file theory_bitvector.h. Referenced by assertFact(), and checkSat().

CDO<size_t> CVCL::TheoryBitvector::d_eqIdx [private]

Pointer to the next unasserted equality in d_eq. Definition at line 157 of file theory_bitvector.h. Referenced by checkSat().

CDO<size_t> CVCL::TheoryBitvector::d_eqBlastIdx [private]

Pointer to the next equality in d_eq which is not bit-blasted yet. Definition at line 159 of file theory_bitvector.h. Referenced by checkSat().

CDList<Theorem> CVCL::TheoryBitvector::d_diseq [private]

Backtracking queue for disequalities (to delay them till checkSat() call). Definition at line 161 of file theory_bitvector.h. Referenced by assertFact(), and checkSat().

CDO<size_t> CVCL::TheoryBitvector::d_diseqIdx [private]

Pointer to the next unasserted disequality in d_diseq. Definition at line 163 of file theory_bitvector.h. Referenced by checkSat().

CDMap<Expr,bool> CVCL::TheoryBitvector::d_staleDB [private]

Database of stale bit-expansions for update(). Definition at line 165 of file theory_bitvector.h. Referenced by update().

CDList<Theorem> CVCL::TheoryBitvector::d_tccs [private]

Backtracking queue for TCCs on individual bits. Definition at line 167 of file theory_bitvector.h. Referenced by assertTypePred(), and checkSat().

CDO<size_t> CVCL::TheoryBitvector::d_tccsIdx [private]

Pointer to the next unasserted TCC in d_tccs. Definition at line 169 of file theory_bitvector.h. Referenced by checkSat().

CDMap<Expr,bool> CVCL::TheoryBitvector::d_sharedSubterms [private]

Backtracking database of subterms of shared terms. Definition at line 171 of file theory_bitvector.h. Referenced by assertTypePred(), collectSharedSubterms(), and update().

CDMap<Expr, Theorem> CVCL::TheoryBitvector::d_typePredsCache [private]

Cache for typePredicates of non shared terms. Definition at line 173 of file theory_bitvector.h. Referenced by assertTypePred(), and collectSharedSubterms().

Expr CVCL::TheoryBitvector::d_bvZero [private]

Constant 1-bit bit-vector 0bin0. Definition at line 178 of file theory_bitvector.h. Referenced by bvZero(), and TheoryBitvector().

Expr CVCL::TheoryBitvector::d_bvOne [private]

Constant 1-bit bit-vector 0bin0. Definition at line 180 of file theory_bitvector.h. Referenced by bvOne(), and TheoryBitvector().

ExprMap<Expr> CVCL::TheoryBitvector::d_bvPlusCarryCacheLeftBV

Definition at line 257 of file theory_bitvector.h. Referenced by bitBlastDisEqn(), bitBlastEqn(), and CVCL::BitvectorTheoremProducer::computeCarryPreComputed().

ExprMap<Expr> CVCL::TheoryBitvector::d_bvPlusCarryCacheRightBV

Definition at line 258 of file theory_bitvector.h. Referenced by bitBlastDisEqn(), bitBlastEqn(), and CVCL::BitvectorTheoremProducer::computeCarryPreComputed().

---

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

• theory_bitvector.h
• bitvector_theorem_producer.cpp
• theory_bitvector.cpp

---