43 d_processQueue(core->getCM()->getCurrentContext()),
44 d_processQueueKind(core->getCM()->getCurrentContext()),
45 d_processIndex(core->getCM()->getCurrentContext(), 0),
46 d_typeComplete(core->getCM()->getCurrentContext(), false)
53 "datatype: instantiate: Expected find(e)=e");
56 "datatype: instantiate: Expected single label in u");
59 +
"\n\n for expression: "+e.
toString());
62 for (; c_it != c_end; ++c_it) {
63 if ((u & ((
Unsigned)1 <<
unsigned((*c_it).second))) != 0)
break;
66 "datatype: instantiate: couldn't find constructor");
67 Expr cons = (*c_it).first;
72 if (consType.
arity() == 1) {
79 for (
int i = 0; i < consType.
arity()-1; ++i) {
80 vars.push_back(
getEM()->newBoundVarExpr(consType[i]));
93 "datatype: initializeLabels: Expected find(e)=e");
98 "datatype: initializeLabels: expected unlabeled expr");
102 "datatype: initializeLabels: Couldn't find constructor "
104 unsigned position = c[cons];
127 "datatype: mergeLabels: Expected hasFind(e2)");
129 const Expr& f = fthm.getRHS();
132 "mergeLabels: expr is not labeled");
145 if (uNew != 0 && ((uNew - 1) & uNew) == 0) {
152 unsigned position,
bool positive)
155 "datatype: mergeLabels2: Expected hasFind(e)");
157 const Expr& f = fthm.getRHS();
159 "mergeLabels2: expr is not labeled");
164 if (u == uNew)
return;
165 }
else if ((u & uNew) != 0) uNew = u - uNew;
172 else if (((uNew - 1) & uNew) == 0) {
185 "checkSat: expr is not labeled");
187 if ((u & (u-1)) != 0) {
190 "splitter should have been resolved");
195 +
"\n\n for expression: "+e.
toString());
198 for (; c_it != c_end; ++c_it) {
199 if ((u & ((
Unsigned)1 <<
unsigned((*c_it).second))) != 0)
break;
202 "datatype: checkSat: couldn't find constructor");
289 if (sigNew == dsig)
return;
303 if (!repEQsigNew.
isNull()) {
309 int k, ar(d.
arity());
310 for (k = 0; k < ar; ++k) {
311 if (sigNew[k] != dsig[k]) {