(proof-new) Witness axiom reconstruction for purification skolems (#5289)

This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify.

This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.

6 files changed, 81 insertions, 34 deletions

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 4000d4df7..9c955d067 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -670,10 +670,11 @@ enum class PfRule : uint32_t
   WITNESS_INTRO,
   // ======== Exists intro
   // Children: (P:F[t])
-  // Arguments: (t)
+  // Arguments: ((exists ((x T)) F[x]))
   // ----------------------------------------
   // Conclusion: (exists ((x T)) F[x])
-  // where x is a BOUND_VARIABLE unique to the pair F,t.
+  // This rule verifies that F[x] indeed matches F[t] with a substitution
+  // over x.
   EXISTS_INTRO,
   // ======== Skolemize
   // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index e34813dcd..a3647e84f 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -33,6 +33,7 @@ struct SkolemFormAttributeId
 };
 typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
 
+// Maps terms to their purify skolem variables
 struct PurifySkolemAttributeId
 {
 };
@@ -125,7 +126,7 @@ Node SkolemManager::skolemize(Node q,
     // 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);
+    Node avp = getOrMakeBoundVariable(av);
     ovarsW.push_back(avp);
     ovars.push_back(av);
   }
@@ -182,19 +183,9 @@ Node SkolemManager::mkBooleanTermVariable(Node t)
   return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
 }
 
-Node SkolemManager::mkExistential(Node t, Node p)
+ProofGenerator* SkolemManager::getProofGenerator(Node t) const
 {
-  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);
+  std::map<Node, ProofGenerator*>::const_iterator it = d_gens.find(t);
   if (it != d_gens.end())
   {
     return it->second;
@@ -353,18 +344,16 @@ Node SkolemManager::getOrMakeSkolem(Node w,
   return k;
 }
 
-Node SkolemManager::getOrMakeBoundVariable(Node t, Node s)
+Node SkolemManager::getOrMakeBoundVariable(Node t)
 {
-  std::pair<Node, Node> key(t, s);
-  std::map<std::pair<Node, Node>, Node>::iterator it =
-      d_witnessBoundVar.find(key);
+  std::map<Node, Node>::iterator it = d_witnessBoundVar.find(t);
   if (it != d_witnessBoundVar.end())
   {
     return it->second;
   }
   TypeNode tt = t.getType();
   Node v = NodeManager::currentNM()->mkBoundVar(tt);
-  d_witnessBoundVar[key] = v;
+  d_witnessBoundVar[t] = v;
   return v;
 }
 
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index ec5189d6d..537c0b1e9 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -159,13 +159,7 @@ class SkolemManager
    * 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 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);
+  ProofGenerator* getProofGenerator(Node q) const;
   /**
    * Convert to witness form, where notice this recursively replaces *all*
    * skolems in n by their corresponding witness term. This is intended to be
@@ -197,7 +191,7 @@ class SkolemManager
    * Map to canonical bound variables. This is used for example by the method
    * mkExistential.
    */
-  std::map<std::pair<Node, Node>, Node> d_witnessBoundVar;
+  std::map<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 */
@@ -224,10 +218,11 @@ class SkolemManager
                  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.
+   * Get or make bound variable unique to t whose type is the same as t. This
+   * is used to construct canonical bound variables e.g. for constructing
+   * bound variables for witness terms in the skolemize method above.
    */
-  Node getOrMakeBoundVariable(Node t, Node s);
+  Node getOrMakeBoundVariable(Node t);
 };
 
 }  // namespace CVC4
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index e8d4f7356..e4f0a56dc 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -28,7 +28,8 @@ WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm)
              "WfGenerator::TConvProofGenerator",
              nullptr,
              true),
-      d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof")
+      d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"),
+      d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof")
 {
 }
 
@@ -92,6 +93,20 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
           Node skBody = SkolemManager::getSkolemForm(curw[1]);
           Node exists = nm->mkNode(kind::EXISTS, curw[0], skBody);
           ProofGenerator* pg = skm->getProofGenerator(exists);
