From 237891c901ef3a49ed5c64e9b6bc6a616b44dde3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 13 Aug 2025 10:24:36 -0700
Subject: [PATCH] updates to euf completion

---
 src/ast/euf/euf_arith_plugin.cpp       | 26 ++++++++++++++++++++++++++
 src/ast/simplifiers/euf_completion.cpp |  5 +++++
 2 files changed, 31 insertions(+)

diff --git a/src/ast/euf/euf_arith_plugin.cpp b/src/ast/euf/euf_arith_plugin.cpp
index df9207a3b..487cc1392 100644
--- a/src/ast/euf/euf_arith_plugin.cpp
+++ b/src/ast/euf/euf_arith_plugin.cpp
@@ -56,6 +56,32 @@ namespace euf {
         TRACE(plugin, tout << g.bpp(n) << "\n");
         m_add.register_node(n);
         m_mul.register_node(n);
+        expr* e = n->get_expr(), * x, * y;
+        // x - y = x + (* -1 y)
+        if (a.is_sub(e, x, y)) {
+            auto& m = g.get_manager();
+            auto e1 = a.mk_numeral(rational(-1), a.is_int(x));
+            auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
+            auto e2 = a.mk_mul(e1, y);
+            enode* es1[2] = { n1, g.find(y)};
+            auto mul = g.find(e2) ? g.find(e2) : g.mk(e2, 0, 2, es1);
+            enode* es2[2] = { g.find(x), mul };
+            expr* e_add = a.mk_add(x, e2);
+            auto add = g.find(e_add) ? g.find(e_add): g.mk(e_add, 0, 2, es2);
+            push_merge(n, add);
+        }
+        // c1 * c2 = c1*c2
+        rational r1, r2;
+        if (a.is_mul(e, x, y) && a.is_numeral(x, r1) && a.is_numeral(y, r2)) {
+            rational r = r1 * r2;
+            auto e1 = a.mk_numeral(r, a.is_int(x));
+            auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
+            push_merge(n, n1);
+        }
+        if (a.is_uminus(e, x)) {
+            NOT_IMPLEMENTED_YET();
+        }
+
     }
 
     void arith_plugin::merge_eh(enode* n1, enode* n2) {
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 1a32a1bd5..cea801ae7 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -359,6 +359,11 @@ namespace euf {
             IF_VERBOSE(1, verbose_stream() << "not: " << nf << "\n");
         }
         else {
+            expr_ref f1(f, m);
+            if (!m.is_implies(f) && !is_quantifier(f)) {
+                m_rewriter(f1);
+                f = f1;
+            }
             enode* n = mk_enode(f);
             if (m.is_true(n->get_root()->get_expr()))
                 return;