21 #ifndef _cvc3__include__theory_array_h_
22 #define _cvc3__include__theory_array_h_
28 class ArrayProofRules;
97 bool enumerate,
bool computeSize);
const bool & d_liftReadIte
Flag to lift ite's over reads.
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Expr getBaseArray(const Expr &e) const
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
CDO< unsigned > d_index
Used in checkSat.
Expr arrayLiteral(const Expr &ind, const Expr &body)
CDO< size_t > d_sharedIdx1
void computeType(const Expr &e)
Compute and store the type of e.
ExprMap< Theorem > d_renameThms
Set of renaming theorems indexed by t.
bool isWrite(const Expr &e)
Type arrayType(const Type &type1, const Type &type2)
MS C++ specific settings.
TheoryArray(TheoryCore *core)
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
CDO< size_t > d_sharedIdx2
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
bool isArrayLiteral(const Expr &e)
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
ArrayProofRules * createProofRules()
const Expr & getExpr() const
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Theorem solve(const Theorem &e)
An optional solver.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
bool isArray(const Type &t)
CDMap< Expr, Expr > d_sharedSubterms
Backtracking database of subterms of shared terms.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
CDList< Expr > d_sharedSubtermsList
Backtracking database of subterms of shared terms.
Theorem pullIndex(const Expr &e, const Expr &index)
Derived rule.
This theory handles arrays.
CDList< Expr > d_reads
Backtracking list of array reads, for building concrete models.
ArrayProofRules * d_rules
bool isRead(const Expr &e)
void checkType(const Expr &e)
Check that e is a valid Type expr.
Cardinality
Enum for cardinality of types.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
int d_inCheckSat
Flag for use in checkSat.
const bool & d_applicationsInModel
Flag to include array reads to the concrete model.