From f4fd94747cbd41a6b8fcf579db5603c98e4ec9cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Oct 2019 09:39:40 -0700 Subject: [PATCH] fix #2652 Signed-off-by: Nikolaj Bjorner --- src/ast/fpa/bv2fpa_converter.cpp | 14 ++++++-------- src/ast/fpa/fpa2bv_converter.cpp | 24 ------------------------ src/smt/smt_model_checker.cpp | 2 +- 3 files changed, 7 insertions(+), 33 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index fca1dc4b933..3eeacab247e 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -466,16 +466,14 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode } continue; } - // kv.m_value contains the model for the unspecified cases of kv.m_key. - // TBD: instead of mapping the interpretation of f to just the graph for the - // uninterpreted case, map it to a condition, ite, that filters out the - // pre-condition for which argument combinations are interpreted vs. uninterpreted. - // if (m_fpa_util.is_to_ieee_bv(f)) { - // } - // if (m_fpa_util.is_to_sbv(f)) { - // } + // f is a floating point function: f(x,y) : Float + // f_uf is a bit-vector function: f_uf(xB,yB) : BitVec + // then there is f_def: f_Bv(xB, yB) := if(range(xB),.., f_uf(xB,yB)) + // f(x,y) := to_float(if(range(to_bv(x)), ... f_uf(to_bv(xB), to_bv(yB)))) - not practical + // := if(range_fp(x), ...., to_float(f_uf(...)) - approach + target_model->register_decl(f, convert_func_interp(mc, f, f_uf)); } } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 4407a824fc2..f5468af698c 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3201,26 +3201,6 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args sort * xs = m.get_sort(x); sort * bv_srt = f->get_range(); -#if 0 - // for this to work, the following is required: - // 1. split_fp should succeed even if the argument does not satisfy is_fp - // we would need functions to access the sgn, exp and sig fields - // 2. an inverse of bv2rm, here called rm2bv. - expr_ref arg1(m), arg2(m), _rm(m); - - var_subst vsubst(m, false); - expr* def = get_bv_def(f); - if (def) { - result = vsubst(def, 2, args); - return; - } - arg1 = m.mk_var(0, m.get_sort(args[0])); - arg2 = m.mk_var(1, m.get_sort(args[1])); - _rm = m_util.mk_rm2bv(arg1); - rm = _rm; - x = arg2; -#endif - expr_ref sgn(m), sig(m), exp(m), lz(m); unpack(x, sgn, sig, exp, lz, true); @@ -3370,10 +3350,6 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args result = m.mk_ite(c2, v2, result); result = m.mk_ite(c1, v1, result); -#if 0 - set_bv_def(f, result); - result = vsubst(result, 2, args); -#endif SASSERT(is_well_sorted(m, result)); } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 49b8dff2e6e..618cfd4abb6 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -238,7 +238,7 @@ namespace smt { sk_value = get_type_compatible_term(sk_value); } func_decl * f = nullptr; - if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f)) { + if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f) && cex->get_func_interp(f)->get_interp()) { expr_ref body(cex->get_func_interp(f)->get_interp(), m); ptr_vector sorts(f->get_arity(), f->get_domain()); svector names;