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