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

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 3278c8187..68a2e1436 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -32,6 +32,7 @@
 #include "theory/assertion.h"
 #include "theory/care_graph.h"
 #include "theory/logic_info.h"
+#include "theory/skolem_lemma.h"
 #include "theory/theory_id.h"
 #include "theory/trust_node.h"
 #include "theory/valuation.h"
@@ -730,8 +731,22 @@ class Theory {
    * preprocessing pass, where n is an equality from the input formula,
    * and in theory preprocessing, where n is a (non-equality) term occurring
    * in the input or generated in a lemma.
+   *
+   * @param n the node to preprocess-rewrite.
+   * @param lems a set of lemmas that should be added as a consequence of
+   * preprocessing n. These are in the form of "skolem lemmas". For example,
+   * calling this method on (div x n), we return a trust node proving:
+   *   (= (div x n) k_div)
+   * for fresh skolem k, and add the skolem lemma for k that indicates that
+   * it is the division of x and n.
+   *
+   * Note that ppRewrite should not return WITNESS terms, since the internal
+   * calculus works in "original forms" and not "witness forms".
    */
-  virtual TrustNode ppRewrite(TNode n) { return TrustNode::null(); }
+  virtual TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
+  {
+    return TrustNode::null();
+  }
 
   /**
    * Notify preprocessed assertions. Called on new assertions after