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.

1 files changed, 36 insertions, 42 deletions

diff --git a/src/smt/model.h b/src/smt/model.h
index 342a9f3b0..5275ea680 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -15,8 +15,8 @@
 
 #include "cvc5_private.h"
 
-#ifndef CVC5__MODEL_H
-#define CVC5__MODEL_H
+#ifndef CVC5__SMT__MODEL_H
+#define CVC5__SMT__MODEL_H
 
 #include <iosfwd>
 #include <vector>
@@ -24,13 +24,6 @@
 #include "expr/node.h"
 
 namespace cvc5 {
-
-class SmtEngine;
-
-namespace theory {
-class TheoryModel;
-}
-
 namespace smt {
 
 class Model;
@@ -38,22 +31,15 @@ class Model;
 std::ostream& operator<<(std::ostream&, const Model&);
 
 /**
- * This is the SMT-level model object, that is responsible for maintaining
- * the necessary information for how to print the model, as well as
- * holding a pointer to the underlying implementation of the theory model.
- *
- * The model declarations maintained by this class are context-independent
- * and should be updated when this model is printed.
+ * A utility for representing a model for pretty printing.
  */
 class Model {
-  friend std::ostream& operator<<(std::ostream&, const Model&);
-  friend class ::cvc5::SmtEngine;
-
  public:
-  /** construct */
-  Model(theory::TheoryModel* tm);
-  /** virtual destructor */
-  ~Model() {}
+  /** Constructor
+   * @param isKnownSat True if this model is associated with a "sat" response,
+   * or false if it is associated with an "unknown" response.
+   */
+  Model(bool isKnownSat, const std::string& inputName);
   /** get the input name (file name, etc.) this model is associated to */
   std::string getInputName() const { return d_inputName; }
   /**
@@ -63,31 +49,37 @@ class Model {
    * only a candidate solution.
    */
   bool isKnownSat() const { return d_isKnownSat; }
-  /** Get the underlying theory model */
-  theory::TheoryModel* getTheoryModel();
-  /** Get the underlying theory model (const version) */
-  const theory::TheoryModel* getTheoryModel() const;
-  //----------------------- helper methods in the underlying theory model
-  /** Is the node n a model core symbol? */
-  bool isModelCoreSymbol(TNode sym) const;
+  /** Get domain elements */
+  const std::vector<Node>& getDomainElements(TypeNode tn) const;
   /** Get value */
   Node getValue(TNode n) const;
-  /** Does this model have approximations? */
-  bool hasApproximations() const;
-  //----------------------- end helper methods
+  /** Get separation logic heap and nil, return true if they have been set */
+  bool getHeapModel(Node& h, Node& nilEq) const;
   //----------------------- model declarations
-  /** Clear the current model declarations. */
-  void clearModelDeclarations();
   /**
    * Set that tn is a sort that should be printed in the model, when applicable,
    * based on the output language.
+   *
+   * @param tn The uninterpreted sort
+   * @param elements The domain elements of tn in the model
    */
-  void addDeclarationSort(TypeNode tn);
+  void addDeclarationSort(TypeNode tn, const std::vector<Node>& elements);
   /**
    * Set that n is a variable that should be printed in the model, when
    * applicable, based on the output language.
+   *
+   * @param n The variable
+   * @param value The value of the variable in the model
+   */
+  void addDeclarationTerm(Node n, Node value);
+  /**
+   * Set the separation logic model information where h is the heap and nilEq
+   * is the value of sep.nil.
+   *
+   * @param h The value of heap in the heap model
+   * @param nilEq The value of sep.nil in the heap model
    */
-  void addDeclarationTerm(Node n);
+  void setHeapModel(Node h, Node nilEq);
   /** get declared sorts */
   const std::vector<TypeNode>& getDeclaredSorts() const;
   /** get declared terms */
@@ -102,23 +94,25 @@ class Model {
    */
   bool d_isKnownSat;
   /**
-   * Pointer to the underlying theory model, which maintains all data regarding
-   * the values of sorts and terms.
-   */
-  theory::TheoryModel* d_tmodel;
-  /**
    * The list of types to print, generally corresponding to declare-sort
    * commands.
    */
   std::vector<TypeNode> d_declareSorts;
+  /** The interpretation of the above sorts, as a list of domain elements. */
+  std::map<TypeNode, std::vector<Node>> d_domainElements;
   /**
    * The list of terms to print, is typically one-to-one with declare-fun
    * commands.
    */
   std::vector<Node> d_declareTerms;
+  /** Mapping terms to values */
+  std::map<Node, Node> d_declareTermValues;
+  /** Separation logic heap and nil */
+  Node d_sepHeap;
+  Node d_sepNilEq;
 };
 
 }  // namespace smt
 }  // namespace cvc5
 
-#endif /* CVC5__MODEL_H */
+#endif /* CVC5__SMT__MODEL_H */