00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024 #define _CVC3_TRUSTED_
00025
00026
00027 #include "array_theorem_producer.h"
00028 #include "theory_array.h"
00029 #include "theory_core.h"
00030
00031
00032 using namespace std;
00033 using namespace CVC3;
00034
00035
00036
00037
00038
00039
00040
00041 ArrayProofRules* TheoryArray::createProofRules() {
00042 return new ArrayTheoremProducer(theoryCore()->getTM());
00043 }
00044
00045
00046
00047
00048
00049
00050
00051 #define CLASS_NAME "CVC3::ArrayTheoremProducer"
00052
00053
00054
00055
00056
00057
00058
00059
00060
00061
00062
00063 Theorem
00064 ArrayTheoremProducer::rewriteSameStore(const Expr& e, int n)
00065 {
00066 IF_DEBUG(
00067 DebugAssert(e.isEq(), "EQ expected");
00068 Expr e1 = e[0];
00069 int N = 0;
00070 while (isWrite(e1)) { N++; e1 = e1[0]; }
00071 DebugAssert(N == n && n > 0, "Counting error");
00072 DebugAssert(e1 == e[1], "Stores do not match");
00073 )
00074
00075 Proof pf;
00076 Expr write_i, write_j, index_i, index_j, hyp, conc, result;
00077 int i, j;
00078
00079 write_i = e[0];
00080 for (i = n-1; i >= 0; --i) {
00081 index_i = write_i[1];
00082
00083
00084
00085 write_j = e[0];
00086 for (j = n - 1; j > i; --j) {
00087 index_j = write_j[1];
00088 Expr hyp2(!((index_i.getType().isBool())?
00089 index_i.iffExpr(index_j) : index_i.eqExpr(index_j)));
00090 if (hyp.isNull()) hyp = hyp2;
00091 else hyp = hyp && hyp2;
00092 write_j = write_j[0];
00093 }
00094 Expr r1(Expr(READ, e[1], index_i));
00095 conc = (r1.getType().isBool())?
00096 r1.iffExpr(write_i[2]) : r1.eqExpr(write_i[2]);
00097 if (!hyp.isNull()) conc = hyp.impExpr(conc);
00098
00099
00100 if (result.isNull()) result = conc;
00101 else result = result && conc;
00102
00103
00104 write_i = write_i[0];
00105 hyp = Expr();
00106 }
00107 if (withProof()) pf = newPf("rewriteSameStore", e);
00108 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
00109 }
00110
00111
00112
00113
00114
00115 Theorem
00116 ArrayTheoremProducer::rewriteWriteWrite(const Expr& e)
00117 {
00118 IF_DEBUG(
00119 DebugAssert(e.isEq(), "EQ expected");
00120 DebugAssert(isWrite(e[0]) && isWrite(e[1]),
00121 "Expected WRITE = WRITE");
00122 )
00123 Proof pf;
00124 const Expr& left = e[0];
00125 const Expr& right = e[1];
00126 const Expr& store = left[0];
00127 const Expr& index = left[1];
00128 const Expr& value = left[2];
00129 Expr e1 = (store.getType().isBool())?
00130 store.iffExpr(Expr(WRITE, right, index, Expr(READ, store, index)))
00131 : store.eqExpr(Expr(WRITE, right, index, Expr(READ, store, index)));
00132 Expr e2 = (value.getType().isBool()) ?
00133 value.iffExpr(Expr(READ, right, index)) :
00134 value.eqExpr(Expr(READ, right, index));
00135 if (withProof()) pf = newPf("rewriteWriteWrite", e);
00136 return newRWTheorem(e, e1.andExpr(e2), Assumptions::emptyAssump(), pf);
00137 }
00138
00139
00140
00141
00142 Theorem
00143 ArrayTheoremProducer::rewriteReadWrite(const Expr& e)
00144 {
00145 IF_DEBUG(
00146 DebugAssert(isRead(e), "Read expected");
00147 DebugAssert(isWrite(e[0]), "Expected Read(Write)");
00148 )
00149 Proof pf;
00150 const Expr& store = e[0][0];
00151 const Expr& index1 = e[0][1];
00152 const Expr& value = e[0][2];
00153 const Expr& index2 = e[1];
00154 Expr indexCond = (index1.getType().isBool())?
00155 index1.iffExpr(index2) : index1.eqExpr(index2);
00156 if (withProof()) pf = newPf("rewriteReadWrite", e);
00157 return newRWTheorem(e, indexCond.iteExpr(value,
00158 Expr(READ, store, index2)), Assumptions::emptyAssump(), pf);
00159 }
00160
00161
00162
00163
00164
00165
00166
00167
00168
00169
00170
00171
00172
00173 Theorem
00174 ArrayTheoremProducer::rewriteRedundantWrite1(const Theorem& r_eq_v,
00175 const Expr& write)
00176 {
00177 DebugAssert(r_eq_v.isRewrite(), "Expected equation");
00178 DebugAssert(isRead(r_eq_v.getLHS()), "Expected Read");
00179 const Expr& index = r_eq_v.getLHS()[1];
00180 const Expr& value = r_eq_v.getRHS();
00181 DebugAssert(isWrite(write) &&
00182 index == write[1] && value == write[2],
00183 "Error in parameters to rewriteRedundantWrite1");
00184
00185 vector<Expr> indices;
00186 vector<Expr> values;
00187 Expr store = write[0];
00188 while (isWrite(store)) {
00189 indices.push_back(store[1]);
00190 values.push_back(store[2]);
00191 store = store[0];
00192 }
00193 DebugAssert(store == r_eq_v.getLHS()[0],
00194 "Store does not match in rewriteRedundantWrite");
00195 while (!indices.empty()) {
00196 store = Expr(WRITE, store, indices.back(),
00197 index.eqExpr(indices.back()).iteExpr(value, values.back()));
00198 indices.pop_back();
00199 values.pop_back();
00200 }
00201
00202 Proof pf;
00203 if(withProof()) {
00204 pf = newPf("rewriteRedundantWrite1", write, r_eq_v.getProof());
00205 }
00206 return newRWTheorem(write, store, r_eq_v.getAssumptionsRef(), pf);
00207 }
00208
00209
00210
00211
00212 Theorem
00213 ArrayTheoremProducer::rewriteRedundantWrite2(const Expr& e)
00214 {
00215 DebugAssert(isWrite(e) && isWrite(e[0]) &&
00216 e[0][1] == e[1],
00217 "Error in parameters to rewriteRedundantWrite2");
00218
00219 Proof pf;
00220
00221 if(withProof()) {
00222 pf = newPf("rewriteRedundantWrite2", e);
00223 }
00224
00225 return newRWTheorem(e, Expr(WRITE, e[0][0], e[1], e[2]), Assumptions::emptyAssump(), pf);
00226 }
00227
00228
00229
00230
00231
00232 Theorem
00233 ArrayTheoremProducer::interchangeIndices(const Expr& e)
00234 {
00235 DebugAssert(isWrite(e) && isWrite(e[0]),
00236 "Error in parameters to interchangeIndices");
00237
00238 Proof pf;
00239
00240 if(withProof()) {
00241 pf = newPf("interchangeIndices", e);
00242 }
00243
00244 Expr w0 = Expr(WRITE, e[0][0], e[1], e[2]);
00245 Expr indexCond = (e[0][1].getType().isBool())?
00246 e[0][1].iffExpr(e[1]) : e[0][1].eqExpr(e[1]);
00247 Expr w2 = Expr(WRITE, w0, e[0][1], indexCond.iteExpr(e[2], e[0][2]));
00248
00249 return newRWTheorem(e, w2, Assumptions::emptyAssump(), pf);
00250 }
00251
00252 Theorem
00253 ArrayTheoremProducer::readArrayLiteral(const Expr& e) {
00254 if(CHECK_PROOFS) {
00255 CHECK_SOUND(e.getKind() == READ,
00256 "ArrayTheoremProducer::readArrayLiteral("+e.toString()
00257 +"):\n\n expression is not a READ");
00258 }
00259
00260 Expr arrayLit(e[0]);
00261
00262 if (CHECK_PROOFS) {
00263 CHECK_SOUND(arrayLit.isClosure() && arrayLit.getKind()==ARRAY_LITERAL,
00264 "ArrayTheoremProducer::readArrayLiteral("+e.toString()+")");
00265 }
00266
00267 Expr body(arrayLit.getBody());
00268 const vector<Expr>& vars = arrayLit.getVars();
00269
00270 if(CHECK_PROOFS) {
00271 CHECK_SOUND(vars.size() == 1,
00272 "ArrayTheoremProducer::readArrayLiteral("+e.toString()+"):\n"
00273 +"wrong number of bound variables");
00274 }
00275
00276
00277 vector<Expr> ind;
00278 ind.push_back(e[1]);
00279 body = body.substExpr(vars, ind);
00280
00281 Proof pf;
00282 if(withProof())
00283 pf = newPf("read_array_literal", e);
00284 return newRWTheorem(e, body, Assumptions::emptyAssump(), pf);
00285 }
00286
00287
00288 Theorem ArrayTheoremProducer::liftReadIte(const Expr& e)
00289 {
00290 if(CHECK_PROOFS) {
00291 CHECK_SOUND(e.getKind() == READ && e[0].getKind() == ITE,
00292 "ArrayTheoremProducer::liftReadIte("+e.toString()
00293 +"):\n\n expression is not READ(ITE...");
00294 }
00295
00296 const Expr& ite = e[0];
00297
00298 Proof pf;
00299 if (withProof())
00300 pf = newPf("lift_read_ite",e);
00301 return newRWTheorem(e, Expr(ITE, ite[0], Expr(READ, ite[1], e[1]),
00302 Expr(READ, ite[2], e[1])),
00303 Assumptions::emptyAssump(), pf);
00304 }