42 :
Theory(core,
"Datatypes"),
43 d_labels(core->getCM()->getCurrentContext()),
44 d_facts(core->getCM()->getCurrentContext()),
45 d_splitters(core->getCM()->getCurrentContext()),
46 d_splittersIndex(core->getCM()->getCurrentContext(), 0),
47 d_splitterAsserted(core->getCM()->getCurrentContext(), false),
48 d_smartSplits(core->getFlags()[
"dt-smartsplits"].getBool())
78 "datatype: instantiate: Expected find(e)=e");
81 "datatype: instantiate: Expected single label in u");
84 +
"\n\n for expression: "+e.
toString());
87 for (; c_it != c_end; ++c_it) {
88 if ((u & (
Unsigned(1) << (
unsigned)(*c_it).second)) != 0)
break;
91 "datatype: instantiate: couldn't find constructor");
92 const Expr& cons = (*c_it).first;
97 if (consType.
arity() == 1) {
103 for (
int i = 0; i < consType.
arity()-1; ++i) {
104 vars.push_back(
getEM()->newBoundVarExpr(consType[i]));
115 "datatype: initializeLabels: Expected find(e)=e");
120 "datatype: initializeLabels: expected unlabeled expr");
124 "datatype: initializeLabels: Couldn't find constructor "
148 "datatype: mergeLabels: Expected find(e2)=e2");
151 "mergeLabels: expr is not labeled");
161 if (uNew != 0 && ((uNew - 1) & uNew) == 0) {
168 unsigned position,
bool positive)
171 "datatype: mergeLabels2: Expected find(e)=e");
173 "mergeLabels2: expr is not labeled");
178 if (u == uNew)
return;
179 }
else if ((u & uNew) != 0) uNew = u - uNew;
185 else if (((uNew - 1) & uNew) == 0) {
210 else if (expr.
isNot()) {
211 if (expr[0].getOpKind() ==
TESTER) {
216 else if (expr[0].isEq() &&
232 for (; c_it != c_end; ++c_it) {
233 if ((u1 & u2 & ((
Unsigned)1 <<
unsigned((*c_it).second))) != 0) {
236 for (
unsigned i = 0; i < selectors.size(); ++i) {
237 Expr e1 =
Expr(selectors[i].mkOp(), expr[0][0]);
239 if (conj.
isNull()) conj = e2;
245 conj = (e1 && e2).impExpr(!conj);
246 if (bigConj.
isNull()) bigConj = conj;
247 else bigConj = bigConj.
andExpr(conj);
268 "checkSat: expr is not labeled");
270 if ((u & (u-1)) != 0) {
273 "splitter should have been resolved");
278 +
"\n\n for expression: "+e.
toString());
282 for (; c_it != c_end; ++c_it) {
283 if ((u & ((
Unsigned)1 <<
unsigned((*c_it).second))) != 0) {
287 DebugAssert(vec.size() > 1,
"datatype: checkSat: expected 2 or more possible constructors");
296 "checkSat: expr is not labeled");
298 if ((u & (u-1)) != 0) {
300 unsigned pos =
getConsPos(selectorInfo.first);
301 if ((u & ((
Unsigned)1 << pos)) != 0) {
304 "splitter should have been resolved");
372 "Expected datatype");
392 if (sigNew == dsig)
return;
404 if (!repEQsigNew.
isNull()) {
409 int k, ar(d.
arity());
410 for (k = 0; k < ar; ++k) {
411 if (sigNew[k] != dsig[k]) {
451 FatalAssert(
false,
"Unexpected kind in TheoryDatatype::checkType"
458 bool enumerate,
bool computeSize)
461 "Unexpected kind in TheoryDatatype::finiteTypeInfo");
471 bool getSize = enumerate || computeSize;
472 Unsigned totalSize = 0, thisSize, size;
473 vector<Unsigned> sizes;
478 for (; c_it != c_end; ++c_it) {
479 const Expr& cons = (*c_it).first;
482 for (j = 0; j < funType.
arity()-1; ++j) {
483 Expr e2 = funType[j];
495 thisSize = thisSize * size;
497 if (thisSize > 1000000) thisSize = 0;
506 sizes.push_back(thisSize);
507 totalSize = totalSize + thisSize;
516 for (; i < sizes.size(); ++i, ++c_it) {
520 else n = n - sizes[i];
522 if (i == sizes.size() && n != 0) {
526 const Expr& cons = (*c_it).first;
528 if (funType.
arity() == 1) {
532 vector<Expr> kids(funType.
arity()-1);
535 for (
int j = funType.
arity()-2; j >= 0; --j) {
570 Type t = op.lookupType();
584 for (; i != iend; ++i, ++j) {
588 +
"\n\nhas the following type:\n\n "
589 + (*i).getType().getExpr().toString()
590 +
"\n\nbut the expected type is:\n\n "
592 +
"\n\nin datatype function application:\n\n "
601 DebugAssert(
false,
"Unexpected kind in datatype::computeType: "
622 if (op.getKind() !=
SELECTOR)
return tcc;
644 os <<
"DATATYPE" <<
endl;
647 if (first) first =
false;
648 else os <<
"," <<
endl;
651 "Unknown datatype: "+(*i).toString());
654 bool firstCons(
true);
655 for (; c_it != c_end; ++c_it) {
659 else firstCons =
false;
660 const Expr& cons = (*c_it).first;
664 for (
unsigned j = 0; j < sels.size(); ++j) {
671 os << sels[j] <<
space <<
": ";
672 os << sels[j].getType().getExpr()[1];
696 if(first) first =
false;
697 else os <<
"," <<
space;
710 DebugAssert(
false,
"TheoryDatatype::print: Unexpected kind: "
738 "TheoryDatatype::parseExprOp:\n e = "+e.
toString());
741 "Expected ID kind for first elem in list expr");
743 const Expr& c1 = e[0][0];
748 "Empty DATATYPE expression\n"
749 " (expected at least one datatype): "+e.
toString());
753 vector<Expr> allConstructorNames;
754 vector<Expr> constructorNames;
756 vector<Expr> allSelectorNames;
757 vector<Expr> selectorNames;
758 vector<Expr> selectorNamesKids;
760 vector<Expr> allTypes;
762 vector<Expr> typesKids;
765 Expr dt, constructor, selectors, selector;
769 for (i = 0; i < e.
arity()-1; ++i) {
772 "Bad formed datatype expression"
775 "Expected ID kind for datatype name"
777 names.push_back(dt[0][0]);
778 if (namesMap.
count(dt[0][0]) != 0) {
779 throw ParserException(
"Datatype name used more than once"+dt[0][0].getString());
781 namesMap.
insert(dt[0][0],
true);
785 for (i = 0; i < e.
arity()-1; ++i) {
788 "Expected non-empty list for datatype constructors"
793 for(j = 0; j < dt.arity(); ++j) {
796 (constructor.
arity() == 1 || constructor.
arity() == 2),
797 "Unexpected constructor"+constructor.
toString());
799 "Expected ID kind for constructor name"
801 constructorNames.push_back(constructor[0][0]);
803 if (constructor.
arity() == 2) {
804 selectors = constructor[1];
806 "Non-empty list expected as second argument of constructor:\n"
810 for (k = 0; k < selectors.
arity(); ++k) {
811 selector = selectors[k];
813 "Expected list of arity 2 for selector"
816 "Expected ID kind for selector name"
818 selectorNamesKids.push_back(selector[0][0]);
819 if (selector[1].getKind() ==
ID && namesMap.
count(selector[1][0]) > 0) {
820 typesKids.push_back(selector[1][0]);
823 typesKids.push_back(
parseExpr(selector[1]));
826 selectorNames.push_back(
Expr(
RAW_LIST, selectorNamesKids));
827 selectorNamesKids.clear();
836 allConstructorNames.push_back(
Expr(
RAW_LIST, constructorNames));
837 constructorNames.clear();
838 allSelectorNames.push_back(
Expr(
RAW_LIST, selectorNames));
839 selectorNames.clear();
860 const vector<string>& constructors,
861 const vector<vector<string> >& selectors,
862 const vector<vector<Expr> >& types)
864 vector<string> names;
865 vector<vector<string> > constructors2;
866 vector<vector<vector<string> > > selectors2;
867 vector<vector<vector<Expr> > > types2;
868 names.push_back(name);
869 constructors2.push_back(constructors);
870 selectors2.push_back(selectors);
871 types2.push_back(types);
872 return dataType(names, constructors2, selectors2, types2);
879 const vector<vector<string> >& allConstructors,
880 const vector<vector<vector<string> > >& allSelectors,
881 const vector<vector<vector<Expr> > >& allTypes)
883 vector<Expr> returnTypes;
886 bool thisWellFounded;
888 if (names.size() != allConstructors.size() ||
889 allConstructors.size() != allSelectors.size() ||
890 allSelectors.size() != allTypes.size()) {
892 (
"dataType: vector sizes don't match");
899 vector<Type> funTypeArgs;
908 for (i = 0; i < names.size(); ++i) {
912 (
"Attempt to define datatype "+names[i]+
":\n "
913 "This variable is already defined.");
917 returnTypes.push_back(e);
921 vector<Expr> selectorVec;
923 for (i = 0; i < names.size(); ++i) {
925 const vector<string>& constructors = allConstructors[i];
926 const vector<vector<string> >& selectors = allSelectors[i];
927 const vector<vector<Expr> >& types = allTypes[i];
929 if (constructors.size() == 0) {
931 (
"datatype: "+names[i]+
": must have at least one constructor");
933 if (constructors.size() != selectors.size() ||
934 selectors.size() != types.size()) {
936 (
"dataType: vector sizes at index "+
int2string(i)+
" don't match");
941 for (j = 0; j < constructors.size(); ++j) {
945 (
"Attempt to define datatype constructor "+constructors[j]+
":\n "
946 "This variable is already defined.");
950 if (selectors[j].size() != types[j].size()) {
953 ": number of selectors does not match number of types");
955 thisWellFounded =
true;
956 const vector<string>& sels = selectors[j];
957 const vector<Expr>& tps = types[j];
959 vector<Type> selTypes;
962 for (k = 0; k < sels.size(); ++k) {
966 (
"Attempt to define datatype selector "+sels[k]+
":\n "
967 "This variable is already defined.");
970 if (tps[k].isString()) {
974 (
"Unable to resolve type identifier: "+tps[k].getString());
976 }
else t =
Type(tps[k]);
979 (
"Cannot have BOOLEAN inside of datatype");
983 (
"Cannot have function inside of datatype");
986 selTypes.push_back(
Type(t));
989 thisWellFounded =
false;
993 selectorVec.push_back(s);
996 if (selTypes.size() == 0) {
1004 selectorVec.clear();
1006 string testerString =
"is_"+constructors[j];
1010 (
"Attempt to define datatype tester "+testerString+
":\n "
1011 "This variable is already defined.");
1022 bool changed, thisFinite;
1023 int firstNotWellFounded;
1026 firstNotWellFounded = -1;
1027 for (i = 0; i < names.size(); ++i) {
1030 thisWellFounded =
false;
1032 for (; c_it != c_end; ++c_it) {
1033 const Expr& cons = (*c_it).first;
1037 for (j = 0; j < funType.
arity()-1; ++j) {
1041 if (j == funType.
arity()-1) {
1045 else thisFinite =
false;
1048 thisWellFounded =
true;
1051 for (j = 0; j < funType.
arity()-1; ++j) {
1055 if (j == funType.
arity()-1) {
1058 thisWellFounded =
true;
1061 if (!thisWellFounded) {
1062 if (firstNotWellFounded == -1) firstNotWellFounded = i;
1065 if (!returnTypes[i].isWellFounded()) {
1067 returnTypes[i].setWellFounded();
1070 if (thisFinite && !returnTypes[i].isFinite()) {
1072 returnTypes[i].setFinite();
1077 if (firstNotWellFounded >= 0) {
1080 (
"Datatype "+names[firstNotWellFounded]+
" has no finite terms");
1087 const vector<Expr>& args)
1091 throw Exception(
"datatype: unknown constructor: "+constructor);
1094 "\nwhich is not a constructor");
1095 if (args.size() == 0)
return e;
1104 throw Exception(
"datatype: unknown selector: "+selector);
1107 "\nwhich is not a selector");
1116 throw Exception(
"datatype: unknown tester: is_"+constructor);
1119 "\nwhich is not a tester");
1129 "Unknown selector: "+e.
toString());
1137 "getConsForTester called on non-tester"
1148 "getConsPos called on non-constructor");
1150 if (t.isFunction()) t = t[t.arity()-1];
1153 "Could not find datatype: "+t.toString());
1156 "Could not find constructor: "+e.
toString());
1168 "TheoryDatatype::getconstant: too deep recursion depth");
1175 for (; i != iend; ++i) {
1176 const Expr& cons = (*i).first;
1178 d_getConstantStack.erase(t.
getExpr());
1182 for (i = c.
begin(), iend = c.end(); i != iend; ++i) {
1183 const Expr& cons = (*i).first;
1187 for (; j < funType.
arity()-1; ++j) {
1191 DebugAssert(!args.back().isNull(),
"Expected non-null");
1193 if (j == funType.
arity()-1) {
1194 d_getConstantStack.erase(t.
getExpr());
1198 for (i = c.
begin(), iend = c.end(); i != iend; ++i) {
1199 const Expr& cons = (*i).first;
1203 for (; j < funType.
arity()-1; ++j) {
1205 if (t_j == t)
break;
1207 if (args.back().isNull())
break;
1209 if (j == funType.
arity()-1) {
1210 d_getConstantStack.erase(t.
getExpr());
1218 "Expected non-bool, non-function type");
1222 d_getConstantStack.erase(t.
getExpr());
1232 "Couldn't find reachable predicate");
1244 "canCollapse: Expected find(e[0])=e[0]");
1248 if ((u & uCons) == 0)
return true;