Remove more uses of Expr (#5357)

This PR removes more uses of Expr, mostly related to UnsatCore.

It makes UnsatCore a cvc4_private object storing Node instead of Expr.

4 files changed, 16 insertions, 12 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index eb03edf4f..9b0784831 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -32,6 +32,7 @@
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
+#include "proof/unsat_core.h"
 #include "smt/dump.h"
 #include "smt/model.h"
 #include "smt/smt_engine.h"
@@ -2341,8 +2342,8 @@ void GetUnsatCoreCommand::invoke(api::Solver* solver)
 {
   try
   {
-    d_result = UnsatCore(solver->getSmtEngine(),
-                         api::termVectorToExprs(solver->getUnsatCore()));
+    d_solver = solver;
+    d_result = solver->getUnsatCore();
 
     d_commandStatus = CommandSuccess::instance();
   }
@@ -2365,11 +2366,12 @@ void GetUnsatCoreCommand::printResult(std::ostream& out,
   }
   else
   {
-    d_result.toStream(out);
+    UnsatCore ucr(d_solver->getSmtEngine(), api::termVectorToNodes(d_result));
+    ucr.toStream(out);
   }
 }
 
-const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const
+const std::vector<api::Term>& GetUnsatCoreCommand::getUnsatCore() const
 {
   // of course, this will be empty if the command hasn't been invoked yet
   return d_result;
@@ -2378,6 +2380,7 @@ const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const
 Command* GetUnsatCoreCommand::clone() const
 {
   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
+  c->d_solver = d_solver;
   c->d_result = d_result;
   return c;
 }
diff --git a/src/smt/command.h b/src/smt/command.h
index b81b55b91..7088c09ed 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -31,8 +31,6 @@
 #include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "expr/type.h"
-#include "expr/variable_type_map.h"
-#include "proof/unsat_core.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 
@@ -43,6 +41,7 @@ class Solver;
 class Term;
 }  // namespace api
 
+class UnsatCore;
 class SmtEngine;
 class Command;
 class CommandStatus;
@@ -1224,7 +1223,7 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
 {
  public:
   GetUnsatCoreCommand();
-  const UnsatCore& getUnsatCore() const;
+  const std::vector<api::Term>& getUnsatCore() const;
 
   void invoke(api::Solver* solver) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
@@ -1239,8 +1238,10 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
-  // the result of the unsat core call
-  UnsatCore d_result;
+  /** The solver we were invoked with */
+  api::Solver* d_solver;
+  /** the result of the unsat core call */
+  std::vector<api::Term> d_result;
 }; /* class GetUnsatCoreCommand */
 
 class CVC4_PUBLIC GetAssertionsCommand : public Command
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d0906ce98..dc5338199 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1028,7 +1028,7 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
   std::vector<Node>& assumps = d_asserts->getAssumptions();
   for (const Node& e : assumps)
   {
-    if (std::find(core.begin(), core.end(), e.toExpr()) != core.end())
+    if (std::find(core.begin(), core.end(), e) != core.end())
     {
       res.push_back(e);
     }
@@ -1490,7 +1490,7 @@ void SmtEngine::checkUnsatCore() {
 
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
-    Node assertionAfterExpansion = expandDefinitions(Node::fromExpr(*i));
+    Node assertionAfterExpansion = expandDefinitions(*i);
     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
              << ", expanded to " << assertionAfterExpansion << "\n";
     coreChecker.assertFormula(assertionAfterExpansion);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 53e982a2d..de0daffd0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -29,7 +29,6 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "options/options.h"
-#include "proof/unsat_core.h"
 #include "smt/logic_exception.h"
 #include "smt/output_manager.h"
 #include "smt/smt_mode.h"
@@ -59,6 +58,7 @@ class DecisionEngine;
 class TheoryEngine;
 
 class ProofManager;
+class UnsatCore;
 
 class LogicRequest;
 class StatisticsRegistry;