CVC3  2.4.1
theory_records.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_records.cpp
4  *
5  * Author: Daniel Wichs
6  *
7  * Created: 7/21/03
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 #include "theory_records.h"
21 #include "typecheck_exception.h"
22 #include "parser_exception.h"
23 #include "smtlib_exception.h"
24 #include "records_proof_rules.h"
25 #include "theory_core.h"
26 
27 
28 using namespace std;
29 using namespace CVC3;
30 
31 /*!
32  * When a record/tuple (dis)equality is expanded into the
33  * (dis)equalities of fields, we have to perform rewrites on the
34  * resulting record terms before the simplifier kicks in.
35  *
36  * Otherwise, if we have r1.f = r2.f, but r1=r2 was asserted before,
37  * for some complex record expressions r1 and r2, then the simplifier
38  * will substitute r2 for r1, and we get r2.f=r2.f at the end, which
39  * is not a useful fact to have.
40  *
41  * However, r1.f and/or r2.f may rewrite to something interesting, and
42  * the equality may yield new important facts.
43  */
44 Theorem
45 TheoryRecords::rewriteAux(const Expr& e) {
46  Theorem res;
47  switch(e.getKind()) {
48  case EQ:
49  case IFF:
50  case AND:
51  case OR: {
52  vector<unsigned> changed;
53  vector<Theorem> thms;
54  for(int i=0, iend=e.arity(); i<iend; ++i) {
55  Theorem t(rewriteAux(e[i]));
56  if(t.getLHS() != t.getRHS()) {
57  changed.push_back(i);
58  thms.push_back(t);
59  }
60  }
61  if(thms.size() > 0) {
62  res = substitutivityRule(e, changed, thms);
63  // Need to guarantee that new expressions are fully simplified
64  if(res.getRHS().hasFind())
65  res = transitivityRule(res, res.getRHS().getFind());
66  } else
67  res = reflexivityRule(e);
68  break;
69  }
70  case NOT: {
71  vector<Theorem> thms;
72  thms.push_back(rewriteAux(e[0]));
73  if(thms[0].getLHS() != thms[0].getRHS()) {
74  res = substitutivityRule(NOT, thms);
75  // Need to guarantee that new expressions are fully simplified
76  if(res.getRHS().hasFind())
77  res = transitivityRule(res, res.getRHS().getFind());
78  } else
79  res = reflexivityRule(e);
80  break;
81  }
82  default:
83  res = rewrite(e);
84  break;
85  }
86  return res;
87 }
88 
89 
90 Theorem
91 TheoryRecords::rewriteAux(const Theorem& thm) {
92  return iffMP(thm, rewriteAux(thm.getExpr()));
93 }
94 
95 
96 TheoryRecords::TheoryRecords(TheoryCore* core)
97  : Theory(core, "Records")
98 {
99 
100  getEM()->newKind(RECORD_TYPE, "_RECORD_TYPE", true);
101  getEM()->newKind(TUPLE_TYPE, "_TUPLE_TYPE", true);
102 
103  getEM()->newKind(RECORD, "_RECORD");
104  getEM()->newKind(RECORD_SELECT, "_RECORD_SELECT");
105  getEM()->newKind(RECORD_UPDATE, "_RECORD_UPDATE");
106  getEM()->newKind(TUPLE, "_TUPLE");
107  getEM()->newKind(TUPLE_SELECT, "_TUPLE_SELECT");
108  getEM()->newKind(TUPLE_UPDATE, "_TUPLE_UPDATE");
109 
111  vector<int> kinds;
112 
113  kinds.push_back(RECORD);
114  kinds.push_back(RECORD_SELECT);
115  kinds.push_back(RECORD_UPDATE);
116  kinds.push_back(RECORD_TYPE);
117  kinds.push_back(TUPLE_TYPE);
118  kinds.push_back(TUPLE);
119  kinds.push_back(TUPLE_SELECT);
120  kinds.push_back(TUPLE_UPDATE);
121 
122  registerTheory(this, kinds);
123 }
124 
126  delete d_rules;
127 }
128 
130 {
131  // TRACE("records", "assertFact => ", e.toString(), "");
132  const Expr& expr = e.getExpr();
133  Theorem expanded;
134  switch(expr.getKind()) {
135  case IFF:
136  case EQ: {
137  int lhsKind = getBaseType(expr[0]).getExpr().getOpKind();
138  if(lhsKind == RECORD_TYPE || lhsKind== TUPLE_TYPE)
139  {
140  expanded = rewriteAux(d_rules->expandEq(e));
141  TRACE("records", "assertFact: enqueuing: ", expanded.toString(), "");
142  enqueueFact(expanded);
143  }
144  return;
145  }
146  case NOT:
147  DebugAssert(expr[0].getKind() == EQ || expr[0].getKind() == IFF,
148  "expecting a disequality or boolean field extraction: "
149  +expr.toString());
150  break;
151  default:
152  DebugAssert(false, "TheoryRecords::assertFact expected an equation"
153  " or negation of equation expression. Instead it got"
154  + e.toString());
155 
156  }
157 
158 }
159 
160 
162  Theorem rw;
163  TRACE("records", "rewrite(", e, ") {");
164  bool needRecursion=false;
165  switch(e.getOpKind()) {
166  case TUPLE_SELECT:
167  case RECORD_SELECT: {
168  switch(e[0].getOpKind()){
169  case RECORD:{
170  rw = d_rules->rewriteLitSelect(e);
171  break;
172  }
173  case TUPLE: {
174  rw = d_rules->rewriteLitSelect(e);
175  break;
176  }
177  case RECORD_UPDATE: {
178  rw = d_rules->rewriteUpdateSelect(e);
179  needRecursion=true;
180  break;
181  }
182  case TUPLE_UPDATE: {
183  rw = d_rules->rewriteUpdateSelect(e);
184  needRecursion=true;
185  break;
186  }
187  default:{
188  rw = reflexivityRule(e);
189  break;
190  }
191  }
192  break;
193  }
194  case RECORD_UPDATE: {
195  DebugAssert(e.arity() == 2,
196  "TheoryRecords::rewrite(RECORD_UPDATE): e="+e.toString());
197  if(e[0].getOpKind() == RECORD)
198  rw= d_rules->rewriteLitUpdate(e);
199  else
200  rw = reflexivityRule(e);
201  break;
202  }
203  case TUPLE_UPDATE: {
204  if(e[0].getOpKind() == TUPLE)
205  rw = d_rules->rewriteLitUpdate(e);
206  else
207  rw = reflexivityRule(e);
208  break;
209  }
210  case RECORD:
211  case TUPLE:
212  rw = rewriteCC(e); // Congruence closure rewrites
213  break;
214  default: {
215  rw = reflexivityRule(e);
216  break;
217  }
218  }
219  Theorem res;
220  if(needRecursion==true) res = transitivityRule(rw, rewrite(rw.getRHS()));
221  else
222  res = rw;
223  TRACE("records", "rewrite => ", res.getRHS(), " }");
224  return res;
225 }
226 
227 
229 {
230  TRACE("records", "computeTCC( ", e, ") {");
231  Expr tcc(Theory::computeTCC(e));
232  switch (e.getOpKind()) {
233  case RECORD:
234  case RECORD_SELECT:
235  case TUPLE:
236  case TUPLE_SELECT:
237  break;
238  case RECORD_UPDATE: {
239  Expr tExpr = e.getType().getExpr();
240  const std::string field(getField(e));
241  int index = getFieldIndex(tExpr, field);
242  Expr pred = getTypePred(e.getType()[index], e[1]);
243  tcc = rewriteAnd(tcc.andExpr(pred)).getRHS();
244  break;
245  }
246  case TUPLE_UPDATE: {
247  Expr tExpr = e.getType().getExpr();
248  int index = getIndex(e);
249  Expr pred = getTypePred(e.getType()[index], e[1]);
250  tcc = rewriteAnd(tcc.andExpr(pred)).getRHS();
251  break;
252  }
253  default: {
254  DebugAssert (false, "Theory records cannot calculate this tcc");
255  }
256  }
257  TRACE("records", "computeTCC => ", tcc, "}");
258  return tcc;
259 }
260 
261 void TheoryRecords::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
262  Type t = e.getType();
263  Expr tExpr = t.getExpr();
264  if(tExpr.getOpKind() == RECORD_TYPE) {
265  const vector<Expr>& fields = getFields(tExpr);
266  for(unsigned int i = 0; i < fields.size() ; i++) {
267  Expr term(recordSelect(e, fields[i].getString()));
268  term = rewrite(term).getRHS();
269  v.push_back(term);
270  }
271  }
272  else if(tExpr.getOpKind() == TUPLE_TYPE) {
273  for(int i=0; i<tExpr.arity(); i++) {
274  Expr term(tupleSelect(e, i));
275  term = rewrite(term).getRHS();
276  v.push_back(term);
277  }
278  }
279 }
280 
281 void TheoryRecords::computeModel(const Expr& e, std::vector<Expr>& v) {
282  Type t = getBaseType(e);
283  Expr tExpr = t.getExpr();
284  vector<Theorem> thms;
285  vector<unsigned> changed;
286  Theorem asst;
287  if(tExpr.getOpKind() == RECORD_TYPE)
288  asst = d_rules->expandRecord(e);
289  else if(tExpr.getOpKind() == TUPLE_TYPE)
290  asst = d_rules->expandTuple(e);
291  else {
292  DebugAssert(false, "TheoryRecords::computeModel("+e.toString()+")");
293  return;
294  }
295 
296  const Expr& lit = asst.getRHS();
297  int size(lit.arity());
298  for(int i = 0; i < size ; i++) {
299  Theorem thm(getModelValue(lit[i]));
300  if(thm.getLHS() != thm.getRHS()) {
301  thms.push_back(thm);
302  changed.push_back(i);
303  }
304  }
305  if(changed.size()>0)
306  asst = transitivityRule(asst, substitutivityRule(lit, changed, thms));
307  assignValue(asst);
308  v.push_back(e);
309 }
310 
311 
313 {
314  TRACE("typePred", "ComputeTypePred[Records]", e, "");
315  Expr tExpr = t.getExpr();
316  switch(tExpr.getOpKind()) {
317  case RECORD_TYPE: {
318  const vector<Expr>& fields = getFields(tExpr);
319  vector<Expr> fieldPreds;
320  for(unsigned int i = 0; i<fields.size(); i++) {
321  Expr sel(recordSelect(e, fields[i].getString()));
322  fieldPreds.push_back(getTypePred(tExpr[i], sel));
323  }
324  Expr pred = andExpr(fieldPreds);
325  TRACE("typePred", "Computed predicate ", pred, "");
326  return pred;
327  }
328  case TUPLE_TYPE: {
329  std::vector<Expr> fieldPreds;
330  for(int i = 0; i<tExpr.arity(); i++) {
331  fieldPreds.push_back(getTypePred(tExpr[i], tupleSelect(e, i)));
332  }
333  Expr pred = andExpr(fieldPreds);
334  TRACE("typePred", "Computed predicate ", pred, "");
335  return pred;
336  }
337  default:
338  DebugAssert(false, "computeTypePred[TheoryRecords] called with wrong type");
339  return Expr();
340  }
341 }
342 
343 
345 {
346  switch (e.getOpKind()) {
347  case RECORD_TYPE: {
348  Expr::iterator i = e.begin(), iend = e.end();
349  for (; i != iend; ) {
350  Type t(*i);
351  ++i;
352  if (t.isBool()) throw Exception
353  ("Records cannot contain BOOLEANs: "
354  +e.toString());
355  if (t.isFunction()) throw Exception
356  ("Records cannot contain functions");
357  }
358  break;
359  }
360  case TUPLE_TYPE: {
361  Expr::iterator i = e.begin(), iend = e.end();
362  for (; i != iend; ) {
363  Type t(*i);
364  ++i;
365  if (t.isBool()) throw Exception
366  ("Tuples cannot contain BOOLEANs: "
367  +e.toString());
368  if (t.isFunction()) throw Exception
369  ("Tuples cannot contain functions");
370  }
371  break;
372  }
373  default:
374  DebugAssert(false, "Unexpected kind in TheoryRecords::checkType"
375  +getEM()->getKindName(e.getOpKind()));
376  }
377 }
378 
379 
380 //TODO: implement finiteTypeInfo
382  bool enumerate, bool computeSize)
383 {
384  return CARD_UNKNOWN;
385 }
386 
387 
389 {
390  switch (e.getOpKind()) {
391  case RECORD:{
392  DebugAssert(e.arity() > 0, "wrong arity of RECORD" + e.toString());
393  vector<Expr> fieldTypes;
394  const vector<Expr>& fields = getFields(e);
395  string previous;
396  DebugAssert((unsigned int)e.arity() == fields.size(),
397  "size of fields does not match size of values");
398  for(int i = 0; i<e.arity(); ++i) {
399  DebugAssert(fields[i].getString() != previous,
400  "a record cannot not contain repeated fields"
401  + e.toString());
402  fieldTypes.push_back(e[i].getType().getExpr());
403  previous=fields[i].getString();
404  }
405  e.setType(Type(recordType(fields, fieldTypes)));
406  return;
407  }
408  case RECORD_SELECT: {
409  DebugAssert(e.arity() == 1, "wrong arity of RECORD_SELECT" + e.toString());
410  Expr t = e[0].getType().getExpr();
411  const string& field = getField(e);
412  DebugAssert(t.getOpKind() == RECORD_TYPE, "incorrect RECORD_SELECT expression"
413  "first child not a RECORD_TYPE" + e.toString());
414  int index = getFieldIndex(t, field);
415  if(index==-1)
416  throw TypecheckException("record selection does not match any field "
417  "in record" + e.toString());
418  e.setType(Type(t[index]));
419  return;
420  }
421  case RECORD_UPDATE: {
422  DebugAssert(e.arity() == 2, "wrong arity of RECORD_UPDATE" + e.toString());
423  Expr t = e[0].getType().getExpr();
424  const string& field = getField(e);
425  DebugAssert(t.getOpKind() == RECORD_TYPE, "incorrect RECORD_SELECT expression"
426  "first child not a RECORD_TYPE" + e.toString());
427  int index = getFieldIndex(t, field);
428  if(index==-1)
429  throw TypecheckException
430  ("record update field \""+field
431  +"\" does not match any in record type:\n"
432  +t.toString()+"\n\nThe complete expression is:\n\n"
433  + e.toString());
434  if(getBaseType(Type(t[index])) != getBaseType(e[1]))
435  throw TypecheckException("Type checking error: \n"+ e.toString());
436  e.setType(e[0].getType());
437  return;
438  }
439  case TUPLE: {
440  DebugAssert(e.arity() > 0, "wrong arity of TUPLE"+ e.toString());
441  std::vector<Expr> types;
442  for(Expr::iterator it = e.begin(), end=e.end(); it!=end; ++it)
443  {
444  types.push_back((*it).getType().getExpr());
445  }
446  e.setType(Type(Expr(TUPLE_TYPE, types, getEM())));
447  return;
448  }
449  case TUPLE_SELECT: {
450  DebugAssert(e.arity() == 1, "wrong arity of TUPLE_SELECT" + e.toString());
451  Expr t = e[0].getType().getExpr();
452  int index = getIndex(e);
453  DebugAssert(t.getOpKind() == TUPLE_TYPE,
454  "incorrect TUPLE_SELECT expression: "
455  "first child is not a TUPLE_TYPE:\n\n" + e.toString());
456  if(index >= t.arity())
457  throw TypecheckException("tuple index exceeds number of fields: \n"
458  + e.toString());
459  e.setType(Type(t[index]));
460  return;
461  }
462  case TUPLE_UPDATE: {
463  DebugAssert(e.arity() == 2, "wrong arity of TUPLE_UPDATE" + e.toString());
464  Expr t = e[0].getType().getExpr();
465  int index = getIndex(e);
466  DebugAssert(t.getOpKind() == TUPLE_TYPE, "incorrect TUPLE_SELECT expression: "
467  "first child not a TUPLE_TYPE:\n\n" + e.toString());
468  if(index >= t.arity())
469  throw TypecheckException("tuple index exceeds number of fields: \n"
470  + e.toString());
471  if(getBaseType(Type(t[index])) != getBaseType(e[1]))
472  throw TypecheckException("tuple update type mismatch: \n"+ e.toString());
473  e.setType(e[0].getType());
474  return;
475  }
476  default:
477  DebugAssert(false,"Unexpected type: "+e.toString());
478  break;
479  }
480 }
481 
482 
483 Type
485  const Expr& e = t.getExpr();
486  Type res;
487  switch(e.getOpKind()) {
488  case TUPLE_TYPE:
489  case RECORD_TYPE: {
490  DebugAssert(e.arity() > 0, "Expected non-empty type");
491  vector<Expr> kids;
492  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
493  kids.push_back(getBaseType(Type(*i)).getExpr());
494  }
495  res = Type(Expr(e.getOp(), kids));
496  break;
497  }
498  default:
499  DebugAssert(false,
500  "TheoryRecords::computeBaseType("+t.toString()+")");
501  res = t;
502  }
503  return res;
504 }
505 
506 
507 void
509  // Only set up terms
510  if (e.isTerm()) {
511  switch(e.getOpKind()) {
512  case RECORD:
513  case TUPLE: // Setup for congruence closure
514  setupCC(e);
515  break;
516  default: { // Everything else
517  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
518  i->addToNotify(this, e);
519  // Check if we have a tuple of record type, and set up those for CC
520  Type tp(getBaseType(e));
521  Theorem thm;
522  if(isRecordType(tp)) // Expand e into its literal, and it setup for CC
523  thm = d_rules->expandRecord(e);
524  else if(isTupleType(tp))
525  thm = d_rules->expandTuple(e);
526  if(!thm.isNull()) {
527  Expr lit(thm.getRHS());
528  TRACE("records", "setup: lit = ", lit, "");
529  // Simplify the kids
530  vector<Theorem> thms;
531  vector<unsigned> changed;
532  for(int i=0,iend=lit.arity(); i<iend; ++i) {
533  TRACE("records", "setup: rewriting lit["+int2string(i)+"] = ",
534  lit[i], "");
535  Theorem t = rewrite(lit[i]);
536  t = transitivityRule(t, find(t.getRHS()));
537  if(lit[i] != t.getRHS()) {
538  thms.push_back(t);
539  changed.push_back(i);
540  }
541  }
542  if(changed.size()>0) {
543  thm = transitivityRule(thm, substitutivityRule(lit, changed, thms));
544  lit = thm.getRHS();
545  }
546  // Check if lit has already been setup
547  if(lit.hasFind()) {
548  enqueueFact(transitivityRule(thm, find(lit)));
549  } else {
550  theoryCore()->setupTerm(lit, this, thm);
552  }
553  }
554  }
555  }
556  }
557 }
558 
559 
560 void
561 TheoryRecords::update(const Theorem& e, const Expr& d) {
562  if (inconsistent()) return;
563  DebugAssert(d.hasFind(), "Expected d to have find");
564 
565  switch(d.getOpKind()) {
566  case RECORD:
567  case TUPLE:
568  // Record and tuple literals are handled by congruence closure updates
569  updateCC(e, d);
570  break;
571  default: // Everything else
572  // If d is not its own representative, don't do anything; the
573  // representative will be sent to us eventually.
574  if (find(d).getRHS() == d) {
575  // Substitute e[1] for e[0] in d and assert the result equal to d
576  Theorem thm = updateHelper(d);
577  thm = transitivityRule(thm, rewrite(thm.getRHS()));
579  }
580  }
581 }
582 
583 
585 {
586  switch(os.lang()) {
587  case PRESENTATION_LANG: {
588  switch(e.getOpKind()){
589  case TUPLE:{
590  int i=0, iend=e.arity();
591  os << "(" << push;
592  if(i!=iend) os << e[i];
593  ++i;
594  for(; i!=iend; ++i) os << push << "," << pop << space << e[i];
595  os << push << ")";
596  break;
597  }
598  case TUPLE_TYPE: {
599  int i=0, iend=e.arity();
600  os << "[" << push;
601  if(i!=iend) os << e[i];
602  ++i;
603  for(; i!=iend; ++i) os << push << "," << pop << space << e[i];
604  os << push << "]";
605  break;
606  }
607  case RECORD: {
608  size_t i=0, iend=e.arity();
609  if(!isRecord(e)) {
610  e.printAST(os);
611  break;
612  }
613  const vector<Expr>& fields = getFields(e);
614  if(iend != fields.size()) {
615  e.printAST(os);
616  break;
617  }
618  os << "(# " << push;
619  if(i!=iend) {
620  os << fields[i].getString() << space
621  << ":="<< space << push << e[i] << pop;
622  ++i;
623  }
624  for(; i!=iend; ++i)
625  os << push << "," << pop << space << fields[i].getString()
626  << space
627  << ":="<< space << push << e[i] << pop;
628  os << push << space << "#)";
629  break;
630  }
631  case RECORD_TYPE: {
632  size_t i=0, iend=e.arity();
633  if(!isRecordType(e)) {
634  e.printAST(os);
635  break;
636  }
637  const vector<Expr>& fields = getFields(e);
638  if(iend != fields.size()) {
639  e.printAST(os);
640  break;
641  }
642  os << "[# " << push;
643  if(i!=iend) {
644  os << fields[i].getString() << ":"<< space << push << e[i] << pop;
645  ++i;
646  }
647  for(; i!=iend; ++i)
648  os << push << "," << pop << space << fields[i].getString()
649  << ":"<< space << push << e[i] << pop;
650  os << push << space << "#]";
651  break;
652  }
653  case RECORD_SELECT:
654  if(isRecordAccess(e) && e.arity() == 1)
655  os << "(" << push << e[0] << push << ")" << "." << push
656  << getField(e);
657  else
658  e.printAST(os);
659  break;
660  case TUPLE_SELECT:
661  if(isTupleAccess(e) && e.arity() == 1)
662  os << "(" << push << e[0] << push << ")" << "." << push
663  << getIndex(e);
664  else
665  e.printAST(os);
666  break;
667  case RECORD_UPDATE:
668  if(isRecordAccess(e) && e.arity() == 2)
669  os << "(" << push << e[0] << space << "WITH ."
670  << push << getField(e)
671  << space << ":=" << space << push << e[1] << push << ")";
672  else
673  e.printAST(os);
674  break;
675  case TUPLE_UPDATE:
676  if(isTupleAccess(e) && e.arity() == 2)
677  os << "(" << push << e[0] << space << "WITH ."
678  << push << getIndex(e)
679  << space << ":=" << space << push << e[1] << push << ")";
680  else
681  e.printAST(os);
682  break;
683  default:
684  e.printAST(os);
685  break;
686  }
687  break;
688  }
689  case SMTLIB_LANG:
690  case SMTLIB_V2_LANG: {
691  d_theoryUsed = true;
692  throw SmtlibException("TheoryRecords::print: SMTLIB not supported");
693  switch(e.getOpKind()){
694  case TUPLE:{
695  int i=0, iend=e.arity();
696  os << "(" << push << "TUPLE";
697  for(; i<iend; ++i) os << space << e[i];
698  os << push << ")";
699  break;
700  }
701  case TUPLE_TYPE: { // FIXME: change to TUPLE_TYPE
702  int i=0, iend=e.arity();
703  os << "(" << push << "TUPLE_TYPE";
704  for(; i!=iend; ++i) os << space << e[i];
705  os << push << ")";
706  break;
707  }
708  case RECORD: {
709  size_t i=0, iend=e.arity();
710  if(!isRecord(e)) {
711  e.printAST(os);
712  break;
713  }
714  const vector<Expr>& fields = getFields(e);
715  if(iend != fields.size()) {
716  e.printAST(os);
717  break;
718  }
719  os << "(" << push << "RECORD";
720  for(; i!=iend; ++i)
721  os << space << "(" << push << fields[i].getString() << space
722  << e[i] << push << ")" << pop << pop;
723  os << push << ")";
724  break;
725  }
726  case RECORD_TYPE: {
727  size_t i=0, iend=e.arity();
728  if(!isRecord(e)) {
729  e.printAST(os);
730  break;
731  }
732  const vector<Expr>& fields = getFields(e);
733  if(iend != fields.size()) {
734  e.printAST(os);
735  break;
736  }
737  os << "(" << push << "RECORD_TYPE";
738  for(; i!=iend; ++i)
739  os << space << "(" << push << fields[i].getString()
740  << space << e[i] << push << ")" << pop << pop;
741  os << push << space << ")";
742  break;
743  }
744  case RECORD_SELECT:
745  if(isRecordAccess(e))
746  os << "(" << push << "RECORD_SELECT" << space
747  << e[0] << space << getField(e) << push << ")";
748  else
749  e.printAST(os);
750  break;
751  case TUPLE_SELECT:
752  if(isTupleAccess(e))
753  os << "(" << push << "TUPLE_SELECT" << space
754  << e[0] << space << getIndex(e) << push << ")";
755  else
756  e.printAST(os);
757  break;
758  case RECORD_UPDATE:
759  if(isRecordAccess(e) && e.arity() == 2)
760  os << "(" << push << "RECORD_UPDATE" << space
761  << e[0] << space << getField(e)
762  << space << e[1] << push << ")";
763  else
764  e.printAST(os);
765  break;
766  case TUPLE_UPDATE:
767  if(isTupleAccess(e))
768  os << "(" << push << "TUPLE_UPDATE" << space << e[0]
769  << space << getIndex(e)
770  << space << e[1] << push << ")";
771  else
772  e.printAST(os);
773  break;
774  default:
775  e.printAST(os);
776  break;
777  }
778  break;
779  }
780  case LISP_LANG: {
781  switch(e.getOpKind()){
782  case TUPLE:{
783  int i=0, iend=e.arity();
784  os << "(" << push << "TUPLE";
785  for(; i<iend; ++i) os << space << e[i];
786  os << push << ")";
787  break;
788  }
789  case TUPLE_TYPE: { // FIXME: change to TUPLE_TYPE
790  int i=0, iend=e.arity();
791  os << "(" << push << "TUPLE_TYPE";
792  for(; i!=iend; ++i) os << space << e[i];
793  os << push << ")";
794  break;
795  }
796  case RECORD: {
797  size_t i=0, iend=e.arity();
798  if(!isRecord(e)) {
799  e.printAST(os);
800  break;
801  }
802  const vector<Expr>& fields = getFields(e);
803  if(iend != fields.size()) {
804  e.printAST(os);
805  break;
806  }
807  os << "(" << push << "RECORD";
808  for(; i!=iend; ++i)
809  os << space << "(" << push << fields[i].getString() << space
810  << e[i] << push << ")" << pop << pop;
811  os << push << ")";
812  break;
813  }
814  case RECORD_TYPE: {
815  size_t i=0, iend=e.arity();
816  if(!isRecord(e)) {
817  e.printAST(os);
818  break;
819  }
820  const vector<Expr>& fields = getFields(e);
821  if(iend != fields.size()) {
822  e.printAST(os);
823  break;
824  }
825  os << "(" << push << "RECORD_TYPE";
826  for(; i!=iend; ++i)
827  os << space << "(" << push << fields[i].getString()
828  << space << e[i] << push << ")" << pop << pop;
829  os << push << space << ")";
830  break;
831  }
832  case RECORD_SELECT:
833  if(isRecordAccess(e))
834  os << "(" << push << "RECORD_SELECT" << space
835  << e[0] << space << getField(e) << push << ")";
836  else
837  e.printAST(os);
838  break;
839  case TUPLE_SELECT:
840  if(isTupleAccess(e))
841  os << "(" << push << "TUPLE_SELECT" << space
842  << e[0] << space << getIndex(e) << push << ")";
843  else
844  e.printAST(os);
845  break;
846  case RECORD_UPDATE:
847  if(isRecordAccess(e) && e.arity() == 2)
848  os << "(" << push << "RECORD_UPDATE" << space
849  << e[0] << space << getField(e)
850  << space << e[1] << push << ")";
851  else
852  e.printAST(os);
853  break;
854  case TUPLE_UPDATE:
855  if(isTupleAccess(e))
856  os << "(" << push << "TUPLE_UPDATE" << space << e[0]
857  << space << getIndex(e)
858  << space << e[1] << push << ")";
859  else
860  e.printAST(os);
861  break;
862  default:
863  e.printAST(os);
864  break;
865  }
866  break;
867  }
868  default:
869  e.printAST(os);
870  break;
871  }
872  return os;
873 }
874 
875 ///////////////////////////////////////////////////////////////////////////////
876 //parseExprOp:
877 //translating special Exprs to regular EXPR??
878 ///////////////////////////////////////////////////////////////////////////////
879 Expr
881  TRACE("parser", "TheoryRecords::parseExprOp(", e, ")");
882  // If the expression is not a list, it must have been already
883  // parsed, so just return it as is.
884  if(RAW_LIST != e.getKind()) return e;
885 
886  DebugAssert(e.arity() > 0,
887  "TheoryRecords::parseExprOp:\n e = "+e.toString());
888 
889  const Expr& c1 = e[0][0];
890  const string& kindStr = c1.getString();
891  int kind = e.getEM()->getKind(kindStr);
892  switch(kind) {
893  case RECORD_TYPE: // (RECORD_TYPE (f1 e1) (f2 e2) ...)
894  case RECORD: { // (RECORD (f1 e1) (f2 e2) ...)
895  if(e.arity() < 2)
896  throw ParserException("Empty "+kindStr+": "+e.toString());
897  vector<Expr> fields;
898  vector<Expr> kids;
899  Expr::iterator i = e.begin(), iend=e.end();
900  ++i;
901  for(; i!=iend; ++i) {
902  if(i->arity() != 2 || (*i)[0].getKind() != ID)
903  throw ParserException("Bad field declaration in "+kindStr+": "
904  +i->toString()+"\n in "+e.toString());
905  fields.push_back((*i)[0][0]);
906  kids.push_back(parseExpr((*i)[1]));
907  }
908  return (kind==RECORD)? recordExpr(fields, kids)
909  : recordType(fields, kids).getExpr();
910  }
911  case RECORD_SELECT: { // (RECORD_SELECT e field)
912  if(e.arity() != 3 || e[2].getKind() != ID)
913  throw ParserException("Field must be an ID in RECORD_SELECT: "
914  +e.toString());
915  return recordSelect(parseExpr(e[1]), e[2][0].getString());
916  }
917  case RECORD_UPDATE: { // (RECORD_UPDATE e1 field e2)
918  if(e.arity() != 4 || e[2].getKind() != ID)
919  throw ParserException("Field must be an ID in RECORD_UPDATE: "
920  +e.toString());
921  return recordUpdate(parseExpr(e[1]), e[2][0].getString(), parseExpr(e[3]));
922  }
923  case TUPLE_SELECT: { // (TUPLE_SELECT e index)
924  if(e.arity() != 3 || !e[2].isRational() || !e[2].getRational().isInteger())
925  throw ParserException("Index must be an integer in TUPLE_SELECT: "
926  +e.toString());
927  return tupleSelect(parseExpr(e[1]), e[2].getRational().getInt());
928  }
929  case TUPLE_UPDATE: { // (TUPLE_UPDATE e1 index e2)
930  if(e.arity() != 4 || !e[2].isRational() || !e[2].getRational().isInteger())
931  throw ParserException("Index must be an integer in TUPLE_UPDATE: "
932  +e.toString());
933  return tupleUpdate(parseExpr(e[1]), e[2].getRational().getInt(),
934  parseExpr(e[3]));
935  }
936  case TUPLE_TYPE:
937  case TUPLE: {
938  if(e.arity() < 2)
939  throw ParserException("Empty "+kindStr+": "+e.toString());
940  vector<Expr> k;
941  Expr::iterator i = e.begin(), iend=e.end();
942  // Skip first element of the vector of kids in 'e'.
943  // The first element is the operator.
944  ++i;
945  // Parse the kids of e and push them into the vector 'k'
946  for(; i!=iend; ++i)
947  k.push_back(parseExpr(*i));
948  return (kind==TUPLE)? tupleExpr(k) : tupleType(k).getExpr();
949  }
950  default:
951  DebugAssert(false,
952  "TheoryRecords::parseExprOp: invalid command or expression: " + e.toString());
953  break;
954  }
955  return e;
956 }
957 
958 
959 //! Create a record literal
960 Expr
961 TheoryRecords::recordExpr(const std::vector<std::string>& fields,
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));
966  return recordExpr(fieldExprs, kids);
967 }
968 
969 Expr
970 TheoryRecords::recordExpr(const std::vector<Expr>& fields,
971  const std::vector<Expr>& kids) {
972  return Expr(Expr(RECORD, fields).mkOp(), kids);
973 }
974 
975 //! Create a record type
976 Type
977 TheoryRecords::recordType(const std::vector<std::string>& fields,
978  const std::vector<Type>& types) {
979  vector<Expr> kids;
980  for(vector<Type>::const_iterator i=types.begin(), iend=types.end();
981  i!=iend; ++i)
982  kids.push_back(i->getExpr());
983  return recordType(fields, kids);
984 }
985 
986 //! Create a record type
987 Type
988 TheoryRecords::recordType(const std::vector<std::string>& fields,
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));
993  return recordType(fieldExprs, types);
994 }
995 
996 Type
997 TheoryRecords::recordType(const std::vector<Expr>& fields,
998  const std::vector<Expr>& types) {
999  return Type(Expr(Expr(RECORD_TYPE, fields).mkOp(), types));
1000 }
1001 
1002 //! Create a record field selector expression
1003 Expr
1004 TheoryRecords::recordSelect(const Expr& r, const std::string& field) {
1005  return Expr(getEM()->newSymbolExpr(field, RECORD_SELECT).mkOp(), r);
1006 }
1007 
1008 //! Create a record field update expression
1009 Expr
1010 TheoryRecords::recordUpdate(const Expr& r, const std::string& field,
1011  const Expr& val) {
1012  return Expr(getEM()->newSymbolExpr(field, RECORD_UPDATE).mkOp(), r, val);
1013 }
1014 
1015 //! Get the list of fields from a record literal
1016 const vector<Expr>&
1018  DebugAssert(r.isApply() &&
1019  (r.getOpKind() == RECORD || r.getOpKind() == RECORD_TYPE),
1020  "TheoryRecords::getFields: Not a record literal: "
1021  +r.toString(AST_LANG));
1022  return r.getOpExpr().getKids();
1023 }
1024 
1025 // Get the i-th field name from the record literal
1026 const string&
1027 TheoryRecords::getField(const Expr& r, int i) {
1028  DebugAssert(r.isApply() &&
1029  (r.getOpKind() == RECORD || r.getOpKind() == RECORD_TYPE),
1030  "TheoryRecords::getField: Not a record literal: "
1031  +r.toString());
1032  return r.getOpExpr()[i].getString();
1033 }
1034 
1035 // Get field index from the record literal
1036 int
1037 TheoryRecords::getFieldIndex(const Expr& e, const string& field) {
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;
1041  }
1042  DebugAssert(false, "TheoryRecords::getFieldIndex(e="+e.toString()
1043  +", field="+field+"): field is not found");
1044  return -1;
1045 }
1046 
1047 //! Get the field name from the record select and update expressions
1048 const std::string&
1050  DebugAssert(r.isApply() && (r.getOpKind() == RECORD_SELECT ||
1051  r.getOpKind() == RECORD_UPDATE),
1052  "TheoryRecords::getField: Not a record literal: ");
1053  return r.getOpExpr().getName();
1054 }
1055 
1056 //! Create a tuple literal
1057 Expr
1058 TheoryRecords::tupleExpr(const std::vector<Expr>& kids) {
1059  return Expr(TUPLE, kids, getEM());
1060 }
1061 
1062 //! Create a tuple type
1063 Type
1064 TheoryRecords::tupleType(const std::vector<Type>& types) {
1065  vector<Expr> kids;
1066  for(vector<Type>::const_iterator i=types.begin(), iend=types.end();
1067  i!=iend; ++i)
1068  kids.push_back(i->getExpr());
1069  return Type(Expr(TUPLE_TYPE, kids, getEM()));
1070 }
1071 
1072 //! Create a tuple type
1073 Type
1074 TheoryRecords::tupleType(const std::vector<Expr>& types) {
1075  return Expr(TUPLE_TYPE, types, getEM());
1076 }
1077 
1078 //! Create a tuple index selector expression
1079 Expr
1080 TheoryRecords::tupleSelect(const Expr& tup, int i) {
1081  return Expr(Expr(TUPLE_SELECT, getEM()->newRatExpr(i)).mkOp(), tup);
1082 }
1083 
1084 //! Create a tuple index update expression
1085 Expr
1086 TheoryRecords::tupleUpdate(const Expr& tup, int i, const Expr& val) {
1087  return Expr(Expr(TUPLE_UPDATE, getEM()->newRatExpr(i)).mkOp(), tup, val);
1088 }
1089 
1090 //! Get the index from the tuple select and update expressions
1091 int
1093  DebugAssert(r.isApply() && (r.getOpKind() == TUPLE_SELECT ||
1094  r.getOpKind() == TUPLE_UPDATE),
1095  "TheoryRecords::getField: Not a record literal: ");
1096  return r.getOpExpr()[0].getRational().getInt();
1097 }
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
Definition: theory.cpp:519
int arity() const
Definition: expr.h:1201
ExprStream & pop(ExprStream &os)
Restore the indentation.
void setupTerm(const Expr &e, Theory *i, const Theorem &thm)
Setup additional terms within a theory-specific setup().
iterator begin() const
Begin iterator.
Definition: expr.h:1211
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
Definition: expr.cpp:400
TheoryCore * theoryCore()
Get a pointer to theoryCore.
Definition: theory.h:93
Data structure of expressions in CVC3.
Definition: expr.h:133
const Theorem & getFind() const
Definition: expr.h:1237
ExprManager * getEM() const
Definition: expr.h:1156
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Type recordType(const std::vector< std::string > &fields, const std::vector< Type > &types)
Create a record type.
An exception thrown by the parser.
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
Definition: theory.cpp:142
bool isRational() const
Definition: expr.h:431
void setupCC(const Expr &e)
Setup a term for congruence closure (must have sig and rep attributes)
Definition: theory.cpp:459
virtual Theorem expandEq(const Theorem &eqThrm)=0
From T|- e = e' return T|- AND (e.i = e'.i) for all i.
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
An exception to be thrown at typecheck error.
Expr tupleSelect(const Expr &tup, int i)
Create a tuple index selector expression.
bool isRecordAccess(const Expr &e)
Test whether expr is a record select/update subclass.
bool isRecordType(const Expr &e)
Test whether expr is a record type.
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
MS C++ specific settings.
Definition: type.h:42
void checkType(const Expr &e)
check record or tuple type
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
Definition: theory.cpp:128
Base class for theories.
Definition: theory.h:64
SMT-LIB v2 format.
Definition: lang.h:52
STL namespace.
Lisp-like format for automatically generated specs.
Definition: lang.h:36
Definition: kinds.h:66
bool isBool() const
Definition: type.h:60
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
Definition: theory.h:719
#define DebugAssert(cond, str)
Definition: debug.h:408
virtual Theorem rewriteLitSelect(const Expr &e)=0
==> (REC_LITERAL (f1 v1) ... (fi vi) ...).fi = vi
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Definition: expr.h:1021
bool hasFind() const
Definition: expr.h:1232
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
RecordsProofRules * d_rules
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Definition: theory.cpp:203
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Definition: expr.h:1191
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
const Expr & getExpr() const
Definition: type.h:52
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
Definition: theory.cpp:162
virtual Theorem expandRecord(const Expr &e)=0
Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #)
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Expr recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &kids)
Create a record literal.
Definition: kinds.h:44
bool d_theoryUsed
Definition: theory.h:79
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory.cpp:81
Identifier is (ID (STRING_EXPR "name"))
Definition: kinds.h:46
bool isInteger() const
std::string toString() const
Definition: theorem.h:404
Theorem rewriteCC(const Expr &e)
Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
Definition: theory.cpp:512
void computeType(const Expr &e)
computes the type of a record or a tuple
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
Definition: kinds.h:68
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
std::string int2string(int n)
Definition: cvc_util.h:46
const Expr & getRHS() const
Definition: theorem.cpp:246
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Definition: theory.cpp:541
Theorem rewrite(const Expr &e)
rewrites an expression e to one of several allowed forms
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
Definition: theory.cpp:406
std::string toString() const
Definition: type.h:80
void assertFact(const Theorem &e)
assert a fact to the theory of records
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Expr getExpr() const
Definition: theorem.cpp:230
bool isNull() const
Definition: theorem.h:164
bool isApply() const
Definition: expr.h:1014
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
Type tupleType(const std::vector< Type > &types)
Create a tuple type.
bool isRecord(const Expr &e)
Test whether expr is a record literal.
const std::string & getName() const
Definition: expr.h:1050
RecordsProofRules * createProofRules()
creates a reference to the proof rules
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Theorem rewriteAux(const Expr &e)
Auxiliary rewrites: Processing of AND and OR of equations. Returns e=e'.
Theorem updateHelper(const Expr &e)
Update the children of the term e.
Definition: theory.cpp:417
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
Definition: theory.cpp:383
void updateCC(const Theorem &e, const Expr &d)
Update a term w.r.t. congruence closure (must be setup with setupCC())
Definition: theory.cpp:473
virtual bool inconsistent()
Check if the current context is inconsistent.
Definition: theory.cpp:97
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
Expr recordUpdate(const Expr &r, const std::string &field, const Expr &val)
Create a record field update expression.
An exception to be thrown by the smtlib translator.
virtual Theorem rewriteUpdateSelect(const Expr &e)=0
==> (REC_SELECT (REC_UPDATE e fi vi) fi) = vi
bool isTupleAccess(const Expr &e)
Test whether expr is a tuple select/update subclass.
ExprStream & print(ExprStream &os, const Expr &e)
pretty printing
int getFieldIndex(const Expr &e, const std::string &field)
Get the field index in the record literal or type.
SMT-LIB format.
Definition: lang.h:34
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
const Expr & getLHS() const
Definition: theorem.cpp:240
bool isTupleType(const Expr &e)
Test if expr represents a tuple type.
Definition: kinds.h:61
Expr tupleUpdate(const Expr &tup, int i, const Expr &val)
Create a tuple index update expression.
Theorem reflexivityRule(const Expr &a)
==> a == a
Definition: theory.h:673
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Definition: theory.h:686
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
const std::string & getString() const
Definition: expr.h:1055
Definition: expr.cpp:35
Definition: kinds.h:99
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
virtual Theorem expandTuple(const Expr &e)=0
Expand a tuple into a literal: |- e = (e.0, ..., e.n-1)
InputLanguage lang() const
Get the current output language.
Definition: expr_stream.h:165
bool isFunction() const
Definition: type.h:62
const std::vector< Expr > & getFields(const Expr &r)
Get the list of fields from a record literal.
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
Definition: theory.cpp:310
virtual Theorem rewriteLitUpdate(const Expr &e)=0
==> (REC_UPDATE (REC_LITERAL (f1 v1) ... (fi vi) ...) fi v') =(REC_LITERAL (f1 v1) ...
int getIndex(const Expr &e)
Get the index from the tuple select and update expressions.
Definition: kinds.h:67
const std::string & getField(const Expr &e, int i)
Get the i-th field name from the record literal or type.
Expr recordSelect(const Expr &r, const std::string &field)
Create a record field select expression.
int getInt() const
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
Definition: theory.h:677
Definition: kinds.h:70
Nice SAL-like language for manually written specs.
Definition: lang.h:32
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
Expr tupleExpr(const std::vector< Expr > &kids)
Create a tuple literal.
iterator end() const
End iterator.
Definition: expr.h:1217