Disabled arith-rewrite-equalities by default unless in a pure arithmetic theory

3 files changed, 24 insertions, 4 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 75b332314..73ad5bd40 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -430,6 +430,12 @@ void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
     Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
     NodeManager::currentNM()->getOptions()->doITESimp = iteSimp;
   }
+  // Turn on ite simplification only for pure arithmetic
+  if(! Options::current()->arithRewriteEqSetByUser) {
+    bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified();
+    Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
+    NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq;
+  }
 
 }
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 7c8a07489..46997a04d 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -114,7 +114,8 @@ Options::Options() :
   ufSymmetryBreaker(false),
   ufSymmetryBreakerSetByUser(false),
   dioSolver(true),
-  arithRewriteEq(true),
+  arithRewriteEq(false),
+  arithRewriteEqSetByUser(false),
   lemmaOutputChannel(NULL),
   lemmaInputChannel(NULL),
   threads(2),// default should be 1 probably, but say 2 for now
@@ -386,7 +387,8 @@ enum OptionValue {
   ARITHMETIC_PIVOT_THRESHOLD,
   ARITHMETIC_PROP_MAX_LENGTH,
   ARITHMETIC_DIO_SOLVER,
-  ARITHMETIC_REWRITE_EQUALITIES,
+  ENABLE_ARITHMETIC_REWRITE_EQUALITIES,
+  DISABLE_ARITHMETIC_REWRITE_EQUALITIES,
   ENABLE_SYMMETRY_BREAKER,
   DISABLE_SYMMETRY_BREAKER,
   PARALLEL_THREADS,
@@ -483,7 +485,8 @@ static struct option cmdlineOptions[] = {
   { "print-winner", no_argument     , NULL, PRINT_WINNER  },
   { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
-  { "disable-arith-rewrite-equalities", no_argument, NULL, ARITHMETIC_REWRITE_EQUALITIES },
+  { "enable-arith-rewrite-equalities", no_argument, NULL, ENABLE_ARITHMETIC_REWRITE_EQUALITIES },
+  { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES },
   { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER },
   { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
   { "threads", required_argument, NULL, PARALLEL_THREADS },
@@ -882,8 +885,14 @@ throw(OptionException) {
       dioSolver = false;
       break;
 
-    case ARITHMETIC_REWRITE_EQUALITIES:
+    case ENABLE_ARITHMETIC_REWRITE_EQUALITIES:
+      arithRewriteEq = true;
+      arithRewriteEqSetByUser = true;
+      break;
+
+    case DISABLE_ARITHMETIC_REWRITE_EQUALITIES:
       arithRewriteEq = false;
+      arithRewriteEqSetByUser = true;
       break;
 
     case ENABLE_SYMMETRY_BREAKER:
diff --git a/src/util/options.h b/src/util/options.h
index 3b6584727..fd09d4149 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -269,6 +269,11 @@ struct CVC4_PUBLIC Options {
    */
   bool arithRewriteEq;
 
+  /**
+   * Whether the flag was set by the user
+   */
+  bool arithRewriteEqSetByUser;
+
   /** The output channel to receive notfication events for new lemmas */
   LemmaOutputChannel* lemmaOutputChannel;
   LemmaInputChannel* lemmaInputChannel;