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

Implement inverter functions for finite-set operators (#7974)

Browse source 
* Initial plan

* Add set operator inverters to array_expr_inverter

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Refactor expr_inverter to remove set operations

Removed handling for set operations like union, intersection, and difference in expr_inverter.cpp. Introduced finite_set_inverter class to manage set union operation.

* Remove OP_SET_COMPLEMENT case from expr_inverter

Removed handling for OP_SET_COMPLEMENT in expr_inverter.

* Change OP_SET_UNION to OP_FINITE_SET_UNION

---------

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 <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2025-10-14 17:48:40 +02:00 • committed by GitHub
parent 0efe3820fc
commit 930ba5ebd6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 29 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -823,6 +823,35 @@ public:
};
#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_FINITE_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 {
seq_util seq;