expr_transform.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr_transform.cpp
00004  * 
00005  * Author: Ying Hu, Clark Barrett
00006  * 
00007  * Created: Jun 05 2003
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 "expr_transform.h"
00023 #include "theory_core.h"
00024 #include "theory_arith.h"
00025 #include "command_line_flags.h"
00026 #include "core_proof_rules.h"
00027 #include <set>
00028 
00029 
00030 using namespace std;
00031 using namespace CVC3;
00032 
00033 
00034 ExprTransform::ExprTransform(TheoryCore* core)
00035   : d_core(core)
00036 {
00037   d_commonRules = d_core->getCommonRules();  
00038   d_rules = d_core->getCoreRules();
00039 }
00040 
00041 
00042 Theorem ExprTransform::smartSimplify(const Expr& e, ExprMap<bool>& cache)
00043 {
00044   ExprMap<bool>::iterator it;
00045   vector<Expr> operatorStack;
00046   vector<int> childStack;
00047   Expr e2;
00048 
00049   operatorStack.push_back(e);
00050   childStack.push_back(0);
00051 
00052   while (!operatorStack.empty()) {
00053     DebugAssert(operatorStack.size() == childStack.size(), "Invariant violated");
00054     if (childStack.back() < operatorStack.back().arity()) {
00055       e2 = operatorStack.back()[childStack.back()++];
00056       it = cache.find(e2);
00057       if (it != cache.end() || e2.hasFind() ||
00058           e2.validSimpCache() || e2.arity() == 0) continue;
00059       if (operatorStack.size() >= 5000) {
00060         smartSimplify(e2, cache);
00061         cache[e2] = true;
00062       }
00063       else {
00064         operatorStack.push_back(e2);
00065         childStack.push_back(0);
00066       }
00067     }
00068     else {
00069       cache[operatorStack.back()] = true;
00070       operatorStack.pop_back();
00071       childStack.pop_back();
00072     }
00073   }
00074   DebugAssert(childStack.empty(), "Invariant violated");
00075   return d_core->simplify(e);
00076 }
00077 
00078 
00079 Theorem ExprTransform::preprocess(const Expr& e)
00080 {
00081   // Force simplifier to run
00082   d_core->getEM()->invalidateSimpCache();
00083   d_core->setInPP();
00084   Theorem res = d_commonRules->reflexivityRule(e);
00085 
00086   if (d_core->getFlags()["preprocess"].getBool()) {
00087     if (d_core->getFlags()["pp-pushneg"].getBool()) {
00088       res = pushNegation(e);
00089     }
00090     ExprMap<bool> cache;
00091     if (d_core->getFlags()["pp-bryant"].getBool()) {
00092       res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
00093       res = d_commonRules->transitivityRule(res, dobryant(res.getRHS()));
00094     }
00095     if (d_core->getFlags()["pp-care"].getBool()) {
00096       res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
00097       res = d_commonRules->transitivityRule(res, simplifyWithCare(res.getRHS()));
00098     }
00099     int budget = 0;
00100     d_budgetLimit = d_core->getFlags()["pp-budget"].getInt();
00101     while (budget < d_budgetLimit) {
00102       res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
00103       Theorem ppRes = newPP(res.getRHS(), budget);
00104       if (ppRes.isRefl()) break;
00105       res = d_commonRules->transitivityRule(res, ppRes);
00106       if (d_core->getFlags()["pp-care"].getBool()) {
00107         res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
00108         res = d_commonRules->transitivityRule(res, simplifyWithCare(res.getRHS()));
00109       }
00110     }
00111     res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
00112     // Make sure this call is last as it cleans up theory core
00113     res = d_commonRules->transitivityRule(res, d_core->callTheoryPreprocess(res.getRHS()));
00114   }
00115   d_core->clearInPP();
00116   return res;
00117 }
00118 
00119 
00120 Theorem ExprTransform::preprocess(const Theorem& thm)
00121 {
00122   return d_commonRules->iffMP(thm, preprocess(thm.getExpr()));
00123 }
00124 
00125 
00126 // We assume that the cache is initially empty
00127 Theorem ExprTransform::pushNegation(const Expr& e) {
00128   if(e.isTerm()) return d_commonRules->reflexivityRule(e);
00129   Theorem res(pushNegationRec(e, false));
00130   d_pushNegCache.clear();
00131   return res;
00132 }
00133 
00134 
00135 // Recursively descend into the expression e, keeping track of whether
00136 // we are under even or odd number of negations ('neg' == true means
00137 // odd, the context is "negative").
00138 
00139 // Produce a proof of e <==> e' or !e <==> e', depending on whether
00140 // neg is false or true, respectively.
00141 Theorem ExprTransform::pushNegationRec(const Expr& e, bool neg) {
00142   TRACE("pushNegation", "pushNegationRec(", e,
00143   ", neg=" + string(neg? "true":"false") + ") {");
00144   DebugAssert(!e.isTerm(), "pushNegationRec: not boolean e = "+e.toString());
00145   ExprMap<Theorem>::iterator i = d_pushNegCache.find(neg? !e : e);
00146   if(i != d_pushNegCache.end()) { // Found cached result
00147     TRACE("pushNegation", "pushNegationRec [cached] => ", (*i).second, "}");
00148     return (*i).second;
00149   }
00150   // By default, do not rewrite
00151   Theorem res(d_core->reflexivityRule((neg)? !e : e));
00152   if(neg) {
00153     switch(e.getKind()) {
00154       case TRUE_EXPR: res = d_commonRules->rewriteNotTrue(!e); break;
00155       case FALSE_EXPR: res = d_commonRules->rewriteNotFalse(!e); break;
00156       case NOT: 
00157         res = pushNegationRec(d_commonRules->rewriteNotNot(!e), false);
00158         break;
00159       case AND:
00160         res = pushNegationRec(d_rules->rewriteNotAnd(!e), false);
00161         break;
00162       case OR: 
00163         res = pushNegationRec(d_rules->rewriteNotOr(!e), false);
00164         break;
00165       case IMPLIES: {
00166         vector<Theorem> thms;
00167         thms.push_back(d_rules->rewriteImplies(e));
00168         res = pushNegationRec
00169           (d_commonRules->substitutivityRule(NOT, thms), true);
00170         break;
00171       }
00172 //       case IFF:
00173 //  // Preserve equivalences to explore structural similarities
00174 //  if(e[0].getKind() == e[1].getKind())
00175 //    res = d_commonRules->reflexivityRule(!e);
00176 //  else
00177 //    res = pushNegationRec(d_commonRules->rewriteNotIff(!e), false);
00178 //         break;
00179       case ITE:
00180         res = pushNegationRec(d_rules->rewriteNotIte(!e), false);
00181         break;
00182 
00183       // Replace LETDECL with its definition.  The
00184       // typechecker makes sure it's type-safe to do so.
00185       case LETDECL: {
00186         vector<Theorem> thms;
00187         thms.push_back(d_rules->rewriteLetDecl(e));
00188         res = pushNegationRec
00189           (d_commonRules->substitutivityRule(NOT, thms), true);
00190         break;
00191       }
00192       default:
00193         res = d_commonRules->reflexivityRule(!e);
00194     } // end of switch(e.getKind())
00195   } else { // if(!neg)
00196     switch(e.getKind()) {
00197       case NOT: res = pushNegationRec(e[0], true); break;
00198       case AND:
00199       case OR:
00200       case IFF:
00201       case ITE: {
00202         Op op = e.getOp();
00203         vector<Theorem> thms;
00204         for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
00205           thms.push_back(pushNegationRec(*i, false));
00206         res = d_commonRules->substitutivityRule(op, thms);
00207         break;
00208       }
00209       case IMPLIES:
00210         res = pushNegationRec(d_rules->rewriteImplies(e), false);
00211         break;
00212       case LETDECL:
00213         res = pushNegationRec(d_rules->rewriteLetDecl(e), false);
00214         break;
00215       default:
00216         res = d_commonRules->reflexivityRule(e);
00217     } // end of switch(e.getKind())
00218   }
00219   TRACE("pushNegation", "pushNegationRec => ", res, "}");
00220   d_pushNegCache[neg? !e : e] = res;
00221   return res;
00222 }
00223 
00224 
00225 Theorem ExprTransform::pushNegationRec(const Theorem& thm, bool neg) {
00226   DebugAssert(thm.isRewrite(), "pushNegationRec(Theorem): bad theorem: "
00227         + thm.toString());
00228   Expr e(thm.getRHS());
00229   if(neg) {
00230     DebugAssert(e.isNot(), 
00231     "pushNegationRec(Theorem, neg = true): bad Theorem: "
00232     + thm.toString());
00233     e = e[0];
00234   }
00235   return d_commonRules->transitivityRule(thm, pushNegationRec(e, neg));
00236 }
00237 
00238 
00239 Theorem ExprTransform::pushNegation1(const Expr& e) {
00240   TRACE("pushNegation1", "pushNegation1(", e, ") {");
00241   DebugAssert(e.isNot(), "pushNegation1("+e.toString()+")");
00242   Theorem res;
00243   switch(e[0].getKind()) {
00244     case TRUE_EXPR: res = d_commonRules->rewriteNotTrue(e); break;
00245     case FALSE_EXPR: res = d_commonRules->rewriteNotFalse(e); break;
00246     case NOT: 
00247       res = d_commonRules->rewriteNotNot(e);
00248       break;
00249     case AND:
00250       res = d_rules->rewriteNotAnd(e);
00251       break;
00252     case OR: 
00253       res = d_rules->rewriteNotOr(e);
00254       break;
00255     case IMPLIES: {
00256       vector<Theorem> thms;
00257       thms.push_back(d_rules->rewriteImplies(e[0]));
00258       res = d_commonRules->substitutivityRule(e.getOp(), thms);
00259       res = d_commonRules->transitivityRule(res, d_rules->rewriteNotOr(res.getRHS()));
00260       break;
00261     }
00262     case ITE:
00263       res = d_rules->rewriteNotIte(e);
00264       break;
00265       // Replace LETDECL with its definition.  The
00266       // typechecker makes sure it's type-safe to do so.
00267     case LETDECL: {
00268       vector<Theorem> thms;
00269       thms.push_back(d_rules->rewriteLetDecl(e[0]));
00270       res = d_commonRules->substitutivityRule(e.getOp(), thms);
00271       res = d_commonRules->transitivityRule(res, pushNegation1(res.getRHS()));
00272       break;
00273     }
00274     default:
00275       res = d_commonRules->reflexivityRule(e);
00276   }
00277   TRACE("pushNegation1", "pushNegation1 => ", res.getExpr(), " }");
00278   return res;
00279 }
00280 
00281 
00282 Theorem ExprTransform::newPP(const Expr& e, int& budget)
00283 {
00284   if (!e.getType().isBool()) return d_commonRules->reflexivityRule(e);
00285   d_newPPCache.clear();
00286   Theorem thm = newPPrec(e, budget);
00287   //  cout << "budget = " << budget << endl;
00288   if (budget > d_budgetLimit ||
00289       thm.getRHS().getSize() > 2 * e.getSize()) {
00290     return d_commonRules->reflexivityRule(e);
00291   }
00292   return thm;
00293 }
00294 
00295 
00296 Theorem ExprTransform::specialSimplify(const Expr& e, ExprHashMap<Theorem>& cache)
00297 {
00298   if (e.isAtomic()) return d_commonRules->reflexivityRule(e);
00299 
00300   ExprHashMap<Theorem>::iterator it = cache.find(e);
00301   if (it != cache.end()) return (*it).second;
00302 
00303   Theorem thm;
00304   if (e.getType().isBool()) {
00305     thm = d_core->simplify(e);
00306     if (thm.getRHS().isBoolConst()) {
00307       cache[e] = thm;
00308       return thm;
00309     }
00310   }
00311 
00312   thm = d_commonRules->reflexivityRule(e);
00313 
00314   vector<Theorem> newChildrenThm;
00315   vector<unsigned> changed;
00316   int ar = e.arity();
00317   for(int k = 0; k < ar; ++k) {
00318     // Recursively process the kids
00319     Theorem thm2 = specialSimplify(e[k], cache);
00320     if (!thm2.isRefl()) {
00321       newChildrenThm.push_back(thm2);
00322       changed.push_back(k);
00323     }
00324   }
00325   if(changed.size() > 0) {
00326     thm = d_commonRules->substitutivityRule(e, changed, newChildrenThm);
00327   }
00328 
00329   cache[e] = thm;
00330   return thm;
00331 }
00332 
00333 
00334 Theorem ExprTransform::newPPrec(const Expr& e, int& budget)
00335 {
00336   DebugAssert(e.getType().isBool(), "Expected Boolean expression");
00337   Theorem res = d_commonRules->reflexivityRule(e);
00338 
00339   if (!e.containsTermITE()) return res;
00340 
00341   ExprMap<Theorem>::iterator i = d_newPPCache.find(e);
00342   if (i != d_newPPCache.end()) { // Found cached result
00343     res = (*i).second;
00344     return res;
00345   }
00346 
00347   Expr current = e;
00348   Expr newExpr;
00349   Theorem thm, thm2;
00350 
00351   do {
00352 
00353     if (budget > d_budgetLimit) break;
00354 
00355     ++budget;
00356     // Recursive case
00357     if (!current.isPropAtom()) {
00358       vector<Theorem> newChildrenThm;
00359       vector<unsigned> changed;
00360       int ar = current.arity();
00361       for(int k = 0; k < ar; ++k) {
00362         // Recursively process the kids
00363         thm = newPPrec(current[k], budget);
00364         if (!thm.isRefl()) {
00365           newChildrenThm.push_back(thm);
00366           changed.push_back(k);
00367         }
00368       }
00369       if(changed.size() > 0) {
00370         thm = d_commonRules->transitivityRule(res, d_commonRules->substitutivityRule(current, changed, newChildrenThm));
00371         newExpr = thm.getRHS();
00372         res = thm;
00373       }
00374       break;
00375     }
00376 
00377 //     if (current.getSize() > 1000) {
00378 //       break;
00379 //     }
00380 
00381     // Contains Term ITEs
00382 
00383     thm = d_commonRules->transitivityRule(res, d_commonRules->liftOneITE(current));
00384     newExpr = thm.getRHS();
00385 
00386     if ((newExpr[0].isLiteral() || newExpr[0].isAnd())) {
00387       d_core->getCM()->push();
00388       d_core->addFact(d_commonRules->assumpRule(newExpr[0]));
00389       thm2 = d_core->simplify(newExpr[1]);
00390       thm = d_commonRules->transitivityRule(thm, d_rules->rewriteIteThen(newExpr, thm2));
00391       d_core->getCM()->pop();
00392 
00393       d_core->getCM()->push();
00394       d_core->addFact(d_commonRules->assumpRule(newExpr[0].negate()));
00395 
00396       thm2 = d_core->simplify(newExpr[2]);
00397       newExpr = thm.getRHS();
00398       thm = d_commonRules->transitivityRule(thm, d_rules->rewriteIteElse(newExpr, thm2));
00399       d_core->getCM()->pop();
00400       newExpr = thm.getRHS();
00401     }
00402     res = thm;
00403     current = newExpr;
00404 
00405   } while (current.containsTermITE());
00406 
00407   d_newPPCache[e] = res;
00408   return res;
00409   
00410 }
00411 
00412 
00413 void ExprTransform::updateQueue(ExprMap<set<Expr>* >& queue,
00414                                 const Expr& e,
00415                                 const set<Expr>& careSet)
00416 {
00417   ExprMap<set<Expr>* >::iterator it = queue.find(e), iend = queue.end();
00418 
00419   if (it != iend) {
00420 
00421     set<Expr>* cs2 = (*it).second;
00422     set<Expr>* csNew = new set<Expr>;
00423     set_intersection(careSet.begin(), careSet.end(), cs2->begin(), cs2->end(),
00424                      inserter(*csNew, csNew->begin()));
00425     (*it).second = csNew;
00426     delete cs2;
00427   }
00428   else {
00429     queue[e] = new set<Expr>(careSet);
00430   }
00431 }
00432 
00433 
00434 Theorem ExprTransform::substitute(const Expr& e,
00435                                   ExprHashMap<Theorem>& substTable,
00436                                   ExprHashMap<Theorem>& cache)
00437 {
00438   if (e.isAtomic()) return d_commonRules->reflexivityRule(e);
00439 
00440   // check cache
00441 
00442   ExprHashMap<Theorem>::iterator it = cache.find(e), iend = cache.end();
00443   if (it != iend) {
00444     return it->second;
00445   }
00446 
00447   // do substitution?
00448 
00449   it = substTable.find(e);
00450   iend = substTable.end();
00451   if (it != iend) {
00452     return d_commonRules->transitivityRule(it->second, substitute(it->second.getRHS(), substTable, cache));
00453   }
00454 
00455   Theorem res = d_commonRules->reflexivityRule(e);
00456   int ar = e.arity();
00457   if (ar > 0) {
00458     vector<Theorem> newChildrenThm;
00459     vector<unsigned> changed;
00460     for(int k = 0; k < ar; ++k) {
00461       Theorem thm = substitute(e[k], substTable, cache);
00462       if (!thm.isRefl()) {
00463         newChildrenThm.push_back(thm);
00464         changed.push_back(k);
00465       }
00466     }
00467     if(changed.size() > 0) {
00468       res = d_commonRules->substitutivityRule(e, changed, newChildrenThm);
00469     }
00470   }
00471   cache[e] = res;
00472   return res;
00473 }
00474 
00475 
00476 Theorem ExprTransform::simplifyWithCare(const Expr& e)
00477 {
00478   ExprHashMap<Theorem> substTable;
00479   ExprMap<set<Expr>* > queue;
00480   ExprMap<set<Expr>* >::iterator it;
00481   set<Expr> cs;
00482   updateQueue(queue, e, cs);
00483 
00484   Expr v;
00485   bool done;
00486   Theorem thm;
00487   int i;
00488 
00489   while (!queue.empty()) {
00490     it = queue.end();
00491     --it;
00492     v = it->first;
00493     cs = *(it->second);
00494     delete it->second;
00495     queue.erase(v);
00496 
00497     if (v.isAtomic() || v.isAtomicFormula()) {
00498 
00499 // Unfortunately, this can lead to incompleteness bugs
00500 
00501 //       d_core->getCM()->push();
00502 //       set<Expr>::iterator iCare = cs.begin(), iCareEnd = cs.end();
00503 //       for (; iCare != iCareEnd; ++iCare) {
00504 //         d_core->addFact(d_commonRules->assumpRule((*iCare)));
00505 //       }
00506 //       thm = d_core->simplify(v);
00507 //       if (!thm.isRefl()) {
00508 //         substTable[v] = d_rules->dummyTheorem(thm.getExpr());
00509 //       }
00510 //       d_core->getCM()->pop();
00511       continue;
00512     }
00513 
00514     if (false && v.isPropAtom() && d_core->theoryOf(v) == d_theoryArith &&
00515         d_theoryArith->leavesAreNumConst(v)) {
00516       Expr vNew = v;
00517       thm = d_commonRules->reflexivityRule(vNew);
00518       while (vNew.containsTermITE()) {
00519         thm = d_commonRules->transitivityRule(thm, d_commonRules->liftOneITE(vNew));
00520         DebugAssert(!thm.isRefl(), "Expected non-reflexive");
00521         thm = d_commonRules->transitivityRule(thm, d_rules->rewriteIteCond(thm.getRHS()));
00522         thm = d_commonRules->transitivityRule(thm, d_core->simplify(thm.getRHS()));
00523         vNew = thm.getRHS();
00524       }
00525       substTable[v] = thm;
00526       continue;
00527     }
00528 
00529     done = false;
00530     set<Expr>::iterator iCare, iCareEnd = cs.end();
00531 
00532     switch (v.getKind()) {
00533       case ITE: {
00534         iCare = cs.find(v[0]);
00535         if (iCare != iCareEnd) {
00536           Expr rewrite = v.getType().isBool() ? v.iffExpr(v[1]) : v.eqExpr(v[1]);
00537           substTable[v] = d_rules->dummyTheorem(rewrite);
00538           updateQueue(queue, v[1], cs);
00539           done = true;
00540           break;
00541         }
00542         else {
00543           iCare = cs.find(v[0].negate());
00544           if (iCare != iCareEnd) {
00545             Expr rewrite = v.getType().isBool() ? v.iffExpr(v[2]) : v.eqExpr(v[2]);
00546             substTable[v] = d_rules->dummyTheorem(rewrite);
00547             updateQueue(queue, v[2], cs);
00548             done = true;
00549             break;
00550           }
00551         }
00552         updateQueue(queue, v[0], cs);
00553         cs.insert(v[0]);
00554         updateQueue(queue, v[1], cs);
00555         cs.erase(v[0]);
00556         cs.insert(v[0].negate());
00557         updateQueue(queue, v[2], cs);
00558         done = true;
00559         break;
00560       }
00561       case AND: {
00562         for (i = 0; i < v.arity(); ++i) {
00563           iCare = cs.find(v[i].negate());
00564           if (iCare != iCareEnd) {
00565             Expr rewrite = v.iffExpr(d_core->getEM()->falseExpr());
00566             substTable[v] = d_rules->dummyTheorem(rewrite);
00567             done = true;
00568             break;
00569           }
00570         }
00571         if (done) break;
00572 
00573         DebugAssert(v.arity() > 1, "Expected arity > 1");
00574         cs.insert(v[1]);
00575         updateQueue(queue, v[0], cs);
00576         cs.erase(v[1]);
00577         cs.insert(v[0]);
00578         for (i = 1; i < v.arity(); ++i) {
00579           updateQueue(queue, v[i], cs);
00580         }
00581         done = true;
00582         break;
00583       }
00584       case OR: {
00585         for (i = 0; i < v.arity(); ++i) {
00586           iCare = cs.find(v[i]);
00587           if (iCare != iCareEnd) {
00588             Expr rewrite = v.iffExpr(d_core->getEM()->trueExpr());
00589             substTable[v] = d_rules->dummyTheorem(rewrite);
00590             done = true;
00591             break;
00592           }
00593         }
00594         if (done) break;
00595         DebugAssert(v.arity() > 1, "Expected arity > 1");
00596         cs.insert(v[1].negate());
00597         updateQueue(queue, v[0], cs);
00598         cs.erase(v[1].negate());
00599         cs.insert(v[0].negate());
00600         for (i = 1; i < v.arity(); ++i) {
00601           updateQueue(queue, v[i], cs);
00602         }
00603         done = true;
00604         break;
00605       }
00606       default:
00607         break;
00608     }
00609 
00610     if (done) continue;
00611 
00612     for (int i = 0; i < v.arity(); ++i) {
00613       updateQueue(queue, v[i], cs);
00614     }
00615   }
00616   ExprHashMap<Theorem> cache;
00617   return substitute(e, substTable, cache);
00618 }
00619 

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2