mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

streamlining expr-inverter code

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-13 11:48:32 -08:00
parent 3d570aaa0a
commit ce76e3138d
2 changed files with 19 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -49,6 +49,8 @@ public:
basic_expr_inverter(ast_manager& m, iexpr_inverter& inv) : iexpr_inverter(m), inv(inv) {} basic_expr_inverter(ast_manager& m, iexpr_inverter& inv) : iexpr_inverter(m), inv(inv) {}
family_id get_fid() const override { return m.get_basic_family_id(); }
/** /**
* if (c, x, x') -> fresh * if (c, x, x') -> fresh
* x := fresh * x := fresh
@ -147,7 +149,7 @@ public:
arith_expr_inverter(ast_manager& m) : iexpr_inverter(m), a(m) {} arith_expr_inverter(ast_manager& m) : iexpr_inverter(m), a(m) {}
family_id get_fid() const { return a.get_family_id(); } family_id get_fid() const override { return a.get_family_id(); }
bool process_le_ge(func_decl* f, expr* arg1, expr* arg2, bool le, expr_ref& r) { bool process_le_ge(func_decl* f, expr* arg1, expr* arg2, bool le, expr_ref& r) {
expr* v; expr* v;
@ -350,6 +352,9 @@ class bv_expr_inverter : public iexpr_inverter {
// parity can be defined using a "giant" ite expression. // parity can be defined using a "giant" ite expression.
// //
if (uncnstr(args[i]))
IF_VERBOSE(11, verbose_stream() << "MISSED mult-unconstrained " << mk_bounded_pp(args[i], m) << "\n");
return false; return false;
} }
@ -462,7 +467,7 @@ class bv_expr_inverter : public iexpr_inverter {
public: public:
bv_expr_inverter(ast_manager& m) : iexpr_inverter(m), bv(m) {} bv_expr_inverter(ast_manager& m) : iexpr_inverter(m), bv(m) {}
family_id get_fid() const { return bv.get_family_id(); } family_id get_fid() const override { return bv.get_family_id(); }
/** /**
* x + t -> fresh * x + t -> fresh
@ -567,7 +572,7 @@ class array_expr_inverter : public iexpr_inverter {
public: public:
array_expr_inverter(ast_manager& m, iexpr_inverter& s) : iexpr_inverter(m), a(m), inv(s) {} array_expr_inverter(ast_manager& m, iexpr_inverter& s) : iexpr_inverter(m), a(m), inv(s) {}
family_id get_fid() const { return a.get_family_id(); } family_id get_fid() const override { return a.get_family_id(); }
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override { bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override {
SASSERT(f->get_family_id() == a.get_family_id()); SASSERT(f->get_family_id() == a.get_family_id());
@ -631,7 +636,7 @@ public:
dt_expr_inverter(ast_manager& m) : iexpr_inverter(m), dt(m) {} dt_expr_inverter(ast_manager& m) : iexpr_inverter(m), dt(m) {}
family_id get_fid() const { return dt.get_family_id(); } family_id get_fid() const override { return dt.get_family_id(); }
/** /**
* head(x) -> fresh * head(x) -> fresh
* x := cons(fresh, arb) * x := cons(fresh, arb)
@ -745,20 +750,16 @@ void iexpr_inverter::add_defs(unsigned num, expr* const* args, expr* u, expr* id
expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) { expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) {
auto* a = alloc(arith_expr_inverter, m); auto add = [&](iexpr_inverter* i) {
auto* b = alloc(bv_expr_inverter, m); m_inverters.setx(i->get_fid(), i, nullptr);
auto* ar = alloc(array_expr_inverter, m, *this); };
auto* dt = alloc(dt_expr_inverter, m); add(alloc(arith_expr_inverter, m));
m_inverters.setx(m.get_basic_family_id(), alloc(basic_expr_inverter, m, *this), nullptr); add(alloc(bv_expr_inverter, m));
m_inverters.setx(a->get_fid(), a, nullptr); add(alloc(array_expr_inverter, m, *this));
m_inverters.setx(b->get_fid(), b, nullptr); add(alloc(dt_expr_inverter, m));
m_inverters.setx(ar->get_fid(), ar, nullptr); add(alloc(basic_expr_inverter, m, *this));
m_inverters.setx(dt->get_fid(), dt, nullptr);
} }
bool expr_inverter::is_converted(func_decl* f, unsigned num, expr* const* args) {
return false;
}
bool expr_inverter::operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) { bool expr_inverter::operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) {
if (num == 0) if (num == 0)
@ -772,9 +773,6 @@ bool expr_inverter::operator()(func_decl* f, unsigned num, expr* const* args, ex
if (fid == null_family_id) if (fid == null_family_id)
return false; return false;
if (is_converted(f, num, args))
return false;
auto* p = m_inverters.get(fid, nullptr); auto* p = m_inverters.get(fid, nullptr);
return p && (*p)(f, num, args, new_expr, side_cond); return p && (*p)(f, num, args, new_expr, side_cond);
} }

4
src/ast/converters/expr_inverter.h
View file

@ -40,13 +40,12 @@ public:
virtual bool operator()(func_decl* f, unsigned n, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) = 0; virtual bool operator()(func_decl* f, unsigned n, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) = 0;
virtual bool mk_diff(expr* t, expr_ref& r) = 0; virtual bool mk_diff(expr* t, expr_ref& r) = 0;
virtual family_id get_fid() const = 0;
}; };
class expr_inverter : public iexpr_inverter { class expr_inverter : public iexpr_inverter {
ptr_vector<iexpr_inverter> m_inverters; ptr_vector<iexpr_inverter> m_inverters;
bool is_converted(func_decl* f, unsigned num, expr* const* args);
public: public:
expr_inverter(ast_manager& m); expr_inverter(ast_manager& m);
~expr_inverter() override; ~expr_inverter() override;
@ -54,4 +53,5 @@ public:
bool mk_diff(expr* t, expr_ref& r) override; bool mk_diff(expr* t, expr_ref& r) override;
void set_is_var(std::function<bool(expr*)>& is_var) override; void set_is_var(std::function<bool(expr*)>& is_var) override;
void set_model_converter(generic_model_converter* mc) override; void set_model_converter(generic_model_converter* mc) override;
family_id get_fid() const override { return null_family_id; }
}; };