(proof-new) Refactor skolemization (#4586)

This PR refactors skolemization in SkolemManager so that we use a "curried" form, where witnesses for a variable x is based on the existential where the prefix up to x has already been skolemized.

This additionally adds more utility functions that will be used in the internal proof checker for quantifiers.

2 files changed, 176 insertions, 41 deletions

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 0570af687..ced58eaf2 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -20,6 +20,8 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
+// Attributes are global maps from Nodes to data. Thus, note that these could
+// be implemented as internal maps in SkolemManager.
 struct WitnessFormAttributeId
 {
 };
@@ -50,43 +52,97 @@ Node SkolemManager::mkSkolem(Node v,
   Node predw = getWitnessForm(pred);
   // make the witness term, which should not contain any skolem
   Node w = nm->mkNode(WITNESS, bvl, predw);
-  // store the mapping to proof generator
-  d_gens[w] = pg;
+  // store the mapping to proof generator if it exists
+  if (pg != nullptr)
+  {
+    Node q = nm->mkNode(EXISTS, w[0], w[1]);
+    // 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 SkolemManager::mkSkolemExists(Node v,
-                                   Node q,
-                                   const std::string& prefix,
-                                   const std::string& comment,
-                                   int flags,
-                                   ProofGenerator* pg)
+Node SkolemManager::mkSkolemize(Node q,
+                                std::vector<Node>& skolems,
+                                const std::string& prefix,
+                                const std::string& comment,
+                                int flags,
+                                ProofGenerator* pg)
+{
+  Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
+  Assert(q.getKind() == EXISTS);
+  Node currQ = q;
+  for (const Node& av : q[0])
+  {
+    Assert(currQ.getKind() == EXISTS && av == currQ[0][0]);
+    // currQ is updated to the result of skolemizing its first variable in
+    // the method below.
+    Node sk = skolemize(currQ, currQ, prefix, comment, flags);
+    Trace("sk-manager-debug")
+        << "made skolem " << sk << " for " << av << std::endl;
+    skolems.push_back(sk);
+  }
+  if (pg != nullptr)
+  {
+    // Same as above, this may overwrite an existing proof generator
+    d_gens[q] = pg;
+  }
+  return currQ;
+}
+
+Node SkolemManager::skolemize(Node q,
+                              Node& qskolem,
+                              const std::string& prefix,
+                              const std::string& comment,
+                              int flags)
 {
   Assert(q.getKind() == EXISTS);
-  bool foundVar = false;
+  Node v;
   std::vector<Node> ovars;
+  std::vector<Node> ovarsW;
+  Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
   for (const Node& av : q[0])
   {
-    if (av == v)
+    if (v.isNull())
     {
-      foundVar = true;
+      v = av;
       continue;
     }
+    // must make fresh variable to avoid shadowing, which is unique per
+    // variable av to ensure that this method is deterministic. Having this
+    // method deterministic ensures that the proof checker (e.g. for
+    // quantifiers) is capable of proving the expected value for conclusions
+    // of proof rules, instead of an alpha-equivalent variant of a conclusion.
+    Node avp = getOrMakeBoundVariable(av, av);
+    ovarsW.push_back(avp);
     ovars.push_back(av);
   }
-  if (!foundVar)
-  {
-    Assert(false);
-    return Node::null();
-  }
+  Assert(!v.isNull());
   Node pred = q[1];
+  qskolem = q[1];
+  Trace("sk-manager-debug") << "make exists predicate" << std::endl;
   if (!ovars.empty())
   {
-    NodeManager* nm = NodeManager::currentNM();
-    Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
+    Node bvl = nm->mkNode(BOUND_VAR_LIST, ovarsW);
     pred = nm->mkNode(EXISTS, bvl, pred);
+    // skolem form keeps the old variables
+    bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
+    qskolem = nm->mkNode(EXISTS, bvl, pred);
   }
-  return mkSkolem(v, pred, prefix, comment, flags, pg);
+  Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl;
+  // don't use a proof generator, since this may be an intermediate, partially
+  // skolemized formula.
+  Node k = mkSkolem(v, pred, prefix, comment, flags, nullptr);
+  Assert(k.getType() == v.getType());
+  TNode tv = v;
+  TNode tk = k;
+  Trace("sk-manager-debug")
+      << "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl;
+  qskolem = qskolem.substitute(tv, tk);
+  Trace("sk-manager-debug") << "qskolem done substitution" << std::endl;
+  return k;
 }
 
 Node SkolemManager::mkPurifySkolem(Node t,
@@ -111,6 +167,16 @@ Node SkolemManager::mkPurifySkolem(Node t,
   return k;
 }
 
+Node SkolemManager::mkExistential(Node t, Node p)
+{
+  Assert(p.getType().isBoolean());
+  NodeManager* nm = NodeManager::currentNM();
+  Node v = getOrMakeBoundVariable(t, p);
+  Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
+  Node psubs = p.substitute(TNode(t), TNode(v));
+  return nm->mkNode(EXISTS, bvl, psubs);
+}
+
 ProofGenerator* SkolemManager::getProofGenerator(Node t)
 {
   std::map<Node, ProofGenerator*>::iterator it = d_gens.find(t);
@@ -131,8 +197,8 @@ Node SkolemManager::convertInternal(Node n, bool toWitness)
   {
     return n;
   }
-  Trace("pf-skolem-debug") << "SkolemManager::convertInternal: " << toWitness
-                           << " " << n << std::endl;
+  Trace("sk-manager-debug") << "SkolemManager::convertInternal: " << toWitness
+                            << " " << n << std::endl;
   WitnessFormAttribute wfa;
   SkolemFormAttribute sfa;
   NodeManager* nm = NodeManager::currentNM();
@@ -217,7 +283,7 @@ Node SkolemManager::convertInternal(Node n, bool toWitness)
   } while (!visit.empty());
   Assert(visited.find(n) != visited.end());
   Assert(!visited.find(n)->second.isNull());
-  Trace("pf-skolem-debug") << "..return " << visited[n] << std::endl;
+  Trace("sk-manager-debug") << "..return " << visited[n] << std::endl;
   return visited[n];
 }
 
@@ -256,9 +322,24 @@ Node SkolemManager::getOrMakeSkolem(Node w,
   k.setAttribute(wfa, w);
   // set skolem form attribute for w
   w.setAttribute(sfa, k);
-  Trace("pf-skolem") << "SkolemManager::mkSkolem: " << k << " : " << w
-                     << std::endl;
+  Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
+                      << std::endl;
   return k;
 }
 
+Node SkolemManager::getOrMakeBoundVariable(Node t, Node s)
+{
+  std::pair<Node, Node> key(t, s);
+  std::map<std::pair<Node, Node>, Node>::iterator it =
+      d_witnessBoundVar.find(key);
+  if (it != d_witnessBoundVar.end())
+  {
+    return it->second;
+  }
+  TypeNode tt = t.getType();
+  Node v = NodeManager::currentNM()->mkBoundVar(tt);
+  d_witnessBoundVar[key] = v;
+  return v;
+}
+
 }  // namespace CVC4
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index eaf74bcce..557947214 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -84,7 +84,7 @@ class SkolemManager
    * @param comment Debug information about the Skolem
    * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
    * @param pg The proof generator for this skolem. If non-null, this proof
-   * generator must respond to a call to getProofFor(exists x. pred) during
+   * generator must respond to a call to getProofFor(exists v. pred) during
    * the lifetime of the current node manager.
    * @return The skolem whose witness form is registered by this class.
    */
@@ -95,20 +95,40 @@ class SkolemManager
                 int flags = NodeManager::SKOLEM_DEFAULT,
                 ProofGenerator* pg = nullptr);
   /**
-   * Same as above, but where pred is an existential quantified formula
-   * whose bound variable list contains v. For example, calling this method on:
-   *   x, (exists ((x Int) (y Int)) (P x y))
-   * will return:
-   *   (witness ((x Int)) (exists ((y Int)) (P x y)))
-   * If the variable v is not in the bound variable list of q, then null is
-   * returned and an assertion failure is thrown.
+   * Make skolemized form of existentially quantified formula q, and store its
+   * Skolems into the argument skolems.
+   *
+   * For example, calling this method on:
+   *   (exists ((x Int) (y Int)) (P x y))
+   * returns:
+   *   (P w1 w2)
+   * where w1 and w2 are skolems with witness forms:
+   *   (witness ((x Int)) (exists ((y' Int)) (P x y')))
+   *   (witness ((y Int)) (P w1 y))
+   * respectively. Additionally, this method will add { w1, w2 } to skolems.
+   * Notice that y is renamed to y' in the witness form of w1 to avoid variable
+   * shadowing.
+   *
+   * In contrast to mkSkolem, the proof generator is for the *entire*
+   * existentially quantified formula q, which may have multiple variables in
+   * its prefix.
+   *
+   * @param q The existentially quantified formula to skolemize,
+   * @param skolems Vector to add Skolems of q to,
+   * @param prefix The prefix of the name of each of the Skolems
+   * @param comment Debug information about each of the Skolems
+   * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
+   * @param pg The proof generator for this skolem. If non-null, this proof
+   * generator must respond to a call to getProofFor(q) during
+   * the lifetime of the current node manager.
+   * @return The skolemized form of q.
    */
