Updates to theory preprocess equality (#5776)

This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.

For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.

The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.

1 files changed, 9 insertions, 6 deletions

diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp
index 190b33684..68de75194 100644
--- a/src/preprocessing/passes/theory_rewrite_eq.cpp
+++ b/src/preprocessing/passes/theory_rewrite_eq.cpp
@@ -59,13 +59,9 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
 
     if (it == visited.end())
     {
-      // don't consider Boolean equality
-      if (cur.getKind() == kind::EQUAL && !cur[0].getType().isBoolean())
+      if (cur.getNumChildren()==0)
       {
-        // For example, (= x y) ---> (and (>= x y) (<= x y))
-        theory::TrustNode trn = te->ppRewriteEquality(cur);
-        // can make proof producing by using proof generator from trn
-        visited[cur] = trn.isNull() ? Node(cur) : trn.getNode();
+        visited[cur] = cur;
       }
       else
       {
@@ -95,6 +91,13 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
       {
         ret = nm->mkNode(cur.getKind(), children);
       }
+      if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean())
+      {
+        // For example, (= x y) ---> (and (>= x y) (<= x y))
+        theory::TrustNode trn = te->ppRewriteEquality(ret);
+        // can make proof producing by using proof generator from trn
+        ret = trn.isNull() ? Node(ret) : trn.getNode();
+      }
       visited[cur] = ret;
     }
   } while (!visit.empty());