[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.

5 files changed, 83 insertions, 36 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index ac0c7819a..264f5480d 100644
--- 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 90ed1b9cd..69cbb0241 100644
--- 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 d98de2a8a..b204c465c 100644
--- 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 d05dd2f16..1f3d043b8 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -85,6 +85,14 @@ class ProofCnfStream : public ProofGenerator
   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. */
   void addBlocked(std::shared_ptr<ProofNode> pfn);
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 28159c229..da19480f9 100644
--- 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;
 }