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());
TheoryArray * d_theoryArray
Data structure of expressions in CVC3.
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Theorem newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)
Create a new theorem. See also newRWTheorem() and newReflTheorem()
bool isWrite(const Expr &e)
Theorem readArrayLiteral(const Expr &e)
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
MS C++ specific settings.
bool withProof()
Testing whether to generate proofs.
Expr eqExpr(const Expr &right) const
Theorem rewriteReadWrite2(const Expr &e)
#define DebugAssert(cond, str)
#define CHECK_SOUND(cond, msg)
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Expr andExpr(const Expr &right) const
Expr orExpr(const std::vector< Expr > &children)
Theorem interchangeIndices(const Expr &e)
Expr impExpr(const Expr &right) const
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Theorem propagateIndexDiseq(const Theorem &read1eqread2isFalse)
Theorem rewriteRedundantWrite2(const Expr &e)
std::string toString() const
std::string toString() const
Print the expression to a string.
Theorem rewriteSameStore(const Expr &e, int n)
Expr iffExpr(const Expr &right) const
const Expr & getBody() const
Get the body of the closure Expr.
const Expr & getRHS() const
const Assumptions & getAssumptionsRef() const
bool isArray(const Type &t)
ExprManager * getEM()
Access to ExprManager.
Theorem rewriteWriteWrite(const Expr &e)
This theory handles arrays.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
Theorem liftReadIte(const Expr &e)
Lift ite over read.
Theorem newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
Create a rewrite theorem: lhs = rhs.
Theorem rewriteRedundantWrite1(const Theorem &v_eq_r, const Expr &write)
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
const Expr & getLHS() const
bool isRead(const Expr &e)
Proof newPf(const std::string &name)
Theorem rewriteReadWrite(const Expr &e)
Type getType() const
Get the type. Recursively compute if necessary.
static const Assumptions & emptyAssump()
Expr andExpr(const std::vector< Expr > &children)
Theorem splitOnConstants(const Expr &a, const std::vector< Expr > &consts)
Theorem arrayNotEq(const Theorem &e)
a /= b |- exists i. a[i] /= b[i]