mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Improved FPA simplifier plugin
This commit is contained in:
parent
37b11cdc74
commit
e9d94e53f6
|
@ -24,16 +24,16 @@ m_rw(m) {}
|
|||
fpa_simplifier_plugin::~fpa_simplifier_plugin() {}
|
||||
|
||||
bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
set_reduce_invoked();
|
||||
set_reduce_invoked();
|
||||
|
||||
SASSERT(f->get_family_id() == get_family_id());
|
||||
|
||||
return m_rw.mk_app_core(f, num_args, args, result) == BR_DONE;
|
||||
return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED;
|
||||
}
|
||||
|
||||
bool fpa_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
|
||||
set_reduce_invoked();
|
||||
|
||||
return m_rw.mk_eq_core(lhs, rhs, result) == BR_DONE;
|
||||
return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue