From cb814732603b584511b49a759fe5c99d3627bdb7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 18 Feb 2023 17:54:26 -0800
Subject: [PATCH] add destructive equality resolution to the main simplifier.

---
 src/ast/rewriter/der.cpp         |  5 +++--
 src/ast/rewriter/th_rewriter.cpp | 12 ++++++++++++
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp
index fd79529f9..0e28cf6f6 100644
--- a/src/ast/rewriter/der.cpp
+++ b/src/ast/rewriter/der.cpp
@@ -197,9 +197,10 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
 
         m_pos2var.reserve(num_args, -1);
 
-        // Find all disequalities
+        // Find all equalities/disequalities
         for (unsigned i = 0; i < num_args; i++) {
-            is_eq = is_forall(q) ? is_var_diseq(literals.get(i), num_decls, v, t) : is_var_eq(literals.get(i), num_decls, v, t);
+            expr* arg = literals.get(i);
+            is_eq = is_forall(q) ? is_var_diseq(arg, num_decls, v, t) : is_var_eq(arg, num_decls, v, t);
             if (is_eq) {
                 unsigned idx = v->get_idx();
                 if (m_map.get(idx, nullptr) == nullptr) {
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index c6ab22636..c57d3aabc 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -31,6 +31,7 @@ Notes:
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/der.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/expr_substitution.h"
 #include "ast/ast_smt2_pp.h"
@@ -54,6 +55,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     recfun_rewriter     m_rec_rw;
     arith_util          m_a_util;
     bv_util             m_bv_util;
+    der                 m_der;
     expr_safe_replace   m_rep;
     expr_ref_vector     m_pinned;
       // substitution support
@@ -819,6 +821,15 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             result_pr = m().mk_transitivity(p1, p2);
         }
 
+        if (is_quantifier(result)) {
+            proof_ref p2(m());
+            expr_ref r(m());
+            m_der(to_quantifier(result), r, p2);
+            if (m().proofs_enabled() && result.get() != r.get()) 
+                result_pr = m().mk_transitivity(result_pr, p2);
+            result = r;
+        }
+
         TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << " " << result_pr << "\n" ;);
 
         SASSERT(old_q->get_sort() == result->get_sort());
@@ -839,6 +850,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_rec_rw(m),
         m_a_util(m),
         m_bv_util(m),
+        m_der(m),
         m_rep(m),
         m_pinned(m),
         m_used_dependencies(m) {