CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file theory_uf.cpp 00004 * 00005 * Author: Clark Barrett 00006 * 00007 * Created: Fri Jan 24 02:07:59 2003 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 */ 00019 /*****************************************************************************/ 00020 00021 #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 #include "translator.h" 00029 // HACK: include theory_records.h to access the TUPLE_TYPE kind 00030 #include "theory_records.h" 00031 00032 00033 using namespace std; 00034 using namespace CVC3; 00035 00036 00037 /////////////////////////////////////////////////////////////////////////////// 00038 // TheoryUF Public Methods // 00039 /////////////////////////////////////////////////////////////////////////////// 00040 00041 00042 TheoryUF::TheoryUF(TheoryCore* core)//, bool useAckermann) 00043 : Theory(core, "Uninterpreted Functions"), 00044 d_applicationsInModel(core->getFlags()["applications"].getBool()), 00045 d_funApplications(core->getCM()->getCurrentContext()), 00046 d_funApplicationsIdx(core->getCM()->getCurrentContext(), 0) 00047 // d_useAckermann(useAckermann) 00048 { 00049 d_rules = createProofRules(); 00050 00051 // Register new local kinds with ExprManager 00052 getEM()->newKind(TRANS_CLOSURE, "_TRANS_CLOSURE"); 00053 getEM()->newKind(OLD_ARROW, "_OLD_ARROW", true); 00054 00055 vector<int> kinds; 00056 //TODO: should this stuff really be in theory_uf? 00057 kinds.push_back(TYPEDECL); 00058 kinds.push_back(LAMBDA); 00059 kinds.push_back(ARROW); 00060 kinds.push_back(OLD_ARROW); 00061 kinds.push_back(UFUNC); 00062 kinds.push_back(TRANS_CLOSURE); 00063 00064 registerTheory(this, kinds); 00065 } 00066 00067 00068 TheoryUF::~TheoryUF() { 00069 delete d_rules; 00070 } 00071 00072 00073 //TODO: clean up transitive closure tables 00074 // be sure to free CD objects 00075 00076 void TheoryUF::assertFact(const Theorem& e) 00077 { 00078 const Expr& expr = e.getExpr(); 00079 switch (expr.getKind()) { 00080 case NOT: 00081 break; 00082 case APPLY: 00083 if (expr.getOpExpr().computeTransClosure()) { 00084 enqueueFact(d_rules->relToClosure(e)); 00085 } 00086 else if (expr.getOpKind() == TRANS_CLOSURE) { 00087 // const Expr& rel = expr.getFun(); 00088 DebugAssert(expr.isApply(), "Should be apply"); 00089 Expr rel = resolveID(expr.getOpExpr().getName()); 00090 DebugAssert(!rel.isNull(), "Expected known identifier"); 00091 DebugAssert(rel.isSymbol() && rel.getKind()==UFUNC && expr.arity()==2, 00092 "Unexpected use of transitive closure: "+expr.toString()); 00093 00094 // Insert into transitive closure table 00095 ExprMap<TCMapPair*>::iterator i = d_transClosureMap.find(rel); 00096 TCMapPair* pTable; 00097 if (i == d_transClosureMap.end()) { 00098 pTable = new TCMapPair(); 00099 d_transClosureMap[rel] = pTable; 00100 } 00101 else { 00102 pTable = (*i).second; 00103 } 00104 00105 ExprMap<CDList<Theorem>*>::iterator i2 = pTable->appearsFirstMap.find(expr[0]); 00106 CDList<Theorem>* pList; 00107 if (i2 == pTable->appearsFirstMap.end()) { 00108 pList = new(true) CDList<Theorem>(theoryCore()->getCM()->getCurrentContext()); 00109 pTable->appearsFirstMap[expr[0]] = pList; 00110 } 00111 else { 00112 pList = (*i2).second; 00113 } 00114 pList->push_back(e); 00115 00116 i2 = pTable->appearsSecondMap.find(expr[1]); 00117 if (i2 == pTable->appearsSecondMap.end()) { 00118 pList = new(true) CDList<Theorem>(theoryCore()->getCM()->getCurrentContext()); 00119 pTable->appearsSecondMap[expr[1]] = pList; 00120 } 00121 else { 00122 pList = (*i2).second; 00123 } 00124 pList->push_back(e); 00125 00126 // Compute transitive closure with existing relations 00127 size_t s,l; 00128 i2 = pTable->appearsFirstMap.find(expr[1]); 00129 if (i2 != pTable->appearsFirstMap.end()) { 00130 pList = (*i2).second; 00131 s = pList->size(); 00132 for (l = 0; l < s; ++l) { 00133 enqueueFact(d_rules->relTrans(e,(*pList)[l])); 00134 } 00135 } 00136 00137 i2 = pTable->appearsSecondMap.find(expr[0]); 00138 if (i2 != pTable->appearsSecondMap.end()) { 00139 pList = (*i2).second; 00140 s = pList->size(); 00141 for (l = 0; l < s; ++l) { 00142 enqueueFact(d_rules->relTrans((*pList)[l],e)); 00143 } 00144 } 00145 } 00146 break; 00147 default: 00148 break; 00149 } 00150 } 00151 00152 00153 void TheoryUF::checkSat(bool fullEffort) 00154 { 00155 // Check for any unexpanded lambdas 00156 for(; d_funApplicationsIdx < d_funApplications.size(); 00157 d_funApplicationsIdx = d_funApplicationsIdx + 1) { 00158 const Expr& e = d_funApplications[d_funApplicationsIdx]; 00159 if(e.getOp().getExpr().isLambda()) { 00160 IF_DEBUG(debugger.counter("Expanded lambdas (checkSat)")++;) 00161 enqueueFact(d_rules->applyLambda(e)); 00162 } 00163 } 00164 } 00165 00166 00167 Theorem TheoryUF::rewrite(const Expr& e) 00168 { 00169 if (e.isApply()) { 00170 const Expr& op = e.getOpExpr(); 00171 int opKind = op.getKind(); 00172 switch(opKind) { 00173 case LAMBDA: { 00174 Theorem res = d_rules->applyLambda(e); 00175 // Simplify recursively 00176 res = transitivityRule(res, simplify(res.getRHS())); 00177 IF_DEBUG(debugger.counter("Expanded lambdas")++;) 00178 return res; 00179 } 00180 default: // A truly uninterpreted function 00181 if (e.getType().isBool()) return reflexivityRule(e); 00182 else return rewriteCC(e); 00183 } 00184 } 00185 else { 00186 e.setRewriteNormal(); 00187 return reflexivityRule(e); 00188 } 00189 } 00190 00191 00192 void TheoryUF::setup(const Expr& e) 00193 { 00194 if (e.getKind() != APPLY) return; 00195 // if (d_useAckermann) { 00196 // Theorem thm = getCommonRules()->varIntroSkolem(e); 00197 // theoryCore()->addToVarDB(thm.getRHS()); 00198 // enqueueFact(thm); 00199 // } 00200 // else { 00201 setupCC(e); 00202 // } 00203 // Add this function application for concrete model generation 00204 TRACE("model", "TheoryUF: add function application ", e, ""); 00205 d_funApplications.push_back(e); 00206 } 00207 00208 00209 void TheoryUF::update(const Theorem& e, const Expr& d) 00210 { 00211 /* 00212 int k, ar(d.arity()); 00213 const Theorem& dEQdsig = d.getSig(); 00214 if (!dEQdsig.isNull()) { 00215 Expr dsig = dEQdsig.getRHS(); 00216 Theorem thm = updateHelper(d); 00217 const Expr& sigNew = thm.getRHS(); 00218 if (sigNew == dsig) return; 00219 dsig.setRep(Theorem()); 00220 const Theorem& repEQsigNew = sigNew.getRep(); 00221 if (!repEQsigNew.isNull()) { 00222 d.setSig(Theorem()); 00223 enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm))); 00224 } 00225 else { 00226 for (k = 0; k < ar; ++k) { 00227 if (sigNew[k] != dsig[k]) { 00228 sigNew[k].addToNotify(this, d); 00229 } 00230 } 00231 d.setSig(thm); 00232 sigNew.setRep(thm); 00233 00234 if (d_compute_trans_closure && d.getKind() == APPLY && 00235 d.arity() == 2 && findExpr(d).isTrue()) { 00236 thm = iffTrueElim(transitivityRule(symmetryRule(thm),find(d))); 00237 enqueueFact(d_rules->relToClosure(thm)); 00238 } 00239 00240 } 00241 } 00242 */ 00243 // Record the original signature 00244 const Theorem& dEQdsig = d.getSig(); 00245 if (!dEQdsig.isNull()) { 00246 const Expr& dsig = dEQdsig.getRHS(); 00247 Theorem thm = updateHelper(d); 00248 const Expr& sigNew = thm.getRHS(); 00249 if (sigNew == dsig) { 00250 // TRACE_MSG("facts update", "updateCC["+getName()+"]() [no change] => }"); 00251 return; 00252 } 00253 dsig.setRep(Theorem()); 00254 const Theorem& repEQsigNew = sigNew.getRep(); 00255 if (!repEQsigNew.isNull()) { 00256 d.setSig(Theorem()); 00257 enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm))); 00258 } 00259 else if (d.getType().isBool()) { 00260 d.setSig(Theorem()); 00261 enqueueFact(thm); 00262 } 00263 else { 00264 int k, ar(d.arity()); 00265 for (k = 0; k < ar; ++k) { 00266 if (sigNew[k] != dsig[k]) { 00267 sigNew[k].addToNotify(this, d); 00268 } 00269 } 00270 d.setSig(thm); 00271 sigNew.setRep(thm); 00272 if (dsig != sigNew && d.isApply() && findExpr(d).isTrue()) { 00273 if (d.getOpExpr().computeTransClosure()) { 00274 thm = getCommonRules()->iffTrueElim(transitivityRule(symmetryRule(thm), 00275 find(d))); 00276 enqueueFact(d_rules->relToClosure(thm)); 00277 } 00278 else if (d.getOpKind() == TRANS_CLOSURE) { 00279 thm = getCommonRules()->iffTrueElim(transitivityRule(symmetryRule(thm), 00280 find(d))); 00281 enqueueFact(thm); 00282 } 00283 } 00284 } 00285 } 00286 } 00287 00288 00289 void TheoryUF::checkType(const Expr& e) 00290 { 00291 switch (e.getKind()) { 00292 case ARROW: { 00293 if (e.arity() < 2) throw Exception 00294 ("Function type needs at least two arguments" 00295 +e.toString()); 00296 Expr::iterator i = e.begin(), iend = e.end(); 00297 for (; i != iend; ) { 00298 Type t(*i); 00299 ++i; 00300 if (i == iend && t.isBool()) break; 00301 if (t.isBool()) throw Exception 00302 ("Function argument types must be non-Boolean: " 00303 +e.toString()); 00304 if (t.isFunction()) throw Exception 00305 ("Function domain or range types cannot be functions: " 00306 +e.toString()); 00307 } 00308 break; 00309 } 00310 case TYPEDECL: { 00311 break; 00312 } 00313 default: 00314 DebugAssert(false, "Unexpected kind in TheoryUF::checkType" 00315 +getEM()->getKindName(e.getKind())); 00316 } 00317 } 00318 00319 00320 Cardinality TheoryUF::finiteTypeInfo(Expr& e, Unsigned& n, 00321 bool enumerate, bool computeSize) 00322 { 00323 DebugAssert(e.getKind() == ARROW, 00324 "Unexpected kind in TheoryUF::finiteTypeInfo"); 00325 Expr::iterator i = e.begin(), iend = e.end(); 00326 Cardinality card = CARD_FINITE, cardTmp; 00327 Unsigned thisSize = 1, size; 00328 bool getSize = enumerate || computeSize; 00329 for (; i != iend; ) { 00330 Expr e2 = (*i); 00331 cardTmp = theoryOf(e2)->finiteTypeInfo(e2, size, getSize, false); 00332 if (cardTmp == CARD_INFINITE) { 00333 return CARD_INFINITE; 00334 } 00335 else if (cardTmp == CARD_UNKNOWN) { 00336 card = CARD_UNKNOWN; 00337 getSize = false; 00338 // Keep looking to see if we can determine it is infinite 00339 } 00340 else if (getSize) { 00341 thisSize = thisSize * size; 00342 // Give up if it gets too big 00343 if (thisSize > 1000000) thisSize = 0; 00344 if (thisSize == 0) { 00345 getSize = false; 00346 } 00347 } 00348 } 00349 00350 if (card == CARD_FINITE) { 00351 00352 if (enumerate) { 00353 // TODO: enumerate functions? maybe at least n == 0 00354 e = Expr(); 00355 } 00356 00357 if (computeSize) { 00358 n = thisSize; 00359 } 00360 00361 } 00362 00363 return card; 00364 } 00365 00366 00367 void TheoryUF::computeType(const Expr& e) 00368 { 00369 switch (e.getKind()) { 00370 case LAMBDA: { 00371 vector<Type> args; 00372 const vector<Expr>& vars = e.getVars(); 00373 DebugAssert(vars.size() > 0, 00374 "TheorySimulate::computeType("+e.toString()+")"); 00375 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end(); 00376 i!=iend; ++i) 00377 args.push_back((*i).getType()); 00378 e.setType(Type::funType(args, e.getBody().getType())); 00379 break; 00380 } 00381 case APPLY: { 00382 theoryOf(APPLY)->computeType(e); 00383 break; 00384 } 00385 case TRANS_CLOSURE: { 00386 DebugAssert(e.isSymbol(), "Expected symbol"); 00387 Expr funExpr = resolveID(e.getName()); 00388 if (funExpr.isNull()) { 00389 throw TypecheckException 00390 ("Attempt to take transitive closure of unknown id: " 00391 +e.getName()); 00392 } 00393 Type funType = funExpr.getType(); 00394 if(!funType.isFunction()) { 00395 throw TypecheckException 00396 ("Attempt to take transitive closure of non-function:\n\n" 00397 +funExpr.toString() + "\n\n which has type: " 00398 +funType.toString()); 00399 } 00400 if(funType.arity()!=3) { 00401 throw TypecheckException 00402 ("Attempt to take transitive closure of non-binary function:\n\n" 00403 +funExpr.toString() + "\n\n which has type: " 00404 +funType.toString()); 00405 } 00406 if (!funType[2].isBool()) { 00407 throw TypecheckException 00408 ("Attempt to take transitive closure of function:\n\n" 00409 +funExpr.toString() + "\n\n which does not return BOOLEAN"); 00410 } 00411 e.setType(funType); 00412 break; 00413 } 00414 default: 00415 DebugAssert(false,"Unexpected type: "+e.toString()); 00416 break; 00417 } 00418 } 00419 00420 00421 Type TheoryUF::computeBaseType(const Type& t) { 00422 const Expr& e = t.getExpr(); 00423 switch(e.getKind()) { 00424 case ARROW: { 00425 DebugAssert(e.arity() > 0, "Expected non-empty ARROW"); 00426 vector<Expr> kids; 00427 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 00428 kids.push_back(getBaseType(Type(*i)).getExpr()); 00429 } 00430 return Type(Expr(e.getOp(), kids)); 00431 } 00432 case TYPEDECL: return t; 00433 default: 00434 DebugAssert(false, 00435 "TheoryUF::computeBaseType("+t.toString()+")"); 00436 return t; 00437 } 00438 } 00439 00440 00441 void TheoryUF::computeModelTerm(const Expr& e, std::vector<Expr>& v) { 00442 for(CDList<Expr>::const_iterator i=d_funApplications.begin(), 00443 iend=d_funApplications.end(); i!=iend; ++i) { 00444 if((*i).isApply() && (*i).getOp().getExpr() == e) { 00445 // Add both the function application 00446 // getModelTerm(*i, v); 00447 v.push_back(*i); 00448 // and the arguments to the model terms. Reason: the argument 00449 // to the function better be a concrete value, and it might not 00450 // necessarily be in the current list of model terms. 00451 for(Expr::iterator j=(*i).begin(), jend=(*i).end(); j!=jend; ++j) 00452 // getModelTerm(*j, v); 00453 v.push_back(*j); 00454 } 00455 } 00456 } 00457 00458 00459 void TheoryUF::computeModel(const Expr& e, std::vector<Expr>& vars) { 00460 // Repeat the same search for applications of e as in 00461 // computeModelTerm(), but this time get the concrete values of the 00462 // arguments, and return the applications of e to concrete values in 00463 // vars. 00464 00465 // We'll assign 'e' a value later. 00466 vars.push_back(e); 00467 // Map of f(c) to val for concrete values of c and val 00468 ExprHashMap<Expr> appls; 00469 for(CDList<Expr>::const_iterator i=d_funApplications.begin(), 00470 iend=d_funApplications.end(); i!=iend; ++i) { 00471 if((*i).isApply() && (*i).getOp().getExpr() == e) { 00472 // Update all arguments with concrete values 00473 vector<Theorem> thms; 00474 vector<unsigned> changed; 00475 for(int j=0; j<(*i).arity(); ++j) { 00476 Theorem asst(getModelValue((*i)[j])); 00477 if(asst.getLHS()!=asst.getRHS()) { 00478 thms.push_back(asst); 00479 changed.push_back(j); 00480 } 00481 } 00482 Expr var; 00483 if(changed.size()>0) { 00484 // Arguments changed. Compute the new application, and assign 00485 // it a concrete value 00486 Theorem subst = substitutivityRule(*i, changed, thms); 00487 assignValue(transitivityRule(symmetryRule(subst), getModelValue(*i))); 00488 var = subst.getRHS(); 00489 } else 00490 var = *i; 00491 if(d_applicationsInModel) vars.push_back(var); 00492 // Record it in the map 00493 appls[var] = getModelValue(var).getRHS(); 00494 } 00495 } 00496 // Create a LAMBDA expression for e 00497 if(appls.size()==0) { // Leave it fully uninterpreted 00498 assignValue(reflexivityRule(e)); 00499 } else { 00500 // Bound vars 00501 vector<Expr> args; 00502 Type tp(e.getType()); 00503 static unsigned count(0); 00504 DebugAssert(tp.isFunction(), "TheoryUF::computeModel("+e.toString() 00505 +" : "+tp.toString()+")"); 00506 for(int i=0, iend=tp.arity()-1; i<iend; ++i) { 00507 string str = "uf_"+int2string(count); 00508 Expr v = getEM()->newBoundVarExpr(str, int2string(count++)); 00509 v.setType(tp[i]); 00510 args.push_back(v); 00511 } 00512 DebugAssert(args.size()>0, "TheoryUF::computeModel()"); 00513 ExprHashMap<Expr>::iterator i=appls.begin(), iend=appls.end(); 00514 DebugAssert(i!=iend, "TheoryUF::computeModel(): empty appls hash"); 00515 // Use one of the concrete values as a default 00516 Expr res((*i).second); ++i; 00517 for(; i!=iend; ++i) { 00518 // Optimization: if the current value is the same as that of the 00519 // next application, skip this case; i.e. keep 'res' instead of 00520 // building ite(cond, res, res). 00521 if((*i).second == res) continue; 00522 00523 // Create an ITE condition 00524 Expr cond; 00525 vector<Expr> eqs; 00526 for(int j=0, jend=args.size(); j<jend; ++j) 00527 eqs.push_back(args[j].eqExpr((*i).first[j])); 00528 if(eqs.size()==1) 00529 cond = eqs[0]; 00530 else 00531 cond = andExpr(eqs); 00532 // Create an ITE 00533 res = cond.iteExpr((*i).second, res); 00534 } 00535 res = lambdaExpr(args, res); 00536 assignValue(e, res); 00537 } 00538 } 00539 00540 00541 Expr TheoryUF::computeTCC(const Expr& e) 00542 { 00543 switch (e.getKind()) { 00544 case APPLY: { 00545 // Compute subtype predicates from the domain types applied to 00546 // the corresponding arguments. That is, if f: (T0,..,Tn)->T, 00547 // and e = f(e0,...,en), then the TCC is 00548 // 00549 // pred_T0(e0) & ... & pred_Tn(en) & TCC(e), 00550 // 00551 // where the last TCC(e) is the conjunction of TCCs for the 00552 // arguments, which ensures that all arguments are defined. 00553 // 00554 // If the operator is a lambda-expression, compute the TCC for 00555 // the beta-reduced expression. We do this in a somewhat sneaky 00556 // but an efficient way: first, compute TCC of the op.body 00557 // (which depends on the bound vars), then wrap that into 00558 // lambda, and apply it to the arguments: 00559 // 00560 // (LAMBDA(x0...xn): TCC(op.body)) (e0 ... en) 00561 // 00562 // The reason it is more efficient is that TCC(op.body) is cached, 00563 // and doesn't change with the arguments. 00564 00565 vector<Expr> preds; 00566 preds.push_back(Theory::computeTCC(e)); 00567 DebugAssert(e.isApply(), "Should be application"); 00568 Expr op(e.getOp().getExpr()); 00569 Type funType(op.getType()); 00570 DebugAssert(funType.isFunction() || funType.isBool(), 00571 "TheoryUF::computeTCC(): funType = " 00572 +funType.toString()); 00573 if(funType.isFunction()) { 00574 DebugAssert(funType.arity() == e.arity()+1, 00575 "TheoryUF::computeTCC(): funType = " 00576 +funType.toString()+"\n e = "+e.toString()); 00577 for(int i=0, iend=e.arity(); i<iend; ++i) { 00578 // Optimization: if the type of the formal argument is 00579 // exactly the same as the type of the actual, then skip the 00580 // type predicate for that argument 00581 if(funType[i] != e[i].getType()) 00582 preds.push_back(getTypePred(funType[i], e[i])); 00583 } 00584 } 00585 // Now strip off all the LETDECL 00586 while(op.getKind()==LETDECL) op = op[1]; 00587 // and add a TCC for the lambda-expression 00588 if(op.isLambda()) { 00589 preds.push_back(Expr(lambdaExpr(op.getVars(), 00590 getTCC(op.getBody())).mkOp(), 00591 e.getKids())); 00592 } 00593 return rewriteAnd(andExpr(preds)).getRHS(); 00594 } 00595 case LAMBDA: 00596 return trueExpr(); 00597 default: 00598 DebugAssert(false,"Unexpected type: "+e.toString()); 00599 return trueExpr(); 00600 } 00601 } 00602 00603 /////////////////////////////////////////////////////////////////////////////// 00604 // Pretty-printing // 00605 /////////////////////////////////////////////////////////////////////////////// 00606 00607 00608 ExprStream& TheoryUF::print(ExprStream& os, const Expr& e) { 00609 switch(os.lang()) { 00610 case SIMPLIFY_LANG: 00611 switch(e.getKind()) { 00612 case OLD_ARROW: 00613 case ARROW: 00614 os<<"ERROR:ARROW:unsupported in Simplify\n"; 00615 break; 00616 case LAMBDA: { 00617 os<<"ERROR:LAMBDA:unsupported in Simplify\n"; 00618 break; 00619 } 00620 case TRANS_CLOSURE: 00621 os<<"ERROR:TRANS_CLOSURE:unsupported in Simplify\n"; 00622 break; 00623 case TYPEDECL: 00624 os<<"ERROR:TYPEDECL:unsupported in Simplify\n"; 00625 break; 00626 case UFUNC: 00627 case APPLY: 00628 if(e.isApply()) os << "(" << e.getOp().getExpr()<<" "; 00629 if(e.arity() > 0) { 00630 bool first(true); 00631 for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 00632 if(first) first = false; 00633 else os << " " ; 00634 os << *i; 00635 } 00636 os << ")"; 00637 } 00638 break; 00639 default: { 00640 DebugAssert(false, "TheoryUF::print: Unexpected expression: " 00641 +getEM()->getKindName(e.getKind())); 00642 } 00643 } 00644 break; // end of case SIMPLIFY_LANGUAGE 00645 00646 case TPTP_LANG: 00647 switch(e.getKind()) { 00648 case OLD_ARROW: 00649 case ARROW: 00650 if(e.arity() < 2) e.printAST(os); 00651 else { 00652 os << "(" << push; 00653 bool first(true); 00654 for(int i=0, iend=e.arity()-1; i<iend; ++i) { 00655 if(first) first=false; 00656 else os << " * " ; 00657 os << e[i]; 00658 } 00659 os << ")" ; 00660 os << " > " << e[e.arity()-1]; 00661 } 00662 break; 00663 00664 case LAMBDA: { 00665 os<<"ERROR:LAMBDA:unsupported in TPTP\n"; 00666 break; 00667 } 00668 case TRANS_CLOSURE: 00669 os<<"ERROR:TRANS_CLOSURE:unsupported in TPTP\n"; 00670 break; 00671 case TYPEDECL: 00672 if(e.arity() != 1) e.printAST(os); 00673 else os << e[0].getString(); 00674 break; 00675 00676 case UFUNC: 00677 DebugAssert(e.isSymbol(), "Expected symbol"); 00678 os << to_lower(e.getName()); 00679 break; 00680 00681 case APPLY: 00682 if(e.isApply()) os <<e.getOpExpr()<<"("; 00683 if(e.arity() > 0) { 00684 bool first(true); 00685 for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 00686 if(first) first = false; 00687 else os << "," ; 00688 os << *i; 00689 } 00690 os << ")"; 00691 } 00692 break; 00693 default: { 00694 DebugAssert(false, "TheoryUF::print: Unexpected expression: " 00695 +getEM()->getKindName(e.getKind())); 00696 } 00697 } 00698 break; // end of case TPTP_LANGUAGE 00699 00700 00701 case PRESENTATION_LANG: 00702 switch(e.getKind()) { 00703 case OLD_ARROW: 00704 case ARROW: 00705 if(e.arity() < 2) e.printAST(os); 00706 else { 00707 if(e.arity() == 2) 00708 os << e[0]; 00709 else { 00710 os << "(" << push; 00711 bool first(true); 00712 for(int i=0, iend=e.arity()-1; i<iend; ++i) { 00713 if(first) first=false; 00714 else os << "," << space; 00715 os << e[i]; 00716 } 00717 os << push << ")" << pop << pop; 00718 } 00719 os << space << "->" << space << e[e.arity()-1]; 00720 } 00721 break; 00722 case TYPEDECL: 00723 // If it's straight from the parser, we may have several type 00724 // names in one declaration. Print these in LISP format. 00725 // Otherwise, print the name of the type. 00726 if(e.arity() != 1) e.printAST(os); 00727 else os << e[0].getString(); 00728 break; 00729 case LAMBDA: { 00730 DebugAssert(e.isLambda(), "Expected Lambda"); 00731 os << "(" << push << "LAMBDA" << space << push; 00732 const vector<Expr>& vars = e.getVars(); 00733 bool first(true); 00734 os << "(" << push; 00735 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end(); 00736 i!=iend; ++i) { 00737 if(first) first = false; 00738 else os << push << "," << pop << space; 00739 os << *i; 00740 // The lambda Expr may be in a raw parsed form, in which case 00741 // the type is not assigned yet 00742 if(i->isVar()) 00743 os << ":" << space << pushdag << (*i).getType() << popdag; 00744 } 00745 os << push << "): " << pushdag << push 00746 << e.getBody() << push << ")"; 00747 break; 00748 } 00749 case APPLY: 00750 os << e.getOpExpr(); 00751 if(e.arity() > 0) { 00752 os << "(" << push; 00753 bool first(true); 00754 for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 00755 if(first) first = false; 00756 else os << "," << space; 00757 os << *i; 00758 } 00759 os << push << ")"; 00760 } 00761 break; 00762 case TRANS_CLOSURE: 00763 DebugAssert(e.isSymbol(), "Expected symbol"); 00764 os << e.getName() << "*"; 00765 break; 00766 case UFUNC: 00767 DebugAssert(e.isSymbol(), "Expected symbol"); 00768 os << e.getName(); 00769 break; 00770 default: { 00771 DebugAssert(false, "TheoryUF::print: Unexpected expression: " 00772 +getEM()->getKindName(e.getKind())); 00773 } 00774 } 00775 break; // end of case PRESENTATION_LANGUAGE 00776 case SMTLIB_LANG: 00777 switch(e.getKind()) { 00778 case OLD_ARROW: 00779 case ARROW: { 00780 if(e.arity() < 2) { 00781 throw SmtlibException("TheoryUF::print: Expected 2 or more arguments to ARROW"); 00782 // e.print(os); 00783 } 00784 d_theoryUsed = true; 00785 os << push; 00786 bool oldDagFlag = os.dagFlag(false); 00787 int iend = e.arity(); 00788 if (e[iend-1].getKind() == BOOLEAN) --iend; 00789 for(int i=0; i<iend; ++i) { 00790 if (i != 0) os << space; 00791 os << e[i]; 00792 } 00793 os.dagFlag(oldDagFlag); 00794 break; 00795 } 00796 case TYPEDECL: 00797 if (e.arity() == 1 && e[0].isString()) { 00798 os << e[0].getString(); 00799 break; 00800 } 00801 // If it's straight from the parser, we may have several type 00802 // names in one declaration. Print these in LISP format. 00803 // Otherwise, print the name of the type. 00804 throw SmtlibException("TheoryUF::print: TYPEDECL not supported"); 00805 // if(e.arity() != 1) e.print(os); 00806 // else if(e[0].isString()) os << e[0].getString(); 00807 // else e[0].print(os); 00808 break; 00809 case APPLY: 00810 if (e.arity() == 0) os << e.getOp().getExpr(); 00811 else { 00812 os << "(" << push << e.getOp().getExpr(); 00813 for (int i=0, iend=e.arity(); i<iend; ++i) 00814 os << space << e[i]; 00815 if (e.getOpKind() == TRANS_CLOSURE) { 00816 os << space << ":transclose"; 00817 } 00818 os << push << ")"; 00819 } 00820 break; 00821 case TRANS_CLOSURE: 00822 os << e.getName(); 00823 break; 00824 case UFUNC: 00825 DebugAssert(e.isSymbol(), "Expected symbol"); 00826 os << theoryCore()->getTranslator()->fixConstName(e.getName()); 00827 break; 00828 default: { 00829 DebugAssert(false, "TheoryUF::print: SMTLIB_LANG: Unexpected expression: " 00830 +getEM()->getKindName(e.getKind())); 00831 } 00832 } 00833 break; // End of SMT_LIB 00834 case LISP_LANG: 00835 switch(e.getKind()) { 00836 case OLD_ARROW: 00837 case ARROW: 00838 if(e.arity() < 2) e.printAST(os); 00839 os << "(" << push << "ARROW"; 00840 for(int i=0, iend=e.arity(); i<iend; ++i) 00841 os << space << e[i]; 00842 os << push << ")"; 00843 break; 00844 case TRANS_CLOSURE: 00845 e.printAST(os); 00846 break; 00847 case TYPEDECL: 00848 // If it's straight from the parser, we may have several type 00849 // names in one declaration. Print these in LISP format. 00850 // Otherwise, print the name of the type. 00851 if(e.arity() != 1) e.printAST(os); 00852 else if(e[0].isString()) os << e[0].getString(); 00853 else e[0].print(os); 00854 break; 00855 case LAMBDA: { 00856 DebugAssert(e.isLambda(), "Expected LAMBDA"); 00857 os << "(" << push << "LAMBDA" << space; 00858 const vector<Expr>& vars = e.getVars(); 00859 bool first(true); 00860 os << "(" << push; 00861 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end(); 00862 i!=iend; ++i) { 00863 if(first) first = false; 00864 else os << space; 00865 os << "(" << push << *i; 00866 // The expression may be in a raw parsed form, in which case 00867 // the type is not assigned yet 00868 if(i->isVar()) 00869 os << space << pushdag << (*i).getType() << popdag; 00870 os << push << ")" << pop << pop; 00871 } 00872 os << push << ")" << pop << pop << pushdag 00873 << e.getBody() << push << ")"; 00874 break; 00875 } 00876 case APPLY: 00877 DebugAssert(e.isApply(), "Expected Apply"); 00878 if (e.arity() == 0) os << e.getOp().getExpr(); 00879 else { 00880 os << "(" << push << e.getOp().getExpr(); 00881 for (int i=0, iend=e.arity(); i<iend; ++i) 00882 os << space << e[i]; 00883 os << push << ")"; 00884 } 00885 break; 00886 default: { 00887 DebugAssert(false, "TheoryUF::print: Unexpected expression: " 00888 +getEM()->getKindName(e.getKind())); 00889 } 00890 } 00891 break; // End of LISP_LANG 00892 default: 00893 // Print the top node in the default format, continue with 00894 // pretty-printing for children. 00895 e.printAST(os); 00896 break; 00897 } 00898 return os; 00899 } 00900 00901 ////////////////////////////////////////////////////////////////////////////// 00902 //parseExprOp: 00903 //translating special Exprs to regular EXPR?? 00904 /////////////////////////////////////////////////////////////////////////////// 00905 Expr 00906 TheoryUF::parseExprOp(const Expr& e) { 00907 // If the expression is not a list, it must have been already 00908 // parsed, so just return it as is. 00909 if(RAW_LIST != e.getKind()) return e; 00910 00911 DebugAssert(e.arity() > 0, 00912 "TheoryUF::parseExprOp:\n e = "+e.toString()); 00913 00914 if (e[0].getKind() == RAW_LIST) { 00915 if(e.arity() < 2) 00916 throw ParserException("Bad function application: "+e.toString()); 00917 Expr::iterator i=e.begin(), iend=e.end(); 00918 Expr op(parseExpr(*i)); ++i; 00919 vector<Expr> args; 00920 for(; i!=iend; ++i) args.push_back(parseExpr(*i)); 00921 return Expr(op.mkOp(), args); 00922 } 00923 00924 DebugAssert(e[0].getKind() == ID || e[0][0].getKind() == ID, 00925 "Expected identifier"); 00926 int kind = e[0].getKind(); 00927 if (kind == ID) kind = getEM()->getKind(e[0][0].getString()); 00928 switch(kind) { 00929 case OLD_ARROW: { 00930 if (!theoryCore()->getFlags()["old-func-syntax"].getBool()) { 00931 throw ParserException("You seem to be using the old syntax for function types.\n" 00932 "Please convert to the new syntax or run with +old-func-syntax"); 00933 } 00934 DebugAssert(e.arity()==3,"Expected arity 3 in OLD_ARROW"); 00935 Expr arg = parseExpr(e[1]); 00936 vector<Expr> k; 00937 if (arg.getOpKind() == TUPLE_TYPE) { 00938 Expr::iterator i = arg.begin(), iend=arg.end(); 00939 for (; i != iend; ++i) { 00940 k.push_back(*i); 00941 } 00942 } 00943 else k.push_back(arg); 00944 k.push_back(parseExpr(e[2])); 00945 return Expr(ARROW, k); 00946 } 00947 case ARROW: 00948 case TYPEDECL: { 00949 vector<Expr> k; 00950 Expr::iterator i = e.begin(), iend=e.end(); 00951 // Skip first element of the vector of kids in 'e'. 00952 // The first element is the operator. 00953 ++i; 00954 // Parse the kids of e and push them into the vector 'k' 00955 for(; i!=iend; ++i) 00956 k.push_back(parseExpr(*i)); 00957 return Expr(kind, k, e.getEM()); 00958 break; 00959 } 00960 case TRANS_CLOSURE: { 00961 if(e.arity() != 4) 00962 throw ParserException("Wrong number of arguments to " 00963 "TRANS_CLOSURE expression\n" 00964 " (expected 3 arguments): "+e.toString()); 00965 const string& name = e[1][0].getString(); 00966 Expr funExpr = resolveID(name); 00967 if (funExpr.isNull()) 00968 throw ParserException("Attempt to take transitive closure of unknown " 00969 "predicate"+name); 00970 return transClosureExpr(name, parseExpr(e[2]), parseExpr(e[3])); 00971 } 00972 case LAMBDA: { // (LAMBDA ((v1 ... vn tp1) ...) body) 00973 if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0)) 00974 throw ParserException("Bad LAMBDA expression: "+e.toString()); 00975 // Iterate through the groups of bound variables 00976 vector<pair<string,Type> > vars; // temporary stack of bound variables 00977 for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) { 00978 if(i->getKind() != RAW_LIST || i->arity() < 2) 00979 throw ParserException("Bad variable declaration block in LAMBDA " 00980 "expression: "+i->toString()+ 00981 "\n e = "+e.toString()); 00982 // Iterate through individual bound vars in the group. The 00983 // last element is the type, which we have to rebuild and 00984 // parse, since it is used in the creation of bound variables. 00985 Type tp(parseExpr((*i)[i->arity()-1])); 00986 for(int j=0, jend=i->arity()-1; j<jend; ++j) { 00987 if((*i)[j].getKind() != ID) 00988 throw ParserException("Bad variable declaration in LAMBDA" 00989 " expression: "+(*i)[j].toString()+ 00990 "\n e = "+e.toString()); 00991 vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp)); 00992 } 00993 } 00994 // Create all the bound vars and save them in a vector 00995 vector<Expr> boundVars; 00996 for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end(); 00997 i!=iend; ++i) 00998 boundVars.push_back(addBoundVar(i->first, i->second)); 00999 // Rebuild the body 01000 Expr body(parseExpr(e[2])); 01001 // Build the resulting Expr as (LAMBDA (vars) body) 01002 return lambdaExpr(boundVars, body); 01003 break; 01004 } 01005 case RAW_LIST: // Lambda application 01006 default: { // Application of an uninterpreted function 01007 if(e.arity() < 2) 01008 throw ParserException("Bad function application: "+e.toString()); 01009 Expr::iterator i=e.begin(), iend=e.end(); 01010 Expr op(parseExpr(*i)); ++i; 01011 vector<Expr> args; 01012 for(; i!=iend; ++i) args.push_back(parseExpr(*i)); 01013 return Expr(op.mkOp(), args); 01014 } 01015 } 01016 return e; 01017 } 01018 01019 01020 Expr TheoryUF::lambdaExpr(const vector<Expr>& vars, const Expr& body) { 01021 return getEM()->newClosureExpr(LAMBDA, vars, body); 01022 } 01023 01024 01025 Expr TheoryUF::transClosureExpr(const std::string& name, const Expr& e1, 01026 const Expr& e2) { 01027 return Expr(getEM()->newSymbolExpr(name, TRANS_CLOSURE).mkOp(), e1, e2); 01028 }