From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 6 Oct 2021 23:12:46 +0000 (-0700)
Subject: Change semantics of dumpUnsatCoresFull (#7314)
X-Git-Tag: cvc5-1.0.0~1116
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fb45de5d7385a1ba9e40237a745720f54d67db92;p=cvc5.git

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 4f5fd5c24..8188f247f 100644
--- 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 3d78a6ebb..974bdd155 100644
--- 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 427b79c67..311d6713a 100644
--- 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 e174570fb..40c940b5a 100644
--- 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 a21508efb..3ed2f534c 100644
--- 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))