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

3 files changed, 16 insertions, 31 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