-  Node mkSkolemExists(Node v,
-                      Node q,
-                      const std::string& prefix,
-                      const std::string& comment = "",
-                      int flags = NodeManager::SKOLEM_DEFAULT,
-                      ProofGenerator* pg = nullptr);
+  Node mkSkolemize(Node q,
+                   std::vector<Node>& skolems,
+                   const std::string& prefix,
+                   const std::string& comment = "",
+                   int flags = NodeManager::SKOLEM_DEFAULT,
+                   ProofGenerator* pg = nullptr);
   /**
    * Same as above, but for special case of (witness ((x T)) (= x t))
    * where T is the type of t. This skolem is unique for each t, which we
@@ -123,10 +143,16 @@ class SkolemManager
                       const std::string& comment = "",
                       int flags = NodeManager::SKOLEM_DEFAULT);
   /**
-   * Get proof generator for witness term t. This returns the proof generator
-   * that was provided in a call to mkSkolem above.
+   * Get proof generator for existentially quantified formula q. This returns
+   * the proof generator that was provided in a call to mkSkolem above.
    */
-  ProofGenerator* getProofGenerator(Node t);
+  ProofGenerator* getProofGenerator(Node q);
+  /**
+   * Make existential. Given t and p[t] where p is a formula, this returns
+   *   (exists ((x T)) p[x])
+   * 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
    *
    * @param n The term or formula to convert to witness form described above
@@ -149,6 +175,11 @@ class SkolemManager
    * Mapping from witness terms to proof generators.
    */
   std::map<Node, ProofGenerator*> d_gens;