+          if (pg == nullptr)
+          {
+            // it may be a purification skolem
+            pg = convertExistsInternal(exists);
+            if (pg == nullptr)
+            {
+              // if no proof generator is provided, we justify the existential
+              // using the WITNESS_AXIOM trusted rule by providing it to the
+              // call to addLazyStep below.
+              Trace("witness-form")
+                  << "WitnessFormGenerator: No proof generator for " << exists
+                  << std::endl;
+            }
+          }
           // --------------------------- from pg
           // (exists ((x T)) (P x))
           // --------------------------- WITNESS_INTRO
@@ -141,5 +156,28 @@ WitnessFormGenerator::getWitnessFormEqs() const
   return d_eqs;
 }
 
+ProofGenerator* WitnessFormGenerator::convertExistsInternal(Node exists)
+{
+  Assert(exists.getKind() == kind::EXISTS);
+  if (exists[0].getNumChildren() == 1 && exists[1].getKind() == kind::EQUAL
+      && exists[1][0] == exists[0][0])
+  {
+    Node tpurified = exists[1][1];
+    Trace("witness-form") << "convertExistsInternal: infer purification "
+                          << exists << " for " << tpurified << std::endl;
+    // ------ REFL
+    // t = t
+    // ---------------- EXISTS_INTRO
+    // exists x. x = t
+    // The concluded existential is then used to construct the witness term
+    // via witness intro.
+    Node teq = tpurified.eqNode(tpurified);
+    d_pskPf.addStep(teq, PfRule::REFL, {}, {tpurified});
+    d_pskPf.addStep(exists, PfRule::EXISTS_INTRO, {teq}, {exists});
+    return &d_pskPf;
+  }
+  return nullptr;
+}
+
 }  // namespace smt
 }  // namespace CVC4
diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h
index 50c913ae9..eb0cf3005 100644
--- a/src/smt/witness_form.h
+++ b/src/smt/witness_form.h
@@ -81,6 +81,10 @@ class WitnessFormGenerator : public ProofGenerator
    * of this class (d_tcpg).
    */
   Node convertToWitnessForm(Node t);
+  /**
+   * Return a proof generator that can prove the given axiom exists.
+   */
+  ProofGenerator* convertExistsInternal(Node exists);
   /** The term conversion proof generator */
   TConvProofGenerator d_tcpg;
   /** The nodes we have already added rewrite steps for in d_tcpg */
@@ -89,6 +93,8 @@ class WitnessFormGenerator : public ProofGenerator
   std::unordered_set<Node, NodeHashFunction> d_eqs;
   /** Lazy proof storing witness intro steps */
   LazyCDProof d_wintroPf;
+  /** CDProof for justifying purification existentials */
+  CDProof d_pskPf;
 };
 
 }  // namespace smt
diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp
index e2a416120..8371492b5 100644
--- a/src/theory/quantifiers/proof_checker.cpp
+++ b/src/theory/quantifiers/proof_checker.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/proof_checker.h"
 
+#include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "theory/builtin/proof_checker.h"
 
@@ -43,8 +44,25 @@ Node QuantifiersProofRuleChecker::checkInternal(
     Assert(children.size() == 1);
     Assert(args.size() == 1);
     Node p = children[0];
-    Node t = args[0];
-    return sm->mkExistential(t, p);
+    Node exists = args[0];
+    if (exists.getKind() != kind::EXISTS || exists[0].getNumChildren() != 1)
+    {
+      return Node::null();
+    }
+    std::unordered_map<Node, Node, NodeHashFunction> subs;
+    if (!expr::match(exists[1], p, subs))
+    {
+      return Node::null();
+    }
+    // substitution must contain only the variable of the existential
+    for (const std::pair<const Node, Node>& s : subs)
+    {
+      if (s.first != exists[0][0])
+      {
+        return Node::null();
+      }
+    }
+    return exists;
   }
   else if (id == PfRule::WITNESS_INTRO)
   {