disable unate lemmas when using incremental mode

3 files changed, 24 insertions, 21 deletions

diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 123313617..bbd1b3694 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -125,11 +125,11 @@ public:
 };
 std::ostream& operator<<(std::ostream& os, const CutInfo& ci);
 
-struct BranchCutInfo : public CutInfo {
+class BranchCutInfo : public CutInfo {
   BranchCutInfo(int execOrd, int br,  Kind dir, double val);
 };
 
-struct RowsDeleted : public CutInfo {
+class RowsDeleted : public CutInfo {
   RowsDeleted(int execOrd, int nrows, const int num[]);
 };
 
diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h
index f81f1b227..038baf79d 100644
--- a/src/theory/arith/options_handlers.h
+++ b/src/theory/arith/options_handlers.h
@@ -25,10 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-static const std::string arithPresolveLemmasHelp = "\
-Presolve lemmas are generated before SAT search begins using the relationship\n\
+static const std::string arithUnateLemmasHelp = "\
+Unate lemmas are generated before SAT search begins using the relationship\n\
 of constant terms and polynomials.\n\
-Modes currently supported by the --arith-presolve-lemmas option:\n\
+Modes currently supported by the --unate-lemmas option:\n\
 + none \n\
 + ineqs \n\
   Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
@@ -73,7 +73,7 @@ inline ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::
   } else if(optarg == "eqs") {
     return EQUALITY_PRESOLVE_LEMMAS;
   } else if(optarg == "help") {
-    puts(arithPresolveLemmasHelp.c_str());
+    puts(arithUnateLemmasHelp.c_str());
     exit(1);
   } else {
     throw OptionException(std::string("unknown option for --unate-lemmas: `") +
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index f3bdca7c7..b2eec924c 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -40,6 +40,7 @@
 
 #include "smt/logic_request.h"
 #include "smt/logic_exception.h"
+#include "smt/options.h"  // for incrementalSolving()
 
 #include "theory/arith/arithvar.h"
 #include "theory/arith/cut_log.h"
@@ -4212,21 +4213,23 @@ void TheoryArithPrivate::presolve(){
   }
 
   vector<Node> lemmas;
-  switch(options::arithUnateLemmaMode()){
-  case NO_PRESOLVE_LEMMAS:
-    break;
-  case INEQUALITY_PRESOLVE_LEMMAS:
-    d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
-    break;
-  case EQUALITY_PRESOLVE_LEMMAS:
-    d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
-    break;
-  case ALL_PRESOLVE_LEMMAS:
-    d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
-    d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
-    break;
-  default:
-    Unhandled(options::arithUnateLemmaMode());
+  if(!options::incrementalSolving()) {
+    switch(options::arithUnateLemmaMode()){
+    case NO_PRESOLVE_LEMMAS:
+      break;
+    case INEQUALITY_PRESOLVE_LEMMAS:
+      d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
+      break;
+    case EQUALITY_PRESOLVE_LEMMAS:
+      d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
+      break;
+    case ALL_PRESOLVE_LEMMAS:
+      d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
+      d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
+      break;
+    default:
+      Unhandled(options::arithUnateLemmaMode());
+    }
   }
 
   vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();