/*****************************************************************************/
/*!
 * \file theory_array.cpp
 * 
 * Author: Clark Barrett
 * 
 * Created: Thu Feb 27 00:38:55 2003
 *
 * <hr>
 *
 * 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.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/


#include "theory_array.h"
#include "array_proof_rules.h"
#include "typecheck_exception.h"
#include "parser_exception.h"
#include "smtlib_exception.h"
#include "theory_core.h"
#include "command_line_flags.h"
#include "translator.h"


using namespace std;
using namespace CVC3;


///////////////////////////////////////////////////////////////////////////////
// TheoryArray Private Methods                                               //
///////////////////////////////////////////////////////////////////////////////

Theorem TheoryArray::renameExpr(const Expr& e) {
  Theorem thm = getCommonRules()->varIntroSkolem(e);
  DebugAssert(thm.isRewrite() && thm.getRHS().isSkolem(),
              "thm = "+thm.toString());
  theoryCore()->addToVarDB(thm.getRHS());
  return thm;
}


///////////////////////////////////////////////////////////////////////////////
// TheoryArray Public Methods                                                //
///////////////////////////////////////////////////////////////////////////////


TheoryArray::TheoryArray(TheoryCore* core)
  : Theory(core, "Arrays"), d_reads(core->getCM()->getCurrentContext()),
    d_applicationsInModel(core->getFlags()["applications"].getBool()),
    d_liftReadIte(core->getFlags()["liftReadIte"].getBool())
{
  d_rules = createProofRules();

  // Register new local kinds with ExprManager
  getEM()->newKind(ARRAY, "_ARRAY", true);
  getEM()->newKind(READ, "_READ");
  getEM()->newKind(WRITE, "_WRITE");
  getEM()->newKind(ARRAY_LITERAL, "_ARRAY_LITERAL");

  vector<int> kinds;
  kinds.push_back(ARRAY);
  kinds.push_back(READ);
  kinds.push_back(WRITE);

  kinds.push_back(ARRAY_LITERAL);

  registerTheory(this, kinds);
}


// Destructor: delete the proof rules class if it's present
TheoryArray::~TheoryArray() {
  if(d_rules != NULL) delete d_rules;
}


Theorem TheoryArray::rewrite(const Expr& e)
{
  Theorem thm;
  if (isRead(e)) {
    switch(e[0].getKind()) {
      case WRITE:
	thm = d_rules->rewriteReadWrite(e);
	return transitivityRule(thm, simplify(thm.getRHS()));
      case ARRAY_LITERAL: {
	IF_DEBUG(debugger.counter("Read array literals")++);
	thm = d_rules->readArrayLiteral(e);
	return transitivityRule(thm, simplify(thm.getRHS()));
      }
      case ITE: {
        if (d_liftReadIte) {
          thm = d_rules->liftReadIte(e);
          return transitivityRule(thm, simplify(thm.getRHS()));
        }
      }
      default: {
	const Theorem& rep = e.getRep();
	if (rep.isNull()) return reflexivityRule(e);
	else return symmetryRule(rep);
      }
    }
  }
  else if (!e.isTerm()) {
    if (e.isEq() && e[0].isAtomic() && e[1].isAtomic() && isWrite(e[0])) {
      Expr left = e[0], right = e[1];
      int leftWrites = 1, rightWrites = 0;

      // Count nested writes
      Expr e1 = left[0];
      while (isWrite(e1)) { leftWrites++; e1 = e1[0]; }

      Expr e2 = right;
      while (isWrite(e2)) { rightWrites++; e2 = e2[0]; }

      if (rightWrites == 0) {
	if (e1 == e2) {
	  thm = d_rules->rewriteSameStore(e, leftWrites);
	  return transitivityRule(thm, simplify(thm.getRHS()));
	}
	else {
	  e.setRewriteNormal();
	  return reflexivityRule(e);
	}
      }

      if (leftWrites > rightWrites) {
	thm = getCommonRules()->rewriteUsingSymmetry(e);
	thm = transitivityRule(thm, d_rules->rewriteWriteWrite(thm.getRHS()));
      }
      else thm = d_rules->rewriteWriteWrite(e);
      return transitivityRule(thm, simplify(thm.getRHS()));
    }
    e.setRewriteNormal();
    return reflexivityRule(e);
  }
  else if (!e.isAtomic()) {
    e.setRewriteNormal();
    return reflexivityRule(e);
  }
  else if (isWrite(e)) {
    Expr store = e[0];
    while (isWrite(store)) store = store[0];
    DebugAssert(findExpr(e[2]) == e[2], "Expected own find");
    thm = simplify(Expr(READ, store, e[1]));
    if (thm.getRHS() == e[2]) {
      thm = d_rules->rewriteRedundantWrite1(thm, e);
      return transitivityRule(thm, simplify(thm.getRHS()));
    }
    if (isWrite(e[0])) {
      if (e[0][1] == e[1]) {
	return d_rules->rewriteRedundantWrite2(e);
      }
      if (e[0][1] > e[1]) {
	thm = d_rules->interchangeIndices(e);
	return transitivityRule(thm, simplify(thm.getRHS()));
      }
    }
    return reflexivityRule(e);
  }
  return reflexivityRule(e);
}


void TheoryArray::setup(const Expr& e)
{
  if (e.isNot() || e.isEq()) return;
  DebugAssert(e.isAtomic(), "e should be atomic");
  for (int k = 0; k < e.arity(); ++k) {
    e[k].addToNotify(this, e);
  }
  if (isRead(e)) {
    Theorem thm = reflexivityRule(e);
    e.setSig(thm);
    e.setRep(thm);
    // Record the read operator for concrete models
    TRACE("model", "TheoryArray: add array read ", e, "");
    d_reads.push_back(e);
  }
  else if (isWrite(e)) {
    // there is a hidden dependency of write(a,i,v) on read(a,i)
    Expr store = e[0];
    while (isWrite(store)) store = store[0];
    Expr r = simplifyExpr(Expr(READ, store, e[1]));
    theoryCore()->setupTerm(r, this, theoryCore()->getTheoremForTerm(e));
    DebugAssert(r.isAtomic(), "Should be atomic");
    DebugAssert(r != e[2], "Should have been rewritten");
    r.addToNotify(this, e);
  }
}


void TheoryArray::update(const Theorem& e, const Expr& d)
{
  int k, ar(d.arity());

  if (isRead(d)) {
    const Theorem& dEQdsig = d.getSig();
    if (!dEQdsig.isNull()) {
      Expr dsig = dEQdsig.getRHS();
      Theorem thm = updateHelper(d);
      Expr sigNew = thm.getRHS();
      if (sigNew == dsig) return;
      dsig.setRep(Theorem());
      if (isWrite(sigNew[0])) {
	thm = transitivityRule(thm, d_rules->rewriteReadWrite(sigNew));
	Theorem renameTheorem = renameExpr(d);
	enqueueFact(transitivityRule(symmetryRule(renameTheorem), thm));
	d.setSig(Theorem());
	enqueueFact(renameTheorem);
      }
      else {
	const Theorem& repEQsigNew = sigNew.getRep();
	if (!repEQsigNew.isNull()) {
	  d.setSig(Theorem());
	  enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
	}
	else {
	  for (k = 0; k < ar; ++k) {
	    if (sigNew[k] != dsig[k]) {
	      sigNew[k].addToNotify(this, d);
	    }
	  }
	  d.setSig(thm);
	  sigNew.setRep(thm);
	}
      }
    }
  }
  else {
    DebugAssert(isWrite(d), "Expected write: d = "+d.toString());
    if (find(d).getRHS() == d) {
      Theorem thm = updateHelper(d);
      Expr sigNew = thm.getRHS();

      Expr store = sigNew[0];
      while (isWrite(store)) store = store[0];

      // TODO: calling simplify from update is generally bad
      Theorem thm2 = simplify(Expr(READ, store, sigNew[1]));
      if (thm2.getRHS() == sigNew[2]) {
        thm = transitivityRule(thm,
                               d_rules->rewriteRedundantWrite1(thm2, sigNew));
        sigNew = thm.getRHS();
      }
      else if (isWrite(sigNew[0])) {
        if (sigNew[0][1] == sigNew[1]) {
          thm = transitivityRule(thm, d_rules->rewriteRedundantWrite2(sigNew));
          sigNew = thm.getRHS();
        }
        else if (sigNew[0][1] > sigNew[1]) {
          thm = transitivityRule(thm, d_rules->interchangeIndices(sigNew));
          sigNew = thm.getRHS();
        }
      }

      if (d == sigNew) {
	// Hidden dependency must have changed.  Update notify list.
        DebugAssert(!e.isNull(), "Shouldn't be possible");
	e.getRHS().addToNotify(this, d);
      }
      else if (sigNew.isAtomic()) {
 	assertEqualities(thm);
      }
      else {
 	Theorem renameTheorem = renameExpr(d);
 	enqueueFact(transitivityRule(symmetryRule(renameTheorem), thm));
 	assertEqualities(renameTheorem);
      }
    }
  }
}


Theorem TheoryArray::solve(const Theorem& eThm)
{
  const Expr& e = eThm.getExpr();
  DebugAssert(e.isEq(), "TheoryArray::solve("+e.toString()+")");
  if (isWrite(e[0])) {
    DebugAssert(!isWrite(e[1]), "Should have been rewritten: e = "
		+e.toString());
    return symmetryRule(eThm);
  }
  return eThm;
}


void TheoryArray::checkType(const Expr& e)
{
  switch (e.getKind()) {
    case ARRAY: {
      if (e.arity() != 2) throw Exception
          ("ARRAY type should have two arguments");
      Type t1(e[0]);
      if (t1.isBool()) throw Exception
          ("Array index types must be non-Boolean");
      if (t1.isFunction()) throw Exception
          ("Array index types cannot be functions");
      Type t2(e[1]);
      if (t2.isBool()) throw Exception
          ("Array value types must be non-Boolean");
      if (t2.isFunction()) throw Exception
          ("Array value types cannot be functions");
      break;
    }
    default:
      DebugAssert(false, "Unexpected kind in TheoryArray::checkType"
                  +getEM()->getKindName(e.getKind()));
  }

}


void TheoryArray::computeType(const Expr& e)
{
  switch (e.getKind()) {
    case READ: {
      DebugAssert(e.arity() == 2,"");
      Type arrType = e[0].getType();
      if (!isArray(arrType)) {
        arrType = getBaseType(arrType);
      }
      if (!isArray(arrType))
	throw TypecheckException
	  ("Expected an ARRAY type in\n\n  "
	   +e[0].toString()+"\n\nBut received this:\n\n  "
	   +arrType.toString()+"\n\nIn the expression:\n\n  "
	   +e.toString());
      Type idxType = getBaseType(e[1]);
      if(getBaseType(arrType[0]) != idxType && idxType != Type::anyType(getEM())) {
	throw TypecheckException
	  ("The type of index expression:\n\n  "
	   +idxType.toString()
	   +"\n\nDoes not match the ARRAY index type:\n\n  "
	   +arrType[0].toString()
	   +"\n\nIn the expression: "+e.toString());
      }
      e.setType(arrType[1]);
      break;
    }
    case WRITE: {
      DebugAssert(e.arity() == 3,"");
      Type arrType = e[0].getType();
      if (!isArray(arrType)) {
        arrType = getBaseType(arrType);
      }
      Type idxType = getBaseType(e[1]);
      Type valType = getBaseType(e[2]);
      if (!isArray(arrType))
	throw TypecheckException
	  ("Expected an ARRAY type in\n\n  "
	   +e[0].toString()+"\n\nBut received this:\n\n  "
	   +arrType.toString()+"\n\nIn the expression:\n\n  "
	   +e.toString());
      bool idxCorrect = getBaseType(arrType[0]) == idxType || idxType == Type::anyType(getEM());
      bool valCorrect = getBaseType(arrType[1]) == valType || valType == Type::anyType(getEM());;
      if(!idxCorrect) {
	throw TypecheckException
	  ("The type of index expression:\n\n  "
	   +idxType.toString()
	   +"\n\nDoes not match the ARRAY's type index:\n\n  "
	   +arrType[0].toString()
	   +"\n\nIn the expression: "+e.toString());
      }
      if(!valCorrect) {
	throw TypecheckException
	  ("The type of value expression:\n\n  "
	   +valType.toString()
	   +"\n\nDoes not match the ARRAY's value type:\n\n  "
	   +arrType[1].toString()
	   +"\n\nIn the expression: "+e.toString());
      }
      e.setType(arrType);
      break;
    }
    case ARRAY_LITERAL: {
      DebugAssert(e.isClosure(), "TheoryArray::computeType("+e.toString()+")");
      DebugAssert(e.getVars().size()==1,
		  "TheoryArray::computeType("+e.toString()+")");
      Type ind(e.getVars()[0].getType());
      e.setType(arrayType(ind, e.getBody().getType()));
      break;
    }
    default:
      DebugAssert(false,"Unexpected type");
      break;
  }
}


Type TheoryArray::computeBaseType(const Type& t) {
  const Expr& e = t.getExpr();
  DebugAssert(e.getKind()==ARRAY && e.arity() == 2,
	      "TheoryArray::computeBaseType("+t.toString()+")");
  vector<Expr> kids;
  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
    kids.push_back(getBaseType(Type(*i)).getExpr());
  }
  return Type(Expr(e.getOp(), kids));
}


void TheoryArray::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
  switch(e.getKind()) {
  case WRITE:
    // a WITH [i] := v -- report a, i and v as the model terms.
//     getModelTerm(e[1], v);
//     getModelTerm(e[2], v);
    v.push_back(e[0]);
    v.push_back(e[1]);
    v.push_back(e[2]);
    break;
  case READ:
    // For a[i], add the index i
    // getModelTerm(e[1], v);
    v.push_back(e[1]);
    // And continue to collect the reads a[i][j] (remember, e is of
    // ARRAY type)
  default:
    // For array terms, find all their reads
    if(e.getType().getExpr().getKind() == ARRAY) {
      for(CDList<Expr>::const_iterator i=d_reads.begin(), iend=d_reads.end();
	  i!=iend; ++i) {
	DebugAssert(isRead(*i) && (*i).arity()==2, "Bad array read: "
		    +(*i).toString());
	if((*i)[0] == e) {
	  // Add both the read operator a[i]
	  // getModelTerm(*i, v);
	  v.push_back(*i);
      // and the index 'i' to the model terms.  Reason: the index to
      // the array should better be a concrete value, and it might not
      // necessarily be in the current list of model terms.
	  // getModelTerm((*i)[1], v);
	  v.push_back((*i)[1]);
	}
      }
    }
    break;
  }
}


void TheoryArray::computeModel(const Expr& e, std::vector<Expr>& v) {
  static unsigned count(0); // For bound vars

  switch(e.getKind()) {
  case WRITE: {
    // We should already have a value for the original array
    Expr res(getModelValue(e[0]).getRHS());
    Expr ind(getEM()->newBoundVarExpr("arr_var", int2string(count++)));
    Type tp(e.getType());
    DebugAssert(isArray(tp) && tp.arity()==2,
		"TheoryArray::computeModel(WRITE)");
    ind.setType(tp[0]);
    res = rewrite(Expr(READ, res, ind)).getRHS();
    Expr indVal(getModelValue(e[1]).getRHS());
    Expr updVal(getModelValue(e[2]).getRHS());
    res = (ind.eqExpr(indVal)).iteExpr(updVal, res);
    res = arrayLiteral(ind, res);
    assignValue(e, res);
    v.push_back(e);
    break;
  }
//   case READ: {
//     // Get the assignment for the index
//     Expr idx(getModelValue(e[1]).getRHS());
//     // And the assignment for the 
//     var = read(idxThm.getRHS(), e[0]);
//   }
    // And continue to collect the reads a[i][j] (remember, e is of
    // ARRAY type)
  default: {
    // Assign 'e' a value later.
    v.push_back(e);
    // Map of e[i] to val for concrete values of i and val
    ExprHashMap<Expr> reads;
    // For array terms, find all their reads
    DebugAssert(getBaseType(e).getExpr().getKind() == ARRAY, "");

    for(CDList<Expr>::const_iterator i=d_reads.begin(), iend=d_reads.end();
	i!=iend; ++i) {
      TRACE("model", "TheoryArray::computeModel: read = ", *i, "");
      DebugAssert(isRead(*i) && (*i).arity()==2, "Bad array read: "
		  +(*i).toString());
      if((*i)[0] == e) {
	// Get the value of the index
	Theorem asst(getModelValue((*i)[1]));
	Expr var;
	if(asst.getLHS()!=asst.getRHS()) {
	  vector<Theorem> thms;
	  vector<unsigned> changed;
	  thms.push_back(asst);
	  changed.push_back(1);
	  Theorem subst(substitutivityRule(*i, changed, thms));
	  assignValue(transitivityRule(symmetryRule(subst),
				       getModelValue(*i)));
	  var = subst.getRHS();
	} else
	  var = *i;
	if(d_applicationsInModel) v.push_back(var);
	// Record it in the map
	Expr val(getModelValue(var).getRHS());
	DebugAssert(!val.isNull(), "TheoryArray::computeModel(): Variable "
		    +var.toString()+" has a Null value");
	reads[var] = val;
      }
    }
    // Create an array literal
    if(reads.size()==0) { // Leave the array uninterpreted
      assignValue(reflexivityRule(e));
    } else {
      // Bound var for the index
      Expr ind(getEM()->newBoundVarExpr("arr_var", int2string(count++)));
      Type tp(e.getType());
      DebugAssert(isArray(tp) && tp.arity()==2,
		  "TheoryArray::computeModel(WRITE)");
      ind.setType(tp[0]);
      ExprHashMap<Expr>::iterator i=reads.begin(), iend=reads.end();
      DebugAssert(i!=iend,
		  "TheoryArray::computeModel(): expected the reads "
		  "table be non-empty");
      // Use one of the concrete values as a default
      Expr res((*i).second);
      ++i;
      DebugAssert(!res.isNull(), "TheoryArray::computeModel()");
      for(; i!=iend; ++i) {
	// Optimization: if the current value is the same as that of the
	// next application, skip this case; i.e. keep 'res' instead of
	// building ite(cond, res, res).
	if((*i).second == res) continue;
	// ITE condition
	Expr cond = ind.eqExpr((*i).first[1]);
	res = cond.iteExpr((*i).second, res);
      }
      // Construct the array literal
      res = arrayLiteral(ind, res);
      assignValue(e, res);
    }
    break;
  }
  }
}


Expr TheoryArray::computeTCC(const Expr& e)
{
  Expr tcc(Theory::computeTCC(e));
  switch (e.getKind()) {
    case READ:
      DebugAssert(e.arity() == 2,"");
      return tcc.andExpr(getTypePred(e[0].getType()[0], e[1]));
    case WRITE: {
      DebugAssert(e.arity() == 3,"");
      Type arrType = e[0].getType();
      return rewriteAnd(getTypePred(arrType[0], e[1]).andExpr
                        (getTypePred(arrType[1], e[2])).andExpr(tcc)).getRHS();
    }
    case ARRAY_LITERAL: {
      return tcc;
    }
    default:
      DebugAssert(false,"TheoryArray::computeTCC: Unexpected expression: "
		  +e.toString());
      return tcc;
  }
}


///////////////////////////////////////////////////////////////////////////////
// Pretty-printing			                                     //
///////////////////////////////////////////////////////////////////////////////


ExprStream& TheoryArray::print(ExprStream& os, const Expr& e)
{
  d_theoryUsed = true;
  if (theoryCore()->getTranslator()->printArrayExpr(os, e)) return os;
  switch(os.lang()) {
  case PRESENTATION_LANG:
    switch(e.getKind()) {
    case READ:
      if(e.arity() == 1)
	os << "[" << push << e[0] << push << "]";
      else
	os << e[0] << "[" << push << e[1] << push << "]";
      break;
    case WRITE:
      os << "(" << push << e[0] << space << "WITH [" 
	 << push << e[1] << "] := " << push << e[2] << push << ")";
      break;
    case ARRAY:
      os << "ARRAY" << space << e[0] << space << "OF" << space << e[1];
      break;
    case ARRAY_LITERAL:
      if(e.isClosure()) {
	const vector<Expr>& vars = e.getVars();
	const Expr& body = e.getBody();
	os << "(" << push << "ARRAY" << space << "(" << push;
	bool first(true);
	for(size_t i=0; i<vars.size(); ++i) {
	  if(first) first=false;
	  else os << push << "," << pop << space;
	  os << vars[i];
	  if(vars[i].isVar())
	    os << ":" << space << pushdag << vars[i].getType() << popdag;
	}
	os << push << "):" << pop << pop << space << body << push << ")";
      } else
	e.printAST(os);
      break;
    default:
      // Print the top node in the default LISP format, continue with
      // pretty-printing for children.
      e.printAST(os);
    }
    break; // end of case PRESENTATION_LANGUAGE
  case SMTLIB_LANG:
    switch(e.getKind()) {
    case READ:
      if(e.arity() == 2)
	os << "(" << push << "select" << space << e[0]
	   << space << e[1] << push << ")";
      else
	e.printAST(os);
      break;
    case WRITE:
      if(e.arity() == 3)
	os << "(" << push << "store" << space << e[0]
	   << space << e[1] << space << e[2] << push << ")";
      else
	e.printAST(os);
      break;
    case ARRAY:
      throw SmtlibException("ARRAY should be handled by printArrayExpr");
      break;      
    default:
      throw SmtlibException("TheoryArray::print: default not supported");
      // Print the top node in the default LISP format, continue with
      // pretty-printing for children.
      e.printAST(os);
    }
    break; // end of case LISP_LANGUAGE
  case LISP_LANG:
    switch(e.getKind()) {
    case READ:
      if(e.arity() == 2)
	os << "(" << push << "READ" << space << e[0]
	   << space << e[1] << push << ")";
      else
	e.printAST(os);
      break;
    case WRITE:
      if(e.arity() == 3)
	os << "(" << push << "WRITE" << space << e[0]
	   << space << e[1] << space << e[2] << push << ")";
      else
	e.printAST(os);
      break;
    case ARRAY:
      os << "(" << push << "ARRAY" << space << e[0]
	 << space << e[1] << push << ")";
      break;      
    default:
      // Print the top node in the default LISP format, continue with
      // pretty-printing for children.
      e.printAST(os);
    }
    break; // end of case LISP_LANGUAGE
  default:
    // Print the top node in the default LISP format, continue with
    // pretty-printing for children.
    e.printAST(os);
  }
  return os;
}

//////////////////////////////////////////////////////////////////////////////
//parseExprOp:
//translating special Exprs to regular EXPR??
///////////////////////////////////////////////////////////////////////////////
Expr
TheoryArray::parseExprOp(const Expr& e) {
  //  TRACE("parser", "TheoryArray::parseExprOp(", e, ")");
  // If the expression is not a list, it must have been already
  // parsed, so just return it as is.
  if(RAW_LIST != e.getKind()) return e;

  DebugAssert(e.arity() > 0,
	      "TheoryArray::parseExprOp:\n e = "+e.toString());
  
  const Expr& c1 = e[0][0];
  int kind = getEM()->getKind(c1.getString());
  switch(kind) {
    case READ: 
      if(!(e.arity() == 3))
	throw ParserException("Bad array access expression: "+e.toString());
      return Expr(READ, parseExpr(e[1]), parseExpr(e[2]));
    case WRITE: 
      if(!(e.arity() == 4))
	throw ParserException("Bad array update expression: "+e.toString());
      return Expr(WRITE, parseExpr(e[1]), parseExpr(e[2]), parseExpr(e[3]));
    case ARRAY: { 
      vector<Expr> k;
      Expr::iterator i = e.begin(), iend=e.end();
      // Skip first element of the vector of kids in 'e'.
      // The first element is the operator.
      ++i; 
      // Parse the kids of e and push them into the vector 'k'
      for(; i!=iend; ++i) 
        k.push_back(parseExpr(*i));
      return Expr(kind, k, e.getEM());
      break;
    }
    case ARRAY_LITERAL: { // (ARRAY (v tp1) body)
      if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() == 2))
	throw ParserException("Bad ARRAY literal expression: "+e.toString());
      const Expr& varPair = e[1];
      if(varPair.getKind() != RAW_LIST)
	throw ParserException("Bad variable declaration block in ARRAY "
			      "literal expression: "+varPair.toString()+
			      "\n e = "+e.toString());
      if(varPair[0].getKind() != ID)
	throw ParserException("Bad variable declaration in ARRAY"
			      "literal expression: "+varPair.toString()+
			      "\n e = "+e.toString());
      Type varTp(parseExpr(varPair[1]));
      vector<Expr> var;
      var.push_back(addBoundVar(varPair[0][0].getString(), varTp));
      Expr body(parseExpr(e[2]));
      // Build the resulting Expr as (LAMBDA (vars) body)
      return getEM()->newClosureExpr(ARRAY_LITERAL, var, body);
      break;
    }
    default:
      DebugAssert(false,
	  	  "TheoryArray::parseExprOp: wrong type: "
		  + e.toString());
    break;
  }
  return e;
}

namespace CVC3 {

Expr arrayLiteral(const Expr& ind, const Expr& body) {
  vector<Expr> vars;
  vars.push_back(ind);
  return body.getEM()->newClosureExpr(ARRAY_LITERAL, vars, body);
}

} // end of namespace CVC3