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

1 files changed, 45 insertions, 27 deletions

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: