From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 23 Feb 2021 14:59:32 +0000 (-0300)
Subject: [proof-new] Fix handling of removable clauses in proof cnf stream (#5961)
X-Git-Tag: cvc5-1.0.0~2238
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c2311f97441befbf10e80ab597455b3ab8ccc10c;p=cvc5.git

[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 b204c465c..61ecefb8e 100644
--- 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 1f3d043b8..12beaf6eb 100644
--- 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. */