00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
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
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
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
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);
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
00501 if (e.isTerm()) {
00502 switch(e.getOpKind()) {
00503 case RECORD:
00504 case TUPLE:
00505 setupCC(e);
00506 break;
00507 default: {
00508 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
00509 i->addToNotify(this, e);
00510
00511 Type tp(getBaseType(e));
00512 Theorem thm;
00513 if(isRecordType(tp))
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
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
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
00560 updateCC(e, d);
00561 break;
00562 default:
00563
00564
00565 if (find(d).getRHS() == d) {
00566
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: {
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: {
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
00867
00868
00869 Expr
00870 TheoryRecords::parseExprOp(const Expr& e) {
00871 TRACE("parser", "TheoryRecords::parseExprOp(", e, ")");
00872
00873
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:
00884 case RECORD: {
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: {
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: {
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: {
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: {
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
00933
00934 ++i;
00935
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
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
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
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
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
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
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
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
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
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
01047 Expr
01048 TheoryRecords::tupleExpr(const std::vector<Expr>& kids) {
01049 return Expr(TUPLE, kids, getEM());
01050 }
01051
01052
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
01063 Type
01064 TheoryRecords::tupleType(const std::vector<Expr>& types) {
01065 return Expr(TUPLE_TYPE, types, getEM());
01066 }
01067
01068
01069 Expr
01070 TheoryRecords::tupleSelect(const Expr& tup, int i) {
01071 return Expr(Expr(TUPLE_SELECT, getEM()->newRatExpr(i)).mkOp(), tup);
01072 }
01073
01074
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
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 }