[proof-new] Adds a proof manager for the SAT solver (#5140)

Tracks the refutation proof built by Minisat. See the header for extensive explanations.

This commit also adds a few dependencies for the SAT proof manager to work (making it a friend of the SAT solver, getting the cnf stream from theory proxy, having lazy cdproof chain give all the links).

2 files changed, 18 insertions, 0 deletions

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index a01d541eb..95704d82a 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -29,6 +29,20 @@ LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
 
 LazyCDProofChain::~LazyCDProofChain() {}
 
+const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks()
+    const
+{
+  std::map<Node, std::shared_ptr<ProofNode>> links;
+  for (const std::pair<const Node, ProofGenerator*>& link : d_gens)
+  {
+    Assert(link.second);
+    std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first);
+    Assert(pfn);
+    links[link.first] = pfn;
+  }
+  return links;
+}
+
 std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
 {
   Trace("lazy-cdproofchain")
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 7fa49bccc..a58cc5c7d 100644
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -119,6 +119,10 @@ class LazyCDProofChain : public ProofGenerator
   /** identify */
   std::string identify() const override;
 
+  /** Retrieve, for each fact in d_gens, it mapped to the proof node generated
+   * by its generator in d_gens.  */
+  const std::map<Node, std::shared_ptr<ProofNode>> getLinks() const;
+
  private:
   /** The proof manager, used for allocating new ProofNode objects */
   ProofNodeManager* d_manager;