From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 28 Oct 2020 21:21:53 +0000 (-0500)
Subject: Remove more uses of Expr (#5357)
X-Git-Tag: cvc5-1.0.0~2650
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=66e80ff2464bfd7fb0904d972b43b96ff2bd9da8;p=cvc5.git

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.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index e198c0d89..be82a517f 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -51,6 +51,7 @@
 #include "options/main_options.h"
 #include "options/options.h"
 #include "options/smt_options.h"
+#include "proof/unsat_core.h"
 #include "smt/model.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_mode.h"
@@ -5145,7 +5146,7 @@ std::vector<Term> Solver::getUnsatCore(void) const
    *   return std::vector<Term>(core.begin(), core.end());
    * here since constructor is private */
   std::vector<Term> res;
-  for (const Expr& e : core)
+  for (const Node& e : core)
   {
     res.push_back(Term(this, e));
   }
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index e760c21aa..195247df7 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -23,6 +23,7 @@
 #include "printer/cvc/cvc_printer.h"
 #include "printer/smt2/smt2_printer.h"
 #include "printer/tptp/tptp_printer.h"
+#include "proof/unsat_core.h"
 #include "smt/command.h"
 #include "smt/node_command.h"
 
@@ -88,7 +89,7 @@ void Printer::toStream(std::ostream& out, const smt::Model& m) const
 void Printer::toStream(std::ostream& out, const UnsatCore& core) const
 {
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
-    toStreamCmdAssert(out, Node::fromExpr(*i));
+    toStreamCmdAssert(out, *i);
     out << std::endl;
   }
 }/* Printer::toStream(UnsatCore) */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2024c87b6..8815f9632 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -31,6 +31,7 @@
 #include "options/printer_options.h"
 #include "options/smt_options.h"
 #include "printer/dagification_visitor.h"
+#include "proof/unsat_core.h"
 #include "smt/command.h"
 #include "smt/node_command.h"
 #include "smt/smt_engine.h"
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 009f78a1d..d18d0c1fd 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -24,6 +24,7 @@
 #include "expr/node_manager.h"    // for VarNameAttr
 #include "options/language.h"     // for LANG_AST
 #include "options/smt_options.h"  // for unsat cores
+#include "proof/unsat_core.h"
 #include "smt/command.h"
 #include "smt/node_command.h"
 #include "smt/smt_engine.h"
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 */
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;
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index a7b3e149d..78d7f8c38 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/src/smt_util/boolean_simplification.h
@@ -201,18 +201,6 @@ class BooleanSimplification {
     }
   }
 
-  /**
-   * Negates an Expr, doing all the double-negation elimination that's
-   * possible.
-   *
-   * @param e the Expr to negate (cannot be the null Expr)
-   */
-  static Expr negate(Expr e)
-  {
-    ExprManagerScope ems(e);
-    return negate(Node::fromExpr(e)).toExpr();
-  }
-
   /**
    * Simplify an OR, AND, or IMPLIES.  This function is the identity
    * for all other kinds.
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 96eae4fa8..aa0e62891 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -23,7 +23,6 @@
 
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "expr/variable_type_map.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 06b884b72..33fce2e84 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -611,7 +611,7 @@ bool CegisCoreConnective::getUnsatCore(
   bool hasQuery = false;
   for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i)
   {
-    Node uassert = Node::fromExpr(*i);
+    Node uassert = *i;
     Trace("sygus-ccore-debug") << "  uc " << uassert << std::endl;
     if (queryAsserts.find(uassert) != queryAsserts.end())
     {
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 139d5f9ff..d34729dec 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -24,7 +24,6 @@
 
 #include "expr/expr_manager.h"
 #include "expr/node.h"
-#include "expr/variable_type_map.h"
 #include "smt/smt_engine.h"
 
 namespace CVC4 {