00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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
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
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
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
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
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
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
00478
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
00494 }
00495 else if (getSize) {
00496 thisSize = thisSize * size;
00497
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
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
00730
00731
00732 Expr TheoryDatatype::parseExprOp(const Expr& e)
00733 {
00734
00735
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
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
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
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
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
00878
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
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
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 );
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
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
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
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
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 }