(proof-new) Add TrustNode interfaces to OutputChannel (#4643)

diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index 2a86c43a4162f1a827b65c32a0e6355ae4a6c3b9..d83d2ba6267ce63bfbe8526d09395c5645cfa4f3 100644 (file)
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -85,8 +85,9 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma,
 
   PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); });
 
+  TrustNode tlem = TrustNode::mkTrustLemma(lemma);
   theory::LemmaStatus result =
-      d_engine->lemma(lemma,
+      d_engine->lemma(tlem.getNode(),
                       rule,
                       false,
                       removable,
@@ -234,8 +235,9 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
 
   Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
                        << std::endl;
-  theory::LemmaStatus result =
-      d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory);
+  TrustNode tlem = TrustNode::mkTrustLemma(lemma);
+  theory::LemmaStatus result = d_engine->lemma(
+      tlem.getNode(), RULE_SPLIT, false, removable, false, d_theory);
   return result;
 }
 
@@ -257,7 +259,8 @@ void EngineOutputChannel::conflict(TNode conflictNode,
   Assert(!proof);  // Theory shouldn't be producing proofs yet
   ++d_statistics.conflicts;
   d_engine->d_outputChannelUsed = true;
-  d_engine->conflict(conflictNode, d_theory);
+  TrustNode tConf = TrustNode::mkTrustConflict(conflictNode);
+  d_engine->conflict(tConf.getNode(), d_theory);
 }
 
 void EngineOutputChannel::demandRestart()
@@ -298,5 +301,41 @@ void EngineOutputChannel::handleUserAttribute(const char* attr,
   d_engine->handleUserAttribute(attr, t);
 }
 
+void EngineOutputChannel::trustedConflict(TrustNode pconf)
+{
+  Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
+  Trace("theory::conflict")
+      << "EngineOutputChannel<" << d_theory << ">::conflict(" << pconf.getNode()
+      << ")" << std::endl;
+  if (pconf.getGenerator() != nullptr)
+  {
+    ++d_statistics.trustedConflicts;
+  }
+  ++d_statistics.conflicts;
+  d_engine->d_outputChannelUsed = true;
+  d_engine->conflict(pconf.getNode(), d_theory);
+}
+
+LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem,
+                                              bool removable,
+                                              bool preprocess,
+                                              bool sendAtoms)
+{
+  Assert(plem.getKind() == TrustNodeKind::LEMMA);
+  if (plem.getGenerator() != nullptr)
+  {
+    ++d_statistics.trustedLemmas;
+  }
+  ++d_statistics.lemmas;
+  d_engine->d_outputChannelUsed = true;
+  // now, call the normal interface for lemma
+  return d_engine->lemma(plem.getNode(),
+                         RULE_INVALID,
+                         false,
+                         removable,
+                         preprocess,
+                         sendAtoms ? d_theory : theory::THEORY_LAST);
+}
+
 }  // namespace theory
 }  // namespace CVC4

diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 992ef064b1f67db72a71a31ba69a4ed6bd5cd879..d7b26928db281f1c6ec30a3ffd28e6b92af6f100 100644 (file)
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -67,6 +67,24 @@ 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. Apart from pfg, the interface for this method is
+   * the same as calling OutputChannel::lemma on conf.
+   */
+  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 calling OutputChannel::lemma on lem.
+   */
+  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/output_channel.h b/src/theory/output_channel.h
index 215ec8e0a1276f3b3d49e3317ac5b79d5bb1a2ce..ff13d1b6b2af1bb3eec67ba06b5bb6d2bbbcbe0f 100644 (file)
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -21,9 +21,11 @@
 
 #include <memory>
 
+#include "expr/proof_node.h"
 #include "proof/proof_manager.h"
 #include "smt/logic_exception.h"
 #include "theory/interrupted.h"
+#include "theory/trust_node.h"
 #include "util/proof.h"
 #include "util/resource_manager.h"
 
@@ -188,6 +190,33 @@ class OutputChannel {
    */
   virtual void demandRestart() {}
 
+  //---------------------------- new proof
+  /**
+   * 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. Apart from pfg, the interface for this method is
+   * the same as OutputChannel.
+   */
+  virtual void trustedConflict(TrustNode pconf)
+  {
+    Unreachable() << "OutputChannel::trustedConflict: no implementation"
+                  << std::endl;
+  }
+  /**
+   * 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.
+   */
+  virtual LemmaStatus trustedLemma(TrustNode lem,
+                                   bool removable = false,
+                                   bool preprocess = false,
+                                   bool sendAtoms = false)
+  {
+    Unreachable() << "OutputChannel::trustedLemma: no implementation"
+                  << std::endl;
+  }
+  //---------------------------- end new proof
 }; /* class OutputChannel */
 
 }  // namespace theory