theory_uf.cpp

Go to the documentation of this file.
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 // HACK: include theory_records.h to access the TUPLE_TYPE kind
00029 #include "theory_records.h"
00030 
00031 
00032 using namespace std;
00033 using namespace CVC3;
00034 
00035 
00036 ///////////////////////////////////////////////////////////////////////////////
00037 // TheoryUF Public Methods                                                   //
00038 ///////////////////////////////////////////////////////////////////////////////
00039 
00040 
00041 TheoryUF::TheoryUF(TheoryCore* core)//, bool useAckermann)
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     //    d_useAckermann(useAckermann)
00047 {
00048   d_rules = createProofRules();
00049 
00050   // Register new local kinds with ExprManager
00051   getEM()->newKind(TRANS_CLOSURE, "_TRANS_CLOSURE");
00052   getEM()->newKind(OLD_ARROW, "_OLD_ARROW", true);
00053 
00054   vector<int> kinds;
00055   //TODO: should this stuff really be in theory_uf?
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 //TODO: clean up transitive closure tables
00073 // be sure to free CD objects
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         // const Expr& rel = expr.getFun();
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         // Insert into transitive closure table
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         // Compute transitive closure with existing relations
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   // Check for any unexpanded lambdas
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         // Simplify recursively
00175         res = transitivityRule(res, simplify(res.getRHS()));
00176         IF_DEBUG(debugger.counter("Expanded lambdas")++);
00177         return res;
00178       }
00179       default: // A truly uninterpreted function
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 //   if (d_useAckermann) {
00195 //     Theorem thm = getCommonRules()->varIntroSkolem(e);
00196 //     theoryCore()->addToVarDB(thm.getRHS());
00197 //     enqueueFact(thm);
00198 //   }
00199 //   else {
00200     setupCC(e);
00201 //   }
00202   // Add this function application for concrete model generation
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   int k, ar(d.arity());
00212   const Theorem& dEQdsig = d.getSig();
00213   if (!dEQdsig.isNull()) {
00214     Expr dsig = dEQdsig.getRHS();
00215     Theorem thm = updateHelper(d);
00216     const Expr& sigNew = thm.getRHS();
00217     if (sigNew == dsig) return;
00218     dsig.setRep(Theorem());
00219     const Theorem& repEQsigNew = sigNew.getRep();
00220     if (!repEQsigNew.isNull()) {
00221       d.setSig(Theorem());
00222       enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
00223     }
00224     else {
00225       for (k = 0; k < ar; ++k) {
00226   if (sigNew[k] != dsig[k]) {
00227     sigNew[k].addToNotify(this, d);
00228   }
00229       }
00230       d.setSig(thm);
00231       sigNew.setRep(thm);
00232 
00233       if (d_compute_trans_closure && d.getKind() == APPLY &&
00234     d.arity() == 2 && findExpr(d).isTrue()) {
00235   thm = iffTrueElim(transitivityRule(symmetryRule(thm),find(d)));
00236   enqueueFact(d_rules->relToClosure(thm));
00237       }
00238 
00239     }
00240   }
00241   */
00242   // Record the original signature
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       //      TRACE_MSG("facts update", "updateCC["+getName()+"]() [no change] => }");
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       // Add both the function application
00398       // getModelTerm(*i, v);
00399       v.push_back(*i);
00400       // and the arguments to the model terms.  Reason: the argument
00401       // to the function better be a concrete value, and it might not
00402       // necessarily be in the current list of model terms.
00403       for(Expr::iterator j=(*i).begin(), jend=(*i).end(); j!=jend; ++j)
00404   // getModelTerm(*j, v);
00405   v.push_back(*j);
00406     }
00407   }
00408 }
00409 
00410 
00411 void TheoryUF::computeModel(const Expr& e, std::vector<Expr>& vars) {
00412   // Repeat the same search for applications of e as in
00413   // computeModelTerm(), but this time get the concrete values of the
00414   // arguments, and return the applications of e to concrete values in
00415   // vars.
00416 
00417   // We'll assign 'e' a value later.
00418   vars.push_back(e);
00419   // Map of f(c) to val for concrete values of c and val
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       // Update all arguments with concrete values
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   // Arguments changed.  Compute the new application, and assign
00437   // it a concrete value
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       // Record it in the map
00445       appls[var] = getModelValue(var).getRHS();
00446     }
00447   }
00448   // Create a LAMBDA expression for e
00449   if(appls.size()==0) { // Leave it fully uninterpreted
00450     assignValue(reflexivityRule(e));
00451   } else {
00452     // Bound vars
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     // Use one of the concrete values as a default
00467     Expr res((*i).second); ++i;
00468     for(; i!=iend; ++i) {
00469       // Optimization: if the current value is the same as that of the
00470       // next application, skip this case; i.e. keep 'res' instead of
00471       // building ite(cond, res, res).
00472       if((*i).second == res) continue;
00473 
00474       // Create an ITE condition
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       // Create an ITE
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       // Compute subtype predicates from the domain types applied to
00497       // the corresponding arguments.  That is, if f: (T0,..,Tn)->T,
00498       // and e = f(e0,...,en), then the TCC is
00499       //
00500       //   pred_T0(e0) & ... & pred_Tn(en) & TCC(e),
00501       //
00502       // where the last TCC(e) is the conjunction of TCCs for the
00503       // arguments, which ensures that all arguments are defined.
00504       //
00505       // If the operator is a lambda-expression, compute the TCC for
00506       // the beta-reduced expression.  We do this in a somewhat sneaky
00507       // but an efficient way: first, compute TCC of the op.body
00508       // (which depends on the bound vars), then wrap that into
00509       // lambda, and apply it to the arguments:
00510       //
00511       //   (LAMBDA(x0...xn): TCC(op.body)) (e0 ... en)
00512       //
00513       // The reason it is more efficient is that TCC(op.body) is cached,
00514       // and doesn't change with the arguments.
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     // Optimization: if the type of the formal argument is
00530     // exactly the same as the type of the actual, then skip the
00531     // type predicate for that argument
00532     if(funType[i] != e[i].getType())
00533       preds.push_back(getTypePred(funType[i], e[i]));
00534   }
00535       }
00536       // Now strip off all the LETDECL
00537       while(op.getKind()==LETDECL) op = op[1];
00538       // and add a TCC for the lambda-expression
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 // Pretty-printing                                           //
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; // end of case SIMPLIFY_LANGUAGE
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       // If it's straight from the parser, we may have several type
00620       // names in one declaration.  Print these in LISP format.
00621       // Otherwise, print the name of the type.
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         // The lambda Expr may be in a raw parsed form, in which case
00637         // the type is not assigned yet
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; // end of case PRESENTATION_LANGUAGE
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         //        e.print(os);
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       // If it's straight from the parser, we may have several type
00696       // names in one declaration.  Print these in LISP format.
00697       // Otherwise, print the name of the type.
00698       throw SmtlibException("TheoryUF::print: TYPEDECL not supported");
00699 //       if(e.arity() != 1) e.print(os);
00700 //       else if(e[0].isString()) os << e[0].getString();
00701 //       else e[0].print(os);
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; // End of SMT_LIB
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       // If it's straight from the parser, we may have several type
00743       // names in one declaration.  Print these in LISP format.
00744       // Otherwise, print the name of the type.
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         // The expression may be in a raw parsed form, in which case
00761         // the type is not assigned yet
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; // End of LISP_LANG
00786   default:
00787     // Print the top node in the default format, continue with
00788     // pretty-printing for children.
00789     e.printAST(os);
00790     break;
00791   }
00792   return os;
00793 }
00794 
00795 //////////////////////////////////////////////////////////////////////////////
00796 //parseExprOp:
00797 //translating special Exprs to regular EXPR??
00798 ///////////////////////////////////////////////////////////////////////////////
00799 Expr
00800 TheoryUF::parseExprOp(const Expr& e) {
00801   // If the expression is not a list, it must have been already
00802   // parsed, so just return it as is.
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     // Skip first element of the vector of kids in 'e'.
00834     // The first element is the operator.
00835     ++i; 
00836     // Parse the kids of e and push them into the vector 'k'
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: { // (LAMBDA ((v1 ... vn tp1) ...) body)
00855     if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0))
00856       throw ParserException("Bad LAMBDA expression: "+e.toString());
00857     // Iterate through the groups of bound variables
00858     vector<pair<string,Type> > vars; // temporary stack of bound variables
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       // Iterate through individual bound vars in the group.  The
00865       // last element is the type, which we have to rebuild and
00866       // parse, since it is used in the creation of bound variables.
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     // Create all the bound vars and save them in a vector
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     // Rebuild the body
00882     Expr body(parseExpr(e[2]));
00883     // Build the resulting Expr as (LAMBDA (vars) body)
00884     return lambdaExpr(boundVars, body);
00885     break;
00886   }
00887     // case APPLY: 
00888   default: { // Application of an uninterpreted function
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 }

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1