From f2260d959da23069c3ba7889e713eabf8a42d353 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Oct 2025 18:01:41 +0200 Subject: [PATCH] test Signed-off-by: Nikolaj Bjorner --- src/ast/converters/expr_inverter.cpp | 23 ++++++++++++++++++----- src/ast/rewriter/th_rewriter.cpp | 7 ++++++- 2 files changed, 24 insertions(+), 6 deletions(-) diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp index 324b3657c..7a1861fb0 100644 --- a/src/ast/converters/expr_inverter.cpp +++ b/src/ast/converters/expr_inverter.cpp @@ -828,16 +828,28 @@ class finite_set_inverter : public iexpr_inverter { public: finite_set_inverter(ast_manager& m): iexpr_inverter(m), fs(m) {} + family_id get_fid() const override { return fs.get_family_id(); } + 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 + // x union y -> x + // y := x if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) { - mk_fresh_uncnstr_var_for(f, r); + r = args[0]; if (m_mc) { - add_def(args[0], r); - add_def(args[1], fs.mk_empty(args[1]->get_sort())); + add_def(args[1], r); + } + return true; + } + return false; + case OP_FINITE_SET_INTERSECT: + // x intersect y -> x + // y := x + if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) { + r = args[0]; + if (m_mc) { + add_def(args[1], r); } return true; } @@ -1001,6 +1013,7 @@ expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) { add(alloc(basic_expr_inverter, m, *this)); add(alloc(seq_expr_inverter, m)); //add(alloc(pb_expr_inverter, m)); + add(alloc(finite_set_inverter, m)); } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index f35d666d6..b5a96612c 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -30,6 +30,7 @@ Notes: #include "ast/rewriter/pb_rewriter.h" #include "ast/rewriter/recfun_rewriter.h" #include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/finite_set_rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/var_subst.h" #include "ast/rewriter/der.h" @@ -55,6 +56,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { seq_rewriter m_seq_rw; char_rewriter m_char_rw; recfun_rewriter m_rec_rw; + finite_set_rewriter m_fs_rw; arith_util m_a_util; bv_util m_bv_util; der m_der; @@ -229,6 +231,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return m_char_rw.mk_app_core(f, num, args, result); if (fid == m_rec_rw.get_fid()) return m_rec_rw.mk_app_core(f, num, args, result); + if (fid == m_fs_rw.get_fid()) + return m_fs_rw.mk_app_core(f, num, args, result); return BR_FAILED; } @@ -882,7 +886,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_pb_rw(m), m_seq_rw(m, p), m_char_rw(m), - m_rec_rw(m), + m_rec_rw(m), + m_fs_rw(m), m_a_util(m), m_bv_util(m), m_der(m),