[proofs] Simplifying and adding new utils to SAT proof manager and Proof Cnf Stream...

These will be necessary for upcoming changes to the SAT proof manager and Proof Cnf Stream to handle incremental proofs when optimizing the level of SAT clauses.

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index b5542ab357c241253fb13d5b88867b9e173c0163..8aaa68b9ab06e816660bad868fb4701f2b69f8b8 100644 (file)
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -20,8 +20,6 @@
 #include "theory/builtin/proof_checker.h"
 #include "util/rational.h"
 
-using namespace cvc5::kind;
-
 namespace cvc5 {
 namespace prop {
 
@@ -58,7 +56,7 @@ bool ProofCnfStream::hasProofFor(Node f)
 
 std::string ProofCnfStream::identify() const { return "ProofCnfStream"; }
 
-void ProofCnfStream::normalizeAndRegister(TNode clauseNode)
+Node ProofCnfStream::normalizeAndRegister(TNode clauseNode)
 {
   Node normClauseNode = d_psb.factorReorderElimDoubleNeg(clauseNode);
   if (Trace.isOn("cnf") && normClauseNode != clauseNode)
@@ -69,6 +67,7 @@ void ProofCnfStream::normalizeAndRegister(TNode clauseNode)
                  << pop;
   }
   d_satPM->registerSatAssumptions({normClauseNode});
+  return normClauseNode;
 }
 
 void ProofCnfStream::convertAndAssert(TNode node,
@@ -104,7 +103,8 @@ void ProofCnfStream::convertAndAssert(TNode node,
 void ProofCnfStream::convertAndAssert(TNode node, bool negated)
 {
   Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
-               << ", negated = " << (negated ? "true" : "false") << ")\n";
+               << ", negated = " << (negated ? "true" : "false") << ")\n"
+               << push;
   switch (node.getKind())
   {
     case kind::AND: convertAndAssertAnd(node, negated); break;
@@ -159,12 +159,14 @@ void ProofCnfStream::convertAndAssert(TNode node, bool negated)
       }
     }
   }
+  Trace("cnf") << pop;
 }
 
 void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated)
 {
   Trace("cnf") << "ProofCnfStream::convertAndAssertAnd(" << node
-               << ", negated = " << (negated ? "true" : "false") << ")\n";
+               << ", negated = " << (negated ? "true" : "false") << ")\n"
+               << push;
   Assert(node.getKind() == kind::AND);
   if (!negated)
   {
@@ -205,12 +207,14 @@ void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated)
       normalizeAndRegister(clauseNode);
     }
   }
+  Trace("cnf") << pop;
 }
 
 void ProofCnfStream::convertAndAssertOr(TNode node, bool negated)
 {
   Trace("cnf") << "ProofCnfStream::convertAndAssertOr(" << node
-               << ", negated = " << (negated ? "true" : "false") << ")\n";
+               << ", negated = " << (negated ? "true" : "false") << ")\n"
+               << push;
   Assert(node.getKind() == kind::OR);
   if (!negated)
   {
@@ -240,12 +244,14 @@ void ProofCnfStream::convertAndAssertOr(TNode node, bool negated)
       convertAndAssert(node[i], true);
     }
   }
+  Trace("cnf") << pop;
 }
 
 void ProofCnfStream::convertAndAssertXor(TNode node, bool negated)
 {
   Trace("cnf") << "ProofCnfStream::convertAndAssertXor(" << node
-               << ", negated = " << (negated ? "true" : "false") << ")\n";
+               << ", negated = " << (negated ? "true" : "false") << ")\n"
+               << push;
   if (!negated)
   {
     // p XOR q
@@ -317,12 +323,14 @@ void ProofCnfStream::convertAndAssertXor(TNode node, bool negated)
       normalizeAndRegister(clauseNode);
     }
   }
+  Trace("cnf") << pop;
 }
 
 void ProofCnfStream::convertAndAssertIff(TNode node, bool negated)
 {
   Trace("cnf") << "ProofCnfStream::convertAndAssertIff(" << node
-               << ", negated = " << (negated ? "true" : "false") << ")\n";
+               << ", negated = " << (negated ? "true" : "false") << ")\n"
+               << push;
   if (!negated)
   {
     // p <=> q
@@ -400,12 +408,14 @@ void ProofCnfStream::convertAndAssertIff(TNode node, bool negated)
       normalizeAndRegister(clauseNode);
     }
   }
