Use symbol manager for unsat cores (#5468)

This PR uses the symbol manager for handling names for unsat cores.

This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.

6 files changed, 22 insertions, 199 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c8362fae1..717d423fe 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2289,12 +2289,12 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
 /* class GetUnsatCoreCommand                                                  */
 /* -------------------------------------------------------------------------- */
 
-GetUnsatCoreCommand::GetUnsatCoreCommand() {}
+GetUnsatCoreCommand::GetUnsatCoreCommand() : d_sm(nullptr) {}
 void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    d_solver = solver;
+    d_sm = sm;
     d_result = solver->getUnsatCore();
 
     d_commandStatus = CommandSuccess::instance();
@@ -2318,8 +2318,20 @@ void GetUnsatCoreCommand::printResult(std::ostream& out,
   }
   else
   {
-    UnsatCore ucr(d_solver->getSmtEngine(), api::termVectorToNodes(d_result));
-    ucr.toStream(out);
+    if (options::dumpUnsatCoresFull())
+    {
+      // use the assertions
+      UnsatCore ucr(api::termVectorToNodes(d_result));
+      ucr.toStream(out);
+    }
+    else
+    {
+      // otherwise, use the names
+      std::vector<std::string> names;
+      d_sm->getExpressionNames(d_result, names, true);
+      UnsatCore ucr(names);
+      ucr.toStream(out);
+    }
   }
 }
 
@@ -2332,7 +2344,7 @@ const std::vector<api::Term>& GetUnsatCoreCommand::getUnsatCore() const
 Command* GetUnsatCoreCommand::clone() const
 {
   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
-  c->d_solver = d_solver;
+  c->d_sm = d_sm;
   c->d_result = d_result;
   return c;
 }
@@ -2710,42 +2722,6 @@ void GetOptionCommand::toStream(std::ostream& out,
 }
 
 /* -------------------------------------------------------------------------- */
-/* class SetExpressionNameCommand                                             */
-/* -------------------------------------------------------------------------- */
-
-SetExpressionNameCommand::SetExpressionNameCommand(api::Term term,
-                                                   std::string name)
-    : d_term(term), d_name(name)
-{
-}
-
-void SetExpressionNameCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
-  solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name);
-  d_commandStatus = CommandSuccess::instance();
-}
-
-Command* SetExpressionNameCommand::clone() const
-{
-  SetExpressionNameCommand* c = new SetExpressionNameCommand(d_term, d_name);
-  return c;
-}
-
-std::string SetExpressionNameCommand::getCommandName() const
-{
-  return "set-expr-name";
-}
-
-void SetExpressionNameCommand::toStream(std::ostream& out,
-                                        int toDepth,
-                                        size_t dag,
-                                        OutputLanguage language) const
-{
-  Printer::getPrinter(language)->toStreamCmdSetExpressionName(
-      out, d_term.getNode(), d_name);
-}
-
-/* -------------------------------------------------------------------------- */
 /* class DatatypeDeclarationCommand                                           */
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/smt/command.h b/src/smt/command.h
index 85897458d..96a6938d6 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1221,8 +1221,8 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
-  /** The solver we were invoked with */
-  api::Solver* d_solver;
+  /** The symbol manager we were invoked with */
+  SymbolManager* d_sm;
   /** the result of the unsat core call */
   std::vector<api::Term> d_result;
 }; /* class GetUnsatCoreCommand */
@@ -1376,32 +1376,6 @@ class CVC4_PUBLIC GetOptionCommand : public Command
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetOptionCommand */
 
-// Set expression name command
-// Note this is not an official smt2 command
-// Conceptually:
-//   (assert (! expr :named name))
-// is converted to
-//   (assert expr)
-//   (set-expr-name expr name)
-class CVC4_PUBLIC SetExpressionNameCommand : public Command
-{
- protected:
-  api::Term d_term;
-  std::string d_name;
-
- public:
-  SetExpressionNameCommand(api::Term term, std::string name);
-
-  void invoke(api::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
-}; /* class SetExpressionNameCommand */
-
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
 {
  private:
diff --git a/src/smt/expr_names.cpp b/src/smt/expr_names.cpp
deleted file mode 100644
index ccced2cac..000000000
--- a/src/smt/expr_names.cpp
+++ /dev/null
@@ -1,39 +0,0 @@
-/*********************                                                        */
-/*! \file expr_names.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utility for maintaining expression names.
- **/
-
-#include "smt/expr_names.h"
-
-namespace CVC4 {
-namespace smt {
-
-ExprNames::ExprNames(context::UserContext* u)
-    : d_exprNames(u)
-{
-}
-
-void ExprNames::setExpressionName(const Node& e, const std::string& name) {
-  d_exprNames[e] = name;
-}
-
-bool ExprNames::getExpressionName(const Node& e, std::string& name) const {
-  auto it = d_exprNames.find(e);
-  if(it!=d_exprNames.end()) {
-    name = (*it).second;
-    return true;
-  }
-  return false;
-}
-
-}  // namespace smt
-}  // namespace CVC4
diff --git a/src/smt/expr_names.h b/src/smt/expr_names.h
deleted file mode 100644
index 9a13b0c08..000000000
--- a/src/smt/expr_names.h
+++ /dev/null
@@ -1,59 +0,0 @@
-/*********************                                                        */
-/*! \file expr_names.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Aina Niemetz, Kshitij Bansal
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utility for maintaining expression names.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__SMT__EXPR_NAMES_H
-#define CVC4__SMT__EXPR_NAMES_H
-
-#include <string>
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace smt {
-
-/**
- * This utility is responsible for maintaining names for expressions.
- */
-class ExprNames
-{
- public:
-  ExprNames(context::UserContext* u);
-  /**
-   * Get expression name.
-   *
-   * Return true if given expression has a name in the current context.
-   * If it returns true, the name of expression 'e' is stored in 'name'.
-   */
-  bool getExpressionName(const Node& e, std::string& name) const;
-
-  /**
-   * Set name of given expression 'e' to 'name'.
-   *
-   * This information is user-context-dependent.
-   * If 'e' already has a name, it is overwritten.
-   */
-  void setExpressionName(const Node& e, const std::string& name);
-
- private:
-  /** mapping from expressions to name */
-  context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
-};
-
-}  // namespace smt
-}  // namespace CVC4
-
-#endif
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8aad05235..27bcdc036 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -38,7 +38,6 @@
 #include "smt/check_models.h"
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
-#include "smt/expr_names.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
 #include "smt/logic_request.h"
@@ -80,7 +79,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_nodeManager(d_exprManager->getNodeManager()),
       d_absValues(new AbstractValues(d_nodeManager)),
       d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
-      d_exprNames(new ExprNames(getUserContext())),
       d_dumpm(new DumpManager(getUserContext())),
       d_routListener(new ResourceOutListener(*this)),
       d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)),
@@ -334,7 +332,6 @@ SmtEngine::~SmtEngine()
 
     d_absValues.reset(nullptr);
     d_asserts.reset(nullptr);
-    d_exprNames.reset(nullptr);
     d_dumpm.reset(nullptr);
 
     d_sygusSolver.reset(nullptr);
@@ -1391,7 +1388,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
   }
 
   d_proofManager->traceUnsatCore();  // just to trigger core creation
-  return UnsatCore(this, d_proofManager->extractUnsatCore());
+  return UnsatCore(d_proofManager->extractUnsatCore());
 #else  /* IS_PROOFS_BUILD */
   throw ModalException(
       "This build of CVC4 doesn't have proof support (required for unsat "
@@ -1418,7 +1415,8 @@ void SmtEngine::checkUnsatCore() {
     coreChecker->declareSepHeap(sepLocType, sepDataType);
   }
 
-  Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
+  Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions"
+           << std::endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
     Node assertionAfterExpansion = expandDefinitions(*i);
     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
@@ -1857,15 +1855,6 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
   return SExpr::parseAtom(d_options.getOption(key));
 }
 
-bool SmtEngine::getExpressionName(const Node& e, std::string& name) const {
-  return d_exprNames->getExpressionName(e, name);
-}
-
-void SmtEngine::setExpressionName(const Node& e, const std::string& name) {
-  Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl;
-  d_exprNames->setExpressionName(e,name);
-}
-
 Options& SmtEngine::getOptions() { return d_options; }
 
 const Options& SmtEngine::getOptions() const { return d_options; }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index d8d2ea171..6c721b9b0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -822,22 +822,6 @@ class CVC4_PUBLIC SmtEngine
                         const std::vector<Expr>& expr_values,
                         const std::string& str_value);
 
-  /**
-   * Get expression name.
-   *
-   * Return true if given expressoion has a name in the current context.
-   * If it returns true, the name of expression 'e' is stored in 'name'.
-   */
-  bool getExpressionName(const Node& e, std::string& name) const;
-
-  /**
-   * Set name of given expression 'e' to 'name'.
-   *
-   * This information is user-context-dependent.
-   * If 'e' already has a name, it is overwritten.
-   */
-  void setExpressionName(const Node& e, const std::string& name);
-
   /** Get the options object (const and non-const versions) */
   Options& getOptions();
   const Options& getOptions() const;
@@ -1049,8 +1033,6 @@ class CVC4_PUBLIC SmtEngine
   std::unique_ptr<smt::AbstractValues> d_absValues;
   /** Assertions manager */
   std::unique_ptr<smt::Assertions> d_asserts;
-  /** Expression names */
-  std::unique_ptr<smt::ExprNames> d_exprNames;
   /** The dump manager */
   std::unique_ptr<smt::DumpManager> d_dumpm;
   /** Resource out listener */