Distinguish unknown status for model printing (#3454)

diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 72fdfe41dc0b2989c65333c0a5d943af20fbc5a5..d06b80e7b8ad78a68446c5c3085a44c08becce62 100644 (file)
--- 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 e452905e13fddb17b513efe85722020328403fa5..c6048da15d5e2dd5fb94268c550ab7fcd712fc72 100644 (file)
--- 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 06b616f9b66419215f63ba0fff8d9ed63cd9d9bb..3ff63e915695d39d684dffd5a5a5f81ea0565b95 100644 (file)
--- 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<Expr> 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 7d28d8b85016cf0d8bcdfd3e8a23ad746a39bafc..073c2ebc51586e8951e273f53d610ca4bf2ebfcd 100644 (file)
--- 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<Expr>& 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 d99606126079230d64d9924145b35d2c042e2323..a91a3a2011653fabc49f5412afa645ebf28ce89b 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -838,8 +838,8 @@ class CVC4_PUBLIC SmtEngine
   typedef context::CDList<Node> 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