CVC3

theory_array.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_array.cpp
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Thu Feb 27 00:38:55 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 
00022 #include "theory_array.h"
00023 #include "theory_bitvector.h"
00024 #include "array_proof_rules.h"
00025 #include "typecheck_exception.h"
00026 #include "parser_exception.h"
00027 #include "smtlib_exception.h"
00028 #include "theory_core.h"
00029 #include "command_line_flags.h"
00030 #include "translator.h"
00031 
00032 
00033 using namespace std;
00034 using namespace CVC3;
00035 
00036 
00037 ///////////////////////////////////////////////////////////////////////////////
00038 // TheoryArray Public Methods                                                //
00039 ///////////////////////////////////////////////////////////////////////////////
00040 
00041 
00042 TheoryArray::TheoryArray(TheoryCore* core)
00043   : Theory(core, "Arrays"), d_reads(core->getCM()->getCurrentContext()),
00044     d_applicationsInModel(core->getFlags()["applications"].getBool()),
00045     d_liftReadIte(core->getFlags()["liftReadIte"].getBool()),
00046     d_sharedSubterms(core->getCM()->getCurrentContext()),
00047     d_sharedSubtermsList(core->getCM()->getCurrentContext()),
00048     d_index(core->getCM()->getCurrentContext(), 0, 0),
00049     d_sharedIdx1(core->getCM()->getCurrentContext(), 0, 0),
00050     d_sharedIdx2(core->getCM()->getCurrentContext(), 0, 0),
00051     d_inCheckSat(0)
00052 {
00053   d_rules = createProofRules();
00054 
00055   // Register new local kinds with ExprManager
00056   getEM()->newKind(ARRAY, "_ARRAY", true);
00057   getEM()->newKind(READ, "_READ");
00058   getEM()->newKind(WRITE, "_WRITE");
00059   getEM()->newKind(ARRAY_LITERAL, "_ARRAY_LITERAL");
00060 
00061   vector<int> kinds;
00062   kinds.push_back(ARRAY);
00063   kinds.push_back(READ);
00064   kinds.push_back(WRITE);
00065 
00066   kinds.push_back(ARRAY_LITERAL);
00067 
00068   registerTheory(this, kinds);
00069 }
00070 
00071 
00072 // Destructor: delete the proof rules class if it's present
00073 TheoryArray::~TheoryArray() {
00074   if(d_rules != NULL) delete d_rules;
00075 }
00076 
00077 
00078 void TheoryArray::addSharedTerm(const Expr& e)
00079 {
00080   if (d_sharedSubterms.count(e) > 0) return;
00081 
00082   TRACE("arrAddSharedTerm", "TheoryArray::addSharedTerm(", e.toString(), ")");
00083 
00084   // Cache all shared terms
00085   d_sharedSubterms[e]=e;
00086 
00087   // Make sure we get notified if shared term is assigned to something else
00088   // We need this because we only check non-array-normalized (nan) shared terms,
00089   // so if a variable gets set to a nan term, we will need to know about it.
00090   e.addToNotify(this, Expr());
00091 
00092   if (isWrite(e) || (isRead(e) && isWrite(e[0]))) {
00093 
00094     // Children of shared terms better be shared so we can detect any failure of normalization
00095     for (int i = 0; i < e.arity(); ++i) addSharedTerm(e[i]);
00096 
00097     // Only check writes that are not normalized
00098     if (!isWrite(e) || e.notArrayNormalized()) {
00099       // Put in list to check during checkSat
00100       d_sharedSubtermsList.push_back(e);
00101     }
00102   }
00103 }
00104 
00105 
00106 void TheoryArray::assertFact(const Theorem& e)
00107 {
00108   const Expr& expr = e.getExpr();
00109   TRACE("arrAssertFact", "TheoryArray::assertFact(", e.getExpr().toString(), ")");
00110 
00111   switch (expr.getOpKind()) {
00112 
00113     case NOT:
00114       DebugAssert(expr[0].isEq(), "Unexpected negation");
00115 
00116       if (isArray(getBaseType(expr[0][0]))) {
00117         // For disequalities between arrays, do the polite thing, and introduce witnesses
00118         enqueueFact(d_rules->arrayNotEq(e));
00119         break;
00120       }
00121 
00122       // We can use the shared term mechanism here:
00123       // In checksat we will ensure that all shared terms are in a normal form
00124       // so if two are known to be equal, we will discover it
00125       addSharedTerm(expr[0][0]);
00126       addSharedTerm(expr[0][1]);
00127       
00128       break;
00129       
00130     case EQ:
00131       DebugAssert(theoryCore()->inUpdate() ||
00132                   (d_inCheckSat > 0) ||
00133                   !isWrite(expr[0]), "Invariant violated");
00134       break;
00135 
00136     default:
00137       FatalAssert(false, "Unexpected case");
00138       break;
00139   }
00140 }
00141 
00142 
00143 Expr findAtom(Expr e) {
00144   DebugAssert(e.arity() != 0, "Invariant Violated");
00145   int i;
00146   for (i = 0; i < e.arity(); ++i) {
00147     if (!e[i].isAtomic()) break;
00148   }
00149   if (e[i].isAbsAtomicFormula()) return e[i];
00150   return findAtom(e[i]);
00151 }
00152 
00153 
00154 void TheoryArray::checkSat(bool fullEffort)
00155 {
00156   if (fullEffort == true) {
00157     // Check that all non-array-normalized shared terms are normalized
00158     Theorem thm;
00159     for (; d_index < d_sharedSubtermsList.size(); d_index = d_index + 1) {
00160       Expr e = d_sharedSubtermsList[d_index];
00161 
00162       if (isRead(e)) {
00163         DebugAssert(isWrite(e[0]), "Expected read(write)");
00164 
00165         // This should be a signature without a find
00166         DebugAssert(!e.hasFind(), "Expected no find");
00167 
00168         // If this is no longer a valid signature, we can skip it
00169         if (!e.hasRep()) continue;
00170 
00171         // Check to see if we know whether indices are equal
00172         Expr ieq = e[0][1].eqExpr(e[1]);
00173         Theorem ieqSimp = simplify(ieq);
00174         if (!ieqSimp.getRHS().isBoolConst()) {
00175           // if not, split on equality of indices
00176           // TODO: really tricky optimization: maybe we can avoid this split
00177           // if both then and else are unknown terms?
00178           addSplitter(ieq);
00179           return;
00180         }
00181 
00182         // Get the representative for the signature
00183         Theorem repEqSig = e.getRep();
00184         DebugAssert(!repEqSig.isRefl(), "Expected non-self rep");
00185 
00186         // Apply the read over write rule
00187   thm = d_rules->rewriteReadWrite(e);
00188 
00189         // Carefully simplify
00190         thm = transitivityRule(thm, 
00191                                substitutivityRule(thm.getRHS(), 0, ieqSimp));
00192         thm = transitivityRule(thm, rewriteIte(thm.getRHS()));
00193 
00194         // Derive the new equality and simplify
00195         thm = transitivityRule(repEqSig, thm);
00196         thm = iffMP(thm, simplify(thm.getExpr()));
00197         Expr newExpr = thm.getExpr();
00198         if (newExpr.isTrue()) {
00199           // Fact is already known, continue
00200           continue;
00201         }
00202         else if (newExpr.isAbsAtomicFormula()) {
00203           enqueueFact(thm);
00204         }
00205         else {
00206           // expr is not atomic formula, so pick a splitter that will help make it atomic
00207           addSplitter(findAtom(newExpr));
00208         }
00209         return;
00210       }
00211 
00212       // OK, everything else should be a write
00213       DebugAssert(isWrite(e), "Expected Write");
00214       DebugAssert(e.notArrayNormalized(),
00215                   "Only non-normalized writes expected");
00216 
00217       // If write is not its own find, this means that the write
00218       // was normalized to something else already, so it's not relevant
00219       // any more
00220       if (find(e).getRHS() != e) continue;
00221 
00222       // First check for violation of redundantWrite1
00223       Expr store = e[0];
00224       while (isWrite(store)) store = store[0];
00225       DebugAssert(findExpr(e[2]) == e[2], "Expected own find");
00226       thm = simplify(Expr(READ, store, e[1]));
00227       if (thm.getRHS() == e[2]) {
00228         thm = d_rules->rewriteRedundantWrite1(thm, e);
00229       }
00230 
00231       // Then check for violation of redundantWrite2
00232       else if (isWrite(e[0]) && e[0][1] > e[1]) {
00233         thm = d_rules->interchangeIndices(e);
00234       }
00235 
00236       else {
00237         FatalAssert(false, "Unexpected expr");
00238         continue;
00239       }
00240 
00241       // Write needs to be normalized, see what its new normal form is:
00242       thm = transitivityRule(thm, simplify(thm.getRHS()));
00243       Expr newExpr = thm.getRHS();
00244 
00245       if (newExpr.isAtomic()) {
00246         // If the new normal form is atomic, go ahead and update the normal form directly
00247         ++d_inCheckSat;
00248         assertEqualities(thm);
00249         // To ensure updates are processed and checkSat gets called again
00250         enqueueFact(thm);
00251         --d_inCheckSat;
00252       }
00253       else {
00254         // normal form is not atomic, so pick a splitter that will help make it atomic
00255         addSplitter(findAtom(newExpr));
00256       }
00257       return;
00258     }
00259 
00260     // All the terms should be normalized now... Ok, lets split on the read
00261     // indices.
00262     TRACE("sharing", "checking shared terms, size = ", int2string(d_reads.size()), "");
00263     // Collect all the arrays and indices of interest
00264     ExprMap< hash_set<Expr> > reads_by_array;
00265     ExprMap< hash_set<Expr> > const_reads_by_array;
00266     for (unsigned i = 0; i < d_reads.size(); ++i) {
00267       Expr read = d_reads[i];
00268       if (read.getSig().isNull()) continue;
00269       if( d_sharedSubterms.find(read[1]) == d_sharedSubterms.end() ) continue;
00270       Expr read_array = getBaseArray(read[0]);
00271       if (read[1].getKind() != BVCONST) {
00272         hash_set<Expr>& reads = reads_by_array[read_array];
00273         reads.insert(read);
00274       } else {
00275         hash_set<Expr>& reads = const_reads_by_array[read_array];
00276         reads.insert(read);
00277       }
00278     }
00279 
00280     ExprMap< hash_set<Expr> >::iterator it = reads_by_array.begin();
00281     ExprMap< hash_set<Expr> >::iterator it_end = reads_by_array.end();
00282     for(; it != it_end; ++ it) {
00283       Expr array = it->first;
00284       hash_set<Expr>& reads_single_array = it->second;
00285 
00286       hash_set<Expr>::iterator read1_it = reads_single_array.begin();
00287       hash_set<Expr>::iterator read1_end = reads_single_array.end();
00288       for (; read1_it != read1_end; ++ read1_it) {
00289         Expr read1 = (*read1_it);
00290         Expr x_k = read1[1];
00291         Expr read1_find = find(read1).getRHS();
00292         // The non-const reads arrays
00293         hash_set<Expr>::iterator read2_it = reads_single_array.begin();
00294         for (; read2_it != read1_it; ++ read2_it) {
00295           Expr read2 = (*read2_it);
00296           Expr read2_find = find(read2).getRHS();
00297           if (read1_find != read2_find) {
00298             Theorem simpl = simplify(read1.eqExpr(read2));
00299             Expr y_k = read2[1];
00300             Expr eq = x_k.eqExpr(y_k);
00301             if( !simplify(eq).getRHS().isBoolConst() ) {
00302               if (simpl.getRHS().isFalse()) {
00303                 enqueueFact(d_rules->propagateIndexDiseq(simpl));
00304               } else {
00305                 TRACE("sharing", "from " + read2.toString(), "with find = ", find(read2).getRHS());
00306                 TRACE("sharing", "from " + read1.toString(), "with find = ", find(read1).getRHS());
00307                 TRACE("sharing", "splitting " + y_k.toString(), " and ", x_k.toString());
00308                 addSplitter(eq);
00309               }
00310             }
00311           }
00312         }
00313         // The const reads arrays
00314         hash_set<Expr>& const_reads_single_array = const_reads_by_array[array];
00315         read2_it = const_reads_single_array.begin();
00316         hash_set<Expr>::iterator read2_it_end = const_reads_single_array.end();
00317         for (; read2_it != read2_it_end; ++ read2_it) {
00318           Expr read2 = (*read2_it);
00319           Expr read2_find = find(read2).getRHS();
00320           if (read1_find != read2_find) {
00321             Theorem simpl = simplify(read1.eqExpr(read2));
00322             Expr y_k = read2[1];
00323             Expr eq = x_k.eqExpr(y_k);
00324             if( !simplify(eq).getRHS().isBoolConst() ) {
00325               if (simpl.getRHS().isFalse()) {
00326                 enqueueFact(d_rules->propagateIndexDiseq(simpl));
00327               } else {
00328                 TRACE("sharing", "from " + read2.toString(), "with find = ", find(read2).getRHS());
00329                 TRACE("sharing", "from " + read1.toString(), "with find = ", find(read1).getRHS());
00330                 TRACE("sharing", "splitting " + y_k.toString(), " and ", x_k.toString());
00331                 addSplitter(eq);
00332               }
00333             }
00334           }
00335         }
00336       }
00337     }
00338     TRACE("sharing", "checking shared terms, done", int2string(d_reads.size()), "");
00339   }
00340 }
00341 
00342 
00343 // w(...,i,v1,...,) => w(......,i,v1')
00344 // Returns Null Theorem if index does not appear
00345 Theorem TheoryArray::pullIndex(const Expr& e, const Expr& index)
00346 {
00347   DebugAssert(isWrite(e), "Expected write");
00348 
00349   if (e[1] == index) return reflexivityRule(e);
00350 
00351   // Index does not appear
00352   if (!isWrite(e[0])) return Theorem();
00353 
00354   // Index is at next nesting level
00355   if (e[0][1] == index) {
00356     return d_rules->interchangeIndices(e);
00357   }
00358 
00359   // Index is (possibly) at deeper nesting level
00360   Theorem thm = pullIndex(e[0], index);
00361   if (thm.isNull()) return thm;
00362   thm = substitutivityRule(e, 0, thm);
00363   thm = transitivityRule(thm, d_rules->interchangeIndices(thm.getRHS()));
00364   return thm;
00365 }
00366 
00367 
00368 Theorem TheoryArray::rewrite(const Expr& e)
00369 {
00370   Theorem thm;
00371   switch (e.getKind()) {
00372     case READ: {
00373       switch(e[0].getKind()) {
00374         case WRITE:
00375           thm = d_rules->rewriteReadWrite(e);
00376           return transitivityRule(thm, simplify(thm.getRHS()));
00377         case ARRAY_LITERAL: {
00378           IF_DEBUG(debugger.counter("Read array literals")++;)
00379             thm = d_rules->readArrayLiteral(e);
00380           return transitivityRule(thm, simplify(thm.getRHS()));
00381         }
00382         case ITE: {
00383           if (d_liftReadIte) {
00384             thm = d_rules->liftReadIte(e);
00385             return transitivityRule(thm, simplify(thm.getRHS()));
00386           }
00387           e.setRewriteNormal();
00388           return reflexivityRule(e);
00389         }
00390         default: {
00391           break;
00392         }
00393       }
00394       const Theorem& rep = e.getRep();
00395       if (rep.isNull()) return reflexivityRule(e);
00396       else return symmetryRule(rep);
00397     }
00398     case EQ:
00399       //      if (e[0].isAtomic() && e[1].isAtomic() && isWrite(e[0])) {
00400       if (isWrite(e[0])) {
00401         Expr left = e[0], right = e[1];
00402         int leftWrites = 1, rightWrites = 0;
00403 
00404         // Count nested writes
00405         Expr e1 = left[0];
00406         while (isWrite(e1)) { leftWrites++; e1 = e1[0]; }
00407 
00408         Expr e2 = right;
00409         while (isWrite(e2)) { rightWrites++; e2 = e2[0]; }
00410 
00411         if (rightWrites == 0) {
00412           if (e1 == e2) {
00413             thm = d_rules->rewriteSameStore(e, leftWrites);
00414             return transitivityRule(thm, simplify(thm.getRHS()));
00415           }
00416           else {
00417             e.setRewriteNormal();
00418             return reflexivityRule(e);
00419           }
00420         }
00421         if (leftWrites > rightWrites) {
00422           thm = getCommonRules()->rewriteUsingSymmetry(e);
00423           thm = transitivityRule(thm, d_rules->rewriteWriteWrite(thm.getRHS()));
00424         }
00425         else thm = d_rules->rewriteWriteWrite(e);
00426         return transitivityRule(thm, simplify(thm.getRHS()));
00427       }
00428       e.setRewriteNormal();
00429       return reflexivityRule(e);
00430     case NOT:
00431       e.setRewriteNormal();
00432       return reflexivityRule(e);
00433     case WRITE: {
00434 //       if (!e.isAtomic()) {
00435 //         e.setRewriteNormal();
00436 //         return reflexivityRule(e);
00437 //       }
00438       const Expr& store = e[0];
00439       // Enabling this slows stuff down a lot
00440       if (!isWrite(store)) {
00441         DebugAssert(findExpr(e[2]) == e[2], "Expected own find");
00442         if (isRead(e[2]) && e[2][0] == store && e[2][1] == e[1]) {
00443           thm = d_rules->rewriteRedundantWrite1(reflexivityRule(e[2]), e);
00444           return transitivityRule(thm, simplify(thm.getRHS()));
00445         }
00446         e.setRewriteNormal();
00447         return reflexivityRule(e);
00448       }
00449       else {
00450         //      if (isWrite(store)) {
00451         thm = pullIndex(store,e[1]);
00452         if (!thm.isNull()) {
00453           if (thm.isRefl()) {
00454             return d_rules->rewriteRedundantWrite2(e);
00455           }
00456           thm = substitutivityRule(e,0,thm);
00457           thm = transitivityRule(thm, 
00458                                  d_rules->rewriteRedundantWrite2(thm.getRHS()));
00459           return transitivityRule(thm, simplify(thm.getRHS()));
00460         }
00461         if (store[1] > e[1]) {
00462           // Only do this rewrite if the result is atomic
00463           // (avoid too many ITEs)
00464           thm = d_rules->interchangeIndices(e);
00465           thm = transitivityRule(thm, simplify(thm.getRHS()));
00466           if (thm.getRHS().isAtomic()) {
00467             return thm;
00468           }
00469           // not normal because might be possible to interchange later
00470           return reflexivityRule(e);
00471         }
00472       }
00473       e.setRewriteNormal();
00474       return reflexivityRule(e);
00475     }
00476     case ARRAY_LITERAL:
00477       e.setRewriteNormal();
00478       return reflexivityRule(e);
00479     default:
00480       DebugAssert(e.isVar() && isArray(getBaseType(e)),
00481                   "Unexpected default case");
00482       e.setRewriteNormal();
00483       return reflexivityRule(e);
00484   }
00485   FatalAssert(false, "should be unreachable");
00486   return reflexivityRule(e);
00487 }
00488 
00489 
00490 void TheoryArray::setup(const Expr& e)
00491 {
00492   if (e.isNot() || e.isEq()) return;
00493   DebugAssert(e.isAtomic(), "e should be atomic");
00494   for (int k = 0; k < e.arity(); ++k) {
00495     e[k].addToNotify(this, e);
00496   }
00497   if (isRead(e)) {
00498     if (e.getType().card() != CARD_INFINITE) {
00499       addSharedTerm(e);
00500       theoryOf(e.getType())->addSharedTerm(e);
00501     }
00502     Theorem thm = reflexivityRule(e);
00503     e.setSig(thm);
00504     e.setRep(thm);
00505     e.setUsesCC();
00506     DebugAssert(!isWrite(e[0]), "expected no read of writes");
00507     // Record the read operator for concrete models
00508     TRACE("model", "TheoryArray: add array read ", e, "");
00509     d_reads.push_back(e);
00510   }
00511   else if (isWrite(e)) {
00512     Expr store = e[0];
00513 
00514     if (isWrite(store)) {
00515       // check interchangeIndices invariant
00516       if (store[1] > e[1]) {
00517         e.setNotArrayNormalized();
00518         if (d_sharedSubterms.count(e) > 0) {
00519           // write was identified as a shared term before it was setup: add it to list to check
00520           d_sharedSubtermsList.push_back(e);
00521         }
00522       }
00523       // redundantWrite2 invariant should hold
00524       DebugAssert(pullIndex(store, e[1]).isNull(),
00525                   "Unexpected non-array-normalized term in setup");
00526     }
00527 
00528     // check redundantWrite1 invariant
00529     // there is a hidden dependency of write(a,i,v) on read(a,i)
00530     while (isWrite(store)) store = store[0];
00531     // Need to simplify, not just take find: read could be a signature
00532     Expr r = simplifyExpr(Expr(READ, store, e[1]));
00533     theoryCore()->setupTerm(r, this, theoryCore()->getTheoremForTerm(e));
00534     DebugAssert(r.isAtomic(), "Should be atomic");
00535     DebugAssert(findExpr(e[2]) == e[2], "Expected own find");
00536     if (r == e[2] && !e.notArrayNormalized()) {
00537       e.setNotArrayNormalized();
00538       if (d_sharedSubterms.count(e) > 0) {
00539         // write was identified as a shared term before it was setup: add it to list to check
00540         d_sharedSubtermsList.push_back(e);
00541       }
00542     }
00543     else {
00544       r.addToNotify(this, e);
00545     }
00546   }
00547 }
00548 
00549 
00550 void TheoryArray::update(const Theorem& e, const Expr& d)
00551 {
00552   if (inconsistent()) return;
00553 
00554   if (d.isNull()) {
00555     // d is a shared term
00556     // we want to mark the new find representative as a shared term too
00557     Expr lhs = e.getLHS();
00558     Expr rhs = e.getRHS();
00559     DebugAssert(d_sharedSubterms.find(lhs) != d_sharedSubterms.end(),
00560                 "Expected lhs to be shared");
00561     CDMap<Expr,Expr>::iterator it = d_sharedSubterms.find(rhs);
00562     if (it == d_sharedSubterms.end()) {
00563       addSharedTerm(rhs);
00564     }
00565     return;
00566   }
00567 
00568   int k, ar(d.arity());
00569 
00570   if (isRead(d)) {
00571     const Theorem& dEQdsig = d.getSig();
00572     if (!dEQdsig.isNull()) {
00573       Expr dsig = dEQdsig.getRHS();
00574       Theorem thm = updateHelper(d);
00575       Expr sigNew = thm.getRHS();
00576       if (sigNew == dsig) return;
00577       dsig.setRep(Theorem());
00578       if (isWrite(sigNew[0])) {
00579         // This is the tricky case.
00580         // 
00581     Theorem thm2 = d_rules->rewriteReadWrite(sigNew);
00582         thm2 = transitivityRule(thm2, simplify(thm2.getRHS()));
00583         if (thm2.getRHS().isAtomic()) {
00584           // If read over write simplifies, go ahead and assert the equality
00585           enqueueFact(transitivityRule(thm, thm2));
00586         }
00587         else {
00588           // Otherwise, delay processing until checkSat
00589           addSharedTerm(sigNew);
00590         }
00591         //        thm = d_rules->rewriteReadWrite2(sigNew);
00592         //  Theorem renameTheorem = renameExpr(d);
00593         //  enqueueFact(transitivityRule(symmetryRule(renameTheorem), thm));
00594         //  d.setSig(Theorem());
00595         //  enqueueFact(thm);
00596         //  enqueueFact(renameTheorem);
00597       }
00598       //      else {
00599 
00600       // Update the signature in all cases
00601       Theorem repEQsigNew = sigNew.getRep();
00602   if (!repEQsigNew.isNull()) {
00603     d.setSig(Theorem());
00604     enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
00605   }
00606   else {
00607     for (k = 0; k < ar; ++k) {
00608       if (sigNew[k] != dsig[k]) {
00609         sigNew[k].addToNotify(this, d);
00610       }
00611     }
00612     d.setSig(thm);
00613     sigNew.setRep(thm);
00614           getEM()->invalidateSimpCache();
00615   }
00616         //      }
00617     }
00618     return;
00619   }
00620 
00621   DebugAssert(isWrite(d), "Expected write: d = "+d.toString());
00622   if (find(d).getRHS() != d) return;
00623 
00624   Theorem thm = updateHelper(d);
00625   Expr sigNew = thm.getRHS();
00626 
00627   // TODO: better normalization in some cases
00628   Expr store = sigNew[0];
00629   if (!isWrite(store)) {
00630     Theorem thm2 = find(Expr(READ, store, sigNew[1]));
00631     if (thm2.getRHS() == sigNew[2]) {
00632       thm = transitivityRule(thm,
00633                              d_rules->rewriteRedundantWrite1(thm2, sigNew));
00634       sigNew = thm.getRHS();
00635     }
00636   }
00637   else {
00638     // TODO: this check is expensive, it seems
00639     Theorem thm2 = pullIndex(store,sigNew[1]);
00640     if (!thm2.isNull()) {
00641       if (thm2.isRefl()) {
00642         thm = transitivityRule(thm,
00643                                d_rules->rewriteRedundantWrite2(sigNew));
00644       }
00645       else {
00646         thm2 = substitutivityRule(sigNew,0,thm2);
00647         thm2 = transitivityRule(thm2,
00648                                 d_rules->rewriteRedundantWrite2(thm2.getRHS()));
00649         thm = transitivityRule(thm, thm2);
00650       }
00651       sigNew = thm.getRHS();
00652       store = sigNew[0];
00653     }
00654 
00655     if (isWrite(store) && (store[1] > sigNew[1])) {
00656       thm2 = d_rules->interchangeIndices(sigNew);
00657       thm2 = transitivityRule(thm2, simplify(thm2.getRHS()));
00658       // Only update if result is atomic
00659       if (thm2.getRHS().isAtomic()) {
00660         thm = transitivityRule(thm, thm2);
00661         sigNew = thm.getRHS();
00662         // no need to update store because d == sigNew
00663         // case only happens if sigNew hasn't changed
00664       }
00665     }
00666   }
00667 
00668   if (d == sigNew) {
00669     // Hidden dependency must have changed
00670     while (isWrite(store)) store = store[0];
00671     Expr r = e.getRHS();
00672     if (r == d[2]) {
00673       // no need to update notify list as we are already on list of d[2]
00674       if (!d.notArrayNormalized()) {
00675         d.setNotArrayNormalized();
00676         if (d_sharedSubterms.count(d) > 0) {
00677           // write has become non-normalized: add it to list to check
00678           d_sharedSubtermsList.push_back(d);
00679         }
00680       }
00681     }
00682     else {
00683       // update the notify list
00684       r.addToNotify(this, d);
00685     }
00686     return;
00687   }
00688 
00689   DebugAssert(sigNew.isAtomic(), "Expected atomic formula");
00690   // Since we aren't doing a full normalization here, it's possible that sigNew is not normal
00691   // and so it might have a different find.  In that case, the find should be the new rhs.
00692   if (sigNew.hasFind()) {
00693     Theorem findThm = findRef(sigNew);
00694     if (!findThm.isRefl()) {
00695       thm = transitivityRule(thm, findThm);
00696     }
00697     assertEqualities(thm);
00698     return;
00699   }
00700 
00701   // If it doesn't have a find at all, it needs to be simplified
00702   Theorem simpThm = simplify(sigNew);
00703   thm = transitivityRule(thm, simpThm);
00704   sigNew = thm.getRHS();
00705   if (sigNew.isAtomic()) {
00706     assertEqualities(thm);
00707   }
00708   else {
00709     // Simplify could maybe? introduce case splits in the expression.  Handle this by renaminig
00710     Theorem renameTheorem = renameExpr(d);
00711     enqueueFact(transitivityRule(symmetryRule(renameTheorem), thm));
00712     assertEqualities(renameTheorem);
00713   }
00714 
00715 }
00716 
00717 
00718 Theorem TheoryArray::solve(const Theorem& eThm)
00719 {
00720   const Expr& e = eThm.getExpr();
00721   DebugAssert(e.isEq(), "TheoryArray::solve("+e.toString()+")");
00722   if (isWrite(e[0])) {
00723     DebugAssert(!isWrite(e[1]), "Should have been rewritten: e = "
00724     +e.toString());
00725     return symmetryRule(eThm);
00726   }
00727   return eThm;
00728 }
00729 
00730 
00731 void TheoryArray::checkType(const Expr& e)
00732 {
00733   switch (e.getKind()) {
00734     case ARRAY: {
00735       if (e.arity() != 2) throw Exception
00736           ("ARRAY type should have two arguments");
00737       Type t1(e[0]);
00738       if (t1.isBool()) throw Exception
00739           ("Array index types must be non-Boolean");
00740       if (t1.isFunction()) throw Exception
00741           ("Array index types cannot be functions");
00742       Type t2(e[1]);
00743       if (t2.isBool()) throw Exception
00744           ("Array value types must be non-Boolean");
00745       if (t2.isFunction()) throw Exception
00746           ("Array value types cannot be functions");
00747       break;
00748     }
00749     default:
00750       DebugAssert(false, "Unexpected kind in TheoryArray::checkType"
00751                   +getEM()->getKindName(e.getKind()));
00752   }
00753 
00754 }
00755 
00756 
00757 Cardinality TheoryArray::finiteTypeInfo(Expr& e, Unsigned& n,
00758                                         bool enumerate, bool computeSize)
00759 {
00760   Cardinality card = CARD_INFINITE;
00761   switch (e.getKind()) {
00762     case ARRAY: {
00763       Type typeIndex = Type(e[0]);
00764       Type typeElem = Type(e[1]);
00765       if (typeElem.card() == CARD_FINITE &&
00766           (typeIndex.card() == CARD_FINITE || typeElem.sizeFinite() == 1)) {
00767 
00768         card = CARD_FINITE;
00769 
00770         if (enumerate) {
00771           // Right now, we only enumerate the first element for finite arrays
00772           if (n == 0) {
00773             Expr ind(getEM()->newBoundVarExpr(Type(e[0])));
00774             e = arrayLiteral(ind, typeElem.enumerateFinite(0));
00775           }
00776           else e = Expr();
00777         }
00778 
00779         if (computeSize) {
00780           n = 0;
00781           Unsigned sizeElem = typeElem.sizeFinite();
00782           if (sizeElem == 1) {
00783             n = 1;
00784           }
00785           else if (sizeElem > 1) {
00786             Unsigned sizeIndex = typeIndex.sizeFinite();
00787             if (sizeIndex > 0) {
00788               n = sizeElem;
00789               while (--sizeIndex > 0) {
00790                 n = n * sizeElem;
00791                 if (n > 1000000) {
00792                   // if it starts getting too big, just return 0
00793                   n = 0;
00794                   break;
00795                 }
00796               }
00797             }
00798           }
00799         }
00800       }
00801       break;
00802     }
00803     default:
00804       break;
00805   }
00806   return card;
00807 }
00808 
00809 
00810 void TheoryArray::computeType(const Expr& e)
00811 {
00812   switch (e.getKind()) {
00813     case READ: {
00814       DebugAssert(e.arity() == 2,"");
00815       Type arrType = e[0].getType();
00816       if (!isArray(arrType)) {
00817         arrType = getBaseType(arrType);
00818       }
00819       if (!isArray(arrType))
00820   throw TypecheckException
00821     ("Expected an ARRAY type in\n\n  "
00822      +e[0].toString()+"\n\nBut received this:\n\n  "
00823      +arrType.toString()+"\n\nIn the expression:\n\n  "
00824      +e.toString());
00825       Type idxType = getBaseType(e[1]);
00826       if(getBaseType(arrType[0]) != idxType && idxType != Type::anyType(getEM())) {
00827   throw TypecheckException
00828     ("The type of index expression:\n\n  "
00829      +idxType.toString()
00830      +"\n\nDoes not match the ARRAY index type:\n\n  "
00831      +arrType[0].toString()
00832      +"\n\nIn the expression: "+e.toString());
00833       }
00834       e.setType(arrType[1]);
00835       break;
00836     }
00837     case WRITE: {
00838       DebugAssert(e.arity() == 3,"");
00839       Type arrType = e[0].getType();
00840       if (!isArray(arrType)) {
00841         arrType = getBaseType(arrType);
00842       }
00843       Type idxType = getBaseType(e[1]);
00844       Type valType = getBaseType(e[2]);
00845       if (!isArray(arrType))
00846   throw TypecheckException
00847     ("Expected an ARRAY type in\n\n  "
00848      +e[0].toString()+"\n\nBut received this:\n\n  "
00849      +arrType.toString()+"\n\nIn the expression:\n\n  "
00850      +e.toString());
00851       bool idxCorrect = getBaseType(arrType[0]) == idxType || idxType == Type::anyType(getEM());
00852       bool valCorrect = getBaseType(arrType[1]) == valType || valType == Type::anyType(getEM());;
00853       if(!idxCorrect) {
00854   throw TypecheckException
00855     ("The type of index expression:\n\n  "
00856      +idxType.toString()
00857      +"\n\nDoes not match the ARRAY's type index:\n\n  "
00858      +arrType[0].toString()
00859      +"\n\nIn the expression: "+e.toString());
00860       }
00861       if(!valCorrect) {
00862   throw TypecheckException
00863     ("The type of value expression:\n\n  "
00864      +valType.toString()
00865      +"\n\nDoes not match the ARRAY's value type:\n\n  "
00866      +arrType[1].toString()
00867      +"\n\nIn the expression: "+e.toString());
00868       }
00869       e.setType(arrType);
00870       break;
00871     }
00872     case ARRAY_LITERAL: {
00873       DebugAssert(e.isClosure(), "TheoryArray::computeType("+e.toString()+")");
00874       DebugAssert(e.getVars().size()==1,
00875       "TheoryArray::computeType("+e.toString()+")");
00876       Type ind(e.getVars()[0].getType());
00877       e.setType(arrayType(ind, e.getBody().getType()));
00878       break;
00879     }
00880     default:
00881       DebugAssert(false,"Unexpected type");
00882       break;
00883   }
00884 }
00885 
00886 
00887 Type TheoryArray::computeBaseType(const Type& t) {
00888   const Expr& e = t.getExpr();
00889   DebugAssert(e.getKind()==ARRAY && e.arity() == 2,
00890         "TheoryArray::computeBaseType("+t.toString()+")");
00891   vector<Expr> kids;
00892   for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00893     kids.push_back(getBaseType(Type(*i)).getExpr());
00894   }
00895   return Type(Expr(e.getOp(), kids));
00896 }
00897 
00898 
00899 void TheoryArray::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
00900   switch(e.getKind()) {
00901   case WRITE:
00902     // a WITH [i] := v -- report a, i and v as the model terms.
00903 //     getModelTerm(e[1], v);
00904 //     getModelTerm(e[2], v);
00905     v.push_back(e[0]);
00906     v.push_back(e[1]);
00907     v.push_back(e[2]);
00908     break;
00909   case READ:
00910     // For a[i], add the index i
00911     // getModelTerm(e[1], v);
00912     v.push_back(e[1]);
00913     // And continue to collect the reads a[i][j] (remember, e is of
00914     // ARRAY type)
00915   default:
00916     // For array terms, find all their reads
00917     if(e.getType().getExpr().getKind() == ARRAY) {
00918       for(CDList<Expr>::const_iterator i=d_reads.begin(), iend=d_reads.end();
00919     i!=iend; ++i) {
00920   DebugAssert(isRead(*i) && (*i).arity()==2, "Bad array read: "
00921         +(*i).toString());
00922   if((*i)[0] == e) {
00923     // Add both the read operator a[i]
00924     // getModelTerm(*i, v);
00925     v.push_back(*i);
00926       // and the index 'i' to the model terms.  Reason: the index to
00927       // the array should better be a concrete value, and it might not
00928       // necessarily be in the current list of model terms.
00929     // getModelTerm((*i)[1], v);
00930     v.push_back((*i)[1]);
00931   }
00932       }
00933     }
00934     break;
00935   }
00936 }
00937 
00938 
00939 void TheoryArray::computeModel(const Expr& e, std::vector<Expr>& v) {
00940   static unsigned count(0); // For bound vars
00941 
00942   switch(e.getKind()) {
00943   case WRITE: {
00944     // We should already have a value for the original array
00945     Expr res(getModelValue(e[0]).getRHS());
00946     Expr ind(getEM()->newBoundVarExpr("arr_var", int2string(count++)));
00947     Type tp(e.getType());
00948     DebugAssert(isArray(tp) && tp.arity()==2,
00949     "TheoryArray::computeModel(WRITE)");
00950     ind.setType(tp[0]);
00951     res = rewrite(Expr(READ, res, ind)).getRHS();
00952     Expr indVal(getModelValue(e[1]).getRHS());
00953     Expr updVal(getModelValue(e[2]).getRHS());
00954     res = (ind.eqExpr(indVal)).iteExpr(updVal, res);
00955     res = arrayLiteral(ind, res);
00956     assignValue(e, res);
00957     v.push_back(e);
00958     break;
00959   }
00960 //   case READ: {
00961 //     // Get the assignment for the index
00962 //     Expr idx(getModelValue(e[1]).getRHS());
00963 //     // And the assignment for the 
00964 //     var = read(idxThm.getRHS(), e[0]);
00965 //   }
00966     // And continue to collect the reads a[i][j] (remember, e is of
00967     // ARRAY type)
00968   default: {
00969     // Assign 'e' a value later.
00970     v.push_back(e);
00971     // Map of e[i] to val for concrete values of i and val
00972     ExprHashMap<Expr> reads;
00973     // For array terms, find all their reads
00974     DebugAssert(getBaseType(e).getExpr().getKind() == ARRAY, "");
00975 
00976     for(CDList<Expr>::const_iterator i=d_reads.begin(), iend=d_reads.end();
00977   i!=iend; ++i) {
00978       TRACE("model", "TheoryArray::computeModel: read = ", *i, "");
00979       DebugAssert(isRead(*i) && (*i).arity()==2, "Bad array read: "
00980       +(*i).toString());
00981       if((*i)[0] == e) {
00982   // Get the value of the index
00983   Theorem asst(getModelValue((*i)[1]));
00984   Expr var;
00985   if(asst.getLHS()!=asst.getRHS()) {
00986     vector<Theorem> thms;
00987     vector<unsigned> changed;
00988     thms.push_back(asst);
00989     changed.push_back(1);
00990     Theorem subst(substitutivityRule(*i, changed, thms));
00991     assignValue(transitivityRule(symmetryRule(subst),
00992                getModelValue(*i)));
00993     var = subst.getRHS();
00994   } else
00995     var = *i;
00996   if(d_applicationsInModel) v.push_back(var);
00997   // Record it in the map
00998   Expr val(getModelValue(var).getRHS());
00999   DebugAssert(!val.isNull(), "TheoryArray::computeModel(): Variable "
01000         +var.toString()+" has a Null value");
01001   reads[var] = val;
01002       }
01003     }
01004     // Create an array literal
01005     if(reads.size()==0) { // Leave the array uninterpreted
01006       assignValue(reflexivityRule(e));
01007     } else {
01008       // Bound var for the index
01009       Expr ind(getEM()->newBoundVarExpr("arr_var", int2string(count++)));
01010       Type tp(e.getType());
01011       DebugAssert(isArray(tp) && tp.arity()==2,
01012       "TheoryArray::computeModel(WRITE)");
01013       ind.setType(tp[0]);
01014       ExprHashMap<Expr>::iterator i=reads.begin(), iend=reads.end();
01015       DebugAssert(i!=iend,
01016       "TheoryArray::computeModel(): expected the reads "
01017       "table be non-empty");
01018       // Use one of the concrete values as a default
01019       Expr res((*i).second);
01020       ++i;
01021       DebugAssert(!res.isNull(), "TheoryArray::computeModel()");
01022       for(; i!=iend; ++i) {
01023   // Optimization: if the current value is the same as that of the
01024   // next application, skip this case; i.e. keep 'res' instead of
01025   // building ite(cond, res, res).
01026   if((*i).second == res) continue;
01027   // ITE condition
01028   Expr cond = ind.eqExpr((*i).first[1]);
01029   res = cond.iteExpr((*i).second, res);
01030       }
01031       // Construct the array literal
01032       res = arrayLiteral(ind, res);
01033       assignValue(e, res);
01034     }
01035     break;
01036   }
01037   }
01038 }
01039 
01040 
01041 Expr TheoryArray::computeTCC(const Expr& e)
01042 {
01043   Expr tcc(Theory::computeTCC(e));
01044   switch (e.getKind()) {
01045     case READ:
01046       DebugAssert(e.arity() == 2,"");
01047       return tcc.andExpr(getTypePred(e[0].getType()[0], e[1]));
01048     case WRITE: {
01049       DebugAssert(e.arity() == 3,"");
01050       Type arrType = e[0].getType();
01051       return rewriteAnd(getTypePred(arrType[0], e[1]).andExpr
01052                         (getTypePred(arrType[1], e[2])).andExpr(tcc)).getRHS();
01053     }
01054     case ARRAY_LITERAL: {
01055       return tcc;
01056     }
01057     default:
01058       DebugAssert(false,"TheoryArray::computeTCC: Unexpected expression: "
01059       +e.toString());
01060       return tcc;
01061   }
01062 }
01063 
01064 
01065 ///////////////////////////////////////////////////////////////////////////////
01066 // Pretty-printing                                           //
01067 ///////////////////////////////////////////////////////////////////////////////
01068 
01069 
01070 bool debug_write = false;
01071 
01072 ExprStream& TheoryArray::print(ExprStream& os, const Expr& e)
01073 {
01074   d_theoryUsed = true;
01075   if (theoryCore()->getTranslator()->printArrayExpr(os, e)) return os;
01076   switch(os.lang()) {
01077   case PRESENTATION_LANG:
01078     switch(e.getKind()) {
01079     case READ:
01080       if(e.arity() == 1)
01081   os << "[" << push << e[0] << push << "]";
01082       else
01083   os << e[0] << "[" << push << e[1] << push << "]";
01084       break;
01085     case WRITE:
01086       IF_DEBUG(
01087         if (debug_write) {
01088           os << "w(" << push << e[0] << space << ", " 
01089              << push << e[1] << ", " << push << e[2] << push << ")";
01090           break;
01091         }
01092       )
01093       os << "(" << push << e[0] << space << "WITH [" 
01094    << push << e[1] << "] := " << push << e[2] << push << ")";
01095       break;
01096     case ARRAY:
01097       os << "(ARRAY" << space << e[0] << space << "OF" << space << e[1] << ")";
01098       break;
01099     case ARRAY_LITERAL:
01100       if(e.isClosure()) {
01101   const vector<Expr>& vars = e.getVars();
01102   const Expr& body = e.getBody();
01103   os << "(" << push << "ARRAY" << space << "(" << push;
01104   bool first(true);
01105   for(size_t i=0; i<vars.size(); ++i) {
01106     if(first) first=false;
01107     else os << push << "," << pop << space;
01108     os << vars[i];
01109     if(vars[i].isVar())
01110       os << ":" << space << pushdag << vars[i].getType() << popdag;
01111   }
01112   os << push << "):" << pop << pop << space << body << push << ")";
01113       } else
01114   e.printAST(os);
01115       break;
01116     default:
01117       // Print the top node in the default LISP format, continue with
01118       // pretty-printing for children.
01119       e.printAST(os);
01120     }
01121     break; // end of case PRESENTATION_LANGUAGE
01122   case SMTLIB_LANG:
01123   case SMTLIB_V2_LANG:
01124     switch(e.getKind()) {
01125     case READ:
01126       if(e.arity() == 2)
01127   os << "(" << push << "select" << space << e[0]
01128      << space << e[1] << push << ")";
01129       else
01130   e.printAST(os);
01131       break;
01132     case WRITE:
01133       if(e.arity() == 3)
01134   os << "(" << push << "store" << space << e[0]
01135      << space << e[1] << space << e[2] << push << ")";
01136       else
01137   e.printAST(os);
01138       break;
01139     case ARRAY:
01140       throw SmtlibException("ARRAY should be handled by printArrayExpr");
01141       break;      
01142     case ARRAY_LITERAL:
01143       throw SmtlibException("SMT-LIB does not support ARRAY literals.\n"
01144                             "Suggestion: use command-line flag:\n"
01145                             "  -output-lang presentation");
01146       e.printAST(os);
01147     default:
01148       throw SmtlibException("TheoryArray::print: default not supported");
01149       // Print the top node in the default LISP format, continue with
01150       // pretty-printing for children.
01151       e.printAST(os);
01152     }
01153     break; // end of case LISP_LANGUAGE
01154   case LISP_LANG:
01155     switch(e.getKind()) {
01156     case READ:
01157       if(e.arity() == 2)
01158   os << "(" << push << "READ" << space << e[0]
01159      << space << e[1] << push << ")";
01160       else
01161   e.printAST(os);
01162       break;
01163     case WRITE:
01164       if(e.arity() == 3)
01165   os << "(" << push << "WRITE" << space << e[0]
01166      << space << e[1] << space << e[2] << push << ")";
01167       else
01168   e.printAST(os);
01169       break;
01170     case ARRAY:
01171       os << "(" << push << "ARRAY" << space << e[0]
01172    << space << e[1] << push << ")";
01173       break;      
01174     default:
01175       // Print the top node in the default LISP format, continue with
01176       // pretty-printing for children.
01177       e.printAST(os);
01178     }
01179     break; // end of case LISP_LANGUAGE
01180   default:
01181     // Print the top node in the default LISP format, continue with
01182     // pretty-printing for children.
01183     e.printAST(os);
01184   }
01185   return os;
01186 }
01187 
01188 //////////////////////////////////////////////////////////////////////////////
01189 //parseExprOp:
01190 //translating special Exprs to regular EXPR??
01191 ///////////////////////////////////////////////////////////////////////////////
01192 Expr
01193 TheoryArray::parseExprOp(const Expr& e) {
01194   //  TRACE("parser", "TheoryArray::parseExprOp(", e, ")");
01195   // If the expression is not a list, it must have been already
01196   // parsed, so just return it as is.
01197   if(RAW_LIST != e.getKind()) return e;
01198 
01199   DebugAssert(e.arity() > 0,
01200         "TheoryArray::parseExprOp:\n e = "+e.toString());
01201   
01202   const Expr& c1 = e[0][0];
01203   int kind = getEM()->getKind(c1.getString());
01204   switch(kind) {
01205     case READ: 
01206       if(!(e.arity() == 3))
01207   throw ParserException("Bad array access expression: "+e.toString());
01208       return Expr(READ, parseExpr(e[1]), parseExpr(e[2]));
01209     case WRITE: 
01210       if(!(e.arity() == 4))
01211   throw ParserException("Bad array update expression: "+e.toString());
01212       return Expr(WRITE, parseExpr(e[1]), parseExpr(e[2]), parseExpr(e[3]));
01213     case ARRAY: { 
01214       vector<Expr> k;
01215       Expr::iterator i = e.begin(), iend=e.end();
01216       // Skip first element of the vector of kids in 'e'.
01217       // The first element is the operator.
01218       ++i; 
01219       // Parse the kids of e and push them into the vector 'k'
01220       for(; i!=iend; ++i) 
01221         k.push_back(parseExpr(*i));
01222       return Expr(kind, k, e.getEM());
01223       break;
01224     }
01225     case ARRAY_LITERAL: { // (ARRAY (v tp1) body)
01226       if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() == 2))
01227   throw ParserException("Bad ARRAY literal expression: "+e.toString());
01228       const Expr& varPair = e[1];
01229       if(varPair.getKind() != RAW_LIST)
01230   throw ParserException("Bad variable declaration block in ARRAY "
01231             "literal expression: "+varPair.toString()+
01232             "\n e = "+e.toString());
01233       if(varPair[0].getKind() != ID)
01234   throw ParserException("Bad variable declaration in ARRAY"
01235             "literal expression: "+varPair.toString()+
01236             "\n e = "+e.toString());
01237       Type varTp(parseExpr(varPair[1]));
01238       vector<Expr> var;
01239       var.push_back(addBoundVar(varPair[0][0].getString(), varTp));
01240       Expr body(parseExpr(e[2]));
01241       // Build the resulting Expr as (LAMBDA (vars) body)
01242       return getEM()->newClosureExpr(ARRAY_LITERAL, var, body);
01243       break;
01244     }
01245     default:
01246       DebugAssert(false,
01247         "TheoryArray::parseExprOp: wrong type: "
01248       + e.toString());
01249     break;
01250   }
01251   return e;
01252 }
01253 
01254 Expr TheoryArray::getBaseArray(const Expr& e) const {
01255   if (e.getKind() == WRITE) return getBaseArray(e[0]);
01256   return e;
01257 }
01258 
01259 namespace CVC3 {
01260 
01261 Expr arrayLiteral(const Expr& ind, const Expr& body) {
01262   vector<Expr> vars;
01263   vars.push_back(ind);
01264   return body.getEM()->newClosureExpr(ARRAY_LITERAL, vars, body);
01265 }
01266 
01267 } // end of namespace CVC3