(proof-new) Theory engine proof generator (#4657)

This adds the proof generator used by TheoryEngine for generating proofs for explanations.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9c95163bc42a2ce409203679d2e8c29c0743db5e..1b7236d3a185f4eef41e87f5b3030a672d4655a9 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -751,6 +751,8 @@ libcvc4_add_sources(
   theory/theory.h
   theory/theory_engine.cpp
   theory/theory_engine.h
+  theory/theory_engine_proof_generator.cpp
+  theory/theory_engine_proof_generator.h
   theory/theory_id.cpp
   theory/theory_id.h
   theory/theory_model.cpp

diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp
new file mode 100644 (file)
index 0000000..2ac1236
--- /dev/null
+++ b/src/theory/theory_engine_proof_generator.cpp
@@ -0,0 +1,80 @@
+/*********************                                                        */
+/*! \file theory_engine_proof_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 theory engine proof generator
+ **/
+
+#include "theory/theory_engine_proof_generator.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm,
+                                                       context::UserContext* u)
+    : d_pnm(pnm), d_proofs(u)
+{
+}
+
+theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(
+    TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf)
+{
+  theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit, exp, this);
+  Node p = trn.getProven();
+  Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2);
+  // should not already be proven
+  NodeLazyCDProofMap::iterator it = d_proofs.find(p);
+  if (it == d_proofs.end())
+  {
+    // we will prove the fact p using the proof from lpf.
+    d_proofs.insert(p, lpf);
+  }
+  return trn;
+}
+
+std::shared_ptr<ProofNode> TheoryEngineProofGenerator::getProofFor(Node f)
+{
+  // should only ask this generator for proofs of implications
+  Assert(f.getKind() == IMPLIES && f.getNumChildren() == 2);
+  NodeLazyCDProofMap::iterator it = d_proofs.find(f);
+  if (it == d_proofs.end())
+  {
+    return nullptr;
+  }
+  std::shared_ptr<LazyCDProof> lcp = (*it).second;
+  // finalize it via scope
+  std::vector<Node> scopeAssumps;
+  if (f[0].getKind() == AND)
+  {
+    for (const Node& fc : f[0])
+    {
+      scopeAssumps.push_back(fc);
+    }
+  }
+  else
+  {
+    scopeAssumps.push_back(f[0]);
+  }
+  Node conclusion = f[1];
+
+  // get the proof for conclusion
+  std::shared_ptr<ProofNode> pfb = lcp->getProofFor(conclusion);
+  // call the scope method of proof node manager
+  std::shared_ptr<ProofNode> pf = d_pnm->mkScope(pfb, scopeAssumps);
+  return pf;
+}
+
+std::string TheoryEngineProofGenerator::identify() const
+{
+  return "TheoryEngineProofGenerator";
+}
+
+}  // namespace CVC4

diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h
new file mode 100644 (file)
index 0000000..a551e79
--- /dev/null
+++ b/src/theory/theory_engine_proof_generator.h
@@ -0,0 +1,78 @@
+/*********************                                                        */
+/*! \file theory_engine.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Andrew Reynolds
+ ** 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 theory engine proof generator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
+#define CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
+
+#include <memory>
+
+#include "context/cdhashmap.h"
+#include "context/context.h"
+#include "expr/lazy_proof.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+#include "theory/trust_node.h"
+
+namespace CVC4 {
+
+/**
+ * A simple proof generator class used by the theory engine. This class
+ * stores proofs for TheoryEngine::getExplanation.
+ *
+ * Notice that this class could be made general purpose. Its main feature is
+ * storing lazy proofs for facts in a context-dependent manner.
+ */
+class TheoryEngineProofGenerator : public ProofGenerator
+{
+  typedef context::
+      CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction>
+          NodeLazyCDProofMap;
+
+ public:
+  TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u);
+  ~TheoryEngineProofGenerator() {}
+  /**
+   * Make trust explanation. Called when lpf has a proof of lit from free
+   * assumptions in exp.
+   *
+   * This stores lpf in the map d_proofs below and returns the trust node for
+   * this propagation, which has TrustNodeKind TrustNodeKind::PROP_EXP. If this
+   * explanation already exists, then the previous explanation is taken, which
+   * also suffices for proving the implication.
+   */
+  theory::TrustNode mkTrustExplain(TNode lit,
+                                   Node exp,
+                                   std::shared_ptr<LazyCDProof> lpf);
+  /**
+   * Get proof for, which expects implications corresponding to explained
+   * propagations (=> exp lit) registered by the above method. This currently
+   * involves calling the mkScope method of ProofNodeManager internally, which
+   * returns a closed proof.
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Identify this generator (for debugging, etc..) */
+  std::string identify() const override;
+
+ private:
+  /** The proof manager, used for allocating new ProofNode objects */
+  ProofNodeManager* d_pnm;
+  /** Map from formulas to lazy CD proofs */
+  NodeLazyCDProofMap d_proofs;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */