Add missing methods to Solver API for models (#7052)

This adds the last two remaining API methods required for implementing the text output of get-model on the API side.

A followup PR will implement GetModelCommand on the API side and eliminate the (last remaining) call to getSmtEngine() from the command layer.

This PR does some minor reorganization of the model cores code to account for the new interface. It also removes a deprecated interface from TheoryModel.

14 files changed, 174 insertions, 54 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index f85286acb..1eaae8761 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7131,6 +7131,51 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
   CVC5_API_TRY_CATCH_END;
 }
 
+std::vector<Term> Solver::getModelDomainElements(const Sort& s) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  NodeManagerScope scope(getNodeManager());
+  CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+      << "Cannot get domain elements unless model generation is enabled "
+         "(try --produce-models)";
+  CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+      << "Cannot get domain elements unless after a SAT or unknown response.";
+  CVC5_API_SOLVER_CHECK_SORT(s);
+  CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort())
+      << "Expecting an uninterpreted sort as argument to "
+         "getModelDomainElements.";
+  //////// all checks before this line
+  std::vector<Term> res;
+  std::vector<Node> elements =
+      d_smtEngine->getModelDomainElements(s.getTypeNode());
+  for (const Node& n : elements)
+  {
+    res.push_back(Term(this, n));
+  }
+  return res;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Solver::isModelCoreSymbol(const Term& v) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  NodeManagerScope scope(getNodeManager());
+  CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+      << "Cannot check if model core symbol unless model generation is enabled "
+         "(try --produce-models)";
+  CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+      << "Cannot check if model core symbol unless after a SAT or unknown "
+         "response.";
+  CVC5_API_SOLVER_CHECK_TERM(v);
+  CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT)
+      << "Expecting a free constant as argument to isModelCoreSymbol.";
+  //////// all checks before this line
+  return d_smtEngine->isModelCoreSymbol(v.getNode());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Term Solver::getQuantifierElimination(const Term& q) const
 {
   NodeManagerScope scope(getNodeManager());
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 3c0241311..9f805fa65 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3782,7 +3782,7 @@ class CVC5_EXPORT Solver
   std::string getProof() const;
 
   /**
-   * Get the value of the given term.
+   * Get the value of the given term in the current model.
    * SMT-LIB:
    * \verbatim
    * ( get-value ( <term> ) )
@@ -3791,8 +3791,9 @@ class CVC5_EXPORT Solver
    * @return the value of the given term
    */
   Term getValue(const Term& term) const;
+
   /**
-   * Get the values of the given terms.
+   * Get the values of the given terms in the current model.
    * SMT-LIB:
    * \verbatim
    * ( get-value ( <term>+ ) )
@@ -3803,6 +3804,27 @@ class CVC5_EXPORT Solver
   std::vector<Term> getValue(const std::vector<Term>& terms) const;
 
   /**
+   * Get the domain elements of uninterpreted sort s in the current model. The
+   * current model interprets s as the finite sort whose domain elements are
+   * given in the return value of this method.
+   *
+   * @param s The uninterpreted sort in question
+   * @return the domain elements of s in the current model
+   */
+  std::vector<Term> getModelDomainElements(const Sort& s) const;
+
+  /**
+   * This returns false if the model value of free constant v was not essential
+   * for showing the satisfiability of the last call to checkSat using the
+   * current model. This method will only return false (for any v) if
+   * the model-cores option has been set.
+   *
+   * @param v The term in question
+   * @return true if v is a model core symbol
+   */
+  bool isModelCoreSymbol(const Term& v) const;
+
+  /**
    * Do quantifier elimination.
    * SMT-LIB:
    * \verbatim
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 2665706c0..ef9971c20 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -278,6 +278,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         vector[Term] getUnsatCore() except +
         Term getValue(Term term) except +
         vector[Term] getValue(const vector[Term]& terms) except +
+        vector[Term] getModelDomainElements(Sort sort) except +
+        bint isModelCoreSymbol(Term v) except +
         void declareSeparationHeap(Sort locSort, Sort dataSort) except +
         Term getSeparationHeap() except +
         Term getSeparationNilTerm() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 36dcc066e..68998d521 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1296,6 +1296,18 @@ cdef class Solver:
         term.cterm = self.csolver.getValue(t.cterm)
         return term
 
+    def getModelDomainElements(self, Sort s):
+        result = []
+        cresult = self.csolver.getModelDomainElements(s.csort)
+        for e in cresult:
+            term = Term(self)
+            term.cterm = e
+            result.append(term)
+        return result
+
+    def isModelCoreSymbol(self, Term v):
+        return self.csolver.isModelCoreSymbol(v.cterm)
+
     def getSeparationHeap(self):
         cdef Term term = Term(self)
         term.cterm = self.csolver.getSeparationHeap()
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index b42304ecc..1f1296b7f 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1095,16 +1095,6 @@ void CvcPrinter::toStreamModelTerm(std::ostream& out,
 
 void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const
 {
-  const theory::TheoryModel* tm = m.getTheoryModel();
-  // print the model comments
-  std::stringstream c;
-  tm->getComments(c);
-  std::string ln;
-  while (std::getline(c, ln))
-  {
-    out << "; " << ln << std::endl;
-  }
-
   // print the model
   out << "MODEL BEGIN" << std::endl;
   this->Printer::toStream(out, m);
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b7f32123d..523b3efa9 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1262,13 +1262,6 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
 void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const
 {
   const theory::TheoryModel* tm = m.getTheoryModel();
-  //print the model comments
-  std::stringstream c;
-  tm->getComments(c);
-  std::string ln;
-  while( std::getline( c, ln ) ){
-    out << "; " << ln << std::endl;
-  }
   //print the model
   out << "(" << endl;
   // don't need to print approximations since they are built into choice
diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index 0395a32fd..9e9eb5f23 100644
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -25,6 +25,11 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions,
                                     theory::TheoryModel* m,
                                     options::ModelCoresMode mode)
 {
+  if (m->isUsingModelCore())
+  {
+    // already computed
+    return true;
+  }
   if (Trace.isOn("model-core"))
   {
     Trace("model-core") << "Compute model core, assertions:" << std::endl;
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 3c0a4ac5b..c36ff1bce 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -135,6 +135,15 @@ Node Preprocessor::expandDefinitions(const Node& node,
   return n;
 }
 
+void Preprocessor::expandDefinitions(std::vector<Node>& ns)
+{
+  std::unordered_map<Node, Node> cache;
+  for (size_t i = 0, nasserts = ns.size(); i < nasserts; i++)
+  {
+    ns[i] = expandDefinitions(ns[i], cache);
+  }
+}
+
 Node Preprocessor::simplify(const Node& node)
 {
   Trace("smt") << "SMT simplify(" << node << ")" << endl;
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 3a1f9f080..03246ed67 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -90,6 +90,8 @@ class Preprocessor
   Node expandDefinitions(const Node& n);
   /** Same as above, with a cache of previous results. */
   Node expandDefinitions(const Node& n, std::unordered_map<Node, Node>& cache);
+  /** Same as above, for a list of assertions, updating in place */
+  void expandDefinitions(std::vector<Node>& ns);
   /**
    * Set proof node manager. Enables proofs in this preprocessor.
    */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ea253e4ef..be5c75af0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1166,7 +1166,7 @@ Node SmtEngine::getValue(const Node& ex) const
   return resultNode;
 }
 
