theory_records.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_records.cpp
00004  * 
00005  * Author: Daniel Wichs
00006  * 
00007  * Created: 7/21/03
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 #include "theory_records.h"
00021 #include "typecheck_exception.h"
00022 #include "parser_exception.h"
00023 #include "smtlib_exception.h"
00024 #include "records_proof_rules.h"
00025 
00026 
00027 using namespace std;
00028 using namespace CVC3;
00029 
00030 /*!
00031  * When a record/tuple (dis)equality is expanded into the
00032  * (dis)equalities of fields, we have to perform rewrites on the
00033  * resulting record terms before the simplifier kicks in.  
00034  *
00035  * Otherwise, if we have r1.f = r2.f, but r1=r2 was asserted before,
00036  * for some complex record expressions r1 and r2, then the simplifier
00037  * will substitute r2 for r1, and we get r2.f=r2.f at the end, which
00038  * is not a useful fact to have.
00039  *
00040  * However, r1.f and/or r2.f may rewrite to something interesting, and
00041  * the equality may yield new important facts.
00042  */
00043 Theorem 
00044 TheoryRecords::rewriteAux(const Expr& e) {
00045   Theorem res;
00046   switch(e.getKind()) {
00047   case EQ:
00048   case IFF:
00049   case AND:
00050   case OR: {
00051     vector<unsigned> changed;
00052     vector<Theorem> thms;
00053     for(int i=0, iend=e.arity(); i<iend; ++i) {
00054       Theorem t(rewriteAux(e[i]));
00055       if(t.getLHS() != t.getRHS()) {
00056   changed.push_back(i);
00057   thms.push_back(t);
00058       }
00059     }
00060     if(thms.size() > 0) {
00061       res = substitutivityRule(e, changed, thms);
00062       // Need to guarantee that new expressions are fully simplified
00063       if(res.getRHS().hasFind())
00064   res = transitivityRule(res, res.getRHS().getFind());
00065     } else
00066       res = reflexivityRule(e);
00067     break;
00068   }
00069   case NOT: {
00070     vector<Theorem> thms;
00071     thms.push_back(rewriteAux(e[0]));
00072     if(thms[0].getLHS() != thms[0].getRHS()) {
00073       res = substitutivityRule(NOT, thms);
00074       // Need to guarantee that new expressions are fully simplified
00075       if(res.getRHS().hasFind())
00076   res = transitivityRule(res, res.getRHS().getFind());
00077     } else
00078       res = reflexivityRule(e);
00079     break;
00080   }
00081   default:
00082     res = rewrite(e);
00083     break;
00084   }
00085   return res;
00086 }
00087 
00088 
00089 Theorem 
00090 TheoryRecords::rewriteAux(const Theorem& thm) {
00091   return iffMP(thm, rewriteAux(thm.getExpr()));
00092 }
00093 
00094 
00095 TheoryRecords::TheoryRecords(TheoryCore* core)
00096   : Theory(core, "Records")
00097 {
00098 
00099   getEM()->newKind(RECORD_TYPE, "_RECORD_TYPE", true);
00100   getEM()->newKind(TUPLE_TYPE, "_TUPLE_TYPE", true);
00101 
00102   getEM()->newKind(RECORD, "_RECORD");
00103   getEM()->newKind(RECORD_SELECT, "_RECORD_SELECT");
00104   getEM()->newKind(RECORD_UPDATE, "_RECORD_UPDATE");
00105   getEM()->newKind(TUPLE, "_TUPLE");
00106   getEM()->newKind(TUPLE_SELECT, "_TUPLE_SELECT");
00107   getEM()->newKind(TUPLE_UPDATE, "_TUPLE_UPDATE");
00108 
00109   d_rules = createProofRules();
00110   vector<int> kinds;
00111 
00112   kinds.push_back(RECORD);
00113   kinds.push_back(RECORD_SELECT);
00114   kinds.push_back(RECORD_UPDATE);
00115   kinds.push_back(RECORD_TYPE);
00116   kinds.push_back(TUPLE_TYPE);
00117   kinds.push_back(TUPLE);
00118   kinds.push_back(TUPLE_SELECT);
00119   kinds.push_back(TUPLE_UPDATE);
00120 
00121   registerTheory(this, kinds);
00122 }
00123 
00124 TheoryRecords::~TheoryRecords() {
00125   delete d_rules;
00126 }
00127 
00128 void TheoryRecords::assertFact(const Theorem& e)
00129 {
00130   //  TRACE("records", "assertFact => ", e.toString(), "");
00131   const Expr& expr = e.getExpr();
00132   Theorem expanded;
00133   switch(expr.getKind()) {
00134   case IFF:
00135   case EQ: {
00136     int lhsKind = getBaseType(expr[0]).getExpr().getOpKind();
00137     if(lhsKind == RECORD_TYPE || lhsKind== TUPLE_TYPE)
00138       {
00139   expanded = rewriteAux(d_rules->expandEq(e));
00140   TRACE("records", "assertFact: enqueuing: ", expanded.toString(), "");
00141   enqueueFact(expanded);
00142       }
00143     return;
00144   }
00145   case NOT:
00146     DebugAssert(expr[0].getKind() == EQ || expr[0].getKind() == IFF,
00147                 "expecting a disequality or boolean field extraction: "
00148                 +expr.toString());
00149     break;
00150   default:
00151     DebugAssert(false, "TheoryRecords::assertFact expected an equation"
00152     " or negation of equation expression. Instead it got"
00153     + e.toString());
00154     
00155   }
00156       
00157 }
00158 
00159 
00160 Theorem TheoryRecords::rewrite(const Expr& e) {
00161   Theorem rw;
00162   TRACE("records", "rewrite(", e, ") {");
00163   bool needRecursion=false;
00164   switch(e.getOpKind()) {
00165   case TUPLE_SELECT:
00166   case RECORD_SELECT: {
00167     switch(e[0].getOpKind()){
00168     case RECORD:{
00169       rw = d_rules->rewriteLitSelect(e);
00170       break;
00171     }
00172     case TUPLE: {
00173       rw =   d_rules->rewriteLitSelect(e);
00174       break;
00175     }
00176     case RECORD_UPDATE: {
00177       rw = d_rules->rewriteUpdateSelect(e);
00178       needRecursion=true;
00179       break;
00180     }
00181     case TUPLE_UPDATE: {
00182       rw = d_rules->rewriteUpdateSelect(e);
00183       needRecursion=true;
00184       break;
00185     }
00186     default:{
00187       rw =  reflexivityRule(e);
00188       break;
00189     }
00190     }
00191     break;
00192   } 
00193   case RECORD_UPDATE: {
00194     DebugAssert(e.arity() == 2, 
00195     "TheoryRecords::rewrite(RECORD_UPDATE): e="+e.toString());
00196     if(e[0].getOpKind() == RECORD)
00197       rw= d_rules->rewriteLitUpdate(e);
00198     else
00199       rw =  reflexivityRule(e);
00200     break;
00201   }
00202   case TUPLE_UPDATE: {
00203     if(e[0].getOpKind() == TUPLE)
00204       rw = d_rules->rewriteLitUpdate(e);
00205     else
00206       rw =  reflexivityRule(e);
00207     break;
00208   }
00209   case RECORD:
00210   case TUPLE:
00211     rw = rewriteCC(e); // Congruence closure rewrites
00212     break;
00213   default: {
00214     rw = reflexivityRule(e);
00215     break;
00216   }   
00217   }
00218   Theorem res;
00219   if(needRecursion==true) res = transitivityRule(rw, rewrite(rw.getRHS()));
00220   else
00221     res = rw;
00222   TRACE("records", "rewrite => ", res.getRHS(), " }");
00223   return res;
00224 }
00225 
00226 
00227 Expr TheoryRecords::computeTCC(const Expr& e)
00228 {
00229   TRACE("records", "computeTCC( ", e, ")   {");
00230   Expr tcc(Theory::computeTCC(e));
00231   switch (e.getOpKind()) {
00232   case RECORD:
00233   case RECORD_SELECT:
00234   case TUPLE:
00235   case TUPLE_SELECT:
00236     break;
00237   case RECORD_UPDATE: {
00238     Expr tExpr = e.getType().getExpr();
00239     const std::string field(getField(e));
00240     int index = getFieldIndex(tExpr, field);
00241     Expr pred = getTypePred(e.getType()[index], e[1]);
00242     tcc = rewriteAnd(tcc.andExpr(pred)).getRHS();
00243     break;
00244   }
00245   case TUPLE_UPDATE: {
00246     Expr tExpr = e.getType().getExpr();
00247     int index = getIndex(e);
00248     Expr pred = getTypePred(e.getType()[index], e[1]);
00249     tcc = rewriteAnd(tcc.andExpr(pred)).getRHS();
00250     break;
00251   }
00252   default: {
00253     DebugAssert (false, "Theory records cannot calculate this tcc");
00254   }
00255   }
00256   TRACE("records", "computeTCC => ", tcc, "}");
00257   return tcc;
00258 }
00259 
00260 void TheoryRecords::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
00261   Type t = e.getType();
00262   Expr tExpr  = t.getExpr();
00263   if(tExpr.getOpKind() == RECORD_TYPE) {
00264     const vector<Expr>& fields = getFields(tExpr);
00265     for(unsigned int i = 0; i < fields.size() ; i++) {
00266       Expr term(recordSelect(e, fields[i].getString()));
00267       term = rewrite(term).getRHS();
00268       v.push_back(term);
00269     }
00270   }
00271   else if(tExpr.getOpKind() == TUPLE_TYPE) {
00272     for(int i=0; i<tExpr.arity(); i++) {
00273       Expr term(tupleSelect(e, i));
00274       term = rewrite(term).getRHS();
00275       v.push_back(term);
00276     }
00277   }
00278 }
00279 
00280 void TheoryRecords::computeModel(const Expr& e, std::vector<Expr>& v) {
00281   Type t = getBaseType(e);
00282   Expr tExpr  = t.getExpr();
00283   vector<Theorem> thms;
00284   vector<unsigned> changed;
00285   Theorem asst;
00286   if(tExpr.getOpKind() == RECORD_TYPE)
00287     asst = d_rules->expandRecord(e);
00288   else if(tExpr.getOpKind() == TUPLE_TYPE)
00289     asst = d_rules->expandTuple(e);
00290   else {
00291     DebugAssert(false, "TheoryRecords::computeModel("+e.toString()+")");
00292     return;
00293   }
00294 
00295   const Expr& lit = asst.getRHS();
00296   int size(lit.arity());
00297   for(int i = 0; i < size ; i++) {
00298     Theorem thm(getModelValue(lit[i]));
00299     if(thm.getLHS() != thm.getRHS()) {
00300       thms.push_back(thm);
00301       changed.push_back(i);
00302     }
00303   }
00304   if(changed.size()>0)
00305     asst = transitivityRule(asst, substitutivityRule(lit, changed, thms));
00306   assignValue(asst);
00307   v.push_back(e);
00308 }
00309 
00310 
00311 Expr TheoryRecords::computeTypePred(const Type& t, const Expr& e)
00312 {
00313   TRACE("typePred", "ComputeTypePred[Records]", e, "");
00314   Expr tExpr = t.getExpr();
00315   switch(tExpr.getOpKind()) {
00316   case RECORD_TYPE: {
00317     const vector<Expr>& fields = getFields(tExpr);
00318     vector<Expr> fieldPreds;
00319     for(unsigned int i = 0; i<fields.size(); i++) {
00320       Expr sel(recordSelect(e, fields[i].getString()));
00321       fieldPreds.push_back(getTypePred(tExpr[i], sel));
00322     }
00323       Expr pred = andExpr(fieldPreds);
00324       TRACE("typePred", "Computed predicate ", pred, "");
00325       return pred;
00326   }
00327   case TUPLE_TYPE: {
00328     std::vector<Expr> fieldPreds;
00329     for(int i = 0; i<tExpr.arity(); i++) {
00330       fieldPreds.push_back(getTypePred(tExpr[i], tupleSelect(e, i)));
00331     }
00332     Expr pred = andExpr(fieldPreds);
00333     TRACE("typePred", "Computed predicate ", pred, "");
00334     return pred;    
00335   }
00336   default:
00337    DebugAssert(false, "computeTypePred[TheoryRecords] called with wrong type");
00338    return Expr();
00339   }
00340 }
00341 
00342 
00343 void TheoryRecords::checkType(const Expr& e)
00344 {
00345   switch (e.getOpKind()) {
00346     case RECORD_TYPE: {
00347       Expr::iterator i = e.begin(), iend = e.end();
00348       for (; i != iend; ) {
00349         Type t(*i);
00350         ++i;
00351         if (t.isBool()) throw Exception
00352             ("Records cannot contain BOOLEANs: "
00353              +e.toString());
00354         if (t.isFunction()) throw Exception
00355             ("Records cannot contain functions");
00356       }
00357       break;
00358     }
00359     case TUPLE_TYPE: {
00360       Expr::iterator i = e.begin(), iend = e.end();
00361       for (; i != iend; ) {
00362         Type t(*i);
00363         ++i;
00364         if (t.isBool()) throw Exception
00365             ("Tuples cannot contain BOOLEANs: "
00366              +e.toString());
00367         if (t.isFunction()) throw Exception
00368             ("Tuples cannot contain functions");
00369       }
00370       break;
00371     }
00372     default:
00373       DebugAssert(false, "Unexpected kind in TheoryRecords::checkType"
00374                   +getEM()->getKindName(e.getOpKind()));
00375   }
00376 }
00377 
00378 
00379 void TheoryRecords::computeType(const Expr& e)
00380 {
00381   switch (e.getOpKind()) {
00382   case RECORD:{
00383     DebugAssert(e.arity() > 0, "wrong arity of RECORD" + e.toString());
00384     vector<Expr> fieldTypes;
00385     const vector<Expr>& fields = getFields(e);
00386     string previous;
00387     DebugAssert((unsigned int)e.arity() == fields.size(),
00388     "size of fields does not match size of values");
00389     for(int i = 0; i<e.arity(); ++i) {
00390       DebugAssert(fields[i].getString() != previous, 
00391       "a record cannot not contain repeated fields"
00392       + e.toString());
00393       fieldTypes.push_back(e[i].getType().getExpr());
00394       previous=fields[i].getString();
00395     }
00396     e.setType(Type(recordType(fields, fieldTypes)));
00397     return;
00398   }
00399   case RECORD_SELECT: {
00400     DebugAssert(e.arity() == 1, "wrong arity of RECORD_SELECT" + e.toString());
00401     Expr t = e[0].getType().getExpr();
00402     const string& field = getField(e);
00403     DebugAssert(t.getOpKind() == RECORD_TYPE, "incorrect RECORD_SELECT expression"
00404     "first child not a RECORD_TYPE" + e.toString());
00405     int index = getFieldIndex(t, field);
00406     if(index==-1)
00407       throw TypecheckException("record selection does not match any field "
00408              "in record" + e.toString());
00409     e.setType(Type(t[index]));
00410     return;
00411   }
00412   case RECORD_UPDATE: {
00413     DebugAssert(e.arity() == 2, "wrong arity of RECORD_UPDATE" + e.toString());
00414     Expr t = e[0].getType().getExpr();
00415     const string& field = getField(e);
00416     DebugAssert(t.getOpKind() == RECORD_TYPE, "incorrect RECORD_SELECT expression"
00417     "first child not a RECORD_TYPE" + e.toString());
00418     int index = getFieldIndex(t, field);
00419     if(index==-1)
00420       throw TypecheckException
00421   ("record update field \""+field
00422    +"\" does not match any in record type:\n"
00423    +t.toString()+"\n\nThe complete expression is:\n\n"
00424    + e.toString());
00425     if(getBaseType(Type(t[index])) != getBaseType(e[1]))
00426       throw TypecheckException("Type checking error: \n"+ e.toString());
00427     e.setType(e[0].getType());
00428     return;
00429   }
00430   case TUPLE: {
00431     DebugAssert(e.arity() > 0, "wrong arity of TUPLE"+ e.toString());
00432     std::vector<Expr> types;
00433     for(Expr::iterator it = e.begin(), end=e.end(); it!=end; ++it)
00434       {
00435   types.push_back((*it).getType().getExpr());
00436       }
00437     e.setType(Type(Expr(TUPLE_TYPE, types, getEM())));
00438     return;
00439   }
00440   case TUPLE_SELECT: {
00441     DebugAssert(e.arity() == 1, "wrong arity of TUPLE_SELECT" + e.toString());
00442     Expr t = e[0].getType().getExpr();
00443     int index = getIndex(e);
00444     DebugAssert(t.getOpKind() == TUPLE_TYPE,
00445     "incorrect TUPLE_SELECT expression: "
00446     "first child is not a TUPLE_TYPE:\n\n" + e.toString());
00447     if(index >= t.arity())
00448       throw TypecheckException("tuple index exceeds number of fields: \n"
00449              + e.toString());
00450     e.setType(Type(t[index]));
00451     return;
00452   }
00453   case TUPLE_UPDATE: {
00454     DebugAssert(e.arity() == 2, "wrong arity of TUPLE_UPDATE" + e.toString());
00455     Expr t = e[0].getType().getExpr();
00456     int index = getIndex(e);
00457     DebugAssert(t.getOpKind() == TUPLE_TYPE, "incorrect TUPLE_SELECT expression: "
00458     "first child not a TUPLE_TYPE:\n\n" + e.toString());
00459     if(index >= t.arity())
00460       throw TypecheckException("tuple index exceeds number of fields: \n"
00461              + e.toString());
00462     if(getBaseType(Type(t[index])) != getBaseType(e[1]))
00463       throw TypecheckException("tuple update type mismatch: \n"+ e.toString());
00464     e.setType(e[0].getType());
00465     return;
00466   }
00467   default:
00468     DebugAssert(false,"Unexpected type: "+e.toString());
00469     break;
00470   }
00471 }
00472 
00473 
00474 Type
00475 TheoryRecords::computeBaseType(const Type& t) {
00476   const Expr& e = t.getExpr();
00477   Type res;
00478   switch(e.getOpKind()) {
00479   case TUPLE_TYPE:
00480   case RECORD_TYPE: {
00481     DebugAssert(e.arity() > 0, "Expected non-empty type");
00482     vector<Expr> kids;
00483     for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
00484       kids.push_back(getBaseType(Type(*i)).getExpr());
00485     }
00486     res = Type(Expr(e.getOp(), kids));
00487     break;
00488   }
00489   default:
00490     DebugAssert(false,
00491     "TheoryRecords::computeBaseType("+t.toString()+")");
00492     res = t;
00493   }
00494   return res;
00495 }
00496 
00497 
00498 void
00499 TheoryRecords::setup(const Expr& e) {
00500   // Only set up terms
00501   if (e.isTerm()) {
00502     switch(e.getOpKind()) {
00503     case RECORD:
00504     case TUPLE: // Setup for congruence closure
00505       setupCC(e);
00506       break;
00507     default: { // Everything else
00508       for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
00509   i->addToNotify(this, e);
00510       // Check if we have a tuple of record type, and set up those for CC
00511       Type tp(getBaseType(e));
00512       Theorem thm;
00513       if(isRecordType(tp)) // Expand e into its literal, and it setup for CC
00514   thm = d_rules->expandRecord(e);
00515       else if(isTupleType(tp))
00516   thm = d_rules->expandTuple(e);
00517       if(!thm.isNull()) {
00518   Expr lit(thm.getRHS());
00519   TRACE("records", "setup: lit = ", lit, "");
00520   // Simplify the kids
00521   vector<Theorem> thms;
00522   vector<unsigned> changed;
00523   for(int i=0,iend=lit.arity(); i<iend; ++i) {
00524     TRACE("records", "setup: rewriting lit["+int2string(i)+"] = ",
00525     lit[i], "");
00526     Theorem t = rewrite(lit[i]);
00527     t = transitivityRule(t, find(t.getRHS()));
00528     if(lit[i] != t.getRHS()) {
00529       thms.push_back(t);
00530       changed.push_back(i);
00531     }
00532   }
00533   if(changed.size()>0) {
00534     thm = transitivityRule(thm, substitutivityRule(lit, changed, thms));
00535     lit = thm.getRHS();
00536   }
00537   // Check if lit has already been setup
00538   if(lit.hasFind()) {
00539     enqueueFact(transitivityRule(thm, find(lit)));
00540   } else {
00541     setup(lit);
00542     lit.setFind(symmetryRule(thm));
00543   }
00544       }
00545     }
00546     }
00547   }
00548 }
00549  
00550 
00551 void
00552 TheoryRecords::update(const Theorem& e, const Expr& d) {
00553   if (inconsistent()) return;
00554   DebugAssert(d.hasFind(), "Expected d to have find");
00555 
00556   switch(d.getOpKind()) {
00557   case RECORD:
00558   case TUPLE:
00559     // Record and tuple literals are handled by congruence closure updates
00560     updateCC(e, d);
00561     break;
00562   default: // Everything else
00563     // If d is not its own representative, don't do anything; the
00564     // representative will be sent to us eventually.
00565     if (find(d).getRHS() == d) {
00566       // Substitute e[1] for e[0] in d and assert the result equal to d
00567       Theorem thm = updateHelper(d);
00568       thm = transitivityRule(thm, rewrite(thm.getRHS()));
00569       assertEqualities(transitivityRule(thm, find(thm.getRHS())));
00570     }
00571   }
00572 }
00573 
00574 
00575 ExprStream& TheoryRecords::print(ExprStream& os, const Expr& e)
00576 {
00577    switch(os.lang()) {
00578    case PRESENTATION_LANG: {
00579      switch(e.getOpKind()){
00580      case TUPLE:{
00581        int i=0, iend=e.arity();
00582        os << "(" << push;
00583        if(i!=iend) os << e[i];
00584        ++i;
00585        for(; i!=iend; ++i) os << push << "," << pop << space << e[i];
00586        os << push << ")";
00587        break;
00588      }
00589      case TUPLE_TYPE: {
00590        int i=0, iend=e.arity();
00591        os << "[" << push;
00592        if(i!=iend) os << e[i];
00593        ++i;
00594        for(; i!=iend; ++i) os << push << "," << pop << space << e[i];
00595        os << push << "]";
00596        break;
00597      }
00598      case RECORD: {
00599        size_t i=0, iend=e.arity();
00600        if(!isRecord(e)) {
00601    e.printAST(os);
00602    break;
00603        }
00604        const vector<Expr>& fields = getFields(e);
00605        if(iend != fields.size()) {
00606    e.printAST(os); 
00607    break;
00608        }
00609        os << "(# " << push;
00610        if(i!=iend) {
00611    os <<  fields[i] << space 
00612       << ":="<< space << push << e[i] << pop;
00613    ++i;
00614        }
00615        for(; i!=iend; ++i)
00616    os << push << "," << pop << space <<  fields[i] 
00617       << space 
00618       << ":="<< space << push << e[i] << pop;
00619        os << push << space << "#)";
00620        break;
00621      }
00622      case RECORD_TYPE: {
00623        size_t i=0, iend=e.arity();
00624        if(!isRecordType(e)) {
00625    e.printAST(os);
00626    break;
00627        }
00628        const vector<Expr>& fields = getFields(e);
00629        if(iend != fields.size()) {
00630    e.printAST(os); 
00631    break;
00632        }
00633        os << "[# " << push;
00634        if(i!=iend) {
00635    os <<  fields[i] << ":"<< space << push << e[i] << pop;
00636    ++i;
00637        }
00638        for(; i!=iend; ++i)
00639    os << push << "," << pop << space <<  fields[i] 
00640       << ":"<< space << push << e[i] << pop;
00641        os << push << space << "#]";
00642        break;
00643      }
00644      case RECORD_SELECT:
00645        if(isRecordAccess(e) && e.arity() == 1)
00646    os << "(" << push <<  e[0] << push << ")" << "." << push 
00647       << getField(e);
00648        else
00649    e.printAST(os);
00650        break;
00651      case TUPLE_SELECT:
00652        if(isTupleAccess(e) && e.arity() == 1)
00653    os << "(" << push << e[0]  << push << ")" <<   "." << push 
00654       << getIndex(e);
00655        else
00656    e.printAST(os);
00657        break;
00658      case RECORD_UPDATE:
00659        if(isRecordAccess(e) && e.arity() == 2)
00660    os << "(" << push <<  e[0] << space << "WITH ."
00661       << push << getField(e)
00662       << space << ":=" << space << push << e[1] << push << ")";
00663        else
00664    e.printAST(os);
00665        break;
00666      case TUPLE_UPDATE:
00667        if(isTupleAccess(e) && e.arity() == 2)
00668    os << "(" << push <<  e[0] << space << "WITH ."
00669       << push << getIndex(e) 
00670       << space << ":=" << space << push << e[1] << push << ")";
00671        else
00672    e.printAST(os);
00673        break;
00674      default:
00675        e.printAST(os);
00676        break;
00677      }
00678      break;
00679    }
00680    case SMTLIB_LANG: {
00681      d_theoryUsed = true;
00682      throw SmtlibException("TheoryRecords::print: SMTLIB not supported");
00683      switch(e.getOpKind()){
00684      case TUPLE:{
00685        int i=0, iend=e.arity();
00686        os << "(" << push << "TUPLE";
00687        for(; i<iend; ++i) os << space << e[i];
00688        os << push << ")";
00689        break;
00690      }
00691      case TUPLE_TYPE: { // FIXME: change to TUPLE_TYPE
00692        int i=0, iend=e.arity();
00693        os << "(" << push << "TUPLE_TYPE";
00694        for(; i!=iend; ++i) os << space << e[i];
00695        os << push << ")";
00696        break;
00697      }
00698      case RECORD: {
00699        size_t i=0, iend=e.arity();
00700        if(!isRecord(e)) {
00701    e.printAST(os);
00702    break;
00703        }
00704        const vector<Expr>& fields = getFields(e);
00705        if(iend != fields.size()) {
00706    e.printAST(os); 
00707    break;
00708        }
00709        os << "(" << push << "RECORD";
00710        for(; i!=iend; ++i)
00711    os <<  space << "(" << push << fields[i] << space 
00712       << e[i] << push << ")" << pop << pop;
00713        os << push << ")";
00714        break;
00715      }
00716      case RECORD_TYPE: {
00717        size_t i=0, iend=e.arity();
00718        if(!isRecord(e)) {
00719    e.printAST(os);
00720    break;
00721        }
00722        const vector<Expr>& fields = getFields(e);
00723        if(iend != fields.size()) {
00724    e.printAST(os); 
00725    break;
00726        }
00727        os << "(" << push << "RECORD_TYPE";
00728        for(; i!=iend; ++i)
00729    os << space << "(" << push <<  fields[i] 
00730       << space << e[i] << push << ")" << pop << pop;
00731        os << push << space << ")";
00732        break;
00733      }
00734      case RECORD_SELECT:
00735        if(isRecordAccess(e))
00736    os << "(" << push << "RECORD_SELECT" << space 
00737       << e[0] << space << getField(e) << push << ")";
00738        else
00739    e.printAST(os);
00740        break;
00741      case TUPLE_SELECT:
00742        if(isTupleAccess(e))
00743    os << "(" << push << "TUPLE_SELECT" << space
00744       << e[0] << space << getIndex(e) << push << ")";
00745        else
00746    e.printAST(os);
00747        break;
00748      case RECORD_UPDATE:
00749        if(isRecordAccess(e) && e.arity() == 2)
00750    os << "(" << push << "RECORD_UPDATE" << space
00751       << e[0] << space << getField(e) 
00752       << space << e[1] << push << ")";
00753        else
00754    e.printAST(os);
00755        break;
00756      case TUPLE_UPDATE:
00757        if(isTupleAccess(e))
00758    os << "(" << push << "TUPLE_UPDATE" << space << e[0]
00759       << space << getIndex(e) 
00760       << space << e[1] << push << ")";
00761        else
00762    e.printAST(os);
00763        break;
00764      default:
00765        e.printAST(os);
00766        break;
00767      }
00768      break;
00769    }
00770    case LISP_LANG: {
00771      switch(e.getOpKind()){
00772      case TUPLE:{
00773        int i=0, iend=e.arity();
00774        os << "(" << push << "TUPLE";
00775        for(; i<iend; ++i) os << space << e[i];
00776        os << push << ")";
00777        break;
00778      }
00779      case TUPLE_TYPE: { // FIXME: change to TUPLE_TYPE
00780        int i=0, iend=e.arity();
00781        os << "(" << push << "TUPLE_TYPE";
00782        for(; i!=iend; ++i) os << space << e[i];
00783        os << push << ")";
00784        break;
00785      }
00786      case RECORD: {
00787        size_t i=0, iend=e.arity();
00788        if(!isRecord(e)) {
00789    e.printAST(os);
00790    break;
00791        }
00792        const vector<Expr>& fields = getFields(e);
00793        if(iend != fields.size()) {
00794    e.printAST(os); 
00795    break;
00796        }
00797        os << "(" << push << "RECORD";
00798        for(; i!=iend; ++i)
00799    os <<  space << "(" << push << fields[i] << space 
00800       << e[i] << push << ")" << pop << pop;
00801        os << push << ")";
00802        break;
00803      }
00804      case RECORD_TYPE: {
00805        size_t i=0, iend=e.arity();
00806        if(!isRecord(e)) {
00807    e.printAST(os);
00808    break;
00809        }
00810        const vector<Expr>& fields = getFields(e);
00811        if(iend != fields.size()) {
00812    e.printAST(os); 
00813    break;
00814        }
00815        os << "(" << push << "RECORD_TYPE";
00816        for(; i!=iend; ++i)
00817    os << space << "(" << push <<  fields[i] 
00818       << space << e[i] << push << ")" << pop << pop;
00819        os << push << space << ")";
00820        break;
00821      }
00822      case RECORD_SELECT:
00823        if(isRecordAccess(e))
00824    os << "(" << push << "RECORD_SELECT" << space 
00825       << e[0] << space << getField(e) << push << ")";
00826        else
00827    e.printAST(os);
00828        break;
00829      case TUPLE_SELECT:
00830        if(isTupleAccess(e))
00831    os << "(" << push << "TUPLE_SELECT" << space
00832       << e[0] << space << getIndex(e) << push << ")";
00833        else
00834    e.printAST(os);
00835        break;
00836      case RECORD_UPDATE:
00837        if(isRecordAccess(e) && e.arity() == 2)
00838    os << "(" << push << "RECORD_UPDATE" << space
00839       << e[0] << space << getField(e)
00840       << space << e[1] << push << ")";
00841        else
00842    e.printAST(os);
00843        break;
00844      case TUPLE_UPDATE:
00845        if(isTupleAccess(e))
00846    os << "(" << push << "TUPLE_UPDATE" << space << e[0]
00847       << space << getIndex(e)
00848       << space << e[1] << push << ")";
00849        else
00850    e.printAST(os);
00851        break;
00852      default:
00853        e.printAST(os);
00854        break;
00855      }
00856      break;
00857    }
00858    default:
00859      e.printAST(os);
00860      break;
00861    }
00862    return os;
00863 }
00864 
00865 ///////////////////////////////////////////////////////////////////////////////
00866 //parseExprOp:
00867 //translating special Exprs to regular EXPR??
00868 ///////////////////////////////////////////////////////////////////////////////
00869 Expr
00870 TheoryRecords::parseExprOp(const Expr& e) {
00871   TRACE("parser", "TheoryRecords::parseExprOp(", e, ")");
00872   // If the expression is not a list, it must have been already
00873   // parsed, so just return it as is.
00874   if(RAW_LIST != e.getKind()) return e;
00875 
00876   DebugAssert(e.arity() > 0,
00877         "TheoryRecords::parseExprOp:\n e = "+e.toString());
00878   
00879   const Expr& c1 = e[0][0];
00880   const string& kindStr = c1.getString();
00881   int kind = e.getEM()->getKind(kindStr);
00882   switch(kind) {
00883   case RECORD_TYPE: // (RECORD_TYPE (f1 e1) (f2 e2) ...)
00884   case RECORD: {    // (RECORD      (f1 e1) (f2 e2) ...)
00885     if(e.arity() < 2)
00886       throw ParserException("Empty "+kindStr+": "+e.toString());
00887     vector<Expr> fields;
00888     vector<Expr> kids; 
00889     Expr::iterator i = e.begin(), iend=e.end();
00890     ++i;
00891     for(; i!=iend; ++i) {
00892       if(i->arity() != 2 || (*i)[0].getKind() != ID)
00893   throw ParserException("Bad field declaration in "+kindStr+": "
00894             +i->toString()+"\n in "+e.toString());
00895       fields.push_back((*i)[0][0]);
00896       kids.push_back(parseExpr((*i)[1]));
00897     }
00898     return (kind==RECORD)? recordExpr(fields, kids)
00899       : recordType(fields, kids).getExpr();
00900   }
00901   case RECORD_SELECT: { // (RECORD_SELECT e field)
00902     if(e.arity() != 3 || e[2].getKind() != ID)
00903       throw ParserException("Field must be an ID in RECORD_SELECT: "
00904           +e.toString());
00905     return recordSelect(parseExpr(e[1]), e[2][0].getString());
00906   }
00907   case RECORD_UPDATE: { // (RECORD_UPDATE e1 field e2)
00908     if(e.arity() != 4 || e[2].getKind() != ID)
00909       throw ParserException("Field must be an ID in RECORD_UPDATE: "
00910           +e.toString());
00911     return recordUpdate(parseExpr(e[1]), e[2][0].getString(), parseExpr(e[3]));
00912   }
00913   case TUPLE_SELECT:  { // (TUPLE_SELECT e index)
00914     if(e.arity() != 3 || !e[2].isRational() || !e[2].getRational().isInteger())
00915       throw ParserException("Index must be an integer in TUPLE_SELECT: "
00916           +e.toString());
00917     return tupleSelect(parseExpr(e[1]), e[2].getRational().getInt());
00918   }
00919   case TUPLE_UPDATE:  { // (TUPLE_UPDATE e1 index e2)
00920     if(e.arity() != 4 || !e[2].isRational() || !e[2].getRational().isInteger())
00921       throw ParserException("Index must be an integer in TUPLE_UPDATE: "
00922           +e.toString());
00923     return tupleUpdate(parseExpr(e[1]), e[2].getRational().getInt(),
00924            parseExpr(e[3]));
00925   }
00926   case TUPLE_TYPE:
00927   case TUPLE: {
00928     if(e.arity() < 2)
00929       throw ParserException("Empty "+kindStr+": "+e.toString());
00930     vector<Expr> k;
00931     Expr::iterator i = e.begin(), iend=e.end();
00932     // Skip first element of the vector of kids in 'e'.
00933     // The first element is the operator.
00934     ++i; 
00935     // Parse the kids of e and push them into the vector 'k'
00936     for(; i!=iend; ++i) 
00937       k.push_back(parseExpr(*i));
00938     return (kind==TUPLE)? tupleExpr(k) : tupleType(k).getExpr();
00939   }
00940   default:
00941     DebugAssert(false,
00942     "TheoryRecords::parseExprOp: invalid command or expression: " + e.toString());
00943     break;
00944   }
00945   return e;
00946 }
00947 
00948 
00949 //! Create a record literal
00950 Expr
00951 TheoryRecords::recordExpr(const std::vector<std::string>& fields,
00952         const std::vector<Expr>& kids) {
00953   vector<Expr> fieldExprs;
00954   vector<string>::const_iterator i = fields.begin(), iend = fields.end();
00955   for (; i != iend; ++i) fieldExprs.push_back(getEM()->newStringExpr(*i));
00956   return recordExpr(fieldExprs, kids);
00957 }
00958 
00959 Expr
00960 TheoryRecords::recordExpr(const std::vector<Expr>& fields,
00961         const std::vector<Expr>& kids) {
00962   return Expr(Expr(RECORD, fields).mkOp(), kids);
00963 }
00964 
00965 //! Create a record type
00966 Type
00967 TheoryRecords::recordType(const std::vector<std::string>& fields,
00968         const std::vector<Type>& types) {
00969   vector<Expr> kids;
00970   for(vector<Type>::const_iterator i=types.begin(), iend=types.end();
00971       i!=iend; ++i)
00972     kids.push_back(i->getExpr());
00973   return recordType(fields, kids);
00974 }
00975 
00976 //! Create a record type
00977 Type
00978 TheoryRecords::recordType(const std::vector<std::string>& fields,
00979         const std::vector<Expr>& types) {
00980   vector<Expr> fieldExprs;
00981   vector<string>::const_iterator i = fields.begin(), iend = fields.end();
00982   for (; i != iend; ++i) fieldExprs.push_back(getEM()->newStringExpr(*i));
00983   return recordType(fieldExprs, types);
00984 }
00985 
00986 Type
00987 TheoryRecords::recordType(const std::vector<Expr>& fields,
00988         const std::vector<Expr>& types) {
00989   return Type(Expr(Expr(RECORD_TYPE, fields).mkOp(), types));
00990 }
00991 
00992 //! Create a record field selector expression
00993 Expr
00994 TheoryRecords::recordSelect(const Expr& r, const std::string& field) {
00995   return Expr(getEM()->newSymbolExpr(field, RECORD_SELECT).mkOp(), r);
00996 }
00997 
00998 //! Create a record field update expression
00999 Expr
01000 TheoryRecords::recordUpdate(const Expr& r, const std::string& field,
01001           const Expr& val) {
01002   return Expr(getEM()->newSymbolExpr(field, RECORD_UPDATE).mkOp(), r, val);
01003 }
01004 
01005 //! Get the list of fields from a record literal
01006 const vector<Expr>&
01007 TheoryRecords::getFields(const Expr& r) {
01008   DebugAssert(r.isApply() &&
01009               (r.getOpKind() == RECORD || r.getOpKind() == RECORD_TYPE),
01010         "TheoryRecords::getFields: Not a record literal: "
01011         +r.toString(AST_LANG));
01012   return r.getOpExpr().getKids();
01013 }
01014 
01015 // Get the i-th field name from the record literal
01016 const string&
01017 TheoryRecords::getField(const Expr& r, int i) {
01018   DebugAssert(r.isApply() && 
01019               (r.getOpKind() == RECORD || r.getOpKind() == RECORD_TYPE),
01020         "TheoryRecords::getField: Not a record literal: "
01021         +r.toString());
01022   return r.getOpExpr()[i].getString();
01023 }
01024 
01025 // Get field index from the record literal
01026 int
01027 TheoryRecords::getFieldIndex(const Expr& e, const string& field) {
01028   const vector<Expr>& fields = getFields(e);
01029   for(size_t i=0, iend=fields.size(); i<iend; ++i) {
01030     if(fields[i].getString() == field) return i;
01031   }
01032   DebugAssert(false, "TheoryRecords::getFieldIndex(e="+e.toString()
01033         +", field="+field+"): field is not found");
01034   return -1;
01035 }
01036 
01037 //! Get the field name from the record select and update expressions
01038 const std::string&
01039 TheoryRecords::getField(const Expr& r) {
01040   DebugAssert(r.isApply() && (r.getOpKind() == RECORD_SELECT ||
01041                               r.getOpKind() == RECORD_UPDATE),
01042         "TheoryRecords::getField: Not a record literal: ");
01043   return r.getOpExpr().getName();
01044 }
01045 
01046 //! Create a tuple literal
01047 Expr
01048 TheoryRecords::tupleExpr(const std::vector<Expr>& kids) {
01049   return Expr(TUPLE, kids, getEM());
01050 }
01051 
01052 //! Create a tuple type
01053 Type
01054 TheoryRecords::tupleType(const std::vector<Type>& types) {
01055   vector<Expr> kids;
01056   for(vector<Type>::const_iterator i=types.begin(), iend=types.end();
01057       i!=iend; ++i)
01058     kids.push_back(i->getExpr());
01059   return Type(Expr(TUPLE_TYPE, kids, getEM()));
01060 }
01061 
01062 //! Create a tuple type
01063 Type
01064 TheoryRecords::tupleType(const std::vector<Expr>& types) {
01065   return Expr(TUPLE_TYPE, types, getEM());
01066 }
01067 
01068 //! Create a tuple index selector expression
01069 Expr
01070 TheoryRecords::tupleSelect(const Expr& tup, int i) {
01071   return Expr(Expr(TUPLE_SELECT, getEM()->newRatExpr(i)).mkOp(), tup);
01072 }
01073 
01074 //! Create a tuple index update expression
01075 Expr
01076 TheoryRecords::tupleUpdate(const Expr& tup, int i, const Expr& val) {
01077   return Expr(Expr(TUPLE_UPDATE, getEM()->newRatExpr(i)).mkOp(), tup, val);
01078 }
01079 
01080 //! Get the index from the tuple select and update expressions
01081 int
01082 TheoryRecords::getIndex(const Expr& r) {
01083   DebugAssert(r.isApply() && (r.getOpKind() == TUPLE_SELECT ||
01084                               r.getOpKind() == TUPLE_UPDATE),
01085         "TheoryRecords::getField: Not a record literal: ");
01086   return r.getOpExpr()[0].getRational().getInt();
01087 }

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