(proof-new) Clean up uses of witness with skolem lemmas (#6109)

This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy.

It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.

1 files changed, 16 insertions, 4 deletions

diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h
index a44d5a30d..c669b527d 100644
--- a/src/theory/skolem_lemma.h
+++ b/src/theory/skolem_lemma.h
@@ -36,14 +36,26 @@ namespace theory {
 class SkolemLemma
 {
  public:
-  SkolemLemma(TrustNode lem, Node k) : d_lemma(lem), d_skolem(k)
-  {
-    Assert(lem.getKind() == TrustNodeKind::LEMMA);
-  }
+  /**
+   * Make skolem from trust node lem of kind LEMMA and skolem k.
+   */
+  SkolemLemma(TrustNode lem, Node k);
+  /**
+   * Make skolem lemma from witness form of skolem k. If non-null, pg is
+   * proof generator that can generator a proof for getSkolemLemmaFor(k).
+   */
+  SkolemLemma(Node k, ProofGenerator* pg);
+
   /** The lemma, a trust node of kind LEMMA */
   TrustNode d_lemma;
   /** The skolem associated with that lemma */
   Node d_skolem;
+
+  /**
+   * Get the lemma for skolem k based on its witness form. If k has witness
+   * form (witness ((x T)) (P x)), this is the formula (P k).
+   */
+  static Node getSkolemLemmaFor(Node k);
 };
 
 }  // namespace theory