(proof-new) Replace witness form by original form in the internal proof calculus (#6051)

This makes a simplification to the internal proof calculus. In particular, purification skolems are no longer are special case of witness skolems. They are now independent concepts. The concept of "witness form" is replaced in most places by "original form".

This is required for fixing two issues:
(1) variable shadowing issues in skolemization.
(2) bookkeeping issues for bound variables introduced to construct witness terms. This made the LFSC proof conversion extremely cumbersome for e.g. string reductions.

In this PR, the main changes:

The internals of SkolemManager are changed to use original form vs witness form when necessary. This eliminates the need to do variable renaming in SkolemManager::skolemize.
the rule WITNESS_INTRO is replaced by SKOLEM_INTRO
MACRO_SR_* rules use original form
Proof post processing is simplified
These changes imply that ppRewrite should not return WITNESS terms. Followup PRs will modify arithmetic preprocessing so that its ppRewrite method returns skolems instead.

4 files changed, 115 insertions, 150 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 0b7c8cc69..579b06c76 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -127,7 +127,7 @@ const char* toString(PfRule id)
     case PfRule::DT_CLASH: return "DT_CLASH";
     case PfRule::DT_TRUST: return "DT_TRUST";
     //================================================= Quantifiers rules
-    case PfRule::WITNESS_INTRO: return "WITNESS_INTRO";
+    case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO";
     case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
     case PfRule::SKOLEMIZE: return "SKOLEMIZE";
     case PfRule::INSTANTIATE: return "INSTANTIATE";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index b25866b5e..909f7b7cd 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -133,16 +133,16 @@ enum class PfRule : uint32_t
   // where ids and idr are method identifiers.
   //
   // More generally, this rule also holds when:
-  //   Rewriter::rewrite(toWitness(F')) == true
+  //   Rewriter::rewrite(toOriginal(F')) == true
   // where F' is the result of the left hand side of the equality above. Here,
-  // notice that we apply rewriting on the witness form of F', meaning that this
-  // rule may conclude an F whose Skolem form is justified by the definition of
-  // its (fresh) Skolem variables. For example, this rule may justify the
-  // conclusion (= k t) where k is the purification Skolem for t, whose
-  // witness form is (witness ((x T)) (= x t)).
+  // notice that we apply rewriting on the original form of F', meaning that
+  // this rule may conclude an F whose Skolem form is justified by the
+  // definition of its (fresh) Skolem variables. For example, this rule may
+  // justify the conclusion (= k t) where k is the purification Skolem for t,
+  // e.g. where the original form of k is t.
   //
   // Furthermore, notice that the rewriting and substitution is applied only
-  // within the side condition, meaning the rewritten form of the witness form
+  // within the side condition, meaning the rewritten form of the original form
   // of F does not escape this rule.
   MACRO_SR_PRED_INTRO,
   // ======== Substitution + Rewriting predicate elimination
@@ -176,9 +176,9 @@ enum class PfRule : uint32_t
   //   Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
   //
   // More generally, this rule also holds when:
-  //   Rewriter::rewrite(toWitness(F')) == Rewriter::rewrite(toWitness(G'))
+  //   Rewriter::rewrite(toOriginal(F')) == Rewriter::rewrite(toOriginal(G'))
   // where F' and G' are the result of each side of the equation above. Here,
-  // witness forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
+  // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
   MACRO_SR_PRED_TRANSFORM,
 
   //================================================= Processing rules
@@ -759,13 +759,13 @@ enum class PfRule : uint32_t
   DT_TRUST,
 
   //================================================= Quantifiers rules
-  // ======== Witness intro
-  // Children: (P:(exists ((x T)) F[x]))
-  // Arguments: none
+  // ======== Skolem intro
+  // Children: none
+  // Arguments: (k)
   // ----------------------------------------
-  // Conclusion: (= k (witness ((x T)) F[x]))
-  // where k is the Skolem form of (witness ((x T)) F[x]).
-  WITNESS_INTRO,
+  // Conclusion: (= k t)
+  // where t is the original form of skolem k.
+  SKOLEM_INTRO,
   // ======== Exists intro
   // Children: (P:F[t])
   // Arguments: ((exists ((x T)) F[x]))
@@ -781,7 +781,9 @@ enum class PfRule : uint32_t
   // Conclusion: F*sigma
   // sigma maps x1 ... xn to their representative skolems obtained by
   // SkolemManager::mkSkolemize, returned in the skolems argument of that
-  // method. Alternatively, can use negated forall as a premise.
+  // method. Alternatively, can use negated forall as a premise. The witness
+  // terms for the returned skolems can be obtained by
+  // SkolemManager::getWitnessForm.
   SKOLEMIZE,
   // ======== Instantiate
   // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 3f77a170a..23ae919d3 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -22,17 +22,6 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-/**
- * Attribute for associating terms to a unique bound variable.  This
- * is used to construct canonical bound variables e.g. for constructing
- * bound variables for witness terms in the skolemize method below.
- */
-struct WitnessBoundVarAttributeId
-{
-};
-typedef expr::Attribute<WitnessBoundVarAttributeId, Node>
-    WitnessBoundVarAttribute;
-
 // Attributes are global maps from Nodes to data. Thus, note that these could
 // be implemented as internal maps in SkolemManager.
 struct WitnessFormAttributeId
@@ -45,11 +34,10 @@ struct SkolemFormAttributeId
 };
 typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
 
