Make theory preprocess rewrite equalities a preprocessing pass (#5711)

Some theories rewrite equalities during ppRewrite. An example is arithmetic with the option arith-rewrite-eq, which rewrites (= x y) to (and (>= x y) (<= x y)) during theory preprocessing.

This PR makes it so that ppRewrite is only called on equalities in preprocessing, during a new preprocessing pass "TheoryRewriteEq". On the other hand, ppRewrite is never called on new equalities generated in lemmas from TheoryEngine.

In detail, the motivation for this change:

(1) Rewriting equalities during ppRewrite is dangerous since it may break invariants wrt theory combination. In particular, equalities in splitting lemmas originating from theory combination must not be theory-preprocessed, or else we may be non-terminating or solution unsound. This can happen if a theory requests a split on (= x y) but is not notified of this atom when another theory rewrites (= x y) during ppRewrite.

(2) After this PR, we can simplify our policy for all lemmas generated, in particular, we can say that all lemmas must be theory preprocessed before their literals are asserted to TheoryEngine. This is now possible as the invariant cannot be broken (theoryRewriteEq is relegated to the preprocessor, which is only applied once). This will make LemmaProperty::PREPROCESS obsolete, which in turn will simplify several lemma caches for nonlinear and quantifiers. It will also significantly simplify proof production for the theory preprocessor (which maintains two stacks of utilities for preprocessed vs non-preprocessed lemmas).

(3) Simplifications to the above policy will make it significantly easier to implement theory-preprocessing apply when literals are asserted. It is currently not possible to implement this in a coherent way without tracking which literals were a part of lemmas marked as "do not theory-preprocess".

1 files changed, 14 insertions, 9 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 6256360e4..a9783c19c 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -721,15 +721,20 @@ class Theory {
                                   TrustSubstitutionMap& outSubstitutions);
 
   /**
-   * Given an atom of the theory coming from the input formula, this
-   * method can be overridden in a theory implementation to rewrite
-   * the atom into an equivalent form.  This is only called just
-   * before an input atom to the engine. This method returns a TrustNode of
-   * kind TrustNodeKind::REWRITE, which carries information about the proof
-   * generator for the rewrite. Similarly to expandDefinition, this method may
-   * return the null TrustNode if atom is unchanged.
-   */
-  virtual TrustNode ppRewrite(TNode atom) { return TrustNode::null(); }
+   * Given a term of the theory coming from the input formula or
+   * from a lemma generated during solving, this method can be overridden in a
+   * theory implementation to rewrite the term into an equivalent form.
+   *
+   * This method returns a TrustNode of kind TrustNodeKind::REWRITE, which
+   * carries information about the proof generator for the rewrite, which can
+   * be the null TrustNode if n is unchanged.
+   *
+   * Notice this method is used both in the "theory rewrite equalities"
+   * 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.
+   */
+  virtual TrustNode ppRewrite(TNode n) { return TrustNode::null(); }
 
   /**
    * Notify preprocessed assertions. Called on new assertions after