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.

16 files changed, 56 insertions, 332 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index a7cc8e17f..1112530d3 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -5160,11 +5160,11 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
-  CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
+  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
-  CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
-      << "Cannot get value when in unsat mode.";
+  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+      << "Cannot get value unless after a SAT or unknown response.";
   std::vector<Term> res;
   for (size_t i = 0, n = terms.size(); i < n; ++i)
   {
@@ -5222,8 +5222,8 @@ Term Solver::getSeparationHeap() const
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get separation heap term unless model generation is enabled "
          "(try --produce-models)";
-  CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
-      << "Cannot get separtion heap term when in unsat mode.";
+  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+      << "Can only get separtion heap term after sat or unknown response.";
   return Term(this, d_smtEngine->getSepHeapExpr());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5239,8 +5239,8 @@ Term Solver::getSeparationNilTerm() const
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get separation nil term unless model generation is enabled "
          "(try --produce-models)";
-  CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
-      << "Cannot get separtion nil term when in unsat mode.";
+  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+      << "Can only get separtion nil term after sat or unknown response.";
   return Term(this, d_smtEngine->getSepNilExpr());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5330,8 +5330,8 @@ void Solver::printModel(std::ostream& out) const
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
-  CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
-      << "Cannot get value when in unsat mode.";
+  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+      << "Can only get value after sat or unknown response.";
   out << *d_smtEngine->getModel();
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5343,8 +5343,8 @@ void Solver::blockModel() const
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
-  CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
-      << "Cannot get value when in unsat mode.";
+  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+      << "Can only block model after sat or unknown response.";
   d_smtEngine->blockModel();
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5355,8 +5355,8 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
-  CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
-      << "Cannot get value when in unsat mode.";
+  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+      << "Can only block model values after sat or unknown response.";
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms)
       << "a non-empty set of terms";
   for (size_t i = 0, tsize = terms.size(); i < tsize; ++i)
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 916e20d9b..2b32afa15 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1841,18 +1841,8 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
     {
       attr = std::string(":named");
-      api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr);
-      std::string name = sexpr.getValue();
-      // bind name to expr with define-fun
-      // TODO (projects-248) SYM_MAN->setExpressionName(func, name, false);
-      Command* c =
-          new DefineNamedFunctionCommand(name,
-                                         func,
-                                         std::vector<api::Term>(),
-                                         expr,
-                                         SYM_MAN->getGlobalDeclarations());
-      c->setMuted(true);
-      PARSER_STATE->preemptCommand(c);
+      // notify that expression was given a name
+      PARSER_STATE->notifyNamedExpression(expr, sexpr.getValue());
     }
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 892c628dc..b9279fcb0 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1218,28 +1218,16 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   return ret;
 }
 
-api::Term Smt2::setNamedAttribute(api::Term& expr, const SExpr& sexpr)
+void Smt2::notifyNamedExpression(api::Term& expr, std::string name)
 {
-  if (!sexpr.isKeyword())
-  {
-    parseError("improperly formed :named annotation");
-  }
-  std::string name = sexpr.getValue();
   checkUserSymbol(name);
-  // ensure expr is a closed subterm
-  if (expr.getExpr().hasFreeVariable())
-  {
-    std::stringstream ss;
-    ss << ":named annotations can only name terms that are closed";
-    parseError(ss.str());
-  }
-  // check that sexpr is a fresh function symbol, and reserve it
-  reserveSymbolAtAssertionLevel(name);
-  // define it
-  api::Term func = bindVar(name, expr.getSort(), ExprManager::VAR_FLAG_DEFINED);
-  // remember the last term to have been given a :named attribute
+  // remember the expression name in the symbol manager
+  getSymbolManager()->setExpressionName(expr, name, false);
+  // define the variable
+  defineVar(name, expr);
+  // set the last named term, which ensures that we catch when assertions are
+  // named
   setLastNamedTerm(expr, name);
-  return func;
 }
 
 api::Term Smt2::mkAnd(const std::vector<api::Term>& es)
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 734b00f92..fd08ab241 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -343,17 +343,11 @@ class Smt2 : public Parser
     }
     this->Parser::checkDeclaration(name, check, type, notes);
   }
