From c832802183284b8db3a46559b26ad8efe70903f8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Oct 2025 16:21:33 +0100 Subject: [PATCH] disable tracking literals, they are not used added trivial rewrites for set.size --- src/ast/rewriter/finite_set_rewriter.cpp | 44 +++++++++++++++++++----- src/ast/rewriter/finite_set_rewriter.h | 5 +-- src/smt/theory_finite_set_size.cpp | 9 ++--- 3 files changed, 42 insertions(+), 16 deletions(-) diff --git a/src/ast/rewriter/finite_set_rewriter.cpp b/src/ast/rewriter/finite_set_rewriter.cpp index 3773a6483..6ca280105 100644 --- a/src/ast/rewriter/finite_set_rewriter.cpp +++ b/src/ast/rewriter/finite_set_rewriter.cpp @@ -16,6 +16,7 @@ Author: --*/ #include "ast/rewriter/finite_set_rewriter.h" +#include "ast/arith_decl_plugin.h" br_status finite_set_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_family_id() == get_fid()); @@ -37,6 +38,9 @@ br_status finite_set_rewriter::mk_app_core(func_decl * f, unsigned num_args, exp case OP_FINITE_SET_IN: SASSERT(num_args == 2); return mk_in(args[0], args[1], result); + case OP_FINITE_SET_SIZE: + // Size is already in normal form, no simplifications + return mk_size(args[0], result); default: return BR_FAILED; } @@ -147,26 +151,26 @@ br_status finite_set_rewriter::mk_difference(expr * arg1, expr * arg2, expr_ref br_status finite_set_rewriter::mk_subset(expr * arg1, expr * arg2, expr_ref & result) { // set.subset(x, x) -> true if (arg1 == arg2) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } // set.subset(empty, x) -> true if (m_util.is_empty(arg1)) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } // set.subset(x, empty) -> x = empty if (m_util.is_empty(arg2)) { - result = m().mk_eq(arg1, arg2); + result = m.mk_eq(arg1, arg2); return BR_REWRITE1; } // General case: set.subset(x, y) -> set.intersect(x, y) = x - expr_ref intersect(m()); + expr_ref intersect(m); intersect = m_util.mk_intersect(arg1, arg2); - result = m().mk_eq(intersect, arg1); + result = m.mk_eq(intersect, arg1); return BR_REWRITE3; } @@ -175,10 +179,34 @@ br_status finite_set_rewriter::mk_singleton(expr * arg, expr_ref & result) { return BR_FAILED; } +br_status finite_set_rewriter::mk_size(expr * arg, expr_ref & result) { + arith_util a(m); + if (m_util.is_empty(arg)) { + // size(empty) -> 0 + result = a.mk_int(0); + return BR_DONE; + } + if (m_util.is_singleton(arg)) { + // size(singleton(x)) -> 1 + result = a.mk_int(1); + return BR_DONE; + } + expr *lower, *upper; + if (m_util.is_range(arg, lower, upper)) { + // size(range(a, b)) -> b - a + 1 + expr_ref size_expr(m); + size_expr = a.mk_add(a.mk_sub(upper, lower), a.mk_int(1)); + result = m.mk_ite(a.mk_gt(lower, upper), a.mk_int(0), size_expr); + return BR_REWRITE3; + } + // Size is already in normal form, no simplifications + return BR_FAILED; +} + br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result) { // set.in(x, empty) -> false if (m_util.is_empty(set)) { - result = m().mk_false(); + result = m.mk_false(); return BR_DONE; } @@ -187,11 +215,11 @@ br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result) if (m_util.is_singleton(set, singleton_elem)) { // set.in(x, singleton(x)) -> true (when x is the same) if (elem == singleton_elem) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } // set.in(x, singleton(y)) -> x = y (when x != y) - result = m().mk_eq(elem, singleton_elem); + result = m.mk_eq(elem, singleton_elem); return BR_REWRITE1; } diff --git a/src/ast/rewriter/finite_set_rewriter.h b/src/ast/rewriter/finite_set_rewriter.h index 1dc536946..7586b05ce 100644 --- a/src/ast/rewriter/finite_set_rewriter.h +++ b/src/ast/rewriter/finite_set_rewriter.h @@ -34,6 +34,7 @@ where the signature is defined in finite_set_decl_plugin.h. */ class finite_set_rewriter { friend class finite_set_rewriter_test; + ast_manager &m; finite_set_util m_util; // Rewrite rules for set operations @@ -43,13 +44,13 @@ class finite_set_rewriter { br_status mk_subset(expr *arg1, expr *arg2, expr_ref &result); br_status mk_singleton(expr *arg1, expr_ref &result); br_status mk_in(expr *arg1, expr *arg2, expr_ref &result); + br_status mk_size(expr *arg, expr_ref &result); public: finite_set_rewriter(ast_manager & m, params_ref const & p = params_ref()): - m_util(m) { + m(m), m_util(m) { } - ast_manager & m() const { return m_util.get_manager(); } family_id get_fid() const { return m_util.get_family_id(); } finite_set_util& util() { return m_util; } diff --git a/src/smt/theory_finite_set_size.cpp b/src/smt/theory_finite_set_size.cpp index d1071bc1f..e3b8dd651 100644 --- a/src/smt/theory_finite_set_size.cpp +++ b/src/smt/theory_finite_set_size.cpp @@ -391,17 +391,14 @@ namespace smt { } /** - * Introduce an assumption literal to manage incremental search for solutions + * Placeholder to introduce an assumption literal to manage incremental search for solutions */ void theory_finite_set_size::add_theory_assumptions(expr_ref_vector &assumptions) { - if (m_set_size_decls.empty()) - return; - m_assumption = m.mk_fresh_const(symbol("set.size.solver"), m.mk_bool_sort()); - assumptions.push_back(m_assumption); + } bool theory_finite_set_size::should_research(expr_ref_vector& unsat_core) { - return unsat_core.contains(m_assumption); + return false; } std::ostream& theory_finite_set_size::display(std::ostream& out) {