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 1aeac83dab36c86db912260bf245314f14c6e0e2..26e0edbb6f4b9d309a3a508e14a422268fc85619 100644 (file)
--- 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 733c2239cea90d382d75d58904bdf16aa9e2d576..ddffe8c12f086aff390d080483af0f44f3cde3bd 100644 (file)
--- 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 7c5d775ed3aa444978df232d4a62a58d3d01b30a..be19923afc205b24aa8745c94873d12c6c64990d 100644 (file)
--- 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 67273f8549275c78ce513416d1e8a1d74f4c1504..0e1ff8878c10d52ad674c62270040bbac97bfbd4 100644 (file)
--- 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 de3946ef0d8ca9df5819d8052c74914bcf253cc9..a97863d7db180010f4dbb5c88c1872607cb40f19 100644 (file)
--- 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 bcb077f4f4ebe1443a31d2b216c703c18a62fd4e..6d910b4646f83d9ae86b65cac351fb52e22c6a1c 100644 (file)
--- 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)