array_theorem_producer.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file array_theorem_producer.cpp
 * \brief Description: TRUSTED implementation of array proof rules.
 * 
 * Author: Clark Barrett
 * 
 * Created: Thu May 29 14:02:16 2003
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/


// This code is trusted
#define _CVCL_TRUSTED_


#include "array_theorem_producer.h"
#include "theory_array.h"
#include "theory_core.h"


using namespace std;
using namespace CVCL;


////////////////////////////////////////////////////////////////////
// TheoryArray: trusted method for creating ArrayTheoremProducer
////////////////////////////////////////////////////////////////////


ArrayProofRules* TheoryArray::createProofRules() {
  return new ArrayTheoremProducer(theoryCore()->getTM());
}
  

////////////////////////////////////////////////////////////////////
// Proof rules
////////////////////////////////////////////////////////////////////


#define CLASS_NAME "CVCL::ArrayTheoremProducer"


// ==>
// write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
//
// read(store, index_n) = v_n &
// index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
// (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
// ...
// (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
// (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
Theorem
ArrayTheoremProducer::rewriteSameStore(const Expr& e, int n)
{
  IF_DEBUG(
    DebugAssert(e.isEq(), "EQ expected");
    Expr e1 = e[0];
    int N = 0;
    while (isWrite(e1)) { N++; e1 = e1[0]; }
    DebugAssert(N == n && n > 0, "Counting error");
    DebugAssert(e1 == e[1], "Stores do not match");
  )
    
  Assumptions a;
  Proof pf;
  Expr write_i, write_j, index_i, index_j, hyp, conc, result;
  int i, j;

  write_i = e[0];
  for (i = n-1; i >= 0; --i) {
    index_i = write_i[1];

    // build: [index_i /= index_n && index_i /= index_(n-1) &&
    //         ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
    write_j = e[0];
    for (j = n - 1; j > i; --j) {
      index_j = write_j[1];
      Expr hyp2(!((index_i.getType().isBool())? 
                   index_i.iffExpr(index_j) : index_i.eqExpr(index_j)));
      if (hyp.isNull()) hyp = hyp2;
      else hyp = hyp && hyp2;
      write_j = write_j[0];
    }
    Expr r1(Expr(READ, e[1], index_i));
    conc = (r1.getType().isBool())? 
      r1.iffExpr(write_i[2]) : r1.eqExpr(write_i[2]);
    if (!hyp.isNull()) conc = hyp.impExpr(conc);

    // And into result
    if (result.isNull()) result = conc;
    else result = result && conc;

    // Prepare for next iteration
    write_i = write_i[0];
    hyp = Expr();
  }
  if (withProof()) pf = newPf("rewriteSameStore", e);
  return newRWTheorem(e, result, a, pf);
}


// ==> write(store, index, value) = write(...) IFF
//       store = write(write(...), index, read(store, index)) &
//       value = read(write(...), index)
Theorem
ArrayTheoremProducer::rewriteWriteWrite(const Expr& e)
{
  IF_DEBUG(
    DebugAssert(e.isEq(), "EQ expected");
    DebugAssert(isWrite(e[0]) && isWrite(e[1]),
                "Expected WRITE = WRITE");
  )
  Assumptions a;
  Proof pf;
  const Expr& left = e[0];
  const Expr& right = e[1];
  const Expr& store = left[0];
  const Expr& index = left[1];
  const Expr& value = left[2];
  Expr e1 = (store.getType().isBool())?
    store.iffExpr(Expr(WRITE, right, index, Expr(READ, store, index)))
    : store.eqExpr(Expr(WRITE, right, index, Expr(READ, store, index)));
  Expr e2 = (value.getType().isBool()) ?
    value.iffExpr(Expr(READ, right, index)) :
    value.eqExpr(Expr(READ, right, index));
  if (withProof()) pf = newPf("rewriteWriteWrite", e);
  return newRWTheorem(e, e1.andExpr(e2), a, pf);
}


