diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-09 15:21:22 -0700 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-09 15:21:22 -0700 |
commit | c15ff43597b41ea457befecb1b0e2402e28cb523 (patch) | |
tree | 54bcae42b1a8363eb37cb12512e7b0ede3687cbc /src/theory/theory_engine.cpp | |
parent | dd84403eb19b769d80b4c57ae690ba14c02df041 (diff) |
Re-enabling ite simplification in incremental mode - no reason why
it should be a problem.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f2231ff7a..1ab4c228b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1558,15 +1558,9 @@ void TheoryEngine::mkAckermanizationAsssertions(std::vector<Node>& assertions) { Node TheoryEngine::ppSimpITE(TNode assertion) { - if(options::incrementalSolving()){ - // disabling the d_iteUtilities->simpITE(assertion) pass for incremental solving. - // This is paranoia. We do not actually know of a bug coming from this. - // TODO re-enable + if (!d_iteRemover.containsTermITE(assertion)) { return assertion; - } else if(!d_iteRemover.containsTermITE(assertion)){ - return assertion; - }else{ - + } else { Node result = d_iteUtilities->simpITE(assertion); Node res_rewritten = Rewriter::rewrite(result); @@ -1576,10 +1570,9 @@ Node TheoryEngine::ppSimpITE(TNode assertion) Chat() << "ending simplifyWithCare()" << " post simplifyWithCare()" << postSimpWithCare.getId() << endl; result = Rewriter::rewrite(postSimpWithCare); - }else{ + } else { result = res_rewritten; } - return result; } } |