-  /** Set named attribute
-   *
-   * This is called when expression expr is annotated with a name, i.e.
-   * (! expr :named sexpr). It sets up the necessary information to process
-   * this naming, including marking that expr is the last named term.
-   *
-   * We construct an expression symbol whose name is the name of s-expression
-   * which is used later for tracking assertions in unsat cores. This
-   * symbol is returned by this method.
+  /**
+   * Notify that expression expr was given name std::string via a :named
+   * attribute.
    */
-  api::Term setNamedAttribute(api::Term& expr, const SExpr& sexpr);
+  void notifyNamedExpression(api::Term& expr, std::string name);
 
   // Throw a ParserException with msg appended with the current logic.
   inline void parseErrorLogic(const std::string& msg)
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,
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());
   }
diff --git a/src/smt/command.h b/src/smt/command.h
index 7d794cf3f..85897458d 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -496,28 +496,6 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
 }; /* class DefineFunctionCommand */
 
 /**
- * This differs from DefineFunctionCommand only in that it instructs
- * the SmtEngine to "remember" this function for later retrieval with
- * getAssignment().  Used for :named attributes in SMT-LIBv2.
- */
-class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
-{
- public:
-  DefineNamedFunctionCommand(const std::string& id,
-                             api::Term func,
-                             const std::vector<api::Term>& formals,
-                             api::Term formula,
-                             bool global);
-  void invoke(api::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
-}; /* class DefineNamedFunctionCommand */
-
-/**
  * The command when parsing define-fun-rec or define-funs-rec.
  * This command will assert a set of quantified formulas that specify
  * the (mutually recursive) function definitions provided to it.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a5861c6b0..9826cd097 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -102,7 +102,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_abductSolver(nullptr),
       d_interpolSolver(nullptr),
       d_quantElimSolver(nullptr),
-      d_assignments(nullptr),
       d_logic(),
       d_originalOptions(),
       d_isInternalSubsolver(false),
@@ -176,6 +175,11 @@ size_t SmtEngine::getNumUserLevels() const
   return d_state->getNumUserLevels();
 }
 SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); }
+bool SmtEngine::isSmtModeSat() const
+{
+  SmtMode mode = getSmtMode();
+  return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN;
+}
 Result SmtEngine::getStatusOfLastCommand() const
 {
   return d_state->getStatus();
@@ -318,10 +322,6 @@ SmtEngine::~SmtEngine()
     // of context-dependent data structures
     d_state->cleanup();
 
-    if(d_assignments != NULL) {
-      d_assignments->deleteSelf();
-    }
-
     d_definedFunctions->deleteSelf();
 
     //destroy all passes before destroying things that they refer to
@@ -1227,99 +1227,6 @@ std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs)
   return result;
 }
 
-bool SmtEngine::addToAssignment(const Expr& ex) {
-  SmtScope smts(this);
-  finishInit();
-  d_state->doPendingPops();
-  // Substitute out any abstract values in ex
-  Node n = d_absValues->substituteAbstractValues(Node::fromExpr(ex));
-  TypeNode type = n.getType(options::typeChecking());
-  // must be Boolean
-  PrettyCheckArgument(type.isBoolean(),
-                      n,
-                      "expected Boolean-typed variable or function application "
-                      "in addToAssignment()");
-  // must be a defined constant, or a variable
-  PrettyCheckArgument(
-      (((d_definedFunctions->find(n) != d_definedFunctions->end())
-        && n.getNumChildren() == 0)
-       || n.isVar()),
-      n,
-      "expected variable or defined-function application "
-      "in addToAssignment(),\ngot %s",
-      n.toString().c_str());
-  if(!options::produceAssignments()) {
-    return false;
-  }
-  if(d_assignments == NULL) {
-    d_assignments = new (true) AssignmentSet(getContext());
-  }
-  d_assignments->insert(n);
-
-  return true;
-}
-
-// TODO(#1108): Simplify the error reporting of this method.
-vector<pair<Expr, Expr>> SmtEngine::getAssignment()
-{
-  Trace("smt") << "SMT getAssignment()" << endl;
-  SmtScope smts(this);
-  finishInit();
-  if(Dump.isOn("benchmark")) {
-    getOutputManager().getPrinter().toStreamCmdGetAssignment(
-        getOutputManager().getDumpOut());
-  }
-  if(!options::produceAssignments()) {
-    const char* msg =
-      "Cannot get the current assignment when "
-      "produce-assignments option is off.";
-    throw ModalException(msg);
-  }
-
-  // Get the model here, regardless of whether d_assignments is null, since
-  // we should throw errors related to model availability whether or not
-  // assignments is null.
-  Model* m = getAvailableModel("get assignment");
-
-  vector<pair<Expr,Expr>> res;
-  if (d_assignments != nullptr)
-  {
-    TypeNode boolType = d_nodeManager->booleanType();
-    for (AssignmentSet::key_iterator i = d_assignments->key_begin(),
-                                     iend = d_assignments->key_end();
-         i != iend;
-         ++i)
-    {
-      Node as = *i;
-      Assert(as.getType() == boolType);
-
-      Trace("smt") << "--- getting value of " << as << endl;
-
-      // Expand, then normalize
-      std::unordered_map<Node, Node, NodeHashFunction> cache;
-      Node n = d_pp->expandDefinitions(as, cache);
-      n = Rewriter::rewrite(n);
-
-      Trace("smt") << "--- getting value of " << n << endl;
-      Node resultNode;
-      if (m != nullptr)
-      {
-        resultNode = m->getValue(n);
-      }
-
-      // type-check the result we got
-      Assert(resultNode.isNull() || resultNode.getType() == boolType);
-
-      // ensure it's a constant
-      Assert(resultNode.isConst());
-
-      Assert(as.isVar());
-      res.emplace_back(as.toExpr(), resultNode.toExpr());
-    }
-  }
-  return res;
-}
-
 // TODO(#1108): Simplify the error reporting of this method.
 Model* SmtEngine::getModel() {
   Trace("smt") << "SMT getModel()" << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0661ae918..7a55d3b74 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -206,6 +206,12 @@ class CVC4_PUBLIC SmtEngine
   /** Return the current mode of the solver. */
   SmtMode getSmtMode() const;
   /**
+   * Whether the SmtMode allows for get-value, get-model, get-assignment, etc.
+   * This is equivalent to:
+   * getSmtMode()==SmtMode::SAT || getSmtMode()==SmtMode::SAT_UNKNOWN
+   */
+  bool isSmtModeSat() const;
+  /**
    * Returns the most recent result of checkSat/checkEntailed or
    * (set-info :status).
    */
@@ -548,24 +554,6 @@ class CVC4_PUBLIC SmtEngine
    */
   std::vector<Node> getValues(const std::vector<Node>& exprs);
 
-  /**
-   * Add a function to the set of expressions whose value is to be
-   * later returned by a call to getAssignment().  The expression
-   * should be a Boolean zero-ary defined function or a Boolean
-   * variable.  Rather than throwing a ModalException on modal
-   * failures (not in interactive mode or not producing assignments),
-   * this function returns true if the expression was added and false
-   * if this request was ignored.
-   */
-  bool addToAssignment(const Expr& e);
-
-  /**
-   * Get the assignment (only if immediately preceded by a SAT or
-   * NOT_ENTAILED query).  Only permitted if the SmtEngine is set to
-   * operate interactively and produce-assignments is on.
-   */
-  std::vector<std::pair<Expr, Expr> > getAssignment();
-
   /** Print all instantiations made by the quantifiers module.  */
   void printInstantiations(std::ostream& out);
 
@@ -907,8 +895,6 @@ class CVC4_PUBLIC SmtEngine
       DefinedFunctionMap;
   /** The type of our internal assertion list */
   typedef context::CDList<Node> AssertionList;
-  /** The type of our internal assignment set */
-  typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
 
   // disallow copy/assignment
   SmtEngine(const SmtEngine&) = delete;
@@ -1146,11 +1132,6 @@ class CVC4_PUBLIC SmtEngine
   /** The solver for quantifier elimination queries */
   std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver;
   /**
-   * List of items for which to retrieve values using getAssignment().
-   */
-  AssignmentSet* d_assignments;
-
-  /**
    * The logic we're in. This logic may be an extension of the logic set by the
    * user.
    */