(proof-new) Update ppRewrite to use skolem lemmas (#6102)

This is required for proofs. The internal calculus no longer uses witness forms for reasoning, and hence we cannot return witness terms in ppRewrite. This is required to fix a debug failure, as well as making life easier on external proof conversions.

As a result of this PR, for example, given (P a) as input to ppRewrite, previous we returned:

(P (witness ((x T)) (A x)))

now we return:

(P k), with skolem lemma ( (A k), k )

Followup PRs will remove the use of WITNESS in ppRewrite (e.g. in sets and strings); this PR modifies arithmetic to not return WITNESS in response to ppRewrite.

1 files changed, 15 insertions, 3 deletions

diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index c6f961129..100116fd7 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -479,9 +479,21 @@ Node OperatorElim::mkWitnessTerm(Node v,
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
   // we mark that we should send a lemma
-  Node k = sm->mkSkolem(
-      v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this, true);
-  // TODO: (project #37) add to lems
+  Node k =
+      sm->mkSkolem(v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this);
+  TNode tv = v;
+  TNode tk = k;
+  Node lem = pred.substitute(tv, tk);
+  if (d_pnm != nullptr)
+  {
+    TrustNode tlem =
+        mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem});
+    lems.push_back(SkolemLemma(tlem, k));
+  }
+  else
+  {
+    lems.push_back(SkolemLemma(TrustNode::mkTrustLemma(lem), k));
+  }
   return k;
 }