[proofs] [sat] Add manager for optimized clauses and their proofs (#7824)

This utility is going to be used by both the proof cnf stream and the sat proof manager to re-add to their respective internal proofs the proof nodes that were stored for clauses saved within the SAT solver at an assertion level below the current user level.

The utility is a context notify object, which means that it can be called when the tracked context pops.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1ee7260475a8f7f7478d2b22e33b08f93db2d889..7a62a327aad0ee4002e017d0c412c70a507a32ef 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -237,6 +237,8 @@ libcvc5_add_sources(
   prop/cryptominisat.h
   prop/kissat.cpp
   prop/kissat.h
+  prop/opt_clauses_manager.cpp
+  prop/opt_clauses_manager.h
   prop/proof_cnf_stream.cpp
   prop/proof_cnf_stream.h
   prop/minisat/core/Dimacs.h

diff --git a/src/prop/opt_clauses_manager.cpp b/src/prop/opt_clauses_manager.cpp
new file mode 100644 (file)
index 0000000..20dee72
--- /dev/null
+++ b/src/prop/opt_clauses_manager.cpp
@@ -0,0 +1,85 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Implementation of lazy proof utility.
+ */
+
+#include "prop/opt_clauses_manager.h"
+
+#include "proof/proof_node.h"
+
+namespace cvc5 {
+namespace prop {
+
+OptimizedClausesManager::OptimizedClausesManager(
+    context::Context* context,
+    CDProof* parentProof,
+    std::map<int, std::vector<std::shared_ptr<ProofNode>>>& optProofs)
+    : context::ContextNotifyObj(context),
+      d_context(context),
+      d_optProofs(optProofs),
+      d_parentProof(parentProof)
+{
+}
+
+void OptimizedClausesManager::contextNotifyPop()
+{
+  int newLvl = d_context->getLevel();
+  Trace("sat-proof") << "contextNotifyPop: called with lvl " << newLvl << "\n"
+                     << push;
+  // the increment is handled inside the loop, so that we can erase as we go
+  for (auto it = d_optProofs.cbegin(); it != d_optProofs.cend();)
+  {
+    if (it->first <= newLvl)
+    {
+      Trace("sat-proof") << "Should re-add pfs of [" << it->first << "]:\n";
+      for (const auto& pf : it->second)
+      {
+        Node processedPropgation = pf->getResult();
+        Trace("sat-proof") << "\t- " << processedPropgation << "\n";
+        Trace("sat-proof-debug") << "\t\t{" << pf << "} " << *pf.get() << "\n";
+        // Note that this proof may have already been added in a previous
+        // pop. For example, if a proof associated with level 1 was added
+        // when going down from 2 to 1, but then we went up to 2 again, when
+        // we go back to 1 the proof will still be there. Note that if say
+        // we had a proof of level 1 that was added at level 2 when we were
+        // going down from 3, we'd still need to add it again when going to
+        // level 1, since it'd be popped in that case.
+        if (!d_parentProof->hasStep(processedPropgation))
+        {
+          d_parentProof->addProof(pf);
+        }
+        else
+        {
+          Trace("sat-proof")
+              << "\t..skipped since its proof was already added\n";
+        }
+      }
+      ++it;
+      continue;
+    }
+    if (Trace.isOn("sat-proof"))
+    {
+      Trace("sat-proof") << "Should remove from map pfs of [" << it->first
+                         << "]:\n";
+      for (const auto& pf : it->second)
+      {
+        Trace("sat-proof") << "\t- " << pf->getResult() << "\n";
+      }
+    }
+    it = d_optProofs.erase(it);
+  }
+  Trace("sat-proof") << pop;
+}
+
+}  // namespace prop
+}  // namespace cvc5

diff --git a/src/prop/opt_clauses_manager.h b/src/prop/opt_clauses_manager.h
new file mode 100644 (file)
index 0000000..935eae1
--- /dev/null
+++ b/src/prop/opt_clauses_manager.h
@@ -0,0 +1,74 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Manager of proofs for optimized clauses
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROP__OPT_CLAUSES_MANAGER_H
+#define CVC5__PROP__OPT_CLAUSES_MANAGER_H
+
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+#include "proof/proof.h"
+
+namespace cvc5 {
+namespace prop {
+
+/**
+ * A manager for the proofs of clauses that are stored in the SAT solver in a
+ * context level below the one in which its proof is generated.
+ *
+ * Due to the above, when popping the context in which the proof was generated
+ * the respective clause, if ever needed in a subsequent (lower than generated)
+ * context, would be proofless. To prevent the issue this manager allows, for a
+ * given context, storing a proof in a given level and, when the the respective
+ * context pops, proofs of level no greater than the new one are reinserted in
+ * the proof marked to be notified.
+ */
+class OptimizedClausesManager : context::ContextNotifyObj
+{
+ public:
+  /** Constructor for OptimizedClausesManager
+   *
+   * @param context The context generating notifications
+   * @param parentProof The proof to be updated when context pops
+   * @param optProofs A mapping from context levels (note it has to be `int`) to
+   * proof nodes to be reinserted at these levels
+   */
+  OptimizedClausesManager(
+      context::Context* context,
+      CDProof* parentProof,
+      std::map<int, std::vector<std::shared_ptr<ProofNode>>>& optProofs);
+
+ private:
+  /** Event triggered by the tracked contexting popping
+   *
+   * When the context pops, every proof node associated with a level up to new
+   * level is reinsented in `d_parentProof`. Proof nodes with levels above the
+   * current one are discarded.
+   */
+  void contextNotifyPop() override;
+
+  /** The context being tracked. */
+  context::Context* d_context;
+  /** Map from levels to proof nodes. */
+  std::map<int, std::vector<std::shared_ptr<ProofNode>>>& d_optProofs;
+  /** Proof to be updated when context pops. */
+  CDProof* d_parentProof;
+};
+
+}  // namespace prop
+}  // namespace cvc5
+
+#endif /* CVC5__PROP__OPT_CLAUSES_MANAGER_H */