mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
Make fpa2bv debug symbol names optional
This commit is contained in:
parent
515a2a771e
commit
f1acc4b78a
|
@ -346,7 +346,7 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
|
||||||
app * a0 = to_app(val->get_arg(0));
|
app * a0 = to_app(val->get_arg(0));
|
||||||
|
|
||||||
expr_ref v0(m), v1(m), v2(m);
|
expr_ref v0(m), v1(m), v2(m);
|
||||||
#ifdef Z3DEBUG
|
#ifdef Z3DEBUG_FPA2BV_NAMES
|
||||||
app * a1 = to_app(val->get_arg(1));
|
app * a1 = to_app(val->get_arg(1));
|
||||||
app * a2 = to_app(val->get_arg(2));
|
app * a2 = to_app(val->get_arg(2));
|
||||||
v0 = mc->get_const_interp(a0->get_decl());
|
v0 = mc->get_const_interp(a0->get_decl());
|
||||||
|
@ -378,7 +378,7 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
|
||||||
|
|
||||||
SASSERT(val->is_app_of(m_fpa_util.get_family_id(), OP_FPA_FP));
|
SASSERT(val->is_app_of(m_fpa_util.get_family_id(), OP_FPA_FP));
|
||||||
|
|
||||||
#ifdef Z3DEBUG
|
#ifdef Z3DEBUG_FPA2BV_NAMES
|
||||||
SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0);
|
SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0);
|
||||||
SASSERT(to_app(val->get_arg(1))->get_decl()->get_arity() == 0);
|
SASSERT(to_app(val->get_arg(1))->get_decl()->get_arity() == 0);
|
||||||
SASSERT(to_app(val->get_arg(2))->get_decl()->get_arity() == 0);
|
SASSERT(to_app(val->get_arg(2))->get_decl()->get_arity() == 0);
|
||||||
|
@ -386,9 +386,10 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
|
||||||
seen.insert(to_app(val->get_arg(1))->get_decl());
|
seen.insert(to_app(val->get_arg(1))->get_decl());
|
||||||
seen.insert(to_app(val->get_arg(2))->get_decl());
|
seen.insert(to_app(val->get_arg(2))->get_decl());
|
||||||
#else
|
#else
|
||||||
SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT);
|
SASSERT(is_app(val->get_arg(0)));
|
||||||
SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT);
|
SASSERT(m_bv_util.is_extract(val->get_arg(0)));
|
||||||
seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl());
|
seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl());
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
if (!sgn && !sig && !exp)
|
if (!sgn && !sig && !exp)
|
||||||
|
|
|
@ -192,7 +192,7 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
|
||||||
|
|
||||||
app_ref sgn(m), s(m), e(m);
|
app_ref sgn(m), s(m), e(m);
|
||||||
|
|
||||||
#ifdef Z3DEBUG
|
#ifdef Z3DEBUG_FPA2BV_NAMES
|
||||||
std::string p("fpa2bv");
|
std::string p("fpa2bv");
|
||||||
std::string name = f->get_name().str();
|
std::string name = f->get_name().str();
|
||||||
|
|
||||||
|
@ -326,7 +326,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
|
||||||
|
|
||||||
expr_ref bv3(m);
|
expr_ref bv3(m);
|
||||||
bv3 = m.mk_fresh_const(
|
bv3 = m.mk_fresh_const(
|
||||||
#ifdef Z3DEBUG
|
#ifdef Z3DEBUG_FPA2BV_NAMES
|
||||||
"fpa2bv_rm"
|
"fpa2bv_rm"
|
||||||
#else
|
#else
|
||||||
nullptr
|
nullptr
|
||||||
|
@ -3839,7 +3839,7 @@ void fpa2bv_converter::mk_rounding_mode(decl_kind k, expr_ref & result)
|
||||||
}
|
}
|
||||||
|
|
||||||
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
|
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
|
||||||
#ifdef Z3DEBUG
|
#ifdef Z3DEBUG_FPA2BV_NAMES
|
||||||
return;
|
return;
|
||||||
// CMW: This works only for quantifier-free formulas.
|
// CMW: This works only for quantifier-free formulas.
|
||||||
if (m_util.is_fp(e)) {
|
if (m_util.is_fp(e)) {
|
||||||
|
|
Loading…
Reference in a new issue