mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fix empty set declaration, add axioms and rewrites

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-27 18:18:46 +01:00
parent 4630373a97
commit 4464ab9431
6 changed files with 180 additions and 122 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/finite_set_decl_plugin.cpp
View file

@ -39,6 +39,7 @@ finite_set_decl_plugin::finite_set_decl_plugin():
m_names[OP_FINITE_SET_FILTER] = "set.filter";
m_names[OP_FINITE_SET_RANGE] = "set.range";
m_names[OP_FINITE_SET_EXT] = "set.diff";
m_names[OP_FINITE_SET_MAP_INVERSE] = "set.map.inverse";
}
finite_set_decl_plugin::~finite_set_decl_plugin() {
@ -70,6 +71,7 @@ void finite_set_decl_plugin::init() {
sort* arrABsetA[2] = { arrAB, setA };
sort* arrABoolsetA[2] = { arrABool, setA };
sort* intintT[2] = { intT, intT };
sort *arrABsetBsetA[3] = {arrAB, setB, setA};
m_sigs.resize(LAST_FINITE_SET_OP);
m_sigs[OP_FINITE_SET_EMPTY] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_EMPTY], 1, 0, nullptr, setA);
@ -84,7 +86,7 @@ void finite_set_decl_plugin::init() {
m_sigs[OP_FINITE_SET_FILTER] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_FILTER], 1, 2, arrABoolsetA, setA);
m_sigs[OP_FINITE_SET_RANGE] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_RANGE], 0, 2, intintT, setInt);
m_sigs[OP_FINITE_SET_EXT] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_EXT], 1, 2, setAsetA, A);
// m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A);
m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A);
}
sort * finite_set_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
@ -190,6 +192,7 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param
case OP_FINITE_SET_SIZE:
case OP_FINITE_SET_SUBSET:
case OP_FINITE_SET_MAP:
case OP_FINITE_SET_MAP_INVERSE:
case OP_FINITE_SET_FILTER:
case OP_FINITE_SET_RANGE:
case OP_FINITE_SET_EXT:
@ -322,3 +325,4 @@ func_decl *finite_set_util::mk_range_decl() {
sort *domain[2] = {i, i};
return m_manager.mk_func_decl(m_fid, OP_FINITE_SET_RANGE, 0, nullptr, 2, domain, nullptr);
}

4
src/ast/finite_set_decl_plugin.h
View file

@ -201,6 +201,10 @@ public:
return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP, arr, set);
}
app *mk_map_inverse(expr *arr, expr *a, expr *b) {
return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP_INVERSE, arr, b, a);
}
app * mk_filter(expr* arr, expr* set) {
return m_manager.mk_app(m_fid, OP_FINITE_SET_FILTER, arr, set);
}

156
src/ast/rewriter/finite_set_axioms.cpp
View file

