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

Made fp.* comparison chainable.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-20 17:57:27 +01:00
parent ccc1f02216
commit c377fec7a4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/fpa_decl_plugin.cpp
View file

@ -289,7 +289,7 @@ func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_param
func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 2)
if (arity < 2)
m_manager->raise_exception("invalid number of arguments to floating point relation");
if (domain[0] != domain[1] || !is_float_sort(domain[0]))
m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments");
@ -306,7 +306,7 @@ func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameter
}
func_decl_info finfo(m_family_id, k);
finfo.set_chainable(true);
return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), finfo);
return m_manager->mk_func_decl(name, domain[0], domain[1], m_manager->mk_bool_sort(), finfo);
}
func_decl * fpa_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,