[proof-new] Fix handling of removable clauses in proof cnf stream (#5961)

Previously the removable information was not being communicated from the proof cnf stream to the cnf stream, which is the one that actually uses this when asserting clauses into the SAT solver. This commit fixes this by having the proof cnf stream directly use the cnf stream d_removable attribute.

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index b204c465c32263bc167a755323d11e212651b5e7..61ecefb8ece1b862951d70bd1b120c878a97d446 100644 (file)
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -75,7 +75,7 @@ void ProofCnfStream::convertAndAssert(TNode node,
   Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
                << ", negated = " << (negated ? "true" : "false")
                << ", removable = " << (removable ? "true" : "false") << ")\n";
-  d_removable = removable;
+  d_cnfStream.d_removable = removable;
   if (pg)
   {
     Trace("cnf") << "ProofCnfStream::convertAndAssert: pg: " << pg->identify()
@@ -583,6 +583,8 @@ void ProofCnfStream::ensureLiteral(TNode n)
   n = n.getKind() == kind::NOT ? n[0] : n;
   if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
   {
+    // These are not removable
+    d_cnfStream.d_removable = false;
     SatLiteral lit = toCNF(n, false);
     // Store backward-mappings
     // These may already exist
@@ -622,7 +624,9 @@ SatLiteral ProofCnfStream::toCNF(TNode node, bool negated)
       lit = node[0].getType().isBoolean() ? handleIff(node)
                                           : d_cnfStream.convertAtom(node);
       break;
-    default: { lit = d_cnfStream.convertAtom(node);
+    default:
+    {
+      lit = d_cnfStream.convertAtom(node);
     }
     break;
   }
@@ -635,7 +639,8 @@ SatLiteral ProofCnfStream::handleAnd(TNode node)
   Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
   Assert(node.getKind() == kind::AND) << "Expecting an AND expression!";
   Assert(node.getNumChildren() > 1) << "Expecting more than 1 child!";
-  Assert(!d_removable) << "Removable clauses cannot contain Boolean structure";
+  Assert(!d_cnfStream.d_removable)
+      << "Removable clauses cannot contain Boolean structure";
   Trace("cnf") << "ProofCnfStream::handleAnd(" << node << ")\n";
   // Number of children
   unsigned size = node.getNumChildren();
@@ -698,7 +703,8 @@ SatLiteral ProofCnfStream::handleOr(TNode node)
   Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
   Assert(node.getKind() == kind::OR) << "Expecting an OR expression!";
   Assert(node.getNumChildren() > 1) << "Expecting more then 1 child!";
-  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Assert(!d_cnfStream.d_removable)
+      << "Removable clauses can not contain Boolean structure";
   Trace("cnf") << "ProofCnfStream::handleOr(" << node << ")\n";
   // Number of children
   unsigned size = node.getNumChildren();
@@ -754,7 +760,8 @@ SatLiteral ProofCnfStream::handleXor(TNode node)
   Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
   Assert(node.getKind() == kind::XOR) << "Expecting an XOR expression!";
   Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
-  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Assert(!d_cnfStream.d_removable)
+      << "Removable clauses can not contain Boolean structure";
   Trace("cnf") << "ProofCnfStream::handleXor(" << node << ")\n";
   SatLiteral a = toCNF(node[0]);
   SatLiteral b = toCNF(node[1]);
@@ -871,7 +878,8 @@ SatLiteral ProofCnfStream::handleImplies(TNode node)
   Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
   Assert(node.getKind() == kind::IMPLIES) << "Expecting an IMPLIES expression!";
   Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
-  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Assert(!d_cnfStream.d_removable)
+      << "Removable clauses can not contain Boolean structure";
   Trace("cnf") << "ProofCnfStream::handleImplies(" << node << ")\n";
   // Convert the children to cnf
   SatLiteral a = toCNF(node[0]);
@@ -920,7 +928,8 @@ SatLiteral ProofCnfStream::handleIte(TNode node)
   Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
   Assert(node.getKind() == kind::ITE);
   Assert(node.getNumChildren() == 3);
-  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Assert(!d_cnfStream.d_removable)
+      << "Removable clauses can not contain Boolean structure";
   Trace("cnf") << "handleIte(" << node[0] << " " << node[1] << " " << node[2]
                << ")\n";
   SatLiteral condLit = toCNF(node[0]);

diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index 1f3d043b82b94887a0178d573d84cd6d04d44d5e..12beaf6eb1a42d6d8e73a471224e1bb7ccdb546a 100644 (file)
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -151,13 +151,6 @@ class ProofCnfStream : public ProofGenerator
    * above normalizations on all added clauses.
    */
   void normalizeAndRegister(TNode clauseNode);
-  /**
-   * Are we asserting a removable clause (true) or a permanent clause (false).
-   * This is set at the beginning of convertAndAssert so that it doesn't need to
-   * be passed on over the stack. Only pure clauses can be asserted as
-   * removable.
-   */
-  bool d_removable;
   /** Reference to the underlying cnf stream. */
   CnfStream& d_cnfStream;
   /** The proof manager of underlying SAT solver associated with this stream. */