CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 *\file theory_datatype.cpp 00004 * 00005 * Author: Clark Barrett 00006 * 00007 * Created: Wed Dec 1 22:32:26 2004 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_datatype.h" 00023 #include "datatype_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 "theory_uf.h" 00029 #include "command_line_flags.h" 00030 00031 00032 using namespace std; 00033 using namespace CVC3; 00034 00035 00036 /////////////////////////////////////////////////////////////////////////////// 00037 // TheoryDatatype Public Methods // 00038 /////////////////////////////////////////////////////////////////////////////// 00039 00040 00041 TheoryDatatype::TheoryDatatype(TheoryCore* core) 00042 : Theory(core, "Datatypes"), 00043 d_labels(core->getCM()->getCurrentContext()), 00044 d_facts(core->getCM()->getCurrentContext()), 00045 d_splitters(core->getCM()->getCurrentContext()), 00046 d_splittersIndex(core->getCM()->getCurrentContext(), 0), 00047 d_splitterAsserted(core->getCM()->getCurrentContext(), false), 00048 d_smartSplits(core->getFlags()["dt-smartsplits"].getBool()) 00049 { 00050 d_rules = createProofRules(); 00051 00052 // Register new local kinds with ExprManager 00053 getEM()->newKind(DATATYPE_DECL, "_DATATYPE_DECL"); 00054 getEM()->newKind(DATATYPE, "_DATATYPE", true); 00055 getEM()->newKind(CONSTRUCTOR, "_CONSTRUCTOR"); 00056 getEM()->newKind(SELECTOR, "_SELECTOR"); 00057 getEM()->newKind(TESTER, "_TESTER"); 00058 00059 vector<int> kinds; 00060 kinds.push_back(DATATYPE_DECL); 00061 kinds.push_back(DATATYPE); 00062 kinds.push_back(TESTER); 00063 kinds.push_back(CONSTRUCTOR); 00064 kinds.push_back(SELECTOR); 00065 00066 registerTheory(this, kinds); 00067 } 00068 00069 00070 TheoryDatatype::~TheoryDatatype() { 00071 delete d_rules; 00072 } 00073 00074 00075 void TheoryDatatype::instantiate(const Expr& e, const Unsigned& u) 00076 { 00077 DebugAssert(!e.hasFind() || findExpr(e) == e, 00078 "datatype: instantiate: Expected find(e)=e"); 00079 if (isConstructor(e)) return; 00080 DebugAssert(u != 0 && (u & (u-1)) == 0, 00081 "datatype: instantiate: Expected single label in u"); 00082 DebugAssert(d_datatypes.find(getBaseType(e).getExpr()) != d_datatypes.end(), 00083 "datatype: instantiate: Unexpected type: "+getBaseType(e).toString() 00084 +"\n\n for expression: "+e.toString()); 00085 ExprMap<unsigned>& c = d_datatypes[getBaseType(e).getExpr()]; 00086 ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end(); 00087 for (; c_it != c_end; ++c_it) { 00088 if (u & (1 << Unsigned((*c_it).second))) break; 00089 } 00090 DebugAssert(c_it != c_end, 00091 "datatype: instantiate: couldn't find constructor"); 00092 const Expr& cons = (*c_it).first; 00093 00094 if (!cons.isFinite() && !e.isSelected()) return; 00095 00096 Type consType = getBaseType(cons); 00097 if (consType.arity() == 1) { 00098 enqueueFact(d_rules->dummyTheorem(d_facts, e.eqExpr(cons))); 00099 return; 00100 } 00101 // create vars 00102 vector<Expr> vars; 00103 for (int i = 0; i < consType.arity()-1; ++i) { 00104 vars.push_back(getEM()->newBoundVarExpr(consType[i])); 00105 } 00106 Expr e2 = getEM()->newClosureExpr(EXISTS, vars, 00107 e.eqExpr(Expr(cons.mkOp(), vars))); 00108 enqueueFact(d_rules->dummyTheorem(d_facts, e2)); 00109 } 00110 00111 00112 void TheoryDatatype::initializeLabels(const Expr& e, const Type& t) 00113 { 00114 DebugAssert(findExpr(e) == e, 00115 "datatype: initializeLabels: Expected find(e)=e"); 00116 DebugAssert(d_datatypes.find(t.getExpr()) != d_datatypes.end(), 00117 "Unknown datatype: "+t.getExpr().toString()); 00118 ExprMap<unsigned>& c = d_datatypes[t.getExpr()]; 00119 DebugAssert(d_labels.find(e) == d_labels.end(), 00120 "datatype: initializeLabels: expected unlabeled expr"); 00121 if (isConstructor(e)) { 00122 Expr cons = getConstructor(e); 00123 DebugAssert(c.find(cons) != c.end(), 00124 "datatype: initializeLabels: Couldn't find constructor " 00125 +cons.toString()); 00126 Unsigned position = c[cons]; 00127 d_labels.insert(e, 00128 SmartCDO<Unsigned>(theoryCore()->getCM()->getCurrentContext(), 00129 1 << position, 0)); 00130 } 00131 else { 00132 DebugAssert(c.size() > 0, "No constructors?"); 00133 Unsigned value = (1 << Unsigned(c.size())) - 1; 00134 d_labels.insert(e, 00135 SmartCDO<Unsigned>(theoryCore()->getCM()->getCurrentContext(), 00136 value, 0)); 00137 if (value == 1) instantiate(e, 1); 00138 else { 00139 if (!d_smartSplits || t.getExpr().isFinite()) d_splitters.push_back(e); 00140 } 00141 } 00142 } 00143 00144 00145 void TheoryDatatype::mergeLabels(const Theorem& thm, 00146 const Expr& e1, const Expr& e2) 00147 { 00148 DebugAssert(e2.hasFind() && findExpr(e2) == e2, 00149 "datatype: mergeLabels: Expected find(e2)=e2"); 00150 DebugAssert(d_labels.find(e1) != d_labels.end() && 00151 d_labels.find(e2) != d_labels.end(), 00152 "mergeLabels: expr is not labeled"); 00153 DebugAssert(getBaseType(e1) == getBaseType(e2), "Expected same type"); 00154 Unsigned u = d_labels[e2].get().get(); 00155 Unsigned uNew = u & d_labels[e1].get().get(); 00156 if (u != uNew) { 00157 if (!thm.isNull()) d_facts.push_back(thm); 00158 d_labels[e2].get().set(uNew); 00159 if (uNew == 0) 00160 setInconsistent(d_rules->dummyTheorem(d_facts, falseExpr())); 00161 } 00162 if (uNew != 0 && ((uNew - 1) & uNew) == 0) { 00163 instantiate(e2, uNew); 00164 } 00165 } 00166 00167 00168 void TheoryDatatype::mergeLabels(const Theorem& thm, const Expr& e, 00169 unsigned position, bool positive) 00170 { 00171 DebugAssert(e.hasFind() && findExpr(e) == e, 00172 "datatype: mergeLabels2: Expected find(e)=e"); 00173 DebugAssert(d_labels.find(e) != d_labels.end(), 00174 "mergeLabels2: expr is not labeled"); 00175 Unsigned u = d_labels[e].get().get(); 00176 Unsigned uNew = 1 << Unsigned(position); 00177 if (positive) { 00178 uNew = u & uNew; 00179 if (u == uNew) return; 00180 } else if (u & uNew) uNew = u - uNew; 00181 else return; 00182 d_facts.push_back(thm); 00183 d_labels[e].get().set(uNew); 00184 if (uNew == 0) 00185 setInconsistent(d_rules->dummyTheorem(d_facts, falseExpr())); 00186 else if (((uNew - 1) & uNew) == 0) { 00187 instantiate(e, uNew); 00188 } 00189 } 00190 00191 00192 void TheoryDatatype::addSharedTerm(const Expr& e) 00193 { 00194 if (getBaseType(e).getExpr().getKind() == DATATYPE && 00195 d_labels.find(e) == d_labels.end()) { 00196 initializeLabels(e, getBaseType(e)); 00197 e.addToNotify(this, Expr()); 00198 } 00199 } 00200 00201 00202 void TheoryDatatype::assertFact(const Theorem& e) 00203 { 00204 if (!e.isRewrite()) { 00205 const Expr& expr = e.getExpr(); 00206 if (expr.getOpKind() == TESTER) { 00207 mergeLabels(e, expr[0], 00208 getConsPos(getConsForTester(expr.getOpExpr())), 00209 true); 00210 } 00211 else if (expr.isNot()) { 00212 if (expr[0].getOpKind() == TESTER) { 00213 mergeLabels(e, expr[0][0], 00214 getConsPos(getConsForTester(expr[0].getOpExpr())), 00215 false); 00216 } 00217 else if (expr[0].isEq() && 00218 getBaseType(expr[0][0]).getExpr().getKind() == DATATYPE) { 00219 // Propagate disequality down 00220 if (d_labels.find(expr[0][0]) == d_labels.end()) { 00221 initializeLabels(expr[0][0], getBaseType(expr[0][0])); 00222 expr[0][0].addToNotify(this, Expr()); 00223 } 00224 if (d_labels.find(expr[0][1]) == d_labels.end()) { 00225 initializeLabels(expr[0][1], getBaseType(expr[0][1])); 00226 expr[0][1].addToNotify(this, Expr()); 00227 } 00228 Unsigned u1 = d_labels[expr[0][0]].get().get(); 00229 Unsigned u2 = d_labels[expr[0][1]].get().get(); 00230 ExprMap<unsigned>& c = d_datatypes[getBaseType(expr[0][0]).getExpr()]; 00231 ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end(); 00232 Expr bigConj; 00233 for (; c_it != c_end; ++c_it) { 00234 if (u1 & u2 & (1 << Unsigned((*c_it).second))) { 00235 vector<Expr>& selectors = d_constructorMap[(*c_it).first]; 00236 Expr conj; 00237 for (unsigned i = 0; i < selectors.size(); ++i) { 00238 Expr e1 = Expr(selectors[i].mkOp(), expr[0][0]); 00239 Expr e2 = e1.eqExpr(Expr(selectors[i].mkOp(), expr[0][1])); 00240 if (conj.isNull()) conj = e2; 00241 else conj = conj.andExpr(e2); 00242 } 00243 if (!conj.isNull()) { 00244 Expr e1 = datatypeTestExpr((*c_it).first.getName(), expr[0][0]); 00245 Expr e2 = datatypeTestExpr((*c_it).first.getName(), expr[0][1]); 00246 conj = (e1 && e2).impExpr(!conj); 00247 if (bigConj.isNull()) bigConj = conj; 00248 else bigConj = bigConj.andExpr(conj); 00249 } 00250 } 00251 } 00252 if (!bigConj.isNull()) { 00253 enqueueFact(d_rules->dummyTheorem(d_facts, bigConj)); 00254 } 00255 } 00256 } 00257 } 00258 } 00259 00260 00261 void TheoryDatatype::checkSat(bool fullEffort) 00262 { 00263 bool done = false; 00264 while (!done && d_splittersIndex < d_splitters.size()) { 00265 Expr e = d_splitters[d_splittersIndex]; 00266 if ((!d_smartSplits || getBaseType(e).getExpr().isFinite()) && 00267 findExpr(e) == e) { 00268 DebugAssert(d_labels.find(e) != d_labels.end(), 00269 "checkSat: expr is not labeled"); 00270 Unsigned u = d_labels[e].get().get(); 00271 if ((u & (u-1)) != 0) { 00272 done = true; 00273 DebugAssert(!d_splitterAsserted || !fullEffort, 00274 "splitter should have been resolved"); 00275 if (!d_splitterAsserted) { 00276 DebugAssert 00277 (d_datatypes.find(getBaseType(e).getExpr()) != d_datatypes.end(), 00278 "datatype: checkSat: Unexpected type: "+getBaseType(e).toString() 00279 +"\n\n for expression: "+e.toString()); 00280 ExprMap<unsigned>& c = d_datatypes[getBaseType(e).getExpr()]; 00281 ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end(); 00282 vector<Expr> vec; 00283 for (; c_it != c_end; ++c_it) { 00284 if (u & (1 << Unsigned((*c_it).second))) { 00285 vec.push_back(datatypeTestExpr((*c_it).first.getName(), e)); 00286 } 00287 } 00288 DebugAssert(vec.size() > 1, "datatype: checkSat: expected 2 or more possible constructors"); 00289 enqueueFact(d_rules->dummyTheorem(d_facts, Expr(OR, vec))); 00290 d_splitterAsserted = true; 00291 } 00292 } 00293 } 00294 if (d_smartSplits && !done && isSelector(e)) { 00295 Expr f = findExpr(e[0]); 00296 DebugAssert(d_labels.find(f) != d_labels.end(), 00297 "checkSat: expr is not labeled"); 00298 Unsigned u = d_labels[f].get().get(); 00299 if ((u & (u-1)) != 0) { 00300 pair<Expr, unsigned> selectorInfo = getSelectorInfo(e.getOpExpr()); 00301 Unsigned pos = getConsPos(selectorInfo.first); 00302 if (u & (1 << pos)) { 00303 done = true; 00304 DebugAssert(!d_splitterAsserted || !fullEffort, 00305 "splitter should have been resolved"); 00306 if (!d_splitterAsserted) { 00307 addSplitter(datatypeTestExpr(selectorInfo.first.getName(), f)); 00308 d_splitterAsserted = true; 00309 } 00310 } 00311 } 00312 } 00313 if (!done) { 00314 d_splitterAsserted = false; 00315 d_splittersIndex = d_splittersIndex + 1; 00316 } 00317 } 00318 } 00319 00320 00321 Theorem TheoryDatatype::rewrite(const Expr& e) 00322 { 00323 // TODO: UF rewrite? 00324 Theorem thm; 00325 if (isSelector(e)) { 00326 if (canCollapse(e)) { 00327 thm = d_rules->rewriteSelCons(d_facts, e); 00328 return transitivityRule(thm, simplify(thm.getRHS())); 00329 } 00330 } 00331 else if (isTester(e)) { 00332 if (isConstructor(e[0])) { 00333 return d_rules->rewriteTestCons(e); 00334 } 00335 } 00336 return reflexivityRule(e); 00337 } 00338 00339 00340 void TheoryDatatype::setup(const Expr& e) 00341 { 00342 if (getBaseType(e).getExpr().getKind() == DATATYPE && 00343 d_labels.find(e) == d_labels.end()) { 00344 initializeLabels(e, getBaseType(e)); 00345 e.addToNotify(this, Expr()); 00346 } 00347 if (e.getKind() != APPLY) return; 00348 if (isConstructor(e) && e.arity() > 0) { 00349 enqueueFact(d_rules->noCycle(e)); 00350 } 00351 if (isSelector(e)) { 00352 if (d_smartSplits) d_splitters.push_back(e); 00353 e[0].setSelected(); 00354 mergeLabels(Theorem(), e[0], e[0]); 00355 } 00356 setupCC(e); 00357 } 00358 00359 00360 void TheoryDatatype::update(const Theorem& e, const Expr& d) 00361 { 00362 if (d.isNull()) { 00363 const Expr& lhs = e.getLHS(); 00364 const Expr& rhs = e.getRHS(); 00365 if (isConstructor(lhs) && isConstructor(rhs) && 00366 lhs.isApply() && rhs.isApply() && 00367 lhs.getOpExpr() == rhs.getOpExpr()) { 00368 enqueueFact(d_rules->decompose(e)); 00369 } 00370 else { 00371 // Possible for rhs to never have been seen: initialize it here 00372 DebugAssert(getBaseType(rhs).getExpr().getKind() == DATATYPE, 00373 "Expected datatype"); 00374 if (d_labels.find(rhs) == d_labels.end()) { 00375 initializeLabels(rhs, getBaseType(rhs)); 00376 rhs.addToNotify(this, Expr()); 00377 } 00378 Theorem thm(e); 00379 if (lhs.isSelected() && !rhs.isSelected()) { 00380 d_facts.push_back(e); 00381 rhs.setSelected(); 00382 thm = Theorem(); 00383 } 00384 mergeLabels(thm, lhs, rhs); 00385 } 00386 } 00387 else { 00388 const Theorem& dEQdsig = d.getSig(); 00389 if (!dEQdsig.isNull()) { 00390 const Expr& dsig = dEQdsig.getRHS(); 00391 Theorem thm = updateHelper(d); 00392 const Expr& sigNew = thm.getRHS(); 00393 if (sigNew == dsig) return; 00394 dsig.setRep(Theorem()); 00395 if (isSelector(sigNew) && canCollapse(sigNew)) { 00396 d.setSig(Theorem()); 00397 enqueueFact(transitivityRule(thm, d_rules->rewriteSelCons(d_facts, sigNew))); 00398 } 00399 else if (isTester(sigNew) && isConstructor(sigNew[0])) { 00400 d.setSig(Theorem()); 00401 enqueueFact(transitivityRule(thm, d_rules->rewriteTestCons(sigNew))); 00402 } 00403 else { 00404 const Theorem& repEQsigNew = sigNew.getRep(); 00405 if (!repEQsigNew.isNull()) { 00406 d.setSig(Theorem()); 00407 enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm))); 00408 } 00409 else { 00410 int k, ar(d.arity()); 00411 for (k = 0; k < ar; ++k) { 00412 if (sigNew[k] != dsig[k]) { 00413 sigNew[k].addToNotify(this, d); 00414 } 00415 } 00416 d.setSig(thm); 00417 sigNew.setRep(thm); 00418 getEM()->invalidateSimpCache(); 00419 } 00420 } 00421 } 00422 } 00423 } 00424 00425 00426 Theorem TheoryDatatype::solve(const Theorem& e) 00427 { 00428 DebugAssert(e.isRewrite() && e.getLHS().isTerm(), "Expected equality"); 00429 const Expr& lhs = e.getLHS(); 00430 if (isConstructor(lhs) && !isConstructor(e.getRHS())) { 00431 return symmetryRule(e); 00432 } 00433 return e; 00434 } 00435 00436 00437 void TheoryDatatype::checkType(const Expr& e) 00438 { 00439 switch (e.getKind()) { 00440 case DATATYPE: { 00441 if (e.arity() != 1 || !e[0].isString()) 00442 throw Exception("Ill-formed datatype"+e.toString()); 00443 if (resolveID(e[0].getString()) != e) 00444 throw Exception("Unknown datatype"+e.toString()); 00445 break; 00446 } 00447 case CONSTRUCTOR: 00448 case SELECTOR: 00449 case TESTER: 00450 throw Exception("Non-type: "+e.toString()); 00451 default: 00452 FatalAssert(false, "Unexpected kind in TheoryDatatype::checkType" 00453 +getEM()->getKindName(e.getKind())); 00454 } 00455 } 00456 00457 00458 Cardinality TheoryDatatype::finiteTypeInfo(Expr& e, Unsigned& n, 00459 bool enumerate, bool computeSize) 00460 { 00461 DebugAssert(e.getKind() == DATATYPE, 00462 "Unexpected kind in TheoryDatatype::finiteTypeInfo"); 00463 if (d_getConstantStack.count(e) != 0) { 00464 return CARD_INFINITE; 00465 } 00466 d_getConstantStack[e] = true; 00467 00468 Expr typeExpr = e; 00469 ExprMap<unsigned>& c = d_datatypes[typeExpr]; 00470 ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end(); 00471 Cardinality card = CARD_FINITE, cardTmp; 00472 bool getSize = enumerate || computeSize; 00473 Unsigned totalSize = 0, thisSize, size; 00474 vector<Unsigned> sizes; 00475 int j; 00476 00477 // Loop through constructors, and check if each one only has a finite number 00478 // of possibilities 00479 for (; c_it != c_end; ++c_it) { 00480 const Expr& cons = (*c_it).first; 00481 Expr funType = cons.getType().getExpr(); 00482 thisSize = 1; 00483 for (j = 0; j < funType.arity()-1; ++j) { 00484 Expr e2 = funType[j]; 00485 cardTmp = theoryOf(e2)->finiteTypeInfo(e2, size, false, getSize); 00486 if (cardTmp == CARD_INFINITE) { 00487 card = CARD_INFINITE; 00488 break; 00489 } 00490 else if (cardTmp == CARD_UNKNOWN) { 00491 card = CARD_UNKNOWN; 00492 getSize = false; 00493 // Keep looking to see if we can determine it is infinite 00494 } 00495 else if (getSize) { 00496 thisSize = thisSize * size; 00497 // Give up if it gets too big 00498 if (thisSize > 1000000) thisSize = 0; 00499 if (thisSize == 0) { 00500 totalSize = 0; 00501 getSize = false; 00502 } 00503 } 00504 } 00505 if (card == CARD_INFINITE) break; 00506 if (getSize) { 00507 sizes.push_back(thisSize); 00508 totalSize = totalSize + thisSize; 00509 } 00510 } 00511 00512 if (card == CARD_FINITE) { 00513 00514 if (enumerate) { 00515 c_it = c.begin(); 00516 unsigned i = 0; 00517 for (; i < sizes.size(); ++i, ++c_it) { 00518 if (n < sizes[i]) { 00519 break; 00520 } 00521 else n = n - sizes[i]; 00522 } 00523 if (i == sizes.size() && n != 0) { 00524 e = Expr(); 00525 } 00526 else { 00527 const Expr& cons = (*c_it).first; 00528 Expr funType = cons.getType().getExpr(); 00529 if (funType.arity() == 1) { 00530 e = cons; 00531 } 00532 else { 00533 vector<Expr> kids(funType.arity()-1); 00534 Unsigned thisSize; 00535 Unsigned elem; 00536 for (int j = funType.arity()-2; j >= 0; --j) { 00537 if (n == 0) { 00538 elem = 0; 00539 } 00540 else { 00541 thisSize = funType[j].typeSizeFinite(); 00542 elem = n % thisSize; 00543 n = n - elem; 00544 n = n / thisSize; 00545 } 00546 kids[j] = funType[j].typeEnumerateFinite(elem); 00547 } 00548 e = Expr(cons.mkOp(), kids); 00549 } 00550 } 00551 } 00552 00553 if (computeSize) { 00554 n = totalSize; 00555 } 00556 00557 } 00558 d_getConstantStack.erase(typeExpr); 00559 return card; 00560 } 00561 00562 00563 void TheoryDatatype::computeType(const Expr& e) 00564 { 00565 switch (e.getOpKind()) { 00566 case CONSTRUCTOR: 00567 case SELECTOR: 00568 case TESTER: { 00569 DebugAssert(e.isApply(), "Expected application"); 00570 Expr op = e.getOp().getExpr(); 00571 Type t = op.lookupType(); 00572 DebugAssert(!t.isNull(), "Expected operator to be well-typed"); 00573 if (t.getExpr().getKind() == DATATYPE) { 00574 if (e.arity() != 0) 00575 throw TypecheckException("Expected no children: "+e.toString()); 00576 e.setType(t); 00577 break; 00578 } 00579 else { 00580 DebugAssert(t.getExpr().getKind() == ARROW, "Expected function type"); 00581 if (e.arity() != t.getExpr().arity()-1) 00582 throw TypecheckException("Wrong number of children:\n"+e.toString()); 00583 Expr::iterator i = e.begin(), iend = e.end(); 00584 Expr::iterator j = t.getExpr().begin(); 00585 for (; i != iend; ++i, ++j) { 00586 if (getBaseType(*i) != getBaseType(Type(*j))) { 00587 throw TypecheckException("Type mismatch for expression:\n\n " 00588 + (*i).toString() 00589 + "\n\nhas the following type:\n\n " 00590 + (*i).getType().getExpr().toString() 00591 + "\n\nbut the expected type is:\n\n " 00592 + (*j).toString() 00593 + "\n\nin datatype function application:\n\n " 00594 + e.toString()); 00595 } 00596 } 00597 e.setType(*j); 00598 } 00599 break; 00600 } 00601 default: 00602 DebugAssert(false, "Unexpected kind in datatype::computeType: " 00603 +e.toString()); 00604 } 00605 } 00606 00607 00608 void TheoryDatatype::computeModelTerm(const Expr& e, std::vector<Expr>& v) { 00609 } 00610 00611 00612 00613 Expr TheoryDatatype::computeTCC(const Expr& e) 00614 { 00615 Expr tcc(Theory::computeTCC(e)); 00616 switch (e.getKind()) { 00617 case CONSTRUCTOR: 00618 DebugAssert(e.arity() == 0, "Expected leaf constructor"); 00619 return trueExpr(); 00620 case APPLY: { 00621 DebugAssert(e.isApply(), "Should be application"); 00622 Expr op(e.getOpExpr()); 00623 if (op.getKind() != SELECTOR) return tcc; 00624 DebugAssert(e.arity() == 1, "Expected single argument"); 00625 const std::pair<Expr,unsigned>& p = getSelectorInfo(op); 00626 Expr tester = datatypeTestExpr(p.first.getName(), e[0]); 00627 return tcc.andExpr(tester); 00628 } 00629 default: 00630 DebugAssert(false,"Unexpected type: "+e.toString()); 00631 return trueExpr(); 00632 } 00633 } 00634 00635 /////////////////////////////////////////////////////////////////////////////// 00636 // Pretty-printing // 00637 /////////////////////////////////////////////////////////////////////////////// 00638 00639 00640 ExprStream& TheoryDatatype::print(ExprStream& os, const Expr& e) { 00641 switch (os.lang()) { 00642 case PRESENTATION_LANG: 00643 switch (e.getKind()) { 00644 case DATATYPE_DECL: { 00645 os << "DATATYPE" << endl; 00646 bool first(true); 00647 for (Expr::iterator i = e.begin(), iend = e.end(); i != iend; ++i) { 00648 if (first) first = false; 00649 else os << "," << endl; 00650 os << " " << push << *i << space << "= " << push; 00651 DebugAssert(d_datatypes.find(*i) != d_datatypes.end(), 00652 "Unknown datatype: "+(*i).toString()); 00653 ExprMap<unsigned>& c = d_datatypes[*i]; 00654 ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end(); 00655 bool firstCons(true); 00656 for (; c_it != c_end; ++c_it) { 00657 if (!firstCons) { 00658 os << space << "| "; 00659 } 00660 else firstCons = false; 00661 const Expr& cons = (*c_it).first; 00662 os << cons; 00663 vector<Expr>& sels = d_constructorMap[cons]; 00664 bool firstSel(true); 00665 for (unsigned j = 0; j < sels.size(); ++j) { 00666 if (firstSel) { 00667 firstSel = false; 00668 os << "("; 00669 } else { 00670 os << ", "; 00671 } 00672 os << sels[j] << space << ": "; 00673 os << sels[j].getType().getExpr()[1]; 00674 } 00675 if (!firstSel) { 00676 os << ")"; 00677 } 00678 } 00679 os << pop; 00680 } 00681 os << pop << endl; 00682 os << "END;"; 00683 break; 00684 } 00685 case DATATYPE: 00686 if (e.arity() == 1 && e[0].isString()) { 00687 os << e[0].getString(); 00688 } 00689 else e.printAST(os); 00690 break; 00691 case APPLY: 00692 os << e.getOpExpr(); 00693 if(e.arity() > 0) { 00694 os << "(" << push; 00695 bool first(true); 00696 for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 00697 if(first) first = false; 00698 else os << "," << space; 00699 os << *i; 00700 } 00701 os << push << ")"; 00702 } 00703 break; 00704 case CONSTRUCTOR: 00705 case SELECTOR: 00706 case TESTER: 00707 DebugAssert(e.isSymbol(), "Expected symbol"); 00708 os << e.getName(); 00709 break; 00710 default: 00711 DebugAssert(false, "TheoryDatatype::print: Unexpected kind: " 00712 +getEM()->getKindName(e.getKind())); 00713 } 00714 break; 00715 case SMTLIB_LANG: 00716 FatalAssert(false, "Not Implemented Yet"); 00717 break; 00718 case LISP_LANG: 00719 FatalAssert(false, "Not Implemented Yet"); 00720 break; 00721 default: 00722 e.printAST(os); 00723 break; 00724 } 00725 return os; 00726 } 00727 00728 ////////////////////////////////////////////////////////////////////////////// 00729 //parseExprOp: 00730 //translating special Exprs to regular EXPR?? 00731 /////////////////////////////////////////////////////////////////////////////// 00732 Expr TheoryDatatype::parseExprOp(const Expr& e) 00733 { 00734 // If the expression is not a list, it must have been already 00735 // parsed, so just return it as is. 00736 if(RAW_LIST != e.getKind()) return e; 00737 00738 DebugAssert(e.arity() > 0, 00739 "TheoryDatatype::parseExprOp:\n e = "+e.toString()); 00740 00741 DebugAssert(e[0].getKind() == ID, 00742 "Expected ID kind for first elem in list expr"); 00743 00744 const Expr& c1 = e[0][0]; 00745 int kind = getEM()->getKind(c1.getString()); 00746 switch(kind) { 00747 case DATATYPE: { 00748 DebugAssert(e.arity() > 1, 00749 "Empty DATATYPE expression\n" 00750 " (expected at least one datatype): "+e.toString()); 00751 00752 vector<Expr> names; 00753 00754 vector<Expr> allConstructorNames; 00755 vector<Expr> constructorNames; 00756 00757 vector<Expr> allSelectorNames; 00758 vector<Expr> selectorNames; 00759 vector<Expr> selectorNamesKids; 00760 00761 vector<Expr> allTypes; 00762 vector<Expr> types; 00763 vector<Expr> typesKids; 00764 00765 int i,j,k; 00766 Expr dt, constructor, selectors, selector; 00767 00768 // Get names of datatypes 00769 ExprMap<bool> namesMap; 00770 for (i = 0; i < e.arity()-1; ++i) { 00771 dt = e[i+1]; 00772 DebugAssert(dt.getKind() == RAW_LIST && dt.arity() == 2, 00773 "Bad formed datatype expression" 00774 +dt.toString()); 00775 DebugAssert(dt[0].getKind() == ID, 00776 "Expected ID kind for datatype name" 00777 +dt.toString()); 00778 names.push_back(dt[0][0]); 00779 if (namesMap.count(dt[0][0]) != 0) { 00780 throw ParserException("Datatype name used more than once"+dt[0][0].getString()); 00781 } 00782 namesMap.insert(dt[0][0], true); 00783 } 00784 00785 // Loop through datatypes 00786 for (i = 0; i < e.arity()-1; ++i) { 00787 dt = e[i+1]; 00788 DebugAssert(dt[1].getKind() == RAW_LIST && dt[1].arity() > 0, 00789 "Expected non-empty list for datatype constructors" 00790 +dt.toString()); 00791 dt = dt[1]; 00792 00793 // Loop through constructors for this datatype 00794 for(j = 0; j < dt.arity(); ++j) { 00795 constructor = dt[j]; 00796 DebugAssert(constructor.getKind() == RAW_LIST && 00797 (constructor.arity() == 1 || constructor.arity() == 2), 00798 "Unexpected constructor"+constructor.toString()); 00799 DebugAssert(constructor[0].getKind() == ID, 00800 "Expected ID kind for constructor name" 00801 +constructor.toString()); 00802 constructorNames.push_back(constructor[0][0]); 00803 00804 if (constructor.arity() == 2) { 00805 selectors = constructor[1]; 00806 DebugAssert(selectors.getKind() == RAW_LIST && selectors.arity() > 0, 00807 "Non-empty list expected as second argument of constructor:\n" 00808 +constructor.toString()); 00809 00810 // Loop through selectors for this constructor 00811 for (k = 0; k < selectors.arity(); ++k) { 00812 selector = selectors[k]; 00813 DebugAssert(selector.getKind() == RAW_LIST && selector.arity() == 2, 00814 "Expected list of arity 2 for selector" 00815 +selector.toString()); 00816 DebugAssert(selector[0].getKind() == ID, 00817 "Expected ID kind for selector name" 00818 +selector.toString()); 00819 selectorNamesKids.push_back(selector[0][0]); 00820 if (selector[1].getKind() == ID && namesMap.count(selector[1][0]) > 0) { 00821 typesKids.push_back(selector[1][0]); 00822 } 00823 else { 00824 typesKids.push_back(parseExpr(selector[1])); 00825 } 00826 } 00827 selectorNames.push_back(Expr(RAW_LIST, selectorNamesKids)); 00828 selectorNamesKids.clear(); 00829 types.push_back(Expr(RAW_LIST, typesKids)); 00830 typesKids.clear(); 00831 } 00832 else { 00833 selectorNames.push_back(Expr(RAW_LIST, selectorNamesKids, getEM())); 00834 types.push_back(Expr(RAW_LIST, typesKids, getEM())); 00835 } 00836 } 00837 allConstructorNames.push_back(Expr(RAW_LIST, constructorNames)); 00838 constructorNames.clear(); 00839 allSelectorNames.push_back(Expr(RAW_LIST, selectorNames)); 00840 selectorNames.clear(); 00841 allTypes.push_back(Expr(RAW_LIST, types)); 00842 types.clear(); 00843 } 00844 00845 return Expr(DATATYPE, 00846 Expr(RAW_LIST, names), 00847 Expr(RAW_LIST, allConstructorNames), 00848 Expr(RAW_LIST, allSelectorNames), 00849 Expr(RAW_LIST, allTypes)); 00850 } 00851 00852 default: { 00853 throw ParserException("Unexpected datatype expression: "+e.toString()); 00854 } 00855 } 00856 return e; 00857 } 00858 00859 00860 Expr TheoryDatatype::dataType(const string& name, 00861 const vector<string>& constructors, 00862 const vector<vector<string> >& selectors, 00863 const vector<vector<Expr> >& types) 00864 { 00865 vector<string> names; 00866 vector<vector<string> > constructors2; 00867 vector<vector<vector<string> > > selectors2; 00868 vector<vector<vector<Expr> > > types2; 00869 names.push_back(name); 00870 constructors2.push_back(constructors); 00871 selectors2.push_back(selectors); 00872 types2.push_back(types); 00873 return dataType(names, constructors2, selectors2, types2); 00874 } 00875 00876 00877 // Elements of types are either the expr from an existing type or a string 00878 // naming one of the datatypes being defined 00879 Expr TheoryDatatype::dataType(const vector<string>& names, 00880 const vector<vector<string> >& allConstructors, 00881 const vector<vector<vector<string> > >& allSelectors, 00882 const vector<vector<vector<Expr> > >& allTypes) 00883 { 00884 vector<Expr> returnTypes; 00885 00886 // bool wellFounded = false, infinite = false, 00887 bool thisWellFounded; 00888 00889 if (names.size() != allConstructors.size() || 00890 allConstructors.size() != allSelectors.size() || 00891 allSelectors.size() != allTypes.size()) { 00892 throw TypecheckException 00893 ("dataType: vector sizes don't match"); 00894 } 00895 00896 unsigned i, j, k; 00897 Expr e; 00898 00899 // Create reachability predicate for constructor cycle detection 00900 vector<Type> funTypeArgs; 00901 funTypeArgs.push_back(Type::anyType(getEM())); 00902 funTypeArgs.push_back(Type::anyType(getEM())); 00903 Op op = newFunction("_reach_"+names[0], 00904 Type::funType(funTypeArgs, boolType()), 00905 true /* compute trans closure */); 00906 Op reach = getEM()->newSymbolExpr(op.getExpr().getName(), 00907 TRANS_CLOSURE).mkOp(); 00908 00909 for (i = 0; i < names.size(); ++i) { 00910 e = resolveID(names[i]); 00911 if (!e.isNull()) { 00912 throw TypecheckException 00913 ("Attempt to define datatype "+names[i]+":\n " 00914 "This variable is already defined."); 00915 } 00916 e = Expr(DATATYPE, getEM()->newStringExpr(names[i])); 00917 installID(names[i], e); 00918 returnTypes.push_back(e); 00919 d_reach[e] = reach; 00920 } 00921 00922 vector<Expr> selectorVec; 00923 00924 for (i = 0; i < names.size(); ++i) { 00925 00926 const vector<string>& constructors = allConstructors[i]; 00927 const vector<vector<string> >& selectors = allSelectors[i]; 00928 const vector<vector<Expr> >& types = allTypes[i]; 00929 00930 if (constructors.size() == 0) { 00931 throw TypecheckException 00932 ("datatype: "+names[i]+": must have at least one constructor"); 00933 } 00934 if (constructors.size() != selectors.size() || 00935 selectors.size() != types.size()) { 00936 throw TypecheckException 00937 ("dataType: vector sizes at index "+int2string(i)+" don't match"); 00938 } 00939 00940 ExprMap<unsigned>& constMap = d_datatypes[returnTypes[i]]; 00941 00942 for (j = 0; j < constructors.size(); ++j) { 00943 Expr c = resolveID(constructors[j]); 00944 if (!c.isNull()) { 00945 throw TypecheckException 00946 ("Attempt to define datatype constructor "+constructors[j]+":\n " 00947 "This variable is already defined."); 00948 } 00949 c = getEM()->newSymbolExpr(constructors[j], CONSTRUCTOR); 00950 00951 if (selectors[j].size() != types[j].size()) { 00952 throw TypecheckException 00953 ("dataType: constructor at index "+int2string(i)+", "+int2string(j)+ 00954 ": number of selectors does not match number of types"); 00955 } 00956 thisWellFounded = true; 00957 const vector<string>& sels = selectors[j]; 00958 const vector<Expr>& tps = types[j]; 00959 00960 vector<Type> selTypes; 00961 Type t; 00962 Expr s; 00963 for (k = 0; k < sels.size(); ++k) { 00964 s = resolveID(sels[k]); 00965 if (!s.isNull()) { 00966 throw TypecheckException 00967 ("Attempt to define datatype selector "+sels[k]+":\n " 00968 "This variable is already defined."); 00969 } 00970 s = getEM()->newSymbolExpr(sels[k], SELECTOR); 00971 if (tps[k].isString()) { 00972 t = Type(resolveID(tps[k].getString())); 00973 if (t.isNull()) { 00974 throw TypecheckException 00975 ("Unable to resolve type identifier: "+tps[k].getString()); 00976 } 00977 } else t = Type(tps[k]); 00978 if (t.isBool()) { 00979 throw TypecheckException 00980 ("Cannot have BOOLEAN inside of datatype"); 00981 } 00982 else if (t.isFunction()) { 00983 throw TypecheckException 00984 ("Cannot have function inside of datatype"); 00985 } 00986 00987 selTypes.push_back(Type(t)); 00988 s.setType(Type(returnTypes[i]).funType(Type(t))); 00989 if (isDatatype(Type(t)) && !t.getExpr().isWellFounded()) { 00990 thisWellFounded = false; 00991 } 00992 d_selectorMap[s] = pair<Expr,unsigned>(c,k); 00993 installID(sels[k], s); 00994 selectorVec.push_back(s); 00995 } 00996 if (thisWellFounded) c.setWellFounded(); 00997 if (selTypes.size() == 0) { 00998 c.setType(Type(returnTypes[i])); 00999 c.setFinite(); 01000 } 01001 else c.setType(Type::funType(selTypes, Type(returnTypes[i]))); 01002 installID(constructors[j], c); 01003 constMap[c] = j; 01004 d_constructorMap[c] = selectorVec; 01005 selectorVec.clear(); 01006 01007 string testerString = "is_"+constructors[j]; 01008 e = resolveID(testerString); 01009 if (!e.isNull()) { 01010 throw TypecheckException 01011 ("Attempt to define datatype tester "+testerString+":\n " 01012 "This variable is already defined."); 01013 } 01014 e = getEM()->newSymbolExpr(testerString, TESTER); 01015 e.setType(Type(returnTypes[i]).funType(boolType())); 01016 d_testerMap[e] = c; 01017 installID(testerString, e); 01018 } 01019 } 01020 01021 // Compute fixed point for wellfoundedness check 01022 01023 bool changed, thisFinite; 01024 int firstNotWellFounded; 01025 do { 01026 changed = false; 01027 firstNotWellFounded = -1; 01028 for (i = 0; i < names.size(); ++i) { 01029 ExprMap<unsigned>& c = d_datatypes[returnTypes[i]]; 01030 ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end(); 01031 thisWellFounded = false; 01032 thisFinite = true; 01033 for (; c_it != c_end; ++c_it) { 01034 const Expr& cons = (*c_it).first; 01035 Expr funType = getBaseType(cons).getExpr(); 01036 int j; 01037 if (!cons.isFinite()) { 01038 for (j = 0; j < funType.arity()-1; ++j) { 01039 if (!isDatatype(funType[j]) || !funType[j].isFinite()) 01040 break; 01041 } 01042 if (j == funType.arity()-1) { 01043 changed = true; 01044 cons.setFinite(); 01045 } 01046 else thisFinite = false; 01047 } 01048 if (cons.isWellFounded()) { 01049 thisWellFounded = true; 01050 continue; 01051 } 01052 for (j = 0; j < funType.arity()-1; ++j) { 01053 if (isDatatype(funType[j]) && !funType[j].isWellFounded()) 01054 break; 01055 } 01056 if (j == funType.arity()-1) { 01057 changed = true; 01058 cons.setWellFounded(); 01059 thisWellFounded = true; 01060 } 01061 } 01062 if (!thisWellFounded) { 01063 if (firstNotWellFounded == -1) firstNotWellFounded = i; 01064 } 01065 else { 01066 if (!returnTypes[i].isWellFounded()) { 01067 changed = true; 01068 returnTypes[i].setWellFounded(); 01069 } 01070 } 01071 if (thisFinite && !returnTypes[i].isFinite()) { 01072 changed = true; 01073 returnTypes[i].setFinite(); 01074 } 01075 } 01076 } while (changed); 01077 01078 if (firstNotWellFounded >= 0) { 01079 // TODO: uninstall all ID's 01080 throw TypecheckException 01081 ("Datatype "+names[firstNotWellFounded]+" has no finite terms"); 01082 } 01083 01084 return Expr(DATATYPE_DECL, returnTypes); 01085 } 01086 01087 Expr TheoryDatatype::datatypeConsExpr(const string& constructor, 01088 const vector<Expr>& args) 01089 { 01090 Expr e = resolveID(constructor); 01091 if (e.isNull()) 01092 throw Exception("datatype: unknown constructor: "+constructor); 01093 if (!(e.isSymbol() && e.getKind() == CONSTRUCTOR)) 01094 throw Exception("datatype: "+constructor+" resolves to: "+e.toString()+ 01095 "\nwhich is not a constructor"); 01096 if (args.size() == 0) return e; 01097 return Expr(e.mkOp(), args); 01098 } 01099 01100 01101 Expr TheoryDatatype::datatypeSelExpr(const string& selector, const Expr& arg) 01102 { 01103 Expr e = resolveID(selector); 01104 if (e.isNull()) 01105 throw Exception("datatype: unknown selector: "+selector); 01106 if (!(e.isSymbol() && e.getKind() == SELECTOR)) 01107 throw Exception("datatype: "+selector+" resolves to: "+e.toString()+ 01108 "\nwhich is not a selector"); 01109 return Expr(e.mkOp(), arg); 01110 } 01111 01112 01113 Expr TheoryDatatype::datatypeTestExpr(const string& constructor, const Expr& arg) 01114 { 01115 Expr e = resolveID("is_"+constructor); 01116 if (e.isNull()) 01117 throw Exception("datatype: unknown tester: is_"+constructor); 01118 if (!(e.isSymbol() && e.getKind() == TESTER)) 01119 throw Exception("datatype: is_"+constructor+" resolves to: "+e.toString()+ 01120 "\nwhich is not a tester"); 01121 return Expr(e.mkOp(), arg); 01122 } 01123 01124 01125 const pair<Expr,unsigned>& TheoryDatatype::getSelectorInfo(const Expr& e) 01126 { 01127 DebugAssert(e.getKind() == SELECTOR, "getSelectorInfo called on non-selector: " 01128 +e.toString()); 01129 DebugAssert(d_selectorMap.find(e) != d_selectorMap.end(), 01130 "Unknown selector: "+e.toString()); 01131 return d_selectorMap[e]; 01132 } 01133 01134 01135 Expr TheoryDatatype::getConsForTester(const Expr& e) 01136 { 01137 DebugAssert(e.getKind() == TESTER, 01138 "getConsForTester called on non-tester" 01139 +e.toString()); 01140 DebugAssert(d_testerMap.find(e) != d_testerMap.end(), 01141 "Unknown tester: "+e.toString()); 01142 return d_testerMap[e]; 01143 } 01144 01145 01146 unsigned TheoryDatatype::getConsPos(const Expr& e) 01147 { 01148 DebugAssert(e.getKind() == CONSTRUCTOR, 01149 "getConsPos called on non-constructor"); 01150 Type t = getBaseType(e); 01151 if (t.isFunction()) t = t[t.arity()-1]; 01152 DebugAssert(isDatatype(t), "Expected datatype"); 01153 DebugAssert(d_datatypes.find(t.getExpr()) != d_datatypes.end(), 01154 "Could not find datatype: "+t.toString()); 01155 ExprMap<unsigned>& constMap = d_datatypes[t.getExpr()]; 01156 DebugAssert(constMap.find(e) != constMap.end(), 01157 "Could not find constructor: "+e.toString()); 01158 return constMap[e]; 01159 } 01160 01161 01162 Expr TheoryDatatype::getConstant(const Type& t) 01163 { 01164 // if a cycle is detected, backtrack from this branch 01165 if (d_getConstantStack.count(t.getExpr()) != 0) { 01166 return Expr(); 01167 } 01168 DebugAssert(d_getConstantStack.size() < 1000, 01169 "TheoryDatatype::getconstant: too deep recursion depth"); 01170 d_getConstantStack[t.getExpr()] = true; 01171 if (isDatatype(t)) { 01172 DebugAssert(d_datatypes.find(t.getExpr()) != d_datatypes.end(), 01173 "Unknown datatype: "+t.getExpr().toString()); 01174 ExprMap<unsigned>& c = d_datatypes[t.getExpr()]; 01175 ExprMap<unsigned>::iterator i = c.begin(), iend = c.end(); 01176 for (; i != iend; ++i) { 01177 const Expr& cons = (*i).first; 01178 if (!getBaseType(cons).isFunction()) { 01179 d_getConstantStack.erase(t.getExpr()); 01180 return cons; 01181 } 01182 } 01183 for (i = c.begin(), iend = c.end(); i != iend; ++i) { 01184 const Expr& cons = (*i).first; 01185 Expr funType = getBaseType(cons).getExpr(); 01186 vector<Expr> args; 01187 int j = 0; 01188 for (; j < funType.arity()-1; ++j) { 01189 Type t_j = Type(funType[j]); 01190 if (t_j == t || isDatatype(t_j)) break; 01191 args.push_back(getConstant(t_j)); 01192 DebugAssert(!args.back().isNull(), "Expected non-null"); 01193 } 01194 if (j == funType.arity()-1) { 01195 d_getConstantStack.erase(t.getExpr()); 01196 return Expr(cons.mkOp(), args); 01197 } 01198 } 01199 for (i = c.begin(), iend = c.end(); i != iend; ++i) { 01200 const Expr& cons = (*i).first; 01201 Expr funType = getBaseType(cons).getExpr(); 01202 vector<Expr> args; 01203 int j = 0; 01204 for (; j < funType.arity()-1; ++j) { 01205 Type t_j = Type(funType[j]); 01206 if (t_j == t) break; 01207 args.push_back(getConstant(t_j)); 01208 if (args.back().isNull()) break; 01209 } 01210 if (j == funType.arity()-1) { 01211 d_getConstantStack.erase(t.getExpr()); 01212 return Expr(cons.mkOp(), args); 01213 } 01214 } 01215 FatalAssert(false, "Couldn't find constant for" 01216 +t.toString()); 01217 } 01218 DebugAssert(!t.isBool() && !t.isFunction(), 01219 "Expected non-bool, non-function type"); 01220 //TODO: this name could be an illegal identifier (i.e. could include spaces) 01221 string name = "datatype_"+t.getExpr().toString(); 01222 Expr e = resolveID(name); 01223 d_getConstantStack.erase(t.getExpr()); 01224 if (e.isNull()) return newVar(name, t); 01225 return e; 01226 } 01227 01228 01229 const Op& TheoryDatatype::getReachablePredicate(const Type& t) 01230 { 01231 DebugAssert(isDatatype(t), "Expected datatype"); 01232 DebugAssert(d_reach.find(t.getExpr()) != d_reach.end(), 01233 "Couldn't find reachable predicate"); 01234 return d_reach[t.getExpr()]; 01235 } 01236 01237 01238 bool TheoryDatatype::canCollapse(const Expr& e) 01239 { 01240 DebugAssert(isSelector(e), "canCollapse: Selector expression expected"); 01241 DebugAssert(e.arity() == 1, "expected arity 1"); 01242 if (isConstructor(e[0])) return true; 01243 if (d_labels.find(e[0]) == d_labels.end()) return false; 01244 DebugAssert(e[0].hasFind() && findExpr(e[0]) == e[0], 01245 "canCollapse: Expected find(e[0])=e[0]"); 01246 Unsigned u = d_labels[e[0]].get().get(); 01247 Expr cons = getSelectorInfo(e.getOpExpr()).first; 01248 Unsigned uCons = 1 << Unsigned(getConsPos(cons)); 01249 if ((u & uCons) == 0) return true; 01250 return false; 01251 }