Dumping unsat cores after check-sat-assuming/QUERY (#5724)

Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.

It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index fe4af6361c45b6aa7adacc4e54e433f290f66e8b..04ed5147aa8ac2e238b57369b656ad6e9aa2bb9e 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -136,14 +136,16 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   if(cs != nullptr) {
     d_result = res = cs->getResult();
   }
+  const CheckSatAssumingCommand* csa =
+      dynamic_cast<const CheckSatAssumingCommand*>(cmd);
+  if (csa != nullptr)
+  {
+    d_result = res = csa->getResult();
+  }
   const QueryCommand* q = dynamic_cast<const QueryCommand*>(cmd);
   if(q != nullptr) {
     d_result = res = q->getResult();
   }
- const  CheckSynthCommand* csy = dynamic_cast<const CheckSynthCommand*>(cmd);
-  if(csy != nullptr) {
-    d_result = res = csy->getResult();
-  }
 
   if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
     std::ostringstream ossCurStats;
@@ -153,6 +155,8 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_lastStatistics = ossCurStats.str();
   }
 
+  bool isResultUnsat = res.isUnsat() || res.isEntailed();
+
   // dump the model/proof/unsat core if option is set
   if (status) {
     std::vector<std::unique_ptr<Command> > getterCommands;
@@ -163,7 +167,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     {
       getterCommands.emplace_back(new GetModelCommand());
     }
-    if (d_options.getDumpProofs() && res.isUnsat())
+    if (d_options.getDumpProofs() && isResultUnsat)
     {
       getterCommands.emplace_back(new GetProofCommand());
     }
@@ -173,17 +177,12 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
              && (res.isSat()
                  || (res.isSatUnknown()
                      && res.getResult().whyUnknown() == Result::INCOMPLETE)))
-            || res.isUnsat()))
+            || isResultUnsat))
     {
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
-    if (d_options.getDumpSynth() && res.isUnsat())
-    {
-      getterCommands.emplace_back(new GetSynthSolutionCommand());
-    }
-
-    if (d_options.getDumpUnsatCores() && res.isUnsat())
+    if (d_options.getDumpUnsatCores() && isResultUnsat)
     {
       getterCommands.emplace_back(new GetUnsatCoreCommand());
     }

diff --git a/src/options/options.h b/src/options/options.h
index b0dca574879d94c0f8b8e2a97e806520d7d559e0..ef5bea2e3809195cba9c12b006c4f6079c254bcc 100644 (file)
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -153,7 +153,6 @@ public:
   bool getDumpInstantiations() const;
   bool getDumpModels() const;
   bool getDumpProofs() const;
-  bool getDumpSynth() const;
   bool getDumpUnsatCores() const;
   bool getEarlyExit() const;
   bool getFilesystemAccess() const;
@@ -190,7 +189,6 @@ public:
   void setOut(std::ostream*);
   void setOutputLanguage(OutputLanguage);
 
-  bool wasSetByUserDumpSynth() const;
   bool wasSetByUserEarlyExit() const;
   bool wasSetByUserForceLogicString() const;
   bool wasSetByUserIncrementalSolving() const;

diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 4043365b9be258525fe18620cb70954d4fbb74d4..61bb36e44350d61c8e87f2a4bc396fa36271acc1 100644 (file)
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -66,10 +66,6 @@ bool Options::getDumpProofs() const{
   return (*this)[options::dumpProofs];
 }
 
-bool Options::getDumpSynth() const{
-  return (*this)[options::dumpSynth];
-}
-
 bool Options::getDumpUnsatCores() const{
   // dump unsat cores full enables dumpUnsatCores
   return (*this)[options::dumpUnsatCores]
@@ -213,10 +209,6 @@ void Options::setOutputLanguage(OutputLanguage value) {
   set(options::outputLanguage, value);
 }
 
-bool Options::wasSetByUserDumpSynth() const {
-  return wasSetByUser(options::dumpSynth);
-}
-
 bool Options::wasSetByUserEarlyExit() const {
   return wasSetByUser(options::earlyExit);
 }

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index b01b7780fff2171408d674190ad94e0e53ec1963..247559c9199233fd1d01ceac3d2ca16f54fe2cd1 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -232,14 +232,6 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)"
 
-[[option]]
-  name       = "dumpSynth"
-  category   = "regular"
-  long       = "dump-synth"
-  type       = "bool"
-  default    = "false"
-  help       = "output solution for synthesis conjectures after every UNSAT/VALID response"
-
 [[option]]
   name       = "unsatCores"
   category   = "regular"

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index b8700f7f6d097fbcd4e4e597951efccbec15360e..ad125a70f7ee45b587cadb521b118b6ef925e3a0 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -977,7 +977,6 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
   Assert(d_master != nullptr);
   // we have generated a solution, print it
   // get the current output stream
-  // this output stream should coincide with wherever --dump-synth is output on
   Options& sopts = smt::currentSmtEngine()->getOptions();
   printSynthSolution(*sopts.getOut());
   excludeCurrentSolution(enums, values);