00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #include "theory_uf.h"
00022 #include "uf_proof_rules.h"
00023 #include "typecheck_exception.h"
00024 #include "parser_exception.h"
00025 #include "smtlib_exception.h"
00026 #include "command_line_flags.h"
00027 #include "theory_core.h"
00028
00029 #include "theory_records.h"
00030
00031
00032 using namespace std;
00033 using namespace CVC3;
00034
00035
00036
00037
00038
00039
00040
00041 TheoryUF::TheoryUF(TheoryCore* core)
00042 : Theory(core, "Uninterpreted Functions"),
00043 d_applicationsInModel(core->getFlags()["applications"].getBool()),
00044 d_funApplications(core->getCM()->getCurrentContext()),
00045 d_funApplicationsIdx(core->getCM()->getCurrentContext(), 0)
00046
00047 {
00048 d_rules = createProofRules();
00049
00050
00051 getEM()->newKind(TRANS_CLOSURE, "_TRANS_CLOSURE");
00052 getEM()->newKind(OLD_ARROW, "_OLD_ARROW", true);
00053
00054 vector<int> kinds;
00055
00056 kinds.push_back(TYPEDECL);
00057 kinds.push_back(LAMBDA);
00058 kinds.push_back(ARROW);
00059 kinds.push_back(OLD_ARROW);
00060 kinds.push_back(UFUNC);
00061 kinds.push_back(TRANS_CLOSURE);
00062
00063 registerTheory(this, kinds);
00064 }
00065
00066
00067 TheoryUF::~TheoryUF() {
00068 delete d_rules;
00069 }
00070
00071
00072
00073
00074
00075 void TheoryUF::assertFact(const Theorem& e)
00076 {
00077 const Expr& expr = e.getExpr();
00078 switch (expr.getKind()) {
00079 case NOT:
00080 break;
00081 case APPLY:
00082 if (expr.getOpExpr().computeTransClosure()) {
00083 enqueueFact(d_rules->relToClosure(e));
00084 }
00085 else if (expr.getOpKind() == TRANS_CLOSURE) {
00086
00087 DebugAssert(expr.isApply(), "Should be apply");
00088 Expr rel = resolveID(expr.getOpExpr().getName());
00089 DebugAssert(!rel.isNull(), "Expected known identifier");
00090 DebugAssert(rel.isSymbol() && rel.getKind()==UFUNC && expr.arity()==2,
00091 "Unexpected use of transitive closure: "+expr.toString());
00092
00093
00094 ExprMap<TCMapPair*>::iterator i = d_transClosureMap.find(rel);
00095 TCMapPair* pTable;
00096 if (i == d_transClosureMap.end()) {
00097 pTable = new TCMapPair();
00098 d_transClosureMap[rel] = pTable;
00099 }
00100 else {
00101 pTable = (*i).second;
00102 }
00103
00104 ExprMap<CDList<Theorem>*>::iterator i2 = pTable->appearsFirstMap.find(expr[0]);
00105 CDList<Theorem>* pList;
00106 if (i2 == pTable->appearsFirstMap.end()) {
00107 pList = new(true) CDList<Theorem>(theoryCore()->getCM()->getCurrentContext());
00108 pTable->appearsFirstMap[expr[0]] = pList;
00109 }
00110 else {
00111 pList = (*i2).second;
00112 }
00113 pList->push_back(e);
00114
00115 i2 = pTable->appearsSecondMap.find(expr[1]);
00116 if (i2 == pTable->appearsSecondMap.end()) {
00117 pList = new(true) CDList<Theorem>(theoryCore()->getCM()->getCurrentContext());
00118 pTable->appearsSecondMap[expr[1]] = pList;
00119 }
00120 else {
00121 pList = (*i2).second;
00122 }
00123 pList->push_back(e);
00124
00125
00126 size_t s,l;
00127 i2 = pTable->appearsFirstMap.find(expr[1]);
00128 if (i2 != pTable->appearsFirstMap.end()) {
00129 pList = (*i2).second;
00130 s = pList->size();
00131 for (l = 0; l < s; ++l) {
00132 enqueueFact(d_rules->relTrans(e,(*pList)[l]));
00133 }
00134 }
00135
00136 i2 = pTable->appearsSecondMap.find(expr[0]);
00137 if (i2 != pTable->appearsSecondMap.end()) {
00138 pList = (*i2).second;
00139 s = pList->size();
00140 for (l = 0; l < s; ++l) {
00141 enqueueFact(d_rules->relTrans((*pList)[l],e));
00142 }
00143 }
00144 }
00145 break;
00146 default:
00147 break;
00148 }
00149 }
00150
00151
00152 void TheoryUF::checkSat(bool fullEffort)
00153 {
00154
00155 for(; d_funApplicationsIdx < d_funApplications.size();
00156 d_funApplicationsIdx = d_funApplicationsIdx + 1) {
00157 const Expr& e = d_funApplications[d_funApplicationsIdx];
00158 if(e.getOp().getExpr().isLambda()) {
00159 IF_DEBUG(debugger.counter("Expanded lambdas (checkSat)")++);
00160 enqueueFact(d_rules->applyLambda(e));
00161 }
00162 }
00163 }
00164
00165
00166 Theorem TheoryUF::rewrite(const Expr& e)
00167 {
00168 if (e.isApply()) {
00169 const Expr& op = e.getOpExpr();
00170 int opKind = op.getKind();
00171 switch(opKind) {
00172 case LAMBDA: {
00173 Theorem res = d_rules->applyLambda(e);
00174
00175 res = transitivityRule(res, simplify(res.getRHS()));
00176 IF_DEBUG(debugger.counter("Expanded lambdas")++);
00177 return res;
00178 }
00179 default:
00180 if (e.getType().isBool()) return reflexivityRule(e);
00181 else return rewriteCC(e);
00182 }
00183 }
00184 else {
00185 e.setRewriteNormal();
00186 return reflexivityRule(e);
00187 }
00188 }
00189
00190
00191 void TheoryUF::setup(const Expr& e)
00192 {
00193 if (e.getKind() != APPLY) return;
00194
00195
00196
00197
00198
00199
00200 setupCC(e);
00201
00202
00203 TRACE("model", "TheoryUF: add function application ", e, "");
00204 d_funApplications.push_back(e);
00205 }
00206
00207
00208 void TheoryUF::update(const Theorem& e, const Expr& d)
00209 {
00210
00211
00212
00213
00214
00215
00216
00217
00218
00219
00220
00221
00222
00223
00224
00225
00226
00227
00228
00229
00230
00231
00232
00233
00234
00235
00236
00237
00238
00239
00240
00241
00242
00243 const Theorem& dEQdsig = d.getSig();
00244 if (!dEQdsig.isNull()) {
00245 const Expr& dsig = dEQdsig.getRHS();
00246 Theorem thm = updateHelper(d);
00247 const Expr& sigNew = thm.getRHS();
00248 if (sigNew == dsig) {
00249
00250 return;
00251 }
00252 dsig.setRep(Theorem());
00253 const Theorem& repEQsigNew = sigNew.getRep();
00254 if (!repEQsigNew.isNull()) {
00255 d.setSig(Theorem());
00256 enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
00257 }
00258 else if (d.getType().isBool()) {
00259 d.setSig(Theorem());
00260 enqueueFact(thm);
00261 }
00262 else {
00263 int k, ar(d.arity());
00264 for (k = 0; k < ar; ++k) {
00265 if (sigNew[k] != dsig[k]) {
00266 sigNew[k].addToNotify(this, d);
00267 }
00268 }
00269 d.setSig(thm);
00270 sigNew.setRep(thm);
00271 if (dsig != sigNew && d.isApply() && findExpr(d).isTrue()) {
00272 if (d.getOpExpr().computeTransClosure()) {
00273 thm = getCommonRules()->iffTrueElim(transitivityRule(symmetryRule(thm),
00274 find(d)));
00275 enqueueFact(d_rules->relToClosure(thm));
00276 }
00277 else if (d.getOpKind() == TRANS_CLOSURE) {
00278 thm = getCommonRules()->iffTrueElim(transitivityRule(symmetryRule(thm),
00279 find(d)));
00280 enqueueFact(thm);
00281 }
00282 }
00283 }
00284 }
00285 }
00286
00287
00288 void TheoryUF::checkType(const Expr& e)
00289 {
00290 switch (e.getKind()) {
00291 case ARROW: {
00292 if (e.arity() < 2) throw Exception
00293 ("Function type needs at least two arguments"
00294 +e.toString());
00295 Expr::iterator i = e.begin(), iend = e.end();
00296 for (; i != iend; ) {
00297 Type t(*i);
00298 ++i;
00299 if (i == iend && t.isBool()) break;
00300 if (t.isBool()) throw Exception
00301 ("Function argument types must be non-Boolean: "
00302 +e.toString());
00303 if (t.isFunction()) throw Exception
00304 ("Function domain or range types cannot be functions: "
00305 +e.toString());
00306 }
00307 break;
00308 }
00309 case TYPEDECL: {
00310 break;
00311 }
00312 default:
00313 DebugAssert(false, "Unexpected kind in TheoryUF::checkType"
00314 +getEM()->getKindName(e.getKind()));
00315 }
00316 }
00317
00318
00319 void TheoryUF::computeType(const Expr& e)
00320 {
00321 switch (e.getKind()) {
00322 case LAMBDA: {
00323 vector<Type> args;
00324 const vector<Expr>& vars = e.getVars();
00325 DebugAssert(vars.size() > 0,
00326 "TheorySimulate::computeType("+e.toString()+")");
00327 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
00328 i!=iend; ++i)
00329 args.push_back((*i).getType());
00330 e.setType(Type::funType(args, e.getBody().getType()));
00331 break;
00332 }
00333 case APPLY: {
00334 theoryOf(APPLY)->computeType(e);
00335 break;
00336 }
00337 case TRANS_CLOSURE: {
00338 DebugAssert(e.isSymbol(), "Expected symbol");
00339 Expr funExpr = resolveID(e.getName());
00340 if (funExpr.isNull()) {
00341 throw TypecheckException
00342 ("Attempt to take transitive closure of unknown id: "
00343 +e.getName());
00344 }
00345 Type funType = funExpr.getType();
00346 if(!funType.isFunction()) {
00347 throw TypecheckException
00348 ("Attempt to take transitive closure of non-function:\n\n"
00349 +funExpr.toString() + "\n\n which has type: "
00350 +funType.toString());
00351 }
00352 if(funType.arity()!=3) {
00353 throw TypecheckException
00354 ("Attempt to take transitive closure of non-binary function:\n\n"
00355 +funExpr.toString() + "\n\n which has type: "
00356 +funType.toString());
00357 }
00358 if (!funType[2].isBool()) {
00359 throw TypecheckException
00360 ("Attempt to take transitive closure of function:\n\n"
00361 +funExpr.toString() + "\n\n which does not return BOOLEAN");
00362 }
00363 e.setType(funType);
00364 break;
00365 }
00366 default:
00367 DebugAssert(false,"Unexpected type: "+e.toString());
00368 break;
00369 }
00370 }
00371
00372
00373 Type TheoryUF::computeBaseType(const Type& t) {
00374 const Expr& e = t.getExpr();
00375 switch(e.getKind()) {
00376 case ARROW: {
00377 DebugAssert(e.arity() > 0, "Expected non-empty ARROW");
00378 vector<Expr> kids;
00379 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00380 kids.push_back(getBaseType(Type(*i)).getExpr());
00381 }
00382 return Type(Expr(e.getOp(), kids));
00383 }
00384 case TYPEDECL: return t;
00385 default:
00386 DebugAssert(false,
00387 "TheoryUF::computeBaseType("+t.toString()+")");
00388 return t;
00389 }
00390 }
00391
00392
00393 void TheoryUF::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
00394 for(CDList<Expr>::const_iterator i=d_funApplications.begin(),
00395 iend=d_funApplications.end(); i!=iend; ++i) {
00396 if((*i).isApply() && (*i).getOp().getExpr() == e) {
00397
00398
00399 v.push_back(*i);
00400
00401
00402
00403 for(Expr::iterator j=(*i).begin(), jend=(*i).end(); j!=jend; ++j)
00404
00405 v.push_back(*j);
00406 }
00407 }
00408 }
00409
00410
00411 void TheoryUF::computeModel(const Expr& e, std::vector<Expr>& vars) {
00412
00413
00414
00415
00416
00417
00418 vars.push_back(e);
00419
00420 ExprHashMap<Expr> appls;
00421 for(CDList<Expr>::const_iterator i=d_funApplications.begin(),
00422 iend=d_funApplications.end(); i!=iend; ++i) {
00423 if((*i).isApply() && (*i).getOp().getExpr() == e) {
00424
00425 vector<Theorem> thms;
00426 vector<unsigned> changed;
00427 for(int j=0; j<(*i).arity(); ++j) {
00428 Theorem asst(getModelValue((*i)[j]));
00429 if(asst.getLHS()!=asst.getRHS()) {
00430 thms.push_back(asst);
00431 changed.push_back(j);
00432 }
00433 }
00434 Expr var;
00435 if(changed.size()>0) {
00436
00437
00438 Theorem subst = substitutivityRule(*i, changed, thms);
00439 assignValue(transitivityRule(symmetryRule(subst), getModelValue(*i)));
00440 var = subst.getRHS();
00441 } else
00442 var = *i;
00443 if(d_applicationsInModel) vars.push_back(var);
00444
00445 appls[var] = getModelValue(var).getRHS();
00446 }
00447 }
00448
00449 if(appls.size()==0) {
00450 assignValue(reflexivityRule(e));
00451 } else {
00452
00453 vector<Expr> args;
00454 Type tp(e.getType());
00455 static unsigned count(0);
00456 DebugAssert(tp.isFunction(), "TheoryUF::computeModel("+e.toString()
00457 +" : "+tp.toString()+")");
00458 for(int i=0, iend=tp.arity()-1; i<iend; ++i) {
00459 Expr v = getEM()->newBoundVarExpr("uf", int2string(count++));
00460 v.setType(tp[i]);
00461 args.push_back(v);
00462 }
00463 DebugAssert(args.size()>0, "TheoryUF::computeModel()");
00464 ExprHashMap<Expr>::iterator i=appls.begin(), iend=appls.end();
00465 DebugAssert(i!=iend, "TheoryUF::computeModel(): empty appls hash");
00466
00467 Expr res((*i).second); ++i;
00468 for(; i!=iend; ++i) {
00469
00470
00471
00472 if((*i).second == res) continue;
00473
00474
00475 Expr cond;
00476 vector<Expr> eqs;
00477 for(int j=0, jend=args.size(); j<jend; ++j)
00478 eqs.push_back(args[j].eqExpr((*i).first[j]));
00479 if(eqs.size()==1)
00480 cond = eqs[0];
00481 else
00482 cond = andExpr(eqs);
00483
00484 res = cond.iteExpr((*i).second, res);
00485 }
00486 res = lambdaExpr(args, res);
00487 assignValue(e, res);
00488 }
00489 }
00490
00491
00492 Expr TheoryUF::computeTCC(const Expr& e)
00493 {
00494 switch (e.getKind()) {
00495 case APPLY: {
00496
00497
00498
00499
00500
00501
00502
00503
00504
00505
00506
00507
00508
00509
00510
00511
00512
00513
00514
00515
00516 vector<Expr> preds;
00517 preds.push_back(Theory::computeTCC(e));
00518 DebugAssert(e.isApply(), "Should be application");
00519 Expr op(e.getOp().getExpr());
00520 Type funType(op.getType());
00521 DebugAssert(funType.isFunction() || funType.isBool(),
00522 "TheoryUF::computeTCC(): funType = "
00523 +funType.toString());
00524 if(funType.isFunction()) {
00525 DebugAssert(funType.arity() == e.arity()+1,
00526 "TheoryUF::computeTCC(): funType = "
00527 +funType.toString()+"\n e = "+e.toString());
00528 for(int i=0, iend=e.arity(); i<iend; ++i) {
00529
00530
00531
00532 if(funType[i] != e[i].getType())
00533 preds.push_back(getTypePred(funType[i], e[i]));
00534 }
00535 }
00536
00537 while(op.getKind()==LETDECL) op = op[1];
00538
00539 if(op.isLambda()) {
00540 preds.push_back(Expr(lambdaExpr(op.getVars(),
00541 getTCC(op.getBody())).mkOp(),
00542 e.getKids()));
00543 }
00544 return rewriteAnd(andExpr(preds)).getRHS();
00545 }
00546 case LAMBDA:
00547 return trueExpr();
00548 default:
00549 DebugAssert(false,"Unexpected type: "+e.toString());
00550 return trueExpr();
00551 }
00552 }
00553
00554
00555
00556
00557
00558
00559 ExprStream& TheoryUF::print(ExprStream& os, const Expr& e) {
00560 switch(os.lang()) {
00561 case SIMPLIFY_LANG:
00562 switch(e.getKind()) {
00563 case OLD_ARROW:
00564 case ARROW:
00565 os<<"ERROR:ARROW:unsupported in Simplify\n";
00566 break;
00567 case LAMBDA: {
00568 os<<"ERROR:LAMBDA:unsupported in Simplify\n";
00569 break;
00570 }
00571 case TRANS_CLOSURE:
00572 os<<"ERROR:TRANS_CLOSURE:unsupported in Simplify\n";
00573 break;
00574 case TYPEDECL:
00575 os<<"ERROR:TYPEDECL:unsupported in Simplify\n";
00576 break;
00577 case UFUNC:
00578 case APPLY:
00579 if(e.isApply()) os << "(" << e.getOp().getExpr()<<" ";
00580 if(e.arity() > 0) {
00581 bool first(true);
00582 for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00583 if(first) first = false;
00584 else os << " " ;
00585 os << *i;
00586 }
00587 os << ")";
00588 }
00589 break;
00590 default: {
00591 DebugAssert(false, "TheoryUF::print: Unexpected expression: "
00592 +getEM()->getKindName(e.getKind()));
00593 }
00594 }
00595 break;
00596
00597 case PRESENTATION_LANG:
00598 switch(e.getKind()) {
00599 case OLD_ARROW:
00600 case ARROW:
00601 if(e.arity() < 2) e.printAST(os);
00602 else {
00603 if(e.arity() == 2)
00604 os << e[0];
00605 else {
00606 os << "(" << push;
00607 bool first(true);
00608 for(int i=0, iend=e.arity()-1; i<iend; ++i) {
00609 if(first) first=false;
00610 else os << "," << space;
00611 os << e[i];
00612 }
00613 os << push << ")" << pop << pop;
00614 }
00615 os << space << "-> " << space << e[e.arity()-1];
00616 }
00617 break;
00618 case TYPEDECL:
00619
00620
00621
00622 if(e.arity() != 1) e.printAST(os);
00623 else os << e[0].getString();
00624 break;
00625 case LAMBDA: {
00626 DebugAssert(e.isLambda(), "Expected Lambda");
00627 os << "(" << push << "LAMBDA" << space << push;
00628 const vector<Expr>& vars = e.getVars();
00629 bool first(true);
00630 os << "(" << push;
00631 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
00632 i!=iend; ++i) {
00633 if(first) first = false;
00634 else os << push << "," << pop << space;
00635 os << *i;
00636
00637
00638 if(i->isVar())
00639 os << ":" << space << pushdag << (*i).getType() << popdag;
00640 }
00641 os << push << "): " << pushdag << push
00642 << e.getBody() << push << ")";
00643 break;
00644 }
00645 case APPLY:
00646 os << e.getOpExpr();
00647 if(e.arity() > 0) {
00648 os << "(" << push;
00649 bool first(true);
00650 for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00651 if(first) first = false;
00652 else os << "," << space;
00653 os << *i;
00654 }
00655 os << push << ")";
00656 }
00657 break;
00658 case TRANS_CLOSURE:
00659 DebugAssert(e.isSymbol(), "Expected symbol");
00660 os << e.getName() << "*";
00661 break;
00662 case UFUNC:
00663 DebugAssert(e.isSymbol(), "Expected symbol");
00664 os << e.getName();
00665 break;
00666 default: {
00667 DebugAssert(false, "TheoryUF::print: Unexpected expression: "
00668 +getEM()->getKindName(e.getKind()));
00669 }
00670 }
00671 break;
00672 case SMTLIB_LANG:
00673 switch(e.getKind()) {
00674 case OLD_ARROW:
00675 case ARROW: {
00676 if(e.arity() < 2) {
00677 throw SmtlibException("TheoryUF::print: Expected 2 or more arguments to ARROW");
00678
00679 }
00680 d_theoryUsed = true;
00681 os << push;
00682 int iend = e.arity();
00683 if (e[iend-1].getKind() == BOOLEAN) --iend;
00684 for(int i=0; i<iend; ++i) {
00685 if (i != 0) os << space;
00686 os << e[i];
00687 }
00688 break;
00689 }
00690 case TYPEDECL:
00691 if (e.arity() == 1 && e[0].isString()) {
00692 os << e[0].getString();
00693 break;
00694 }
00695
00696
00697
00698 throw SmtlibException("TheoryUF::print: TYPEDECL not supported");
00699
00700
00701
00702 break;
00703 case APPLY:
00704 if (e.arity() == 0) os << e.getOp().getExpr();
00705 else {
00706 os << "(" << push << e.getOp().getExpr();
00707 for (int i=0, iend=e.arity(); i<iend; ++i)
00708 os << space << e[i];
00709 if (e.getOpKind() == TRANS_CLOSURE) {
00710 os << space << ":transclose";
00711 }
00712 os << push << ")";
00713 }
00714 break;
00715 case TRANS_CLOSURE:
00716 os << e.getName();
00717 break;
00718 case UFUNC:
00719 DebugAssert(e.isSymbol(), "Expected symbol");
00720 os << e.getName();
00721 break;
00722 default: {
00723 DebugAssert(false, "TheoryUF::print: SMTLIB_LANG: Unexpected expression: "
00724 +getEM()->getKindName(e.getKind()));
00725 }
00726 }
00727 break;
00728 case LISP_LANG:
00729 switch(e.getKind()) {
00730 case OLD_ARROW:
00731 case ARROW:
00732 if(e.arity() < 2) e.printAST(os);
00733 os << "(" << push << "ARROW";
00734 for(int i=0, iend=e.arity(); i<iend; ++i)
00735 os << space << e[i];
00736 os << push << ")";
00737 break;
00738 case TRANS_CLOSURE:
00739 e.printAST(os);
00740 break;
00741 case TYPEDECL:
00742
00743
00744
00745 if(e.arity() != 1) e.printAST(os);
00746 else if(e[0].isString()) os << e[0].getString();
00747 else e[0].print(os);
00748 break;
00749 case LAMBDA: {
00750 DebugAssert(e.isLambda(), "Expected LAMBDA");
00751 os << "(" << push << "LAMBDA" << space;
00752 const vector<Expr>& vars = e.getVars();
00753 bool first(true);
00754 os << "(" << push;
00755 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
00756 i!=iend; ++i) {
00757 if(first) first = false;
00758 else os << space;
00759 os << "(" << push << *i;
00760
00761
00762 if(i->isVar())
00763 os << space << pushdag << (*i).getType() << popdag;
00764 os << push << ")" << pop << pop;
00765 }
00766 os << push << ")" << pop << pop << pushdag
00767 << e.getBody() << push << ")";
00768 break;
00769 }
00770 case APPLY:
00771 DebugAssert(e.isApply(), "Expected Apply");
00772 if (e.arity() == 0) os << e.getOp().getExpr();
00773 else {
00774 os << "(" << push << e.getOp().getExpr();
00775 for (int i=0, iend=e.arity(); i<iend; ++i)
00776 os << space << e[i];
00777 os << push << ")";
00778 }
00779 break;
00780 default: {
00781 DebugAssert(false, "TheoryUF::print: Unexpected expression: "
00782 +getEM()->getKindName(e.getKind()));
00783 }
00784 }
00785 break;
00786 default:
00787
00788
00789 e.printAST(os);
00790 break;
00791 }
00792 return os;
00793 }
00794
00795
00796
00797
00798
00799 Expr
00800 TheoryUF::parseExprOp(const Expr& e) {
00801
00802
00803 if(RAW_LIST != e.getKind()) return e;
00804
00805 DebugAssert(e.arity() > 0,
00806 "TheoryUF::parseExprOp:\n e = "+e.toString());
00807
00808 const Expr& c1 = e[0][0];
00809 int kind = getEM()->getKind(c1.getString());
00810 switch(kind) {
00811 case OLD_ARROW: {
00812 if (!theoryCore()->getFlags()["old-func-syntax"].getBool()) {
00813 throw ParserException("You seem to be using the old syntax for function types.\n"
00814 "Please convert to the new syntax or run with +old-func-syntax");
00815 }
00816 DebugAssert(e.arity()==3,"Expected arity 3 in OLD_ARROW");
00817 Expr arg = parseExpr(e[1]);
00818 vector<Expr> k;
00819 if (arg.getOpKind() == TUPLE_TYPE) {
00820 Expr::iterator i = arg.begin(), iend=arg.end();
00821 for (; i != iend; ++i) {
00822 k.push_back(*i);
00823 }
00824 }
00825 else k.push_back(arg);
00826 k.push_back(parseExpr(e[2]));
00827 return Expr(ARROW, k);
00828 }
00829 case ARROW:
00830 case TYPEDECL: {
00831 vector<Expr> k;
00832 Expr::iterator i = e.begin(), iend=e.end();
00833
00834
00835 ++i;
00836
00837 for(; i!=iend; ++i)
00838 k.push_back(parseExpr(*i));
00839 return Expr(kind, k, e.getEM());
00840 break;
00841 }
00842 case TRANS_CLOSURE: {
00843 if(e.arity() != 4)
00844 throw ParserException("Wrong number of arguments to "
00845 "TRANS_CLOSURE expression\n"
00846 " (expected 3 arguments): "+e.toString());
00847 const string& name = e[1][0].getString();
00848 Expr funExpr = resolveID(name);
00849 if (funExpr.isNull())
00850 throw ParserException("Attempt to take transitive closure of unknown "
00851 "predicate"+name);
00852 return transClosureExpr(name, parseExpr(e[2]), parseExpr(e[3]));
00853 }
00854 case LAMBDA: {
00855 if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0))
00856 throw ParserException("Bad LAMBDA expression: "+e.toString());
00857
00858 vector<pair<string,Type> > vars;
00859 for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
00860 if(i->getKind() != RAW_LIST || i->arity() < 2)
00861 throw ParserException("Bad variable declaration block in LAMBDA "
00862 "expression: "+i->toString()+
00863 "\n e = "+e.toString());
00864
00865
00866
00867 Type tp(parseExpr((*i)[i->arity()-1]));
00868 for(int j=0, jend=i->arity()-1; j<jend; ++j) {
00869 if((*i)[j].getKind() != ID)
00870 throw ParserException("Bad variable declaration in LAMBDA"
00871 " expression: "+(*i)[j].toString()+
00872 "\n e = "+e.toString());
00873 vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
00874 }
00875 }
00876
00877 vector<Expr> boundVars;
00878 for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
00879 i!=iend; ++i)
00880 boundVars.push_back(addBoundVar(i->first, i->second));
00881
00882 Expr body(parseExpr(e[2]));
00883
00884 return lambdaExpr(boundVars, body);
00885 break;
00886 }
00887
00888 default: {
00889 if(e.arity() < 2)
00890 throw ParserException("Bad function application: "+e.toString());
00891 Expr::iterator i=e.begin(), iend=e.end();
00892 Expr op(parseExpr(*i)); ++i;
00893 vector<Expr> args;
00894 for(; i!=iend; ++i) args.push_back(parseExpr(*i));
00895 return Expr(op.mkOp(), args);
00896 }
00897 }
00898 return e;
00899 }
00900
00901
00902 Expr TheoryUF::lambdaExpr(const vector<Expr>& vars, const Expr& body) {
00903 return getEM()->newClosureExpr(LAMBDA, vars, body);
00904 }
00905
00906
00907 Expr TheoryUF::transClosureExpr(const std::string& name, const Expr& e1,
00908 const Expr& e2) {
00909 return Expr(getEM()->newSymbolExpr(name, TRANS_CLOSURE).mkOp(), e1, e2);
00910 }