+  Trace("cnf") << pop;
 }
 
 void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated)
 {
   Trace("cnf") << "ProofCnfStream::convertAndAssertImplies(" << node
-               << ", negated = " << (negated ? "true" : "false") << ")\n";
+               << ", negated = " << (negated ? "true" : "false") << ")\n"
+               << push;
   if (!negated)
   {
     // ~p v q
@@ -444,12 +454,14 @@ void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated)
         << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM2 added "
         << node[1].notNode() << "\n";
   }
+  Trace("cnf") << pop;
 }
 
 void ProofCnfStream::convertAndAssertIte(TNode node, bool negated)
 {
   Trace("cnf") << "ProofCnfStream::convertAndAssertIte(" << node
-               << ", negated = " << (negated ? "true" : "false") << ")\n";
+               << ", negated = " << (negated ? "true" : "false") << ")\n"
+               << push;
   // ITE(p, q, r)
   SatLiteral p = toCNF(node[0], false);
   SatLiteral q = toCNF(node[1], negated);
@@ -515,6 +527,7 @@ void ProofCnfStream::convertAndAssertIte(TNode node, bool negated)
       normalizeAndRegister(clauseNode);
     }
   }
+  Trace("cnf") << pop;
 }
 
 void ProofCnfStream::convertPropagation(TrustNode trn)
@@ -590,6 +603,20 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
   }
 }
 
