[proof-new] Adding a proof-producing ensure literal method (#5889)

The ensureLiteral method in CnfStream may apply CNF conversion to the given literal (for example if it's an IFF), which needs to be recorded in the proof. This commit adds a proof-producing ensureLiteral to ProofCnfStream, which is called by the prop engine if proofs are enabled.

This commit also simplifies the interfaces on ensureLit and convertAtom by removing the preRegistration flag, which was never used.

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index ac0c7819a69651207774216b4e81df7ce6beed30..264f5480db8b632569703df25bf4743e33138015 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -127,41 +127,37 @@ bool CnfStream::hasLiteral(TNode n) const {
   return find != d_nodeToLiteralMap.end();
 }
 
-void CnfStream::ensureLiteral(TNode n, bool noPreregistration)
+void CnfStream::ensureMappingForLiteral(TNode n)
 {
-  // These are not removable and have no proof ID
-  d_removable = false;
-
-  Trace("cnf") << "ensureLiteral(" << n << ")\n";
-  if(hasLiteral(n)) {
-    SatLiteral lit = getLiteral(n);
-    if(!d_literalToNodeMap.contains(lit)){
-      // Store backward-mappings
-      d_literalToNodeMap.insert(lit, n);
-      d_literalToNodeMap.insert(~lit, n.notNode());
-    }
-    return;
+  SatLiteral lit = getLiteral(n);
+  if (!d_literalToNodeMap.contains(lit))
+  {
+    // Store backward-mappings
+    d_literalToNodeMap.insert(lit, n);
+    d_literalToNodeMap.insert(~lit, n.notNode());
   }
+}
 
+void CnfStream::ensureLiteral(TNode n)
+{
   AlwaysAssertArgument(
-      n.getType().isBoolean(),
+      hasLiteral(n) || n.getType().isBoolean(),
       n,
-      "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
+      "ProofCnfStream::ensureLiteral() requires a node of Boolean type.\n"
       "got node: %s\n"
       "its type: %s\n",
       n.toString().c_str(),
       n.getType().toString().c_str());
-
-  bool negated CVC4_UNUSED = false;
-  SatLiteral lit;
-
-  if(n.getKind() == kind::NOT) {
-    negated = true;
-    n = n[0];
+  Trace("cnf") << "ensureLiteral(" << n << ")\n";
+  if (hasLiteral(n))
+  {
+    ensureMappingForLiteral(n);
+    return;
   }
-
-  if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL &&
-      !n.isVar() ) {
+  // remove top level negation
+  n = n.getKind() == kind::NOT ? n[0] : n;
+  if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
+  {
     // If we were called with something other than a theory atom (or
     // Boolean variable), we get a SatLiteral that is definitionally
     // equal to it.
@@ -176,8 +172,10 @@ void CnfStream::ensureLiteral(TNode n, bool noPreregistration)
     {
       d_cnfProof->pushCurrentAssertion(Node::null());
     }
+    // These are not removable and have no proof ID
+    d_removable = false;
 
-    lit = toCNF(n, false);
+    SatLiteral lit = toCNF(n, false);
 
     if (d_cnfProof)
     {
@@ -188,13 +186,12 @@ void CnfStream::ensureLiteral(TNode n, bool noPreregistration)
     // These may already exist
     d_literalToNodeMap.insert_safe(lit, n);
     d_literalToNodeMap.insert_safe(~lit, n.notNode());
-  } else {
+  }
+  else
+  {
     // We have a theory atom or variable.
-    lit = convertAtom(n, noPreregistration);
+    convertAtom(n);
   }
-
-  Assert(hasLiteral(n) && getNode(lit) == n);
-  Debug("ensureLiteral") << "CnfStream::ensureLiteral(): out lit is " << lit << std::endl;
 }
 
 SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) {
@@ -287,7 +284,8 @@ void CnfStream::setProof(CnfProof* proof) {
   d_cnfProof = proof;
 }
 
-SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
+SatLiteral CnfStream::convertAtom(TNode node)
+{
   Trace("cnf") << "convertAtom(" << node << ")\n";
 
   Assert(!hasLiteral(node)) << "atom already mapped!";
@@ -305,7 +303,7 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
   {
     theoryLiteral = true;
     canEliminate = false;
-    preRegister = !noPreregistration;
+    preRegister = true;
   }
 
   // Make a new literal (variables are not considered theory literals)
@@ -557,6 +555,8 @@ SatLiteral CnfStream::toCNF(TNode node, bool negated)
     break;
   }
   // Return the (maybe negated) literal
+  Trace("cnf") << "toCNF(): resulting literal: "
+               << (!negated ? nodeLit : ~nodeLit) << "\n";
   return !negated ? nodeLit : ~nodeLit;
 }
 

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 90ed1b9cd1af3544633874b221ea065fd08bfe9c..69cbb02417d18f89f0b5f9443f750bf1c851c772 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -131,7 +131,7 @@ class CnfStream {
    * can be queried via getSatValue(). Essentially, this is like a "convert-but-
    * don't-assert" version of convertAndAssert().
    */
-  void ensureLiteral(TNode n, bool noPreregistration = false);
+  void ensureLiteral(TNode n);
 
   /**
    * Returns the literal that represents the given node in the SAT CNF
@@ -203,6 +203,13 @@ class CnfStream {
   SatLiteral handleAnd(TNode node);
   SatLiteral handleOr(TNode node);
 
+  /** Stores the literal of the given node in d_literalToNodeMap.
+   *
+   * Note that n must already have a literal associated to it in
+   * d_nodeToLiteralMap.
+   */
+  void ensureMappingForLiteral(TNode n);
+
   /** The SAT solver we will be using */
   SatSolver* d_satSolver;
 
@@ -302,7 +309,7 @@ class CnfStream {
    * structure in this expression.  Assumed to not be in the
    * translation cache.
    */
-  SatLiteral convertAtom(TNode node, bool noPreprocessing = false);
+  SatLiteral convertAtom(TNode node);
 
   /** Pointer to resource manager for associated SmtEngine */
   ResourceManager* d_resourceManager;

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index d98de2a8a8cccdd0b0140a3c06abc3b84d0191f0..b204c465c32263bc167a755323d11e212651b5e7 100644 (file)
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -570,6 +570,31 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn)
   d_psb.clear();
 }
 
+void ProofCnfStream::ensureLiteral(TNode n)
+{
+  Trace("cnf") << "ProofCnfStream::ensureLiteral(" << n << ")\n";
+  if (d_cnfStream.hasLiteral(n))
+  {
+    d_cnfStream.ensureMappingForLiteral(n);
+    return;
+  }
+  // remove top level negation. We don't need to track this because it's a
+  // literal.
+  n = n.getKind() == kind::NOT ? n[0] : n;
+  if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
+  {
+    SatLiteral lit = toCNF(n, false);
+    // Store backward-mappings
+    // These may already exist
+    d_cnfStream.d_literalToNodeMap.insert_safe(lit, n);
+    d_cnfStream.d_literalToNodeMap.insert_safe(~lit, n.notNode());
+  }
+  else
+  {
+    d_cnfStream.convertAtom(n);
+  }
+}
+
 SatLiteral ProofCnfStream::toCNF(TNode node, bool negated)
 {
   Trace("cnf") << "toCNF(" << node

diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index d05dd2f16696a78d2cda5b99ce6812fb7e0c7e8c..1f3d043b82b94887a0178d573d84cd6d04d44d5e 100644 (file)
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -84,6 +84,14 @@ class ProofCnfStream : public ProofGenerator
    * node are saved in d_proof. */
   void convertPropagation(theory::TrustNode ttn);
 
+  /**
+   * Ensure that the given node will have a designated SAT literal that is
+   * definitionally equal to it.  The result of this function is that the Node
+   * can be queried via getSatValue(). Essentially, this is like a "convert-but-
+   * don't-assert" version of convertAndAssert().
+   */
+  void ensureLiteral(TNode n);
+
   /**
    * Blocks a proof, so that it is not further updated by a post processor of
    * this class's proof. */

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 28159c229b14bfa200fd613917ca047ae30c1e35..da19480f9f1d9f2f475dbcb93c056c80cdb17d01 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -422,7 +422,14 @@ Node PropEngine::ensureLiteral(TNode n)
   Node preprocessed = getPreprocessedTerm(n);
   Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
                          << std::endl;
-  d_cnfStream->ensureLiteral(preprocessed);
+  if (isProofEnabled())
+  {
+    d_pfCnfStream->ensureLiteral(preprocessed);
+  }
+  else
+  {
+    d_cnfStream->ensureLiteral(preprocessed);
+  }
   return preprocessed;
 }