21 #ifndef _cvc3__include__theory_bitvector_h_
22 #define _cvc3__include__theory_bitvector_h_
30 class BitvectorProofRules;
233 int min(std::vector<Rational> list);
286 bool enumerate,
bool computeSize);
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
CDList< Expr > d_sharedSubtermsList
Backtracking database of subterms of shared terms.
int check_linear(const Expr &e)
int getFixedRightShiftParam(const Expr &e)
Expr newBVSLTExpr(const Expr &t1, const Expr &t2)
Data structure of expressions in CVC3.
BitvectorProofRules * d_rules
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Theorem rewriteBV(const Theorem &t, ExprMap< Theorem > &cache, int n=1)
StatCounter d_bvBitBlastEq
counts bitblasted equalities
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Expr newBVXnorExpr(const Expr &t1, const Expr &t2)
ExprStream & printSmtLibShared(ExprStream &os, const Expr &e)
Expr multiply_coeff(Rational mult_inv, const Expr &e)
Expr newBVExtractExpr(const Expr &e, int hi, int low)
hi and low are bit indices
TheoryBitvector(TheoryCore *core)
int d_maxLength
Max size of any bitvector we've seen.
Expr newBVUDivExpr(const Expr &t1, const Expr &t2)
StatCounter d_bvAssertDiseq
counts asserted disequalities
CDMap< Expr, Theorem > d_bitvecCache
Cache for storing the results of the bitBlastTerm function.
CDO< unsigned int > d_bb_index
Index to current position in d_bitblast.
const Expr & getTypePredExpr(const Expr &tp)
Expr newBVIndexExpr(int kind, const Expr &t1, int len)
StatCounter d_bvDelayEq
counts delayed asserted equalities
int getExtractHi(const Expr &e)
Expr newBVSLEExpr(const Expr &t1, const Expr &t2)
Expr newBVNorExpr(const Expr &t1, const Expr &t2)
Theorem pushNegationRec(const Expr &e)
MS C++ specific settings.
Type newBitvectorType(int i)
bool canSolveFor(const Expr &term, const Expr &e)
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
Expr newBVOneString(int r)
produces a string of 1's of length bvLength
Expr newConcatExpr(const Expr &t1, const Expr &t2)
Type getTypePredType(const Expr &tp)
bool isTermIn(const Expr &e1, const Expr &e2)
Expr newSXExpr(const Expr &t1, int len)
Expr newBitvectorTypeExpr(int i)
int getBVPlusParam(const Expr &e)
Expr newBitvectorTypePred(const Type &t, const Expr &e)
int countTermIn(const Expr &term, const Expr &e)
int getSXIndex(const Expr &e)
Theorem simplifyPendingEq(const Theorem &thm, int maxEffort)
CDO< unsigned int > d_eq_index
Index to current position in d_eqPending.
size_t d_bvParameterExprIndex
Description: Counters and flags for collecting run-time statistics.
Expr newFixedLeftShiftExpr(const Expr &t1, int r)
size_t d_bvConstExprIndex
MemoryManager index for BVConstExpr subclass.
StatCounter d_bvBitBlastDiseq
counts bitblasted disequalities
const Expr & bvOne() const
Return cached constant 0bin1.
Expr newBVSDivExpr(const Expr &t1, const Expr &t2)
Expr signed_newBVConstExpr(Rational c, int bv_size)
Theorem updateSubterms(const Expr &d)
Expr newBVOrExpr(const Expr &t1, const Expr &t2)
CDList< Theorem > d_eqPending
Backtracking queue for unsolved equalities.
Expr newBVNegExpr(const Expr &t1)
const bool * d_boolExtractCacheFlag
bool extract cache flag
const Expr & getExpr() const
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
void checkType(const Expr &e)
Check that e is a valid Type expr.
int getBitvectorTypeParam(const Expr &e)
Theorem generalBitBlast(const Theorem &thm)
Theorem pushNegation(const Expr &e)
virtual Theorem simplifyOp(const Expr &e)
Top down simplifier.
ExprMap< Theorem > d_pushNegCache
Cache for pushNegation(). it is ok that this is cache is.
Expr newBVConstExpr(const std::string &s, int base=2)
Theorem rewriteBV(const Theorem &t, int n=1)
Expr newBVURemExpr(const Expr &t1, const Expr &t2)
CDMap< Expr, Expr > d_sharedSubterms
Backtracking database of subterms of shared terms.
Expr newBVMultExpr(int bvLength, const Expr &t1, const Expr &t2)
Expr newFixedConstWidthLeftShiftExpr(const Expr &t1, int r)
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Expr d_bvOne
Constant 1-bit bit-vector 0bin0.
Expr newBVLEExpr(const Expr &t1, const Expr &t2)
StatCounter d_bvDelayDiseq
counts delayed asserted disequalities
Expr newBVLTExpr(const Expr &t1, const Expr &t2)
StatCounter d_bvTypePreds
counts type predicates
ExprMap< Expr > d_bvPlusCarryCacheRightBV
Theorem solve(const Theorem &e)
An optional solver.
BitvectorProofRules * createProofRules()
Rational multiplicative_inverse(Rational r, int n_bits)
Expr newBVNandExpr(const Expr &t1, const Expr &t2)
Expr newBVUminusExpr(const Expr &t1)
Expr newBVPlusPadExpr(int bvLength, const std::vector< Expr > &k)
pads children and then builds plus expr
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
int getBVIndex(const Expr &e)
Expr newBVSubExpr(const Expr &t1, const Expr &t2)
const Expr & getRHS() const
const bool * d_bv32Flag
flag which indicates that all arithmetic is 32 bit with no overflow
Theorem bitBlastIneqn(const Expr &e)
function which implements the DP strtagey to bitblast Inequations
int getBitvectorTypeParam(const Type &t)
Expr newBVMultPadExpr(int bvLength, const Expr &t1, const Expr &t2)
int min(std::vector< Rational > list)
Expr newRatExpr(const Rational &r)
int getBoolExtractIndex(const Expr &e)
ExprManager * getEM()
Access to ExprManager.
Theorem rewriteBV(const Expr &e, ExprMap< Theorem > &cache, int n=1)
Internal rewrite method for constants.
CDO< unsigned > d_index1
Used in checkSat.
int getFixedLeftShiftParam(const Expr &e)
Expr rat(const Rational &r)
const bool * d_booleanRWFlag
boolean on the fly rewrite flag
ExprMap< Expr > d_bvPlusCarryCacheLeftBV
bool getBVConstValue(const Expr &e, int i)
CDList< Theorem > d_eq
Backtracking queue for equalities.
StatCounter d_bvAssertEq
counts asserted equalities
size_t d_bvTypePredExprIndex
Rational Odd_coeff(const Expr &e)
Expr newBVPlusExpr(int numbits, const Expr &k1, const Expr &k2)
'numbits' is the number of bits in the result
Theorem rewriteBoolean(const Expr &e)
rewrite input boolean expression e to a simpler form
unsigned getBVConstSize(const Expr &e)
Theorem rewriteAtomic(const Expr &e)
Theory-specific rewrites for atomic formulas.
int getBVMultParam(const Expr &e)
bool isLinearTerm(const Expr &e)
Expr d_bvZero
Constant 1-bit bit-vector 0bin0.
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Expr newFixedRightShiftExpr(const Expr &t1, int r)
Expr newBoolExtractExpr(const Expr &t1, int r)
const Expr & bvZero() const
Return cached constant 0bin0.
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.
void assertTypePred(const Expr &e, const Theorem &pred)
Receives all the type predicates for the types of the given theory.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Theorem bitBlastDisEqn(const Theorem ¬E)
bitblast disequation
Cardinality
Enum for cardinality of types.
CDList< Theorem > d_bitblast
Backtracking queue for all other assertions.
Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
StatCounter d_bvDelayTypePreds
counts delayed type predicates
Expr newBVSRemExpr(const Expr &t1, const Expr &t2)
void extract_vars(const Expr &e, std::vector< Expr > &vars)
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Rational computeNegBVConst(const Expr &e)
computes the integer value of ~c+1 or BVUMINUS(c)
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Expr newBVXorExpr(const Expr &t1, const Expr &t2)
Expr newBVZeroString(int r)
produces a string of 0's of length bvLength
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
Expr newBVCompExpr(const Expr &t1, const Expr &t2)
Rational computeBVConst(const Expr &e)
computes the integer value of a bitvector constant
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Expr newBVAndExpr(const Expr &t1, const Expr &t2)
Theorem bitBlastTerm(const Expr &t, int bitPosition)
functions which implement the DP strategy for bitblasting
Theorem bitBlastEqn(const Expr &e)
functions which implement the DP strategy for bitblasting
std::vector< Theorem > additionalRewriteConstraints
Expr newBVSModExpr(const Expr &t1, const Expr &t2)
void computeType(const Expr &e)
Compute and store the type of e.
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
int getExtractLow(const Expr &e)
bool comparebv(const Expr &e1, const Expr &e2)