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(this);
00043 }
00044   
00045 
00046 ArrayTheoremProducer::ArrayTheoremProducer(TheoryArray* theoryArray)
00047   : TheoremProducer(theoryArray->theoryCore()->getTM()),
00048     d_theoryArray(theoryArray)
00049 {}
00050 
00051 
00052 ////////////////////////////////////////////////////////////////////
00053 // Proof rules
00054 ////////////////////////////////////////////////////////////////////
00055 
00056 
00057 #define CLASS_NAME "CVC3::ArrayTheoremProducer"
00058 
00059 
00060 // ==>
00061 // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
00062 //
00063 // read(store, index_n) = v_n &
00064 // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
00065 // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
00066 // ...
00067 // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
00068 // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
00069 Theorem
00070 ArrayTheoremProducer::rewriteSameStore(const Expr& e, int n)
00071 {
00072   IF_DEBUG(
00073     DebugAssert(e.isEq(), "EQ expected");
00074     Expr e1 = e[0];
00075     int N = 0;
00076     while (isWrite(e1)) { N++; e1 = e1[0]; }
00077     DebugAssert(N == n && n > 0, "Counting error");
00078     DebugAssert(e1 == e[1], "Stores do not match");
00079   )
00080     
00081   Proof pf;
00082   Expr write_i, write_j, index_i, index_j, hyp, conc, result;
00083   int i, j;
00084 
00085   write_i = e[0];
00086   for (i = n-1; i >= 0; --i) {
00087     index_i = write_i[1];
00088 
00089     // build: [index_i /= index_n && index_i /= index_(n-1) &&
00090     //         ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
00091     write_j = e[0];
00092     for (j = n - 1; j > i; --j) {
00093       index_j = write_j[1];
00094       Expr hyp2(!((index_i.getType().isBool())? 
00095        index_i.iffExpr(index_j) : index_i.eqExpr(index_j)));
00096       if (hyp.isNull()) hyp = hyp2;
00097       else hyp = hyp && hyp2;
00098       write_j = write_j[0];
00099     }
00100     Expr r1(Expr(READ, e[1], index_i));
00101     conc = (r1.getType().isBool())? 
00102       r1.iffExpr(write_i[2]) : r1.eqExpr(write_i[2]);
00103     if (!hyp.isNull()) conc = hyp.impExpr(conc);
00104 
00105     // And into result
00106     if (result.isNull()) result = conc;
00107     else result = result && conc;
00108 
00109     // Prepare for next iteration
00110     write_i = write_i[0];
00111     hyp = Expr();
00112   }
00113   if (withProof()) pf = newPf("rewriteSameStore", e);
00114   return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
00115 }
00116 
00117 
00118 // ==> write(store, index, value) = write(...) IFF
00119 //       store = write(write(...), index, read(store, index)) &
00120 //       value = read(write(...), index)
00121 Theorem
00122 ArrayTheoremProducer::rewriteWriteWrite(const Expr& e)
00123 {
00124   IF_DEBUG(
00125     DebugAssert(e.isEq(), "EQ expected");
00126     DebugAssert(isWrite(e[0]) && isWrite(e[1]),
00127     "Expected WRITE = WRITE");
00128   )
00129   Proof pf;
00130   const Expr& left = e[0];
00131   const Expr& right = e[1];
00132   const Expr& store = left[0];
00133   const Expr& index = left[1];
00134   const Expr& value = left[2];
00135   Expr e1 = (store.getType().isBool())?
00136     store.iffExpr(Expr(WRITE, right, index, Expr(READ, store, index)))
00137     : store.eqExpr(Expr(WRITE, right, index, Expr(READ, store, index)));
00138   Expr e2 = (value.getType().isBool()) ?
00139     value.iffExpr(Expr(READ, right, index)) :
00140     value.eqExpr(Expr(READ, right, index));
00141   if (withProof()) pf = newPf("rewriteWriteWrite", e);
00142   return newRWTheorem(e, e1.andExpr(e2), Assumptions::emptyAssump(), pf);
00143 }
00144 
00145 
00146 // ==> read(write(store, index1, value), index2) =
00147 //   ite(index1 = index2, value, read(store, index2))
00148 Theorem
00149 ArrayTheoremProducer::rewriteReadWrite(const Expr& e)
00150 {
00151   IF_DEBUG(
00152     DebugAssert(isRead(e), "Read expected");
00153     DebugAssert(isWrite(e[0]), "Expected Read(Write)");
00154   )
00155   Proof pf;
00156   const Expr& store = e[0][0];
00157   const Expr& index1 = e[0][1];
00158   const Expr& value = e[0][2];
00159   const Expr& index2 = e[1];
00160   Expr indexCond = (index1.getType().isBool())?
00161     index1.iffExpr(index2) : index1.eqExpr(index2);
00162   if (withProof()) pf = newPf("rewriteReadWrite", e);
00163   return newRWTheorem(e, indexCond.iteExpr(value,
00164                                            Expr(READ, store, index2)), Assumptions::emptyAssump(), pf);
00165 }
00166 
00167 
00168 // e = read(write(store, index1, value), index2):
00169 // ==> ite(index1 = index2,
00170 //         read(write(store, index1, value), index2) = value,
00171 //         read(write(store, index1, value), index2) = read(store, index2))
00172 Theorem
00173 ArrayTheoremProducer::rewriteReadWrite2(const Expr& e)
00174 {
00175   IF_DEBUG(
00176     DebugAssert(isRead(e), "Read expected");
00177     DebugAssert(isWrite(e[0]), "Expected Read(Write)");
00178   )
00179   Proof pf;
00180   const Expr& store = e[0][0];
00181   const Expr& index1 = e[0][1];
00182   const Expr& value = e[0][2];
00183   const Expr& index2 = e[1];
00184   Expr indexCond = (index1.getType().isBool())?
00185     index1.iffExpr(index2) : index1.eqExpr(index2);
00186   if (withProof()) pf = newPf("rewriteReadWrite2", e);
00187   return newTheorem(indexCond.iteExpr(e.eqExpr(value),
00188                                       e.eqExpr(Expr(READ, store, index2))),
00189                     Assumptions::emptyAssump(), pf);
00190 }
00191 
00192 
00193 // read(store, index) = value ==>
00194 //   write(store, index, value) = store
00195 //
00196 // More general case:
00197 //
00198 // read(store, index_n) = value_n ==>
00199 //   write(store, index_0, v_0, index_1, v_1, ..., index_n, value_n) =
00200 //   write(store, index_0, ite(index_n = index_0, value_n, v_0),
00201 //                index_1, ite(index_n = index_1, value_n, v_1),
00202 //                ...
00203 //                index_{n-1}, ite(index_n = index_{n-1}, value_n, value_{n-1}))
00204 Theorem
00205 ArrayTheoremProducer::rewriteRedundantWrite1(const Theorem& r_eq_v,
00206                const Expr& write)
00207 {
00208   DebugAssert(r_eq_v.isRewrite(), "Expected equation");
00209   DebugAssert(isRead(r_eq_v.getLHS()), "Expected Read");
00210   const Expr& index = r_eq_v.getLHS()[1];
00211   const Expr& value = r_eq_v.getRHS();
00212   DebugAssert(isWrite(write) &&
00213         index == write[1] && value == write[2],
00214         "Error in parameters to rewriteRedundantWrite1");
00215 
00216   vector<Expr> indices;
00217   vector<Expr> values;
00218   Expr store = write[0];
00219   while (isWrite(store)) {
00220     indices.push_back(store[1]);
00221     values.push_back(store[2]);
00222     store = store[0];
00223   }
00224   DebugAssert(store == r_eq_v.getLHS()[0],
00225               "Store does not match in rewriteRedundantWrite");
00226   while (!indices.empty()) {
00227     store = Expr(WRITE, store, indices.back(),
00228                  index.eqExpr(indices.back()).iteExpr(value, values.back()));
00229     indices.pop_back();
00230     values.pop_back();
00231   }
00232 
00233   Proof pf;
00234   if(withProof()) {
00235     pf = newPf("rewriteRedundantWrite1", write, r_eq_v.getProof());
00236   }
00237   return newRWTheorem(write, store, r_eq_v.getAssumptionsRef(), pf);
00238 }
00239 
00240 
00241 // ==>
00242 //   write(write(store, index, v1), index, v2) = write(store, index, v2)
00243 Theorem
00244 ArrayTheoremProducer::rewriteRedundantWrite2(const Expr& e)
00245 {
00246   DebugAssert(isWrite(e) && isWrite(e[0]) &&
00247         e[0][1] == e[1],
00248         "Error in parameters to rewriteRedundantWrite2");
00249 
00250   Proof pf;
00251   
00252   if(withProof()) {
00253     pf = newPf("rewriteRedundantWrite2", e);
00254   }
00255 
00256   return newRWTheorem(e, Expr(WRITE, e[0][0], e[1], e[2]), Assumptions::emptyAssump(), pf);
00257 }
00258 
00259 
00260 // ==>
00261 //   write(write(store, index1, v1), index2, v2) =
00262 //   write(write(store, index2, v2), index1, ite(index1 = index2, v2, v1))
00263 Theorem
00264 ArrayTheoremProducer::interchangeIndices(const Expr& e)
00265 {
00266   DebugAssert(isWrite(e) && isWrite(e[0]),
00267         "Error in parameters to interchangeIndices");
00268 
00269   Proof pf;
00270   
00271   if(withProof()) {
00272     pf = newPf("interchangeIndices", e);
00273   }
00274 
00275   Expr w0 = Expr(WRITE, e[0][0], e[1], e[2]);
00276   Expr indexCond = (e[0][1].getType().isBool())?
00277     e[0][1].iffExpr(e[1]) : e[0][1].eqExpr(e[1]);
00278   Expr w2 = Expr(WRITE, w0, e[0][1], indexCond.iteExpr(e[2], e[0][2]));
00279 
00280   return newRWTheorem(e, w2, Assumptions::emptyAssump(), pf);
00281 }
00282 
00283 Theorem
00284 ArrayTheoremProducer::readArrayLiteral(const Expr& e) {
00285   if(CHECK_PROOFS) {
00286     CHECK_SOUND(e.getKind() == READ,
00287     "ArrayTheoremProducer::readArrayLiteral("+e.toString()
00288     +"):\n\n  expression is not a READ");
00289   }
00290 
00291   Expr arrayLit(e[0]);
00292 
00293   if (CHECK_PROOFS) {
00294     CHECK_SOUND(arrayLit.isClosure() && arrayLit.getKind()==ARRAY_LITERAL,
00295     "ArrayTheoremProducer::readArrayLiteral("+e.toString()+")");
00296   }
00297 
00298   Expr body(arrayLit.getBody());
00299   const vector<Expr>& vars = arrayLit.getVars();
00300 
00301   if(CHECK_PROOFS) {
00302     CHECK_SOUND(vars.size() == 1, 
00303     "ArrayTheoremProducer::readArrayLiteral("+e.toString()+"):\n"
00304     +"wrong number of bound variables");
00305   }
00306 
00307   // Use the Expr's efficient substitution
00308   vector<Expr> ind;
00309   ind.push_back(e[1]);
00310   body = body.substExpr(vars, ind);
00311 
00312   Proof pf;
00313   if(withProof())
00314     pf = newPf("read_array_literal", e);
00315   return newRWTheorem(e, body, Assumptions::emptyAssump(), pf);
00316 }
00317 
00318 
00319 Theorem ArrayTheoremProducer::liftReadIte(const Expr& e)
00320 {
00321   if(CHECK_PROOFS) {
00322     CHECK_SOUND(e.getKind() == READ && e[0].getKind() == ITE,
00323     "ArrayTheoremProducer::liftReadIte("+e.toString()
00324     +"):\n\n  expression is not READ(ITE...");
00325   }
00326 
00327   const Expr& ite = e[0];
00328 
00329   Proof pf;
00330   if (withProof())
00331     pf = newPf("lift_read_ite",e);
00332   return newRWTheorem(e, Expr(ITE, ite[0], Expr(READ, ite[1], e[1]),
00333                               Expr(READ, ite[2], e[1])),
00334                       Assumptions::emptyAssump(), pf);
00335 }
00336 
00337 
00338 Theorem ArrayTheoremProducer::arrayNotEq(const Theorem& e)
00339 {
00340   if(CHECK_PROOFS) {
00341     CHECK_SOUND(e.getExpr().getKind() == NOT &&
00342                 e.getExpr()[0].getKind() == EQ &&
00343                 isArray(d_theoryArray->getBaseType(e.getExpr()[0][0])),
00344     "ArrayTheoremProducer::arrayNotEq("+e.toString()
00345     +"):\n\n  expression is ill-formed");
00346   }
00347 
00348   Expr eq = e.getExpr()[0];
00349 
00350   Proof pf;
00351   if (withProof())
00352     pf = newPf("array_not_eq", e.getProof());
00353 
00354   Type arrType = d_theoryArray->getBaseType(eq[0]);
00355   Type indType = Type(arrType.getExpr()[0]);
00356   Expr var = d_theoryArray->getEM()->newBoundVarExpr(indType);
00357   eq = Expr(READ, eq[0], var).eqExpr(Expr(READ, eq[1], var));
00358 
00359   return newTheorem(d_theoryArray->getEM()->newClosureExpr(EXISTS, var, !eq),
00360                     Assumptions(e), pf);
00361 }

Generated on Wed Nov 18 16:13:28 2009 for CVC3 by  doxygen 1.5.2