Print response to get-model using the API (#7084)

This changes our implementation of GetModelCommand so that we use the API to print the model.

It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.

It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.

This eliminates the last call to getSmtEngine() from the command layer.

2 files changed, 46 insertions, 10 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d03b8975e..d6c0a58ee 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7381,6 +7381,36 @@ bool Solver::isModelCoreSymbol(const Term& v) const
   CVC5_API_TRY_CATCH_END;
 }
 
+std::string Solver::getModel(const std::vector<Sort>& sorts,
+                             const std::vector<Term>& vars) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  NodeManagerScope scope(getNodeManager());
+  CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+      << "Cannot get model unless model generation is enabled "
+         "(try --produce-models)";
+  CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+      << "Cannot get model unless after a SAT or unknown response.";
+  CVC5_API_SOLVER_CHECK_SORTS(sorts);
+  for (const Sort& s : sorts)
+  {
+    CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort())
+        << "Expecting an uninterpreted sort as argument to "
+           "getModel.";
+  }
+  CVC5_API_SOLVER_CHECK_TERMS(vars);
+  for (const Term& v : vars)
+  {
+    CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT)
+        << "Expecting a free constant as argument to getModel.";
+  }
+  //////// all checks before this line
+  return d_smtEngine->getModel(Sort::sortVectorToTypeNodes(sorts),
+                               Term::termVectorToNodes(vars));
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Term Solver::getQuantifierElimination(const Term& q) const
 {
   NodeManagerScope scope(getNodeManager());
@@ -7900,12 +7930,6 @@ std::vector<Term> Solver::getSynthSolutions(
   CVC5_API_TRY_CATCH_END;
 }
 
-/*
- * !!! This is only temporarily available until the parser is fully migrated to
- * the new API. !!!
- */
-SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
-
 Statistics Solver::getStatistics() const
 {
   return Statistics(d_smtEngine->getStatisticsRegistry());
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 11b138a50..a221f3711 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3951,6 +3951,22 @@ class CVC5_EXPORT Solver
   bool isModelCoreSymbol(const Term& v) const;
 
   /**
+   * Get the model
+   * SMT-LIB:
+   * \verbatim
+   * ( get-model )
+   * \endverbatim
+   * Requires to enable option 'produce-models'.
+   * @param sorts The list of uninterpreted sorts that should be printed in the
+   * model.
+   * @param vars The list of free constants that should be printed in the
+   * model. A subset of these may be printed based on isModelCoreSymbol.
+   * @return a string representing the model.
+   */
+  std::string getModel(const std::vector<Sort>& sorts,
+                       const std::vector<Term>& vars) const;
+
+  /**
    * Do quantifier elimination.
    * SMT-LIB:
    * \verbatim
@@ -4329,10 +4345,6 @@ class CVC5_EXPORT Solver
    */
   std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const;
 
-  // !!! This is only temporarily available until the parser is fully migrated
-  // to the new API. !!!
-  SmtEngine* getSmtEngine(void) const;
-
   /**
    * Returns a snapshot of the current state of the statistic values of this
    * solver. The returned object is completely decoupled from the solver and