// ==> read(write(store, index1, value), index2) =
//   ite(index1 = index2, value, read(store, index2))
Theorem
ArrayTheoremProducer::rewriteReadWrite(const Expr& e)
{
  IF_DEBUG(
    DebugAssert(isRead(e), "Read expected");
    DebugAssert(isWrite(e[0]), "Expected Read(Write)");
  )
  Assumptions a;
  Proof pf;
  const Expr& store = e[0][0];
  const Expr& index1 = e[0][1];
  const Expr& value = e[0][2];
  const Expr& index2 = e[1];
  Expr indexCond = (index1.getType().isBool())?
    index1.iffExpr(index2) : index1.eqExpr(index2);
  if (withProof()) pf = newPf("rewriteReadWrite", e);
  return newRWTheorem(e, indexCond.iteExpr(value,
                                           Expr(READ, store, index2)), a, pf);
}


// value = read(store, index) ==>
//   write(store, index, value) = store
Theorem
ArrayTheoremProducer::rewriteRedundantWrite1(const Theorem& v_eq_r,
                                             const Expr& write)
{
  DebugAssert(v_eq_r.isRewrite(), "Expected equation");
  DebugAssert(isRead(v_eq_r.getRHS()), "Expected Read");
  DebugAssert(isWrite(write) && v_eq_r.getRHS()[0] == write[0] &&
              v_eq_r.getRHS()[1] == write[1] && v_eq_r.getLHS() == write[2],
              "Error in parameters to rewriteRedundantWrite1");
  Assumptions a;
  Proof pf;
  if (withAssumptions()) a = v_eq_r.getAssumptions().copy();
  if(withProof()) {
    pf = newPf("rewriteRedundantWrite1", write, v_eq_r.getProof());
  }
  return newRWTheorem(write, write[0], a, pf);
}


// ==>
//   write(write(store, index, v1), index, v2) = write(store, index, v2)
Theorem
ArrayTheoremProducer::rewriteRedundantWrite2(const Expr& e)
{
  DebugAssert(isWrite(e) && isWrite(e[0]) &&
              e[0][1] == e[1],
              "Error in parameters to rewriteRedundantWrite2");

  Assumptions a;
  Proof pf;
  
  if(withProof()) {
    pf = newPf("rewriteRedundantWrite2", e);
  }

  return newRWTheorem(e, Expr(WRITE, e[0][0], e[1], e[2]), a, pf);
}


// ==>
//   write(write(store, index1, v1), index2, v2) =
//   write(write(store, index2, v2), index1, ite(index1 = index2, v2, v1))
Theorem
ArrayTheoremProducer::interchangeIndices(const Expr& e)
{
  DebugAssert(isWrite(e) && isWrite(e[0]),
              "Error in parameters to interchangeIndices");

  Assumptions a;
  Proof pf;
  
  if(withProof()) {
    pf = newPf("interchangeIndices", e);
  }

  Expr w0 = Expr(WRITE, e[0][0], e[1], e[2]);
  Expr indexCond = (e[0][1].getType().isBool())?
    e[0][1].iffExpr(e[1]) : e[0][1].eqExpr(e[1]);
  Expr w2 = Expr(WRITE, w0, e[0][1], indexCond.iteExpr(e[2], e[0][2]));

  return newRWTheorem(e, w2, a, pf);
}

Theorem
ArrayTheoremProducer::readArrayLiteral(const Expr& e) {
  if(CHECK_PROOFS) {
    CHECK_SOUND(e.getKind() == READ,
                "ArrayTheoremProducer::readArrayLiteral("+e.toString()
                +"):\n\n  expression is not a READ");
  }

  Expr arrayLit(e[0]);

  if (CHECK_PROOFS) {
    CHECK_SOUND(arrayLit.isClosure() && arrayLit.getKind()==ARRAY_LITERAL,
                "ArrayTheoremProducer::readArrayLiteral("+e.toString()+")");
  }

  Expr body(arrayLit.getBody());
  const vector<Expr>& vars = arrayLit.getVars();

  if(CHECK_PROOFS) {
    CHECK_SOUND(vars.size() == 1, 
                "ArrayTheoremProducer::readArrayLiteral("+e.toString()+"):\n"
                +"wrong number of bound variables");
  }

  // Use the Expr's efficient substitution
  vector<Expr> ind;
  ind.push_back(e[1]);
  body = body.substExpr(vars, ind);

  Assumptions a;
  Proof pf;
  if(withProof())
    pf = newPf("read_array_literal", e);
  return newRWTheorem(e, body, a, pf);
}

---