From 75bac9c0cec7bbe1d97586c6ac7a382821311b27 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 14 Oct 2025 17:16:29 +0200 Subject: [PATCH] Implement finite_set_axioms.cpp and fix empty set constructor bug (#7973) * Initial plan * Add finite_set_axioms.cpp implementation and update CMakeLists.txt Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix finite_set_decl_plugin bug and complete implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Use array select instead of function application for map and select axioms Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Simplify range assignment in finite_set_decl_plugin --------- 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 --- src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/finite_set_axioms.cpp | 273 +++++++++++++++++++++++++ 2 files changed, 274 insertions(+) create mode 100644 src/ast/rewriter/finite_set_axioms.cpp diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index ade2dabee..9d529f9b5 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -22,6 +22,7 @@ z3_add_component(rewriter expr_safe_replace.cpp factor_equivs.cpp factor_rewriter.cpp + finite_set_axioms.cpp finite_set_rewriter.cpp fpa_rewriter.cpp func_decl_replace.cpp diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp new file mode 100644 index 000000000..ad78c5956 --- /dev/null +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -0,0 +1,273 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + finite_set_axioms.cpp + +Abstract: + + This module implements axiom schemas that are invoked by saturating constraints + with respect to the semantics of set operations. + +Author: + + GitHub Copilot Agent 2025 + +Revision History: + +--*/ + +#include "ast/ast.h" +#include "ast/finite_set_decl_plugin.h" +#include "ast/arith_decl_plugin.h" +#include "ast/array_decl_plugin.h" +#include "ast/rewriter/finite_set_axioms.h" + +// a ~ set.empty => not (x in a) +// x is an element, generate axiom that x is not in any empty set of x's type +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); + expr_ref x_in_empty(u.mk_in(x, empty_set), m); + + expr_ref_vector clause(m); + clause.push_back(m.mk_not(x_in_empty)); + m_add_clause(clause); +} + +// a := set.union(b, c) +// (x in a) <=> (x in b) or (x in c) +void finite_set_axioms::in_union_axiom(expr *x, expr *a) { + expr* b = nullptr, *c = nullptr; + if (!u.is_union(a, b, c)) + return; + + expr_ref_vector clause(m); + expr_ref x_in_a(u.mk_in(x, a), m); + expr_ref x_in_b(u.mk_in(x, b), m); + expr_ref x_in_c(u.mk_in(x, c), m); + + // (x in a) => (x in b) or (x in c) + expr_ref_vector clause1(m); + clause1.push_back(m.mk_not(x_in_a)); + clause1.push_back(x_in_b); + clause1.push_back(x_in_c); + m_add_clause(clause1); + + // (x in b) => (x in a) + expr_ref_vector clause2(m); + clause2.push_back(m.mk_not(x_in_b)); + clause2.push_back(x_in_a); + m_add_clause(clause2); + + // (x in c) => (x in a) + expr_ref_vector clause3(m); + clause3.push_back(m.mk_not(x_in_c)); + clause3.push_back(x_in_a); + m_add_clause(clause3); +} + +// a := set.intersect(b, c) +// (x in a) <=> (x in b) and (x in c) +void finite_set_axioms::in_intersect_axiom(expr *x, expr *a) { + expr* b = nullptr, *c = nullptr; + if (!u.is_intersect(a, b, c)) + return; + + expr_ref x_in_a(u.mk_in(x, a), m); + expr_ref x_in_b(u.mk_in(x, b), m); + expr_ref x_in_c(u.mk_in(x, c), m); + + // (x in a) => (x in b) + expr_ref_vector clause1(m); + clause1.push_back(m.mk_not(x_in_a)); + clause1.push_back(x_in_b); + m_add_clause(clause1); + + // (x in a) => (x in c) + expr_ref_vector clause2(m); + clause2.push_back(m.mk_not(x_in_a)); + clause2.push_back(x_in_c); + m_add_clause(clause2); + + // (x in b) and (x in c) => (x in a) + expr_ref_vector clause3(m); + clause3.push_back(m.mk_not(x_in_b)); + clause3.push_back(m.mk_not(x_in_c)); + clause3.push_back(x_in_a); + m_add_clause(clause3); +} + +// a := set.difference(b, c) +// (x in a) <=> (x in b) and not (x in c) +void finite_set_axioms::in_difference_axiom(expr *x, expr *a) { + expr* b = nullptr, *c = nullptr; + if (!u.is_difference(a, b, c)) + return; + + expr_ref x_in_a(u.mk_in(x, a), m); + expr_ref x_in_b(u.mk_in(x, b), m); + expr_ref x_in_c(u.mk_in(x, c), m); + + // (x in a) => (x in b) + expr_ref_vector clause1(m); + clause1.push_back(m.mk_not(x_in_a)); + clause1.push_back(x_in_b); + m_add_clause(clause1); + + // (x in a) => not (x in c) + expr_ref_vector clause2(m); + clause2.push_back(m.mk_not(x_in_a)); + clause2.push_back(m.mk_not(x_in_c)); + m_add_clause(clause2); + + // (x in b) and not (x in c) => (x in a) + expr_ref_vector clause3(m); + clause3.push_back(m.mk_not(x_in_b)); + clause3.push_back(x_in_c); + clause3.push_back(x_in_a); + m_add_clause(clause3); +} + +// a := set.singleton(b) +// (x in a) <=> (x == b) +void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) { + expr* b = nullptr; + if (!u.is_singleton(a, b)) + return; + + expr_ref x_in_a(u.mk_in(x, a), m); + expr_ref x_eq_b(m.mk_eq(x, b), m); + + // (x in a) => (x == b) + expr_ref_vector clause1(m); + clause1.push_back(m.mk_not(x_in_a)); + clause1.push_back(x_eq_b); + m_add_clause(clause1); + + // (x == b) => (x in a) + expr_ref_vector clause2(m); + clause2.push_back(m.mk_not(x_eq_b)); + clause2.push_back(x_in_a); + m_add_clause(clause2); +} + +// a := set.range(lo, hi) +// (x in a) <=> (lo <= x <= hi) +void finite_set_axioms::in_range_axiom(expr *x, expr *a) { + expr* lo = nullptr, *hi = nullptr; + if (!u.is_range(a, lo, hi)) + return; + + arith_util arith(m); + expr_ref x_in_a(u.mk_in(x, a), m); + expr_ref lo_le_x(arith.mk_le(lo, x), m); + expr_ref x_le_hi(arith.mk_le(x, hi), m); + + // (x in a) => (lo <= x) + expr_ref_vector clause1(m); + clause1.push_back(m.mk_not(x_in_a)); + clause1.push_back(lo_le_x); + m_add_clause(clause1); + + // (x in a) => (x <= hi) + expr_ref_vector clause2(m); + clause2.push_back(m.mk_not(x_in_a)); + clause2.push_back(x_le_hi); + m_add_clause(clause2); + + // (lo <= x) and (x <= hi) => (x in a) + expr_ref_vector clause3(m); + clause3.push_back(m.mk_not(lo_le_x)); + clause3.push_back(m.mk_not(x_le_hi)); + clause3.push_back(x_in_a); + m_add_clause(clause3); +} + +// a := set.map(f, b) +// (x in a) <=> set.map_inverse(f, x, b) in b +void finite_set_axioms::in_map_axiom(expr *x, expr *a) { + expr* f = nullptr, *b = nullptr; + if (!u.is_map(a, f, b)) + return; + + // For now, we provide a placeholder implementation + // The full implementation would require skolemization + // to express the inverse relationship properly. + // This would be: exists y. f(y) = x and y in b +} + +// a := set.map(f, b) +// (x in b) => f(x) in a +void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) { + expr* f = nullptr, *b = nullptr; + if (!u.is_map(a, f, b)) + return; + + expr_ref x_in_b(u.mk_in(x, b), m); + + // Apply function f to x using array select + array_util autil(m); + expr_ref fx(autil.mk_select(f, x), m); + expr_ref fx_in_a(u.mk_in(fx, a), m); + + // (x in b) => f(x) in a + expr_ref_vector clause(m); + clause.push_back(m.mk_not(x_in_b)); + clause.push_back(fx_in_a); + m_add_clause(clause); +} + +// a := set.select(p, b) +// (x in a) <=> (x in b) and p(x) +void finite_set_axioms::in_select_axiom(expr *x, expr *a) { + expr* p = nullptr, *b = nullptr; + if (!u.is_select(a, p, b)) + return; + + expr_ref x_in_a(u.mk_in(x, a), m); + expr_ref x_in_b(u.mk_in(x, b), m); + + // Apply predicate p to x using array select + array_util autil(m); + expr_ref px(autil.mk_select(p, x), m); + + // (x in a) => (x in b) + expr_ref_vector clause1(m); + clause1.push_back(m.mk_not(x_in_a)); + clause1.push_back(x_in_b); + m_add_clause(clause1); + + // (x in a) => p(x) + expr_ref_vector clause2(m); + clause2.push_back(m.mk_not(x_in_a)); + clause2.push_back(px); + m_add_clause(clause2); + + // (x in b) and p(x) => (x in a) + expr_ref_vector clause3(m); + clause3.push_back(m.mk_not(x_in_b)); + clause3.push_back(m.mk_not(px)); + clause3.push_back(x_in_a); + m_add_clause(clause3); +} + +// a := set.singleton(b) +// set.size(a) = 1 +void finite_set_axioms::size_singleton_axiom(expr *a) { + expr* b = nullptr; + if (!u.is_singleton(a, b)) + return; + + arith_util arith(m); + expr_ref size_a(u.mk_size(a), m); + expr_ref one(arith.mk_int(1), m); + expr_ref eq(m.mk_eq(size_a, one), m); + + expr_ref_vector clause(m); + clause.push_back(eq); + m_add_clause(clause); +}