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));
57 vvNewTriggers.push_back(vNewTriggers);
67 if(getFlag())
return visited[*
this];
71 if(minIndex > (i->first).getIndex())
72 minIndex = (i->first).getIndex();
78 const vector<Expr> & vars = getVars();
81 for(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end();
83 if(subst.
count(*i) > 0) common.push_back(*i);
86 if(common.size() > 0) {
87 IF_DEBUG(debugger.counter(
"substExpr: bound var clashes")++;)
91 for(vector<Expr>::iterator i=common.begin(), iend=common.end();
101 for (; j != newSubst.end(); ++j) {
105 vector<vector<Expr> > vvNewTriggers = substTriggers(newSubst,visited);
108 getEM()->newClosureExpr(getKind(), vars,
109 getBody().recursiveSubst(newSubst, visited),
121 vector<vector<Expr> > vvNewTriggers = substTriggers(subst,visited);
123 getEM()->newClosureExpr(getKind(), vars,
124 getBody().recursiveSubst(subst, visited),
129 vector<Expr> children;
136 children.push_back(repChild);
141 if (opExpr != getOpExpr()) ++changed;
145 replaced =
Expr(op, children);
147 else replaced = *
this;
149 visited.
insert(*
this, replaced);
156 if(e1 == e2)
return true;
159 if(e1 > e2)
return false;
169 Expr::subExprOf(
const Expr& e)
const {
170 if(*
this == e)
return true;
172 if(*
this > e)
return false;
178 Expr Expr::substExpr(
const vector<Expr>& oldTerms,
179 const vector<Expr>& newTerms)
const
181 DebugAssert(oldTerms.size() == newTerms.size(),
"substExpr: vectors"
182 "don't match in size");
184 if(oldTerms.size() == 0)
return *
this;
188 for(
unsigned int i=0; i<oldTerms.size(); i++) {
189 oldToNew.
insert(oldTerms[i], newTerms[i]);
190 oldTerms[i].setFlag();
194 return recursiveSubst(oldToNew, visited);
202 if(oldToNew.
size() == 0)
return *
this;
210 (*i).first.setFlag();
212 return recursiveSubst(oldToNew, visited);
217 Expr Expr::substExprQuant(
const vector<Expr>& oldTerms,
218 const vector<Expr>& newTerms)
const
229 DebugAssert(oldTerms.size() == newTerms.size(),
"substExpr: vectors"
230 "don't match in size");
233 if(oldTerms.size() == 0)
return *
this;
238 for(
unsigned int i=0; i<oldTerms.size(); i++) {
239 oldToNew.
insert(oldTerms[i], newTerms[i]);
245 Expr returnExpr = recursiveQuantSubst(oldToNew, visited);;
257 return recursiveQuantSubst(oldToNew,visited);
264 if (!containsBoundVar()){
275 if (find != substMap.
end()) {
301 const vector<Expr> & vars = getVars();
315 vector<vector<Expr> > vvNewTriggers = substTriggers(substMap,visited);
317 getEM()->newClosureExpr(getKind(), vars,
318 getBody().recursiveQuantSubst(substMap, visited),
323 vector<Expr> children;
329 children.push_back(repChild);
332 replaced =
Expr(getOp(), children);
344 string Expr::toString()
const {
353 if(isNull())
return "Null";
364 cout <<
"Null" <<
endl;
return;
373 void Expr::pprint()
const
376 cout <<
"Null" <<
endl;
return;
383 void Expr::pprintnodag()
const
386 cout <<
"Null" <<
endl;
return;
394 void Expr::printnodag()
const
401 if(isNull())
return os <<
"Null" <<
endl;
402 bool isLetDecl(getKind() ==
LETDECL);
404 os << getEM()->getKindName(getKind());
406 os <<
space <<
"{" << getOp().getExpr() << push <<
"}";
408 else if (isSymbol()) {
409 os <<
space <<
"{Symbol: " << getName() <<
"}";
411 else if (isClosure()) {
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 <<
"}";
424 os <<
space <<
"{" <<
'"'+ getString() +
'"' <<
"}";
428 os <<
space <<
"{SKOLEM_" << (int)getIndex() <<
"}";
431 os <<
space <<
"{" << getRational() <<
"}";
435 os <<
space <<
"{" << getName() <<
"}";
439 os <<
space <<
"{"+getName()+
"_"+getUid()+
"}";
443 os <<
space <<
"{Theorem: " << getTheorem().toString() <<
"}";
449 if(isLetDecl) os <<
nodag;
459 if(isNull())
return os <<
"Null" <<
endl;
460 if (isSymbol())
return os << getName();
465 case STRING_EXPR:
return os <<
'"'+ getString() +
'"';
468 case UCONST:
return os << getName();
469 case BOUND_VAR:
return os <<
"(BOUND_VAR "+getName()+
"_"+getUid()+
")";
472 bool firstTime(
true);
474 if(firstTime) firstTime =
false;
478 return os << push <<
")";
483 os <<
"(" <<
push << getEM()->getKindName(getKind())
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 <<
")";
494 case RESTART:
return os <<
"RESTART " << (*this)[0] <<
";";
497 os << getEM()->getKindName(getKind());
510 Expr& Expr::indent(
int n,
bool permanent) {
511 DebugAssert(!isNull(),
"Expr::indent called on Null Expr");
512 getEM()->indent(n, permanent);
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);
525 bool Expr::containsTermITE()
const
527 if (getType().isBool()) {
531 if (validIsAtomicFlag()) {
532 return !getIsAtomicFlag();
535 for (
int k = 0; k < arity(); ++k) {
536 if ((*
this)[k].containsTermITE()) {
537 setIsAtomicFlag(
false);
542 setIsAtomicFlag(
true);
546 else return !isAtomic();
550 bool Expr::isAtomic()
const
552 if (getType().isBool()) {
553 return isBoolConst();
556 if (validIsAtomicFlag()) {
557 return getIsAtomicFlag();
560 for (
int k = 0; k < arity(); ++k) {
561 if (!(*
this)[k].isAtomic()) {
562 setIsAtomicFlag(
false);
566 setIsAtomicFlag(
true);
571 bool Expr::isAtomicFormula()
const
574 if (!getType().isBool()) {
585 if (!(*k).isAtomic()) {
600 if(e1 == e2)
return 0;
602 if(e1.
d_expr == NULL)
return -1;
603 if(e2.
d_expr == NULL)
return 1;
622 if(e.
isNull())
return os <<
"Null";
634 Type::Type(
Expr expr) : d_expr(expr)
636 if (expr.
isNull())
return;
643 for(vector<Type>::const_iterator i=typeDom.begin(), iend=typeDom.end();
645 tmp.push_back(i->getExpr());
646 tmp.push_back(typeRan.
getExpr());