[proof-new] Updating theory proxy to new proof infrastructure (#5653)

3 files changed, 35 insertions, 12 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 8c1e452e7..e5efcbf8f 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -78,6 +78,7 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_satSolver(NULL),
       d_registrar(NULL),
       d_cnfStream(NULL),
+      d_pfCnfStream(nullptr),
       d_interrupted(false),
       d_resourceManager(rm),
       d_outMgr(outMgr)
@@ -399,6 +400,8 @@ bool PropEngine::properExplanation(TNode node, TNode expl) const {
   return true;
 }
 
+ProofCnfStream* PropEngine::getProofCnfStream() { return d_pfCnfStream.get(); }
+
 std::shared_ptr<ProofNode> PropEngine::getProof()
 {
   // TODO (proj #37) implement this
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 061324947..b36b9d22a 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -28,6 +28,7 @@
 #include "options/options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "proof/proof_manager.h"
+#include "prop/proof_cnf_stream.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
 #include "util/unsafe_interrupt_exception.h"
@@ -235,6 +236,9 @@ class PropEngine
    */
   bool properExplanation(TNode node, TNode expl) const;
 
+  /** Retrieve this modules proof CNF stream. */
+  ProofCnfStream* getProofCnfStream();
+
   /**
    * Return the prop engine proof. This should be called only when proofs are
    * enabled. Returns a proof of false whose free assumptions are the
@@ -274,6 +278,8 @@ class PropEngine
 
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
+  /** Proof-producing CNF converter */
+  std::unique_ptr<ProofCnfStream> d_pfCnfStream;
 
   /** Whether we were just interrupted (or not) */
   bool d_interrupted;
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index d0d593f8a..1b9e78d80 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -75,26 +75,40 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
 
-  theory::TrustNode texp = d_theoryEngine->getExplanation(lNode);
-  Node theoryExplanation = texp.getNode();
-
+  theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
+  Node theoryExplanation = tte.getNode();
+  if (CVC4::options::proofNew())
+  {
+    d_propEngine->getProofCnfStream()->convertPropagation(tte);
+  }
   if (options::unsatCores())
   {
     ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
   }
-
   Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
-  if (theoryExplanation.getKind() == kind::AND) {
-    Node::const_iterator it = theoryExplanation.begin();
-    Node::const_iterator it_end = theoryExplanation.end();
-    explanation.push_back(l);
-    for (; it != it_end; ++ it) {
-      explanation.push_back(~d_cnfStream->getLiteral(*it));
+  explanation.push_back(l);
+  if (theoryExplanation.getKind() == kind::AND)
+  {
+    for (const Node& n : theoryExplanation)
+    {
+      explanation.push_back(~d_cnfStream->getLiteral(n));
     }
-  } else {
-    explanation.push_back(l);
+  }
+  else
+  {
     explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
   }
+  if (Trace.isOn("sat-proof"))
+  {
+    std::stringstream ss;
+    ss << "TheoryProxy::explainPropagation: clause for lit is ";
+    for (unsigned i = 0, size = explanation.size(); i < size; ++i)
+    {
+      ss << explanation[i] << " [" << d_cnfStream->getNode(explanation[i])
+         << "] ";
+    }
+    Trace("sat-proof") << ss.str() << "\n";
+  }
 }
 
 void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {