diff options
| -rw-r--r-- | NEWS | 5 | ||||
| -rw-r--r-- | src/options/smt_options.toml | 2 | ||||
| -rw-r--r-- | src/smt/set_defaults.cpp | 13 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
| -rw-r--r-- | test/regress/regress1/strings/strings-leq-trans-unsat.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress2/nl/ufnia-factor-open-proof.smt2 | 1 |
6 files changed, 17 insertions, 10 deletions
@@ -4,6 +4,11 @@ Changes since 1.8 ================= New Features: + +* New unsat-core production modes based on the new proof infrastructure + (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature + of Minisat (`--unsat-cores-mode=assumptions`). The mode based on SAT + assumptions + preprocessing proofs is the new default. * A new parametric theory of sequences whose syntax is compatible with the syntax for sequences used by Z3. * Arrays: Added support for an `eqrange` predicate. `(eqrange a b i j)` is true diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 733c2239c..ddffe8c12 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -187,7 +187,7 @@ name = "SMT Layer" category = "regular" long = "produce-unsat-cores" type = "bool" - help = "turn on unsat core generation" + help = "turn on unsat core generation. Unless otherwise specified, cores will be produced using SAT soving under assumptions and preprocessing proofs." [[option]] name = "unsatCoresMode" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 7c5d775ed..be19923af 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -80,9 +80,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (opts.wasSetByUser(options::unsatCoresMode)) { Notice() - << "Overriding OFF unsat-core mode since cores were requested..\n"; + << "Overriding OFF unsat-core mode since cores were requested.\n"; } - opts.set(options::unsatCoresMode, options::UnsatCoresMode::OLD_PROOF); + opts.set(options::unsatCoresMode, options::UnsatCoresMode::ASSUMPTIONS); } if (options::checkProofs() || options::dumpProofs()) @@ -352,7 +352,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || options::sygusInference() || options::sygusRewSynthInput()) { // since we are trying to recast as sygus, we assume the input is sygus - isSygus = true; usesSygus = true; } else if (options::sygusInst()) @@ -397,7 +396,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.set(options::unsatCores, true); if (options::unsatCoresMode() == options::UnsatCoresMode::OFF) { - opts.set(options::unsatCoresMode, options::UnsatCoresMode::OLD_PROOF); + opts.set(options::unsatCoresMode, options::UnsatCoresMode::ASSUMPTIONS); } } @@ -415,9 +414,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // whether we want to force safe unsat cores, i.e., if we are in the OLD_PROOF - // unsat core mode, since new ones are experimental + // unsat core mode or ASSUMPTIONS, the new default, since other ones are + // experimental bool safeUnsatCores = - options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF; + options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF + || options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS; // Disable options incompatible with incremental solving, unsat cores or // output an error if enabled explicitly. It is also currently incompatible diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 67273f854..0e1ff8878 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1394,8 +1394,8 @@ UnsatCore SmtEngine::getUnsatCoreInternal() if (!d_env->getOption(options::unsatCores)) { throw ModalException( - "Cannot get an unsat core when produce-unsat-cores[-new] or " - "produce-proofs option is off."); + "Cannot get an unsat core when produce-unsat-cores or produce-proofs " + "option is off."); } if (d_state->getMode() != SmtMode::UNSAT) { diff --git a/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 index de3946ef0..a97863d7d 100644 --- a/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 +++ b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp +; COMMAND-LINE: --strings-exp --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_SLIA) (set-info :status unsat) diff --git a/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 b/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 index bcb077f4f..6d910b464 100644 --- a/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 +++ b/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-unsat-cores (set-logic QF_UFNIA) (set-info :status unsat) (declare-fun pow2 (Int) Int) |