array_theorem_producer.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file array_theorem_producer.cpp
00004  * \brief Description: TRUSTED implementation of array proof rules.
00005  * 
00006  * Author: Clark Barrett
00007  * 
00008  * Created: Thu May 29 14:02:16 2003
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 
00023 // This code is trusted
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 // TheoryArray: trusted method for creating ArrayTheoremProducer
00038 ////////////////////////////////////////////////////////////////////
00039 
00040 
00041 ArrayProofRules* TheoryArray::createProofRules() {
00042   return new ArrayTheoremProducer(theoryCore()->getTM());
00043 }
00044   
00045 
00046 ////////////////////////////////////////////////////////////////////
00047 // Proof rules
00048 ////////////////////////////////////////////////////////////////////
00049 
00050 
00051 #define CLASS_NAME "CVC3::ArrayTheoremProducer"
00052 
00053 
00054 // ==>
00055 // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
00056 //
00057 // read(store, index_n) = v_n &
00058 // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
00059 // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
00060 // ...
00061 // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
00062 // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
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     // build: [index_i /= index_n && index_i /= index_(n-1) &&
00084     //         ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
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     // And into result
00100     if (result.isNull()) result = conc;
00101     else result = result && conc;
00102 
00103     // Prepare for next iteration
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 // ==> write(store, index, value) = write(...) IFF
00113 //       store = write(write(...), index, read(store, index)) &
00114 //       value = read(write(...), index)
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 // ==> read(write(store, index1, value), index2) =
00141 //   ite(index1 = index2, value, read(store, index2))
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 // read(store, index) = value ==>
00163 //   write(store, index, value) = store
00164 //
00165 // More general case:
00166 //
00167 // read(store, index_n) = value_n ==>
00168 //   write(store, index_0, v_0, index_1, v_1, ..., index_n, value_n) =
00169 //   write(store, index_0, ite(index_n = index_0, value_n, v_0),
00170 //                index_1, ite(index_n = index_1, value_n, v_1),
00171 //                ...
00172 //                index_{n-1}, ite(index_n = index_{n-1}, value_n, value_{n-1}))
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 //   write(write(store, index, v1), index, v2) = write(store, index, v2)
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 //   write(write(store, index1, v1), index2, v2) =
00231 //   write(write(store, index2, v2), index1, ite(index1 = index2, v2, v1))
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   // Use the Expr's efficient substitution
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 }

Generated on Tue Jul 3 14:33:34 2007 for CVC3 by  doxygen 1.5.1