mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-06 06:16:02 +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:47:13 +00:00
parent 3e495b1e80
commit 3e81681a99
3 changed files with 16 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/finite_set_decl_plugin.cpp
View file

@ -139,7 +139,10 @@ 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"); m_manager->raise_exception("set.empty requires one sort parameter");
return nullptr; return nullptr;
} }
range = to_sort(parameters[0].get_ast()); sort* element_sort = to_sort(parameters[0].get_ast());
// Create finite_set_sort from element_sort
parameter set_param(element_sort);
range = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, &set_param);
} }
return mk_empty(range); return mk_empty(range);
case OP_FINITE_SET_SINGLETON: case OP_FINITE_SET_SINGLETON:

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

@ -64,14 +64,20 @@ br_status finite_set_rewriter::mk_intersect(unsigned num_args, expr * const * ar
br_status finite_set_rewriter::mk_difference(expr * arg1, expr * arg2, expr_ref & result) { br_status finite_set_rewriter::mk_difference(expr * arg1, expr * arg2, expr_ref & result) {
// set.difference(x, x) -> set.empty // set.difference(x, x) -> set.empty
if (arg1 == arg2) { if (arg1 == arg2) {
// Get the element sort from the set sort // Get the set sort
sort* set_sort = arg1->get_sort(); sort* set_sort = arg1->get_sort();
SASSERT(m_util.is_finite_set(set_sort)); SASSERT(m_util.is_finite_set(set_sort));
// Get element sort - the parameter of the set sort // Create empty set with the same set sort
sort* elem_sort = to_sort(set_sort->get_parameter(0).get_ast()); // We need to get the element sort from the parameters
result = m_util.mk_empty(elem_sort); if (set_sort->get_num_parameters() > 0) {
return BR_DONE; parameter const& param = set_sort->get_parameter(0);
if (param.is_ast() && is_sort(param.get_ast())) {
sort* elem_sort = to_sort(param.get_ast());
result = m_util.mk_empty(elem_sort);
return BR_DONE;
}
}
} }
return BR_FAILED; return BR_FAILED;

1
src/ast/rewriter/finite_set_rewriter.h
View file

@ -26,6 +26,7 @@ where the signature is defined in finite_set_decl_plugin.h.
#include "ast/finite_set_decl_plugin.h" #include "ast/finite_set_decl_plugin.h"
#include "ast/rewriter/rewriter_types.h" #include "ast/rewriter/rewriter_types.h"
#include "util/params.h"
/** /**
\brief Cheap rewrite rules for finite sets \brief Cheap rewrite rules for finite sets