From d847a28589ad272960864c88aa7c8ed5f191a269 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Oct 2025 05:51:42 +0100 Subject: [PATCH] bug fixes Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- src/ast/ast.cpp | 20 +----- src/ast/ast.h | 2 +- src/ast/finite_set_decl_plugin.cpp | 4 +- src/ast/finite_set_decl_plugin.h | 11 ++- src/ast/rewriter/finite_set_axioms.cpp | 20 +++--- src/ast/rewriter/finite_set_rewriter.cpp | 42 ++++++++++- src/ast/rewriter/finite_set_rewriter.h | 2 + src/ast/rewriter/th_rewriter.cpp | 2 + src/smt/theory_finite_set.cpp | 89 ++++++++++++------------ 10 files changed, 118 insertions(+), 76 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index bade9c7bf..6502dc147 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -843,7 +843,7 @@ class FuncDeclRef(AstRef): elif k == Z3_PARAMETER_RATIONAL: result[i] = Z3_get_decl_rational_parameter(self.ctx_ref(), self.ast, i) elif k == Z3_PARAMETER_SYMBOL: - result[i] = Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i) + result[i] = _symbol2py(ctx, Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i)) elif k == Z3_PARAMETER_SORT: result[i] = SortRef(Z3_get_decl_sort_parameter(self.ctx_ref(), self.ast, i), ctx) elif k == Z3_PARAMETER_AST: diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index bff812ec4..0d1f493ec 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3338,26 +3338,12 @@ proof * ast_manager::mk_th_lemma( if (proofs_disabled()) return nullptr; - 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())) - args.push_back(to_expr(p.get_ast())); - else if (p.is_rational()) { - arith_util autil(*this); - args.push_back(autil.mk_real(p.get_rational())); - } - } - pr = mk_app(get_family_name(tid), args.size(), args.data(), mk_proof_sort()); - args.reset(); + for (unsigned i = 0; i < num_params; ++i) + parameters.push_back(params[i]); + ptr_buffer args; args.append(num_proofs, (expr**) proofs); - args.push_back(pr.get()); args.push_back(fact); return mk_app(basic_family_id, PR_TH_LEMMA, parameters.size(), parameters.data(), args.size(), args.data()); } diff --git a/src/ast/ast.h b/src/ast/ast.h index b9562c5e4..9dd564206 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2328,7 +2328,7 @@ public: unsigned get_num_parents(proof const * p) const { SASSERT(is_proof(p)); unsigned n = p->get_num_args(); - return p->get_decl()->get_decl_kind() == PR_TH_LEMMA ? n - 2 : !has_fact(p) ? n : n - 1; + return !has_fact(p) ? n : n - 1; } proof * get_parent(proof const * p, unsigned idx) const { SASSERT(is_proof(p)); return to_app(p->get_arg(idx)); } proof * mk_true_proof(); diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 388e85d4f..70cd5e66f 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -70,7 +70,7 @@ void finite_set_decl_plugin::init() { m_sigs[OP_FINITE_SET_MAP] = alloc(polymorphism::psig, m, "set.map", 2, 2, arrABsetA, setB); m_sigs[OP_FINITE_SET_FILTER] = alloc(polymorphism::psig, m, "set.filter", 1, 2, arrABoolsetA, setA); m_sigs[OP_FINITE_SET_RANGE] = alloc(polymorphism::psig, m, "set.range", 0, 2, intintT, setInt); - m_sigs[OP_FINITE_SET_DIFF] = alloc(polymorphism::psig, m, "set.diff", 1, 2, setAsetA, A); + m_sigs[OP_FINITE_SET_EXT] = alloc(polymorphism::psig, m, "set.diff", 1, 2, setAsetA, A); // m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A); } @@ -179,7 +179,7 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param case OP_FINITE_SET_MAP: case OP_FINITE_SET_FILTER: case OP_FINITE_SET_RANGE: - case OP_FINITE_SET_DIFF: + case OP_FINITE_SET_EXT: return mk_finite_set_op(k, arity, domain, range); default: return nullptr; diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index 1c43d0dd0..6756b140a 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -47,7 +47,7 @@ enum finite_set_op_kind { OP_FINITE_SET_MAP, OP_FINITE_SET_FILTER, OP_FINITE_SET_RANGE, - OP_FINITE_SET_DIFF, + OP_FINITE_SET_EXT, OP_FINITE_SET_MAP_INVERSE, LAST_FINITE_SET_OP }; @@ -154,6 +154,11 @@ public: ast_manager& get_manager() const { return m_manager; } + sort *mk_finite_set_sort(sort *elem_sort) { + parameter param(elem_sort); + return m_manager.mk_sort(m_fid, FINITE_SET_SORT, 1, ¶m); + } + app * mk_empty(sort* set_sort) { parameter param(set_sort); return m_manager.mk_app(m_fid, OP_FINITE_SET_EMPTY, 1, ¶m, 0, nullptr); @@ -175,6 +180,10 @@ public: return m_manager.mk_app(m_fid, OP_FINITE_SET_DIFFERENCE, s1, s2); } + app *mk_ext(expr *s1, expr *s2) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_EXT, s1, s2); + } + app * mk_in(expr* elem, expr* set) { return m_manager.mk_app(m_fid, OP_FINITE_SET_IN, elem, set); } diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index 4bf29c087..7e3adc0ed 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -27,7 +27,10 @@ Revision History: std::ostream& operator<<(std::ostream& out, theory_axiom const& ax) { - return out << "axiom"; + auto &m = ax.clause.get_manager(); + for (auto e : ax.clause) + out << mk_pp(e, m) << " "; + return out; } // a ~ set.empty => not (x in a) @@ -36,7 +39,8 @@ void finite_set_axioms::in_empty_axiom(expr *x) { // Generate: not (x in empty_set) // where empty_set is the empty set of x's type sort* elem_sort = x->get_sort(); - expr_ref empty_set(u.mk_empty(elem_sort), m); + sort *set_sort = u.mk_finite_set_sort(elem_sort); + expr_ref empty_set(u.mk_empty(set_sort), m); expr_ref x_in_empty(u.mk_in(x, empty_set), m); theory_axiom* ax = alloc(theory_axiom, m, "in-empty", x); @@ -357,7 +361,7 @@ void finite_set_axioms::subset_axiom(expr* a) { void finite_set_axioms::extensionality_axiom(expr *a, expr* b) { // a != b => set.in (set.diff(a, b) a) != set.in (set.diff(a, b) b) - expr_ref diff_ab(u.mk_difference(a, b), m); + expr_ref diff_ab(u.mk_ext(a, b), m); expr_ref a_eq_b(m.mk_eq(a, b), m); expr_ref diff_in_a(u.mk_in(diff_ab, a), m); @@ -370,9 +374,9 @@ void finite_set_axioms::extensionality_axiom(expr *a, expr* b) { ax->clause.push_back(m.mk_not(diff_in_b)); m_add_clause(ax); - theory_axiom* ax2 = alloc(theory_axiom, m, "extensionality", a, b); - ax2->clause.push_back(m.mk_not(a_eq_b)); - ax2->clause.push_back(diff_in_a); - ax2->clause.push_back(diff_in_b); - m_add_clause(ax2); + ax = alloc(theory_axiom, m, "extensionality", a, b); + ax->clause.push_back(a_eq_b); + ax->clause.push_back(diff_in_a); + ax->clause.push_back(diff_in_b); + m_add_clause(ax); } \ No newline at end of file diff --git a/src/ast/rewriter/finite_set_rewriter.cpp b/src/ast/rewriter/finite_set_rewriter.cpp index 6ca280105..3ce28557d 100644 --- a/src/ast/rewriter/finite_set_rewriter.cpp +++ b/src/ast/rewriter/finite_set_rewriter.cpp @@ -11,7 +11,7 @@ Abstract: Author: - GitHub Copilot Agent 2025 + Nikolaj Bjorner (nbjorner) - October 2025 --*/ @@ -222,6 +222,44 @@ br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result) result = m.mk_eq(elem, singleton_elem); return BR_REWRITE1; } - + // NB we don't rewrite (set.in x (set.union s t)) to (or (set.in x s) (set.in x t)) + // because it creates two new sub-expressions. The expression (set.union s t) could + // be shared with other expressions so the net effect of this rewrite could be to create + // a larger formula for the solver. return BR_FAILED; } + + +/** +* if a, b are set expressions we can create an on-the-fly heap for their min-elements +* a, b are normalized to the form (set.union s t) or (set.empty) where +* s is a singleton or range expression such that every element in t are above s. +* we distinguish numerical values from value expressions: +* - for numerical values we use the ordering over numerals to pick minimal ranges +* - for unique value expressions ranging over non-numerals use expression identifiers +* - for other expressions use identifiers to sort expressions, but make sure to be inconclusive +* for set difference +* We want mk_eq_core to produce a result true/false if the arguments are both (unique) values. +* This allows to evaluate models for being well-formed conclusively. +* +* A way to convert a set expression to a heap is as follows: +* +* min({s}) = {s} u {} +* min({}) = {} +* min([l..u]) = [l..u] u {} +* min(s u t) = +* let range_s u s1 = min(s) +* let range_t u t1 = min(t) +* if range_s < range_t: +* range_s u (t u s1) +* if range_t < range_t: +* range_t u (s u t1) +* if range_t n range_s != {}: +* min(range_t, range_s) u the rest ... +* etc. +*/ + +br_status finite_set_rewriter::mk_eq_core(expr* a, expr* b, expr_ref& result) { + + return BR_FAILED; +} \ No newline at end of file diff --git a/src/ast/rewriter/finite_set_rewriter.h b/src/ast/rewriter/finite_set_rewriter.h index 7586b05ce..21e2158c7 100644 --- a/src/ast/rewriter/finite_set_rewriter.h +++ b/src/ast/rewriter/finite_set_rewriter.h @@ -55,5 +55,7 @@ public: finite_set_util& util() { return m_util; } br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + + br_status mk_eq_core(expr *a, expr *b, expr_ref &result); }; diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index b5a96612c..db03a5f95 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -688,6 +688,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { st = m_ar_rw.mk_eq_core(a, b, result); else if (s_fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_eq_core(a, b, result); + else if (s_fid == m_fs_rw.get_fid()) + st = m_fs_rw.mk_eq_core(a, b, result); if (st != BR_FAILED) return st; st = extended_bv_eq(a, b, result); diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 1900620aa..ef281097a 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -344,6 +344,7 @@ namespace smt { if (u.is_size(e)) has_size = true; } + TRACE(finite_set, tout << "has-map " << has_map << " has-filter-size " << has_filter << has_size << "\n"); if (has_map) return false; // todo use more expensive model check here if (has_filter && has_size) @@ -408,12 +409,12 @@ namespace smt { // walk the watch list and try to find new watches or propagate unsigned j = 0; for (unsigned i = 0; i < m_clauses.watch[idx].size(); ++i) { - TRACE(finite_set, tout << " watch[" << i << "] size: " << m_clauses.watch[i].size() << "\n";); + TRACE(finite_set, tout << "watch[" << i << "] size: " << m_clauses.watch[i].size() << "\n";); auto clause_idx = m_clauses.watch[idx][i]; auto* ax = m_clauses.axioms[clause_idx]; auto &clause = ax->clause; if (any_of(clause, [&](expr *lit) { return ctx.find_assignment(lit) == l_true; })) { - TRACE(finite_set, tout << " satisfied\n";); + TRACE(finite_set, tout << "satisfied\n";); m_clauses.watch[idx][j++] = clause_idx; continue; // clause is already satisfied } @@ -445,7 +446,7 @@ namespace smt { auto litid = 2 * lit->get_id() + litneg; m_clauses.watch.reserve(litid + 1); m_clauses.watch[litid].push_back(clause_idx); - TRACE(finite_set, tout << " new watch for " << mk_pp(lit, m) << "\n";); + TRACE(finite_set, tout << "new watch for " << mk_pp(lit, m) << "\n";); found_swap = true; break; } @@ -454,7 +455,7 @@ namespace smt { // either all literals are false, or the other watch literal is propagating. m_clauses.squeue.push_back(clause_idx); ctx.push_trail(push_back_vector(m_clauses.squeue)); - TRACE(finite_set, tout << " propagate clause\n";); + TRACE(finite_set, tout << "propagate clause\n";); m_clauses.watch[idx][j++] = clause_idx; ++i; for (; i < m_clauses.watch[idx].size(); ++i) @@ -630,39 +631,44 @@ namespace smt { void theory_finite_set::add_membership_axioms(expr *elem, expr *set) { TRACE(finite_set, tout << "add_membership_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); - if (!is_new_axiom(elem, set)) - return; - - // Instantiate appropriate axiom based on set structure - if (u.is_empty(set)) { - m_axioms.in_empty_axiom(elem); + try { + // Instantiate appropriate axiom based on set structure + if (!is_new_axiom(elem, set)) + ; + else if (u.is_empty(set)) { + m_axioms.in_empty_axiom(elem); + } + else if (u.is_singleton(set)) { + m_axioms.in_singleton_axiom(elem, set); + } + else if (u.is_union(set)) { + m_axioms.in_union_axiom(elem, set); + } + else if (u.is_intersect(set)) { + m_axioms.in_intersect_axiom(elem, set); + } + else if (u.is_difference(set)) { + m_axioms.in_difference_axiom(elem, set); + } + else if (u.is_range(set)) { + m_axioms.in_range_axiom(elem, set); + } + else if (u.is_map(set)) { + m_axioms.in_map_axiom(elem, set); + m_axioms.in_map_image_axiom(elem, set); + } + else if (u.is_filter(set)) { + m_axioms.in_filter_axiom(elem, set); + } + } catch (...) { + TRACE(finite_set, tout << "exception\n"); + throw; } - else if (u.is_singleton(set)) { - m_axioms.in_singleton_axiom(elem, set); - } - else if (u.is_union(set)) { - m_axioms.in_union_axiom(elem, set); - } - else if (u.is_intersect(set)) { - m_axioms.in_intersect_axiom(elem, set); - } - else if (u.is_difference(set)) { - m_axioms.in_difference_axiom(elem, set); - } - else if (u.is_range(set)) { - m_axioms.in_range_axiom(elem, set); - } - else if (u.is_map(set)) { - m_axioms.in_map_axiom(elem, set); - m_axioms.in_map_image_axiom(elem, set); - } - else if (u.is_filter(set)) { - m_axioms.in_filter_axiom(elem, set); - } + TRACE(finite_set, tout << "after add_membership_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); } void theory_finite_set::add_clause(theory_axiom* ax) { - TRACE(finite_set, tout << "add_clause: " << ax << "\n"); + TRACE(finite_set, tout << "add_clause: " << *ax << "\n"); ctx.push_trail(push_back_vector(m_clauses.axioms)); ctx.push_trail(new_obj_trail(ax)); m_clauses.axioms.push_back(ax); @@ -933,7 +939,7 @@ namespace smt { } if (undef_count == 1) { - TRACE(finite_set, tout << " propagate unit: " << mk_pp(unit, m) << "\n" << clause << "\n";); + TRACE(finite_set, tout << "propagate unit: " << mk_pp(unit, m) << "\n" << clause << "\n";); auto lit = mk_literal(unit); literal_vector antecedent; for (auto e : clause) { @@ -951,15 +957,10 @@ namespace smt { // only propagations that are processed by conflict resolution. // this misses conflicts at base level. proof_ref pr(m); - expr_ref_vector args(m); - for (auto const &p : ax->params) { - if (p.is_ast()) - args.push_back(to_expr(p.get_ast())); - else - args.push_back(m.mk_const(p.get_symbol(), m.mk_proof_sort())); - } - - pr = m.mk_app(m.get_family_name(get_family_id()), args.size(), args.data(), m.mk_proof_sort()); + proof_ref_vector args(m); + for (auto a : antecedent) + args.push_back(m.mk_hypothesis(ctx.literal2expr(a))); + pr = m.mk_th_lemma(get_id(), unit, args.size(), args.data(), ax->params.size(), ax->params.data()); justification_proof_wrapper jp(ctx, pr.get(), false); ctx.get_clause_proof().propagate(lit, &jp, antecedent); jp.del_eh(m); @@ -972,7 +973,7 @@ namespace smt { m_stats.m_num_axioms_conflicts++; else m_stats.m_num_axioms_case_splits++; - TRACE(finite_set, tout << " assert " << (is_conflict ? "conflict" : "case split") << clause << "\n";); + TRACE(finite_set, tout << "assert " << (is_conflict ? "conflict" : "case split") << clause << "\n";); literal_vector lclause; for (auto e : clause) lclause.push_back(mk_literal(e));