24 #define _CVC3_TRUSTED_
46 ArrayTheoremProducer::ArrayTheoremProducer(
TheoryArray* theoryArray)
48 d_theoryArray(theoryArray)
57 #define CLASS_NAME "CVC3::ArrayTheoremProducer"
76 while (
isWrite(e1)) { N++; e1 = e1[0]; }
82 Expr write_i, write_j, index_i, index_j, hyp, conc, result;
86 for (i = n-1; i >= 0; --i) {
92 for (j = n - 1; j > i; --j) {
94 Expr hyp2(!((index_i.getType().isBool())?
95 index_i.iffExpr(index_j) : index_i.eqExpr(index_j)));
96 if (hyp.isNull()) hyp = hyp2;
97 else hyp = hyp && hyp2;
103 if (!hyp.isNull()) conc = hyp.
impExpr(conc);
106 if (result.isNull()) result = conc;
107 else result = result && conc;
110 write_i = write_i[0];
127 "Expected WRITE = WRITE");
132 const Expr& store = left[0];
133 const Expr& index = left[1];
134 const Expr& value = left[2];
156 const Expr& store = e[0][0];
157 const Expr& index1 = e[0][1];
158 const Expr& value = e[0][2];
159 const Expr& index2 = e[1];
180 const Expr& store = e[0][0];
181 const Expr& index1 = e[0][1];
182 const Expr& value = e[0][2];
183 const Expr& index2 = e[1];
213 index == write[1] && value == write[2],
214 "Error in parameters to rewriteRedundantWrite1");
216 vector<Expr> indices;
218 Expr store = write[0];
220 indices.push_back(store[1]);
221 values.push_back(store[2]);
225 "Store does not match in rewriteRedundantWrite");
226 while (!indices.empty()) {
227 store =
Expr(
WRITE, store, indices.back(),
228 index.
eqExpr(indices.back()).iteExpr(value, values.back()));
235 pf =
newPf(
"rewriteRedundantWrite1", write, r_eq_v.
getProof());
248 "Error in parameters to rewriteRedundantWrite2");
253 pf =
newPf(
"rewriteRedundantWrite2", e);
267 "Error in parameters to interchangeIndices");
272 pf =
newPf(
"interchangeIndices", e);
277 e[0][1].iffExpr(e[1]) : e[0][1].
eqExpr(e[1]);
287 "ArrayTheoremProducer::readArrayLiteral("+e.
toString()
288 +
"):\n\n expression is not a READ");
295 "ArrayTheoremProducer::readArrayLiteral("+e.
toString()+
")");
299 const vector<Expr>& vars = arrayLit.
getVars();
303 "ArrayTheoremProducer::readArrayLiteral("+e.
toString()+
"):\n"
304 +
"wrong number of bound variables");
310 body = body.substExpr(vars, ind);
314 pf =
newPf(
"read_array_literal", e);
323 "ArrayTheoremProducer::liftReadIte("+e.
toString()
324 +
"):\n\n expression is not READ(ITE...");
327 const Expr& ite = e[0];
331 pf =
newPf(
"lift_read_ite",e);
344 "ArrayTheoremProducer::arrayNotEq("+e.
toString()
345 +
"):\n\n expression is ill-formed");
355 Type indType =
Type(arrType.getExpr()[0]);
369 for (
unsigned i = 0; i < consts.size(); ++ i) {
370 eq.push_back(a.
eqExpr(consts[i]));
374 if (eq.size() == 1) {
375 result = eq[0].orExpr(diseq[0]);
383 pf =
newPf(
"splitOnConstants");
389 Expr read1eqread2 = read1eqread2isFalse.
getLHS();
390 Expr read1 = read1eqread2[0];
391 Expr read2 = read1eqread2[1];
397 pf =
newPf(
"propagateIndexDiseq", read1eqread2isFalse.
getProof());