Use symbol manager for get assignment (#5451)

This replaces the previous methods for get-assignment which involving making a DefinedNamedFunctIonCommand and storing the expression names map in the SmtEngine.

Note: we now limit :named terms to those not beneath quantifiers and let-bindings.

8 files changed, 0 insertions, 73 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 76549d01d..8bf3bd24e 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -296,18 +296,6 @@ void AstPrinter::toStreamCmdDefineType(std::ostream& out,
   out << "]," << t << ')' << std::endl;
 }
 
-void AstPrinter::toStreamCmdDefineNamedFunction(
-    std::ostream& out,
-    const std::string& id,
-    const std::vector<Node>& formals,
-    TypeNode range,
-    Node formula) const
-{
-  out << "DefineNamedFunction( ";
-  toStreamCmdDefineFunction(out, id, formals, range, formula);
-  out << " )" << std::endl;
-}
-
 void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
   out << "Simplify( << " << n << " >> )" << std::endl;
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index ce621d8e1..ad20ffb79 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -79,13 +79,6 @@ class AstPrinter : public CVC4::Printer
                                  TypeNode range,
                                  Node formula) const override;
 
-  /** Print define-named-fun command */
-  void toStreamCmdDefineNamedFunction(std::ostream& out,
-                                      const std::string& id,
-                                      const std::vector<Node>& formals,
-                                      TypeNode range,
-                                      Node formula) const override;
-
   /** Print check-sat command */
   void toStreamCmdCheckSat(std::ostream& out,
                            Node n = Node::null()) const override;
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 8b252d0ea..44ff7be10 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1410,16 +1410,6 @@ void CvcPrinter::toStreamCmdDefineType(std::ostream& out,
   }
 }
 
-void CvcPrinter::toStreamCmdDefineNamedFunction(
-    std::ostream& out,
-    const std::string& id,
-    const std::vector<Node>& formals,
-    TypeNode range,
-    Node formula) const
-{
-  toStreamCmdDefineFunction(out, id, formals, range, formula);
-}
-
 void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
   out << "TRANSFORM " << n << ';' << std::endl;
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 934caf91b..ee4750a61 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -80,13 +80,6 @@ class CvcPrinter : public CVC4::Printer
                                  TypeNode range,
                                  Node formula) const override;
 
-  /** Print define-named-fun command */
-  void toStreamCmdDefineNamedFunction(std::ostream& out,
-                                      const std::string& id,
-                                      const std::vector<Node>& formals,
-                                      TypeNode range,
-                                      Node formula) const override;
-
   /** Print check-sat command */
   void toStreamCmdCheckSat(std::ostream& out,
                            Node n = Node::null()) const override;
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 21eb88c8c..b24025124 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -184,15 +184,6 @@ void Printer::toStreamCmdDefineFunction(std::ostream& out,
   printUnknownCommand(out, "define-fun");
 }
 
-void Printer::toStreamCmdDefineNamedFunction(std::ostream& out,
-                                             const std::string& id,
-                                             const std::vector<Node>& formals,
-                                             TypeNode range,
-                                             Node formula) const
-{
-  printUnknownCommand(out, "define-named-function");
-}
-
 void Printer::toStreamCmdDefineFunctionRec(
     std::ostream& out,
     const std::vector<Node>& funcs,
diff --git a/src/printer/printer.h b/src/printer/printer.h
index ffacaa5d8..d32418deb 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -103,13 +103,6 @@ class Printer
                                          TypeNode range,
                                          Node formula) const;
 
-  /** Print define-named-fun command */
-  virtual void toStreamCmdDefineNamedFunction(std::ostream& out,
-                                              const std::string& id,
-                                              const std::vector<Node>& formals,
-                                              TypeNode range,
-                                              Node formula) const;
-
   /** Print define-fun-rec command */
   virtual void toStreamCmdDefineFunctionRec(
       std::ostream& out,
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6628576dd..bed6a890b 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1715,20 +1715,6 @@ void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
   out << ") " << t << ")" << std::endl;
 }
 
-void Smt2Printer::toStreamCmdDefineNamedFunction(
-    std::ostream& out,
-    const std::string& id,
-    const std::vector<Node>& formals,
-    TypeNode range,
-    Node formula) const
-{
-  out << "DefineNamedFunction( ";
-  toStreamCmdDefineFunction(out, id, formals, range, formula);
-  out << " )" << std::endl;
-
-  printUnknownCommand(out, "define-named-function");
-}
-
 void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
   out << "(simplify " << n << ')' << std::endl;
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 3fc144d46..bc8674275 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -92,13 +92,6 @@ class Smt2Printer : public CVC4::Printer
                                  TypeNode range,
                                  Node formula) const override;
 
-  /** Print define-named-fun command */
-  void toStreamCmdDefineNamedFunction(std::ostream& out,
-                                      const std::string& id,
-                                      const std::vector<Node>& formals,
-                                      TypeNode range,
-                                      Node formula) const override;
-
   /** Print define-fun-rec command */
   void toStreamCmdDefineFunctionRec(
       std::ostream& out,