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.

1 files changed, 19 insertions, 60 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 1e7401fa4..c8362fae1 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1278,57 +1278,6 @@ void DefineFunctionCommand::toStream(std::ostream& out,
 }
 
 /* -------------------------------------------------------------------------- */
-/* class DefineNamedFunctionCommand                                           */
-/* -------------------------------------------------------------------------- */
-
-DefineNamedFunctionCommand::DefineNamedFunctionCommand(
-
-    const std::string& id,
-    api::Term func,
-    const std::vector<api::Term>& formals,
-    api::Term formula,
-    bool global)
-    : DefineFunctionCommand(id, func, formals, formula, global)
-{
-}
-
-void DefineNamedFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
-  this->DefineFunctionCommand::invoke(solver, sm);
-  if (!d_func.isNull() && d_func.getSort().isBoolean())
-  {
-    solver->getSmtEngine()->addToAssignment(d_func.getExpr());
-  }
-  d_commandStatus = CommandSuccess::instance();
-}
-
-Command* DefineNamedFunctionCommand::clone() const
-{
-  return new DefineNamedFunctionCommand(
-      d_symbol, d_func, d_formals, d_formula, d_global);
-}
-
-void DefineNamedFunctionCommand::toStream(std::ostream& out,
-                                          int toDepth,
-                                          size_t dag,
-                                          OutputLanguage language) const
-{
-  // get the range type of the function, or the type itself
-  // if its not a function
-  TypeNode range = d_func.getSort().getTypeNode();
-  if (range.isFunction())
-  {
-    range = range.getRangeType();
-  }
-  Printer::getPrinter(language)->toStreamCmdDefineNamedFunction(
-      out,
-      d_func.toString(),
-      api::termVectorToNodes(d_formals),
-      range,
-      d_formula.getNode());
-}
-
-/* -------------------------------------------------------------------------- */
 /* class DefineFunctionRecCommand                                             */
 /* -------------------------------------------------------------------------- */
 
@@ -1663,20 +1612,30 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    std::vector<std::pair<Expr, Expr>> assignments =
-        solver->getSmtEngine()->getAssignment();
-    vector<SExpr> sexprs;
-    for (const auto& p : assignments)
+    std::map<api::Term, std::string> enames = sm->getExpressionNames();
+    std::vector<api::Term> terms;
+    std::vector<std::string> names;
+    for (const std::pair<const api::Term, std::string>& e : enames)
     {
-      vector<SExpr> v;
-      v.emplace_back(SExpr::Keyword(p.first.toString()));
-      v.emplace_back(SExpr::Keyword(p.second.toString()));
-      sexprs.emplace_back(v);
+      terms.push_back(e.first);
+      names.push_back(e.second);
+    }
+    // Must use vector version of getValue to ensure error is thrown regardless
+    // of whether terms is empty.
+    std::vector<api::Term> values = solver->getValue(terms);
+    Assert(values.size() == names.size());
+    std::vector<SExpr> sexprs;
+    for (size_t i = 0, nterms = terms.size(); i < nterms; i++)
+    {
+      std::vector<SExpr> ss;
+      ss.emplace_back(SExpr::Keyword(names[i]));
+      ss.emplace_back(SExpr::Keyword(values[i].toString()));
+      sexprs.emplace_back(ss);
     }
     d_result = SExpr(sexprs);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (RecoverableModalException& e)
+  catch (api::CVC4ApiRecoverableException& e)
   {
     d_commandStatus = new CommandRecoverableFailure(e.what());
   }