[proofs] [sat] Handle resolution proofs for optimized clauses in incremental (#8389)

The SAT solver may associate, to the result of a resolution, a lower assertion
level than the current one. To be able to produce proofs to such clauses, we
extend the SAT proof manager to track which resolution results were
optimized. Then, when the SAT solver pops, the manager is notified and stores
the proofs for these optimized clauses, so that they can be reinserted when the
user context is popped. The latter is handled by the SAT proof manager's
OptClauseManager attribute.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 75e1d831f0a8eca16841d5df8415e6ecc62b5839..1294b9d330d5e499dd2069f39ca18a6f4a30dca5 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -213,8 +213,7 @@ Solver::Solver(Env& env,
 {
   if (pnm)
   {
-    d_pfManager.reset(
-        new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
+    d_pfManager.reset(new SatProofManager(env, this, proxy->getCnfStream()));
   }
 
   // Create the constant variables

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 582aa5253be1b1b60a728a7cddd0df7345c6ae04..d31b1273a7a6f98b6c4878652bbbda235b627b74 100644 (file)
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -24,17 +24,18 @@
 namespace cvc5 {
 namespace prop {
 
-SatProofManager::SatProofManager(Minisat::Solver* solver,
-                                 CnfStream* cnfStream,
-                                 context::UserContext* userContext,
-                                 ProofNodeManager* pnm)
-    : d_solver(solver),
+SatProofManager::SatProofManager(Env& env,
+                                 Minisat::Solver* solver,
+                                 CnfStream* cnfStream)
+    : EnvObj(env),
+      d_solver(solver),
       d_cnfStream(cnfStream),
-      d_pnm(pnm),
-      d_resChains(pnm, true, userContext),
-      d_resChainPg(userContext, pnm),
-      d_assumptions(userContext),
-      d_conflictLit(undefSatVariable)
+      d_resChains(d_env.getProofNodeManager(), true, userContext()),
+      d_resChainPg(userContext(), d_env.getProofNodeManager()),
+      d_assumptions(userContext()),
+      d_conflictLit(undefSatVariable),
+      d_optResLevels(userContext()),
+      d_optResManager(userContext(), &d_resChains, d_optResProofs)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -118,13 +119,15 @@ void SatProofManager::addResolutionStep(const Minisat::Clause& clause,
                        << satLit.isNegated() << "} [" << ~satLit << "] ";
     printClause(clause);
     Trace("sat-proof") << "\nSatProofManager::addResolutionStep:\t"
-                       << clauseNode << "\n";
+                       << clauseNode << " - lvl " << clause.level() + 1 << "\n";
   }
 }
 
 void SatProofManager::endResChain(Minisat::Lit lit)
 {
   SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
+  Trace("sat-proof") << "SatProofManager::endResChain: curr user level: "
+                     << userContext()->getLevel() << "\n";
   Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "
                      << satLit;
   endResChain(d_cnfStream->getNode(satLit), {satLit});
@@ -134,6 +137,8 @@ void SatProofManager::endResChain(const Minisat::Clause& clause)
 {
   if (TraceIsOn("sat-proof"))
   {
+    Trace("sat-proof") << "SatProofManager::endResChain: curr user level: "
+                       << userContext()->getLevel() << "\n";
     Trace("sat-proof") << "SatProofManager::endResChain: chain_res for ";
     printClause(clause);
   }
@@ -142,7 +147,17 @@ void SatProofManager::endResChain(const Minisat::Clause& clause)
   {
     clauseLits.insert(MinisatSatSolver::toSatLiteral(clause[i]));
   }
-  endResChain(getClauseNode(clause), clauseLits);
+  Node conclusion = getClauseNode(clause);
+  int clauseLevel = clause.level() + 1;
+  if (clauseLevel < userContext()->getLevel())
+  {
+    Assert(!d_optResLevels.count(conclusion));
+    d_optResLevels[conclusion] = clauseLevel;
+    Trace("sat-proof") << "SatProofManager::endResChain: ..clause's lvl "
+                       << clause.level() + 1 << " below curr user level "
+                       << userContext()->getLevel() << "\n";
+  }
+  endResChain(conclusion, clauseLits);
 }
 
 void SatProofManager::endResChain(Node conclusion,
@@ -756,7 +771,7 @@ std::shared_ptr<ProofNode> SatProofManager::getProof()
   std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false);
   if (!pfn)
   {
-    pfn = d_pnm->mkAssume(d_false);
+    pfn = d_env.getProofNodeManager()->mkAssume(d_false);
   }
   return pfn;
 }
@@ -781,5 +796,22 @@ void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps)
   }
 }
 
+void SatProofManager::notifyPop()
+{
+  for (context::CDHashMap<Node, int>::const_iterator it =
+           d_optResLevels.begin();
+       it != d_optResLevels.end();
+       ++it)
+  {
+    // Save into map the proof of the resolution chain. We copy to prevent the
+    // proof node saved to be restored to suffering unintended updates. This is
+    // *necessary*.
+    std::shared_ptr<ProofNode> clauseResPf =
+        d_env.getProofNodeManager()->clone(d_resChains.getProofFor(it->first));
+    Assert(clauseResPf && clauseResPf->getRule() != PfRule::ASSUME);
+    d_optResProofs[it->second].push_back(clauseResPf);
+  }
+}
+
 }  // namespace prop
 }  // namespace cvc5

diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index 98d125591afb265d89a891af7dd49cf60da2bb28..d62905792f367685aea128a4f3c4b11644b34de7 100644 (file)
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -18,12 +18,15 @@
 #ifndef CVC5__SAT_PROOF_MANAGER_H
 #define CVC5__SAT_PROOF_MANAGER_H
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "proof/buffered_proof_generator.h"
 #include "proof/lazy_proof_chain.h"
 #include "prop/minisat/core/SolverTypes.h"
+#include "prop/opt_clauses_manager.h"
 #include "prop/sat_solver_types.h"
+#include "smt/env_obj.h"
 
 namespace Minisat {
 class Solver;
@@ -268,13 +271,10 @@ class CnfStream;
  * getProof
  *
  */
-class SatProofManager
+class SatProofManager : protected EnvObj
 {
  public:
-  SatProofManager(Minisat::Solver* solver,
-                  CnfStream* cnfStream,
-                  context::UserContext* userContext,
-                  ProofNodeManager* pnm);
+  SatProofManager(Env& env, Minisat::Solver* solver, CnfStream* cnfStream);
 
   /** Marks the start of a resolution chain.
    *
@@ -361,6 +361,9 @@ class SatProofManager
   /** Register a set clause inputs. */
   void registerSatAssumptions(const std::vector<Node>& assumps);
 
+  /** Notify this proof manager that the SAT solver has user-context popped. */
+  void notifyPop();
+
  private:
   /** Ends resolution chain concluding clause
    *
@@ -582,6 +585,22 @@ class SatProofManager
   Node getClauseNode(const Minisat::Clause& clause);
   /** Prints clause, as a sequence of literals, in the "sat-proof" trace. */
   void printClause(const Minisat::Clause& clause);
+
+  /** The user context */
+  context::UserContext* d_userContext;
+
+  /** User-context dependent map from resolution conclusions to their assertion
+      level. */
+  context::CDHashMap<Node, int> d_optResLevels;
+  /** Maps assertion level to proof nodes.
+   *
+   * This map is used by d_optResManager to update the internal proof of this
+   * manager when the context pops.
+   */
+  std::map<int, std::vector<std::shared_ptr<ProofNode>>> d_optResProofs;
+  /** Manager for optimized resolution conclusions inserted at assertion levels
+   * below the current user level. */
+  OptimizedClausesManager d_optResManager;
 }; /* class SatProofManager */
 
 }  // namespace prop