Refactor SMT-level model object (#5277)

This refactors the SMT-level model object so that it is a wrapper around TheoryModel instead of a base class. This inheritance was unnecessary.

Moreover, it removes the virtual base models of the SMT-level model which were based on Expr. Now the interface is more minimal and in terms of Node only.

This PR further simplifies a few places in the code that interface with the SmtEngine with things related to models.

2 files changed, 16 insertions, 14 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6d75279e5..2024c87b6 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1323,11 +1323,12 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
   out << ")" << endl;
 }/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
 
-void Smt2Printer::toStream(std::ostream& out, const Model& m) 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;
-  m.getComments( c );
+  tm->getComments(c);
   std::string ln;
   while( std::getline( c, ln ) ){
     out << "; " << ln << std::endl;
@@ -1339,8 +1340,9 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const
   this->Printer::toStream(out, m);
   out << ")" << endl;
   //print the heap model, if it exists
-  Expr h, neq;
-  if( m.getHeapModel( h, neq ) ){
+  Node h, neq;
+  if (tm->getHeapModel(h, neq))
+  {
     // description of the heap+what nil is equal to fully describes model
     out << "(heap" << endl;
     out << h << endl;
@@ -1350,11 +1352,10 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const
 }
 
 void Smt2Printer::toStream(std::ostream& out,
-                           const Model& model,
+                           const smt::Model& model,
                            const NodeCommand* command) const
 {
-  const theory::TheoryModel* theory_model =
-      dynamic_cast<const theory::TheoryModel*>(&model);
+  const theory::TheoryModel* theory_model = model.getTheoryModel();
   AlwaysAssert(theory_model != nullptr);
   if (const DeclareTypeNodeCommand* dtc =
           dynamic_cast<const DeclareTypeNodeCommand*>(command))
@@ -1367,7 +1368,7 @@ void Smt2Printer::toStream(std::ostream& out,
     }
     else
     {
-      std::vector<Expr> elements = theory_model->getDomainElements(tn.toType());
+      std::vector<Node> elements = theory_model->getDomainElements(tn);
       if (options::modelUninterpDtEnum())
       {
         if (isVariant_2_6(d_variant))
@@ -1378,7 +1379,7 @@ void Smt2Printer::toStream(std::ostream& out,
         {
           out << "(declare-datatypes () ((" << (*dtc).getSymbol() << " ";
         }
-        for (const Expr& type_ref : elements)
+        for (const Node& type_ref : elements)
         {
           out << "(" << type_ref << ")";
         }
@@ -1390,9 +1391,8 @@ void Smt2Printer::toStream(std::ostream& out,
         out << "; cardinality of " << tn << " is " << elements.size() << endl;
         out << (*dtc) << endl;
         // print the representatives
-        for (const Expr& type_ref : elements)
+        for (const Node& trn : elements)
         {
-          Node trn = Node::fromExpr(type_ref);
           if (trn.isVar())
           {
             out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")"
@@ -1423,7 +1423,9 @@ void Smt2Printer::toStream(std::ostream& out,
       // don't print out internal stuff
       return;
     }
-    Node val = theory_model->getSmtEngine()->getValue(n);
+    // We get the value from the theory model directly, which notice
+    // does not have to go through the standard SmtEngine::getValue interface.
+    Node val = theory_model->getValue(n);
     if (val.getKind() == kind::LAMBDA)
     {
       out << "(define-fun " << n << " " << val[0] << " "
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 3160771da..ed04da983 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -45,7 +45,7 @@ class Smt2Printer : public CVC4::Printer
                 bool types,
                 size_t dag) const override;
   void toStream(std::ostream& out, const CommandStatus* s) const override;
-  void toStream(std::ostream& out, const Model& m) const override;
+  void toStream(std::ostream& out, const smt::Model& m) const override;
   /**
    * Writes the unsat core to the stream out.
    * We use the expression names that are stored in the SMT engine associated
@@ -231,7 +231,7 @@ class Smt2Printer : public CVC4::Printer
   void toStream(
       std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const;
   void toStream(std::ostream& out,
-                const Model& m,
+                const smt::Model& m,
                 const NodeCommand* c) const override;
   void toStream(std::ostream& out, const SExpr& sexpr) const;
   void toStream(std::ostream& out, const DType& dt) const;