summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/theory/arith/cut_log.h4
-rw-r--r--src/theory/arith/options_handlers.h8
-rw-r--r--src/theory/arith/theory_arith_private.cpp33
-rw-r--r--test/regress/regress0/Makefile.am8
-rw-r--r--test/unit/theory/theory_arith_white.h1
5 files changed, 31 insertions, 23 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();
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback