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

fix #2652

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-23 09:39:40 -07:00
parent e2a9cb80e2
commit f4fd94747c
3 changed files with 7 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -466,16 +466,14 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
} }
continue; 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)); target_model->register_decl(f, convert_func_interp(mc, f, f_uf));
} }
} }

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

@ -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 * xs = m.get_sort(x);
sort * bv_srt = f->get_range(); 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); expr_ref sgn(m), sig(m), exp(m), lz(m);
unpack(x, sgn, sig, exp, lz, true); 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(c2, v2, result);
result = m.mk_ite(c1, v1, 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)); SASSERT(is_well_sorted(m, result));
} }

2
src/smt/smt_model_checker.cpp
View file

@ -238,7 +238,7 @@ namespace smt {
sk_value = get_type_compatible_term(sk_value); sk_value = get_type_compatible_term(sk_value);
} }
func_decl * f = nullptr; 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); expr_ref body(cex->get_func_interp(f)->get_interp(), m);
ptr_vector<sort> sorts(f->get_arity(), f->get_domain()); ptr_vector<sort> sorts(f->get_arity(), f->get_domain());
svector<symbol> names; svector<symbol> names;