CVC3  2.4.1
array_theorem_producer.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file array_theorem_producer.cpp
4  * \brief Description: TRUSTED implementation of array proof rules.
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Thu May 29 14:02:16 2003
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 
23 // This code is trusted
24 #define _CVC3_TRUSTED_
25 
26 
27 #include "array_theorem_producer.h"
28 #include "theory_array.h"
29 #include "theory_core.h"
30 
31 
32 using namespace std;
33 using namespace CVC3;
34 
35 
36 ////////////////////////////////////////////////////////////////////
37 // TheoryArray: trusted method for creating ArrayTheoremProducer
38 ////////////////////////////////////////////////////////////////////
39 
40 
41 ArrayProofRules* TheoryArray::createProofRules() {
42  return new ArrayTheoremProducer(this);
43 }
44 
45 
46 ArrayTheoremProducer::ArrayTheoremProducer(TheoryArray* theoryArray)
47  : TheoremProducer(theoryArray->theoryCore()->getTM()),
48  d_theoryArray(theoryArray)
49 {}
50 
51 
52 ////////////////////////////////////////////////////////////////////
53 // Proof rules
54 ////////////////////////////////////////////////////////////////////
55 
56 
57 #define CLASS_NAME "CVC3::ArrayTheoremProducer"
58 
59 
60 // ==>
61 // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
62 //
63 // read(store, index_n) = v_n &
64 // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
65 // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
66 // ...
67 // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
68 // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
69 Theorem
71 {
72  IF_DEBUG(
73  DebugAssert(e.isEq(), "EQ expected");
74  Expr e1 = e[0];
75  int N = 0;
76  while (isWrite(e1)) { N++; e1 = e1[0]; }
77  DebugAssert(N == n && n > 0, "Counting error");
78  DebugAssert(e1 == e[1], "Stores do not match");
79  )
80 
81  Proof pf;
82  Expr write_i, write_j, index_i, index_j, hyp, conc, result;
83  int i, j;
84 
85  write_i = e[0];
86  for (i = n-1; i >= 0; --i) {
87  index_i = write_i[1];
88 
89  // build: [index_i /= index_n && index_i /= index_(n-1) &&
90  // ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
91  write_j = e[0];
92  for (j = n - 1; j > i; --j) {
93  index_j = write_j[1];
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;
98  write_j = write_j[0];
99  }
100  Expr r1(Expr(READ, e[1], index_i));
101  conc = (r1.getType().isBool())?
102  r1.iffExpr(write_i[2]) : r1.eqExpr(write_i[2]);
103  if (!hyp.isNull()) conc = hyp.impExpr(conc);
104 
105  // And into result
106  if (result.isNull()) result = conc;
107  else result = result && conc;
108 
109  // Prepare for next iteration
110  write_i = write_i[0];
111  hyp = Expr();
112  }
113  if (withProof()) pf = newPf("rewriteSameStore", e);
114  return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
115 }
116 
117 
118 // ==> write(store, index, value) = write(...) IFF
119 // store = write(write(...), index, read(store, index)) &
120 // value = read(write(...), index)
121 Theorem
123 {
124  IF_DEBUG(
125  DebugAssert(e.isEq(), "EQ expected");
126  DebugAssert(isWrite(e[0]) && isWrite(e[1]),
127  "Expected WRITE = WRITE");
128  )
129  Proof pf;
130  const Expr& left = e[0];
131  const Expr& right = e[1];
132  const Expr& store = left[0];
133  const Expr& index = left[1];
134  const Expr& value = left[2];
135  Expr e1 = (store.getType().isBool())?
136  store.iffExpr(Expr(WRITE, right, index, Expr(READ, store, index)))
137  : store.eqExpr(Expr(WRITE, right, index, Expr(READ, store, index)));
138  Expr e2 = (value.getType().isBool()) ?
139  value.iffExpr(Expr(READ, right, index)) :
140  value.eqExpr(Expr(READ, right, index));
141  if (withProof()) pf = newPf("rewriteWriteWrite", e);
142  return newRWTheorem(e, e1.andExpr(e2), Assumptions::emptyAssump(), pf);
143 }
144 
145 
146 // ==> read(write(store, index1, value), index2) =
147 // ite(index1 = index2, value, read(store, index2))
148 Theorem
150 {
151  IF_DEBUG(
152  DebugAssert(isRead(e), "Read expected");
153  DebugAssert(isWrite(e[0]), "Expected Read(Write)");
154  )
155  Proof pf;
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];
160  Expr indexCond = (index1.getType().isBool())?
161  index1.iffExpr(index2) : index1.eqExpr(index2);
162  if (withProof()) pf = newPf("rewriteReadWrite", e);
163  return newRWTheorem(e, indexCond.iteExpr(value,
164  Expr(READ, store, index2)), Assumptions::emptyAssump(), pf);
165 }
166 
167 
168 // e = read(write(store, index1, value), index2):
169 // ==> ite(index1 = index2,
170 // read(write(store, index1, value), index2) = value,
171 // read(write(store, index1, value), index2) = read(store, index2))
172 Theorem
174 {
175  IF_DEBUG(
176  DebugAssert(isRead(e), "Read expected");
177  DebugAssert(isWrite(e[0]), "Expected Read(Write)");
178  )
179  Proof pf;
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];
184  Expr indexCond = (index1.getType().isBool())?
185  index1.iffExpr(index2) : index1.eqExpr(index2);
186  if (withProof()) pf = newPf("rewriteReadWrite2", e);
187  return newTheorem(indexCond.iteExpr(e.eqExpr(value),
188  e.eqExpr(Expr(READ, store, index2))),
190 }
191 
192 
193 // read(store, index) = value ==>
194 // write(store, index, value) = store
195 //
196 // More general case:
197 //
198 // read(store, index_n) = value_n ==>
199 // write(store, index_0, v_0, index_1, v_1, ..., index_n, value_n) =
200 // write(store, index_0, ite(index_n = index_0, value_n, v_0),
201 // index_1, ite(index_n = index_1, value_n, v_1),
202 // ...
203 // index_{n-1}, ite(index_n = index_{n-1}, value_n, value_{n-1}))
204 Theorem
206  const Expr& write)
207 {
208  DebugAssert(r_eq_v.isRewrite(), "Expected equation");
209  DebugAssert(isRead(r_eq_v.getLHS()), "Expected Read");
210  const Expr& index = r_eq_v.getLHS()[1];
211  const Expr& value = r_eq_v.getRHS();
212  DebugAssert(isWrite(write) &&
213  index == write[1] && value == write[2],
214  "Error in parameters to rewriteRedundantWrite1");
215 
216  vector<Expr> indices;
217  vector<Expr> values;
218  Expr store = write[0];
219  while (isWrite(store)) {
220  indices.push_back(store[1]);
221  values.push_back(store[2]);
222  store = store[0];
223  }
224  DebugAssert(store == r_eq_v.getLHS()[0],
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()));
229  indices.pop_back();
230  values.pop_back();
231  }
232 
233  Proof pf;
234  if(withProof()) {
235  pf = newPf("rewriteRedundantWrite1", write, r_eq_v.getProof());
236  }
237  return newRWTheorem(write, store, r_eq_v.getAssumptionsRef(), pf);
238 }
239 
240 
241 // ==>
242 // write(write(store, index, v1), index, v2) = write(store, index, v2)
243 Theorem
245 {
246  DebugAssert(isWrite(e) && isWrite(e[0]) &&
247  e[0][1] == e[1],
248  "Error in parameters to rewriteRedundantWrite2");
249 
250  Proof pf;
251 
252  if(withProof()) {
253  pf = newPf("rewriteRedundantWrite2", e);
254  }
255 
256  return newRWTheorem(e, Expr(WRITE, e[0][0], e[1], e[2]), Assumptions::emptyAssump(), pf);
257 }
258 
259 
260 // ==>
261 // write(write(store, index1, v1), index2, v2) =
262 // write(write(store, index2, v2), index1, ite(index1 = index2, v2, v1))
263 Theorem
265 {
266  DebugAssert(isWrite(e) && isWrite(e[0]),
267  "Error in parameters to interchangeIndices");
268 
269  Proof pf;
270 
271  if(withProof()) {
272  pf = newPf("interchangeIndices", e);
273  }
274 
275  Expr w0 = Expr(WRITE, e[0][0], e[1], e[2]);
276  Expr indexCond = (e[0][1].getType().isBool())?
277  e[0][1].iffExpr(e[1]) : e[0][1].eqExpr(e[1]);
278  Expr w2 = Expr(WRITE, w0, e[0][1], indexCond.iteExpr(e[2], e[0][2]));
279 
280  return newRWTheorem(e, w2, Assumptions::emptyAssump(), pf);
281 }
282 
283 Theorem
285  if(CHECK_PROOFS) {
286  CHECK_SOUND(e.getKind() == READ,
287  "ArrayTheoremProducer::readArrayLiteral("+e.toString()
288  +"):\n\n expression is not a READ");
289  }
290 
291  Expr arrayLit(e[0]);
292 
293  if (CHECK_PROOFS) {
294  CHECK_SOUND(arrayLit.isClosure() && arrayLit.getKind()==ARRAY_LITERAL,
295  "ArrayTheoremProducer::readArrayLiteral("+e.toString()+")");
296  }
297 
298  Expr body(arrayLit.getBody());
299  const vector<Expr>& vars = arrayLit.getVars();
300 
301  if(CHECK_PROOFS) {
302  CHECK_SOUND(vars.size() == 1,
303  "ArrayTheoremProducer::readArrayLiteral("+e.toString()+"):\n"
304  +"wrong number of bound variables");
305  }
306 
307  // Use the Expr's efficient substitution
308  vector<Expr> ind;
309  ind.push_back(e[1]);
310  body = body.substExpr(vars, ind);
311 
312  Proof pf;
313  if(withProof())
314  pf = newPf("read_array_literal", e);
315  return newRWTheorem(e, body, Assumptions::emptyAssump(), pf);
316 }
317 
318 
320 {
321  if(CHECK_PROOFS) {
322  CHECK_SOUND(e.getKind() == READ && e[0].getKind() == ITE,
323  "ArrayTheoremProducer::liftReadIte("+e.toString()
324  +"):\n\n expression is not READ(ITE...");
325  }
326 
327  const Expr& ite = e[0];
328 
329  Proof pf;
330  if (withProof())
331  pf = newPf("lift_read_ite",e);
332  return newRWTheorem(e, Expr(ITE, ite[0], Expr(READ, ite[1], e[1]),
333  Expr(READ, ite[2], e[1])),
335 }
336 
337 
339 {
340  if(CHECK_PROOFS) {
341  CHECK_SOUND(e.getExpr().getKind() == NOT &&
342  e.getExpr()[0].getKind() == EQ &&
344  "ArrayTheoremProducer::arrayNotEq("+e.toString()
345  +"):\n\n expression is ill-formed");
346  }
347 
348  Expr eq = e.getExpr()[0];
349 
350  Proof pf;
351  if (withProof())
352  pf = newPf("array_not_eq", e.getProof());
353 
354  Type arrType = d_theoryArray->getBaseType(eq[0]);
355  Type indType = Type(arrType.getExpr()[0]);
356  Expr var = d_theoryArray->getEM()->newBoundVarExpr(indType);
357  eq = Expr(READ, eq[0], var).eqExpr(Expr(READ, eq[1], var));
358 
359  return newTheorem(d_theoryArray->getEM()->newClosureExpr(EXISTS, var, !eq),
360  Assumptions(e), pf);
361 }
362 
363 Theorem ArrayTheoremProducer::splitOnConstants(const Expr& a, const std::vector<Expr>& consts) {
364  Theorem res;
365  Expr result;
366 
367  vector<Expr> eq;
368  vector<Expr> diseq;
369  for (unsigned i = 0; i < consts.size(); ++ i) {
370  eq.push_back(a.eqExpr(consts[i]));
371  diseq.push_back(a.eqExpr(consts[i]).notExpr());
372  }
373 
374  if (eq.size() == 1) {
375  result = eq[0].orExpr(diseq[0]);
376  } else {
377  eq.push_back(andExpr(diseq));
378  result = orExpr(eq);
379  }
380 
381  Proof pf;
382  if (withProof())
383  pf = newPf("splitOnConstants");
384 
385  return newTheorem(result, Assumptions::emptyAssump(), pf);
386 }
387 
389  Expr read1eqread2 = read1eqread2isFalse.getLHS();
390  Expr read1 = read1eqread2[0];
391  Expr read2 = read1eqread2[1];
392  Expr i1 = read1[1];
393  Expr i2 = read2[1];
394 
395  Proof pf;
396  if (withProof())
397  pf = newPf("propagateIndexDiseq", read1eqread2isFalse.getProof());
398 
399  return newTheorem(i1.eqExpr(i2).notExpr(), Assumptions(read1eqread2isFalse), pf);
400 }