+  /**
+   * Map to canonical bound variables. This is used for example by the method
+   * mkExistential.
+   */
+  std::map<std::pair<Node, Node>, Node> d_witnessBoundVar;
   /** Convert to witness or skolem form */
   static Node convertInternal(Node n, bool toWitness);
   /** Get or make skolem attribute for witness term w */
@@ -156,6 +187,29 @@ class SkolemManager
                               const std::string& prefix,
                               const std::string& comment,
                               int flags);
+  /**
+   * Skolemize the first variable of existentially quantified formula q.
+   * For example, calling this method on:
+   *   (exists ((x Int) (y Int)) (P x y))
+   * will return:
+   *   (witness ((x Int)) (exists ((y Int)) (P x y)))
+   * If q is not an existentially quantified formula, then null is
+   * returned and an assertion failure is thrown.
+   *
+   * This method additionally updates qskolem to be the skolemized form of q.
+   * In the above example, this is set to:
+   *   (exists ((y Int)) (P (witness ((x Int)) (exists ((y' Int)) (P x y'))) y))
+   */
+  Node skolemize(Node q,
+                 Node& qskolem,
+                 const std::string& prefix,
+                 const std::string& comment = "",
+                 int flags = NodeManager::SKOLEM_DEFAULT);
+  /**
+   * Get or make bound variable unique to (s,t), for d_witnessBoundVar, where
+   * t and s are terms.
+   */
+  Node getOrMakeBoundVariable(Node t, Node s);
 };
 
 }  // namespace CVC4