-std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs)
+std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs) const
 {
   std::vector<Node> result;
   for (const Node& e : exprs)
@@ -1176,6 +1176,39 @@ std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs)
   return result;
 }
 
+std::vector<Node> SmtEngine::getModelDomainElements(TypeNode tn) const
+{
+  Assert(tn.isSort());
+  Model* m = getAvailableModel("getModelDomainElements");
+  return m->getTheoryModel()->getDomainElements(tn);
+}
+
+bool SmtEngine::isModelCoreSymbol(Node n)
+{
+  SmtScope smts(this);
+  Assert(n.isVar());
+  const Options& opts = d_env->getOptions();
+  if (opts.smt.modelCoresMode == options::ModelCoresMode::NONE)
+  {
+    // if the model core mode is none, we are always a model core symbol
+    return true;
+  }
+  Model* m = getAvailableModel("isModelCoreSymbol");
+  TheoryModel* tm = m->getTheoryModel();
+  // compute the model core if not done so already
+  if (!tm->isUsingModelCore())
+  {
+    // If we enabled model cores, we compute a model core for m based on our
+    // (expanded) assertions using the model core builder utility. Notice that
+    // we get the assertions using the getAssertionsInternal, which does not
+    // impact whether we are in "sat" mode
+    std::vector<Node> asserts = getAssertionsInternal();
+    d_pp->expandDefinitions(asserts);
+    ModelCoreBuilder::setModelCore(asserts, tm, opts.smt.modelCoresMode);
+  }
+  return tm->isModelCoreSymbol(n);
+}
+
 // TODO(#1108): Simplify the error reporting of this method.
 Model* SmtEngine::getModel() {
   Trace("smt") << "SMT getModel()" << endl;
@@ -1201,10 +1234,10 @@ Model* SmtEngine::getModel() {
   {
     // If we enabled model cores, we compute a model core for m based on our
     // (expanded) assertions using the model core builder utility
-    std::vector<Node> eassertsProc = getExpandedAssertions();
-    ModelCoreBuilder::setModelCore(eassertsProc,
-                                   m->getTheoryModel(),
-                                   d_env->getOptions().smt.modelCoresMode);
+    std::vector<Node> asserts = getAssertionsInternal();
+    d_pp->expandDefinitions(asserts);
+    ModelCoreBuilder::setModelCore(
+        asserts, m->getTheoryModel(), d_env->getOptions().smt.modelCoresMode);
   }
   // set the information on the SMT-level model
   Assert(m != nullptr);
@@ -1294,18 +1327,25 @@ std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void)
   return std::make_pair(heap, nil);
 }
 
