Merge proof engine output channel into engine output channel

12 files changed, 67 insertions, 186 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6deaea082..f5be109ed 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -450,8 +450,6 @@ libcvc4_add_sources(
   theory/logic_info.cpp
   theory/logic_info.h
   theory/output_channel.h
-  theory/proof_engine_output_channel.cpp
-  theory/proof_engine_output_channel.h
   theory/quantifiers/alpha_equivalence.cpp
   theory/quantifiers/alpha_equivalence.h
   theory/quantifiers/anti_skolem.cpp
diff --git a/src/README b/src/README
index c7a940837..1de6ac991 100644
--- a/src/README
+++ b/src/README
@@ -80,7 +80,6 @@ PRs:
 (6) Split EngineOutputChannel from TheoryEngine to its own file
 (7) Add LazyCDProof and ProofGenerator
 (8) Add TrustNode
-(9) Add ProofEngineOutputChannel
 - Add EagerProofGenerator
 (10) ProofEqEngine 
 (11) TheoryEngine proof checker initialize
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index 1b8d4ceb0..0dc87e6ba 100644
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -15,7 +15,6 @@
 #include "theory/eager_proof_generator.h"
 
 #include "expr/proof_node_manager.h"
-#include "theory/proof_engine_output_channel.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index 176d08acf..b473ffc56 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -298,5 +298,26 @@ void EngineOutputChannel::handleUserAttribute(const char* attr,
   d_engine->handleUserAttribute(attr, t);
 }
 
