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.

1 files changed, 17 insertions, 41 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                                           */
 /* -------------------------------------------------------------------------- */