CVC3  2.4.1
expr.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file expr.cpp
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Thu Dec 5 11:35:55 2002
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 <algorithm>
23 
24 
25 #include "expr.h"
26 #include "pretty_printer.h"
27 #include "expr_stream.h"
28 #include "notifylist.h"
29 #include "exception.h"
30 
31 
32 using namespace std;
33 
34 
35 namespace CVC3 {
36 
37 
38 Expr Expr::s_null;
39 
40 ///////////////////////////////////////////////////////////////////////
41 // Class Expr methods //
42 ///////////////////////////////////////////////////////////////////////
43 
44 vector<vector<Expr> > Expr::substTriggers(const ExprHashMap<Expr> & subst,
45  ExprHashMap<Expr> & visited) const {
46  /* Do the substitution in triggers */
47  vector<vector<Expr> > vvOldTriggers(getTriggers());
48  vector<vector<Expr> > vvNewTriggers;
49  vector<vector<Expr> >::const_iterator i, iEnd;
50  for( i = vvOldTriggers.begin(), iEnd = vvOldTriggers.end(); i != iEnd; ++i ) {
51  vector<Expr> vOldTriggers(*i);
52  vector<Expr> vNewTriggers;
53  vector<Expr>::const_iterator j, jEnd;
54  for( j = vOldTriggers.begin(), jEnd = vOldTriggers.end(); j != jEnd; ++j ) {
55  vNewTriggers.push_back((*j).recursiveSubst(subst, visited));
56  }
57  vvNewTriggers.push_back(vNewTriggers);
58  }
59 
60  return vvNewTriggers;
61 }
62 
63 Expr Expr::recursiveSubst(const ExprHashMap<Expr>& subst,
64  ExprHashMap<Expr>& visited) const {
65  // Check the cache.
66  // INVARIANT: visited contains all the flagged expressions, and only those
67  if(getFlag()) return visited[*this];
68 
69  ExprIndex minIndex = 0;
70  for(ExprHashMap<Expr>::const_iterator i = subst.begin(),iend=subst.end();i!=iend;++i) {
71  if(minIndex > (i->first).getIndex())
72  minIndex = (i->first).getIndex();
73  }
74 
75  Expr replaced;
76 
77  if(isClosure()) {
78  const vector<Expr> & vars = getVars();
79  vector<Expr> common; // Bound vars which occur in subst
80 
81  for(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end();
82  i!=iend; ++i) {
83  if(subst.count(*i) > 0) common.push_back(*i);
84  }
85 
86  if(common.size() > 0) {
87  IF_DEBUG(debugger.counter("substExpr: bound var clashes")++;)
88  // Reduced substitution (without the common vars)
89  ExprHashMap<Expr> newSubst(subst);
90  // Remove variables in "common" from the substitution
91  for(vector<Expr>::iterator i=common.begin(), iend=common.end();
92  i!=iend; ++i)
93  newSubst.erase(*i);
94 
95  // Clear all the caches (important!)
96  visited.clear();
97  clearFlags();
98  visited = newSubst;
99 
100  ExprHashMap<Expr>::iterator j = newSubst.begin();
101  for (; j != newSubst.end(); ++j) { // old vars bound in e
102  j->first.setFlag();
103  }
104 
105  vector<vector<Expr> > vvNewTriggers = substTriggers(newSubst,visited);
106 
107  replaced =
108  getEM()->newClosureExpr(getKind(), vars,
109  getBody().recursiveSubst(newSubst, visited),
110  vvNewTriggers);
111 
112  // Clear the flags again, as we restore the substitution
113  visited.clear();
114  clearFlags();
115  visited = subst;
116  // Restore the flags on the original substitutions
117  for (ExprHashMap<Expr>::const_iterator i = subst.begin(), iend=subst.end();
118  i != iend; ++i)
119  i->first.setFlag();
120  } else {
121  vector<vector<Expr> > vvNewTriggers = substTriggers(subst,visited);
122  replaced =
123  getEM()->newClosureExpr(getKind(), vars,
124  getBody().recursiveSubst(subst, visited),
125  vvNewTriggers);
126  }
127  } else { // Not a Closure
128  int changed=0;
129  vector<Expr> children;
130  for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i){
131  Expr repChild = *i;
132  if(repChild.getIndex() >= minIndex)
133  repChild = (*i).recursiveSubst(subst, visited);
134  if(repChild != *i)
135  changed++;
136  children.push_back(repChild);
137  }
138  Expr opExpr;
139  if (isApply()) {
140  opExpr = getOpExpr().recursiveSubst(subst, visited);
141  if (opExpr != getOpExpr()) ++changed;
142  }
143  if(changed > 0) {
144  Op op = opExpr.isNull() ? getOp() : opExpr.mkOp();
145  replaced = Expr(op, children);
146  }
147  else replaced = *this;
148  }
149  visited.insert(*this, replaced);
150  setFlag();
151  return replaced;
152 }
153 
154 
155 static bool subExprRec(const Expr& e1, const Expr& e2) {
156  if(e1 == e2) return true;
157  if(e2.getFlag()) return false;
158  // e1 is created after e2, so e1 cannot be a subexpr of e2
159  if(e1 > e2) return false;
160  e2.setFlag();
161  bool res(false);
162  for(Expr::iterator i=e2.begin(), iend=e2.end(); !res && i!=iend; ++i)
163  res = subExprRec(e1, *i);
164  return res;
165 }
166 
167 
168 bool
169 Expr::subExprOf(const Expr& e) const {
170  if(*this == e) return true;
171  // "this" is created after e, so it cannot be e's subexpression
172  if(*this > e) return false;
173  clearFlags();
174  return subExprRec(*this, e);
175 }
176 
177 
178 Expr Expr::substExpr(const vector<Expr>& oldTerms,
179  const vector<Expr>& newTerms) const
180 {
181  DebugAssert(oldTerms.size() == newTerms.size(), "substExpr: vectors"
182  "don't match in size");
183  // Catch the vacuous case
184  if(oldTerms.size() == 0) return *this;
185 
186  ExprHashMap<Expr> oldToNew(10);
187  clearFlags();
188  for(unsigned int i=0; i<oldTerms.size(); i++) {
189  oldToNew.insert(oldTerms[i], newTerms[i]);
190  oldTerms[i].setFlag();
191  }
192  // For cache, initialized by the substitution
193  ExprHashMap<Expr> visited(oldToNew);
194  return recursiveSubst(oldToNew, visited);
195 
196 }
197 
198 
199 Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const
200 {
201  // Catch the vacuous case
202  if(oldToNew.size() == 0) return *this;
203  // Rebuild the map: we'll be using it as a cache
204  ExprHashMap<Expr> visited(oldToNew);
205  clearFlags();
206  // Flag all the LHS expressions in oldToNew map. We'll be checking
207  // all flagged expressions (and only those) for substitution.
208  for(ExprHashMap<Expr>::const_iterator i=oldToNew.begin(), iend=oldToNew.end();
209  i!=iend; ++i) {
210  (*i).first.setFlag();
211  }
212  return recursiveSubst(oldToNew, visited);
213 }
214 
215 
216 
217 Expr Expr::substExprQuant(const vector<Expr>& oldTerms,
218  const vector<Expr>& newTerms) const
219 {
220  //let us disable this first yeting
221  // static ExprHashMap<Expr> substCache;
222  // Expr cacheIndex = Expr(RAW_LIST, *this, Expr(RAW_LIST, newTerms));
223 
224  // ExprHashMap<Expr>::iterator i = substCache.find(cacheIndex);
225  // if (i != substCache.end()){
226  // return i->second;
227  // }
228 
229  DebugAssert(oldTerms.size() == newTerms.size(), "substExpr: vectors"
230  "don't match in size");
231  // Catch the vacuous case
232 
233  if(oldTerms.size() == 0) return *this;
234 
235  ExprHashMap<Expr> oldToNew(oldTerms.size());
236 
237  // clearFlags();
238  for(unsigned int i=0; i<oldTerms.size(); i++) {
239  oldToNew.insert(oldTerms[i], newTerms[i]);
240  // oldTerms[i].setFlag();
241  }
242 
243  // For cache, initialized by the substitution
244  ExprHashMap<Expr> visited(oldToNew);
245  Expr returnExpr = recursiveQuantSubst(oldToNew, visited);;
246 
247  // substCache[cacheIndex] = returnExpr;
248  // cout<<"pushed " << cacheIndex << endl << "RET " << returnExpr << endl;
249 
250  return returnExpr;
251 
252 }
253 
254 Expr Expr::substExprQuant(const ExprHashMap<Expr>& oldToNew) const
255 {
256  ExprHashMap<Expr> visited(oldToNew);
257  return recursiveQuantSubst(oldToNew,visited);
258 }
259 
260 Expr Expr::recursiveQuantSubst(const ExprHashMap<Expr>& substMap,
261  ExprHashMap<Expr>& visited) const {
262  /* [chris 12/3/2009] It appears that visited is never used. */
263 
264  if (!containsBoundVar()){
265  // std::cout <<"no bound var " << *this << std::endl;
266  return *this;
267  }
268 
269  // Check the cache.
270  // INVARIANT: visited contains all the flagged expressions, and only those
271  // the above invariant is no longer true. yeting
272 
273  if(getKind() == BOUND_VAR ) {
274  ExprHashMap<Expr>::const_iterator find = substMap.find(*this);
275  if (find != substMap.end()) {
276  return find->second;
277  }
278 /*
279  // Expr ret = visited[*this];
280  const Expr ret = substMap[*this];
281  if (!ret.isNull()){
282  return ret;
283  }
284 */
285  }
286 
287  // if(getFlag()) return visited[*this];
288 
289  // why we need this.
290 // ExprIndex minIndex = 0;
291 // for(ExprHashMap<Expr>::iterator i = substMap.begin(),iend=substMap.end();i!=iend;++i) {
292 // if(minIndex > (i->first).getIndex())
293 // minIndex = (i->first).getIndex();
294 // }
295 
296  Expr replaced;
297 
298  if(isClosure()) {
299  // for safety, we can wrap the following lines by if debug
300 
301  const vector<Expr> & vars = getVars();
302 // vector<Expr> common; // Bound vars which occur in subst
303 
304 // for(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end();
305 // i!=iend; ++i) {
306 // if(substMap.count(*i) > 0) common.push_back(*i);
307 // }
308 
309 // if(common.size() > 0) {
310 // cout<<"error in quant subst" << endl;
311 // } else {
312 
313  /* Perform substition on the triggers */
314 
315  vector<vector<Expr> > vvNewTriggers = substTriggers(substMap,visited);
316  replaced =
317  getEM()->newClosureExpr(getKind(), vars,
318  getBody().recursiveQuantSubst(substMap, visited),
319  vvNewTriggers );
320 // }
321  } else { // Not a Closure
322  int changed=0;
323  vector<Expr> children;
324  for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i){
325  Expr repChild ;
326  repChild = (*i).recursiveQuantSubst(substMap, visited);
327  if(repChild != *i)
328  changed++;
329  children.push_back(repChild);
330  }
331  if(changed > 0)
332  replaced = Expr(getOp(), children);
333  else
334  replaced = *this;
335  }
336  // visited.insert(*this, replaced);
337  // setFlag();
338  return replaced;
339 }
340 
341 
342 
343 
344 string Expr::toString() const {
345  return toString(PRESENTATION_LANG);
346 // if(isNull()) return "Null";
347 // ostringstream ss;
348 // ss << (*this);
349 // return ss.str();
350 }
351 
352 string Expr::toString(InputLanguage lang) const {
353  if(isNull()) return "Null";
354  ostringstream ss;
355  ExprStream os(getEM());
356  os.lang(lang);
357  os.os(ss);
358  os << (*this);
359  return ss.str();
360 }
361 
362 void Expr::print(InputLanguage lang, bool dagify) const {
363  if(isNull()) {
364  cout << "Null" << endl; return;
365  }
366  ExprStream os(getEM());
367  os.lang(lang);
368  os.dagFlag(dagify);
369  os << *this << endl;
370 }
371 
372 
373 void Expr::pprint() const
374 {
375  if(isNull()) {
376  cout << "Null" << endl; return;
377  }
378  ExprStream os(getEM());
379  os << *this << endl;
380 }
381 
382 
383 void Expr::pprintnodag() const
384 {
385  if(isNull()) {
386  cout << "Null" << endl; return;
387  }
388  ExprStream os(getEM());
389  os.dagFlag(false);
390  os << *this << endl;
391 }
392 
393 
394 void Expr::printnodag() const
395 {
396  print(AST_LANG, false);
397 }
398 
399 
400 ExprStream& Expr::printAST(ExprStream& os) const {
401  if(isNull()) return os << "Null" << endl;
402  bool isLetDecl(getKind() == LETDECL);
403  os << "(" << push;
404  os << getEM()->getKindName(getKind());
405  if (isApply()) {
406  os << space << "{" << getOp().getExpr() << push << "}";
407  }
408  else if (isSymbol()) {
409  os << space << "{Symbol: " << getName() << "}";
410  }
411  else if (isClosure()) {
412  os << space << "{" << space << "(" << push;
413  const vector<Expr>& vars = getVars();
414  vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
415  if(i!=iend) { os << *i; ++i; }
416  for(; i!=iend; ++i) os << space << *i;
417  os << push << ") " << pop << pop;
418  os << getBody() << push << "}";
419  }
420  else {
421  switch(getKind()) {
422  case STRING_EXPR:
423  DebugAssert(isString(), "Expected String");
424  os << space << "{" << '"'+ getString() + '"' << "}";
425  break;
426  case SKOLEM_VAR:
427  getExistential();
428  os << space << "{SKOLEM_" << (int)getIndex() << "}";
429  break;
430  case RATIONAL_EXPR:
431  os << space << "{" << getRational() << "}";
432  break;
433  case UCONST:
434  DebugAssert(isVar(), "Expected Var");
435  os << space << "{" << getName() << "}";
436  break;
437  case BOUND_VAR:
438  DebugAssert(isVar(), "Expected Var");
439  os << space << "{"+getName()+"_"+getUid()+"}";
440  break;
441  case THEOREM_KIND:
442  DebugAssert(isTheorem(), "Expected Theorem");
443  os << space << "{Theorem: " << getTheorem().toString() << "}";
444  default: ; // Don't do anything
445  }
446  }
447 
448  for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) {
449  if(isLetDecl) os << nodag;
450  os << space << *i;
451  }
452  os << push << ")";
453  os.resetIndent();
454  return os;
455 }
456 
457 
458 ExprStream& Expr::print(ExprStream& os) const {
459  if(isNull()) return os << "Null" << endl;
460  if (isSymbol()) return os << getName();
461  switch(getKind()) {
462  case TRUE_EXPR: return os << "TRUE";
463  case FALSE_EXPR: return os << "FALSE";
464  case NULL_KIND: return os << "Null";
465  case STRING_EXPR: return os << '"'+ getString() + '"';
466  case RATIONAL_EXPR: return os << getRational();
467  case SKOLEM_VAR: return os << "SKOLEM_" << hash();
468  case UCONST: return os << getName();
469  case BOUND_VAR: return os << "(BOUND_VAR "+getName()+"_"+getUid()+")";
470  case RAW_LIST: {
471  os << "(" << push;
472  bool firstTime(true);
473  for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) {
474  if(firstTime) firstTime = false;
475  else os << space;
476  os << *i;
477  }
478  return os << push << ")";
479  }
480  case FORALL:
481  case EXISTS:
482  if(isQuantifier()) {
483  os << "(" << push << getEM()->getKindName(getKind())
484  << space << "(" << push;
485  const vector<Expr>& vars = getVars();
486  vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
487  if(i!=iend) { os << *i; ++i; }
488  for(; i!=iend; ++i) os << space << *i;
489  os << push << ") " << pop << pop;
490  return os << getBody() << push << ")";
491  }
492  // If not an internal representation of quantifiers, it'll be
493  // printed as "normal" Expr with a kind and children
494  case RESTART: return os << "RESTART " << (*this)[0] << ";";
495  default:
496  // os << "(" << push;
497  os << getEM()->getKindName(getKind());
498  // os << push << ")";
499  }
500  os.resetIndent();
501  return os;
502 }
503 
504 
505 //! Set initial indentation to n.
506 /*! The indentation will be reset to default unless the second
507  argument is true. This setting only takes effect when printing to
508  std::ostream. When printing to ExprStream, the indentation can be
509  set directly in the ExprStream. */
510 Expr& Expr::indent(int n, bool permanent) {
511  DebugAssert(!isNull(), "Expr::indent called on Null Expr");
512  getEM()->indent(n, permanent);
513  return *this;
514 }
515 
516 
517 void Expr::addToNotify(Theory* i, const Expr& e) const {
518  DebugAssert(!isNull(), "Expr::addToNotify() on Null expr");
519  if(getNotify() == NULL)
520  d_expr->d_notifyList = new NotifyList(getEM()->getCurrentContext());
521  getNotify()->add(i, e);
522 }
523 
524 
525 bool Expr::containsTermITE() const
526 {
527  if (getType().isBool()) {
528 
529  // We overload the isAtomicFlag to mean !containsTermITE for exprs
530  // of Boolean type
531  if (validIsAtomicFlag()) {
532  return !getIsAtomicFlag();
533  }
534 
535  for (int k = 0; k < arity(); ++k) {
536  if ((*this)[k].containsTermITE()) {
537  setIsAtomicFlag(false);
538  return true;
539  }
540  }
541 
542  setIsAtomicFlag(true);
543  return false;
544 
545  }
546  else return !isAtomic();
547 }
548 
549 
550 bool Expr::isAtomic() const
551 {
552  if (getType().isBool()) {
553  return isBoolConst();
554  }
555 
556  if (validIsAtomicFlag()) {
557  return getIsAtomicFlag();
558  }
559 
560  for (int k = 0; k < arity(); ++k) {
561  if (!(*this)[k].isAtomic()) {
562  setIsAtomicFlag(false);
563  return false;
564  }
565  }
566  setIsAtomicFlag(true);
567  return true;
568 }
569 
570 
571 bool Expr::isAtomicFormula() const
572 {
573  // TRACE("isAtomic", "isAtomicFormula(", *this, ") {");
574  if (!getType().isBool()) {
575  // TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }");
576  return false;
577  }
578  switch(getKind()) {
579  case FORALL: case EXISTS: case XOR:
580  case NOT: case AND: case OR: case ITE: case IFF: case IMPLIES:
581  // TRACE_MSG("isAtomic", "isAtomicFormula[connective] => false }");
582  return false;
583  }
584  for (Expr::iterator k = begin(), kend=end(); k != kend; ++k) {
585  if (!(*k).isAtomic()) {
586  // TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }");
587  return false;
588  }
589  }
590  // TRACE_MSG("isAtomic", "isAtomicFormula => true }");
591  return true;
592 }
593 
594 
595  // This is one of the most friequently called routines. Make it as
596  // efficient as possible.
597 int compare(const Expr& e1, const Expr& e2) {
598  // Quick equality check (operator== is implemented independently
599  // and more efficiently)
600  if(e1 == e2) return 0;
601 
602  if(e1.d_expr == NULL) return -1;
603  if(e2.d_expr == NULL) return 1;
604 
605  // Both are non-Null. Check for constant
606  bool e1c = e1.isConstant();
607  if (e1c != e2.isConstant()) {
608  return e1c ? -1 : 1;
609  }
610 
611  // Compare the indices
612  return (e1.getIndex() < e2.getIndex())? -1 : 1;
613 }
614 
615 
616 ///////////////////////////////////////////////////////////////////////
617 // Class Expr::iterator methods //
618 ///////////////////////////////////////////////////////////////////////
619 
620 
621 ostream& operator<<(ostream& os, const Expr& e) {
622  if(e.isNull()) return os << "Null";
623  ExprStream es(e.getEM());
624  es.os(os);
625  es << e;
626  e.getEM()->restoreIndent();
627  return os;
628 }
629 
630 
631 // Functions from class Type
632 
633 
634 Type::Type(Expr expr) : d_expr(expr)
635 {
636  if (expr.isNull()) return;
637  expr.getEM()->checkType(expr);
638 }
639 
640 
641 Type Type::funType(const std::vector<Type>& typeDom, const Type& typeRan) {
642  vector<Expr> tmp;
643  for(vector<Type>::const_iterator i=typeDom.begin(), iend=typeDom.end();
644  i!=iend; ++i)
645  tmp.push_back(i->getExpr());
646  tmp.push_back(typeRan.getExpr());
647  return Type(Expr(ARROW, tmp));
648 }
649 
650 
651 } // end of namespace CVC3