mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-13 09:31:14 +00:00
Code Activity

Refactor expr_inverter to remove set operations

Browse source 
Removed handling for set operations like union, intersection, and difference in expr_inverter.cpp. Introduced finite_set_inverter class to manage set union operation.
This commit is contained in:
Nikolaj Bjorner 2025-10-14 17:27:35 +02:00 • committed by GitHub
parent 6b6f043dc0
commit 2eb203ef37
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 29 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

69
src/ast/converters/expr_inverter.cpp
View file

@ -637,46 +637,6 @@ public:
return true; return true;
} }
return false; return false;
case OP_SET_UNION:
// x union y -> fresh
// x := fresh, y := empty
if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) {
mk_fresh_uncnstr_var_for(f, r);
if (m_mc) {
add_def(args[0], r);
add_def(args[1], a.mk_empty_set(args[1]->get_sort()));
}
return true;
}
return false;
case OP_SET_INTERSECT:
// x intersect y -> fresh
// x := if fresh = empty then empty else y
// This handles the case where x = intersect(x, y)
if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) {
mk_fresh_uncnstr_var_for(f, r);
if (m_mc) {
sort* s = args[0]->get_sort();
expr_ref empty_set(a.mk_empty_set(s), m);
expr_ref is_empty(m.mk_eq(r, empty_set), m);
add_def(args[0], m.mk_ite(is_empty, empty_set, args[1]));
add_def(args[1], r);
}
return true;
}
return false;
case OP_SET_DIFFERENCE:
// x difference y -> fresh
// x := fresh union y, y := empty
if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) {
mk_fresh_uncnstr_var_for(f, r);
if (m_mc) {
add_def(args[0], a.mk_union(r, args[1]));
add_def(args[1], a.mk_empty_set(args[1]->get_sort()));
}
return true;
}
return false;
case OP_SET_COMPLEMENT: case OP_SET_COMPLEMENT:
// complement(x) -> fresh // complement(x) -> fresh
// x := complement(fresh) // x := complement(fresh)
@ -873,6 +833,35 @@ public:
}; };
#endif #endif
class finite_set_inverter : public iexpr_inverter {
finite_set_util fs;
public:
finite_set_inverter(ast_manager& m): iexpr_inverter(m), fs(m) {}
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
switch (f->get_decl_kind()) {
case OP_SET_UNION:
// x union y -> fresh
// x := fresh, y := empty
if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) {
mk_fresh_uncnstr_var_for(f, r);
if (m_mc) {
add_def(args[0], r);
add_def(args[1], fs.mk_empty_set(args[1]->get_sort()));
}
return true;
}
return false;
default:
break;
}
return false;
}
bool mk_diff(expr* t, expr_ref& r) override {
return false;
}
};
class seq_expr_inverter : public iexpr_inverter { class seq_expr_inverter : public iexpr_inverter {
seq_util seq; seq_util seq;