(proof-new) Updates to skolem manager interface (#4664)

Adds a fix for mkPurifySkolem and introduces new interfaces in preparation for arithmetic operator elimination and term formula removal proofs.

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index c3435f445cbddfaec7eb2c60a75da72a3ee15cf7..098ff8eeaaffc8a4d61ea76a0617caa27eb2777e 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -550,8 +550,10 @@ public:
     SKOLEM_DEFAULT = 0,    /**< default behavior */
     SKOLEM_NO_NOTIFY = 1,  /**< do not notify subscribers */
     SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */
-    SKOLEM_IS_GLOBAL = 4   /**< global vars appear in models even after a pop */
-  };
+    SKOLEM_IS_GLOBAL = 4,  /**< global vars appear in models even after a pop */
+    SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
+  };                         /* enum SkolemFlags */
+
   /**
    * Create a skolem constant with the given name, type, and comment.
    *

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 99f2525303689c3bb99d29cac7ca5be45e904f80..e22bd26cf1f195aacb7f60bf26c55e5ce58c6abe 100644 (file)
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -15,6 +15,7 @@
 #include "expr/skolem_manager.h"
 
 #include "expr/attribute.h"
+#include "expr/node_algorithm.h"
 
 using namespace CVC4::kind;
 
@@ -42,7 +43,8 @@ Node SkolemManager::mkSkolem(Node v,
                              const std::string& prefix,
                              const std::string& comment,
                              int flags,
-                             ProofGenerator* pg)
+                             ProofGenerator* pg,
+                             bool retWitness)
 {
   Assert(v.getKind() == BOUND_VARIABLE);
   // make the witness term
@@ -55,12 +57,20 @@ Node SkolemManager::mkSkolem(Node v,
   // store the mapping to proof generator if it exists
   if (pg != nullptr)
   {
-    Node q = nm->mkNode(EXISTS, w[0], w[1]);
+    // We cache based on the original (Skolem) form, since the user of this
+    // method operates on Skolem forms.
+    Node q = nm->mkNode(EXISTS, bvl, pred);
     // Notice this may overwrite an existing proof generator. This does not
     // matter since either should be able to prove q.
     d_gens[q] = pg;
   }
-  return getOrMakeSkolem(w, prefix, comment, flags);
+  Node k = getOrMakeSkolem(w, prefix, comment, flags);
+  // if we want to return the witness term, make it
+  if (retWitness)
+  {
+    return nm->mkNode(WITNESS, bvl, pred);
+  }
+  return k;
 }
 
 Node SkolemManager::mkSkolemize(Node q,
@@ -159,7 +169,7 @@ Node SkolemManager::mkPurifySkolem(Node t,
   // directly.
   if (t.getKind() == WITNESS)
   {
-    return getOrMakeSkolem(t, prefix, comment, flags);
+    return getOrMakeSkolem(getWitnessForm(t), prefix, comment, flags);
   }
   Node v = NodeManager::currentNM()->mkBoundVar(t.getType());
   Node k = mkSkolem(v, v.eqNode(t), prefix, comment, flags);
@@ -167,6 +177,11 @@ Node SkolemManager::mkPurifySkolem(Node t,
   return k;
 }
 
+Node SkolemManager::mkBooleanTermVariable(Node t)
+{
+  return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
+}
+
 Node SkolemManager::mkExistential(Node t, Node p)
 {
   Assert(p.getType().isBoolean());
@@ -275,7 +290,9 @@ Node SkolemManager::convertInternal(Node n, bool toWitness)
         // called on them. Regardless, witness terms with free variables
         // should never be themselves assigned skolems (otherwise we would have
         // assertions with free variables), and thus they can be treated like
-        // ordinary terms here.
+        // ordinary terms here. We use an assertion to check that this is
+        // indeed the case.
+        Assert(cur.getKind() != WITNESS || expr::hasFreeVar(cur));
         cur.setAttribute(sfa, ret);
       }
       visited[cur] = ret;
@@ -316,7 +333,16 @@ Node SkolemManager::getOrMakeSkolem(Node w,
   }
   NodeManager* nm = NodeManager::currentNM();
   // make the new skolem
-  Node k = nm->mkSkolem(prefix, w.getType(), comment, flags);
+  Node k;
+  if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR)
+  {
+    Assert (w.getType().isBoolean());
+    k = nm->mkBooleanTermVariable();
+  }
+  else
+  {
+    k = nm->mkSkolem(prefix, w.getType(), comment, flags);
+  }
   // set witness form attribute for k
   WitnessFormAttribute wfa;
   k.setAttribute(wfa, w);

diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 8dd3a3ef969fa09ce1f0eaf58f81bb7c98318972..1e02d94f4447a7537201e20f4a7c515bf573b771 100644 (file)
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -86,6 +86,12 @@ class SkolemManager
    * @param pg The proof generator for this skolem. If non-null, this proof
    * generator must respond to a call to getProofFor(exists v. pred) during
    * the lifetime of the current node manager.
+   * @param retWitness Whether we wish to return the witness term for the
+   * given Skolem, which notice is of the form (witness v. pred), where pred
+   * is in Skolem form. A typical use case of setting this flag to true
+   * is preprocessing passes that eliminate terms. Using a witness term
+   * instead of its corresponding Skolem indicates that the body of the witness
+   * term needs to be added as an assertion, e.g. by the term formula remover.
    * @return The skolem whose witness form is registered by this class.
    */
   Node mkSkolem(Node v,
@@ -93,7 +99,8 @@ class SkolemManager
                 const std::string& prefix,
                 const std::string& comment = "",
                 int flags = NodeManager::SKOLEM_DEFAULT,
-                ProofGenerator* pg = nullptr);
+                ProofGenerator* pg = nullptr,
+                bool retWitness = false);
   /**
    * Make skolemized form of existentially quantified formula q, and store its
    * Skolems into the argument skolems.
@@ -142,6 +149,12 @@ class SkolemManager
                       const std::string& prefix,
                       const std::string& comment = "",
                       int flags = NodeManager::SKOLEM_DEFAULT);
+  /**
+   * Make Boolean term variable for term t. This is a special case of
+   * mkPurifySkolem above, where the returned term has kind
+   * BOOLEAN_TERM_VARIABLE.
+   */
+  Node mkBooleanTermVariable(Node t);
   /**
    * Get proof generator for existentially quantified formula q. This returns
    * the proof generator that was provided in a call to mkSkolem above.
@@ -153,13 +166,18 @@ class SkolemManager
    * where T is the type of t, and x is a variable unique to t,p.
    */
   Node mkExistential(Node t, Node p);
-  /** convert to witness form
+  /**
+   * Convert to witness form, where notice this recursively replaces *all*
+   * skolems in n by their corresponding witness term. This is intended to be
+   * used by the proof checker only.
    *
    * @param n The term or formula to convert to witness form described above
    * @return n in witness form.
    */
   static Node getWitnessForm(Node n);
-  /** convert to Skolem form
+  /**
+   * Convert to Skolem form, which recursively replaces all witness terms in n
+   * by their corresponding Skolems.
    *
    * @param n The term or formula to convert to Skolem form described above
    * @return n in Skolem form.