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

test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-14 18:01:41 +02:00
parent a1b831a3e1
commit f2260d959d
2 changed files with 24 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -828,16 +828,28 @@ class finite_set_inverter : public iexpr_inverter {
public:
finite_set_inverter(ast_manager& m): iexpr_inverter(m), fs(m) {}
family_id get_fid() const override { return fs.get_family_id(); }
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
// x union y -> x
// y := x
if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) {
mk_fresh_uncnstr_var_for(f, r);
r = args[0];
if (m_mc) {
add_def(args[0], r);
add_def(args[1], fs.mk_empty(args[1]->get_sort()));
add_def(args[1], r);
}
return true;
}
return false;
case OP_FINITE_SET_INTERSECT:
// x intersect y -> x
// y := x
if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) {
r = args[0];
if (m_mc) {
add_def(args[1], r);
}
return true;
}
@ -1001,6 +1013,7 @@ expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) {
add(alloc(basic_expr_inverter, m, *this));
add(alloc(seq_expr_inverter, m));
//add(alloc(pb_expr_inverter, m));
add(alloc(finite_set_inverter, m));
}

7
src/ast/rewriter/th_rewriter.cpp
View file

@ -30,6 +30,7 @@ Notes:
#include "ast/rewriter/pb_rewriter.h"
#include "ast/rewriter/recfun_rewriter.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/finite_set_rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/der.h"
@ -55,6 +56,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
seq_rewriter m_seq_rw;
char_rewriter m_char_rw;
recfun_rewriter m_rec_rw;
finite_set_rewriter m_fs_rw;
arith_util m_a_util;
bv_util m_bv_util;
der m_der;
@ -229,6 +231,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return m_char_rw.mk_app_core(f, num, args, result);
if (fid == m_rec_rw.get_fid())
return m_rec_rw.mk_app_core(f, num, args, result);
if (fid == m_fs_rw.get_fid())
return m_fs_rw.mk_app_core(f, num, args, result);
return BR_FAILED;
}
@ -882,7 +886,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_pb_rw(m),
m_seq_rw(m, p),
m_char_rw(m),
m_rec_rw(m),
m_rec_rw(m),
m_fs_rw(m),
m_a_util(m),
m_bv_util(m),
m_der(m),