Change semantics of dumpUnsatCoresFull (#7314)

This PR changes --dump-unsat-cores-full to --print-unsat-cores-full.
It also makes it so that solely having --dump-unsat-cores-full no longer automatically prints unsat cores.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 4f5fd5c244485a8ad87c65ab4939fb6156f67c26..8188f247fb8b1748cea4190d47b4cc87176f9a82 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -162,8 +162,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
-    if ((d_solver->getOptionInfo("dump-unsat-cores").boolValue()
-         || d_solver->getOptionInfo("dump-unsat-cores-full").boolValue())
+    if (d_solver->getOptionInfo("dump-unsat-cores").boolValue()
         && isResultUnsat)
     {
       getterCommands.emplace_back(new GetUnsatCoreCommand());

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 3d78a6ebbbc2883e27bebb47d824d10af7984602..974bdd155c407a2758783bb2152b31f85a9fc735 100644 (file)
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -125,9 +125,9 @@ name   = "Driver"
   help       = "output unsat cores after every UNSAT/VALID response"
 
 [[option]]
-  name       = "dumpUnsatCoresFull"
+  name       = "printUnsatCoresFull"
   category   = "regular"
-  long       = "dump-unsat-cores-full"
+  long       = "print-unsat-cores-full"
   type       = "bool"
   default    = "false"
   help       = "dump the full unsat core, including unlabeled assertions"

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 427b79c67d6ff60c7507657786a61c4978663f7d..311d6713aadd59574fa02f83d594d130f636fcbe 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2339,7 +2339,7 @@ void GetUnsatCoreCommand::printResult(std::ostream& out,
   }
   else
   {
-    if (options::dumpUnsatCoresFull())
+    if (options::printUnsatCoresFull())
     {
       // use the assertions
       UnsatCore ucr(termVectorToNodes(d_result));

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index e174570fbb41acd08a0d2009017d6ee0c7ba8e67..40c940b5af64b20674a0090a30b9d464352e3446 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -77,10 +77,6 @@ void SetDefaults::setDefaultsPre(Options& opts)
     opts.smt.produceAssignments = true;
   }
   // unsat cores and proofs shenanigans
-  if (opts.driver.dumpUnsatCoresFull)
-  {
-    opts.driver.dumpUnsatCores = true;
-  }
   if (opts.driver.dumpDifficulty)
   {
     opts.smt.produceDifficulty = true;

diff --git a/test/regress/regress0/dump-unsat-core-full.smt2 b/test/regress/regress0/dump-unsat-core-full.smt2
index a21508efb6cb88bd5b92677cb034221c556c65df..3ed2f534cd0c70bb71ac72c68e6ca60c5965dc09 100644 (file)
--- a/test/regress/regress0/dump-unsat-core-full.smt2
+++ b/test/regress/regress0/dump-unsat-core-full.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --dump-unsat-cores-full
+; COMMAND-LINE: --print-unsat-cores-full --dump-unsat-cores
 ; EXPECT: unsat
 ; EXPECT: (
 ; EXPECT: (and (= x y) (< x y))