mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-09 15:47:29 +00:00
Code Activity

Fix finite_set_decl_plugin bug and complete implementation

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-14 08:55:02 +00:00
parent ab7229b01d
commit 819979db67
2 changed files with 10 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/finite_set_decl_plugin.cpp
View file

@ -139,7 +139,9 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param
m_manager->raise_exception("set.empty requires one sort parameter");
return nullptr;
}
range = to_sort(parameters[0].get_ast());
sort* element_sort = to_sort(parameters[0].get_ast());
parameter param(element_sort);
range = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, &param);
}
return mk_empty(range);
case OP_FINITE_SET_SINGLETON:

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

@ -24,11 +24,15 @@ Revision History:
#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) {
expr_ref_vector clause(m);
sort* s = x->get_sort();
expr_ref empty_set(u.mk_empty(s), m);
// 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);
}