CVC3  2.4.1
expr_transform.cpp
Go to the documentation of this file.
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 
34 ExprTransform::ExprTransform(TheoryCore* core)
35  : d_core(core)
36 {
39 }
40 
41 
43 {
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 
80 {
81  // Force simplifier to run
83  d_core->setInPP();
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));
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));
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
114  }
115  d_core->clearInPP();
116  return res;
117 }
118 
119 
121 {
122  return d_commonRules->iffMP(thm, preprocess(thm.getExpr()));
123 }
124 
125 
126 // We assume that the cache is initially empty
128  if(e.isTerm()) return d_commonRules->reflexivityRule(e);
129  Theorem res(pushNegationRec(e, false));
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.
142  TRACE("pushNegation", "pushNegationRec(", e,
143  ", neg=" + string(neg? "true":"false") + ") {");
144  DebugAssert(!e.isTerm(), "pushNegationRec: not boolean e = "+e.toString());
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 
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 
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 
282 Theorem ExprTransform::newPP(const Expr& e, int& budget)
283 {
284  if (!e.getType().isBool()) return d_commonRules->reflexivityRule(e);
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 
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 
334 Theorem ExprTransform::newPPrec(const Expr& e, int& budget)
335 {
336  DebugAssert(e.getType().isBool(), "Expected Boolean expression");
338 
339  if (!e.containsTermITE()) return res;
340 
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 
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 
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 
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 
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 
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 &&
516  Expr vNew = v;
517  thm = d_commonRules->reflexivityRule(vNew);
518  while (vNew.containsTermITE()) {
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