From dcb4cc33b05f1d6c5307208f711dc5ad90a09041 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 17 Jun 2014 23:03:22 -0400 Subject: [PATCH] disable unate lemmas when using incremental mode --- src/theory/arith/cut_log.h | 4 +-- src/theory/arith/options_handlers.h | 8 +++--- src/theory/arith/theory_arith_private.cpp | 33 ++++++++++++----------- test/regress/regress0/Makefile.am | 8 ++++-- test/unit/theory/theory_arith_white.h | 1 + 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 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::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); -- 2.30.2