+
+Node ProofCnfStream::getClauseNode(const SatClause& clause)
+{
+  std::vector<Node> clauseNodes;
+  for (size_t i = 0, size = clause.size(); i < size; ++i)
+  {
+    SatLiteral satLit = clause[i];
+    clauseNodes.push_back(d_cnfStream.getNode(satLit));
+  }
+  // order children by node id
+  std::sort(clauseNodes.begin(), clauseNodes.end());
+  return NodeManager::currentNM()->mkNode(kind::OR, clauseNodes);
+}
+
 void ProofCnfStream::ensureLiteral(TNode n)
 {
   Trace("cnf") << "ProofCnfStream::ensureLiteral(" << n << ")\n";

diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index af131c2c39dc1107252975b57c913beaabb67579..b79b3098f11e2ca4b435a6db57620a23dfc3439f 100644 (file)
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -148,8 +148,19 @@ class ProofCnfStream : public ProofGenerator
    * resulting clauses of the clausification process are synchronized with the
    * clauses used in the underlying SAT solver, which automatically performs the
    * above normalizations on all added clauses.
+   *
+   * @param clauseNode The clause node to be normalized.
+   * @return The normalized clause node.
+   */
+  Node normalizeAndRegister(TNode clauseNode);
+
+  /** Gets node equivalent to SAT clause.
+   *
+   * To avoid generating different nodes for the same clause, modulo ordering,
+   * an invariant assumed throughout this class, the OR node generated by this
+   * method always has its children ordered.
    */
-  void normalizeAndRegister(TNode clauseNode);
+  Node getClauseNode(const SatClause& clause);
 
   /** Reference to the underlying cnf stream. */
   CnfStream& d_cnfStream;

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index fb37b1d011172d540d401259c9f48abdeb6f820a..fd57fb13c76ff5ed73ff4de8019538962c793a27 100644 (file)
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -42,33 +42,20 @@ SatProofManager::SatProofManager(Minisat::Solver* solver,
 
 void SatProofManager::printClause(const Minisat::Clause& clause)
 {
-  for (unsigned i = 0, size = clause.size(); i < size; ++i)
+  for (size_t i = 0, size = clause.size(); i < size; ++i)
   {
     SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
     Trace("sat-proof") << satLit << " ";
   }
 }
 
-Node SatProofManager::getClauseNode(SatLiteral satLit)
-{
-  Assert(d_cnfStream->getNodeCache().find(satLit)
-         != d_cnfStream->getNodeCache().end())
-      << "SatProofManager::getClauseNode: literal " << satLit
-      << " undefined.\n";
-  return d_cnfStream->getNodeCache()[satLit];
-}
-
 Node SatProofManager::getClauseNode(const Minisat::Clause& clause)
 {
   std::vector<Node> clauseNodes;
-  for (unsigned i = 0, size = clause.size(); i < size; ++i)
+  for (size_t i = 0, size = clause.size(); i < size; ++i)
   {
     SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
-    Assert(d_cnfStream->getNodeCache().find(satLit)
-           != d_cnfStream->getNodeCache().end())
-        << "SatProofManager::getClauseNode: literal " << satLit
-        << " undefined\n";
-    clauseNodes.push_back(d_cnfStream->getNodeCache()[satLit]);
+    clauseNodes.push_back(d_cnfStream->getNode(satLit));
   }
   // order children by node id
   std::sort(clauseNodes.begin(), clauseNodes.end());
@@ -140,7 +127,7 @@ void SatProofManager::endResChain(Minisat::Lit lit)
   SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
   Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "
                      << satLit;
-  endResChain(getClauseNode(satLit), {satLit});
+  endResChain(d_cnfStream->getNode(satLit), {satLit});
 }
 
 void SatProofManager::endResChain(const Minisat::Clause& clause)
@@ -346,7 +333,7 @@ void SatProofManager::explainLit(SatLiteral lit,
                                  std::unordered_set<TNode>& premises)
 {
   Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
-  Node litNode = getClauseNode(lit);
+  Node litNode = d_cnfStream->getNode(lit);
   Trace("sat-proof") << " [" << litNode << "]\n";
   // We don't need to explain nodes who are inputs. Note that it's *necessary*
   // to avoid attempting such explanations because they can introduce cycles at
@@ -723,7 +710,7 @@ void SatProofManager::finalizeProof()
   Trace("sat-proof")
       << "SatProofManager::finalizeProof: conflicting (lazy) satLit: "
       << d_conflictLit << "\n";
-  finalizeProof(getClauseNode(d_conflictLit), {d_conflictLit});
+  finalizeProof(d_cnfStream->getNode(d_conflictLit), {d_conflictLit});
   // reset since if in incremental mode this may be used again
   d_conflictLit = undefSatVariable;
 }
@@ -733,7 +720,7 @@ void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding)
   SatLiteral satLit = MinisatSatSolver::toSatLiteral(inConflict);
   Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting satLit: "
                      << satLit << "\n";
-  Node clauseNode = getClauseNode(satLit);
+  Node clauseNode = d_cnfStream->getNode(satLit);
   if (adding)
   {
     registerSatAssumptions({clauseNode});
@@ -777,9 +764,11 @@ std::shared_ptr<ProofNode> SatProofManager::getProof()
 void SatProofManager::registerSatLitAssumption(Minisat::Lit lit)
 {
   Trace("sat-proof") << "SatProofManager::registerSatLitAssumption: - "
-                     << getClauseNode(MinisatSatSolver::toSatLiteral(lit))
+                     << d_cnfStream->getNode(
+                            MinisatSatSolver::toSatLiteral(lit))
                      << "\n";
-  d_assumptions.insert(getClauseNode(MinisatSatSolver::toSatLiteral(lit)));
+  d_assumptions.insert(
+      d_cnfStream->getNode(MinisatSatSolver::toSatLiteral(lit)));
 }
 
 void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps)

diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index a224f3a28fc2d81aa3aaa385686fb7ce62f3ece2..98d125591afb265d89a891af7dd49cf60da2bb28 100644 (file)
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -568,14 +568,11 @@ class SatProofManager
   /** All clauses added to the SAT solver, kept in a context-dependent manner.
    */
   context::CDHashSet<Node> d_assumptions;
-
   /**
    * A placeholder that may be used to store the literal with the final
    * conflict.
    */
   SatLiteral d_conflictLit;
-  /** Gets node equivalent to literal */
-  Node getClauseNode(SatLiteral satLit);
   /** Gets node equivalent to clause.
    *
    * To avoid generating different nodes for the same clause, modulo ordering,