[proof-new] Optimizing sat proof (#6324)

For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.

2 files changed, 10 insertions, 11 deletions

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index da9354c2f..0d075de45 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -35,6 +35,7 @@ SatProofManager::SatProofManager(Minisat::Solver* solver,
       d_assumptions(userContext),
       d_conflictLit(undefSatVariable)
 {
+  d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
@@ -169,7 +170,6 @@ void SatProofManager::endResChain(Node conclusion,
   }
   d_redundantLits.clear();
   // build resolution chain
-  NodeManager* nm = NodeManager::currentNM();
   // the conclusion is stored already in the arguments because of the
   // possibility of reordering
   std::vector<Node> children, args{conclusion};
@@ -212,7 +212,7 @@ void SatProofManager::endResChain(Node conclusion,
     Trace("sat-proof") << " : ";
     if (i > 0)
     {
-      args.push_back(nm->mkConst(posFirst));
+      args.push_back(posFirst ? d_true : d_false);
       args.push_back(pivot);
       Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] ";
     }
@@ -249,7 +249,7 @@ void SatProofManager::endResChain(Node conclusion,
   // step, which bypasses these. Note that we could generate a chain resolution
   // rule here by explicitly computing the detailed steps, but leave this for
   // post-processing.
-  ProofStep ps(PfRule::MACRO_RESOLUTION, children, args);
+  ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
   d_resChainPg.addStep(conclusion, ps);
   // the premises of this resolution may not have been justified yet, so we do
   // not pass assumptions to check closedness
@@ -369,7 +369,6 @@ void SatProofManager::explainLit(
   // SAT solver, we directly get the literals we need to explain so we no
   // longer depend on the reference to reason
   std::vector<Node> toExplain{children.back().begin(), children.back().end()};
-  NodeManager* nm = NodeManager::currentNM();
   Trace("sat-proof") << push;
   for (unsigned i = 0; i < size; ++i)
   {
@@ -397,7 +396,7 @@ void SatProofManager::explainLit(
     // note this is the opposite of what is done in addResolutionStep. This is
     // because here the clause, which contains the literal being analyzed, is
     // the first clause rather than the second
-    args.push_back(nm->mkConst(!negated));
+    args.push_back(!negated ? d_true : d_false);
     args.push_back(negated ? currLitNode[0] : currLitNode);
     // add child premises and the child itself
     premises.insert(childPremises.begin(), childPremises.end());
@@ -429,7 +428,7 @@ void SatProofManager::explainLit(
   Trace("sat-proof") << pop;
   // create step
   args.insert(args.begin(), litNode);
-  ProofStep ps(PfRule::MACRO_RESOLUTION, children, args);
+  ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
   d_resChainPg.addStep(litNode, ps);
   // the premises in the limit of the justification may correspond to other
   // links in the chain which have, themselves, literals yet to be justified. So
@@ -490,7 +489,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
       // get resolution
       Node cur = link.first;
       std::shared_ptr<ProofNode> pfn = link.second;
-      while (pfn->getRule() != PfRule::MACRO_RESOLUTION)
+      while (pfn->getRule() != PfRule::MACRO_RESOLUTION_TRUST)
       {
         Assert(pfn->getChildren().size() == 1
                && pfn->getChildren()[0]->getRule() == PfRule::ASSUME)
@@ -539,7 +538,6 @@ void SatProofManager::finalizeProof(Node inConflictNode,
   // arguments for the resolution step to conclude false.
   std::vector<Node> children{inConflictNode}, args;
   std::unordered_set<TNode, TNodeHashFunction> premises;
-  NodeManager* nm = NodeManager::currentNM();
   for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
   {
     Assert(d_cnfStream->getNodeCache().find(inConflict[i])
@@ -555,7 +553,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
     // note this is the opposite of what is done in addResolutionStep. This is
     // because here the clause, which contains the literal being analyzed, is
     // the first clause rather than the second
-    args.push_back(nm->mkConst(!negated));
+    args.push_back(!negated ? d_true : d_false);
     args.push_back(negated ? litNode[0] : litNode);
     // add child premises and the child itself
     premises.insert(childPremises.begin(), childPremises.end());
@@ -578,7 +576,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
   }
   // create step
   args.insert(args.begin(), d_false);
-  ProofStep ps(PfRule::MACRO_RESOLUTION, children, args);
+  ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
   d_resChainPg.addStep(d_false, ps);
   // not yet ready to check closedness because maybe only now we will justify
   // literals used in resolutions
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index 4d45ce3b7..6407939c7 100644
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -561,7 +561,8 @@ class SatProofManager
   /** The proof generator for resolution chains */
   BufferedProofGenerator d_resChainPg;
 
-  /** The false node */
+  /** The true/false nodes */
+  Node d_true;
   Node d_false;
 
   /** All clauses added to the SAT solver, kept in a context-dependent manner.