00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #include <algorithm>
00023
00024
00025 #include "expr.h"
00026 #include "pretty_printer.h"
00027 #include "expr_stream.h"
00028 #include "notifylist.h"
00029 #include "exception.h"
00030
00031
00032 using namespace std;
00033
00034
00035 namespace CVC3 {
00036
00037
00038 Expr Expr::s_null;
00039
00040
00041
00042
00043
00044
00045 Expr Expr::recursiveSubst(const ExprHashMap<Expr>& subst,
00046 ExprHashMap<Expr>& visited) const {
00047
00048
00049 if(getFlag()) return visited[*this];
00050
00051 ExprIndex minIndex = 0;
00052 for(ExprHashMap<Expr>::iterator i = subst.begin(),iend=subst.end();i!=iend;++i) {
00053 if(minIndex > (i->first).getIndex())
00054 minIndex = (i->first).getIndex();
00055 }
00056
00057 Expr replaced;
00058
00059 if(isClosure()) {
00060 const vector<Expr> & vars = getVars();
00061 vector<Expr> common;
00062
00063 for(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end();
00064 i!=iend; ++i) {
00065 if(subst.count(*i) > 0) common.push_back(*i);
00066 }
00067
00068 if(common.size() > 0) {
00069 IF_DEBUG(debugger.counter("substExpr: bound var clashes")++);
00070
00071 ExprHashMap<Expr> newSubst(subst);
00072
00073 for(vector<Expr>::iterator i=common.begin(), iend=common.end();
00074 i!=iend; ++i)
00075 newSubst.erase(*i);
00076
00077
00078 visited.clear();
00079 clearFlags();
00080 visited = newSubst;
00081
00082 ExprHashMap<Expr>::iterator j = newSubst.begin();
00083 for (; j != newSubst.end(); ++j) {
00084 j->first.setFlag();
00085 }
00086
00087 replaced =
00088 getEM()->newClosureExpr(getKind(), vars,
00089 getBody().recursiveSubst(newSubst, visited));
00090
00091
00092 visited.clear();
00093 clearFlags();
00094 visited = subst;
00095
00096 for (ExprHashMap<Expr>::iterator i = subst.begin(), iend=subst.end();
00097 i != iend; ++i)
00098 i->first.setFlag();
00099 } else {
00100 replaced =
00101 getEM()->newClosureExpr(getKind(), vars,
00102 getBody().recursiveSubst(subst, visited));
00103 }
00104 } else {
00105 int changed=0;
00106 vector<Expr> children;
00107 for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i){
00108 Expr repChild = *i;
00109 if(repChild.getIndex() >= minIndex)
00110 repChild = (*i).recursiveSubst(subst, visited);
00111 if(repChild != *i)
00112 changed++;
00113 children.push_back(repChild);
00114 }
00115 if(changed > 0)
00116 replaced = Expr(getOp(), children);
00117 else
00118 replaced = *this;
00119 }
00120 visited.insert(*this, replaced);
00121 setFlag();
00122 return replaced;
00123 }
00124
00125
00126 static bool subExprRec(const Expr& e1, const Expr& e2) {
00127 if(e1 == e2) return true;
00128 if(e2.getFlag()) return false;
00129
00130 if(e1 > e2) return false;
00131 e2.setFlag();
00132 bool res(false);
00133 for(Expr::iterator i=e2.begin(), iend=e2.end(); !res && i!=iend; ++i)
00134 res = subExprRec(e1, *i);
00135 return res;
00136 }
00137
00138
00139 bool
00140 Expr::subExprOf(const Expr& e) const {
00141 if(*this == e) return true;
00142
00143 if(*this > e) return false;
00144 clearFlags();
00145 return subExprRec(*this, e);
00146 }
00147
00148
00149 Expr Expr::substExpr(const vector<Expr>& oldTerms,
00150 const vector<Expr>& newTerms) const
00151 {
00152 DebugAssert(oldTerms.size() == newTerms.size(), "substExpr: vectors"
00153 "don't match in size");
00154
00155 if(oldTerms.size() == 0) return *this;
00156
00157 ExprHashMap<Expr> oldToNew(10);
00158 clearFlags();
00159 for(unsigned int i=0; i<oldTerms.size(); i++) {
00160 oldToNew.insert(oldTerms[i], newTerms[i]);
00161 oldTerms[i].setFlag();
00162 }
00163
00164 ExprHashMap<Expr> visited(oldToNew);
00165 return recursiveSubst(oldToNew, visited);
00166
00167 }
00168
00169
00170 Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const
00171 {
00172
00173 if(oldToNew.size() == 0) return *this;
00174
00175 ExprHashMap<Expr> visited(oldToNew);
00176 clearFlags();
00177
00178
00179 for(ExprHashMap<Expr>::iterator i=oldToNew.begin(), iend=oldToNew.end();
00180 i!=iend; ++i) {
00181 (*i).first.setFlag();
00182 }
00183 return recursiveSubst(oldToNew, visited);
00184 }
00185
00186
00187 string Expr::toString() const {
00188 return toString(PRESENTATION_LANG);
00189
00190
00191
00192
00193 }
00194
00195 string Expr::toString(InputLanguage lang) const {
00196 if(isNull()) return "Null";
00197 ostringstream ss;
00198 ExprStream os(getEM());
00199 os.lang(lang);
00200 os.os(ss);
00201 os << (*this);
00202 return ss.str();
00203 }
00204
00205 void Expr::print(InputLanguage lang, bool dagify) const {
00206 if(isNull()) {
00207 cout << "Null" << endl; return;
00208 }
00209 ExprStream os(getEM());
00210 os.lang(lang);
00211 os.dagFlag(dagify);
00212 os << *this << endl;
00213 }
00214
00215
00216 void Expr::pprint() const
00217 {
00218 if(isNull()) {
00219 cout << "Null" << endl; return;
00220 }
00221 ExprStream os(getEM());
00222 os << *this << endl;
00223 }
00224
00225
00226 void Expr::pprintnodag() const
00227 {
00228 if(isNull()) {
00229 cout << "Null" << endl; return;
00230 }
00231 ExprStream os(getEM());
00232 os.dagFlag(false);
00233 os << *this << endl;
00234 }
00235
00236
00237 void Expr::printnodag() const
00238 {
00239 print(AST_LANG, false);
00240 }
00241
00242
00243 ExprStream& Expr::printAST(ExprStream& os) const {
00244 if(isNull()) return os << "Null" << endl;
00245 bool isLetDecl(getKind() == LETDECL);
00246 os << "(" << push;
00247 os << getEM()->getKindName(getKind());
00248 if (isApply()) {
00249 os << space << "{" << getOp().getExpr() << push << "}";
00250 }
00251 else if (isSymbol()) {
00252 os << space << "{Symbol: " << getName() << "}";
00253 }
00254 else if (isClosure()) {
00255 os << space << "{" << space << "(" << push;
00256 const vector<Expr>& vars = getVars();
00257 vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
00258 if(i!=iend) { os << *i; ++i; }
00259 for(; i!=iend; ++i) os << space << *i;
00260 os << push << ") " << pop << pop;
00261 os << getBody() << push << "}";
00262 }
00263 else {
00264 switch(getKind()) {
00265 case STRING_EXPR:
00266 DebugAssert(isString(), "Expected String");
00267 os << space << "{" << '"'+ getString() + '"' << "}";
00268 break;
00269 case SKOLEM_VAR:
00270 getExistential();
00271 os << space << "{SKOLEM_" << (int)getIndex() << "}";
00272 break;
00273 case RATIONAL_EXPR:
00274 os << space << "{" << getRational() << "}";
00275 break;
00276 case UCONST:
00277 DebugAssert(isVar(), "Expected Var");
00278 os << space << "{" << getName() << "}";
00279 break;
00280 case BOUND_VAR:
00281 DebugAssert(isVar(), "Expected Var");
00282 os << space << "{"+getName()+"_"+getUid()+"}";
00283 break;
00284 case THEOREM_KIND:
00285 DebugAssert(isTheorem(), "Expected Theorem");
00286 os << space << "{Theorem: " << getTheorem().toString() << "}";
00287 default: ;
00288 }
00289 }
00290
00291 for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) {
00292 if(isLetDecl) os << nodag;
00293 os << space << *i;
00294 }
00295 os << push << ")";
00296 os.resetIndent();
00297 return os;
00298 }
00299
00300
00301 ExprStream& Expr::print(ExprStream& os) const {
00302 if(isNull()) return os << "Null" << endl;
00303 DebugAssert(arity() == 0, "Expected arity 0");
00304 if (isSymbol()) return os << getName();
00305 switch(getKind()) {
00306 case TRUE_EXPR: return os << "TRUE";
00307 case FALSE_EXPR: return os << "FALSE";
00308 case NULL_KIND: return os << "Null";
00309 case STRING_EXPR: return os << '"'+ getString() + '"';
00310 case RATIONAL_EXPR: return os << getRational();
00311 case SKOLEM_VAR: return os << "SKOLEM_" << hash();
00312 case UCONST: return os << getName();
00313 case BOUND_VAR: return os << "(BOUND_VAR "+getName()+"_"+getUid()+")";
00314 case RAW_LIST: {
00315 os << "(" << push;
00316 bool firstTime(true);
00317 for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) {
00318 if(firstTime) firstTime = false;
00319 else os << space;
00320 os << *i;
00321 }
00322 return os << push << ")";
00323 }
00324 case FORALL:
00325 case EXISTS:
00326 if(isQuantifier()) {
00327 os << "(" << push << getEM()->getKindName(getKind())
00328 << space << "(" << push;
00329 const vector<Expr>& vars = getVars();
00330 vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
00331 if(i!=iend) { os << *i; ++i; }
00332 for(; i!=iend; ++i) os << space << *i;
00333 os << push << ") " << pop << pop;
00334 return os << getBody() << push << ")";
00335 }
00336
00337
00338 default:
00339
00340 os << getEM()->getKindName(getKind());
00341
00342 }
00343 os.resetIndent();
00344 return os;
00345 }
00346
00347
00348
00349
00350
00351
00352
00353 Expr& Expr::indent(int n, bool permanent) {
00354 DebugAssert(!isNull(), "Expr::indent called on Null Expr");
00355 getEM()->indent(n, permanent);
00356 return *this;
00357 }
00358
00359
00360 void Expr::addToNotify(Theory* i, const Expr& e) const {
00361 DebugAssert(!isNull(), "Expr::addToNotify() on Null expr");
00362 if(getNotify() == NULL)
00363 d_expr->d_notifyList = new NotifyList(getEM()->getCurrentContext());
00364 getNotify()->add(i, e);
00365 }
00366
00367
00368 bool Expr::isAtomic() const
00369 {
00370
00371 if (validIsAtomicFlag()) {
00372
00373
00374 return getIsAtomicFlag();
00375 }
00376 if (getType().isBool() && !isBoolConst()) {
00377 setIsAtomicFlag(false);
00378
00379 return false;
00380 }
00381 for (int k = 0; k < arity(); ++k) {
00382 if (!(*this)[k].isAtomic()) {
00383 setIsAtomicFlag(false);
00384
00385 return false;
00386 }
00387 }
00388 setIsAtomicFlag(true);
00389
00390 return true;
00391 }
00392
00393
00394 bool Expr::isAtomicFormula() const
00395 {
00396
00397 if (!getType().isBool()) {
00398
00399 return false;
00400 }
00401 switch(getKind()) {
00402 case FORALL: case EXISTS: case XOR:
00403 case NOT: case AND: case OR: case ITE: case IFF: case IMPLIES:
00404
00405 return false;
00406 }
00407 for (Expr::iterator k = begin(), kend=end(); k != kend; ++k) {
00408 if (!(*k).isAtomic()) {
00409
00410 return false;
00411 }
00412 }
00413
00414 return true;
00415 }
00416
00417
00418
00419
00420 int compare(const Expr& e1, const Expr& e2) {
00421
00422
00423 if(e1 == e2) return 0;
00424
00425 if(e1.d_expr == NULL) return -1;
00426 if(e2.d_expr == NULL) return 1;
00427
00428 return (e1.getIndex() < e2.getIndex())? -1 : 1;
00429 }
00430
00431
00432
00433
00434
00435
00436
00437 ostream& operator<<(ostream& os, const Expr& e) {
00438 if(e.isNull()) return os << "Null";
00439 ExprStream es(e.getEM());
00440 es.os(os);
00441 es << e;
00442 e.getEM()->restoreIndent();
00443 return os;
00444 }
00445
00446
00447
00448
00449
00450 Type::Type(Expr expr) : d_expr(expr)
00451 {
00452 if (expr.isNull()) return;
00453 expr.getEM()->checkType(expr);
00454 }
00455
00456
00457 Type Type::funType(const std::vector<Type>& typeDom, const Type& typeRan) {
00458 vector<Expr> tmp;
00459 for(vector<Type>::const_iterator i=typeDom.begin(), iend=typeDom.end();
00460 i!=iend; ++i)
00461 tmp.push_back(i->getExpr());
00462 tmp.push_back(typeRan.getExpr());
00463 return Type(Expr(ARROW, tmp));
00464 }
00465
00466
00467 }