From 930ba5ebd6bd94bf576aa6968917c89a290ad20f Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Tue, 14 Oct 2025 17:48:40 +0200
Subject: [PATCH] Implement inverter functions for finite-set operators (#7974)

* Initial plan

* Add set operator inverters to array_expr_inverter

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Refactor expr_inverter to remove set operations

Removed handling for set operations like union, intersection, and difference in expr_inverter.cpp. Introduced finite_set_inverter class to manage set union operation.

* Remove OP_SET_COMPLEMENT case from expr_inverter

Removed handling for OP_SET_COMPLEMENT in expr_inverter.

* Change OP_SET_UNION to OP_FINITE_SET_UNION

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/converters/expr_inverter.cpp | 29 ++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
index 63578487e..beb37193b 100644
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@@ -823,6 +823,35 @@ public:
 };
 #endif
 
+class finite_set_inverter : public iexpr_inverter {
+    finite_set_util fs;
+public:
+    finite_set_inverter(ast_manager& m): iexpr_inverter(m), fs(m) {}
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
+        switch (f->get_decl_kind()) {
+        case OP_FINITE_SET_UNION:
+            // x union y -> fresh
+            // x := fresh, y := empty
+            if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                if (m_mc) {
+                    add_def(args[0], r);
+                    add_def(args[1], fs.mk_empty_set(args[1]->get_sort()));
+                }
+                return true;
+            }
+            return false;
+        default:
+            break;
+        }
+        return false;
+    }
+    
+    bool mk_diff(expr* t, expr_ref& r) override {
+        return false;
+    }
+};
 
 class seq_expr_inverter : public iexpr_inverter {
     seq_util seq;