CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file expr.cpp 00004 * 00005 * Author: Sergey Berezin 00006 * 00007 * Created: Thu Dec 5 11:35:55 2002 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 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 // Class Expr methods // 00042 /////////////////////////////////////////////////////////////////////// 00043 00044 00045 Expr Expr::recursiveSubst(const ExprHashMap<Expr>& subst, 00046 ExprHashMap<Expr>& visited) const { 00047 // Check the cache. 00048 // INVARIANT: visited contains all the flagged expressions, and only those 00049 if(getFlag()) return visited[*this]; 00050 00051 ExprIndex minIndex = 0; 00052 for(ExprHashMap<Expr>::const_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; // Bound vars which occur in subst 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 // Reduced substitution (without the common vars) 00071 ExprHashMap<Expr> newSubst(subst); 00072 // Remove variables in "common" from the substitution 00073 for(vector<Expr>::iterator i=common.begin(), iend=common.end(); 00074 i!=iend; ++i) 00075 newSubst.erase(*i); 00076 00077 // Clear all the caches (important!) 00078 visited.clear(); 00079 clearFlags(); 00080 visited = newSubst; 00081 00082 ExprHashMap<Expr>::iterator j = newSubst.begin(); 00083 for (; j != newSubst.end(); ++j) { // old vars bound in e 00084 j->first.setFlag(); 00085 } 00086 00087 replaced = 00088 getEM()->newClosureExpr(getKind(), vars, 00089 getBody().recursiveSubst(newSubst, visited)); 00090 00091 // Clear the flags again, as we restore the substitution 00092 visited.clear(); 00093 clearFlags(); 00094 visited = subst; 00095 // Restore the flags on the original substitutions 00096 for (ExprHashMap<Expr>::const_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 { // Not a Closure 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 Expr opExpr; 00116 if (isApply()) { 00117 opExpr = getOpExpr().recursiveSubst(subst, visited); 00118 if (opExpr != getOpExpr()) ++changed; 00119 } 00120 if(changed > 0) { 00121 Op op = opExpr.isNull() ? getOp() : opExpr.mkOp(); 00122 replaced = Expr(op, children); 00123 } 00124 else replaced = *this; 00125 } 00126 visited.insert(*this, replaced); 00127 setFlag(); 00128 return replaced; 00129 } 00130 00131 00132 static bool subExprRec(const Expr& e1, const Expr& e2) { 00133 if(e1 == e2) return true; 00134 if(e2.getFlag()) return false; 00135 // e1 is created after e2, so e1 cannot be a subexpr of e2 00136 if(e1 > e2) return false; 00137 e2.setFlag(); 00138 bool res(false); 00139 for(Expr::iterator i=e2.begin(), iend=e2.end(); !res && i!=iend; ++i) 00140 res = subExprRec(e1, *i); 00141 return res; 00142 } 00143 00144 00145 bool 00146 Expr::subExprOf(const Expr& e) const { 00147 if(*this == e) return true; 00148 // "this" is created after e, so it cannot be e's subexpression 00149 if(*this > e) return false; 00150 clearFlags(); 00151 return subExprRec(*this, e); 00152 } 00153 00154 00155 Expr Expr::substExpr(const vector<Expr>& oldTerms, 00156 const vector<Expr>& newTerms) const 00157 { 00158 DebugAssert(oldTerms.size() == newTerms.size(), "substExpr: vectors" 00159 "don't match in size"); 00160 // Catch the vacuous case 00161 if(oldTerms.size() == 0) return *this; 00162 00163 ExprHashMap<Expr> oldToNew(10); 00164 clearFlags(); 00165 for(unsigned int i=0; i<oldTerms.size(); i++) { 00166 oldToNew.insert(oldTerms[i], newTerms[i]); 00167 oldTerms[i].setFlag(); 00168 } 00169 // For cache, initialized by the substitution 00170 ExprHashMap<Expr> visited(oldToNew); 00171 return recursiveSubst(oldToNew, visited); 00172 00173 } 00174 00175 00176 Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const 00177 { 00178 // Catch the vacuous case 00179 if(oldToNew.size() == 0) return *this; 00180 // Rebuild the map: we'll be using it as a cache 00181 ExprHashMap<Expr> visited(oldToNew); 00182 clearFlags(); 00183 // Flag all the LHS expressions in oldToNew map. We'll be checking 00184 // all flagged expressions (and only those) for substitution. 00185 for(ExprHashMap<Expr>::const_iterator i=oldToNew.begin(), iend=oldToNew.end(); 00186 i!=iend; ++i) { 00187 (*i).first.setFlag(); 00188 } 00189 return recursiveSubst(oldToNew, visited); 00190 } 00191 00192 00193 00194 Expr Expr::substExprQuant(const vector<Expr>& oldTerms, 00195 const vector<Expr>& newTerms) const 00196 { 00197 //let us disable this first yeting 00198 // static ExprHashMap<Expr> substCache; 00199 // Expr cacheIndex = Expr(RAW_LIST, *this, Expr(RAW_LIST, newTerms)); 00200 00201 // ExprHashMap<Expr>::iterator i = substCache.find(cacheIndex); 00202 // if (i != substCache.end()){ 00203 // return i->second; 00204 // } 00205 00206 DebugAssert(oldTerms.size() == newTerms.size(), "substExpr: vectors" 00207 "don't match in size"); 00208 // Catch the vacuous case 00209 00210 if(oldTerms.size() == 0) return *this; 00211 00212 ExprHashMap<Expr> oldToNew(10); 00213 00214 // clearFlags(); 00215 for(unsigned int i=0; i<oldTerms.size(); i++) { 00216 oldToNew.insert(oldTerms[i], newTerms[i]); 00217 // oldTerms[i].setFlag(); 00218 } 00219 // For cache, initialized by the substitution 00220 ExprHashMap<Expr> visited(oldToNew); 00221 Expr returnExpr = recursiveQuantSubst(oldToNew, visited);; 00222 // return recursiveQuantSubst(oldToNew, visited); 00223 // substCache[cacheIndex] = returnExpr; 00224 // cout<<"pushed " << cacheIndex << endl << "RET " << returnExpr << endl; 00225 return returnExpr; 00226 00227 } 00228 00229 00230 00231 Expr Expr::recursiveQuantSubst(ExprHashMap<Expr>& substMap, 00232 ExprHashMap<Expr>& visited) const { 00233 00234 if (!containsBoundVar()){ 00235 // std::cout <<"no bound var " << *this << std::endl; 00236 return *this; 00237 } 00238 00239 // Check the cache. 00240 // INVARIANT: visited contains all the flagged expressions, and only those 00241 // the above invariant is no longer true. yeting 00242 00243 if(getKind() == BOUND_VAR ) { 00244 // Expr ret = visited[*this]; 00245 const Expr ret = substMap[*this]; 00246 if (!ret.isNull()){ 00247 return ret; 00248 } 00249 } 00250 00251 // if(getFlag()) return visited[*this]; 00252 00253 // why we need this. 00254 // ExprIndex minIndex = 0; 00255 // for(ExprHashMap<Expr>::iterator i = substMap.begin(),iend=substMap.end();i!=iend;++i) { 00256 // if(minIndex > (i->first).getIndex()) 00257 // minIndex = (i->first).getIndex(); 00258 // } 00259 00260 Expr replaced; 00261 00262 if(isClosure()) { 00263 // for safety, we can wrap the following lines by if debug 00264 00265 const vector<Expr> & vars = getVars(); 00266 // vector<Expr> common; // Bound vars which occur in subst 00267 00268 // for(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end(); 00269 // i!=iend; ++i) { 00270 // if(substMap.count(*i) > 0) common.push_back(*i); 00271 // } 00272 00273 // if(common.size() > 0) { 00274 // cout<<"error in quant subst" << endl; 00275 // } else { 00276 replaced = 00277 getEM()->newClosureExpr(getKind(), vars, 00278 getBody().recursiveQuantSubst(substMap, visited)); 00279 // } 00280 } else { // Not a Closure 00281 int changed=0; 00282 vector<Expr> children; 00283 for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i){ 00284 Expr repChild ; 00285 repChild = (*i).recursiveQuantSubst(substMap, visited); 00286 if(repChild != *i) 00287 changed++; 00288 children.push_back(repChild); 00289 } 00290 if(changed > 0) 00291 replaced = Expr(getOp(), children); 00292 else 00293 replaced = *this; 00294 } 00295 // visited.insert(*this, replaced); 00296 // setFlag(); 00297 return replaced; 00298 } 00299 00300 00301 00302 00303 string Expr::toString() const { 00304 return toString(PRESENTATION_LANG); 00305 // if(isNull()) return "Null"; 00306 // ostringstream ss; 00307 // ss << (*this); 00308 // return ss.str(); 00309 } 00310 00311 string Expr::toString(InputLanguage lang) const { 00312 if(isNull()) return "Null"; 00313 ostringstream ss; 00314 ExprStream os(getEM()); 00315 os.lang(lang); 00316 os.os(ss); 00317 os << (*this); 00318 return ss.str(); 00319 } 00320 00321 void Expr::print(InputLanguage lang, bool dagify) const { 00322 if(isNull()) { 00323 cout << "Null" << endl; return; 00324 } 00325 ExprStream os(getEM()); 00326 os.lang(lang); 00327 os.dagFlag(dagify); 00328 os << *this << endl; 00329 } 00330 00331 00332 void Expr::pprint() const 00333 { 00334 if(isNull()) { 00335 cout << "Null" << endl; return; 00336 } 00337 ExprStream os(getEM()); 00338 os << *this << endl; 00339 } 00340 00341 00342 void Expr::pprintnodag() const 00343 { 00344 if(isNull()) { 00345 cout << "Null" << endl; return; 00346 } 00347 ExprStream os(getEM()); 00348 os.dagFlag(false); 00349 os << *this << endl; 00350 } 00351 00352 00353 void Expr::printnodag() const 00354 { 00355 print(AST_LANG, false); 00356 } 00357 00358 00359 ExprStream& Expr::printAST(ExprStream& os) const { 00360 if(isNull()) return os << "Null" << endl; 00361 bool isLetDecl(getKind() == LETDECL); 00362 os << "(" << push; 00363 os << getEM()->getKindName(getKind()); 00364 if (isApply()) { 00365 os << space << "{" << getOp().getExpr() << push << "}"; 00366 } 00367 else if (isSymbol()) { 00368 os << space << "{Symbol: " << getName() << "}"; 00369 } 00370 else if (isClosure()) { 00371 os << space << "{" << space << "(" << push; 00372 const vector<Expr>& vars = getVars(); 00373 vector<Expr>::const_iterator i=vars.begin(), iend=vars.end(); 00374 if(i!=iend) { os << *i; ++i; } 00375 for(; i!=iend; ++i) os << space << *i; 00376 os << push << ") " << pop << pop; 00377 os << getBody() << push << "}"; 00378 } 00379 else { 00380 switch(getKind()) { 00381 case STRING_EXPR: 00382 DebugAssert(isString(), "Expected String"); 00383 os << space << "{" << '"'+ getString() + '"' << "}"; 00384 break; 00385 case SKOLEM_VAR: 00386 getExistential(); 00387 os << space << "{SKOLEM_" << (int)getIndex() << "}"; 00388 break; 00389 case RATIONAL_EXPR: 00390 os << space << "{" << getRational() << "}"; 00391 break; 00392 case UCONST: 00393 DebugAssert(isVar(), "Expected Var"); 00394 os << space << "{" << getName() << "}"; 00395 break; 00396 case BOUND_VAR: 00397 DebugAssert(isVar(), "Expected Var"); 00398 os << space << "{"+getName()+"_"+getUid()+"}"; 00399 break; 00400 case THEOREM_KIND: 00401 DebugAssert(isTheorem(), "Expected Theorem"); 00402 os << space << "{Theorem: " << getTheorem().toString() << "}"; 00403 default: ; // Don't do anything 00404 } 00405 } 00406 00407 for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) { 00408 if(isLetDecl) os << nodag; 00409 os << space << *i; 00410 } 00411 os << push << ")"; 00412 os.resetIndent(); 00413 return os; 00414 } 00415 00416 00417 ExprStream& Expr::print(ExprStream& os) const { 00418 if(isNull()) return os << "Null" << endl; 00419 if (isSymbol()) return os << getName(); 00420 switch(getKind()) { 00421 case TRUE_EXPR: return os << "TRUE"; 00422 case FALSE_EXPR: return os << "FALSE"; 00423 case NULL_KIND: return os << "Null"; 00424 case STRING_EXPR: return os << '"'+ getString() + '"'; 00425 case RATIONAL_EXPR: return os << getRational(); 00426 case SKOLEM_VAR: return os << "SKOLEM_" << hash(); 00427 case UCONST: return os << getName(); 00428 case BOUND_VAR: return os << "(BOUND_VAR "+getName()+"_"+getUid()+")"; 00429 case RAW_LIST: { 00430 os << "(" << push; 00431 bool firstTime(true); 00432 for(Expr::iterator i=begin(), iend=end(); i!=iend; ++i) { 00433 if(firstTime) firstTime = false; 00434 else os << space; 00435 os << *i; 00436 } 00437 return os << push << ")"; 00438 } 00439 case FORALL: 00440 case EXISTS: 00441 if(isQuantifier()) { 00442 os << "(" << push << getEM()->getKindName(getKind()) 00443 << space << "(" << push; 00444 const vector<Expr>& vars = getVars(); 00445 vector<Expr>::const_iterator i=vars.begin(), iend=vars.end(); 00446 if(i!=iend) { os << *i; ++i; } 00447 for(; i!=iend; ++i) os << space << *i; 00448 os << push << ") " << pop << pop; 00449 return os << getBody() << push << ")"; 00450 } 00451 // If not an internal representation of quantifiers, it'll be 00452 // printed as "normal" Expr with a kind and children 00453 case RESTART: return os << "RESTART " << (*this)[0] << ";"; 00454 default: 00455 // os << "(" << push; 00456 os << getEM()->getKindName(getKind()); 00457 // os << push << ")"; 00458 } 00459 os.resetIndent(); 00460 return os; 00461 } 00462 00463 00464 //! Set initial indentation to n. 00465 /*! The indentation will be reset to default unless the second 00466 argument is true. This setting only takes effect when printing to 00467 std::ostream. When printing to ExprStream, the indentation can be 00468 set directly in the ExprStream. */ 00469 Expr& Expr::indent(int n, bool permanent) { 00470 DebugAssert(!isNull(), "Expr::indent called on Null Expr"); 00471 getEM()->indent(n, permanent); 00472 return *this; 00473 } 00474 00475 00476 void Expr::addToNotify(Theory* i, const Expr& e) const { 00477 DebugAssert(!isNull(), "Expr::addToNotify() on Null expr"); 00478 if(getNotify() == NULL) 00479 d_expr->d_notifyList = new NotifyList(getEM()->getCurrentContext()); 00480 getNotify()->add(i, e); 00481 } 00482 00483 00484 bool Expr::containsTermITE() const 00485 { 00486 if (getType().isBool()) { 00487 00488 // We overload the isAtomicFlag to mean !containsTermITE for exprs 00489 // of Boolean type 00490 if (validIsAtomicFlag()) { 00491 return !getIsAtomicFlag(); 00492 } 00493 00494 for (int k = 0; k < arity(); ++k) { 00495 if ((*this)[k].containsTermITE()) { 00496 setIsAtomicFlag(false); 00497 return true; 00498 } 00499 } 00500 00501 setIsAtomicFlag(true); 00502 return false; 00503 00504 } 00505 else return !isAtomic(); 00506 } 00507 00508 00509 bool Expr::isAtomic() const 00510 { 00511 if (getType().isBool()) { 00512 return isBoolConst(); 00513 } 00514 00515 if (validIsAtomicFlag()) { 00516 return getIsAtomicFlag(); 00517 } 00518 00519 for (int k = 0; k < arity(); ++k) { 00520 if (!(*this)[k].isAtomic()) { 00521 setIsAtomicFlag(false); 00522 return false; 00523 } 00524 } 00525 setIsAtomicFlag(true); 00526 return true; 00527 } 00528 00529 00530 bool Expr::isAtomicFormula() const 00531 { 00532 // TRACE("isAtomic", "isAtomicFormula(", *this, ") {"); 00533 if (!getType().isBool()) { 00534 // TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }"); 00535 return false; 00536 } 00537 switch(getKind()) { 00538 case FORALL: case EXISTS: case XOR: 00539 case NOT: case AND: case OR: case ITE: case IFF: case IMPLIES: 00540 // TRACE_MSG("isAtomic", "isAtomicFormula[connective] => false }"); 00541 return false; 00542 } 00543 for (Expr::iterator k = begin(), kend=end(); k != kend; ++k) { 00544 if (!(*k).isAtomic()) { 00545 // TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }"); 00546 return false; 00547 } 00548 } 00549 // TRACE_MSG("isAtomic", "isAtomicFormula => true }"); 00550 return true; 00551 } 00552 00553 00554 // This is one of the most friequently called routines. Make it as 00555 // efficient as possible. 00556 int compare(const Expr& e1, const Expr& e2) { 00557 // Quick equality check (operator== is implemented independently 00558 // and more efficiently) 00559 if(e1 == e2) return 0; 00560 00561 if(e1.d_expr == NULL) return -1; 00562 if(e2.d_expr == NULL) return 1; 00563 00564 // Both are non-Null. Check for constant 00565 bool e1c = e1.isConstant(); 00566 if (e1c != e2.isConstant()) { 00567 return e1c ? -1 : 1; 00568 } 00569 00570 // Compare the indices 00571 return (e1.getIndex() < e2.getIndex())? -1 : 1; 00572 } 00573 00574 00575 /////////////////////////////////////////////////////////////////////// 00576 // Class Expr::iterator methods // 00577 /////////////////////////////////////////////////////////////////////// 00578 00579 00580 ostream& operator<<(ostream& os, const Expr& e) { 00581 if(e.isNull()) return os << "Null"; 00582 ExprStream es(e.getEM()); 00583 es.os(os); 00584 es << e; 00585 e.getEM()->restoreIndent(); 00586 return os; 00587 } 00588 00589 00590 // Functions from class Type 00591 00592 00593 Type::Type(Expr expr) : d_expr(expr) 00594 { 00595 if (expr.isNull()) return; 00596 expr.getEM()->checkType(expr); 00597 } 00598 00599 00600 Type Type::funType(const std::vector<Type>& typeDom, const Type& typeRan) { 00601 vector<Expr> tmp; 00602 for(vector<Type>::const_iterator i=typeDom.begin(), iend=typeDom.end(); 00603 i!=iend; ++i) 00604 tmp.push_back(i->getExpr()); 00605 tmp.push_back(typeRan.getExpr()); 00606 return Type(Expr(ARROW, tmp)); 00607 } 00608 00609 00610 } // end of namespace CVC3