43 :
Theory(core,
"Arrays"), d_reads(core->getCM()->getCurrentContext()),
44 d_applicationsInModel(core->getFlags()[
"applications"].getBool()),
45 d_liftReadIte(core->getFlags()[
"liftReadIte"].getBool()),
46 d_sharedSubterms(core->getCM()->getCurrentContext()),
47 d_sharedSubtermsList(core->getCM()->getCurrentContext()),
48 d_index(core->getCM()->getCurrentContext(), 0, 0),
49 d_sharedIdx1(core->getCM()->getCurrentContext(), 0, 0),
50 d_sharedIdx2(core->getCM()->getCurrentContext(), 0, 0),
62 kinds.push_back(
ARRAY);
63 kinds.push_back(
READ);
64 kinds.push_back(
WRITE);
82 TRACE(
"arrAddSharedTerm",
"TheoryArray::addSharedTerm(", e.
toString(),
")");
114 DebugAssert(expr[0].isEq(),
"Unexpected negation");
133 !
isWrite(expr[0]),
"Invariant violated");
146 for (i = 0; i < e.
arity(); ++i) {
147 if (!e[i].isAtomic())
break;
149 if (e[i].isAbsAtomicFormula())
return e[i];
156 if (fullEffort ==
true) {
169 if (!e.
hasRep())
continue;
197 Expr newExpr = thm.getExpr();
215 "Only non-normalized writes expected");
224 while (
isWrite(store)) store = store[0];
227 if (thm.
getRHS() == e[2]) {
232 else if (
isWrite(e[0]) && e[0][1] > e[1]) {
271 if (read[1].getKind() !=
BVCONST) {
282 for(; it != it_end; ++ it) {
283 Expr array = it->first;
288 for (; read1_it != read1_end; ++ read1_it) {
289 Expr read1 = (*read1_it);
294 for (; read2_it != read1_it; ++ read2_it) {
295 Expr read2 = (*read2_it);
297 if (read1_find != read2_find) {
301 if( !
simplify(eq).getRHS().isBoolConst() ) {
307 TRACE(
"sharing",
"splitting " + y_k.toString(),
" and ", x_k.
toString());
314 hash_set<Expr>& const_reads_single_array = const_reads_by_array[array];
315 read2_it = const_reads_single_array.
begin();
317 for (; read2_it != read2_it_end; ++ read2_it) {
318 Expr read2 = (*read2_it);
320 if (read1_find != read2_find) {
324 if( !
simplify(eq).getRHS().isBoolConst() ) {
330 TRACE(
"sharing",
"splitting " + y_k.toString(),
" and ", x_k.
toString());
355 if (e[0][1] == index) {
361 if (thm.
isNull())
return thm;
373 switch(e[0].getKind()) {
378 IF_DEBUG(debugger.counter(
"Read array literals")++;)
402 int leftWrites = 1, rightWrites = 0;
406 while (
isWrite(e1)) { leftWrites++; e1 = e1[0]; }
409 while (
isWrite(e2)) { rightWrites++; e2 = e2[0]; }
411 if (rightWrites == 0) {
421 if (leftWrites > rightWrites) {
438 const Expr& store = e[0];
442 if (
isRead(e[2]) && e[2][0] == store && e[2][1] == e[1]) {
461 if (store[1] > e[1]) {
481 "Unexpected default case");
494 for (
int k = 0; k < e.
arity(); ++k) {
508 TRACE(
"model",
"TheoryArray: add array read ", e,
"");
516 if (store[1] > e[1]) {
525 "Unexpected non-array-normalized term in setup");
530 while (
isWrite(store)) store = store[0];
560 "Expected lhs to be shared");
568 int k, ar(d.
arity());
576 if (sigNew == dsig)
return;
602 if (!repEQsigNew.
isNull()) {
607 for (k = 0; k < ar; ++k) {
608 if (sigNew[k] != dsig[k]) {
628 Expr store = sigNew[0];
631 if (thm2.
getRHS() == sigNew[2]) {
655 if (
isWrite(store) && (store[1] > sigNew[1])) {
670 while (
isWrite(store)) store = store[0];
736 (
"ARRAY type should have two arguments");
739 (
"Array index types must be non-Boolean");
741 (
"Array index types cannot be functions");
744 (
"Array value types must be non-Boolean");
746 (
"Array value types cannot be functions");
750 DebugAssert(
false,
"Unexpected kind in TheoryArray::checkType"
758 bool enumerate,
bool computeSize)
785 else if (sizeElem > 1) {
789 while (--sizeIndex > 0) {
821 (
"Expected an ARRAY type in\n\n "
822 +e[0].toString()+
"\n\nBut received this:\n\n "
823 +arrType.
toString()+
"\n\nIn the expression:\n\n "
828 (
"The type of index expression:\n\n "
830 +
"\n\nDoes not match the ARRAY index type:\n\n "
831 +arrType[0].toString()
832 +
"\n\nIn the expression: "+e.
toString());
847 (
"Expected an ARRAY type in\n\n "
848 +e[0].toString()+
"\n\nBut received this:\n\n "
849 +arrType.
toString()+
"\n\nIn the expression:\n\n "
855 (
"The type of index expression:\n\n "
857 +
"\n\nDoes not match the ARRAY's type index:\n\n "
858 +arrType[0].toString()
859 +
"\n\nIn the expression: "+e.
toString());
863 (
"The type of value expression:\n\n "
865 +
"\n\nDoes not match the ARRAY's value type:\n\n "
866 +arrType[1].toString()
867 +
"\n\nIn the expression: "+e.
toString());
875 "TheoryArray::computeType("+e.
toString()+
")");
890 "TheoryArray::computeBaseType("+t.
toString()+
")");
930 v.push_back((*i)[1]);
940 static unsigned count(0);
949 "TheoryArray::computeModel(WRITE)");
954 res = (ind.
eqExpr(indVal)).iteExpr(updVal, res);
978 TRACE(
"model",
"TheoryArray::computeModel: read = ", *i,
"");
986 vector<Theorem> thms;
987 vector<unsigned> changed;
988 thms.push_back(asst);
989 changed.push_back(1);
1000 +var.
toString()+
" has a Null value");
1005 if(reads.
size()==0) {
1012 "TheoryArray::computeModel(WRITE)");
1016 "TheoryArray::computeModel(): expected the reads "
1017 "table be non-empty");
1019 Expr res((*i).second);
1022 for(; i!=iend; ++i) {
1026 if((*i).second == res)
continue;
1029 res = cond.
iteExpr((*i).second, res);
1058 DebugAssert(
false,
"TheoryArray::computeTCC: Unexpected expression: "
1075 if (
theoryCore()->getTranslator()->printArrayExpr(os, e))
return os;
1081 os <<
"[" <<
push << e[0] <<
push <<
"]";
1083 os << e[0] <<
"[" <<
push << e[1] <<
push <<
"]";
1088 os <<
"w(" << push << e[0] <<
space <<
", "
1089 << push << e[1] <<
", " << push << e[2] << push <<
")";
1093 os <<
"(" << push << e[0] <<
space <<
"WITH ["
1094 << push << e[1] <<
"] := " << push << e[2] << push <<
")";
1097 os <<
"(ARRAY" <<
space << e[0] <<
space <<
"OF" <<
space << e[1] <<
")";
1101 const vector<Expr>& vars = e.getVars();
1103 os <<
"(" << push <<
"ARRAY" <<
space <<
"(" <<
push;
1105 for(
size_t i=0; i<vars.size(); ++i) {
1106 if(first) first=
false;
1107 else os << push <<
"," <<
pop <<
space;
1110 os <<
":" << space <<
pushdag << vars[i].getType() <<
popdag;
1112 os << push <<
"):" <<
pop <<
pop <<
space << body << push <<
")";
1127 os <<
"(" <<
push <<
"select" <<
space << e[0]
1134 os <<
"(" <<
push <<
"store" <<
space << e[0]
1144 "Suggestion: use command-line flag:\n"
1145 " -output-lang presentation");
1158 os <<
"(" <<
push <<
"READ" <<
space << e[0]
1165 os <<
"(" <<
push <<
"WRITE" <<
space << e[0]
1171 os <<
"(" <<
push <<
"ARRAY" <<
space << e[0]
1200 "TheoryArray::parseExprOp:\n e = "+e.
toString());
1202 const Expr& c1 = e[0][0];
1206 if(!(e.
arity() == 3))
1210 if(!(e.
arity() == 4))
1222 return Expr(kind, k, e.
getEM());
1228 const Expr& varPair = e[1];
1231 "literal expression: "+varPair.toString()+
1233 if(varPair[0].getKind() !=
ID)
1235 "literal expression: "+varPair.toString()+
1239 var.push_back(
addBoundVar(varPair[0][0].getString(), varTp));
1247 "TheoryArray::parseExprOp: wrong type: "
1263 vars.push_back(ind);
virtual Theorem simplify(const Expr &e)
Simplify a term e and return a Theorem(e==e')
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
virtual Theorem propagateIndexDiseq(const Theorem &read1eqread2isFalse)=0
ExprStream & pop(ExprStream &os)
Restore the indentation.
const bool & d_liftReadIte
Flag to lift ite's over reads.
void setupTerm(const Expr &e, Theory *i, const Theorem &thm)
Setup additional terms within a theory-specific setup().
iterator begin() const
Begin iterator.
bool isAtomic() const
Test if e is atomic.
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
TheoryCore * theoryCore()
Get a pointer to theoryCore.
void setRewriteNormal() const
Data structure of expressions in CVC3.
Cardinality card() const
Return cardinality of type.
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
ExprManager * getEM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
An exception thrown by the parser.
Expr getBaseArray(const Expr &e) const
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
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)
bool notArrayNormalized() const
void addToNotify(Theory *i, const Expr &e) const
Add (e,i) to the notify list of this expression.
An exception to be thrown at typecheck error.
void computeType(const Expr &e)
Compute and store the type of e.
bool isWrite(const Expr &e)
virtual Theorem rewriteWriteWrite(const Expr &e)=0
Type arrayType(const Type &type1, const Type &type2)
_hash_table::iterator iterator
virtual Theorem liftReadIte(const Expr &e)=0
Lift ite over read.
MS C++ specific settings.
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
Lisp-like format for automatically generated specs.
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Expr eqExpr(const Expr &right) const
ExprStream & space(ExprStream &os)
Insert a single white space separator.
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
virtual Theorem rewriteSameStore(const Expr &e, int n)=0
#define DebugAssert(cond, str)
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
void setRep(const Theorem &e) const
void setSig(const Theorem &e) const
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.
T & push_back(const T &data, int scope=-1)
Expr andExpr(const Expr &right) const
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
ExprStream & pushdag(ExprStream &os)
virtual Theorem arrayNotEq(const Theorem &e)=0
a /= b |- exists i. a[i] /= b[i]
ArrayProofRules * createProofRules()
virtual Theorem rewriteReadWrite(const Expr &e)=0
Theorem renameExpr(const Expr &e)
Derived rule to create a new name for an expression.
Op getOp() const
Get operator from expression.
const Expr & getExpr() const
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
const_iterator end() const
CommonProofRules * getCommonRules()
Get a pointer to common proof rules.
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.
virtual Theorem rewriteRedundantWrite2(const Expr &e)=0
Theorem solve(const Theorem &e)
An optional solver.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Identifier is (ID (STRING_EXPR "name"))
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Expr enumerateFinite(Unsigned n) const
Return nth (starting with 0) element in a finite type.
virtual Theorem rewriteRedundantWrite1(const Theorem &v_eq_r, const Expr &write)=0
std::string toString() const
Print the expression to a string.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
const Theorem & getSig() const
const Theorem & getRep() const
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
const Expr & getBody() const
Get the body of the closure Expr.
std::string int2string(int n)
Expr simplifyExpr(const Expr &e)
Simplify a term e w.r.t. the current context.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
const Expr & getRHS() const
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
const Theorem & findRef(const Expr &e)
Return the find as a reference: expr must have a find.
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
std::string toString() const
iterator begin()
iterators
Expr addBoundVar(const std::string &name, const Type &type)
Create and add a new bound variable to the stack, for parseExprOp().
std::pair< iterator, bool > insert(const value_type &entry)
static Type anyType(ExprManager *em)
bool isArray(const Type &t)
ExprManager * getEM()
Access to ExprManager.
CDMap< Expr, Expr > d_sharedSubterms
Backtracking database of subterms of shared terms.
ExprStream & popdag(ExprStream &os)
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
virtual Theorem readArrayLiteral(const Expr &e)=0
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
Theorem updateHelper(const Expr &e)
Update the children of the term e.
CDList< Expr > d_sharedSubtermsList
Backtracking database of subterms of shared terms.
Theorem pullIndex(const Expr &e, const Expr &index)
Derived rule.
void setType(const Type &t) const
Set the cached type.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
CDList< Expr > d_reads
Backtracking list of array reads, for building concrete models.
virtual bool inconsistent()
Check if the current context is inconsistent.
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
An exception to be thrown by the smtlib translator.
An exception to be thrown by the smtlib translator.
ArrayProofRules * d_rules
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Unsigned sizeFinite() const
Return size of a finite type; returns 0 if size cannot be determined.
virtual Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)=0
const Expr & getLHS() const
virtual Theorem interchangeIndices(const Expr &e)=0
bool isRead(const Expr &e)
void checkType(const Expr &e)
Check that e is a valid Type expr.
Theorem rewriteIte(const Expr &e)
Derived rule for rewriting ITE.
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
const_iterator begin() const
Theorem reflexivityRule(const Expr &a)
==> a == a
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Cardinality
Enum for cardinality of types.
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Type getType() const
Get the type. Recursively compute if necessary.
InputLanguage lang() const
Get the current output language.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
void setNotArrayNormalized() const
Expr andExpr(const std::vector< Expr > &children)
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
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.
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
Nice SAL-like language for manually written specs.
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
iterator end() const
End iterator.