From 6beda739210b7bd13adbb7f62b0c4361156986ee Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 13 Nov 2019 00:03:35 -0600 Subject: [PATCH] Distinguish unknown status for model printing (#3454) --- src/printer/tptp/tptp_printer.cpp | 8 ++++++-- src/smt/model.cpp | 4 +--- src/smt/model.h | 19 ++++++++++++++++--- src/smt/smt_engine.cpp | 11 +++++++---- src/smt/smt_engine.h | 8 +++++--- 5 files changed, 35 insertions(+), 15 deletions(-) diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 72fdfe41d..d06b80e7b 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -55,11 +55,15 @@ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const void TptpPrinter::toStream(std::ostream& out, const Model& m) const { - out << "% SZS output start FiniteModel for " << m.getInputName() << endl; + std::string statusName(m.isKnownSat() ? "FiniteModel" + : "CandidateFiniteModel"); + out << "% SZS output start " << statusName << " for " << m.getInputName() + << endl; for(size_t i = 0; i < m.getNumCommands(); ++i) { this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m, m.getCommand(i)); } - out << "% SZS output end FiniteModel for " << m.getInputName() << endl; + out << "% SZS output end " << statusName << " for " << m.getInputName() + << endl; } void TptpPrinter::toStream(std::ostream& out, diff --git a/src/smt/model.cpp b/src/smt/model.cpp index e452905e1..c6048da15 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -35,9 +35,7 @@ std::ostream& operator<<(std::ostream& out, const Model& m) { return out; } -Model::Model() : - d_smt(*smt::currentSmtEngine()) { -} +Model::Model() : d_smt(*smt::currentSmtEngine()), d_isKnownSat(false) {} size_t Model::getNumCommands() const { return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); diff --git a/src/smt/model.h b/src/smt/model.h index 06b616f9b..3ff63e915 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -35,9 +35,6 @@ class Model { friend std::ostream& operator<<(std::ostream&, const Model&); friend class SmtEngine; - /** the input name (file name, etc.) this model is associated to */ - std::string d_inputName; - protected: /** The SmtEngine we're associated with */ SmtEngine& d_smt; @@ -58,6 +55,13 @@ class Model { const SmtEngine* getSmtEngine() const { return &d_smt; } /** get the input name (file name, etc.) this model is associated to */ std::string getInputName() const { return d_inputName; } + /** + * Returns true if this model is guaranteed to be a model of the input + * formula. Notice that when CVC4 answers "unknown", it may have a model + * available for which this method returns false. In this case, this model is + * only a candidate solution. + */ + bool isKnownSat() const { return d_isKnownSat; } //--------------------------- model cores /** set using model core * @@ -104,6 +108,15 @@ class Model { * this model. */ virtual std::vector getDomainElements(Type t) const = 0; + + protected: + /** the input name (file name, etc.) this model is associated to */ + std::string d_inputName; + /** + * Flag set to false if the model is associated with an "unknown" response + * from the solver. + */ + bool d_isKnownSat; };/* class Model */ class ModelBuilder { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7d28d8b85..073c2ebc5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3094,7 +3094,7 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const throw RecoverableModalException(ss.str().c_str()); } - if (d_smtMode != SMT_MODE_SAT) + if (d_smtMode != SMT_MODE_SAT && d_smtMode != SMT_MODE_SAT_UNKNOWN) { std::stringstream ss; ss << "Cannot " << c @@ -3809,12 +3809,14 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, { d_smtMode = SMT_MODE_UNSAT; } - else + else if (d_status.asSatisfiabilityResult().isSat() == Result::SAT) { - // Notice that unknown response moves to sat mode, since the same set - // of commands (get-model, get-value) are applicable to this case. d_smtMode = SMT_MODE_SAT; } + else + { + d_smtMode = SMT_MODE_SAT_UNKNOWN; + } Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << assumptions << ") => " << r << endl; @@ -4410,6 +4412,7 @@ Model* SmtEngine::getModel() { ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode()); } m->d_inputName = d_filename; + m->d_isKnownSat = (d_smtMode == SMT_MODE_SAT); return m; } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index d99606126..a91a3a201 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -838,8 +838,8 @@ class CVC4_PUBLIC SmtEngine typedef context::CDList NodeList; /** - * The current mode of the solver, see Figure 4.1 on page 52 of the - * SMT-LIB version 2.6 standard + * The current mode of the solver, which is an extension of Figure 4.1 on + * page 52 of the SMT-LIB version 2.6 standard * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf */ enum SmtMode @@ -848,8 +848,10 @@ class CVC4_PUBLIC SmtEngine SMT_MODE_START, // normal state of the solver, after assert/push/pop/declare/define SMT_MODE_ASSERT, - // immediately after a check-sat returning "sat" or "unknown" + // immediately after a check-sat returning "sat" SMT_MODE_SAT, + // immediately after a check-sat returning "unknown" + SMT_MODE_SAT_UNKNOWN, // immediately after a check-sat returning "unsat" SMT_MODE_UNSAT, // immediately after a successful call to get-abduct -- 2.30.2