From: Tim King <taking@cs.nyu.edu>
Date: Sat, 13 Jun 2015 22:51:19 +0000 (+0200)
Subject: Turning off aggressive arith ite simplifications during incremental solving.
X-Git-Tag: cvc5-1.0.0~6276
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d101e7fed051685673c13317cb45166ba5ef7798;p=cvc5.git

Turning off aggressive arith ite simplifications during incremental solving.
---

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 757dab8fb..2b31831e2 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -15,6 +15,7 @@
  ** \todo document this file
  **/
 
+#include "smt/options.h"
 #include "theory/arith/arith_ite_utils.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/arith_utilities.h"
@@ -272,6 +273,7 @@ void ArithIteUtils::addSubstitution(TNode f, TNode t){
 }
 
 Node ArithIteUtils::applySubstitutions(TNode f){
+  AlwaysAssert(!options::incrementalSolving());
   return d_subs->apply(f);
 }
 
@@ -285,6 +287,7 @@ Node ArithIteUtils::selectForCmp(Node n) const{
 }
 
 void ArithIteUtils::learnSubstitutions(const std::vector<Node>& assertions){
+  AlwaysAssert(!options::incrementalSolving());
   for(size_t i=0, N=assertions.size(); i < N; ++i){
     collectAssertions(assertions[i]);
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8d36d9e05..d34f0cd12 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1530,7 +1530,12 @@ void TheoryEngine::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
 
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
-  if(!d_iteRemover.containsTermITE(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
+    return assertion;
+  } else if(!d_iteRemover.containsTermITE(assertion)){
     return assertion;
   }else{
 
@@ -1575,7 +1580,8 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
   }
 
   // Do theory specific preprocessing passes
-  if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)){
+  if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)
+     && !options::incrementalSolving() ){
     if(!simpDidALotOfWork){
       ContainsTermITEVisitor& contains = *d_iteRemover.getContainsVisitor();
       arith::ArithIteUtils aiteu(contains, d_userContext, getModel());