+std::vector<Node> SmtEngine::getAssertionsInternal()
+{
+  Assert(d_state->isFullyInited());
+  context::CDList<Node>* al = d_asserts->getAssertionList();
+  Assert(al != nullptr);
+  std::vector<Node> res;
+  for (const Node& n : *al)
+  {
+    res.emplace_back(n);
+  }
+  return res;
+}
+
 std::vector<Node> SmtEngine::getExpandedAssertions()
 {
   std::vector<Node> easserts = getAssertions();
   // must expand definitions
-  std::vector<Node> eassertsProc;
-  std::unordered_map<Node, Node> cache;
-  for (const Node& e : easserts)
-  {
-    Node eae = d_pp->expandDefinitions(e, cache);
-    eassertsProc.push_back(eae);
-  }
-  return eassertsProc;
+  d_pp->expandDefinitions(easserts);
+  return easserts;
 }
 Env& SmtEngine::getEnv() { return *d_env.get(); }
 
@@ -1787,15 +1827,7 @@ std::vector<Node> SmtEngine::getAssertions()
       "Cannot query the current assertion list when not in produce-assertions mode.";
     throw ModalException(msg);
   }
-  context::CDList<Node>* al = d_asserts->getAssertionList();
-  Assert(al != nullptr);
-  std::vector<Node> res;
-  for (const Node& n : *al)
-  {
-    res.emplace_back(n);
-  }
-  // copy the result out
-  return res;
+  return getAssertionsInternal();
 }
 
 void SmtEngine::push()
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index d9786f6a1..a250e2a7f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -532,7 +532,17 @@ class CVC5_EXPORT SmtEngine
   /**
    * Same as getValue but for a vector of expressions
    */
-  std::vector<Node> getValues(const std::vector<Node>& exprs);
+  std::vector<Node> getValues(const std::vector<Node>& exprs) const;
+
+  /**
+   * @return the domain elements for uninterpreted sort tn.
+   */
+  std::vector<Node> getModelDomainElements(TypeNode tn) const;
+
+  /**
+   * @return true if v is a model core symbol
+   */
+  bool isModelCoreSymbol(Node v);
 
   /** print instantiations
    *
@@ -1022,7 +1032,13 @@ class CVC5_EXPORT SmtEngine
    * element is the nil expression.
    */
   std::pair<Node, Node> getSepHeapAndNilExpr();
-
+  /**
+   * Get assertions internal, which is only called after initialization. This
+   * should be used internally to get the assertions instead of getAssertions
+   * or getExpandedAssertions, which may trigger initialization and SMT state
+   * changes.
+   */
+  std::vector<Node> getAssertionsInternal();
   /* Members -------------------------------------------------------------- */
 
   /** Solver instance that owns this SmtEngine instance. */
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 92d15653e..ba1680c6b 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -198,7 +198,6 @@ void TheorySep::postProcessModel( TheoryModel* m ){
         Trace("sep-model") << " " << l << " -> ";
         if( d_pto_model[l].isNull() ){
           Trace("sep-model") << "_";
-          //m->d_comment_str << "_";
           TypeEnumerator te_range( data_type );
           if (d_state.isFiniteType(data_type))
           {
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 3e902463c..02a837899 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -74,7 +74,6 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee)
 
 void TheoryModel::reset(){
   d_modelCache.clear();
-  d_comment_str.clear();
   d_sep_heap = Node::null();
   d_sep_nil_eq = Node::null();
   d_approximations.clear();
@@ -91,11 +90,6 @@ void TheoryModel::reset(){
   d_model_core.clear();
 }
 
-void TheoryModel::getComments(std::ostream& out) const {
-  Trace("model-builder") << "get comments..." << std::endl;
-  out << d_comment_str.str();
-}
-
 void TheoryModel::setHeapModel( Node h, Node neq ) { 
   d_sep_heap = h;
   d_sep_nil_eq = neq;
@@ -610,6 +604,7 @@ void TheoryModel::recordApproximation(TNode n, TNode pred, Node witness)
   Node predDisj = NodeManager::currentNM()->mkNode(OR, n.eqNode(witness), pred);
   recordApproximation(n, predDisj);
 }
+bool TheoryModel::isUsingModelCore() const { return d_using_model_core; }
 void TheoryModel::setUsingModelCore()
 {
   d_using_model_core = true;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 4034e43bd..6841a11d8 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -296,8 +296,6 @@ class TheoryModel
    * has called buildModel(...) on this model.
    */
   Node getValue(TNode n) const;
-  /** get comments */
-  void getComments(std::ostream& out) const;
 
   //---------------------------- separation logic
   /** set the heap and value sep.nil is equal to */
@@ -318,6 +316,8 @@ class TheoryModel
   RepSet* getRepSetPtr() { return &d_rep_set; }
 
   //---------------------------- model cores
+  /** True if a model core has been computed for this model. */
+  bool isUsingModelCore() const;
   /** set using model core */
   void setUsingModelCore();
   /** record model core symbol */
@@ -394,8 +394,6 @@ class TheoryModel
   /** true/false nodes */
   Node d_true;
   Node d_false;
-  /** comment stream to include in printing */
-  std::stringstream d_comment_str;
   /** are we using model cores? */
   bool d_using_model_core;
   /** symbols that are in the model core */