From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 18 Jun 2014 03:03:22 +0000 (-0400)
Subject: disable unate lemmas when using incremental mode
X-Git-Tag: cvc5-1.0.0~6773
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=875d0f0b01339aab4e60c408f1d7aa601e9653e6;p=cvc5.git

disable unate lemmas when using incremental mode
---

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();
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 10148e5bc..18931e3fa 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -147,7 +147,6 @@ BUG_TESTS = \
 	bug484.smt2 \
 	bug486.cvc \
 	bug507.smt2 \
-	bug512.smt2 \
 	bug512.minimized.smt2 \
 	bug516.smt2 \
 	bug519.smt2 \
@@ -162,6 +161,11 @@ BUG_TESTS = \
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
+# bug512 -- taking too long, --time-per not working perhaps? in any case,
+# we have a minimized version still getting tested
+DISABLED_TESTS = \
+	bug512.smt2
+
 EXTRA_DIST = $(TESTS) \
 	simplification_bug4.smt2.expect \
 	bug216.smt2.expect
@@ -175,7 +179,7 @@ TESTS += \
 endif
 
 # and make sure to distribute it
-EXTRA_DIST += \
+EXTRA_DIST += $(DISABLED_TESTS) \
 	subranges.cvc \
 	arrayinuf_error.smt2 \
 	errorcrash.smt2 \
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index c99c66fff..d117f5173 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -103,6 +103,7 @@ public:
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
+    d_smt->setOption("incremental", false);
     d_ctxt = d_smt->d_context;
     d_uctxt = d_smt->d_userContext;
     d_scope = new SmtScope(d_smt);