add option to get unsat cores lemmas via the previously added command

HanielB · Jan 23, 2024 · 35060fd · 35060fd
1 parent 8bfc06a
commit 35060fd
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 1 deletion.
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
@@ -173,6 +173,12 @@ bool CommandExecutor::doCommandSingleton(Cmd* cmd)
       getterCommands.emplace_back(new GetUnsatCoreCommand());
     }
 
+    if (d_solver->getOptionInfo("dump-unsat-cores-lemmas").boolValue()
+        && isResultUnsat)
+    {
+      getterCommands.emplace_back(new GetUnsatCoreLemmasCommand());
+    }
+
     if (d_solver->getOptionInfo("dump-difficulty").boolValue()
         && (isResultUnsat || isResultSat || res.isUnknown()))
     {

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
@@ -143,6 +143,14 @@ name   = "Driver"
   default    = "false"
   help       = "output unsat cores after every UNSAT/VALID response"
 
+[[option]]
+  name       = "dumpUnsatCoresLemmas"
+  category   = "regular"
+  long       = "dump-unsat-cores-lemmas"
+  type       = "bool"
+  default    = "false"
+  help       = "output lemmas in unsat cores after every UNSAT/VALID response"
+
 [[option]]
   name       = "dumpDifficulty"
   category   = "regular"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
@@ -132,7 +132,8 @@ void SetDefaults::setDefaultsPre(Options& opts)
     SET_AND_NOTIFY(Smt, produceDifficulty, true, "dumpDifficulty");
   }
   if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores
-      || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores
+      || opts.driver.dumpUnsatCoresLemmas || opts.smt.unsatAssumptions
+      || opts.smt.minimalUnsatCores
       || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)
   {
     SET_AND_NOTIFY(