00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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
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
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
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
00136
00137
00138
00139
00140
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()) {
00147 TRACE("pushNegation", "pushNegationRec [cached] => ", (*i).second, "}");
00148 return (*i).second;
00149 }
00150
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
00173
00174
00175
00176
00177
00178
00179 case ITE:
00180 res = pushNegationRec(d_rules->rewriteNotIte(!e), false);
00181 break;
00182
00183
00184
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 }
00195 } else {
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 }
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
00266
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
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
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()) {
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
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
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
00378
00379
00380
00381
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
00441
00442 ExprHashMap<Theorem>::iterator it = cache.find(e), iend = cache.end();
00443 if (it != iend) {
00444 return it->second;
00445 }
00446
00447
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
00500
00501
00502
00503
00504
00505
00506
00507
00508
00509
00510
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