mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-27 05:26:01 +00:00
Code Activity

#4880 add interpreted versions of to_bv functions for MBQI quantifier models

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-17 14:23:14 +01:00
parent 1fc7b63a80
commit d36c3faf76
7 changed files with 42 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -3429,6 +3429,16 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
mk_to_bv(f, num, args, true, result);
}
void fpa2bv_converter::mk_to_ubv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_UBV, 0, nullptr, num, args), m);
mk_to_bv(f, num, args, false, result);
}
void fpa2bv_converter::mk_to_sbv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_SBV, 0, nullptr, num, args), m);
mk_to_bv(f, num, args, true, result);
}
expr_ref fpa2bv_converter::nan_wrap(expr * n) {
expr_ref n_bv(m), arg_is_nan(m), nan(m), nan_bv(m), res(m);
mk_is_nan(n, arg_is_nan);