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);