45 TheoryRecords::rewriteAux(
const Expr& e) {
52 vector<unsigned> changed;
54 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
62 res = substitutivityRule(e, changed, thms);
67 res = reflexivityRule(e);
72 thms.push_back(rewriteAux(e[0]));
73 if(thms[0].getLHS() != thms[0].getRHS()) {
74 res = substitutivityRule(
NOT, thms);
79 res = reflexivityRule(e);
91 TheoryRecords::rewriteAux(
const Theorem& thm) {
92 return iffMP(thm, rewriteAux(thm.
getExpr()));
118 kinds.push_back(
TUPLE);
141 TRACE(
"records",
"assertFact: enqueuing: ", expanded.
toString(),
"");
148 "expecting a disequality or boolean field extraction: "
152 DebugAssert(
false,
"TheoryRecords::assertFact expected an equation"
153 " or negation of equation expression. Instead it got"
163 TRACE(
"records",
"rewrite(", e,
") {");
164 bool needRecursion=
false;
168 switch(e[0].getOpKind()){
196 "TheoryRecords::rewrite(RECORD_UPDATE): e="+e.
toString());
197 if(e[0].getOpKind() ==
RECORD)
204 if(e[0].getOpKind() ==
TUPLE)
223 TRACE(
"records",
"rewrite => ", res.
getRHS(),
" }");
230 TRACE(
"records",
"computeTCC( ", e,
") {");
240 const std::string field(
getField(e));
254 DebugAssert (
false,
"Theory records cannot calculate this tcc");
257 TRACE(
"records",
"computeTCC => ", tcc,
"}");
265 const vector<Expr>& fields =
getFields(tExpr);
266 for(
unsigned int i = 0; i < fields.size() ; i++) {
273 for(
int i=0; i<tExpr.
arity(); i++) {
284 vector<Theorem> thms;
285 vector<unsigned> changed;
297 int size(lit.
arity());
298 for(
int i = 0; i < size ; i++) {
302 changed.push_back(i);
314 TRACE(
"typePred",
"ComputeTypePred[Records]", e,
"");
318 const vector<Expr>& fields =
getFields(tExpr);
319 vector<Expr> fieldPreds;
320 for(
unsigned int i = 0; i<fields.size(); i++) {
325 TRACE(
"typePred",
"Computed predicate ", pred,
"");
329 std::vector<Expr> fieldPreds;
330 for(
int i = 0; i<tExpr.
arity(); i++) {
334 TRACE(
"typePred",
"Computed predicate ", pred,
"");
338 DebugAssert(
false,
"computeTypePred[TheoryRecords] called with wrong type");
349 for (; i != iend; ) {
353 (
"Records cannot contain BOOLEANs: "
356 (
"Records cannot contain functions");
362 for (; i != iend; ) {
366 (
"Tuples cannot contain BOOLEANs: "
369 (
"Tuples cannot contain functions");
374 DebugAssert(
false,
"Unexpected kind in TheoryRecords::checkType"
382 bool enumerate,
bool computeSize)
393 vector<Expr> fieldTypes;
394 const vector<Expr>& fields =
getFields(e);
397 "size of fields does not match size of values");
398 for(
int i = 0; i<e.
arity(); ++i) {
400 "a record cannot not contain repeated fields"
402 fieldTypes.push_back(e[i].getType().getExpr());
403 previous=fields[i].getString();
413 "first child not a RECORD_TYPE" + e.
toString());
426 "first child not a RECORD_TYPE" + e.
toString());
430 (
"record update field \""+field
431 +
"\" does not match any in record type:\n"
432 +t.toString()+
"\n\nThe complete expression is:\n\n"
441 std::vector<Expr> types;
444 types.push_back((*it).getType().getExpr());
454 "incorrect TUPLE_SELECT expression: "
455 "first child is not a TUPLE_TYPE:\n\n" + e.
toString());
456 if(index >= t.arity())
467 "first child not a TUPLE_TYPE:\n\n" + e.
toString());
468 if(index >= t.arity())
500 "TheoryRecords::computeBaseType("+t.
toString()+
")");
518 i->addToNotify(
this, e);
528 TRACE(
"records",
"setup: lit = ", lit,
"");
530 vector<Theorem> thms;
531 vector<unsigned> changed;
532 for(
int i=0,iend=lit.arity(); i<iend; ++i) {
537 if(lit[i] != t.
getRHS()) {
539 changed.push_back(i);
542 if(changed.size()>0) {
574 if (
find(d).getRHS() == d) {
590 int i=0, iend=e.
arity();
592 if(i!=iend) os << e[i];
594 for(; i!=iend; ++i) os << push <<
"," <<
pop <<
space << e[i];
599 int i=0, iend=e.
arity();
601 if(i!=iend) os << e[i];
603 for(; i!=iend; ++i) os << push <<
"," <<
pop <<
space << e[i];
608 size_t i=0, iend=e.
arity();
613 const vector<Expr>& fields =
getFields(e);
614 if(iend != fields.size()) {
620 os << fields[i].getString() <<
space
621 <<
":="<<
space << push << e[i] <<
pop;
625 os << push <<
"," <<
pop <<
space << fields[i].getString()
627 <<
":="<<
space << push << e[i] <<
pop;
628 os << push <<
space <<
"#)";
632 size_t i=0, iend=e.
arity();
637 const vector<Expr>& fields =
getFields(e);
638 if(iend != fields.size()) {
644 os << fields[i].getString() <<
":"<<
space << push << e[i] <<
pop;
648 os << push <<
"," <<
pop <<
space << fields[i].getString()
649 <<
":"<<
space << push << e[i] <<
pop;
650 os << push <<
space <<
"#]";
669 os <<
"(" <<
push << e[0] <<
space <<
"WITH ."
677 os <<
"(" << push << e[0] <<
space <<
"WITH ."
679 <<
space <<
":=" <<
space << push << e[1] << push <<
")";
695 int i=0, iend=e.
arity();
696 os <<
"(" <<
push <<
"TUPLE";
697 for(; i<iend; ++i) os <<
space << e[i];
702 int i=0, iend=e.
arity();
703 os <<
"(" <<
push <<
"TUPLE_TYPE";
704 for(; i!=iend; ++i) os <<
space << e[i];
709 size_t i=0, iend=e.
arity();
714 const vector<Expr>& fields =
getFields(e);
715 if(iend != fields.size()) {
719 os <<
"(" <<
push <<
"RECORD";
721 os <<
space <<
"(" << push << fields[i].getString() <<
space
722 << e[i] << push <<
")" <<
pop <<
pop;
727 size_t i=0, iend=e.
arity();
732 const vector<Expr>& fields =
getFields(e);
733 if(iend != fields.size()) {
737 os <<
"(" <<
push <<
"RECORD_TYPE";
739 os <<
space <<
"(" << push << fields[i].getString()
741 os << push <<
space <<
")";
746 os <<
"(" <<
push <<
"RECORD_SELECT" <<
space
753 os <<
"(" << push <<
"TUPLE_SELECT" <<
space
760 os <<
"(" << push <<
"RECORD_UPDATE" <<
space
762 <<
space << e[1] << push <<
")";
768 os <<
"(" << push <<
"TUPLE_UPDATE" <<
space << e[0]
770 <<
space << e[1] << push <<
")";
783 int i=0, iend=e.
arity();
784 os <<
"(" <<
push <<
"TUPLE";
785 for(; i<iend; ++i) os <<
space << e[i];
790 int i=0, iend=e.
arity();
791 os <<
"(" <<
push <<
"TUPLE_TYPE";
792 for(; i!=iend; ++i) os <<
space << e[i];
797 size_t i=0, iend=e.
arity();
802 const vector<Expr>& fields =
getFields(e);
803 if(iend != fields.size()) {
807 os <<
"(" <<
push <<
"RECORD";
809 os <<
space <<
"(" << push << fields[i].getString() <<
space
810 << e[i] << push <<
")" <<
pop <<
pop;
815 size_t i=0, iend=e.
arity();
820 const vector<Expr>& fields =
getFields(e);
821 if(iend != fields.size()) {
825 os <<
"(" <<
push <<
"RECORD_TYPE";
827 os <<
space <<
"(" << push << fields[i].getString()
829 os << push <<
space <<
")";
834 os <<
"(" <<
push <<
"RECORD_SELECT" <<
space
841 os <<
"(" << push <<
"TUPLE_SELECT" <<
space
848 os <<
"(" << push <<
"RECORD_UPDATE" <<
space
850 <<
space << e[1] << push <<
")";
856 os <<
"(" << push <<
"TUPLE_UPDATE" <<
space << e[0]
858 <<
space << e[1] << push <<
")";
881 TRACE(
"parser",
"TheoryRecords::parseExprOp(", e,
")");
887 "TheoryRecords::parseExprOp:\n e = "+e.
toString());
889 const Expr& c1 = e[0][0];
901 for(; i!=iend; ++i) {
902 if(i->
arity() != 2 || (*i)[0].getKind() !=
ID)
905 fields.push_back((*i)[0][0]);
952 "TheoryRecords::parseExprOp: invalid command or expression: " + e.
toString());
962 const std::vector<Expr>& kids) {
963 vector<Expr> fieldExprs;
964 vector<string>::const_iterator i = fields.begin(), iend = fields.end();
965 for (; i != iend; ++i) fieldExprs.push_back(
getEM()->newStringExpr(*i));
971 const std::vector<Expr>& kids) {
978 const std::vector<Type>& types) {
980 for(vector<Type>::const_iterator i=types.begin(), iend=types.end();
982 kids.push_back(i->getExpr());
989 const std::vector<Expr>& types) {
990 vector<Expr> fieldExprs;
991 vector<string>::const_iterator i = fields.begin(), iend = fields.end();
992 for (; i != iend; ++i) fieldExprs.push_back(
getEM()->newStringExpr(*i));
998 const std::vector<Expr>& types) {
1020 "TheoryRecords::getFields: Not a record literal: "
1030 "TheoryRecords::getField: Not a record literal: "
1038 const vector<Expr>& fields =
getFields(e);
1039 for(
size_t i=0, iend=fields.size(); i<iend; ++i) {
1040 if(fields[i].getString() == field)
return i;
1043 +
", field="+field+
"): field is not found");
1052 "TheoryRecords::getField: Not a record literal: ");
1066 for(vector<Type>::const_iterator i=types.begin(), iend=types.end();
1068 kids.push_back(i->getExpr());
1095 "TheoryRecords::getField: Not a record literal: ");