CVC3  2.4.1
theory_uf.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_uf.cpp
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Fri Jan 24 02:07:59 2003
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 #include "theory_uf.h"
22 #include "uf_proof_rules.h"
23 #include "typecheck_exception.h"
24 #include "parser_exception.h"
25 #include "smtlib_exception.h"
26 #include "command_line_flags.h"
27 #include "theory_core.h"
28 #include "translator.h"
29 // HACK: include theory_records.h to access the TUPLE_TYPE kind
30 #include "theory_records.h"
31 
32 
33 using namespace std;
34 using namespace CVC3;
35 
36 
37 ///////////////////////////////////////////////////////////////////////////////
38 // TheoryUF Public Methods //
39 ///////////////////////////////////////////////////////////////////////////////
40 
41 
42 TheoryUF::TheoryUF(TheoryCore* core)//, bool useAckermann)
43  : Theory(core, "Uninterpreted Functions"),
44  d_applicationsInModel(core->getFlags()["applications"].getBool()),
45  d_funApplications(core->getCM()->getCurrentContext()),
46  d_funApplicationsIdx(core->getCM()->getCurrentContext(), 0),
47  d_sharedIdx1(core->getCM()->getCurrentContext(), 0),
48  d_sharedIdx2(core->getCM()->getCurrentContext(), 0),
49  d_sharedTermsMap(core->getCM()->getCurrentContext())
50  // d_useAckermann(useAckermann)
51 {
53 
54  // Register new local kinds with ExprManager
55  getEM()->newKind(TRANS_CLOSURE, "_TRANS_CLOSURE");
56  getEM()->newKind(OLD_ARROW, "_OLD_ARROW", true);
57 
58  vector<int> kinds;
59  //TODO: should this stuff really be in theory_uf?
60  kinds.push_back(TYPEDECL);
61  kinds.push_back(LAMBDA);
62  kinds.push_back(ARROW);
63  kinds.push_back(OLD_ARROW);
64  kinds.push_back(UFUNC);
65  kinds.push_back(TRANS_CLOSURE);
66 
67  registerTheory(this, kinds);
68 }
69 
70 
72  delete d_rules;
73 }
74 
75 
76 //TODO: clean up transitive closure tables
77 // be sure to free CD objects
78 
80 {
81  const Expr& expr = e.getExpr();
82  switch (expr.getKind()) {
83  case NOT:
84  break;
85  case APPLY:
86  if (expr.getOpExpr().computeTransClosure()) {
88  }
89  else if (expr.getOpKind() == TRANS_CLOSURE) {
90  // const Expr& rel = expr.getFun();
91  DebugAssert(expr.isApply(), "Should be apply");
92  Expr rel = resolveID(expr.getOpExpr().getName());
93  DebugAssert(!rel.isNull(), "Expected known identifier");
94  DebugAssert(rel.isSymbol() && rel.getKind()==UFUNC && expr.arity()==2,
95  "Unexpected use of transitive closure: "+expr.toString());
96 
97  // Insert into transitive closure table
99  TCMapPair* pTable;
100  if (i == d_transClosureMap.end()) {
101  pTable = new TCMapPair();
102  d_transClosureMap[rel] = pTable;
103  }
104  else {
105  pTable = (*i).second;
106  }
107 
108  ExprMap<CDList<Theorem>*>::iterator i2 = pTable->appearsFirstMap.find(expr[0]);
109  CDList<Theorem>* pList;
110  if (i2 == pTable->appearsFirstMap.end()) {
111  pList = new(true) CDList<Theorem>(theoryCore()->getCM()->getCurrentContext());
112  pTable->appearsFirstMap[expr[0]] = pList;
113  }
114  else {
115  pList = (*i2).second;
116  }
117  pList->push_back(e);
118 
119  i2 = pTable->appearsSecondMap.find(expr[1]);
120  if (i2 == pTable->appearsSecondMap.end()) {
121  pList = new(true) CDList<Theorem>(theoryCore()->getCM()->getCurrentContext());
122  pTable->appearsSecondMap[expr[1]] = pList;
123  }
124  else {
125  pList = (*i2).second;
126  }
127  pList->push_back(e);
128 
129  // Compute transitive closure with existing relations
130  size_t s,l;
131  i2 = pTable->appearsFirstMap.find(expr[1]);
132  if (i2 != pTable->appearsFirstMap.end()) {
133  pList = (*i2).second;
134  s = pList->size();
135  for (l = 0; l < s; ++l) {
136  enqueueFact(d_rules->relTrans(e,(*pList)[l]));
137  }
138  }
139 
140  i2 = pTable->appearsSecondMap.find(expr[0]);
141  if (i2 != pTable->appearsSecondMap.end()) {
142  pList = (*i2).second;
143  s = pList->size();
144  for (l = 0; l < s; ++l) {
145  enqueueFact(d_rules->relTrans((*pList)[l],e));
146  }
147  }
148  }
149  break;
150  default:
151  break;
152  }
153 }
154 
155 
156 void TheoryUF::checkSat(bool fullEffort)
157 {
158  // Check for any unexpanded lambdas
159  bool enqueued = false;
163  if(e.getOp().getExpr().isLambda()) {
164  IF_DEBUG(debugger.counter("Expanded lambdas (checkSat)")++;)
166  enqueued = true;
167  }
168  }
169 
170  // If something has been returned, we are done
171  if (!fullEffort || enqueued) return;
172 
173  // Expand on the shared terms
175  + 1, d_sharedIdx2 = 0 ) {
177  if( f1.getOpKind() == UFUNC && !f1.getSig().isNull() ) {
178  f1 = f1.getSig().getRHS();
179  Expr f1_fun = f1.getOp().getExpr();
180  for( ; d_sharedIdx2 < d_sharedIdx1; d_sharedIdx2 = d_sharedIdx2 + 1 ) {
182  if (f2.getOpKind() == UFUNC && !f2.getSig().isNull() ) {
183  f2 = f2.getSig().getRHS();
184  Expr f2_fun = f2.getOp().getExpr();
185  if( f1 != f2 && find(f1).getRHS() != find(f2).getRHS() && f1_fun == f2_fun ) {
186  for( int k = 0; k < f1.arity(); ++k ) {
187  Expr x_k = f1[k];
188  Expr y_k = f2[k];
189  if( d_sharedTermsMap.find(x_k) == d_sharedTermsMap.end() )
190  continue;
191  if( d_sharedTermsMap.find(y_k) == d_sharedTermsMap.end() )
192  continue;
193  Expr eq = x_k.eqExpr(y_k);
194  if( !simplify(eq).getRHS().isBoolConst() ) {
195  TRACE("sharing", "splitting " + y_k.toString(), " and ", x_k.toString());
196  TRACE("sharing", "from " + f2.toString(), " and ", f1.toString());
197  addSplitter(eq);
198  enqueued = true;
199  }
200  }
201  if( enqueued )
202  return;
203  }
204  }
205  }
206  }
207  }
208 }
209 
210 
212 {
213  if (e.isApply()) {
214  const Expr& op = e.getOpExpr();
215  int opKind = op.getKind();
216  switch(opKind) {
217  case LAMBDA: {
218  Theorem res = d_rules->applyLambda(e);
219  // Simplify recursively
220  res = transitivityRule(res, simplify(res.getRHS()));
221  IF_DEBUG(debugger.counter("Expanded lambdas")++;)
222  return res;
223  }
224  default: // A truly uninterpreted function
225  if (e.getType().isBool()) return reflexivityRule(e);
226  else return rewriteCC(e);
227  }
228  }
229  else {
230  e.setRewriteNormal();
231  return reflexivityRule(e);
232  }
233 }
234 
235 
236 void TheoryUF::setup(const Expr& e)
237 {
238  if (e.isTerm() && e.getType().card() != CARD_INFINITE) {
239  addSharedTerm(e);
240  theoryOf(e.getType())->addSharedTerm(e);
241  }
242  if (e.getKind() != APPLY) return;
243 // if (d_useAckermann) {
244 // Theorem thm = getCommonRules()->varIntroSkolem(e);
245 // theoryCore()->addToVarDB(thm.getRHS());
246 // enqueueFact(thm);
247 // }
248 // else {
249  setupCC(e);
250 // }
251  // Add this function application for concrete model generation
252  TRACE("model", "TheoryUF: add function application ", e, "");
254 }
255 
256 
257 void TheoryUF::update(const Theorem& e, const Expr& d)
258 {
259  /*
260  int k, ar(d.arity());
261  const Theorem& dEQdsig = d.getSig();
262  if (!dEQdsig.isNull()) {
263  Expr dsig = dEQdsig.getRHS();
264  Theorem thm = updateHelper(d);
265  const Expr& sigNew = thm.getRHS();
266  if (sigNew == dsig) return;
267  dsig.setRep(Theorem());
268  const Theorem& repEQsigNew = sigNew.getRep();
269  if (!repEQsigNew.isNull()) {
270  d.setSig(Theorem());
271  enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
272  }
273  else {
274  for (k = 0; k < ar; ++k) {
275  if (sigNew[k] != dsig[k]) {
276  sigNew[k].addToNotify(this, d);
277  }
278  }
279  d.setSig(thm);
280  sigNew.setRep(thm);
281 
282  if (d_compute_trans_closure && d.getKind() == APPLY &&
283  d.arity() == 2 && findExpr(d).isTrue()) {
284  thm = iffTrueElim(transitivityRule(symmetryRule(thm),find(d)));
285  enqueueFact(d_rules->relToClosure(thm));
286  }
287 
288  }
289  }
290  */
291  // Record the original signature
292  const Theorem& dEQdsig = d.getSig();
293  if (!dEQdsig.isNull()) {
294  const Expr& dsig = dEQdsig.getRHS();
295  Theorem thm = updateHelper(d);
296  const Expr& sigNew = thm.getRHS();
297  if (sigNew == dsig) {
298  // TRACE_MSG("facts update", "updateCC["+getName()+"]() [no change] => }");
299  return;
300  }
301  dsig.setRep(Theorem());
302  const Theorem& repEQsigNew = sigNew.getRep();
303  if (!repEQsigNew.isNull()) {
304  d.setSig(Theorem());
305  enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
306  }
307  else if (d.getType().isBool()) {
308  d.setSig(Theorem());
309  enqueueFact(thm);
310  }
311  else {
312  int k, ar(d.arity());
313  for (k = 0; k < ar; ++k) {
314  if (sigNew[k] != dsig[k]) {
315  sigNew[k].addToNotify(this, d);
316  }
317  }
318  d.setSig(thm);
319  sigNew.setRep(thm);
320  if (dsig != sigNew && d.isApply() && findExpr(d).isTrue()) {
321  if (d.getOpExpr().computeTransClosure()) {
323  find(d)));
325  }
326  else if (d.getOpKind() == TRANS_CLOSURE) {
328  find(d)));
329  enqueueFact(thm);
330  }
331  }
332  }
333  }
334 }
335 
336 
337 void TheoryUF::checkType(const Expr& e)
338 {
339  switch (e.getKind()) {
340  case ARROW: {
341  if (e.arity() < 2) throw Exception
342  ("Function type needs at least two arguments"
343  +e.toString());
344  Expr::iterator i = e.begin(), iend = e.end();
345  for (; i != iend; ) {
346  Type t(*i);
347  ++i;
348  if (i == iend && t.isBool()) break;
349  if (t.isBool()) throw Exception
350  ("Function argument types must be non-Boolean: "
351  +e.toString());
352  if (t.isFunction()) throw Exception
353  ("Function domain or range types cannot be functions: "
354  +e.toString());
355  }
356  break;
357  }
358  case TYPEDECL: {
359  break;
360  }
361  default:
362  DebugAssert(false, "Unexpected kind in TheoryUF::checkType"
363  +getEM()->getKindName(e.getKind()));
364  }
365 }
366 
367 
369  bool enumerate, bool computeSize)
370 {
371  if (e.getKind() != ARROW) {
372  // uninterpreted type
373  return CARD_UNKNOWN;
374  }
375  Expr::iterator i = e.begin(), iend = e.end();
376  Cardinality card = CARD_FINITE, cardTmp;
377  Unsigned thisSize = 1, size;
378  bool getSize = enumerate || computeSize;
379  for (; i != iend; ) {
380  Expr e2 = (*i);
381  cardTmp = theoryOf(e2)->finiteTypeInfo(e2, size, getSize, false);
382  if (cardTmp == CARD_INFINITE) {
383  return CARD_INFINITE;
384  }
385  else if (cardTmp == CARD_UNKNOWN) {
386  card = CARD_UNKNOWN;
387  getSize = false;
388  // Keep looking to see if we can determine it is infinite
389  }
390  else if (getSize) {
391  thisSize = thisSize * size;
392  // Give up if it gets too big
393  if (thisSize > 1000000) thisSize = 0;
394  if (thisSize == 0) {
395  getSize = false;
396  }
397  }
398  }
399 
400  if (card == CARD_FINITE) {
401 
402  if (enumerate) {
403  // TODO: enumerate functions? maybe at least n == 0
404  e = Expr();
405  }
406 
407  if (computeSize) {
408  n = thisSize;
409  }
410 
411  }
412 
413  return card;
414 }
415 
416 
418 {
419  switch (e.getKind()) {
420  case LAMBDA: {
421  vector<Type> args;
422  const vector<Expr>& vars = e.getVars();
423  DebugAssert(vars.size() > 0,
424  "TheorySimulate::computeType("+e.toString()+")");
425  for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
426  i!=iend; ++i)
427  args.push_back((*i).getType());
428  e.setType(Type::funType(args, e.getBody().getType()));
429  break;
430  }
431  case APPLY: {
433  break;
434  }
435  case TRANS_CLOSURE: {
436  DebugAssert(e.isSymbol(), "Expected symbol");
437  Expr funExpr = resolveID(e.getName());
438  if (funExpr.isNull()) {
439  throw TypecheckException
440  ("Attempt to take transitive closure of unknown id: "
441  +e.getName());
442  }
443  Type funType = funExpr.getType();
444  if(!funType.isFunction()) {
445  throw TypecheckException
446  ("Attempt to take transitive closure of non-function:\n\n"
447  +funExpr.toString() + "\n\n which has type: "
448  +funType.toString());
449  }
450  if(funType.arity()!=3) {
451  throw TypecheckException
452  ("Attempt to take transitive closure of non-binary function:\n\n"
453  +funExpr.toString() + "\n\n which has type: "
454  +funType.toString());
455  }
456  if (!funType[2].isBool()) {
457  throw TypecheckException
458  ("Attempt to take transitive closure of function:\n\n"
459  +funExpr.toString() + "\n\n which does not return BOOLEAN");
460  }
461  e.setType(funType);
462  break;
463  }
464  default:
465  DebugAssert(false,"Unexpected type: "+e.toString());
466  break;
467  }
468 }
469 
470 
472  const Expr& e = t.getExpr();
473  switch(e.getKind()) {
474  case ARROW: {
475  DebugAssert(e.arity() > 0, "Expected non-empty ARROW");
476  vector<Expr> kids;
477  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
478  kids.push_back(getBaseType(Type(*i)).getExpr());
479  }
480  return Type(Expr(e.getOp(), kids));
481  }
482  case TYPEDECL: return t;
483  default:
484  DebugAssert(false,
485  "TheoryUF::computeBaseType("+t.toString()+")");
486  return t;
487  }
488 }
489 
490 
491 void TheoryUF::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
493  iend=d_funApplications.end(); i!=iend; ++i) {
494  if((*i).isApply() && (*i).getOp().getExpr() == e) {
495  // Add both the function application
496  // getModelTerm(*i, v);
497  v.push_back(*i);
498  // and the arguments to the model terms. Reason: the argument
499  // to the function better be a concrete value, and it might not
500  // necessarily be in the current list of model terms.
501  for(Expr::iterator j=(*i).begin(), jend=(*i).end(); j!=jend; ++j)
502  // getModelTerm(*j, v);
503  v.push_back(*j);
504  }
505  }
506 }
507 
508 
509 void TheoryUF::computeModel(const Expr& e, std::vector<Expr>& vars) {
510  // Repeat the same search for applications of e as in
511  // computeModelTerm(), but this time get the concrete values of the
512  // arguments, and return the applications of e to concrete values in
513  // vars.
514 
515  // We'll assign 'e' a value later.
516  vars.push_back(e);
517  // Map of f(c) to val for concrete values of c and val
518  ExprHashMap<Expr> appls;
520  iend=d_funApplications.end(); i!=iend; ++i) {
521  if((*i).isApply() && (*i).getOp().getExpr() == e) {
522  // Update all arguments with concrete values
523  vector<Theorem> thms;
524  vector<unsigned> changed;
525  for(int j=0; j<(*i).arity(); ++j) {
526  Theorem asst(getModelValue((*i)[j]));
527  if(asst.getLHS()!=asst.getRHS()) {
528  thms.push_back(asst);
529  changed.push_back(j);
530  }
531  }
532  Expr var;
533  if(changed.size()>0) {
534  // Arguments changed. Compute the new application, and assign
535  // it a concrete value
536  Theorem subst = substitutivityRule(*i, changed, thms);
538  var = subst.getRHS();
539  } else
540  var = *i;
541  if(d_applicationsInModel) vars.push_back(var);
542  // Record it in the map
543  appls[var] = getModelValue(var).getRHS();
544  }
545  }
546  // Create a LAMBDA expression for e
547  if(appls.size()==0) { // Leave it fully uninterpreted
549  } else {
550  // Bound vars
551  vector<Expr> args;
552  Type tp(e.getType());
553  static unsigned count(0);
554  DebugAssert(tp.isFunction(), "TheoryUF::computeModel("+e.toString()
555  +" : "+tp.toString()+")");
556  for(int i=0, iend=tp.arity()-1; i<iend; ++i) {
557  string str = "uf_"+int2string(count);
558  Expr v = getEM()->newBoundVarExpr(str, int2string(count++));
559  v.setType(tp[i]);
560  args.push_back(v);
561  }
562  DebugAssert(args.size()>0, "TheoryUF::computeModel()");
563  ExprHashMap<Expr>::iterator i=appls.begin(), iend=appls.end();
564  DebugAssert(i!=iend, "TheoryUF::computeModel(): empty appls hash");
565  // Use one of the concrete values as a default
566  Expr res((*i).second); ++i;
567  for(; i!=iend; ++i) {
568  // Optimization: if the current value is the same as that of the
569  // next application, skip this case; i.e. keep 'res' instead of
570  // building ite(cond, res, res).
571  if((*i).second == res) continue;
572 
573  // Create an ITE condition
574  Expr cond;
575  vector<Expr> eqs;
576  for(int j=0, jend=args.size(); j<jend; ++j)
577  eqs.push_back(args[j].eqExpr((*i).first[j]));
578  if(eqs.size()==1)
579  cond = eqs[0];
580  else
581  cond = andExpr(eqs);
582  // Create an ITE
583  res = cond.iteExpr((*i).second, res);
584  }
585  res = lambdaExpr(args, res);
586  assignValue(e, res);
587  }
588 }
589 
590 
592 {
593  switch (e.getKind()) {
594  case APPLY: {
595  // Compute subtype predicates from the domain types applied to
596  // the corresponding arguments. That is, if f: (T0,..,Tn)->T,
597  // and e = f(e0,...,en), then the TCC is
598  //
599  // pred_T0(e0) & ... & pred_Tn(en) & TCC(e),
600  //
601  // where the last TCC(e) is the conjunction of TCCs for the
602  // arguments, which ensures that all arguments are defined.
603  //
604  // If the operator is a lambda-expression, compute the TCC for
605  // the beta-reduced expression. We do this in a somewhat sneaky
606  // but an efficient way: first, compute TCC of the op.body
607  // (which depends on the bound vars), then wrap that into
608  // lambda, and apply it to the arguments:
609  //
610  // (LAMBDA(x0...xn): TCC(op.body)) (e0 ... en)
611  //
612  // The reason it is more efficient is that TCC(op.body) is cached,
613  // and doesn't change with the arguments.
614 
615  vector<Expr> preds;
616  preds.push_back(Theory::computeTCC(e));
617  DebugAssert(e.isApply(), "Should be application");
618  Expr op(e.getOp().getExpr());
619  Type funType(op.getType());
620  DebugAssert(funType.isFunction() || funType.isBool(),
621  "TheoryUF::computeTCC(): funType = "
622  +funType.toString());
623  if(funType.isFunction()) {
624  DebugAssert(funType.arity() == e.arity()+1,
625  "TheoryUF::computeTCC(): funType = "
626  +funType.toString()+"\n e = "+e.toString());
627  for(int i=0, iend=e.arity(); i<iend; ++i) {
628  // Optimization: if the type of the formal argument is
629  // exactly the same as the type of the actual, then skip the
630  // type predicate for that argument
631  if(funType[i] != e[i].getType())
632  preds.push_back(getTypePred(funType[i], e[i]));
633  }
634  }
635  // Now strip off all the LETDECL
636  while(op.getKind()==LETDECL) op = op[1];
637  // and add a TCC for the lambda-expression
638  if(op.isLambda()) {
639  preds.push_back(Expr(lambdaExpr(op.getVars(),
640  getTCC(op.getBody())).mkOp(),
641  e.getKids()));
642  }
643  return rewriteAnd(andExpr(preds)).getRHS();
644  }
645  case LAMBDA:
646  return trueExpr();
647  default:
648  DebugAssert(false,"Unexpected type: "+e.toString());
649  return trueExpr();
650  }
651 }
652 
653 ///////////////////////////////////////////////////////////////////////////////
654 // Pretty-printing //
655 ///////////////////////////////////////////////////////////////////////////////
656 
658  DebugAssert( os.lang() == SMTLIB_LANG || os.lang() == SMTLIB_V2_LANG, "Illegal state in printSmtLibShared");
659  switch( e.getKind() ) {
660  case TYPEDECL:
661  if( e.arity() == 1 && e[0].isString() ) {
662  os << e[0].getString();
663  break;
664  }
665  // If it's straight from the parser, we may have several type
666  // names in one declaration. Print these in LISP format.
667  // Otherwise, print the name of the type.
668  throw SmtlibException("TheoryUF::print: TYPEDECL not supported");
669  // if(e.arity() != 1) e.print(os);
670  // else if(e[0].isString()) os << e[0].getString();
671  // else e[0].print(os);
672  break;
673  case APPLY:
674  if( e.arity() == 0 )
675  os << e.getOp().getExpr();
676  else {
677  os << "(" << push << e.getOp().getExpr();
678  for( int i = 0, iend = e.arity(); i < iend; ++i )
679  os << space << e[i];
680  if( e.getOpKind() == TRANS_CLOSURE ) {
681  os << space << ":transclose";
682  }
683  os << push << ")";
684  }
685  break;
686  case TRANS_CLOSURE:
687  os << e.getName();
688  break;
689  case UFUNC:
690  DebugAssert(e.isSymbol(), "Expected symbol");
691  os << theoryCore()->getTranslator()->fixConstName(e.getName());
692  break;
693  default: {
694  DebugAssert(false, "TheoryUF::print: SMTLIB_LANG: Unexpected expression: "
695  +getEM()->getKindName(e.getKind()));
696  }
697  }
698 }
699 
701  switch(os.lang()) {
702  case SIMPLIFY_LANG:
703  switch(e.getKind()) {
704  case OLD_ARROW:
705  case ARROW:
706  os<<"ERROR:ARROW:unsupported in Simplify\n";
707  break;
708  case LAMBDA: {
709  os<<"ERROR:LAMBDA:unsupported in Simplify\n";
710  break;
711  }
712  case TRANS_CLOSURE:
713  os<<"ERROR:TRANS_CLOSURE:unsupported in Simplify\n";
714  break;
715  case TYPEDECL:
716  os<<"ERROR:TYPEDECL:unsupported in Simplify\n";
717  break;
718  case UFUNC:
719  case APPLY:
720  if(e.isApply()) os << "(" << e.getOp().getExpr()<<" ";
721  if(e.arity() > 0) {
722  bool first(true);
723  for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
724  if(first) first = false;
725  else os << " " ;
726  os << *i;
727  }
728  os << ")";
729  }
730  break;
731  default: {
732  DebugAssert(false, "TheoryUF::print: Unexpected expression: "
733  +getEM()->getKindName(e.getKind()));
734  }
735  }
736  break; // end of case SIMPLIFY_LANGUAGE
737 
738  case TPTP_LANG:
739  switch(e.getKind()) {
740  case OLD_ARROW:
741  case ARROW:
742  if(e.arity() < 2) e.printAST(os);
743  else {
744  os << "(" << push;
745  bool first(true);
746  for(int i=0, iend=e.arity()-1; i<iend; ++i) {
747  if(first) first=false;
748  else os << " * " ;
749  os << e[i];
750  }
751  os << ")" ;
752  os << " > " << e[e.arity()-1];
753  }
754  break;
755 
756  case LAMBDA: {
757  os<<"ERROR:LAMBDA:unsupported in TPTP\n";
758  break;
759  }
760  case TRANS_CLOSURE:
761  os<<"ERROR:TRANS_CLOSURE:unsupported in TPTP\n";
762  break;
763  case TYPEDECL:
764  if(e.arity() != 1) e.printAST(os);
765  else os << e[0].getString();
766  break;
767 
768  case UFUNC:
769  DebugAssert(e.isSymbol(), "Expected symbol");
770  os << to_lower(e.getName());
771  break;
772 
773  case APPLY:
774  if(e.isApply()) os <<e.getOpExpr()<<"(";
775  if(e.arity() > 0) {
776  bool first(true);
777  for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
778  if(first) first = false;
779  else os << "," ;
780  os << *i;
781  }
782  os << ")";
783  }
784  break;
785  default: {
786  DebugAssert(false, "TheoryUF::print: Unexpected expression: "
787  +getEM()->getKindName(e.getKind()));
788  }
789  }
790  break; // end of case TPTP_LANGUAGE
791 
792 
793  case PRESENTATION_LANG:
794  switch(e.getKind()) {
795  case OLD_ARROW:
796  case ARROW:
797  if(e.arity() < 2) e.printAST(os);
798  else {
799  if(e.arity() == 2)
800  os << e[0];
801  else {
802  os << "(" << push;
803  bool first(true);
804  for(int i=0, iend=e.arity()-1; i<iend; ++i) {
805  if(first) first=false;
806  else os << "," << space;
807  os << e[i];
808  }
809  os << push << ")" << pop << pop;
810  }
811  os << space << "->" << space << e[e.arity()-1];
812  }
813  break;
814  case TYPEDECL:
815  // If it's straight from the parser, we may have several type
816  // names in one declaration. Print these in LISP format.
817  // Otherwise, print the name of the type.
818  if(e.arity() != 1) e.printAST(os);
819  else os << e[0].getString();
820  break;
821  case LAMBDA: {
822  DebugAssert(e.isLambda(), "Expected Lambda");
823  os << "(" << push << "LAMBDA" << space << push;
824  const vector<Expr>& vars = e.getVars();
825  bool first(true);
826  os << "(" << push;
827  for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
828  i!=iend; ++i) {
829  if(first) first = false;
830  else os << push << "," << pop << space;
831  os << *i;
832  // The lambda Expr may be in a raw parsed form, in which case
833  // the type is not assigned yet
834  if(i->isVar())
835  os << ":" << space << pushdag << (*i).getType() << popdag;
836  }
837  os << push << "): " << pushdag << push
838  << e.getBody() << push << ")";
839  break;
840  }
841  case APPLY:
842  os << e.getOpExpr();
843  if(e.arity() > 0) {
844  os << "(" << push;
845  bool first(true);
846  for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
847  if(first) first = false;
848  else os << "," << space;
849  os << *i;
850  }
851  os << push << ")";
852  }
853  break;
854  case TRANS_CLOSURE:
855  DebugAssert(e.isSymbol(), "Expected symbol");
856  os << e.getName() << "*";
857  break;
858  case UFUNC:
859  DebugAssert(e.isSymbol(), "Expected symbol");
860  os << e.getName();
861  break;
862  default: {
863  DebugAssert(false, "TheoryUF::print: Unexpected expression: "
864  +getEM()->getKindName(e.getKind()));
865  }
866  }
867  break; // end of case PRESENTATION_LANGUAGE
868  case SMTLIB_LANG:
869  switch(e.getKind()) {
870  case OLD_ARROW:
871  case ARROW: {
872  if(e.arity() < 2) {
873  throw SmtlibException("TheoryUF::print: Expected 2 or more arguments to ARROW");
874  // e.print(os);
875  }
876  d_theoryUsed = true;
877  os << push;
878  bool oldDagFlag = os.dagFlag(false);
879  int iend = e.arity();
880  if (e[iend-1].getKind() == BOOLEAN) --iend;
881  for(int i=0; i<iend; ++i) {
882  if (i != 0) os << space;
883  os << e[i];
884  }
885  os.dagFlag(oldDagFlag);
886  break;
887  }
888  default:
889  printSmtLibShared(os,e);
890  }
891  break; // End of SMT_LIB
892  case SMTLIB_V2_LANG:
893  switch(e.getKind()) {
894  case OLD_ARROW:
895  case ARROW: {
896  /* Prints out a function type (A,B,C) -> D as "(A B C) D" */
897  if(e.arity() < 2) {
898  throw SmtlibException("TheoryUF::print: Expected 2 or more arguments to ARROW");
899  // e.print(os);
900  }
901  d_theoryUsed = true;
902  bool oldDagFlag = os.dagFlag(false);
903  os << push << "(";
904  for( int i = 0; i < e.arity() - 1; ++i ) {
905  if( i != 0 ) {
906  os << space;
907  }
908  os << e[i];
909  }
910  os << ")" << space << e[e.arity() - 1] << pop ;
911  os.dagFlag(oldDagFlag);
912  break;
913  }
914  default:
915  printSmtLibShared(os,e);
916  }
917  break; // End of SMT-LIB v2
918  case LISP_LANG:
919  switch(e.getKind()) {
920  case OLD_ARROW:
921  case ARROW:
922  if(e.arity() < 2) e.printAST(os);
923  os << "(" << push << "ARROW";
924  for(int i=0, iend=e.arity(); i<iend; ++i)
925  os << space << e[i];
926  os << push << ")";
927  break;
928  case TRANS_CLOSURE:
929  e.printAST(os);
930  break;
931  case TYPEDECL:
932  // If it's straight from the parser, we may have several type
933  // names in one declaration. Print these in LISP format.
934  // Otherwise, print the name of the type.
935  if(e.arity() != 1) e.printAST(os);
936  else if(e[0].isString()) os << e[0].getString();
937  else e[0].print(os);
938  break;
939  case LAMBDA: {
940  DebugAssert(e.isLambda(), "Expected LAMBDA");
941  os << "(" << push << "LAMBDA" << space;
942  const vector<Expr>& vars = e.getVars();
943  bool first(true);
944  os << "(" << push;
945  for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
946  i!=iend; ++i) {
947  if(first) first = false;
948  else os << space;
949  os << "(" << push << *i;
950  // The expression may be in a raw parsed form, in which case
951  // the type is not assigned yet
952  if(i->isVar())
953  os << space << pushdag << (*i).getType() << popdag;
954  os << push << ")" << pop << pop;
955  }
956  os << push << ")" << pop << pop << pushdag
957  << e.getBody() << push << ")";
958  break;
959  }
960  case APPLY:
961  DebugAssert(e.isApply(), "Expected Apply");
962  if (e.arity() == 0) os << e.getOp().getExpr();
963  else {
964  os << "(" << push << e.getOp().getExpr();
965  for (int i=0, iend=e.arity(); i<iend; ++i)
966  os << space << e[i];
967  os << push << ")";
968  }
969  break;
970  default: {
971  DebugAssert(false, "TheoryUF::print: Unexpected expression: "
972  +getEM()->getKindName(e.getKind()));
973  }
974  }
975  break; // End of LISP_LANG
976  case SPASS_LANG:
977  switch(e.getKind()) {
978  case UFUNC:
979  os << e.getName();
980  break;
981  case APPLY:
982  os << push << e.getOp().getExpr();
983  if(e.arity() > 0) {
984  os << "(" << e[0];
985  for (int i=1, iend=e.arity(); i<iend; ++i)
986  os << "," << space << e[i];
987  os << ")";
988  }
989  os << push;
990  break;
991  case OLD_ARROW:
992  case ARROW:
993  case TRANS_CLOSURE:
994  case TYPEDECL:
995  case LAMBDA:
996  default:
997  throw SmtlibException("TheoryUF::print: Unexpected expression for SPASS_LANG: "
998  +getEM()->getKindName(e.getKind()));
999  }
1000  break;
1001  default:
1002  // Print the top node in the default format, continue with
1003  // pretty-printing for children.
1004  e.printAST(os);
1005  break;
1006  }
1007  return os;
1008 }
1009 
1010 //////////////////////////////////////////////////////////////////////////////
1011 //parseExprOp:
1012 //translating special Exprs to regular EXPR??
1013 ///////////////////////////////////////////////////////////////////////////////
1014 Expr
1016  // If the expression is not a list, it must have been already
1017  // parsed, so just return it as is.
1018  if(RAW_LIST != e.getKind()) return e;
1019 
1020  DebugAssert(e.arity() > 0,
1021  "TheoryUF::parseExprOp:\n e = "+e.toString());
1022 
1023  if (e[0].getKind() == RAW_LIST) {
1024  if(e.arity() < 2)
1025  throw ParserException("Bad function application: "+e.toString());
1026  Expr::iterator i=e.begin(), iend=e.end();
1027  Expr op(parseExpr(*i)); ++i;
1028  vector<Expr> args;
1029  for(; i!=iend; ++i) args.push_back(parseExpr(*i));
1030  return Expr(op.mkOp(), args);
1031  }
1032 
1033  DebugAssert(e[0].getKind() == ID || e[0][0].getKind() == ID,
1034  "Expected identifier");
1035  int kind = e[0].getKind();
1036  if (kind == ID) kind = getEM()->getKind(e[0][0].getString());
1037  switch(kind) {
1038  case OLD_ARROW: {
1039  if (!theoryCore()->getFlags()["old-func-syntax"].getBool()) {
1040  throw ParserException("You seem to be using the old syntax for function types.\n"
1041  "Please convert to the new syntax or run with +old-func-syntax");
1042  }
1043  DebugAssert(e.arity()==3,"Expected arity 3 in OLD_ARROW");
1044  Expr arg = parseExpr(e[1]);
1045  vector<Expr> k;
1046  if (arg.getOpKind() == TUPLE_TYPE) {
1047  Expr::iterator i = arg.begin(), iend=arg.end();
1048  for (; i != iend; ++i) {
1049  k.push_back(*i);
1050  }
1051  }
1052  else k.push_back(arg);
1053  k.push_back(parseExpr(e[2]));
1054  return Expr(ARROW, k);
1055  }
1056  case ARROW:
1057  case TYPEDECL: {
1058  vector<Expr> k;
1059  Expr::iterator i = e.begin(), iend=e.end();
1060  // Skip first element of the vector of kids in 'e'.
1061  // The first element is the operator.
1062  ++i;
1063  // Parse the kids of e and push them into the vector 'k'
1064  for(; i!=iend; ++i)
1065  k.push_back(parseExpr(*i));
1066  return Expr(kind, k, e.getEM());
1067  break;
1068  }
1069  case TRANS_CLOSURE: {
1070  if(e.arity() != 4)
1071  throw ParserException("Wrong number of arguments to "
1072  "TRANS_CLOSURE expression\n"
1073  " (expected 3 arguments): "+e.toString());
1074  const string& name = e[1][0].getString();
1075  Expr funExpr = resolveID(name);
1076  if (funExpr.isNull())
1077  throw ParserException("Attempt to take transitive closure of unknown "
1078  "predicate"+name);
1079  return transClosureExpr(name, parseExpr(e[2]), parseExpr(e[3]));
1080  }
1081  case LAMBDA: { // (LAMBDA ((v1 ... vn tp1) ...) body)
1082  if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0))
1083  throw ParserException("Bad LAMBDA expression: "+e.toString());
1084  // Iterate through the groups of bound variables
1085  vector<pair<string,Type> > vars; // temporary stack of bound variables
1086  for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
1087  if(i->getKind() != RAW_LIST || i->arity() < 2)
1088  throw ParserException("Bad variable declaration block in LAMBDA "
1089  "expression: "+i->toString()+
1090  "\n e = "+e.toString());
1091  // Iterate through individual bound vars in the group. The
1092  // last element is the type, which we have to rebuild and
1093  // parse, since it is used in the creation of bound variables.
1094  Type tp(parseExpr((*i)[i->arity()-1]));
1095  for(int j=0, jend=i->arity()-1; j<jend; ++j) {
1096  if((*i)[j].getKind() != ID)
1097  throw ParserException("Bad variable declaration in LAMBDA"
1098  " expression: "+(*i)[j].toString()+
1099  "\n e = "+e.toString());
1100  vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
1101  }
1102  }
1103  // Create all the bound vars and save them in a vector
1104  vector<Expr> boundVars;
1105  for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
1106  i!=iend; ++i)
1107  boundVars.push_back(addBoundVar(i->first, i->second));
1108  // Rebuild the body
1109  Expr body(parseExpr(e[2]));
1110  // Build the resulting Expr as (LAMBDA (vars) body)
1111  return lambdaExpr(boundVars, body);
1112  break;
1113  }
1114  case RAW_LIST: // Lambda application
1115  default: { // Application of an uninterpreted function
1116  if(e.arity() < 2)
1117  throw ParserException("Bad function application: "+e.toString());
1118  Expr::iterator i=e.begin(), iend=e.end();
1119  Expr op(parseExpr(*i)); ++i;
1120  vector<Expr> args;
1121  for(; i!=iend; ++i) args.push_back(parseExpr(*i));
1122  return Expr(op.mkOp(), args);
1123  }
1124  }
1125  return e;
1126 }
1127 
1128 
1129 Expr TheoryUF::lambdaExpr(const vector<Expr>& vars, const Expr& body) {
1130  return getEM()->newClosureExpr(LAMBDA, vars, body);
1131 }
1132 
1133 
1134 Expr TheoryUF::transClosureExpr(const std::string& name, const Expr& e1,
1135  const Expr& e2) {
1136  return Expr(getEM()->newSymbolExpr(name, TRANS_CLOSURE).mkOp(), e1, e2);
1137 }
1138 
1140  d_sharedTermsMap[e] = true;
1141 }
virtual Theorem simplify(const Expr &e)
Simplify a term e and return a Theorem(e==e')
Definition: theory.cpp:119
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
Definition: theory.cpp:519
Definition: kinds.h:48
int arity() const
Definition: expr.h:1201
ExprStream & pop(ExprStream &os)
Restore the indentation.
bool isNull() const
Definition: expr.h:1223
for output in SPASS format
Definition: lang.h:49
iterator begin()
Definition: expr_map.h:325
const Expr & getExpr() const
Definition: expr_op.h:84
iterator begin() const
Begin iterator.
Definition: expr.h:1211
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
Definition: theory_uf.cpp:471
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
void setRewriteNormal() const
Definition: expr.h:1457
const std::string fixConstName(const std::string &s)
Data structure of expressions in CVC3.
Definition: expr.h:133
Cardinality card() const
Return cardinality of type.
Definition: type.h:64
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
Definition: theory.cpp:148
ExprMap< CDList< Theorem > * > appearsFirstMap
Definition: theory_uf.h:55
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
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Definition: expr.h:961
An exception thrown by the parser.
static Type funType(const std::vector< Type > &typeDom, const Type &typeRan)
Definition: expr.cpp:641
bool isTrue() const
Definition: expr.h:356
void setupCC(const Expr &e)
Setup a term for congruence closure (must have sig and rep attributes)
Definition: theory.cpp:459
ExprMap< CDList< Theorem > * > appearsSecondMap
Definition: theory_uf.h:56
void addToNotify(Theory *i, const Expr &e) const
Add (e,i) to the notify list of this expression.
Definition: expr.cpp:517
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Definition: theory_uf.cpp:1139
An exception to be thrown at typecheck error.
Definition: kinds.h:227
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Definition: theory_uf.cpp:236
virtual Theorem applyLambda(const Expr &e)=0
Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
CDO< size_t > d_sharedIdx2
Definition: theory_uf.h:68
Expr resolveID(const std::string &name)
Resolve an identifier, for use in parseExprOp()
Definition: theory.cpp:887
for output in TPTP format
Definition: lang.h:46
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory_uf.cpp:591
bool computeTransClosure() const
Definition: expr.h:1334
MS C++ specific settings.
Definition: type.h:42
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
virtual Theorem relToClosure(const Theorem &rel)=0
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Definition: theory_uf.cpp:700
STL namespace.
Lisp-like format for automatically generated specs.
Definition: lang.h:36
Definition: kinds.h:66
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
CDMap< Expr, bool > d_sharedTermsMap
The set of all shared terms.
Definition: theory_uf.h:70
bool isBool() const
Definition: type.h:60
virtual Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
Definition: theory.h:252
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Definition: theory_uf.cpp:1015
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Translator * getTranslator() const
Definition: theory_core.h:354
Definition: kinds.h:51
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
Definition: theory.h:719
#define DebugAssert(cond, str)
Definition: debug.h:408
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Definition: expr.h:1021
Definition: kinds.h:56
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Definition: expr_manager.h:506
void setRep(const Theorem &e) const
Definition: expr.h:1589
void setSig(const Theorem &e) const
Definition: expr.h:1578
CDList< Expr > d_funApplications
Backtracking list of function applications.
Definition: theory_uf.h:64
T & push_back(const T &data, int scope=-1)
Definition: cdlist.h:66
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
const bool & d_applicationsInModel
Flag to include function applications to the concrete model.
Definition: theory_uf.h:51
CDO< size_t > d_funApplicationsIdx
Pointer to the last unprocessed element (for lambda expansions)
Definition: theory_uf.h:66
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Definition: theory.cpp:203
ExprStream & pushdag(ExprStream &os)
Context * getCurrentContext()
Definition: context.h:406
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Definition: expr.h:1191
size_t size() const
Definition: expr_map.h:306
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Definition: expr_manager.h:484
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
const_iterator end() const
Definition: cdlist.h:91
CommonProofRules * getCommonRules()
Get a pointer to common proof rules.
Definition: theory.h:96
void computeType(const Expr &e)
Compute and store the type of e.
Definition: theory_uf.cpp:417
Definition: kinds.h:44
bool d_theoryUsed
Definition: theory.h:79
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory.cpp:81
int arity() const
Definition: type.h:55
Identifier is (ID (STRING_EXPR "name"))
Definition: kinds.h:46
bool isString() const
Definition: expr.h:1006
Theorem rewriteCC(const Expr &e)
Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
Definition: theory.cpp:512
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
void checkType(const Expr &e)
Check that e is a valid Type expr.
Definition: theory_uf.cpp:337
virtual void computeType(const Expr &e)
Compute and store the type of e.
Definition: theory.h:263
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
Definition: expr.cpp:362
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
const Theorem & getSig() const
Definition: expr.h:1560
const Theorem & getRep() const
Definition: expr.h:1569
ExprMap< TCMapPair * > d_transClosureMap
Definition: theory_uf.h:59
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
Definition: kinds.h:88
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Definition: theory_uf.cpp:491
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
std::string int2string(int n)
Definition: cvc_util.h:46
const Expr & getRHS() const
Definition: theorem.cpp:246
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
Definition: theory.h:503
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Definition: theory.cpp:541
CDO< size_t > d_sharedIdx1
The pointers to the last unprocessed shared pair.
Definition: theory_uf.h:68
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
#define IF_DEBUG(code)
Definition: debug.h:406
const Expr & trueExpr()
Return TRUE Expr.
Definition: theory.h:582
Expr addBoundVar(const std::string &name, const Type &type)
Create and add a new bound variable to the stack, for parseExprOp().
Definition: theory.cpp:709
Expr lambdaExpr(const std::vector< Expr > &vars, const Expr &body)
Create a new LAMBDA-abstraction.
Definition: theory_uf.cpp:1129
unsigned size() const
Definition: cdlist.h:64
Expr getExpr() const
Definition: theorem.cpp:230
bool isNull() const
Definition: theorem.h:164
bool isApply() const
Definition: expr.h:1014
Expr transClosureExpr(const std::string &name, const Expr &e1, const Expr &e2)
Create a transitive closure expression.
Definition: theory_uf.cpp:1134
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
Definition: kinds.h:90
ExprStream & popdag(ExprStream &os)
const std::string & getName() const
Definition: expr.h:1050
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Definition: theory_uf.cpp:509
ContextManager * getCM() const
Definition: theory_core.h:348
Theorem updateHelper(const Expr &e)
Update the children of the term e.
Definition: theory.cpp:417
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
Definition: theory_uf.cpp:368
Abstract interface for uninterpreted function/predicate proof rules.
struct CVC3::TheoryUF::TCMapPair TCMapPair
UFProofRules * createProofRules()
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 assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Definition: theory_uf.cpp:79
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Definition: theory_uf.cpp:257
bool isSymbol() const
Definition: expr.h:1018
std::string to_lower(const std::string &src)
Definition: cvc_util.h:38
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
An exception to be thrown by the smtlib translator.
An exception to be thrown by the smtlib translator.
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Definition: expr.h:1062
SMT-LIB format.
Definition: lang.h:34
Op mkOp() const
Make the expr into an operator.
Definition: expr.h:1178
const Expr & getLHS() const
Definition: theorem.cpp:240
Expr getTCC(const Expr &e)
Compute the TCC of e, or the subtyping predicate, if e is a type.
Definition: theory.cpp:367
const_iterator begin() const
Definition: cdlist.h:88
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
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Definition: theory_uf.cpp:156
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Definition: theory.cpp:252
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
bool isLambda() const
Definition: expr.h:1011
InputLanguage lang() const
Get the current output language.
Definition: expr_stream.h:165
bool isFunction() const
Definition: type.h:62
void printSmtLibShared(ExprStream &os, const Expr &e)
Definition: theory_uf.cpp:657
Definition: kinds.h:229
virtual Theorem relTrans(const Theorem &t1, const Theorem &t2)=0
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
UFProofRules * d_rules
Definition: theory_uf.h:49
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Definition: theory_uf.cpp:211
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
Definition: theory.cpp:310
for output into Simplify format
Definition: lang.h:43
bool dagFlag(bool flag=true)
Set the DAG flag (return previous value)
Definition: expr_stream.h:175
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
Nice SAL-like language for manually written specs.
Definition: lang.h:32
virtual Theorem iffTrueElim(const Theorem &e)=0
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
iterator end()
Definition: expr_map.h:326
iterator end() const
End iterator.
Definition: expr.h:1217