From: Haniel Barbosa Date: Wed, 19 May 2021 20:25:18 +0000 (-0300) Subject: Change the default unsat cores (#6571) X-Git-Tag: cvc5-1.0.0~1736 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=467a94cde962d90d3970c4378fc5f2b8a2476352;p=cvc5.git Change the default unsat cores (#6571) This commit changes the default unsat cores to those based on solving-under-assumptions in the SAT solver and the (new) preprocessing proofs. The evaluation below on all the non-fp non-incremental SMT-LIB benchmarks, 120s timeout, shows the differences of the unsat cores based on the old proofs, the new ones based on SAT assumptions + preprocessing proofs, and the new ones based on SAT and preprocessing proofs. Note that the union of the last two is on par with the first. ``` status total solved sat unsat best timeout memout error uniq disagr time_cpu memory benchmark config AUFDTLIRA newUnsatCoresAssumps-safe/ ee 35 4 0 4 4 7 0 23 2 0 954.0 1267.5 newUnsatCoresProofs ok 35 31 0 31 25 4 0 0 0 0 894.1 1692.9 oldUnsatCores ok 35 32 0 32 30 3 0 0 1 0 799.2 1428.5 AUFLIA newUnsatCoresAssumps-safe/ ok 11 7 0 7 7 4 0 0 7 0 532.2 7604.4 newUnsatCoresProofs ok 11 4 0 4 1 6 0 0 0 0 829.0 12459.8 oldUnsatCores ok 11 4 0 4 3 6 0 0 0 0 818.2 7764.4 AUFLIRA newUnsatCoresAssumps-safe/ to 2 0 0 0 0 2 0 0 0 0 241.6 125.6 newUnsatCoresProofs ok 2 2 0 2 1 0 0 0 0 0 54.2 45.5 oldUnsatCores ok 2 2 0 2 2 0 0 0 0 0 49.4 79.7 AUFNIRA newUnsatCoresAssumps-safe/ ok 10 5 0 5 5 5 0 0 2 0 748.4 1630.0 newUnsatCoresProofs ok 10 4 0 4 0 6 0 0 0 0 850.7 2978.8 oldUnsatCores ok 10 8 0 8 5 2 0 0 1 0 502.7 2048.5 BV newUnsatCoresAssumps-safe/ ok 7 1 1 0 1 6 0 0 1 0 734.2 2065.0 newUnsatCoresProofs ok 7 6 3 3 4 1 0 0 0 0 246.7 1023.9 oldUnsatCores ok 7 6 3 3 3 1 0 0 0 0 248.6 992.0 LIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.9 47.7 newUnsatCoresProofs ok 1 1 0 1 1 0 0 0 0 0 0.3 6.5 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 0.3 5.3 LRA newUnsatCoresAssumps-safe/ ok 5 3 0 3 3 2 0 0 3 0 450.7 260.4 newUnsatCoresProofs ok 5 2 0 2 0 3 0 0 0 0 537.8 424.5 oldUnsatCores ok 5 2 0 2 2 3 0 0 0 0 533.8 298.5 NIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.8 22.0 newUnsatCoresProofs ok 1 1 0 1 0 0 0 0 0 0 46.3 48.0 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 43.3 40.3 QF_ABV newUnsatCoresAssumps-safe/ ok 105 70 59 11 70 35 0 0 63 0 8195.5 19363.3 newUnsatCoresProofs ok 105 34 24 10 17 71 0 0 5 0 11099.5 35756.7 oldUnsatCores ok 105 37 23 14 18 69 0 0 1 0 11198.0 26878.1 QF_ANIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1631.8 newUnsatCoresProofs ok 4 4 3 1 2 0 0 0 0 0 175.1 1513.6 oldUnsatCores ok 4 4 3 1 3 0 0 0 0 0 173.8 1495.1 QF_AUFLIA newUnsatCoresAssumps-safe/ ok 35 6 1 5 6 29 0 0 3 0 3718.4 524.1 newUnsatCoresProofs ok 35 24 4 20 1 11 0 0 0 0 2357.2 36556.0 oldUnsatCores ok 35 32 5 27 29 3 0 0 5 0 1857.6 10067.7 QF_AUFNIA newUnsatCoresAssumps-safe/ ok 3 1 0 1 1 2 0 0 0 0 324.7 543.6 newUnsatCoresProofs ok 3 2 2 0 1 1 0 0 1 0 223.1 509.0 oldUnsatCores ok 3 2 1 1 1 1 0 0 0 0 268.5 484.3 QF_AX newUnsatCoresAssumps-safe/ ok 12 1 0 1 1 11 0 0 0 0 1379.2 391.3 newUnsatCoresProofs ok 12 10 0 10 0 2 0 0 0 0 528.7 7433.9 oldUnsatCores ok 12 12 0 12 11 0 0 0 1 0 343.0 2855.2 QF_BV newUnsatCoresAssumps-safe/ ok 96 56 30 26 49 39 2 0 35 0 9248.2 98058.7 newUnsatCoresProofs ok 96 37 26 11 23 52 7 0 7 0 9781.9 135924.7 oldUnsatCores ok 96 50 29 21 24 43 3 0 7 0 9155.6 107216.0 QF_IDL newUnsatCoresAssumps-safe/ ok 109 51 39 12 43 58 0 0 33 0 10427.2 50846.5 newUnsatCoresProofs ok 109 33 32 1 2 76 0 0 0 0 11692.8 108963.1 oldUnsatCores ok 109 75 55 20 64 34 0 0 26 0 10088.1 53105.6 QF_LIA newUnsatCoresAssumps-safe/ ok 306 155 111 44 138 151 0 0 119 0 25346.4 50556.0 newUnsatCoresProofs ok 306 117 95 22 49 189 0 0 0 0 27092.6 122894.9 oldUnsatCores ok 306 187 110 77 152 119 0 0 34 0 24521.0 61261.1 QF_LRA newUnsatCoresAssumps-safe/ ok 72 39 20 19 38 33 0 0 31 0 7475.3 16892.2 newUnsatCoresProofs ok 72 31 16 15 2 41 0 0 0 0 7569.3 35658.7 oldUnsatCores ok 72 41 18 23 32 31 0 0 2 0 7243.2 20593.9 QF_NIA newUnsatCoresAssumps-safe/ ok 4389 2009 1862 147 2002 903 0 0 1931 0 163975.7 280779.3 newUnsatCoresProofs ok 4389 2326 2156 170 752 792 0 0 37 0 151051.9 387779.8 oldUnsatCores ok 4389 2394 2199 195 2174 730 0 0 81 0 146419.3 259669.8 QF_NRA newUnsatCoresAssumps-safe/ ok 135 65 57 8 57 70 0 0 45 0 10195.7 24701.4 newUnsatCoresProofs ok 135 71 49 22 35 64 0 0 5 0 10825.3 32982.8 oldUnsatCores ok 135 75 54 21 51 61 0 0 9 0 10865.3 27260.9 QF_RDL newUnsatCoresAssumps-safe/ ok 7 5 1 4 5 2 0 0 1 0 564.7 958.4 newUnsatCoresProofs ok 7 1 1 0 0 6 0 0 0 0 842.0 11029.6 oldUnsatCores ok 7 6 1 5 2 1 0 0 1 0 665.8 1982.6 QF_S newUnsatCoresAssumps-safe/ ok 5 1 1 0 0 4 0 0 0 0 603.3 191.4 newUnsatCoresProofs ok 5 5 5 0 2 0 0 0 0 0 161.9 285.8 oldUnsatCores ok 5 4 4 0 3 1 0 0 0 0 225.9 219.3 QF_SLIA newUnsatCoresAssumps-safe/ ok 258 74 67 7 70 184 0 0 64 0 27245.9 20290.4 newUnsatCoresProofs ok 258 179 163 16 47 79 0 0 6 0 18996.0 33722.6 oldUnsatCores ok 258 184 162 22 149 74 0 0 9 0 18395.8 23004.3 QF_UF newUnsatCoresAssumps-safe/ ok 29 25 0 25 6 4 0 0 2 0 2362.4 7504.3 newUnsatCoresProofs ok 29 0 0 0 0 28 1 0 0 0 3508.0 124190.7 oldUnsatCores ok 29 27 0 27 23 2 0 0 4 0 1866.3 13635.1 QF_UFBV newUnsatCoresAssumps-safe/ ok 2 2 0 2 1 0 0 0 1 0 189.5 1599.3 newUnsatCoresProofs to 2 0 0 0 0 2 0 0 0 0 241.8 1818.8 oldUnsatCores ok 2 1 0 1 1 1 0 0 0 0 193.7 1500.9 QF_UFIDL newUnsatCoresAssumps-safe/ ok 9 9 0 9 7 0 0 0 4 0 697.0 1133.0 newUnsatCoresProofs to 9 0 0 0 0 9 0 0 0 0 1088.0 14652.6 oldUnsatCores ok 9 5 0 5 2 4 0 0 0 0 848.5 2079.6 QF_UFLIA newUnsatCoresAssumps-safe/ ok 1 1 0 1 0 0 0 0 0 0 117.1 76.4 newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.9 208.5 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 110.6 127.7 QF_UFLRA newUnsatCoresAssumps-safe/ ok 7 4 1 3 0 0 3 0 0 0 266.6 55098.3 newUnsatCoresProofs mo 7 0 0 0 0 0 7 0 0 0 261.7 56000.0 oldUnsatCores ok 7 7 4 3 7 0 0 0 3 0 408.4 20933.4 QF_UFNIA newUnsatCoresAssumps-safe/ ok 48 21 19 2 21 4 0 0 20 0 592.3 880.6 newUnsatCoresProofs ok 48 27 22 5 18 4 0 0 1 0 641.4 1548.8 oldUnsatCores ok 48 26 21 5 26 7 0 0 1 0 887.5 1044.6 QF_UFNRA newUnsatCoresAssumps-safe/ ok 1 1 1 0 1 0 0 0 1 0 108.3 17.9 newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.8 19.0 oldUnsatCores to 1 0 0 0 0 1 0 0 0 0 120.8 14.7 UF newUnsatCoresAssumps-safe/ ok 21 5 0 5 5 16 0 0 5 0 2123.8 3168.7 newUnsatCoresProofs ok 21 13 0 13 6 8 0 0 0 0 1496.3 6617.8 oldUnsatCores ok 21 16 0 16 11 5 0 0 3 0 1443.3 3919.2 UFDT newUnsatCoresAssumps-safe/ ok 35 6 0 6 6 29 0 0 5 0 3777.0 4485.5 newUnsatCoresProofs ok 35 28 0 28 15 7 0 0 0 0 1416.9 4293.6 oldUnsatCores ok 35 30 0 30 26 5 0 0 1 0 1406.9 3188.5 UFDTLIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1640.5 newUnsatCoresProofs ok 4 4 0 4 1 0 0 0 0 0 139.3 942.3 oldUnsatCores ok 4 4 0 4 3 0 0 0 0 0 156.4 851.8 UFDTLIRA newUnsatCoresAssumps-safe/ ok 1 1 0 1 1 0 0 0 1 0 0.0 3.1 newUnsatCoresProofs ok 1 0 0 0 0 0 0 0 0 0 0.0 3.2 oldUnsatCores ok 1 0 0 0 0 0 0 0 0 0 0.0 2.7 UFDTNIRA newUnsatCoresAssumps-safe/ ok 10 3 0 3 3 6 0 0 3 0 754.8 1386.9 newUnsatCoresProofs ok 10 7 0 7 5 3 0 0 0 0 377.0 848.8 oldUnsatCores ok 10 7 0 7 7 3 0 0 0 0 376.5 563.4 UFLIA newUnsatCoresAssumps-safe/ ok 24 8 0 8 8 16 0 0 8 0 2231.6 3179.2 newUnsatCoresProofs ok 24 14 0 14 3 10 0 0 1 0 1915.5 5131.1 oldUnsatCores ok 24 15 0 15 14 9 0 0 2 0 1857.5 3479.7 UFNIA newUnsatCoresAssumps-safe/ ok 354 183 28 155 116 133 0 0 113 0 25941.4 839089.7 newUnsatCoresProofs ok 354 107 17 90 28 107 92 0 2 0 23496.9 1020258.1 oldUnsatCores ok 354 237 19 218 233 72 0 0 66 0 19906.9 914273.0 ``` --- diff --git a/NEWS b/NEWS index 1aeac83da..26e0edbb6 100644 --- a/NEWS +++ b/NEWS @@ -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)