From a539b63c369544ed08a1fa7fa4c8e3d437be3766 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 23 Dec 2020 20:10:34 -0300 Subject: [PATCH] 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. --- src/main/command_executor.cpp | 23 +++++++++---------- src/options/options.h | 2 -- src/options/options_public_functions.cpp | 8 ------- src/options/smt_options.toml | 8 ------- .../quantifiers/sygus/synth_conjecture.cpp | 1 - 5 files changed, 11 insertions(+), 31 deletions(-) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index fe4af6361..04ed5147a 100644 --- 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(cmd); + if (csa != nullptr) + { + d_result = res = csa->getResult(); + } const QueryCommand* q = dynamic_cast(cmd); if(q != nullptr) { d_result = res = q->getResult(); } - const CheckSynthCommand* csy = dynamic_cast(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 > 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 b0dca5748..ef5bea2e3 100644 --- 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 4043365b9..61bb36e44 100644 --- 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 b01b7780f..247559c91 100644 --- 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 b8700f7f6..ad125a70f 100644 --- 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& 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); -- 2.30.2