@ -42,10 +42,7 @@ void finite_set_axioms::in_empty_axiom(expr *x) {
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);
ax->clause.push_back(m.mk_not(x_in_empty));
m_add_clause(ax);
add_unit("in-empty", x, m.mk_not(x_in_empty));
}
// a := set.union(b, c)
@ -55,7 +52,6 @@ void finite_set_axioms::in_union_axiom(expr *x, expr *a) {
if (!u.is_union(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);
@ -151,10 +147,10 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) {
expr_ref x_in_a(u.mk_in(x, a), m);
theory_axiom* ax = alloc(theory_axiom, m, "in-singleton", x, a);
if (x == b) {
// If x and b are syntactically identical, then (x in a) is always true
theory_axiom* ax = alloc(theory_axiom, m, "in-singleton", x, a);
ax->clause.push_back(x_in_a);
m_add_clause(ax);
return;
@ -163,35 +159,28 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) {
expr_ref x_eq_b(m.mk_eq(x, b), m);
// (x in a) => (x == b)
ax->clause.push_back(m.mk_not(x_in_a));
ax->clause.push_back(x_eq_b);
m_add_clause(ax);
ax = alloc(theory_axiom, m, "in-singleton", x, a);
add_binary("in-singleton", x, a, m.mk_not(x_in_a), x_eq_b);
// (x == b) => (x in a)
ax->clause.push_back(m.mk_not(x_eq_b));
ax->clause.push_back(x_in_a);
m_add_clause(ax);
add_binary("in-singleton", x, a, m.mk_not(x_eq_b), x_in_a);
}
void finite_set_axioms::in_singleton_axiom(expr* a) {
expr *b = nullptr;
if (!u.is_singleton(a, b))
return;
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);
add_unit("in-singleton", a, u.mk_in(b, a));
}
// a := set.range(lo, hi)
// (x in a) <=> (lo <= x <= hi)
// we use the rewriter to simplify inequalitiess because the arithmetic solver
// makes some assumptions that inequalities are in normal form.
// this complicates proof checking.
// Options are to include a proof of the rewrite within the justification
// fix the arithmetic solver to use the inequalities without rewriting (it really should)
// the same issue applies to everywhere we apply rewriting when adding theory axioms.
void finite_set_axioms::in_range_axiom(expr *x, expr *a) {
expr* lo = nullptr, *hi = nullptr;
if (!u.is_range(a, lo, hi))
@ -205,16 +194,10 @@ void finite_set_axioms::in_range_axiom(expr *x, expr *a) {
m_rewriter(x_le_hi);
// (x in a) => (lo <= x)
theory_axiom* ax1 = alloc(theory_axiom, m, "in-range", x, a);
ax1->clause.push_back(m.mk_not(x_in_a));
ax1->clause.push_back(lo_le_x);
m_add_clause(ax1);
add_binary("in-range", x, a, m.mk_not(x_in_a), lo_le_x);
// (x in a) => (x <= hi)
theory_axiom* ax2 = alloc(theory_axiom, m, "in-range", x, a);
ax2->clause.push_back(m.mk_not(x_in_a));
ax2->clause.push_back(x_le_hi);
m_add_clause(ax2);
add_binary("in-range", x, a, m.mk_not(x_in_a), x_le_hi);
// (lo <= x) and (x <= hi) => (x in a)
theory_axiom* ax3 = alloc(theory_axiom, m, "in-range", x, a);
@ -246,13 +229,8 @@ void finite_set_axioms::in_range_axiom(expr* r) {
ax->clause.push_back(u.mk_in(hi, r));
m_add_clause(ax);
ax = alloc(theory_axiom, m, "range-bounds", r);
ax->clause.push_back(m.mk_not(u.mk_in(a.mk_add(hi, a.mk_int(1)), r)));
m_add_clause(ax);
ax = alloc(theory_axiom, m, "range-bounds", r);
ax->clause.push_back(m.mk_not(u.mk_in(a.mk_add(lo, a.mk_int(-1)), r)));
m_add_clause(ax);
add_unit("range-bounds", r, m.mk_not(u.mk_in(a.mk_add(hi, a.mk_int(1)), r)));
add_unit("range-bounds", r, m.mk_not(u.mk_in(a.mk_add(lo, a.mk_int(-1)), r)));
}
// a := set.map(f, b)
@ -262,6 +240,11 @@ void finite_set_axioms::in_map_axiom(expr *x, expr *a) {
if (!u.is_map(a, f, b))
return;
expr_ref inv(u.mk_map_inverse(x, f, b), m);
expr_ref f1(u.mk_in(x, a), m);
expr_ref f2(u.mk_in(inv, b), m);
add_binary("map-inverse", x, a, m.mk_not(f1), f2);
add_binary("map-inverse", x, b, f1, m.mk_not(f2));
// For now, we provide a placeholder implementation
// The full implementation would require skolemization
// to express the inverse relationship properly.
@ -281,12 +264,10 @@ void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) {
array_util autil(m);
expr_ref fx(autil.mk_select(f, x), m);
expr_ref fx_in_a(u.mk_in(fx, a), m);
m_rewriter(fx);
// (x in b) => f(x) in a
theory_axiom* ax = alloc(theory_axiom, m, "in-map-image", x, a);
ax->clause.push_back(m.mk_not(x_in_b));
ax->clause.push_back(fx_in_a);
m_add_clause(ax);
add_binary("in-map", x, a, m.mk_not(x_in_b), fx_in_a);
}
// a := set.filter(p, b)
@ -304,16 +285,10 @@ void finite_set_axioms::in_filter_axiom(expr *x, expr *a) {
expr_ref px(autil.mk_select(p, x), m);
// (x in a) => (x in b)
theory_axiom* ax1 = alloc(theory_axiom, m, "in-filter", x, a);
ax1->clause.push_back(m.mk_not(x_in_a));
ax1->clause.push_back(x_in_b);
m_add_clause(ax1);
add_binary("in-filter", x, a, m.mk_not(x_in_a), x_in_b);
// (x in a) => p(x)
theory_axiom* ax2 = alloc(theory_axiom, m, "in-filter", x, a);
ax2->clause.push_back(m.mk_not(x_in_a));
ax2->clause.push_back(px);
m_add_clause(ax2);
add_binary("in-filter", x, a, m.mk_not(x_in_a), px);
// (x in b) and p(x) => (x in a)
theory_axiom* ax3 = alloc(theory_axiom, m, "in-filter", x, a);
@ -323,23 +298,74 @@ void finite_set_axioms::in_filter_axiom(expr *x, expr *a) {
m_add_clause(ax3);
}
// 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);
theory_axiom* ax = alloc(theory_axiom, m, "size-singleton", a);
ax->clause.push_back(eq);
void finite_set_axioms::add_unit(char const* name, expr* e, expr* unit) {
theory_axiom *ax = alloc(theory_axiom, m, name, e);
ax->clause.push_back(unit);
m_add_clause(ax);
}
void finite_set_axioms::add_binary(char const* name, expr* x, expr* y, expr* f1, expr* f2) {
theory_axiom *ax = alloc(theory_axiom, m, name, x, y);
ax->clause.push_back(f1);
ax->clause.push_back(f2);
m_add_clause(ax);
}
// Auxiliary algebraic axioms to ease reasoning about set.size
// The axioms are not required for completenss for the base fragment
// as they are handled by creating semi-linear sets.
void finite_set_axioms::size_ub_axiom(expr *e) {
expr *b = nullptr, *x = nullptr, *y = nullptr;
arith_util a(m);
expr_ref ineq(m);
if (u.is_singleton(e, b))
add_unit("size", e, m.mk_eq(u.mk_size(e), a.mk_int(1)));
else if (u.is_empty(e))
add_unit("size", e, m.mk_eq(u.mk_size(e), a.mk_int(0)));
else if (u.is_union(e, x, y)) {
ineq = a.mk_le(u.mk_size(e), a.mk_add(u.mk_size(x), u.mk_size(y)));
m_rewriter(ineq);
add_unit("size", e, ineq);
}
else if (u.is_intersect(e, x, y)) {
ineq = a.mk_le(u.mk_size(e), u.mk_size(x));
m_rewriter(ineq);
add_unit("size", e, ineq);
ineq = a.mk_le(u.mk_size(e), u.mk_size(y));
m_rewriter(ineq);
add_unit("size", e, ineq);
}
else if (u.is_difference(e, x, y)) {
ineq = a.mk_le(u.mk_size(e), u.mk_size(x));
m_rewriter(ineq);
add_unit("size", e, ineq);
}
else if (u.is_filter(e, x, y)) {
ineq = a.mk_le(u.mk_size(e), u.mk_size(y));
m_rewriter(ineq);
add_unit("size", e, ineq);
}
else if (u.is_map(e, x, y)) {
ineq = a.mk_le(u.mk_size(e), u.mk_size(y));
m_rewriter(ineq);
add_unit("size", e, ineq);
}
else if (u.is_range(e, x, y)) {
ineq = a.mk_eq(u.mk_size(e), m.mk_ite(a.mk_le(x, y), a.mk_add(a.mk_sub(y, x), a.mk_int(1)), a.mk_int(0)));
m_rewriter(ineq);
add_unit("size", e, ineq);
}
}
void finite_set_axioms::size_lb_axiom(expr* e) {
arith_util a(m);
expr_ref ineq(m);
ineq = a.mk_le(a.mk_int(0), u.mk_size(e));
m_rewriter(ineq);
add_unit("size-lb", e, ineq);
}
void finite_set_axioms::subset_axiom(expr* a) {
expr *b = nullptr, *c = nullptr;
if (!u.is_subset(a, b, c))

25
src/ast/rewriter/finite_set_axioms.h
View file

@ -46,6 +46,10 @@ class finite_set_axioms {
std::function<void(theory_axiom *)> m_add_clause;
void add_unit(char const* name, expr* x, expr *e);
void add_binary(char const *name, expr *x, expr *y, expr *f1, expr *f2);
public:
finite_set_axioms(ast_manager &m) : m(m), u(m), m_rewriter(m) {}
@ -86,8 +90,8 @@ public:
// a := set.range(lo, hi)
// (not (set.in (- lo 1) a))
// (not (set.in (+ hi 1) a))
// (set.in lo a)
// (set.in hi a)
// lo <= hi => (set.in lo a)
// lo <= hi => (set.in hi a)
void in_range_axiom(expr *a);
// a := set.map(f, b)
@ -106,9 +110,20 @@ public:
// (a) <=> (set.intersect(b, c) = b)
void subset_axiom(expr *a);
// a := set.singleton(b)
// set.size(a) = 1
void size_singleton_axiom(expr *a);
// set.size(empty) = 0
// set.size(set.singleton(b)) = 1
// set.size(a u b) <= set.size(a) + set.size(b)
// set.size(a n b) <= min(set.size(a), set.size(b))
// set.size(a \ b) <= set.size(a)
// set.size(set.map(f, b)) <= set.size(b)
// set.size(set.filter(p, b)) <= set.size(b)
// set.size([l..u]) = if(l <= u, u - l + 1, 0)
void size_ub_axiom(expr *a);
// 0 <= set.size(e)
void size_lb_axiom(expr *e);
// a != b => set.in (set.diff(a, b) a) != set.in (set.diff(a, b) b)
void extensionality_axiom(expr *a, expr *b);

19
src/ast/rewriter/finite_set_rewriter.cpp
View file

@ -47,14 +47,14 @@ br_status finite_set_rewriter::mk_app_core(func_decl * f, unsigned num_args, exp
}
br_status finite_set_rewriter::mk_union(unsigned num_args, expr * const * args, expr_ref & result) {
VERIFY(num_args == 2);
// Idempotency: set.union(x, x) -> x
if (num_args == 2 && args[0] == args[1]) {
if (args[0] == args[1]) {
result = args[0];
return BR_DONE;
}
// Identity: set.union(x, empty) -> x or set.union(empty, x) -> x
if (num_args == 2) {
if (u.is_empty(args[0])) {
result = args[1];
return BR_DONE;
@ -80,20 +80,22 @@ br_status finite_set_rewriter::mk_union(unsigned num_args, expr * const * args,
return BR_DONE;
}
}
}
return BR_FAILED;
}
br_status finite_set_rewriter::mk_intersect(unsigned num_args, expr * const * args, expr_ref & result) {
if (num_args != 2)
return BR_FAILED;
// Idempotency: set.intersect(x, x) -> x
if (num_args == 2 && args[0] == args[1]) {
if (args[0] == args[1]) {
result = args[0];
return BR_DONE;
}
// Annihilation: set.intersect(x, empty) -> empty or set.intersect(empty, x) -> empty
if (num_args == 2) {
if (u.is_empty(args[0])) {
result = args[0];
return BR_DONE;
@ -119,6 +121,13 @@ br_status finite_set_rewriter::mk_intersect(unsigned num_args, expr * const * ar
return BR_DONE;
}
}
expr *l1, *l2, *u1, *u2;
if (u.is_range(args[0], l1, u1) && u.is_range(args[1], l2, u2)) {
arith_util a(m);
auto max_l = m.mk_ite(a.mk_ge(l1, l2), l1, l2);
auto min_u = m.mk_ite(a.mk_ge(u1, u2), u2, u1);
result = u.mk_range(max_l, min_u);
return BR_REWRITE_FULL;
}
return BR_FAILED;