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