CVC3  2.4.1
theory_datatype.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file theory_datatype.cpp
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Wed Dec 1 22:32:26 2004
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "theory_datatype.h"
23 #include "datatype_proof_rules.h"
24 #include "typecheck_exception.h"
25 #include "parser_exception.h"
26 #include "smtlib_exception.h"
27 #include "theory_core.h"
28 #include "theory_uf.h"
29 #include "command_line_flags.h"
30 
31 
32 using namespace std;
33 using namespace CVC3;
34 
35 
36 ///////////////////////////////////////////////////////////////////////////////
37 // TheoryDatatype Public Methods //
38 ///////////////////////////////////////////////////////////////////////////////
39 
40 
41 TheoryDatatype::TheoryDatatype(TheoryCore* core)
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())
49 {
51 
52  // Register new local kinds with ExprManager
53  getEM()->newKind(DATATYPE_DECL, "_DATATYPE_DECL");
54  getEM()->newKind(DATATYPE, "_DATATYPE", true);
55  getEM()->newKind(CONSTRUCTOR, "_CONSTRUCTOR");
56  getEM()->newKind(SELECTOR, "_SELECTOR");
57  getEM()->newKind(TESTER, "_TESTER");
58 
59  vector<int> kinds;
60  kinds.push_back(DATATYPE_DECL);
61  kinds.push_back(DATATYPE);
62  kinds.push_back(TESTER);
63  kinds.push_back(CONSTRUCTOR);
64  kinds.push_back(SELECTOR);
65 
66  registerTheory(this, kinds);
67 }
68 
69 
71  delete d_rules;
72 }
73 
74 
75 void TheoryDatatype::instantiate(const Expr& e, const Unsigned& u)
76 {
77  DebugAssert(!e.hasFind() || findExpr(e) == e,
78  "datatype: instantiate: Expected find(e)=e");
79  if (isConstructor(e)) return;
80  DebugAssert(u != 0 && (u & (u-1)) == 0,
81  "datatype: instantiate: Expected single label in u");
82  DebugAssert(d_datatypes.find(getBaseType(e).getExpr()) != d_datatypes.end(),
83  "datatype: instantiate: Unexpected type: "+getBaseType(e).toString()
84  +"\n\n for expression: "+e.toString());
86  ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
87  for (; c_it != c_end; ++c_it) {
88  if ((u & (Unsigned(1) << (unsigned)(*c_it).second)) != 0) break;
89  }
90  DebugAssert(c_it != c_end,
91  "datatype: instantiate: couldn't find constructor");
92  const Expr& cons = (*c_it).first;
93 
94  if (!cons.isFinite() && !e.isSelected()) return;
95 
96  Type consType = getBaseType(cons);
97  if (consType.arity() == 1) {
99  return;
100  }
101  // create vars
102  vector<Expr> vars;
103  for (int i = 0; i < consType.arity()-1; ++i) {
104  vars.push_back(getEM()->newBoundVarExpr(consType[i]));
105  }
106  Expr e2 = getEM()->newClosureExpr(EXISTS, vars,
107  e.eqExpr(Expr(cons.mkOp(), vars)));
109 }
110 
111 
113 {
114  DebugAssert(findExpr(e) == e,
115  "datatype: initializeLabels: Expected find(e)=e");
116  DebugAssert(d_datatypes.find(t.getExpr()) != d_datatypes.end(),
117  "Unknown datatype: "+t.getExpr().toString());
119  DebugAssert(d_labels.find(e) == d_labels.end(),
120  "datatype: initializeLabels: expected unlabeled expr");
121  if (isConstructor(e)) {
122  Expr cons = getConstructor(e);
123  DebugAssert(c.find(cons) != c.end(),
124  "datatype: initializeLabels: Couldn't find constructor "
125  +cons.toString());
126  d_labels.insert(e,
127  SmartCDO<Unsigned>(theoryCore()->getCM()->getCurrentContext(),
128  (Unsigned)1 << c[cons], 0));
129  }
130  else {
131  DebugAssert(c.size() > 0, "No constructors?");
132  Unsigned value = ((Unsigned)1 << c.size()) - 1;
133  d_labels.insert(e,
134  SmartCDO<Unsigned>(theoryCore()->getCM()->getCurrentContext(),
135  value, 0));
136  if (value == 1) instantiate(e, 1);
137  else {
139  }
140  }
141 }
142 
143 
145  const Expr& e1, const Expr& e2)
146 {
147  DebugAssert(e2.hasFind() && findExpr(e2) == e2,
148  "datatype: mergeLabels: Expected find(e2)=e2");
149  DebugAssert(d_labels.find(e1) != d_labels.end() &&
150  d_labels.find(e2) != d_labels.end(),
151  "mergeLabels: expr is not labeled");
152  DebugAssert(getBaseType(e1) == getBaseType(e2), "Expected same type");
153  Unsigned u = d_labels[e2].get().get();
154  Unsigned uNew = u & d_labels[e1].get().get();
155  if (u != uNew) {
156  if (!thm.isNull()) d_facts.push_back(thm);
157  d_labels[e2].get().set(uNew);
158  if (uNew == 0)
160  }
161  if (uNew != 0 && ((uNew - 1) & uNew) == 0) {
162  instantiate(e2, uNew);
163  }
164 }
165 
166 
167 void TheoryDatatype::mergeLabels(const Theorem& thm, const Expr& e,
168  unsigned position, bool positive)
169 {
170  DebugAssert(e.hasFind() && findExpr(e) == e,
171  "datatype: mergeLabels2: Expected find(e)=e");
172  DebugAssert(d_labels.find(e) != d_labels.end(),
173  "mergeLabels2: expr is not labeled");
174  Unsigned u = d_labels[e].get().get();
175  Unsigned uNew = (Unsigned)1 << position;
176  if (positive) {
177  uNew = u & uNew;
178  if (u == uNew) return;
179  } else if ((u & uNew) != 0) uNew = u - uNew;
180  else return;
181  d_facts.push_back(thm);
182  d_labels[e].get().set(uNew);
183  if (uNew == 0)
185  else if (((uNew - 1) & uNew) == 0) {
186  instantiate(e, uNew);
187  }
188 }
189 
190 
192 {
193  if (getBaseType(e).getExpr().getKind() == DATATYPE &&
194  d_labels.find(e) == d_labels.end()) {
196  e.addToNotify(this, Expr());
197  }
198 }
199 
200 
202 {
203  if (!e.isRewrite()) {
204  const Expr& expr = e.getExpr();
205  if (expr.getOpKind() == TESTER) {
206  mergeLabels(e, expr[0],
208  true);
209  }
210  else if (expr.isNot()) {
211  if (expr[0].getOpKind() == TESTER) {
212  mergeLabels(e, expr[0][0],
213  getConsPos(getConsForTester(expr[0].getOpExpr())),
214  false);
215  }
216  else if (expr[0].isEq() &&
217  getBaseType(expr[0][0]).getExpr().getKind() == DATATYPE) {
218  // Propagate disequality down
219  if (d_labels.find(expr[0][0]) == d_labels.end()) {
220  initializeLabels(expr[0][0], getBaseType(expr[0][0]));
221  expr[0][0].addToNotify(this, Expr());
222  }
223  if (d_labels.find(expr[0][1]) == d_labels.end()) {
224  initializeLabels(expr[0][1], getBaseType(expr[0][1]));
225  expr[0][1].addToNotify(this, Expr());
226  }
227  Unsigned u1 = d_labels[expr[0][0]].get().get();
228  Unsigned u2 = d_labels[expr[0][1]].get().get();
229  ExprMap<unsigned>& c = d_datatypes[getBaseType(expr[0][0]).getExpr()];
230  ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
231  Expr bigConj;
232  for (; c_it != c_end; ++c_it) {
233  if ((u1 & u2 & ((Unsigned)1 << unsigned((*c_it).second))) != 0) {
234  vector<Expr>& selectors = d_constructorMap[(*c_it).first];
235  Expr conj;
236  for (unsigned i = 0; i < selectors.size(); ++i) {
237  Expr e1 = Expr(selectors[i].mkOp(), expr[0][0]);
238  Expr e2 = e1.eqExpr(Expr(selectors[i].mkOp(), expr[0][1]));
239  if (conj.isNull()) conj = e2;
240  else conj = conj.andExpr(e2);
241  }
242  if (!conj.isNull()) {
243  Expr e1 = datatypeTestExpr((*c_it).first.getName(), expr[0][0]);
244  Expr e2 = datatypeTestExpr((*c_it).first.getName(), expr[0][1]);
245  conj = (e1 && e2).impExpr(!conj);
246  if (bigConj.isNull()) bigConj = conj;
247  else bigConj = bigConj.andExpr(conj);
248  }
249  }
250  }
251  if (!bigConj.isNull()) {
252  enqueueFact(d_rules->dummyTheorem(d_facts, expr.impExpr(bigConj)));
253  }
254  }
255  }
256  }
257 }
258 
259 
260 void TheoryDatatype::checkSat(bool fullEffort)
261 {
262  bool done = false;
263  while (!done && d_splittersIndex < d_splitters.size()) {
265  if ((!d_smartSplits || getBaseType(e).getExpr().isFinite()) &&
266  findExpr(e) == e) {
267  DebugAssert(d_labels.find(e) != d_labels.end(),
268  "checkSat: expr is not labeled");
269  Unsigned u = d_labels[e].get().get();
270  if ((u & (u-1)) != 0) {
271  done = true;
272  DebugAssert(!d_splitterAsserted || !fullEffort,
273  "splitter should have been resolved");
274  if (!d_splitterAsserted) {
276  (d_datatypes.find(getBaseType(e).getExpr()) != d_datatypes.end(),
277  "datatype: checkSat: Unexpected type: "+getBaseType(e).toString()
278  +"\n\n for expression: "+e.toString());
280  ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
281  vector<Expr> vec;
282  for (; c_it != c_end; ++c_it) {
283  if ((u & ((Unsigned)1 << unsigned((*c_it).second))) != 0) {
284  vec.push_back(datatypeTestExpr((*c_it).first.getName(), e));
285  }
286  }
287  DebugAssert(vec.size() > 1, "datatype: checkSat: expected 2 or more possible constructors");
289  d_splitterAsserted = true;
290  }
291  }
292  }
293  if (d_smartSplits && !done && isSelector(e)) {
294  Expr f = findExpr(e[0]);
295  DebugAssert(d_labels.find(f) != d_labels.end(),
296  "checkSat: expr is not labeled");
297  Unsigned u = d_labels[f].get().get();
298  if ((u & (u-1)) != 0) {
299  pair<Expr, unsigned> selectorInfo = getSelectorInfo(e.getOpExpr());
300  unsigned pos = getConsPos(selectorInfo.first);
301  if ((u & ((Unsigned)1 << pos)) != 0) {
302  done = true;
303  DebugAssert(!d_splitterAsserted || !fullEffort,
304  "splitter should have been resolved");
305  if (!d_splitterAsserted) {
306  addSplitter(datatypeTestExpr(selectorInfo.first.getName(), f));
307  d_splitterAsserted = true;
308  }
309  }
310  }
311  }
312  if (!done) {
313  d_splitterAsserted = false;
315  }
316  }
317 }
318 
319 
321 {
322  // TODO: UF rewrite?
323  Theorem thm;
324  if (isSelector(e)) {
325  if (canCollapse(e)) {
326  thm = d_rules->rewriteSelCons(d_facts, e);
327  return transitivityRule(thm, simplify(thm.getRHS()));
328  }
329  }
330  else if (isTester(e)) {
331  if (isConstructor(e[0])) {
332  return d_rules->rewriteTestCons(e);
333  }
334  }
335  return reflexivityRule(e);
336 }
337 
338 
340 {
341  if (getBaseType(e).getExpr().getKind() == DATATYPE &&
342  d_labels.find(e) == d_labels.end()) {
344  e.addToNotify(this, Expr());
345  }
346  if (e.getKind() != APPLY) return;
347  if (isConstructor(e) && e.arity() > 0) {
349  }
350  if (isSelector(e)) {
352  e[0].setSelected();
353  mergeLabels(Theorem(), e[0], e[0]);
354  }
355  setupCC(e);
356 }
357 
358 
359 void TheoryDatatype::update(const Theorem& e, const Expr& d)
360 {
361  if (d.isNull()) {
362  const Expr& lhs = e.getLHS();
363  const Expr& rhs = e.getRHS();
364  if (isConstructor(lhs) && isConstructor(rhs) &&
365  lhs.isApply() && rhs.isApply() &&
366  lhs.getOpExpr() == rhs.getOpExpr()) {
368  }
369  else {
370  // Possible for rhs to never have been seen: initialize it here
371  DebugAssert(getBaseType(rhs).getExpr().getKind() == DATATYPE,
372  "Expected datatype");
373  if (d_labels.find(rhs) == d_labels.end()) {
374  initializeLabels(rhs, getBaseType(rhs));
375  rhs.addToNotify(this, Expr());
376  }
377  Theorem thm(e);
378  if (lhs.isSelected() && !rhs.isSelected()) {
379  d_facts.push_back(e);
380  rhs.setSelected();
381  thm = Theorem();
382  }
383  mergeLabels(thm, lhs, rhs);
384  }
385  }
386  else {
387  const Theorem& dEQdsig = d.getSig();
388  if (!dEQdsig.isNull()) {
389  const Expr& dsig = dEQdsig.getRHS();
390  Theorem thm = updateHelper(d);
391  const Expr& sigNew = thm.getRHS();
392  if (sigNew == dsig) return;
393  dsig.setRep(Theorem());
394  if (isSelector(sigNew) && canCollapse(sigNew)) {
395  d.setSig(Theorem());
397  }
398  else if (isTester(sigNew) && isConstructor(sigNew[0])) {
399  d.setSig(Theorem());
401  }
402  else {
403  const Theorem& repEQsigNew = sigNew.getRep();
404  if (!repEQsigNew.isNull()) {
405  d.setSig(Theorem());
406  enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
407  }
408  else {
409  int k, ar(d.arity());
410  for (k = 0; k < ar; ++k) {
411  if (sigNew[k] != dsig[k]) {
412  sigNew[k].addToNotify(this, d);
413  }
414  }
415  d.setSig(thm);
416  sigNew.setRep(thm);
418  }
419  }
420  }
421  }
422 }
423 
424 
426 {
427  DebugAssert(e.isRewrite() && e.getLHS().isTerm(), "Expected equality");
428  const Expr& lhs = e.getLHS();
429  if (isConstructor(lhs) && !isConstructor(e.getRHS())) {
430  return symmetryRule(e);
431  }
432  return e;
433 }
434 
435 
437 {
438  switch (e.getKind()) {
439  case DATATYPE: {
440  if (e.arity() != 1 || !e[0].isString())
441  throw Exception("Ill-formed datatype"+e.toString());
442  if (resolveID(e[0].getString()) != e)
443  throw Exception("Unknown datatype"+e.toString());
444  break;
445  }
446  case CONSTRUCTOR:
447  case SELECTOR:
448  case TESTER:
449  throw Exception("Non-type: "+e.toString());
450  default:
451  FatalAssert(false, "Unexpected kind in TheoryDatatype::checkType"
452  +getEM()->getKindName(e.getKind()));
453  }
454 }
455 
456 
458  bool enumerate, bool computeSize)
459 {
461  "Unexpected kind in TheoryDatatype::finiteTypeInfo");
462  if (d_getConstantStack.count(e) != 0) {
463  return CARD_INFINITE;
464  }
465  d_getConstantStack[e] = true;
466 
467  Expr typeExpr = e;
468  ExprMap<unsigned>& c = d_datatypes[typeExpr];
469  ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
470  Cardinality card = CARD_FINITE, cardTmp;
471  bool getSize = enumerate || computeSize;
472  Unsigned totalSize = 0, thisSize, size;
473  vector<Unsigned> sizes;
474  int j;
475 
476  // Loop through constructors, and check if each one only has a finite number
477  // of possibilities
478  for (; c_it != c_end; ++c_it) {
479  const Expr& cons = (*c_it).first;
480  Expr funType = cons.getType().getExpr();
481  thisSize = 1;
482  for (j = 0; j < funType.arity()-1; ++j) {
483  Expr e2 = funType[j];
484  cardTmp = theoryOf(e2)->finiteTypeInfo(e2, size, false, getSize);
485  if (cardTmp == CARD_INFINITE) {
486  card = CARD_INFINITE;
487  break;
488  }
489  else if (cardTmp == CARD_UNKNOWN) {
490  card = CARD_UNKNOWN;
491  getSize = false;
492  // Keep looking to see if we can determine it is infinite
493  }
494  else if (getSize) {
495  thisSize = thisSize * size;
496  // Give up if it gets too big
497  if (thisSize > 1000000) thisSize = 0;
498  if (thisSize == 0) {
499  totalSize = 0;
500  getSize = false;
501  }
502  }
503  }
504  if (card == CARD_INFINITE) break;
505  if (getSize) {
506  sizes.push_back(thisSize);
507  totalSize = totalSize + thisSize;
508  }
509  }
510 
511  if (card == CARD_FINITE) {
512 
513  if (enumerate) {
514  c_it = c.begin();
515  unsigned i = 0;
516  for (; i < sizes.size(); ++i, ++c_it) {
517  if (n < sizes[i]) {
518  break;
519  }
520  else n = n - sizes[i];
521  }
522  if (i == sizes.size() && n != 0) {
523  e = Expr();
524  }
525  else {
526  const Expr& cons = (*c_it).first;
527  Expr funType = cons.getType().getExpr();
528  if (funType.arity() == 1) {
529  e = cons;
530  }
531  else {
532  vector<Expr> kids(funType.arity()-1);
533  Unsigned thisSize;
534  Unsigned elem;
535  for (int j = funType.arity()-2; j >= 0; --j) {
536  if (n == 0) {
537  elem = 0;
538  }
539  else {
540  thisSize = funType[j].typeSizeFinite();
541  elem = n % thisSize;
542  n = n - elem;
543  n = n / thisSize;
544  }
545  kids[j] = funType[j].typeEnumerateFinite(elem);
546  }
547  e = Expr(cons.mkOp(), kids);
548  }
549  }
550  }
551 
552  if (computeSize) {
553  n = totalSize;
554  }
555 
556  }
557  d_getConstantStack.erase(typeExpr);
558  return card;
559 }
560 
561 
563 {
564  switch (e.getOpKind()) {
565  case CONSTRUCTOR:
566  case SELECTOR:
567  case TESTER: {
568  DebugAssert(e.isApply(), "Expected application");
569  Expr op = e.getOp().getExpr();
570  Type t = op.lookupType();
571  DebugAssert(!t.isNull(), "Expected operator to be well-typed");
572  if (t.getExpr().getKind() == DATATYPE) {
573  if (e.arity() != 0)
574  throw TypecheckException("Expected no children: "+e.toString());
575  e.setType(t);
576  break;
577  }
578  else {
579  DebugAssert(t.getExpr().getKind() == ARROW, "Expected function type");
580  if (e.arity() != t.getExpr().arity()-1)
581  throw TypecheckException("Wrong number of children:\n"+e.toString());
582  Expr::iterator i = e.begin(), iend = e.end();
583  Expr::iterator j = t.getExpr().begin();
584  for (; i != iend; ++i, ++j) {
585  if (getBaseType(*i) != getBaseType(Type(*j))) {
586  throw TypecheckException("Type mismatch for expression:\n\n "
587  + (*i).toString()
588  + "\n\nhas the following type:\n\n "
589  + (*i).getType().getExpr().toString()
590  + "\n\nbut the expected type is:\n\n "
591  + (*j).toString()
592  + "\n\nin datatype function application:\n\n "
593  + e.toString());
594  }
595  }
596  e.setType(*j);
597  }
598  break;
599  }
600  default:
601  DebugAssert(false, "Unexpected kind in datatype::computeType: "
602  +e.toString());
603  }
604 }
605 
606 
607 void TheoryDatatype::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
608 }
609 
610 
611 
613 {
614  Expr tcc(Theory::computeTCC(e));
615  switch (e.getKind()) {
616  case CONSTRUCTOR:
617  DebugAssert(e.arity() == 0, "Expected leaf constructor");
618  return trueExpr();
619  case APPLY: {
620  DebugAssert(e.isApply(), "Should be application");
621  Expr op(e.getOpExpr());
622  if (op.getKind() != SELECTOR) return tcc;
623  DebugAssert(e.arity() == 1, "Expected single argument");
624  const std::pair<Expr,unsigned>& p = getSelectorInfo(op);
625  Expr tester = datatypeTestExpr(p.first.getName(), e[0]);
626  return tcc.andExpr(tester);
627  }
628  default:
629  DebugAssert(false,"Unexpected type: "+e.toString());
630  return trueExpr();
631  }
632 }
633 
634 ///////////////////////////////////////////////////////////////////////////////
635 // Pretty-printing //
636 ///////////////////////////////////////////////////////////////////////////////
637 
638 
640  switch (os.lang()) {
641  case PRESENTATION_LANG:
642  switch (e.getKind()) {
643  case DATATYPE_DECL: {
644  os << "DATATYPE" << endl;
645  bool first(true);
646  for (Expr::iterator i = e.begin(), iend = e.end(); i != iend; ++i) {
647  if (first) first = false;
648  else os << "," << endl;
649  os << " " << push << *i << space << "= " << push;
650  DebugAssert(d_datatypes.find(*i) != d_datatypes.end(),
651  "Unknown datatype: "+(*i).toString());
653  ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
654  bool firstCons(true);
655  for (; c_it != c_end; ++c_it) {
656  if (!firstCons) {
657  os << space << "| ";
658  }
659  else firstCons = false;
660  const Expr& cons = (*c_it).first;
661  os << cons;
662  vector<Expr>& sels = d_constructorMap[cons];
663  bool firstSel(true);
664  for (unsigned j = 0; j < sels.size(); ++j) {
665  if (firstSel) {
666  firstSel = false;
667  os << "(";
668  } else {
669  os << ", ";
670  }
671  os << sels[j] << space << ": ";
672  os << sels[j].getType().getExpr()[1];
673  }
674  if (!firstSel) {
675  os << ")";
676  }
677  }
678  os << pop;
679  }
680  os << pop << endl;
681  os << "END;";
682  break;
683  }
684  case DATATYPE:
685  if (e.arity() == 1 && e[0].isString()) {
686  os << e[0].getString();
687  }
688  else e.printAST(os);
689  break;
690  case APPLY:
691  os << e.getOpExpr();
692  if(e.arity() > 0) {
693  os << "(" << push;
694  bool first(true);
695  for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
696  if(first) first = false;
697  else os << "," << space;
698  os << *i;
699  }
700  os << push << ")";
701  }
702  break;
703  case CONSTRUCTOR:
704  case SELECTOR:
705  case TESTER:
706  DebugAssert(e.isSymbol(), "Expected symbol");
707  os << e.getName();
708  break;
709  default:
710  DebugAssert(false, "TheoryDatatype::print: Unexpected kind: "
711  +getEM()->getKindName(e.getKind()));
712  }
713  break;
714  case SMTLIB_LANG:
715  FatalAssert(false, "Not Implemented Yet");
716  break;
717  case LISP_LANG:
718  FatalAssert(false, "Not Implemented Yet");
719  break;
720  default:
721  e.printAST(os);
722  break;
723  }
724  return os;
725 }
726 
727 //////////////////////////////////////////////////////////////////////////////
728 //parseExprOp:
729 //translating special Exprs to regular EXPR??
730 ///////////////////////////////////////////////////////////////////////////////
732 {
733  // If the expression is not a list, it must have been already
734  // parsed, so just return it as is.
735  if(RAW_LIST != e.getKind()) return e;
736 
737  DebugAssert(e.arity() > 0,
738  "TheoryDatatype::parseExprOp:\n e = "+e.toString());
739 
740  DebugAssert(e[0].getKind() == ID,
741  "Expected ID kind for first elem in list expr");
742 
743  const Expr& c1 = e[0][0];
744  int kind = getEM()->getKind(c1.getString());
745  switch(kind) {
746  case DATATYPE: {
747  DebugAssert(e.arity() > 1,
748  "Empty DATATYPE expression\n"
749  " (expected at least one datatype): "+e.toString());
750 
751  vector<Expr> names;
752 
753  vector<Expr> allConstructorNames;
754  vector<Expr> constructorNames;
755 
756  vector<Expr> allSelectorNames;
757  vector<Expr> selectorNames;
758  vector<Expr> selectorNamesKids;
759 
760  vector<Expr> allTypes;
761  vector<Expr> types;
762  vector<Expr> typesKids;
763 
764  int i,j,k;
765  Expr dt, constructor, selectors, selector;
766 
767  // Get names of datatypes
768  ExprMap<bool> namesMap;
769  for (i = 0; i < e.arity()-1; ++i) {
770  dt = e[i+1];
771  DebugAssert(dt.getKind() == RAW_LIST && dt.arity() == 2,
772  "Bad formed datatype expression"
773  +dt.toString());
774  DebugAssert(dt[0].getKind() == ID,
775  "Expected ID kind for datatype name"
776  +dt.toString());
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());
780  }
781  namesMap.insert(dt[0][0], true);
782  }
783 
784  // Loop through datatypes
785  for (i = 0; i < e.arity()-1; ++i) {
786  dt = e[i+1];
787  DebugAssert(dt[1].getKind() == RAW_LIST && dt[1].arity() > 0,
788  "Expected non-empty list for datatype constructors"
789  +dt.toString());
790  dt = dt[1];
791 
792  // Loop through constructors for this datatype
793  for(j = 0; j < dt.arity(); ++j) {
794  constructor = dt[j];
795  DebugAssert(constructor.getKind() == RAW_LIST &&
796  (constructor.arity() == 1 || constructor.arity() == 2),
797  "Unexpected constructor"+constructor.toString());
798  DebugAssert(constructor[0].getKind() == ID,
799  "Expected ID kind for constructor name"
800  +constructor.toString());
801  constructorNames.push_back(constructor[0][0]);
802 
803  if (constructor.arity() == 2) {
804  selectors = constructor[1];
805  DebugAssert(selectors.getKind() == RAW_LIST && selectors.arity() > 0,
806  "Non-empty list expected as second argument of constructor:\n"
807  +constructor.toString());
808 
809  // Loop through selectors for this constructor
810  for (k = 0; k < selectors.arity(); ++k) {
811  selector = selectors[k];
812  DebugAssert(selector.getKind() == RAW_LIST && selector.arity() == 2,
813  "Expected list of arity 2 for selector"
814  +selector.toString());
815  DebugAssert(selector[0].getKind() == ID,
816  "Expected ID kind for selector name"
817  +selector.toString());
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]);
821  }
822  else {
823  typesKids.push_back(parseExpr(selector[1]));
824  }
825  }
826  selectorNames.push_back(Expr(RAW_LIST, selectorNamesKids));
827  selectorNamesKids.clear();
828  types.push_back(Expr(RAW_LIST, typesKids));
829  typesKids.clear();
830  }
831  else {
832  selectorNames.push_back(Expr(RAW_LIST, selectorNamesKids, getEM()));
833  types.push_back(Expr(RAW_LIST, typesKids, getEM()));
834  }
835  }
836  allConstructorNames.push_back(Expr(RAW_LIST, constructorNames));
837  constructorNames.clear();
838  allSelectorNames.push_back(Expr(RAW_LIST, selectorNames));
839  selectorNames.clear();
840  allTypes.push_back(Expr(RAW_LIST, types));
841  types.clear();
842  }
843 
844  return Expr(DATATYPE,
845  Expr(RAW_LIST, names),
846  Expr(RAW_LIST, allConstructorNames),
847  Expr(RAW_LIST, allSelectorNames),
848  Expr(RAW_LIST, allTypes));
849  }
850 
851  default: {
852  throw ParserException("Unexpected datatype expression: "+e.toString());
853  }
854  }
855  return e;
856 }
857 
858 
859 Expr TheoryDatatype::dataType(const string& name,
860  const vector<string>& constructors,
861  const vector<vector<string> >& selectors,
862  const vector<vector<Expr> >& types)
863 {
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);
873 }
874 
875 
876 // Elements of types are either the expr from an existing type or a string
877 // naming one of the datatypes being defined
878 Expr TheoryDatatype::dataType(const vector<string>& names,
879  const vector<vector<string> >& allConstructors,
880  const vector<vector<vector<string> > >& allSelectors,
881  const vector<vector<vector<Expr> > >& allTypes)
882 {
883  vector<Expr> returnTypes;
884 
885  // bool wellFounded = false, infinite = false,
886  bool thisWellFounded;
887 
888  if (names.size() != allConstructors.size() ||
889  allConstructors.size() != allSelectors.size() ||
890  allSelectors.size() != allTypes.size()) {
891  throw TypecheckException
892  ("dataType: vector sizes don't match");
893  }
894 
895  unsigned i, j, k;
896  Expr e;
897 
898  // Create reachability predicate for constructor cycle detection
899  vector<Type> funTypeArgs;
900  funTypeArgs.push_back(Type::anyType(getEM()));
901  funTypeArgs.push_back(Type::anyType(getEM()));
902  Op op = newFunction("_reach_"+names[0],
903  Type::funType(funTypeArgs, boolType()),
904  true /* compute trans closure */);
905  Op reach = getEM()->newSymbolExpr(op.getExpr().getName(),
906  TRANS_CLOSURE).mkOp();
907 
908  for (i = 0; i < names.size(); ++i) {
909  e = resolveID(names[i]);
910  if (!e.isNull()) {
911  throw TypecheckException
912  ("Attempt to define datatype "+names[i]+":\n "
913  "This variable is already defined.");
914  }
915  e = Expr(DATATYPE, getEM()->newStringExpr(names[i]));
916  installID(names[i], e);
917  returnTypes.push_back(e);
918  d_reach[e] = reach;
919  }
920 
921  vector<Expr> selectorVec;
922 
923  for (i = 0; i < names.size(); ++i) {
924 
925  const vector<string>& constructors = allConstructors[i];
926  const vector<vector<string> >& selectors = allSelectors[i];
927  const vector<vector<Expr> >& types = allTypes[i];
928 
929  if (constructors.size() == 0) {
930  throw TypecheckException
931  ("datatype: "+names[i]+": must have at least one constructor");
932  }
933  if (constructors.size() != selectors.size() ||
934  selectors.size() != types.size()) {
935  throw TypecheckException
936  ("dataType: vector sizes at index "+int2string(i)+" don't match");
937  }
938 
939  ExprMap<unsigned>& constMap = d_datatypes[returnTypes[i]];
940 
941  for (j = 0; j < constructors.size(); ++j) {
942  Expr c = resolveID(constructors[j]);
943  if (!c.isNull()) {
944  throw TypecheckException
945  ("Attempt to define datatype constructor "+constructors[j]+":\n "
946  "This variable is already defined.");
947  }
948  c = getEM()->newSymbolExpr(constructors[j], CONSTRUCTOR);
949 
950  if (selectors[j].size() != types[j].size()) {
951  throw TypecheckException
952  ("dataType: constructor at index "+int2string(i)+", "+int2string(j)+
953  ": number of selectors does not match number of types");
954  }
955  thisWellFounded = true;
956  const vector<string>& sels = selectors[j];
957  const vector<Expr>& tps = types[j];
958 
959  vector<Type> selTypes;
960  Type t;
961  Expr s;
962  for (k = 0; k < sels.size(); ++k) {
963  s = resolveID(sels[k]);
964  if (!s.isNull()) {
965  throw TypecheckException
966  ("Attempt to define datatype selector "+sels[k]+":\n "
967  "This variable is already defined.");
968  }
969  s = getEM()->newSymbolExpr(sels[k], SELECTOR);
970  if (tps[k].isString()) {
971  t = Type(resolveID(tps[k].getString()));
972  if (t.isNull()) {
973  throw TypecheckException
974  ("Unable to resolve type identifier: "+tps[k].getString());
975  }
976  } else t = Type(tps[k]);
977  if (t.isBool()) {
978  throw TypecheckException
979  ("Cannot have BOOLEAN inside of datatype");
980  }
981  else if (t.isFunction()) {
982  throw TypecheckException
983  ("Cannot have function inside of datatype");
984  }
985 
986  selTypes.push_back(Type(t));
987  s.setType(Type(returnTypes[i]).funType(Type(t)));
988  if (isDatatype(Type(t)) && !t.getExpr().isWellFounded()) {
989  thisWellFounded = false;
990  }
991  d_selectorMap[s] = pair<Expr,unsigned>(c,k);
992  installID(sels[k], s);
993  selectorVec.push_back(s);
994  }
995  if (thisWellFounded) c.setWellFounded();
996  if (selTypes.size() == 0) {
997  c.setType(Type(returnTypes[i]));
998  c.setFinite();
999  }
1000  else c.setType(Type::funType(selTypes, Type(returnTypes[i])));
1001  installID(constructors[j], c);
1002  constMap[c] = j;
1003  d_constructorMap[c] = selectorVec;
1004  selectorVec.clear();
1005 
1006  string testerString = "is_"+constructors[j];
1007  e = resolveID(testerString);
1008  if (!e.isNull()) {
1009  throw TypecheckException
1010  ("Attempt to define datatype tester "+testerString+":\n "
1011  "This variable is already defined.");
1012  }
1013  e = getEM()->newSymbolExpr(testerString, TESTER);
1014  e.setType(Type(returnTypes[i]).funType(boolType()));
1015  d_testerMap[e] = c;
1016  installID(testerString, e);
1017  }
1018  }
1019 
1020  // Compute fixed point for wellfoundedness check
1021 
1022  bool changed, thisFinite;
1023  int firstNotWellFounded;
1024  do {
1025  changed = false;
1026  firstNotWellFounded = -1;
1027  for (i = 0; i < names.size(); ++i) {
1028  ExprMap<unsigned>& c = d_datatypes[returnTypes[i]];
1029  ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
1030  thisWellFounded = false;
1031  thisFinite = true;
1032  for (; c_it != c_end; ++c_it) {
1033  const Expr& cons = (*c_it).first;
1034  Expr funType = getBaseType(cons).getExpr();
1035  int j;
1036  if (!cons.isFinite()) {
1037  for (j = 0; j < funType.arity()-1; ++j) {
1038  if (!isDatatype(funType[j]) || !funType[j].isFinite())
1039  break;
1040  }
1041  if (j == funType.arity()-1) {
1042  changed = true;
1043  cons.setFinite();
1044  }
1045  else thisFinite = false;
1046  }
1047  if (cons.isWellFounded()) {
1048  thisWellFounded = true;
1049  continue;
1050  }
1051  for (j = 0; j < funType.arity()-1; ++j) {
1052  if (isDatatype(funType[j]) && !funType[j].isWellFounded())
1053  break;
1054  }
1055  if (j == funType.arity()-1) {
1056  changed = true;
1057  cons.setWellFounded();
1058  thisWellFounded = true;
1059  }
1060  }
1061  if (!thisWellFounded) {
1062  if (firstNotWellFounded == -1) firstNotWellFounded = i;
1063  }
1064  else {
1065  if (!returnTypes[i].isWellFounded()) {
1066  changed = true;
1067  returnTypes[i].setWellFounded();
1068  }
1069  }
1070  if (thisFinite && !returnTypes[i].isFinite()) {
1071  changed = true;
1072  returnTypes[i].setFinite();
1073  }
1074  }
1075  } while (changed);
1076 
1077  if (firstNotWellFounded >= 0) {
1078  // TODO: uninstall all ID's
1079  throw TypecheckException
1080  ("Datatype "+names[firstNotWellFounded]+" has no finite terms");
1081  }
1082 
1083  return Expr(DATATYPE_DECL, returnTypes);
1084 }
1085 
1086 Expr TheoryDatatype::datatypeConsExpr(const string& constructor,
1087  const vector<Expr>& args)
1088 {
1089  Expr e = resolveID(constructor);
1090  if (e.isNull())
1091  throw Exception("datatype: unknown constructor: "+constructor);
1092  if (!(e.isSymbol() && e.getKind() == CONSTRUCTOR))
1093  throw Exception("datatype: "+constructor+" resolves to: "+e.toString()+
1094  "\nwhich is not a constructor");
1095  if (args.size() == 0) return e;
1096  return Expr(e.mkOp(), args);
1097 }
1098 
1099 
1100 Expr TheoryDatatype::datatypeSelExpr(const string& selector, const Expr& arg)
1101 {
1102  Expr e = resolveID(selector);
1103  if (e.isNull())
1104  throw Exception("datatype: unknown selector: "+selector);
1105  if (!(e.isSymbol() && e.getKind() == SELECTOR))
1106  throw Exception("datatype: "+selector+" resolves to: "+e.toString()+
1107  "\nwhich is not a selector");
1108  return Expr(e.mkOp(), arg);
1109 }
1110 
1111 
1112 Expr TheoryDatatype::datatypeTestExpr(const string& constructor, const Expr& arg)
1113 {
1114  Expr e = resolveID("is_"+constructor);
1115  if (e.isNull())
1116  throw Exception("datatype: unknown tester: is_"+constructor);
1117  if (!(e.isSymbol() && e.getKind() == TESTER))
1118  throw Exception("datatype: is_"+constructor+" resolves to: "+e.toString()+
1119  "\nwhich is not a tester");
1120  return Expr(e.mkOp(), arg);
1121 }
1122 
1123 
1124 const pair<Expr,unsigned>& TheoryDatatype::getSelectorInfo(const Expr& e)
1125 {
1126  DebugAssert(e.getKind() == SELECTOR, "getSelectorInfo called on non-selector: "
1127  +e.toString());
1128  DebugAssert(d_selectorMap.find(e) != d_selectorMap.end(),
1129  "Unknown selector: "+e.toString());
1130  return d_selectorMap[e];
1131 }
1132 
1133 
1135 {
1136  DebugAssert(e.getKind() == TESTER,
1137  "getConsForTester called on non-tester"
1138  +e.toString());
1140  "Unknown tester: "+e.toString());
1141  return d_testerMap[e];
1142 }
1143 
1144 
1146 {
1148  "getConsPos called on non-constructor");
1149  Type t = getBaseType(e);
1150  if (t.isFunction()) t = t[t.arity()-1];
1151  DebugAssert(isDatatype(t), "Expected datatype");
1152  DebugAssert(d_datatypes.find(t.getExpr()) != d_datatypes.end(),
1153  "Could not find datatype: "+t.toString());
1154  ExprMap<unsigned>& constMap = d_datatypes[t.getExpr()];
1155  DebugAssert(constMap.find(e) != constMap.end(),
1156  "Could not find constructor: "+e.toString());
1157  return constMap[e];
1158 }
1159 
1160 
1162 {
1163  // if a cycle is detected, backtrack from this branch
1164  if (d_getConstantStack.count(t.getExpr()) != 0) {
1165  return Expr();
1166  }
1168  "TheoryDatatype::getconstant: too deep recursion depth");
1169  d_getConstantStack[t.getExpr()] = true;
1170  if (isDatatype(t)) {
1171  DebugAssert(d_datatypes.find(t.getExpr()) != d_datatypes.end(),
1172  "Unknown datatype: "+t.getExpr().toString());
1174  ExprMap<unsigned>::iterator i = c.begin(), iend = c.end();
1175  for (; i != iend; ++i) {
1176  const Expr& cons = (*i).first;
1177  if (!getBaseType(cons).isFunction()) {
1178  d_getConstantStack.erase(t.getExpr());
1179  return cons;
1180  }
1181  }
1182  for (i = c.begin(), iend = c.end(); i != iend; ++i) {
1183  const Expr& cons = (*i).first;
1184  Expr funType = getBaseType(cons).getExpr();
1185  vector<Expr> args;
1186  int j = 0;
1187  for (; j < funType.arity()-1; ++j) {
1188  Type t_j = Type(funType[j]);
1189  if (t_j == t || isDatatype(t_j)) break;
1190  args.push_back(getConstant(t_j));
1191  DebugAssert(!args.back().isNull(), "Expected non-null");
1192  }
1193  if (j == funType.arity()-1) {
1194  d_getConstantStack.erase(t.getExpr());
1195  return Expr(cons.mkOp(), args);
1196  }
1197  }
1198  for (i = c.begin(), iend = c.end(); i != iend; ++i) {
1199  const Expr& cons = (*i).first;
1200  Expr funType = getBaseType(cons).getExpr();
1201  vector<Expr> args;
1202  int j = 0;
1203  for (; j < funType.arity()-1; ++j) {
1204  Type t_j = Type(funType[j]);
1205  if (t_j == t) break;
1206  args.push_back(getConstant(t_j));
1207  if (args.back().isNull()) break;
1208  }
1209  if (j == funType.arity()-1) {
1210  d_getConstantStack.erase(t.getExpr());
1211  return Expr(cons.mkOp(), args);
1212  }
1213  }
1214  FatalAssert(false, "Couldn't find constant for"
1215  +t.toString());
1216  }
1217  DebugAssert(!t.isBool() && !t.isFunction(),
1218  "Expected non-bool, non-function type");
1219  //TODO: this name could be an illegal identifier (i.e. could include spaces)
1220  string name = "datatype_"+t.getExpr().toString();
1221  Expr e = resolveID(name);
1222  d_getConstantStack.erase(t.getExpr());
1223  if (e.isNull()) return newVar(name, t);
1224  return e;
1225 }
1226 
1227 
1229 {
1230  DebugAssert(isDatatype(t), "Expected datatype");
1231  DebugAssert(d_reach.find(t.getExpr()) != d_reach.end(),
1232  "Couldn't find reachable predicate");
1233  return d_reach[t.getExpr()];
1234 }
1235 
1236 
1238 {
1239  DebugAssert(isSelector(e), "canCollapse: Selector expression expected");
1240  DebugAssert(e.arity() == 1, "expected arity 1");
1241  if (isConstructor(e[0])) return true;
1242  if (d_labels.find(e[0]) == d_labels.end()) return false;
1243  DebugAssert(e[0].hasFind() && findExpr(e[0]) == e[0],
1244  "canCollapse: Expected find(e[0])=e[0]");
1245  Unsigned u = d_labels[e[0]].get().get();
1246  Expr cons = getSelectorInfo(e.getOpExpr()).first;
1247  Unsigned uCons = (Unsigned)1 << unsigned(getConsPos(cons));
1248  if ((u & uCons) == 0) return true;
1249  return false;
1250 }