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.

3 files changed, 34 insertions, 29 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 93b07b762..20b0e8a92 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -95,17 +95,18 @@ void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
   d_cnfProof->popCurrentAssertion();
 }
 
-
-void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) {
+void ProofManager::traceDeps(TNode n, CDNodeSet* coreAssertions)
+{
   Debug("cores") << "trace deps " << n << std::endl;
   if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) ||
       (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
     return;
   }
-  if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
+  if (d_inputCoreFormulas.find(n) != d_inputCoreFormulas.end())
+  {
     // originating formula was in core set
     Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
-    coreAssertions->insert(n.toExpr());
+    coreAssertions->insert(n);
   } else {
     Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
     if(d_deps.find(n) == d_deps.end()) {
@@ -151,8 +152,9 @@ bool ProofManager::unsatCoreAvailable() const {
   return d_satProof->derivedEmptyClause();
 }
 
-std::vector<Expr> ProofManager::extractUnsatCore() {
-  std::vector<Expr> result;
+std::vector<Node> ProofManager::extractUnsatCore()
+{
+  std::vector<Node> result;
   output_core_iterator it = begin_unsat_core();
   output_core_iterator end = end_unsat_core();
   while ( it != end ) {
@@ -190,9 +192,10 @@ void ProofManager::getLemmasInUnsatCore(std::vector<Node>& lemmas)
   }
 }
 
-void ProofManager::addCoreAssertion(Expr formula) {
+void ProofManager::addCoreAssertion(Node formula)
+{
   Debug("cores") << "assert: " << formula << std::endl;
-  d_deps[Node::fromExpr(formula)]; // empty vector of deps
+  d_deps[formula];  // empty vector of deps
   d_inputCoreFormulas.insert(formula);
 }
 
@@ -208,7 +211,8 @@ void ProofManager::addDependence(TNode n, TNode dep) {
   }
 }
 
-void ProofManager::addUnsatCore(Expr formula) {
+void ProofManager::addUnsatCore(Node formula)
+{
   Assert(d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
   d_outputCoreFormulas.insert(formula);
 }
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 1c2a1ce9a..7276f6402 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -57,7 +57,7 @@ namespace prop {
 }/* CVC4::prop namespace */
 
 typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
-typedef context::CDHashSet<Expr, ExprHashFunction> CDExprSet;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
 typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction> CDNodeToNodes;
 typedef std::unordered_set<ClauseId> IdHashSet;
 
@@ -68,8 +68,8 @@ class ProofManager {
   std::unique_ptr<CnfProof> d_cnfProof;
 
   // information that will need to be shared across proofs
-  CDExprSet    d_inputCoreFormulas;
-  CDExprSet    d_outputCoreFormulas;
+  CDNodeSet d_inputCoreFormulas;
+  CDNodeSet d_outputCoreFormulas;
 
   int d_nextId;
 
@@ -90,16 +90,16 @@ public:
  static CnfProof* getCnfProof();
 
  /** Public unsat core methods **/
- void addCoreAssertion(Expr formula);
+ void addCoreAssertion(Node formula);
 
  void addDependence(TNode n, TNode dep);
- void addUnsatCore(Expr formula);
+ void addUnsatCore(Node formula);
 
  // trace dependences back to unsat core
- void traceDeps(TNode n, CDExprSet* coreAssertions);
+ void traceDeps(TNode n, CDNodeSet* coreAssertions);
  void traceUnsatCore();
 
- typedef CDExprSet::const_iterator output_core_iterator;
+ typedef CDNodeSet::const_iterator output_core_iterator;
 
  output_core_iterator begin_unsat_core() const
  {
@@ -110,7 +110,7 @@ public:
    return d_outputCoreFormulas.end();
  }
  size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
- std::vector<Expr> extractUnsatCore();
+ std::vector<Node> extractUnsatCore();
 
  bool unsatCoreAvailable() const;
  void getLemmasInUnsatCore(std::vector<Node>& lemmas);
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index f50cabbe6..b0e3de24e 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -15,7 +15,7 @@
  ** \todo document this file
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
 #ifndef CVC4__UNSAT_CORE_H
 #define CVC4__UNSAT_CORE_H
@@ -23,29 +23,27 @@
 #include <iosfwd>
 #include <vector>
 
-#include "expr/expr.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 
 class SmtEngine;
-class UnsatCore;
-
-std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC;
-
-class CVC4_PUBLIC UnsatCore {
-  friend std::ostream& operator<<(std::ostream&, const UnsatCore&);
 
+class UnsatCore
+{
   /** The SmtEngine we're associated with */
   SmtEngine* d_smt;
 
-  std::vector<Expr> d_core;
+  std::vector<Node> d_core;
 
   void initMessage() const;
 
 public:
   UnsatCore() : d_smt(NULL) {}
 
-  UnsatCore(SmtEngine* smt, std::vector<Expr> core) : d_smt(smt), d_core(core) {
+  UnsatCore(SmtEngine* smt, const std::vector<Node>& core)
+      : d_smt(smt), d_core(core)
+  {
     initMessage();
   }
 
@@ -56,8 +54,8 @@ public:
 
   size_t size() const { return d_core.size(); }
 
-  typedef std::vector<Expr>::const_iterator iterator;
-  typedef std::vector<Expr>::const_iterator const_iterator;
+  typedef std::vector<Node>::const_iterator iterator;
+  typedef std::vector<Node>::const_iterator const_iterator;
 
   const_iterator begin() const;
   const_iterator end() const;
@@ -69,6 +67,9 @@ public:
 
 };/* class UnsatCore */
 
+/** Print the unsat core to stream out */
+std::ostream& operator<<(std::ostream& out, const UnsatCore& core);
+
 }/* CVC4 namespace */
 
 #endif /* CVC4__UNSAT_CORE_H */