+void EngineOutputChannel::trustedConflict(TrustNode pconf)
+{
+  Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
+  d_engine->processTrustNode(pconf, d_theory);
+  TNode conf = pconf.getNode();
+  // now, call the normal interface to conflict
+  conflict(conf);
+}
+
+LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem,
+                                                   bool removable,
+                                                   bool preprocess,
+                                                   bool sendAtoms)
+{
+  Assert(plem.getKind() == TrustNodeKind::LEMMA);
+  d_engine->processTrustNode(plem, d_theory);
+  TNode lem = plem.getNode();
+  // now, call the normal interface for lemma
+  return OutputChannel::lemma(lem, removable, preprocess, sendAtoms);
+}
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 1699795a1..1be4ec1d3 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -31,6 +31,10 @@ namespace theory {
 /**
  * An output channel for Theory that passes messages back to a TheoryEngine
  * for a given Theory.
+ * 
+ * Notice that is has interfaces trustedConflict and trustedLemma which are
+ * used for ensuring that proof generators are associated with the lemmas
+ * and conflicts sent on this output channel.
  */
 class EngineOutputChannel : public theory::OutputChannel
 {
@@ -63,6 +67,26 @@ class EngineOutputChannel : public theory::OutputChannel
 
   void handleUserAttribute(const char* attr, theory::Theory* t) override;
 
+  /**
+   * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
+   * sends conf on the output channel of this class whose proof can be generated
+   * by the generator pfg. It calls TheoryEngine::processTrustNode,
+   * which ensures that the generator pfg is associated with conf in the
+   * lazy proof owned by the theory engine of this class.
+   */
+  void trustedConflict(TrustNode pconf) override;
+  /**
+   * Let plem be the pair (Node lem, ProofGenerator * pfg).
+   * Send lem on the output channel of this class whose proof can be generated
+   * by the generator pfg. Apart from pfg, the interface for this method is
+   * the same as OutputChannel. It calls TheoryEngine::processTrustNode,
+   * which ensures that the generator pfg is associated with lem in the
+   * lazy proof owned by the theory engine of this class.
+   */
+  LemmaStatus trustedLemma(TrustNode plem,
+                           bool removable = false,
+                           bool preprocess = false,
+                           bool sendAtoms = false) override;
  protected:
   /**
    * Statistics for a particular theory.
diff --git a/src/theory/proof_engine_output_channel.cpp b/src/theory/proof_engine_output_channel.cpp
deleted file mode 100644
index 82363ff9b..000000000
--- a/src/theory/proof_engine_output_channel.cpp
+++ /dev/null
@@ -1,66 +0,0 @@
-/*********************                                                        */
-/*! \file proof_engine_output_channel.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 Evaluator class
- **
- ** The Evaluator class.
- **/
-
-#include "theory/proof_engine_output_channel.h"
-
-#include "expr/lazy_proof.h"
-
-namespace CVC4 {
-namespace theory {
-
-ProofEngineOutputChannel::ProofEngineOutputChannel(TheoryEngine* engine,
-                                                   theory::TheoryId theory,
-                                                   LazyCDProof* lpf)
-    : EngineOutputChannel(engine, theory), d_lazyPf(lpf)
-{
-}
-void ProofEngineOutputChannel::trustedConflict(TrustNode pconf)
-{
-  Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
-  d_engine->processTrustNode(pconf, d_theory);
-  TNode conf = pconf.getNode();
-  // now, call the normal interface to conflict
-  conflict(conf);
-}
-
-LemmaStatus ProofEngineOutputChannel::trustedLemma(TrustNode plem,
-                                                   bool removable,
-                                                   bool preprocess,
-                                                   bool sendAtoms)
-{
-  Assert(plem.getKind() == TrustNodeKind::LEMMA);
-  d_engine->processTrustNode(plem, d_theory);
-  TNode lem = plem.getNode();
-  // now, call the normal interface for lemma
-  return OutputChannel::lemma(lem, removable, preprocess, sendAtoms);
-}
-
-bool ProofEngineOutputChannel::addTheoryLemmaStep(Node f)
-{
-  Assert(d_lazyPf != nullptr);
-  Assert(!f.isNull());
-  std::vector<Node> children;
-  std::vector<Node> args;
-  args.push_back(f);
-  unsigned tid = static_cast<unsigned>(d_theory);
-  Node tidn = NodeManager::currentNM()->mkConst(Rational(tid));
-  args.push_back(tidn);
-  // add the step, should always succeed;
-  return d_lazyPf->addStep(f, PfRule::THEORY_LEMMA, children, args);
-}
-
-}  // namespace theory
-}  // namespace CVC4
diff --git a/src/theory/proof_engine_output_channel.h b/src/theory/proof_engine_output_channel.h
deleted file mode 100644
index 1b1beb84d..000000000
--- a/src/theory/proof_engine_output_channel.h
+++ /dev/null
@@ -1,99 +0,0 @@
-/*********************                                                        */
-/*! \file proof_engine_output_channel.h
- ** \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 proof output channel class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__PROOF_ENGINE_OUTPUT_CHANNEL_H
-#define CVC4__THEORY__PROOF_ENGINE_OUTPUT_CHANNEL_H
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "theory/engine_output_channel.h"
-
-namespace CVC4 {
-
-class LazyCDProof;
-
-namespace theory {
-
-/**
- * TODO: merge with engine output channel
- *
- * A layer on top of an output channel to ensure proofs are constructed and
- * available for conflicts and lemmas that may require proofs. It is
- * intended to be owned by TheoryEngine and passed as reference to each of
- * its Theory solvers. Its use can be summarized in two parts:
- *
- * (1) Theory objects should use the output calls to methods in this class,
- * e.g. trustedConflict(...), trustedLemma(...).
- *
- * (2) This class is responsible for adding proof steps to the provide proof
- * object that correspond to steps.
- *
- * It is implemented by requiring that calls to conflict(...) provide an
- * pointer to a proof generator object, as part of the TrustNode pair.
- *
- * In more detail, when a call to
- *   ProofOutputChannel::trustedConflict(TrustNode(conf, pfg))
- * is made
- */
-class ProofEngineOutputChannel : public EngineOutputChannel
-{
-  typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction>
-      NodeProofGenMap;
-
- public:
-  ProofEngineOutputChannel(TheoryEngine* engine,
-                           theory::TheoryId theory,
-                           LazyCDProof* lpf);
-  ~ProofEngineOutputChannel() {}
-  /**
-   * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
-   * sends conf on the output channel of this class whose proof can be generated
-   * by the generator pfg. It stores the mapping
-   *   getConflictKeyValue(conf) |-> pfg
-   * as a (lazy) step in the lazy proof object owned by this class.
-   */
-  void trustedConflict(TrustNode pconf) override;
-  /**
-   * Let plem be the pair (Node lem, ProofGenerator * pfg).
-   * Send lem on the output channel of this class whose proof can be generated
-   * by the generator pfg. Apart from pfg, the interface for this method is
-   * the same as OutputChannel. It stores the mapping
-   *   getLemmaKeyValue(lem) |-> pfg
-   * as a (lazy) step in the lazy proof object owned by this class.
-   */
-  LemmaStatus trustedLemma(TrustNode plem,
-                           bool removable = false,
-                           bool preprocess = false,
-                           bool sendAtoms = false) override;
-
- private:
-  /** Pointer to the lazy proof
-   *
-   * This object stores the mapping between formulas (conflicts or lemmas)
-   * and the proof generator provided for them.
-   */
-  LazyCDProof* d_lazyPf;
-  /**
-   * Add coarse grained THEORY_LEMMA step for formula f that is the key of
-   * a lemma or conflict being sent out on the output channel of this class.
-   */
-  bool addTheoryLemmaStep(Node f);
-};
-
-}  // namespace theory
-}  // namespace CVC4
-
-#endif /* CVC4__THEORY__PROOF_OUTPUT_CHANNEL_H */
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index ac27a5820..16afb0817 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -23,12 +23,11 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-// below, proofs are enabled in d_pfee if we are provided a lazy proof
 SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
                                          context::Context* context,
                                          context::UserContext* userContext,
                                          ProofNodeManager* pnm,
