[proof-new] Make prop engine proof producing (#5667)

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index fee73babbe785ae9398ec51572856919f4429170..a8a92096cae21d27cac2a542c148c16889664a59 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -31,6 +31,7 @@
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 #include "prop/cnf_stream.h"
+#include "prop/minisat/minisat.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "prop/theory_proxy.h"
@@ -40,9 +41,6 @@
 #include "util/resource_manager.h"
 #include "util/result.h"
 
-using namespace std;
-using namespace CVC4::context;
-
 namespace CVC4 {
 namespace prop {
 
@@ -67,25 +65,25 @@ public:
 };
 
 PropEngine::PropEngine(TheoryEngine* te,
-                       Context* satContext,
-                       UserContext* userContext,
+                       context::Context* satContext,
+                       context::UserContext* userContext,
                        ResourceManager* rm,
                        OutputManager& outMgr,
                        ProofNodeManager* pnm)
     : d_inCheckSat(false),
       d_theoryEngine(te),
       d_context(satContext),
-      d_theoryProxy(NULL),
-      d_satSolver(NULL),
-      d_registrar(NULL),
-      d_cnfStream(NULL),
+      d_theoryProxy(nullptr),
+      d_satSolver(nullptr),
+      d_registrar(nullptr),
+      d_pnm(pnm),
+      d_cnfStream(nullptr),
       d_pfCnfStream(nullptr),
       d_ppm(nullptr),
       d_interrupted(false),
       d_resourceManager(rm),
       d_outMgr(outMgr)
 {
-
   Debug("prop") << "Constructing the PropEngine" << endl;
 
   d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
@@ -96,13 +94,22 @@ PropEngine::PropEngine(TheoryEngine* te,
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::CnfStream(
       d_satSolver, d_registrar, userContext, &d_outMgr, rm, true);
-
   d_theoryProxy = new TheoryProxy(
       this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
   d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm);
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
+  if (pnm)
+  {
+    d_pfCnfStream.reset(new ProofCnfStream(
+        userContext,
+        *d_cnfStream,
+        static_cast<MinisatSatSolver*>(d_satSolver)->getProofManager(),
+        pnm));
+    d_ppm.reset(
+        new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
+  }
   if (options::unsatCores())
   {
     ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
@@ -113,6 +120,16 @@ void PropEngine::finishInit()
 {
   NodeManager* nm = NodeManager::currentNM();
   d_cnfStream->convertAndAssert(nm->mkConst(true), false, false);
+  // this is necessary because if True is later asserted to the prop engine the
+  // CNF stream will ignore it since the SAT solver already had it registered,
+  // thus not having True as an assumption for the SAT proof. To solve this
+  // issue we track it directly here
+  if (isProofEnabled())
+  {
+    static_cast<MinisatSatSolver*>(d_satSolver)
+        ->getProofManager()
+        ->registerSatAssumptions({nm->mkConst(true)});
+  }
   d_cnfStream->convertAndAssert(nm->mkConst(false).notNode(), false, false);
 }
 
@@ -152,7 +169,16 @@ void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as non-removable
-  d_cnfStream->convertAndAssert(node, false, false, true);
+  if (isProofEnabled())
+  {
+    d_pfCnfStream->convertAndAssert(node, false, false, nullptr);
+    // register in proof manager
+    d_ppm->registerAssertion(node);
+  }
+  else
+  {
+    d_cnfStream->convertAndAssert(node, false, false, true);
+  }
 }
 
 void PropEngine::assertLemma(theory::TrustNode trn, bool removable)
@@ -160,9 +186,17 @@ void PropEngine::assertLemma(theory::TrustNode trn, bool removable)
   Node node = trn.getNode();
   bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
-
   // Assert as (possibly) removable
-  d_cnfStream->convertAndAssert(node, removable, negated);
+  if (isProofEnabled())
+  {
+    Assert(trn.getGenerator());
+    d_pfCnfStream->convertAndAssert(
+        node, negated, removable, trn.getGenerator());
+  }
+  else
+  {
+    d_cnfStream->convertAndAssert(node, removable, negated);
+  }
 }
 
 void PropEngine::assertLemmas(theory::TrustNode lem,
@@ -269,61 +303,75 @@ Result PropEngine::checkSat() {
   return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
 }
 
-Node PropEngine::getValue(TNode node) const {
+Node PropEngine::getValue(TNode node) const
+{
   Assert(node.getType().isBoolean());
   Assert(d_cnfStream->hasLiteral(node));
 
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
   SatValue v = d_satSolver->value(lit);
-  if(v == SAT_VALUE_TRUE) {
+  if (v == SAT_VALUE_TRUE)
+  {
     return NodeManager::currentNM()->mkConst(true);
-  } else if(v == SAT_VALUE_FALSE) {
+  }
+  else if (v == SAT_VALUE_FALSE)
+  {
     return NodeManager::currentNM()->mkConst(false);
-  } else {
+  }
+  else
+  {
     Assert(v == SAT_VALUE_UNKNOWN);
     return Node::null();
   }
 }
 
-bool PropEngine::isSatLiteral(TNode node) const {
+bool PropEngine::isSatLiteral(TNode node) const
+{
   return d_cnfStream->hasLiteral(node);
 }
 
-bool PropEngine::hasValue(TNode node, bool& value) const {
+bool PropEngine::hasValue(TNode node, bool& value) const
+{
   Assert(node.getType().isBoolean());
   Assert(d_cnfStream->hasLiteral(node)) << node;
 
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
   SatValue v = d_satSolver->value(lit);
-  if(v == SAT_VALUE_TRUE) {
+  if (v == SAT_VALUE_TRUE)
+  {
     value = true;
     return true;
-  } else if(v == SAT_VALUE_FALSE) {
+  }
+  else if (v == SAT_VALUE_FALSE)
+  {
     value = false;
     return true;
-  } else {
+  }
+  else
+  {
     Assert(v == SAT_VALUE_UNKNOWN);
     return false;
   }
 }
 
-void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const {
+void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const
+{
   d_cnfStream->getBooleanVariables(outputVariables);
 }
 
-void PropEngine::ensureLiteral(TNode n) {
-  d_cnfStream->ensureLiteral(n);
-}
+void PropEngine::ensureLiteral(TNode n) { d_cnfStream->ensureLiteral(n); }
 
-void PropEngine::push() {
+void PropEngine::push()
+{
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   d_satSolver->push();
   Debug("prop") << "push()" << endl;
 }
 
-void PropEngine::pop() {
+void PropEngine::pop()
+{
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   d_satSolver->pop();
   Debug("prop") << "pop()" << endl;
@@ -335,16 +383,16 @@ void PropEngine::resetTrail()
   Debug("prop") << "resetTrail()" << endl;
 }
 
-unsigned PropEngine::getAssertionLevel() const {
+unsigned PropEngine::getAssertionLevel() const
+{
   return d_satSolver->getAssertionLevel();
 }
 
-bool PropEngine::isRunning() const {
-  return d_inCheckSat;
-}
+bool PropEngine::isRunning() const { return d_inCheckSat; }
 void PropEngine::interrupt()
 {
-  if(! d_inCheckSat) {
+  if (!d_inCheckSat)
+  {
     return;
   }
 
@@ -358,43 +406,60 @@ void PropEngine::spendResource(ResourceManager::Resource r)
   d_resourceManager->spendResource(r);
 }
 
-bool PropEngine::properExplanation(TNode node, TNode expl) const {
-  if(! d_cnfStream->hasLiteral(node)) {
-    Trace("properExplanation") << "properExplanation(): Failing because node "
-                               << "being explained doesn't have a SAT literal ?!" << std::endl
-                               << "properExplanation(): The node is: " << node << std::endl;
+bool PropEngine::properExplanation(TNode node, TNode expl) const
+{
+  if (!d_cnfStream->hasLiteral(node))
+  {
+    Trace("properExplanation")
+        << "properExplanation(): Failing because node "
+        << "being explained doesn't have a SAT literal ?!" << std::endl
+        << "properExplanation(): The node is: " << node << std::endl;
     return false;
   }
 
   SatLiteral nodeLit = d_cnfStream->getLiteral(node);
 
-  for(TNode::kinded_iterator i = expl.begin(kind::AND),
-        i_end = expl.end(kind::AND);
-      i != i_end;
-      ++i) {
-    if(! d_cnfStream->hasLiteral(*i)) {
-      Trace("properExplanation") << "properExplanation(): Failing because one of explanation "
-                                 << "nodes doesn't have a SAT literal" << std::endl
-                                 << "properExplanation(): The explanation node is: " << *i << std::endl;
+  for (TNode::kinded_iterator i = expl.begin(kind::AND),
+                              i_end = expl.end(kind::AND);
+       i != i_end;
+       ++i)
+  {
+    if (!d_cnfStream->hasLiteral(*i))
+    {
+      Trace("properExplanation")
+          << "properExplanation(): Failing because one of explanation "
+          << "nodes doesn't have a SAT literal" << std::endl
+          << "properExplanation(): The explanation node is: " << *i
+          << std::endl;
       return false;
     }
 
     SatLiteral iLit = d_cnfStream->getLiteral(*i);
 
-    if(iLit == nodeLit) {
-      Trace("properExplanation") << "properExplanation(): Failing because the node" << std::endl
-                                 << "properExplanation(): " << node << std::endl
-                                 << "properExplanation(): cannot be made to explain itself!" << std::endl;
+    if (iLit == nodeLit)
+    {
+      Trace("properExplanation")
+          << "properExplanation(): Failing because the node" << std::endl
+          << "properExplanation(): " << node << std::endl
+          << "properExplanation(): cannot be made to explain itself!"
+          << std::endl;
       return false;
     }
 
-    if(! d_satSolver->properExplanation(nodeLit, iLit)) {
-      Trace("properExplanation") << "properExplanation(): SAT solver told us that node" << std::endl
-                                 << "properExplanation(): " << *i << std::endl
-                                 << "properExplanation(): is not part of a proper explanation node for" << std::endl
-                                 << "properExplanation(): " << node << std::endl
-                                 << "properExplanation(): Perhaps it one of the two isn't assigned or the explanation" << std::endl
-                                 << "properExplanation(): node wasn't propagated before the node being explained" << std::endl;
+    if (!d_satSolver->properExplanation(nodeLit, iLit))
+    {
+      Trace("properExplanation")
+          << "properExplanation(): SAT solver told us that node" << std::endl
+          << "properExplanation(): " << *i << std::endl
+          << "properExplanation(): is not part of a proper explanation node for"
+          << std::endl
+          << "properExplanation(): " << node << std::endl
+          << "properExplanation(): Perhaps it one of the two isn't assigned or "
+             "the explanation"
+          << std::endl
+          << "properExplanation(): node wasn't propagated before the node "
+             "being explained"
+          << std::endl;
       return false;
     }
   }
@@ -402,13 +467,27 @@ bool PropEngine::properExplanation(TNode node, TNode expl) const {
   return true;
 }
 
+void PropEngine::checkProof(context::CDList<Node>* assertions)
+{
+  if (!d_pnm)
+  {
+    return;
+  }
+  return d_ppm->checkProof(assertions);
+}
+
 ProofCnfStream* PropEngine::getProofCnfStream() { return d_pfCnfStream.get(); }
 
 std::shared_ptr<ProofNode> PropEngine::getProof()
 {
-  // TODO (proj #37) implement this
-  return nullptr;
+  if (!d_pnm)
+  {
+    return nullptr;
+  }
+  return d_ppm->getProof();
 }
 
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; }
+
+}  // namespace prop
+}  // namespace CVC4

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index b311558ab51a1687bab82e43b96921b64d26dd96..55a42c2a7100ba682684f57ab5828e964b63fee4 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -256,6 +256,8 @@ class PropEngine
    */
   std::shared_ptr<ProofNode> getProof();
 
+  /** Is proof enabled? */
+  bool isProofEnabled() const;
  private:
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();