[proof-new] Adding a manager for the new unsat cores (#5723)

Based on proof nodes of refutations.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0fb50582346b5ea0be4cc60f970da5d373836909..152d2e4ffdfc04ebddc556a894ca439318edd50c 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -274,6 +274,8 @@ libcvc4_add_sources(
   smt/sygus_solver.h
   smt/term_formula_removal.cpp
   smt/term_formula_removal.h
+  smt/unsat_core_manager.cpp
+  smt/unsat_core_manager.h
   smt/update_ostream.h
   smt/witness_form.cpp
   smt/witness_form.h

diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp
new file mode 100644 (file)
index 0000000..88806ba
--- /dev/null
+++ b/src/smt/unsat_core_manager.cpp
@@ -0,0 +1,92 @@
+/*********************                                                        */
+/*! \file unsat_core_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 Implementation of the unsat core manager of SmtEngine.
+ **/
+
+#include "unsat_core_manager.h"
+
+#include "expr/proof_node_algorithm.h"
+#include "smt/assertions.h"
+
+namespace CVC4 {
+namespace smt {
+
+void UnsatCoreManager::getUnsatCore(std::shared_ptr<ProofNode> pfn,
+                                    Assertions& as,
+                                    std::vector<Node>& core)
+{
+  Trace("unsat-core") << "UCManager::getUnsatCore: final proof: " << *pfn.get()
+                      << "\n";
+  Assert(pfn->getRule() == PfRule::SCOPE);
+  std::vector<Node> fassumps;
+  expr::getFreeAssumptions(pfn->getChildren()[0].get(), fassumps);
+  Trace("unsat-core") << "UCManager::getUnsatCore: free assumptions: "
+                      << fassumps << "\n";
+  context::CDList<Node>* al = as.getAssertionList();
+  Assert(al != nullptr);
+  for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
+       ++i)
+  {
+    Trace("unsat-core") << "is assertion " << *i << " there?\n";
+    if (std::find(fassumps.begin(), fassumps.end(), *i) != fassumps.end())
+    {
+      Trace("unsat-core") << "\tyes\n";
+      core.push_back(*i);
+    }
+  }
+  if (Trace.isOn("unsat-core"))
+  {
+    Trace("unsat-core") << "UCManager::getUnsatCore():\n";
+    for (const Node& n : core)
+    {
+      Trace("unsat-core") << "- " << n << "\n";
+    }
+  }
+}
+
+void UnsatCoreManager::getRelevantInstantiations(
+    std::shared_ptr<ProofNode> pfn,
+    std::map<Node, std::vector<std::vector<Node>>>& insts)
+{
+  std::unordered_map<ProofNode*, bool> visited;
+  std::unordered_map<ProofNode*, bool>::iterator it;
+  std::vector<std::shared_ptr<ProofNode>> visit;
+
+  std::shared_ptr<ProofNode> cur;
+  visit.push_back(pfn);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur.get());
+    if (it != visited.end())
+    {
+      continue;
+    }
+    visited[cur.get()] = true;
+    const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
+    if (cur->getRule() == PfRule::INSTANTIATE)
+    {
+      const std::vector<Node>& instTerms = cur->getArguments();
+      Assert(cs.size() == 1);
+      Node q = cs[0]->getResult();
+      insts[q].push_back({instTerms.begin(), instTerms.end()});
+    }
+    for (const std::shared_ptr<ProofNode>& cp : cs)
+    {
+      visit.push_back(cp);
+    }
+  } while (!visit.empty());
+}
+
+}  // namespace smt
+}  // namespace CVC4

diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h
new file mode 100644 (file)
index 0000000..25be8b8
--- /dev/null
+++ b/src/smt/unsat_core_manager.h
@@ -0,0 +1,73 @@
+/*********************                                                        */
+/*! \file unsat_core_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 The unsat core manager of SmtEngine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__UNSAT_CORE_MANAGER_H
+#define CVC4__SMT__UNSAT_CORE_MANAGER_H
+
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "expr/node.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+
+namespace smt {
+
+class Assertions;
+
+/**
+ * This class is responsible for managing the proof output of SmtEngine, as
+ * well as setting up the global proof checker and proof node manager.
+ */
+class UnsatCoreManager
+{
+ public:
+  UnsatCoreManager() {}
+  ~UnsatCoreManager(){};
+
+  /** Gets the unsat core.
+   *
+   * The unsat core is the intersection of the assertions in as and the free
+   * assumptions of the underlying refutation proof of pfn. Note that pfn must
+   * be a "final proof", which means that it's a proof of false under a scope
+   * containing all assertions.
+   *
+   * The unsat core is stored in the core argument.
+   */
+  void getUnsatCore(std::shared_ptr<ProofNode> pfn,
+                    Assertions& as,
+                    std::vector<Node>& core);
+
+  /** Gets the relevant instaniations for the refutation.
+   *
+   * The relevant instantiations are all the conclusions of proof nodes of type
+   * INSTANTIATE that occur in pfn.
+   *
+   * This method populates the insts map from quantified formulas occurring as
+   * premises of INSTANTIATE proof nodes to its instantiations, which are a
+   * matrix with each row corresponding to the terms with which the respective
+   * quantified formula is instiated.
+   */
+  void getRelevantInstantiations(
+      std::shared_ptr<ProofNode> pfn,
+      std::map<Node, std::vector<std::vector<Node>>>& insts);
+
+}; /* class UnsatCoreManager */
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__UNSAT_CORE_MANAGER_H */