From b96624727d825746504539dde92e84519e276d19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Oct 2025 09:42:25 +0200 Subject: [PATCH] remove ad-hoc membership axioms, enable boundary point saturatino Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 5 ++++- src/ast/rewriter/finite_set_axioms.cpp | 11 +---------- src/smt/theory_finite_set.cpp | 2 +- 3 files changed, 6 insertions(+), 12 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 4c5703b0b..c0fa954ff 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3340,8 +3340,11 @@ proof * ast_manager::mk_th_lemma( proof_ref pr(*this); ptr_buffer args; + vector parameters; + parameters.push_back(parameter(get_family_name(tid))); for (unsigned i = 0; i < num_params; ++i) { auto const &p = params[i]; + parameters.push_back(p); if (p.is_symbol()) args.push_back(mk_app(p.get_symbol(), 0, nullptr, mk_proof_sort())); else if (p.is_ast() && is_expr(p.get_ast())) @@ -3356,7 +3359,7 @@ proof * ast_manager::mk_th_lemma( args.push_back(pr.get()); args.append(num_proofs, (expr**) proofs); args.push_back(fact); - return mk_app(basic_family_id, PR_TH_LEMMA, 0, nullptr, args.size(), args.data()); + return mk_app(basic_family_id, PR_TH_LEMMA, parameters.size(), parameters.data(), args.size(), args.data()); } proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl, diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index db7739f5e..0f020cbd1 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -175,22 +175,13 @@ void finite_set_axioms::in_singleton_axiom(expr* a) { if (!u.is_singleton(a, b)) return; - arith_util arith(m); + expr_ref b_in_a(u.mk_in(b, a), m); auto ax = alloc(theory_axiom, m, "in-singleton"); ax->clause.push_back(b_in_a); m_add_clause(ax); - - ax = alloc(theory_axiom, m, "in-singleton"); - expr_ref bm1_in_a(u.mk_in(arith.mk_add(b, arith.mk_int(-1)), a), m); - ax->clause.push_back(m.mk_not(bm1_in_a)); - m_add_clause(ax); - - ax = alloc(theory_axiom, m, "in-singleton"); - expr_ref bp1_in_a(u.mk_in(arith.mk_add(b, arith.mk_int(1)), a), m); - ax->clause.push_back(m.mk_not(bp1_in_a)); } diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 9ba9882bb..615ef1785 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -282,7 +282,7 @@ namespace smt { if (activate_unasserted_clause()) return FC_CONTINUE; - if (false && activate_range_local_axioms()) + if (activate_range_local_axioms()) return FC_CONTINUE; if (assume_eqs())