1 /*****************************************************************************/
2 /*!
3 * \file expr_transform.cpp
4 *
5 * Author: Ying Hu, Clark Barrett
6 *
7 * Created: Jun 05 2003
8 *
9 * <hr>
10 *
11 * License to use, copy, modify, sell and/or distribute this software
12 * and its documentation for any purpose is hereby granted without
13 * royalty, subject to the terms and conditions defined in the \ref
14 * LICENSE file provided with this distribution.
15 *
16 * <hr>
17 *
18 */
19 /*****************************************************************************/
20
21
22 #include "expr_transform.h"
23 #include "theory_core.h"
24 #include "theory_arith.h"
25 #include "command_line_flags.h"
26 #include "core_proof_rules.h"
27 #include <set>
28
29
30 using namespace std;
31 using namespace CVC3;
32
33
ExprTransform(TheoryCore * core)34 ExprTransform::ExprTransform(TheoryCore* core)
35 : d_core(core)
36 {
37 d_commonRules = d_core->getCommonRules();
38 d_rules = d_core->getCoreRules();
39 }
40
41
smartSimplify(const Expr & e,ExprMap<bool> & cache)42 Theorem ExprTransform::smartSimplify(const Expr& e, ExprMap<bool>& cache)
43 {
44 ExprMap<bool>::iterator it;
45 vector<Expr> operatorStack;
46 vector<int> childStack;
47 Expr e2;
48
49 operatorStack.push_back(e);
50 childStack.push_back(0);
51
52 while (!operatorStack.empty()) {
53 DebugAssert(operatorStack.size() == childStack.size(), "Invariant violated");
54 if (childStack.back() < operatorStack.back().arity()) {
55 e2 = operatorStack.back()[childStack.back()++];
56 it = cache.find(e2);
57 if (it != cache.end() || e2.hasFind() ||
58 e2.validSimpCache() || e2.arity() == 0) continue;
59 if (operatorStack.size() >= 5000) {
60 smartSimplify(e2, cache);
61 cache[e2] = true;
62 }
63 else {
64 operatorStack.push_back(e2);
65 childStack.push_back(0);
66 }
67 }
68 else {
69 cache[operatorStack.back()] = true;
70 operatorStack.pop_back();
71 childStack.pop_back();
72 }
73 }
74 DebugAssert(childStack.empty(), "Invariant violated");
75 return d_core->simplify(e);
76 }
77
78
preprocess(const Expr & e)79 Theorem ExprTransform::preprocess(const Expr& e)
80 {
81 // Force simplifier to run
82 d_core->getEM()->invalidateSimpCache();
83 d_core->setInPP();
84 Theorem res = d_commonRules->reflexivityRule(e);
85
86 if (d_core->getFlags()["preprocess"].getBool()) {
87 if (d_core->getFlags()["pp-pushneg"].getBool()) {
88 res = pushNegation(e);
89 }
90 ExprMap<bool> cache;
91 if (d_core->getFlags()["pp-bryant"].getBool()) {
92 res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
93 res = d_commonRules->transitivityRule(res, dobryant(res.getRHS()));
94 }
95 if (d_core->getFlags()["pp-care"].getBool()) {
96 res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
97 res = d_commonRules->transitivityRule(res, simplifyWithCare(res.getRHS()));
98 }
99 int budget = 0;
100 d_budgetLimit = d_core->getFlags()["pp-budget"].getInt();
101 while (budget < d_budgetLimit) {
102 res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
103 Theorem ppRes = newPP(res.getRHS(), budget);
104 if (ppRes.isRefl()) break;
105 res = d_commonRules->transitivityRule(res, ppRes);
106 if (d_core->getFlags()["pp-care"].getBool()) {
107 res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
108 res = d_commonRules->transitivityRule(res, simplifyWithCare(res.getRHS()));
109 }
110 }
111 res = d_commonRules->transitivityRule(res, smartSimplify(res.getRHS(), cache));
112 // Make sure this call is last as it cleans up theory core
113 res = d_commonRules->transitivityRule(res, d_core->callTheoryPreprocess(res.getRHS()));
114 }
115 d_core->clearInPP();
116 return res;
117 }
118
119
preprocess(const Theorem & thm)120 Theorem ExprTransform::preprocess(const Theorem& thm)
121 {
122 return d_commonRules->iffMP(thm, preprocess(thm.getExpr()));
123 }
124
125
126 // We assume that the cache is initially empty
pushNegation(const Expr & e)127 Theorem ExprTransform::pushNegation(const Expr& e) {
128 if(e.isTerm()) return d_commonRules->reflexivityRule(e);
129 Theorem res(pushNegationRec(e, false));
130 d_pushNegCache.clear();
131 return res;
132 }
133
134
135 // Recursively descend into the expression e, keeping track of whether
136 // we are under even or odd number of negations ('neg' == true means
137 // odd, the context is "negative").
138
139 // Produce a proof of e <==> e' or !e <==> e', depending on whether
140 // neg is false or true, respectively.
pushNegationRec(const Expr & e,bool neg)141 Theorem ExprTransform::pushNegationRec(const Expr& e, bool neg) {
142 TRACE("pushNegation", "pushNegationRec(", e,
143 ", neg=" + string(neg? "true":"false") + ") {");
144 DebugAssert(!e.isTerm(), "pushNegationRec: not boolean e = "+e.toString());
145 ExprMap<Theorem>::iterator i = d_pushNegCache.find(neg? !e : e);
146 if(i != d_pushNegCache.end()) { // Found cached result
147 TRACE("pushNegation", "pushNegationRec [cached] => ", (*i).second, "}");
148 return (*i).second;
149 }
150 // By default, do not rewrite
151 Theorem res(d_core->reflexivityRule((neg)? !e : e));
152 if(neg) {
153 switch(e.getKind()) {
154 case TRUE_EXPR: res = d_commonRules->rewriteNotTrue(!e); break;
155 case FALSE_EXPR: res = d_commonRules->rewriteNotFalse(!e); break;
156 case NOT:
157 res = pushNegationRec(d_commonRules->rewriteNotNot(!e), false);
158 break;
159 case AND:
160 res = pushNegationRec(d_rules->rewriteNotAnd(!e), false);
161 break;
162 case OR:
163 res = pushNegationRec(d_rules->rewriteNotOr(!e), false);
164 break;
165 case IMPLIES: {
166 vector<Theorem> thms;
167 thms.push_back(d_rules->rewriteImplies(e));
168 res = pushNegationRec
169 (d_commonRules->substitutivityRule(NOT, thms), true);
170 break;
171 }
172 // case IFF:
173 // // Preserve equivalences to explore structural similarities
174 // if(e[0].getKind() == e[1].getKind())
175 // res = d_commonRules->reflexivityRule(!e);
176 // else
177 // res = pushNegationRec(d_commonRules->rewriteNotIff(!e), false);
178 // break;
179 case ITE:
180 res = pushNegationRec(d_rules->rewriteNotIte(!e), false);
181 break;
182
183 // Replace LETDECL with its definition. The
184 // typechecker makes sure it's type-safe to do so.
185 case LETDECL: {
186 vector<Theorem> thms;
187 thms.push_back(d_rules->rewriteLetDecl(e));
188 res = pushNegationRec
189 (d_commonRules->substitutivityRule(NOT, thms), true);
190 break;
191 }
192 default:
193 res = d_commonRules->reflexivityRule(!e);
194 } // end of switch(e.getKind())
195 } else { // if(!neg)
196 switch(e.getKind()) {
197 case NOT: res = pushNegationRec(e[0], true); break;
198 case AND:
199 case OR:
200 case IFF:
201 case ITE: {
202 Op op = e.getOp();
203 vector<Theorem> thms;
204 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
205 thms.push_back(pushNegationRec(*i, false));
206 res = d_commonRules->substitutivityRule(op, thms);
207 break;
208 }
209 case IMPLIES:
210 res = pushNegationRec(d_rules->rewriteImplies(e), false);
211 break;
212 case LETDECL:
213 res = pushNegationRec(d_rules->rewriteLetDecl(e), false);
214 break;
215 default:
216 res = d_commonRules->reflexivityRule(e);
217 } // end of switch(e.getKind())
218 }
219 TRACE("pushNegation", "pushNegationRec => ", res, "}");
220 d_pushNegCache[neg? !e : e] = res;
221 return res;
222 }
223
224
pushNegationRec(const Theorem & thm,bool neg)225 Theorem ExprTransform::pushNegationRec(const Theorem& thm, bool neg) {
226 DebugAssert(thm.isRewrite(), "pushNegationRec(Theorem): bad theorem: "
227 + thm.toString());
228 Expr e(thm.getRHS());
229 if(neg) {
230 DebugAssert(e.isNot(),
231 "pushNegationRec(Theorem, neg = true): bad Theorem: "
232 + thm.toString());
233 e = e[0];
234 }
235 return d_commonRules->transitivityRule(thm, pushNegationRec(e, neg));
236 }
237
238
pushNegation1(const Expr & e)239 Theorem ExprTransform::pushNegation1(const Expr& e) {
240 TRACE("pushNegation1", "pushNegation1(", e, ") {");
241 DebugAssert(e.isNot(), "pushNegation1("+e.toString()+")");
242 Theorem res;
243 switch(e[0].getKind()) {
244 case TRUE_EXPR: res = d_commonRules->rewriteNotTrue(e); break;
245 case FALSE_EXPR: res = d_commonRules->rewriteNotFalse(e); break;
246 case NOT:
247 res = d_commonRules->rewriteNotNot(e);
248 break;
249 case AND:
250 res = d_rules->rewriteNotAnd(e);
251 break;
252 case OR:
253 res = d_rules->rewriteNotOr(e);
254 break;
255 case IMPLIES: {
256 vector<Theorem> thms;
257 thms.push_back(d_rules->rewriteImplies(e[0]));
258 res = d_commonRules->substitutivityRule(e.getOp(), thms);
259 res = d_commonRules->transitivityRule(res, d_rules->rewriteNotOr(res.getRHS()));
260 break;
261 }
262 case ITE:
263 res = d_rules->rewriteNotIte(e);
264 break;
265 // Replace LETDECL with its definition. The
266 // typechecker makes sure it's type-safe to do so.
267 case LETDECL: {
268 vector<Theorem> thms;
269 thms.push_back(d_rules->rewriteLetDecl(e[0]));
270 res = d_commonRules->substitutivityRule(e.getOp(), thms);
271 res = d_commonRules->transitivityRule(res, pushNegation1(res.getRHS()));
272 break;
273 }
274 default:
275 res = d_commonRules->reflexivityRule(e);
276 }
277 TRACE("pushNegation1", "pushNegation1 => ", res.getExpr(), " }");
278 return res;
279 }
280
281
newPP(const Expr & e,int & budget)282 Theorem ExprTransform::newPP(const Expr& e, int& budget)
283 {
284 if (!e.getType().isBool()) return d_commonRules->reflexivityRule(e);
285 d_newPPCache.clear();
286 Theorem thm = newPPrec(e, budget);
287 // cout << "budget = " << budget << endl;
288 if (budget > d_budgetLimit ||
289 thm.getRHS().getSize() > 2 * e.getSize()) {
290 return d_commonRules->reflexivityRule(e);
291 }
292 return thm;
293 }
294
295
specialSimplify(const Expr & e,ExprHashMap<Theorem> & cache)296 Theorem ExprTransform::specialSimplify(const Expr& e, ExprHashMap<Theorem>& cache)
297 {
298 if (e.isAtomic()) return d_commonRules->reflexivityRule(e);
299
300 ExprHashMap<Theorem>::iterator it = cache.find(e);
301 if (it != cache.end()) return (*it).second;
302
303 Theorem thm;
304 if (e.getType().isBool()) {
305 thm = d_core->simplify(e);
306 if (thm.getRHS().isBoolConst()) {
307 cache[e] = thm;
308 return thm;
309 }
310 }
311
312 thm = d_commonRules->reflexivityRule(e);
313
314 vector<Theorem> newChildrenThm;
315 vector<unsigned> changed;
316 int ar = e.arity();
317 for(int k = 0; k < ar; ++k) {
318 // Recursively process the kids
319 Theorem thm2 = specialSimplify(e[k], cache);
320 if (!thm2.isRefl()) {
321 newChildrenThm.push_back(thm2);
322 changed.push_back(k);
323 }
324 }
325 if(changed.size() > 0) {
326 thm = d_commonRules->substitutivityRule(e, changed, newChildrenThm);
327 }
328
329 cache[e] = thm;
330 return thm;
331 }
332
333
newPPrec(const Expr & e,int & budget)334 Theorem ExprTransform::newPPrec(const Expr& e, int& budget)
335 {
336 DebugAssert(e.getType().isBool(), "Expected Boolean expression");
337 Theorem res = d_commonRules->reflexivityRule(e);
338
339 if (!e.containsTermITE()) return res;
340
341 ExprMap<Theorem>::iterator i = d_newPPCache.find(e);
342 if (i != d_newPPCache.end()) { // Found cached result
343 res = (*i).second;
344 return res;
345 }
346
347 Expr current = e;
348 Expr newExpr;
349 Theorem thm, thm2;
350
351 do {
352
353 if (budget > d_budgetLimit) break;
354
355 ++budget;
356 // Recursive case
357 if (!current.isPropAtom()) {
358 vector<Theorem> newChildrenThm;
359 vector<unsigned> changed;
360 int ar = current.arity();
361 for(int k = 0; k < ar; ++k) {
362 // Recursively process the kids
363 thm = newPPrec(current[k], budget);
364 if (!thm.isRefl()) {
365 newChildrenThm.push_back(thm);
366 changed.push_back(k);
367 }
368 }
369 if(changed.size() > 0) {
370 thm = d_commonRules->transitivityRule(res, d_commonRules->substitutivityRule(current, changed, newChildrenThm));
371 newExpr = thm.getRHS();
372 res = thm;
373 }
374 break;
375 }
376
377 // if (current.getSize() > 1000) {
378 // break;
379 // }
380
381 // Contains Term ITEs
382
383 thm = d_commonRules->transitivityRule(res, d_commonRules->liftOneITE(current));
384 newExpr = thm.getRHS();
385
386 if ((newExpr[0].isLiteral() || newExpr[0].isAnd())) {
387 d_core->getCM()->push();
388 d_core->addFact(d_commonRules->assumpRule(newExpr[0]));
389 thm2 = d_core->simplify(newExpr[1]);
390 thm = d_commonRules->transitivityRule(thm, d_rules->rewriteIteThen(newExpr, thm2));
391 d_core->getCM()->pop();
392
393 d_core->getCM()->push();
394 d_core->addFact(d_commonRules->assumpRule(newExpr[0].negate()));
395
396 thm2 = d_core->simplify(newExpr[2]);
397 newExpr = thm.getRHS();
398 thm = d_commonRules->transitivityRule(thm, d_rules->rewriteIteElse(newExpr, thm2));
399 d_core->getCM()->pop();
400 newExpr = thm.getRHS();
401 }
402 res = thm;
403 current = newExpr;
404
405 } while (current.containsTermITE());
406
407 d_newPPCache[e] = res;
408 return res;
409
410 }
411
412
updateQueue(ExprMap<set<Expr> * > & queue,const Expr & e,const set<Expr> & careSet)413 void ExprTransform::updateQueue(ExprMap<set<Expr>* >& queue,
414 const Expr& e,
415 const set<Expr>& careSet)
416 {
417 ExprMap<set<Expr>* >::iterator it = queue.find(e), iend = queue.end();
418
419 if (it != iend) {
420
421 set<Expr>* cs2 = (*it).second;
422 set<Expr>* csNew = new set<Expr>;
423 set_intersection(careSet.begin(), careSet.end(), cs2->begin(), cs2->end(),
424 inserter(*csNew, csNew->begin()));
425 (*it).second = csNew;
426 delete cs2;
427 }
428 else {
429 queue[e] = new set<Expr>(careSet);
430 }
431 }
432
433
substitute(const Expr & e,ExprHashMap<Theorem> & substTable,ExprHashMap<Theorem> & cache)434 Theorem ExprTransform::substitute(const Expr& e,
435 ExprHashMap<Theorem>& substTable,
436 ExprHashMap<Theorem>& cache)
437 {
438 if (e.isAtomic()) return d_commonRules->reflexivityRule(e);
439
440 // check cache
441
442 ExprHashMap<Theorem>::iterator it = cache.find(e), iend = cache.end();
443 if (it != iend) {
444 return it->second;
445 }
446
447 // do substitution?
448
449 it = substTable.find(e);
450 iend = substTable.end();
451 if (it != iend) {
452 return d_commonRules->transitivityRule(it->second, substitute(it->second.getRHS(), substTable, cache));
453 }
454
455 Theorem res = d_commonRules->reflexivityRule(e);
456 int ar = e.arity();
457 if (ar > 0) {
458 vector<Theorem> newChildrenThm;
459 vector<unsigned> changed;
460 for(int k = 0; k < ar; ++k) {
461 Theorem thm = substitute(e[k], substTable, cache);
462 if (!thm.isRefl()) {
463 newChildrenThm.push_back(thm);
464 changed.push_back(k);
465 }
466 }
467 if(changed.size() > 0) {
468 res = d_commonRules->substitutivityRule(e, changed, newChildrenThm);
469 }
470 }
471 cache[e] = res;
472 return res;
473 }
474
475
simplifyWithCare(const Expr & e)476 Theorem ExprTransform::simplifyWithCare(const Expr& e)
477 {
478 ExprHashMap<Theorem> substTable;
479 ExprMap<set<Expr>* > queue;
480 ExprMap<set<Expr>* >::iterator it;
481 set<Expr> cs;
482 updateQueue(queue, e, cs);
483
484 Expr v;
485 bool done;
486 Theorem thm;
487 int i;
488
489 while (!queue.empty()) {
490 it = queue.end();
491 --it;
492 v = it->first;
493 cs = *(it->second);
494 delete it->second;
495 queue.erase(v);
496
497 if (v.isAtomic() || v.isAtomicFormula()) {
498
499 // Unfortunately, this can lead to incompleteness bugs
500
501 // d_core->getCM()->push();
502 // set<Expr>::iterator iCare = cs.begin(), iCareEnd = cs.end();
503 // for (; iCare != iCareEnd; ++iCare) {
504 // d_core->addFact(d_commonRules->assumpRule((*iCare)));
505 // }
506 // thm = d_core->simplify(v);
507 // if (!thm.isRefl()) {
508 // substTable[v] = d_rules->dummyTheorem(thm.getExpr());
509 // }
510 // d_core->getCM()->pop();
511 continue;
512 }
513
514 if (false && v.isPropAtom() && d_core->theoryOf(v) == d_theoryArith &&
515 d_theoryArith->leavesAreNumConst(v)) {
516 Expr vNew = v;
517 thm = d_commonRules->reflexivityRule(vNew);
518 while (vNew.containsTermITE()) {
519 thm = d_commonRules->transitivityRule(thm, d_commonRules->liftOneITE(vNew));
520 DebugAssert(!thm.isRefl(), "Expected non-reflexive");
521 thm = d_commonRules->transitivityRule(thm, d_rules->rewriteIteCond(thm.getRHS()));
522 thm = d_commonRules->transitivityRule(thm, d_core->simplify(thm.getRHS()));
523 vNew = thm.getRHS();
524 }
525 substTable[v] = thm;
526 continue;
527 }
528
529 done = false;
530 set<Expr>::iterator iCare, iCareEnd = cs.end();
531
532 switch (v.getKind()) {
533 case ITE: {
534 iCare = cs.find(v[0]);
535 if (iCare != iCareEnd) {
536 Expr rewrite = v.getType().isBool() ? v.iffExpr(v[1]) : v.eqExpr(v[1]);
537 substTable[v] = d_rules->dummyTheorem(rewrite);
538 updateQueue(queue, v[1], cs);
539 done = true;
540 break;
541 }
542 else {
543 iCare = cs.find(v[0].negate());
544 if (iCare != iCareEnd) {
545 Expr rewrite = v.getType().isBool() ? v.iffExpr(v[2]) : v.eqExpr(v[2]);
546 substTable[v] = d_rules->dummyTheorem(rewrite);
547 updateQueue(queue, v[2], cs);
548 done = true;
549 break;
550 }
551 }
552 updateQueue(queue, v[0], cs);
553 cs.insert(v[0]);
554 updateQueue(queue, v[1], cs);
555 cs.erase(v[0]);
556 cs.insert(v[0].negate());
557 updateQueue(queue, v[2], cs);
558 done = true;
559 break;
560 }
561 case AND: {
562 for (i = 0; i < v.arity(); ++i) {
563 iCare = cs.find(v[i].negate());
564 if (iCare != iCareEnd) {
565 Expr rewrite = v.iffExpr(d_core->getEM()->falseExpr());
566 substTable[v] = d_rules->dummyTheorem(rewrite);
567 done = true;
568 break;
569 }
570 }
571 if (done) break;
572
573 DebugAssert(v.arity() > 1, "Expected arity > 1");
574 cs.insert(v[1]);
575 updateQueue(queue, v[0], cs);
576 cs.erase(v[1]);
577 cs.insert(v[0]);
578 for (i = 1; i < v.arity(); ++i) {
579 updateQueue(queue, v[i], cs);
580 }
581 done = true;
582 break;
583 }
584 case OR: {
585 for (i = 0; i < v.arity(); ++i) {
586 iCare = cs.find(v[i]);
587 if (iCare != iCareEnd) {
588 Expr rewrite = v.iffExpr(d_core->getEM()->trueExpr());
589 substTable[v] = d_rules->dummyTheorem(rewrite);
590 done = true;
591 break;
592 }
593 }
594 if (done) break;
595 DebugAssert(v.arity() > 1, "Expected arity > 1");
596 cs.insert(v[1].negate());
597 updateQueue(queue, v[0], cs);
598 cs.erase(v[1].negate());
599 cs.insert(v[0].negate());
600 for (i = 1; i < v.arity(); ++i) {
601 updateQueue(queue, v[i], cs);
602 }
603 done = true;
604 break;
605 }
606 default:
607 break;
608 }
609
610 if (done) continue;
611
612 for (int i = 0; i < v.arity(); ++i) {
613 updateQueue(queue, v[i], cs);
614 }
615 }
616 ExprHashMap<Theorem> cache;
617 return substitute(e, substTable, cache);
618 }
619
620