(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, 18 insertions, 16 deletions

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))