-                                         LazyCDProof* lcp)
+                      bool pfEnabled)
     : ContextNotifyObj(context),
       d_statSharedTerms("theory::shared_terms", 0),
       d_addedSharedTermsSize(context, 0),
@@ -37,11 +36,10 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
       d_registeredEqualities(context),
       d_EENotify(*this),
       d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true),
-      d_pfee(context, userContext, d_equalityEngine, pnm, lcp != nullptr),
+      d_pfee(context, userContext, d_equalityEngine, pnm, pfEnabled),
       d_theoryEngine(theoryEngine),
       d_inConflict(context, false),
-      d_conflictPolarity(),
-      d_lazyPf(lcp)
+      d_conflictPolarity()
 {
   smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
 }
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index a6e198d3c..88664544b 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -20,7 +20,6 @@
 #include <unordered_map>
 
 #include "context/cdhashset.h"
-#include "expr/lazy_proof.h"
 #include "expr/node.h"
 #include "expr/proof_node_manager.h"
 #include "theory/theory.h"
@@ -163,7 +162,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
                       context::Context* context,
                       context::UserContext* userContext,
                       ProofNodeManager* pnm,
-                      LazyCDProof* lcp);
+                      bool pfEnabled);
   ~SharedTermsDatabase();
 
   /**
@@ -255,8 +254,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
 
  protected:
-  /** Pointer to the lazy proof of TheoryEngine */
-  LazyCDProof* d_lazyPf;
   /**
    * This method gets called on backtracks from the context manager.
    */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7a1e34bef..ce9ac3da7 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -204,7 +204,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
               : nullptr),
       d_tepg(new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)),
       d_sharedTerms(
-          this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()),
+          this, context, userContext, d_pNodeManager.get(), d_lazyProof!=nullptr),
       d_masterEqualityEngine(nullptr),
       d_masterEENotify(*this),
       d_quantEngine(nullptr),
@@ -1793,6 +1793,14 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
     }
   }
 
+  // FIXME
+  std::shared_ptr<LazyCDProof> lcp;
+  if (d_lazyProof != nullptr)
+  {
+    Trace("te-proof-exp") << "TheoryEngine::lemma: process " << node << std::endl;
+    lcp.reset(new LazyCDProof(d_pNodeManager.get()));
+  }
+  
   AssertionPipeline additionalLemmas;
 
   // Run theory preprocessing, maybe
@@ -1928,6 +1936,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe));
 
     // FIXME: have ~( F ) and E => F, prove ~( E )
+    if (d_lazyProof!=nullptr)
+    {
+      
+    }
+    
 
     Node fullConflict = tnc.getNode();
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index de4b17f8c..be5206461 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -38,13 +38,13 @@
 #include "theory/atom_requests.h"
 #include "theory/decision_manager.h"
 #include "theory/interrupted.h"
-#include "theory/proof_engine_output_channel.h"
 #include "theory/rewriter.h"
 #include "theory/shared_terms_database.h"
 #include "theory/sort_inference.h"
 #include "theory/substitutions.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/theory.h"
+#include "theory/engine_output_channel.h"
 #include "theory/trust_node.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
@@ -256,10 +256,8 @@ class TheoryEngine {
    */
   context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
 
-  /**
-   * Output channels for individual theories.
-   */
-  theory::ProofEngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
+  /** Output channels for individual theories. */
+  theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
 
   /**
    * Are we in conflict.
@@ -420,7 +418,7 @@ class TheoryEngine {
   {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
     d_theoryOut[theoryId] =
-        new theory::ProofEngineOutputChannel(this, theoryId, d_lazyProof.get());
+        new theory::EngineOutputChannel(this, theoryId);
     d_theoryTable[theoryId] = new TheoryClass(d_context,
                                               d_userContext,
                                               *d_theoryOut[theoryId],
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index 62213aade..8cb2a1f95 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -15,7 +15,6 @@
 #include "theory/trust_node.h"
 
 #include "expr/proof_generator.h"
-#include "theory/proof_engine_output_channel.h"
 
 namespace CVC4 {
 namespace theory {