From 617e941015a199dab67b02b6b768ada89201058b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 23 May 2016 18:10:17 +0100 Subject: [PATCH] fp2bv refactoring --- src/api/api_ast.cpp | 2 +- src/ast/fpa/fpa2bv_converter.cpp | 34 +++++++++++----------- src/ast/fpa/fpa2bv_rewriter.cpp | 2 +- src/ast/fpa_decl_plugin.cpp | 6 ++-- src/ast/fpa_decl_plugin.h | 19 ++++++------ src/ast/rewriter/fpa_rewriter.cpp | 4 +-- src/ast/rewriter/fpa_rewriter.h | 2 +- src/smt/theory_fpa.cpp | 35 ++++++----------------- src/smt/theory_fpa.h | 3 +- src/tactic/fpa/fpa2bv_model_converter.cpp | 2 +- 10 files changed, 45 insertions(+), 64 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 1e421cb2e..1f16b2d35 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1185,7 +1185,7 @@ extern "C" { case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV; case OP_FPA_INTERNAL_MIN_I: return Z3_OP_FPA_MIN_I; case OP_FPA_INTERNAL_MAX_I: return Z3_OP_FPA_MAX_I; - case OP_FPA_INTERNAL_RM_BVWRAP: + case OP_FPA_INTERNAL_BV2RM: case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_MIN_UNSPECIFIED: case OP_FPA_INTERNAL_MAX_UNSPECIFIED: diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index c6b3c05e5..bd07b5bdc 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -79,7 +79,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { m_simp.mk_or(both_are_nan, both_the_same, result); } else if (is_rm(a) && is_rm(b)) { - SASSERT(m_util.is_rm_bvwrap(b) && m_util.is_rm_bvwrap(a)); + SASSERT(m_util.is_bv2rm(b) && m_util.is_bv2rm(a)); TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl; tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;); @@ -236,7 +236,7 @@ void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * co else if (m_util.is_rm(rng)) { app_ref na(m); na = m.mk_app(fbv, fbv->get_arity(), new_args); - result = m_util.mk_rm(na); + result = m_util.mk_bv2rm(na); } else result = m.mk_app(fbv, fbv->get_arity(), new_args); @@ -284,7 +284,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a bv_rng = m_bv_util.mk_sort(3); func_decl * bv_f = get_bv_uf(f, bv_rng, num); bv_app = m.mk_app(bv_f, num, args); - flt_app = m_util.mk_rm(bv_app); + flt_app = m_util.mk_bv2rm(bv_app); new_eq = m.mk_eq(fapp, flt_app); m_extra_assertions.push_back(new_eq); result = flt_app; @@ -315,7 +315,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) { #endif , m_bv_util.mk_sort(3)); - result = m_util.mk_rm(bv3); + result = m_util.mk_bv2rm(bv3); m_rm_const2bv.insert(f, result); m.inc_ref(f); m.inc_ref(result); @@ -522,7 +522,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); expr_ref rm(m), x(m), y(m); rm = to_app(args[0])->get_arg(0); @@ -692,7 +692,7 @@ void fpa2bv_converter::mk_neg(sort * srt, expr_ref & x, expr_ref & result) { void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); expr_ref rm(m), x(m), y(m); rm = to_app(args[0])->get_arg(0); @@ -842,7 +842,7 @@ void fpa2bv_converter::mk_mul(sort * s, expr_ref & rm, expr_ref & x, expr_ref & void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); expr_ref rm(m), x(m), y(m); rm = to_app(args[0])->get_arg(0); x = args[1]; @@ -1239,7 +1239,7 @@ void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 4); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); // fusedma means (x * y) + z expr_ref rm(m), x(m), y(m), z(m); @@ -1557,7 +1557,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); expr_ref rm(m), x(m); rm = to_app(args[0])->get_arg(0); @@ -1706,7 +1706,7 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); expr_ref rm(m), x(m); rm = to_app(args[0])->get_arg(0); @@ -2166,7 +2166,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) { - SASSERT(m_util.is_rm_bvwrap(rm)); + SASSERT(m_util.is_bv2rm(rm)); mk_to_fp_float(s, to_app(rm)->get_arg(0), x, result); } @@ -2337,7 +2337,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * "x: " << mk_ismt2_pp(x, m) << std::endl;); SASSERT(m_util.is_float(s)); SASSERT(au().is_real(x) || au().is_int(x)); - SASSERT(m_util.is_rm_bvwrap(rm)); + SASSERT(m_util.is_bv2rm(rm)); expr * bv_rm = to_app(rm)->get_arg(0); unsigned ebits = m_util.get_ebits(s); @@ -2472,7 +2472,7 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); expr * bv_rm = to_app(args[0])->get_arg(0); rational e; @@ -2630,7 +2630,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const SASSERT(num == 2); SASSERT(m_util.is_float(f->get_range())); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); SASSERT(m_bv_util.is_bv(args[1])); expr_ref rm(m), x(m); @@ -2772,7 +2772,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con SASSERT(num == 2); SASSERT(m_util.is_float(f->get_range())); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); SASSERT(m_bv_util.is_bv(args[1])); expr_ref rm(m), x(m); @@ -2924,7 +2924,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); SASSERT(num == 2); - SASSERT(m_util.is_rm_bvwrap(args[0])); + SASSERT(m_util.is_bv2rm(args[0])); SASSERT(m_util.is_float(args[1])); expr * rm = to_app(args[0])->get_arg(0); @@ -3528,7 +3528,7 @@ void fpa2bv_converter::mk_rounding_mode(decl_kind k, expr_ref & result) default: UNREACHABLE(); } - result = m_util.mk_rm(result); + result = m_util.mk_bv2rm(result); } void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 2e6314ea0..62281226e 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -156,7 +156,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; case OP_FPA_INTERNAL_BVWRAP: - case OP_FPA_INTERNAL_RM_BVWRAP: + case OP_FPA_INTERNAL_BV2RM: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 22043e7a4..6c8b7ac6f 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -676,7 +676,7 @@ func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k)); } -func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_internal_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 1) m_manager->raise_exception("invalid number of arguments to internal_rm"); @@ -837,8 +837,8 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_FPA_INTERNAL_BVWRAP: return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_INTERNAL_RM_BVWRAP: - return mk_internal_rm(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_INTERNAL_BV2RM: + return mk_internal_bv2rm(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_MIN_I: case OP_FPA_INTERNAL_MAX_I: diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 8ac343f3c..ee7325014 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -88,7 +88,7 @@ enum fpa_op_kind { /* Internal use only */ OP_FPA_INTERNAL_BVWRAP, - OP_FPA_INTERNAL_RM_BVWRAP, // Internal conversion from (_ BitVec 3) to RoundingMode + OP_FPA_INTERNAL_BV2RM, OP_FPA_INTERNAL_MIN_I, OP_FPA_INTERNAL_MAX_I, @@ -164,8 +164,8 @@ class fpa_decl_plugin : public decl_plugin { func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_rm(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); + func_decl * mk_internal_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -301,11 +301,6 @@ public: return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig); } - app * mk_rm(expr * bv3) { - SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3); - return m().mk_app(m_fid, OP_FPA_INTERNAL_RM_BVWRAP, 0, 0, 1, &bv3, mk_rm_sort()); - } - app * mk_to_fp(sort * s, expr * bv_t) { SASSERT(is_float(s) && s->get_num_parameters() == 2); return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t); @@ -373,6 +368,10 @@ public: app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); } + app * mk_bv2rm(expr * bv3) { + SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3); + return m().mk_app(m_fid, OP_FPA_INTERNAL_BV2RM, 0, 0, 1, &bv3, mk_rm_sort()); + } app * mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); app * mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); @@ -380,8 +379,8 @@ public: bool is_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); } bool is_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; } - bool is_rm_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_RM_BVWRAP); } - bool is_rm_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_RM_BVWRAP; } + bool is_bv2rm(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); } + bool is_bv2rm(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; } bool is_min_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); } bool is_min_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); } diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index b4ae744d3..b8d9c232f 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -100,7 +100,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); st = BR_FAILED; break; case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break; - case OP_FPA_INTERNAL_RM_BVWRAP:SASSERT(num_args == 1); st = mk_rm(args[0], result); break; + case OP_FPA_INTERNAL_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break; case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: @@ -719,7 +719,7 @@ br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) return BR_FAILED; } -br_status fpa_rewriter::mk_rm(expr * arg, expr_ref & result) { +br_status fpa_rewriter::mk_bv2rm(expr * arg, expr_ref & result) { bv_util bu(m()); rational bv_val; unsigned sz = 0; diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 10f4ab4aa..0d9c6a380 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -78,7 +78,7 @@ public: br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); - br_status mk_rm(expr * arg, expr_ref & result); + br_status mk_bv2rm(expr * arg, expr_ref & result); br_status mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result); br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index b97b35e24..23095f03a 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -75,7 +75,7 @@ namespace smt { SASSERT(is_rm(f->get_range())); expr_ref bv(m); bv = m_th.wrap(m.mk_const(f)); - result = m_util.mk_rm(bv); + result = m_util.mk_bv2rm(bv); m_rm_const2bv.insert(f, result); m.inc_ref(f); m.inc_ref(result); @@ -339,18 +339,11 @@ namespace smt { TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl; tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;); - if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) { - UNREACHABLE(); - if (!m_fpa_util.is_float(e_conv) && !m_fpa_util.is_rm(e_conv)) - m_th_rw(e_conv, res); - else - res = unwrap(wrap(e_conv), m.get_sort(e)); - } - else if (m_fpa_util.is_rm(e)) { - SASSERT(m_fpa_util.is_rm_bvwrap(e_conv)); + if (m_fpa_util.is_rm(e)) { + SASSERT(m_fpa_util.is_bv2rm(e_conv)); expr_ref bv_rm(m); m_th_rw(to_app(e_conv)->get_arg(0), bv_rm); - res = m_fpa_util.mk_rm(bv_rm); + res = m_fpa_util.mk_bv2rm(bv_rm); } else if (m_fpa_util.is_float(e)) { SASSERT(m_fpa_util.is_fp(e_conv)); @@ -363,20 +356,14 @@ namespace smt { } else UNREACHABLE(); - - SASSERT(res.get() != 0); + return res; } expr_ref theory_fpa::convert_conversion_term(expr * e) { SASSERT(to_app(e)->get_family_id() == get_family_id()); /* This is for the conversion functions fp.to_* */ - ast_manager & m = get_manager(); - expr_ref res(m); - proof_ref pr(m); - - SASSERT(m_arith_util.is_real(e) || m_bv_util.is_bv(e)); - + expr_ref res(get_manager()); m_rw(e, res); m_th_rw(res, res); return res; @@ -402,10 +389,8 @@ namespace smt { res = convert_atom(e); else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e)) res = convert_term(e); - else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e)) + else res = convert_conversion_term(e); - else - UNREACHABLE(); TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl; tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl << @@ -514,7 +499,6 @@ namespace smt { case OP_FPA_TO_SBV: case OP_FPA_TO_REAL: case OP_FPA_TO_IEEE_BV: { - expr_ref conv(m); conv = convert(term); assert_cnstr(m.mk_eq(term, conv)); @@ -545,7 +529,7 @@ namespace smt { if (m_fpa_util.is_rm(s)) { // For every RM term, we need to make sure that it's // associated bit-vector is within the valid range. - if (!m_fpa_util.is_rm_bvwrap(owner)) { + if (!m_fpa_util.is_bv2rm(owner)) { expr_ref valid(m), limit(m); limit = m_bv_util.mk_numeral(4, 3); valid = m_bv_util.mk_ule(wrap(owner), limit); @@ -649,7 +633,6 @@ namespace smt { void theory_fpa::pop_scope_eh(unsigned num_scopes) { m_trail_stack.pop_scope(num_scopes); TRACE("t_fpa", tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";); - // unsigned num_old_vars = get_old_num_vars(num_scopes); theory::pop_scope_eh(num_scopes); } @@ -785,7 +768,7 @@ namespace smt { mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;); res = vp; } - else if (m_fpa_util.is_rm_bvwrap(owner)) { + else if (m_fpa_util.is_bv2rm(owner)) { SASSERT(to_app(owner)->get_num_args() == 1); app_ref a0(m); a0 = to_app(owner->get_arg(0)); diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index f1ed5219f..0a3ed94c6 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -144,8 +144,7 @@ namespace smt { fpa_util & m_fpa_util; bv_util & m_bv_util; arith_util & m_arith_util; - obj_map m_wraps; - obj_map m_unwraps; + obj_map m_wraps; obj_map m_conversions; bool m_is_initialized; obj_hashtable m_is_added_to_model; diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 64423f224..20d8bbbcc 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -395,7 +395,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { func_decl * var = it->m_key; SASSERT(m_fpa_util.is_rm(var->get_range())); expr * val = it->m_value; - SASSERT(m_fpa_util.is_rm_bvwrap(val)); + SASSERT(m_fpa_util.is_bv2rm(val)); expr * bvval = to_app(val)->get_arg(0); expr_ref fv(m); fv = convert_bv2rm(bv_mdl, bvval);