-// Maps terms to their purify skolem variables
-struct PurifySkolemAttributeId
+struct OriginalFormAttributeId
 {
 };
-typedef expr::Attribute<PurifySkolemAttributeId, Node> PurifySkolemAttribute;
+typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
 
 Node SkolemManager::mkSkolem(Node v,
                              Node pred,
@@ -59,25 +47,31 @@ Node SkolemManager::mkSkolem(Node v,
                              ProofGenerator* pg,
                              bool retWitness)
 {
+  // We do not currently insist that pred does not contain witness terms
   Assert(v.getKind() == BOUND_VARIABLE);
   // make the witness term
   NodeManager* nm = NodeManager::currentNM();
   Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
-  // translate pred to witness form, since pred itself may contain skolem
-  Node predw = getWitnessForm(pred);
-  // make the witness term, which should not contain any skolem
-  Node w = nm->mkNode(WITNESS, bvl, predw);
+  // Make the witness term, where notice that pred may contain skolems. We do
+  // not recursively convert pred to witness form, since witness terms should
+  // be treated as opaque. Moreover, the use of witness forms leads to
+  // variable shadowing issues in e.g. skolemization.
+  Node w = nm->mkNode(WITNESS, bvl, pred);
   // store the mapping to proof generator if it exists
   if (pg != nullptr)
   {
-    // We cache based on the original (Skolem) form, since the user of this
-    // method operates on Skolem forms.
+    // We cache based on the existential of the original predicate
     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;
   }
-  Node k = getOrMakeSkolem(w, prefix, comment, flags);
+  Node k = mkSkolemInternal(w, prefix, comment, flags);
+  // set witness form attribute for k
+  WitnessFormAttribute wfa;
+  k.setAttribute(wfa, w);
+  Trace("sk-manager-skolem")
+      << "skolem: " << k << " witness " << w << std::endl;
   // if we want to return the witness term, make it
   if (retWitness)
   {
@@ -124,10 +118,8 @@ Node SkolemManager::skolemize(Node q,
   Assert(q.getKind() == EXISTS);
   Node v;
   std::vector<Node> ovars;
-  std::vector<Node> ovarsW;
   Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
   NodeManager* nm = NodeManager::currentNM();
-  BoundVarManager* bvm = nm->getBoundVarManager();
   for (const Node& av : q[0])
   {
     if (v.isNull())
@@ -135,26 +127,17 @@ Node SkolemManager::skolemize(Node q,
       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 = bvm->mkBoundVar<WitnessBoundVarAttribute>(av, av.getType());
-    ovarsW.push_back(avp);
     ovars.push_back(av);
   }
   Assert(!v.isNull());
+  // make the predicate with one variable stripped off
   Node pred = q[1];
-  qskolem = q[1];
   Trace("sk-manager-debug") << "make exists predicate" << std::endl;
   if (!ovars.empty())
   {
-    // skolem form keeps the old variables
+    // keeps the same variables
     Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
-    qskolem = nm->mkNode(EXISTS, bvl, pred);
     // update the predicate
-    bvl = nm->mkNode(BOUND_VAR_LIST, ovarsW);
     pred = nm->mkNode(EXISTS, bvl, pred);
   }
   Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl;
@@ -166,7 +149,8 @@ Node SkolemManager::skolemize(Node q,
   TNode tk = k;
   Trace("sk-manager-debug")
       << "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl;
-  qskolem = qskolem.substitute(tv, tk);
+  // the quantified formula with one step of skolemization
+  qskolem = pred.substitute(tv, tk);
   Trace("sk-manager-debug") << "qskolem done substitution" << std::endl;
   return k;
 }
@@ -176,20 +160,16 @@ Node SkolemManager::mkPurifySkolem(Node t,
                                    const std::string& comment,
                                    int flags)
 {
-  PurifySkolemAttribute psa;
-  if (t.hasAttribute(psa))
-  {
-    return t.getAttribute(psa);
-  }
-  // The case where t is a witness term is special: we set its Skolem attribute
-  // directly.
-  if (t.getKind() == WITNESS)
-  {
-    return getOrMakeSkolem(getWitnessForm(t), prefix, comment, flags);
-  }
-  Node v = NodeManager::currentNM()->mkBoundVar(t.getType());
-  Node k = mkSkolem(v, v.eqNode(t), prefix, comment, flags);
-  t.setAttribute(psa, k);
+  Node to = getOriginalForm(t);
+  // We do not currently insist that to does not contain witness terms
+
+  Node k = mkSkolemInternal(to, prefix, comment, flags);
+  // set original form attribute for k
+  OriginalFormAttribute ofa;
+  k.setAttribute(ofa, to);
+
+  Trace("sk-manager-skolem")
+      << "skolem: " << k << " purify " << to << std::endl;
   return k;
 }
 
@@ -208,20 +188,23 @@ ProofGenerator* SkolemManager::getProofGenerator(Node t) const
   return nullptr;
 }
 
-Node SkolemManager::getWitnessForm(Node n) { return convertInternal(n, true); }
-
-Node SkolemManager::getSkolemForm(Node n) { return convertInternal(n, false); }
+Node SkolemManager::getWitnessForm(Node k)
+{
+  Assert(k.getKind() == SKOLEM);
+  // simply look up the witness form for k via an attribute
+  WitnessFormAttribute wfa;
+  return k.getAttribute(wfa);
+}
 
-Node SkolemManager::convertInternal(Node n, bool toWitness)
+Node SkolemManager::getOriginalForm(Node n)
 {
   if (n.isNull())
   {
     return n;
   }
-  Trace("sk-manager-debug") << "SkolemManager::convertInternal: " << toWitness
-                            << " " << n << std::endl;
-  WitnessFormAttribute wfa;
-  SkolemFormAttribute sfa;
+  Trace("sk-manager-debug")
+      << "SkolemManager::getOriginalForm " << n << std::endl;
+  OriginalFormAttribute ofa;
   NodeManager* nm = NodeManager::currentNM();
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
@@ -236,13 +219,9 @@ Node SkolemManager::convertInternal(Node n, bool toWitness)
 
     if (it == visited.end())
     {
-      if (toWitness && cur.hasAttribute(wfa))
-      {
-        visited[cur] = cur.getAttribute(wfa);
-      }
-      else if (!toWitness && cur.hasAttribute(sfa))
+      if (cur.hasAttribute(ofa))
       {
-        visited[cur] = cur.getAttribute(sfa);
+        visited[cur] = cur.getAttribute(ofa);
       }
       else
       {
@@ -283,24 +262,7 @@ Node SkolemManager::convertInternal(Node n, bool toWitness)
       {
         ret = nm->mkNode(cur.getKind(), children);
       }
-      if (toWitness)
-      {
-        cur.setAttribute(wfa, ret);
-      }
-      else
-      {
-        // notice that WITNESS terms t may be assigned a skolem form that is
-        // of kind WITNESS here, if t contains a free variable. This is due to
-        // the fact that witness terms in the bodies of quantified formulas are
-        // not eliminated and thus may appear in places where getSkolemForm is
-        // 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. We use an assertion to check that this is
-        // indeed the case.
-        Assert(cur.getKind() != WITNESS || expr::hasFreeVar(cur));
-        cur.setAttribute(sfa, ret);
-      }
+      cur.setAttribute(ofa, ret);
       visited[cur] = ret;
     }
   } while (!visit.empty());
@@ -310,36 +272,22 @@ Node SkolemManager::convertInternal(Node n, bool toWitness)
   return visited[n];
 }
 
-void SkolemManager::convertToWitnessFormVec(std::vector<Node>& vec)
+Node SkolemManager::mkSkolemInternal(Node w,
+                                     const std::string& prefix,
+                                     const std::string& comment,
+                                     int flags)
 {
-  for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
-  {
-    vec[i] = getWitnessForm(vec[i]);
-  }
-}
-void SkolemManager::convertToSkolemFormVec(std::vector<Node>& vec)
-{
-  for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
-  {
-    vec[i] = getSkolemForm(vec[i]);
-  }
-}
-
-Node SkolemManager::getOrMakeSkolem(Node w,
-                                    const std::string& prefix,
-                                    const std::string& comment,
-                                    int flags)
-{
-  Assert(w.getKind() == WITNESS);
+  // note that witness, original forms are independent, but share skolems
+  NodeManager* nm = NodeManager::currentNM();
+  // w is not necessarily a witness term
   SkolemFormAttribute sfa;
+  Node k;
   // could already have a skolem if we used w already
   if (w.hasAttribute(sfa))
   {
     return w.getAttribute(sfa);
   }
-  NodeManager* nm = NodeManager::currentNM();
   // make the new skolem
-  Node k;
   if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR)
   {
     Assert (w.getType().isBoolean());
@@ -349,9 +297,6 @@ Node SkolemManager::getOrMakeSkolem(Node w,
   {
     k = nm->mkSkolem(prefix, w.getType(), comment, flags);
   }
-  // set witness form attribute for k
-  WitnessFormAttribute wfa;
-  k.setAttribute(wfa, w);
   // set skolem form attribute for w
   w.setAttribute(sfa, k);
   Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 6e44db263..1a78bfc83 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -32,9 +32,30 @@ class ProofGenerator;
  * predicate that the introduced variable is intended to witness.
  *
  * It is implemented by mapping terms to an attribute corresponding to their
- * "witness form" as described below. Hence, this class does not impact the
- * reference counting of skolem variables which may be deleted if they are not
- * used.
+ * "original form" and "witness form" as described below. Hence, this class does
+ * not impact the reference counting of skolem variables which may be deleted if
+ * they are not used.
+ *
+ * We distinguish two kinds of mappings between terms and skolems:
+ *
+ * (1) "Original form", which associates skolems with the terms they purify.
+ * This is used in mkPurifySkolem below.
+ *
+ * (2) "Witness form", which associates skolems with their formal definition
+ * as a witness term. This is used in mkSkolem below.
+ *
+ * It is possible to unify these so that purification skolems for t are skolems
+ * whose witness form is (witness ((x T)) (= x t)). However, there are
+ * motivations not to do so. In particular, witness terms in most contexts
+ * should be seen as black boxes, converting something to witness form may have
+ * unintended consequences e.g. variable shadowing. In contrast, converting to
+ * original form does not have these complications. Furthermore, having original
+ * form greatly simplifies reasoning in the proof, in particular, it avoids the
+ * need to reason about identifiers for introduced variables x.
+ *
+ * Furthermore, note that original form and witness form may share skolems
+ * in the rare case that a witness term is purified. This is currently only the
+ * case for algorithms that introduce witness, e.g. BV/set instantiation.
  */
 class SkolemManager
 {
@@ -110,10 +131,13 @@ class SkolemManager
    * returns:
    *   (P w1 w2)
    * where w1 and w2 are skolems with witness forms:
-   *   (witness ((x Int)) (exists ((y' Int)) (P x y')))
+   *   (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
+   * Notice that y is *not* renamed in the witness form of w1. This is not
+   * necessary since w1 is skolem. Although its witness form contains
+   * quantification on y, we never construct a term where the witness form
+   * of w1 is expanded in the witness form of w2. This avoids variable
    * shadowing.
    *
    * In contrast to mkSkolem, the proof generator is for the *entire*
@@ -161,39 +185,33 @@ class SkolemManager
    */
   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
-   * used by the proof checker only.
+   * Convert to witness form, which gets the witness form of a skolem k.
+   * Notice this method is *not* recursive, instead, it is a simple attribute
+   * lookup.
    *
-   * @param n The term or formula to convert to witness form described above
-   * @return n in witness form.
+   * @param k The variable to convert to witness form described above
+   * @return k in witness form.
    */
-  static Node getWitnessForm(Node n);
+  static Node getWitnessForm(Node k);
   /**
-   * Convert to Skolem form, which recursively replaces all witness terms in n
-   * by their corresponding Skolems.
+   * Convert to original form, which recursively replaces all skolems terms in n
+   * by the term they purify.
    *
-   * @param n The term or formula to convert to Skolem form described above
-   * @return n in Skolem form.
+   * @param n The term or formula to convert to original form described above
+   * @return n in original form.
    */
-  static Node getSkolemForm(Node n);
-  /** convert to witness form vector */
-  static void convertToWitnessFormVec(std::vector<Node>& vec);
-  /** convert to Skolem form vector */
-  static void convertToSkolemFormVec(std::vector<Node>& vec);
+  static Node getOriginalForm(Node n);
 
  private:
   /**
    * Mapping from witness terms to proof generators.
    */
   std::map<Node, ProofGenerator*> d_gens;
-  /** Convert to witness or skolem form */
-  static Node convertInternal(Node n, bool toWitness);
-  /** Get or make skolem attribute for witness term w */
-  static Node getOrMakeSkolem(Node w,
-                              const std::string& prefix,
-                              const std::string& comment,
-                              int flags);
+  /** Get or make skolem attribute for term w, which may be a witness term */
+  static Node mkSkolemInternal(Node w,
+                               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: