From fe3f8466b67e4a4a868c87920a4019dc6aba6baf Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 21 May 2016 18:08:48 +0100 Subject: [PATCH] Partial support for fpa2bv translation in complex types. --- src/ast/fpa/fpa2bv_converter.cpp | 191 +++++++++++++++++----- src/ast/fpa/fpa2bv_converter.h | 11 +- src/ast/fpa/fpa2bv_rewriter.cpp | 40 ++--- src/ast/fpa_decl_plugin.cpp | 63 ++++++- src/ast/fpa_decl_plugin.h | 4 +- src/tactic/fpa/fpa2bv_model_converter.cpp | 17 ++ src/tactic/fpa/fpa2bv_model_converter.h | 10 ++ 7 files changed, 266 insertions(+), 70 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d5849a1fd..c103f6773 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -33,6 +33,9 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m_util(m), m_bv_util(m), m_arith_util(m), + m_array_util(m), + m_dt_util(m), + m_seq_util(m), m_mpf_manager(m_util.fm()), m_mpz_manager(m_mpf_manager.mpz_manager()), m_hi_fp_unspecified(true), @@ -46,11 +49,10 @@ fpa2bv_converter::~fpa2bv_converter() { void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { if (is_float(a) && is_float(b)) { - SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP)); - SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP)); + SASSERT(m_util.is_fp(a) && m_util.is_fp(b)); TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl; - tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;); + tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;); expr_ref eq_sgn(m), eq_exp(m), eq_sig(m); m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn); @@ -77,11 +79,10 @@ 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)); - SASSERT(m_util.is_rm_bvwrap(a)); + SASSERT(m_util.is_rm_bvwrap(b) && m_util.is_rm_bvwrap(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;); + tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;); m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result); } @@ -90,8 +91,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { } void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { - SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FPA_FP)); - SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FPA_FP)); + SASSERT(m_util.is_fp(t) && m_util.is_fp(f)); expr *t_sgn, *t_sig, *t_exp; expr *f_sgn, *f_sig, *f_exp; @@ -244,46 +244,119 @@ void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * co } sort_ref fpa2bv_converter::replace_float_sorts(sort * s) { - sort_ref ns(m); + sort_ref ns(m); - if (m_util.is_float(s)) - ns = m_bv_util.mk_sort(m_util.get_sbits(s) + m_util.get_ebits(s)); - else if (m_util.is_rm(s)) - ns = m_bv_util.mk_sort(3); - else - ns = s; + sort * found_sort; + if (m_subst_sorts.find(s, found_sort)) { + ns = found_sort; + } + else { + if (m_util.is_float(s)) + ns = m_bv_util.mk_sort(m_util.get_sbits(s) + m_util.get_ebits(s)); + else if (m_util.is_rm(s)) + ns = m_bv_util.mk_sort(3); + else if (m_array_util.is_array(s)) { + SASSERT(s->get_num_parameters() > 0); + vector new_params; + unsigned num_params = s->get_num_parameters(); + for (unsigned i = 0; i < num_params; i++) + { + parameter const & pi = s->get_parameter(i); + if (pi.is_ast() && is_sort(pi.get_ast())) { + sort_ref nsrt(m); + nsrt = replace_float_sorts(to_sort(pi.get_ast())); + parameter np((ast*)nsrt); + new_params.push_back(np); + } + else + new_params.push_back(pi); + } + ns = m.mk_sort(s->get_family_id(), s->get_decl_kind(), new_params.size(), new_params.c_ptr()); + } + else if (m_dt_util.is_datatype(s)) { + TRACE("fpa2bv", tout << "datatype:"; m_dt_util.display_datatype(s, tout); ); + bool is_recursive = m_dt_util.is_recursive(s); + SASSERT(!is_recursive); + ptr_vector const * cs = m_dt_util.get_datatype_constructors(s); + ptr_vector new_css; + bool has_news = false; + for (unsigned i = 0; i < cs->size(); i++) { + func_decl * cf = cs->get(i); + func_decl * rf = m_dt_util.get_constructor_recognizer(cf); + ptr_vector new_rf; + ptr_vector const * cas = m_dt_util.get_constructor_accessors(cf); + ptr_vector new_cas; + for (unsigned j = 0; j < cas->size(); j++) { + func_decl * ca = cas->get(j); + sort * s1 = ca->get_range(); + sort_ref s1r(m); + s1r = replace_float_sorts(s1); - if (ns->get_num_parameters() != 0) { - vector new_params; - unsigned num_params = ns->get_num_parameters(); - for (unsigned i = 0; i < num_params; i++) - { - parameter const & pi = ns->get_parameter(i); - if (pi.is_ast() && pi.get_ast()->get_kind() == AST_SORT) { - sort_ref nsrt(m); - nsrt = replace_float_sorts(to_sort(pi.get_ast())); - parameter np = parameter((ast*)nsrt); - new_params.push_back(np); + symbol name(ca->get_name()); + if (s1r != s1) { + std::stringstream ss; + ss << name << "!fpa2bv"; + name = symbol(ss.str().c_str()); + has_news = true; + } + + accessor_decl * ad = mk_accessor_decl(name, type_ref(s1r)); + new_cas.push_back(ad); + } + + constructor_decl * cd = 0; + symbol name(cf->get_name()); + symbol rf_name(rf->get_name()); + + if (has_news) { + std::stringstream ss; + ss << name << "!fpa2bv"; + name = symbol(ss.str().c_str()); + std::stringstream ss2; + ss2 << rf_name << "!fpa2bv"; + rf_name = symbol(ss2.str().c_str()); + } + + cd = mk_constructor_decl(name, rf_name, new_cas.size(), new_cas.c_ptr()); + new_css.push_back(cd); + } + + if (has_news) { + std::stringstream ss; + ss << s->get_name() << "!fpa2bv"; + symbol name(ss.str().c_str()); + datatype_decl * dtd = mk_datatype_decl(name, new_css.size(), new_css.c_ptr()); + datatype_decl_plugin * dtp = static_cast(m.get_plugin(m.mk_family_id("datatype"))); + sort_ref_vector sorts(m); + bool is_ok = dtp->mk_datatypes(1, &dtd, sorts); + SASSERT(is_ok); + ns = sorts.get(0); + TRACE("fpa2bv", tout << "new datatype:"; m_dt_util.display_datatype(ns, tout); ); } else - new_params.push_back(pi); + ns = s; } + else if (m_seq_util.is_seq(s)) { + NOT_IMPLEMENTED_YET(); + } + else + ns = s; - TRACE("fpa2bv", tout << "New sort params:"; - for (unsigned i = 0; i < new_params.size(); i++) - tout << " " << new_params[i]; - tout << std::endl;); - - ns = m.mk_sort(ns->get_family_id(), ns->get_decl_kind(), new_params.size(), new_params.c_ptr()); + if (ns != s) { + m_subst_sorts.insert(s, ns); + m.inc_ref(s); + m.inc_ref(ns); + } } + SASSERT(ns != 0); TRACE("fpa2bv", tout << "sorts replaced: " << mk_ismt2_pp(s, m) << " --> " << mk_ismt2_pp(ns, m) << std::endl; ); return ns; } func_decl_ref fpa2bv_converter::replace_function(func_decl * f) { TRACE("fpa2bv", tout << "replacing: " << mk_ismt2_pp(f, m) << std::endl;); - func_decl_ref res(m); + func_decl_ref res(m); sort_ref_buffer new_domain(m); for (unsigned i = 0; i < f->get_arity(); i++) { @@ -308,18 +381,44 @@ func_decl_ref fpa2bv_converter::replace_function(func_decl * f) { } else { - TRACE("fpa2bv", tout << "New domain:"; - for (unsigned i = 0; i < new_domain.size(); i++) - tout << " " << mk_ismt2_pp(new_domain[i], m); - tout << std::endl;); + TRACE("fpa2bv", tout << "Old domain:" << std::endl; + for (unsigned i = 0; i < f->get_arity(); i++) { + if (m_dt_util.is_datatype(f->get_domain(i))) + m_dt_util.display_datatype(f->get_domain(i), tout); + else + tout << mk_ismt2_pp(f->get_domain(i), m); + tout << std::endl; + }); + + TRACE("fpa2bv", tout << "New domain:" << std::endl; + for (unsigned i = 0; i < new_domain.size(); i++) { + if (m_dt_util.is_datatype(new_domain[i])) + m_dt_util.display_datatype(new_domain[i], tout); + else + tout << mk_ismt2_pp(new_domain[i], m); + tout << std::endl; + }); + + vector new_params; + for (unsigned i = 0; i < f->get_num_parameters(); i++) { + parameter const & pi = f->get_parameter(i); + if (pi.is_ast() && is_sort(pi.get_ast())) { + sort_ref ns(m); + ns = replace_float_sorts(to_sort(pi.get_ast())); + parameter np((ast*)ns); + new_params.push_back(np); + } + else + new_params.push_back(pi); + } res = m.mk_func_decl(f->get_family_id(), f->get_decl_kind(), - f->get_num_parameters(), f->get_parameters(), + new_params.size(), new_params.c_ptr(), new_domain.size(), new_domain.c_ptr(), new_range); - TRACE("fpa2bv", tout << "New IF func_decl: " << mk_ismt2_pp(res, m) << std::endl;); + TRACE("fpa2bv", tout << "IF func_decl: " << mk_ismt2_pp(res, m) << std::endl;); } } - + return res; } @@ -391,7 +490,8 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a for (unsigned i = 0; i < num; i++) new_args.push_back(replace_float_arg(args[i])); - TRACE("fpa2bv", tout << "UF bv-args:"; + + CTRACE("fpa2bv", num > 0, tout << "UF bv-args:"; for (unsigned i = 0; i < num; i++) tout << " " << mk_ismt2_pp(new_args[i], m); tout << std::endl; ); @@ -400,7 +500,11 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a rf = replace_function(f); mk_function_output(f->get_range(), rf, new_args.c_ptr(), result); - TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; ); + TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; + tout << "old: " << mk_ismt2_pp(f->get_range(), m) << std::endl; + tout << "new: " << mk_ismt2_pp(m.get_sort(result), m) << std::endl; + tout << "equal: " << (f->get_range() == m.get_sort(result)) << std::endl;); + SASSERT(is_well_sorted(m, result)); } @@ -4118,6 +4222,7 @@ void fpa2bv_converter::reset(void) { dec_ref_map_key_values(m, m_const2bv); dec_ref_map_key_values(m, m_rm_const2bv); dec_ref_map_key_values(m, m_uf2bvuf); + dec_ref_map_key_values(m, m_subst_sorts); for (obj_map >::iterator it = m_specials.begin(); it != m_specials.end(); it++) { diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 879c1e080..17648917f 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -24,6 +24,11 @@ Notes: #include"ref_util.h" #include"fpa_decl_plugin.h" #include"bv_decl_plugin.h" +#include"array_decl_plugin.h" +#include"datatype_decl_plugin.h" +#include"dl_decl_plugin.h" +#include"pb_decl_plugin.h" +#include"seq_decl_plugin.h" #include"basic_simplifier_plugin.h" class fpa2bv_converter { @@ -33,6 +38,9 @@ protected: fpa_util m_util; bv_util m_bv_util; arith_util m_arith_util; + array_util m_array_util; + datatype_util m_dt_util; + seq_util m_seq_util; mpf_manager & m_mpf_manager; unsynch_mpz_manager & m_mpz_manager; fpa_decl_plugin * m_plugin; @@ -41,6 +49,7 @@ protected: obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; + obj_map m_subst_sorts; obj_map > m_specials; @@ -145,7 +154,7 @@ public: expr_ref_vector m_extra_assertions; bool is_special(func_decl * f) { return m_specials.contains(f); } - bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); } + bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); } protected: void mk_one(func_decl *f, expr_ref & sign, expr_ref & result); diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 2eb85c87c..2a66da8d7 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -71,7 +71,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co if (m().is_eq(f)) { SASSERT(num == 2); TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << - mk_ismt2_pp(args[1], m()) << ")" << std::endl;); + mk_ismt2_pp(args[1], m()) << ")" << std::endl;); SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); sort * ds = f->get_domain()[0]; if (m_conv.is_float(ds)) { @@ -83,7 +83,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co return BR_DONE; } return BR_FAILED; - } + } else if (m().is_ite(f)) { SASSERT(num == 3); if (m_conv.is_float(args[1])) { @@ -100,7 +100,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co } return BR_FAILED; } - + if (m_conv.is_float_family(f)) { switch (f->get_decl_kind()) { case OP_FPA_RM_NEAREST_TIES_TO_AWAY: @@ -166,16 +166,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co NOT_IMPLEMENTED_YET(); } } - else { - SASSERT(!m_conv.is_float_family(f)); - bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range()); - - for (unsigned i = 0; i < f->get_arity(); i++) { - sort * di = f->get_domain()[i]; - is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di); - } - - if (is_float_uf) { + else if (f->get_arity() > 0 && !m_conv.is_float_family(f)) { + expr_ref q(m().mk_app(f, num, args), m()); + if (m_conv.fu().contains_floats(q)) { m_conv.mk_function(f, num, args, result); return BR_DONE; } @@ -249,17 +242,16 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res expr_ref new_exp(m()); sort * s = t->get_sort(); - if (m_conv.is_float(s)) - { - expr_ref new_var(m()); - unsigned ebits = m_conv.fu().get_ebits(s); - unsigned sbits = m_conv.fu().get_sbits(s); - new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); - m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), - m_conv.bu().mk_extract(ebits - 1, 0, new_var), - m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), - new_exp); - } + if (m_conv.is_float(s)) { + expr_ref new_var(m()); + unsigned ebits = m_conv.fu().get_ebits(s); + unsigned sbits = m_conv.fu().get_sbits(s); + new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); + m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), + m_conv.bu().mk_extract(ebits - 1, 0, new_var), + m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), + new_exp); + } else new_exp = m().mk_var(t->get_idx(), s); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 069e7ed18..22043e7a4 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -691,7 +691,7 @@ func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters } func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { + unsigned arity, sort * const * domain, sort * range) { if (arity != 1) m_manager->raise_exception("invalid number of arguments to bv_wrap"); if (!is_float_sort(domain[0]) && !is_rm_sort(domain[0])) @@ -1076,3 +1076,64 @@ app * fpa_util::mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits) sort * range = m_a_util.mk_real(); return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range); } + +bool fpa_util::contains_floats(ast * a) { + switch (a->get_kind()) { + case AST_APP: { + app * aa = to_app(a); + if (contains_floats(aa->get_decl())) + return true; + else + for (unsigned i = 0; i < aa->get_num_args(); i++) + if (contains_floats(aa->get_arg(i))) + return true; + break; + } + case AST_VAR: + return contains_floats(to_var(a)->get_sort()); + break; + case AST_QUANTIFIER: { + quantifier * q = to_quantifier(a); + for (unsigned i = 0; i < q->get_num_children(); i++) + if (contains_floats(q->get_child(i))) + return true; + for (unsigned i = 0; i < q->get_num_decls(); i++) + if (contains_floats(q->get_decl_sort(i))) + return true; + if (contains_floats(q->get_expr())) + return true; + break; + } + case AST_SORT: { + sort * s = to_sort(a); + if (is_float(s) || is_rm(s)) + return true; + else { + for (unsigned i = 0; i < s->get_num_parameters(); i++) { + parameter const & pi = s->get_parameter(i); + if (pi.is_ast() && contains_floats(pi.get_ast())) + return true; + } + } + break; + } + case AST_FUNC_DECL: { + func_decl * f = to_func_decl(a); + for (unsigned i = 0; i < f->get_arity(); i++) + if (contains_floats(f->get_domain(i))) + return true; + if (contains_floats(f->get_range())) + return true; + for (unsigned i = 0; i < f->get_num_parameters(); i++) { + parameter const & pi = f->get_parameter(i); + if (pi.is_ast() && contains_floats(pi.get_ast())) + return true; + } + break; + } + default: + UNREACHABLE(); + } + + return false; +} diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 8683bf5f1..725e7371a 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -370,7 +370,9 @@ 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_rm_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_RM_BVWRAP; } + + bool contains_floats(ast * a); }; #endif diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 37e9942e9..db8b13913 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -46,6 +46,12 @@ void fpa2bv_model_converter::display(std::ostream & out) { unsigned indent = n.size() + 4; out << mk_ismt2_pp(it->m_value, m, indent) << ")"; } + for (obj_map::iterator it = m_subst_sorts.begin(); + it != m_subst_sorts.end(); + it++) { + out << "\n " << mk_ismt2_pp(it->m_key, m) << " -> "; + out << mk_ismt2_pp(it->m_value, m); + } for (obj_map >::iterator it = m_specials.begin(); it != m_specials.end(); it++) { @@ -55,6 +61,7 @@ void fpa2bv_model_converter::display(std::ostream & out) { out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " << mk_ismt2_pp(it->m_value.second, m, indent) << ")"; } + out << ")"; } model_converter * fpa2bv_model_converter::translate(ast_translation & translator) { @@ -88,6 +95,15 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator translator.to().inc_ref(k); translator.to().inc_ref(v); } + for (obj_map::iterator it = m_subst_sorts.begin(); + it != m_subst_sorts.end(); + it++) { + sort * k = translator(it->m_key); + sort * v = translator(it->m_value); + res->m_subst_sorts.insert(k, v); + translator.to().inc_ref(k); + translator.to().inc_ref(v); + } for (obj_map >::iterator it = m_specials.begin(); it != m_specials.end(); it++) { @@ -410,6 +426,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { } else { // Just keep. + SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range())); expr_ref val(m); bv_mdl->eval(it->m_value, val); if (val) float_mdl->register_decl(f, val); diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index ce38527c1..bb7c78067 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -32,6 +32,7 @@ class fpa2bv_model_converter : public model_converter { obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; + obj_map m_subst_sorts; obj_map > m_specials; public: @@ -64,6 +65,14 @@ public: m.inc_ref(it->m_key); m.inc_ref(it->m_value); } + for (obj_map::iterator it = conv.m_subst_sorts.begin(); + it != conv.m_subst_sorts.end(); + it++) + { + m_subst_sorts.insert(it->m_key, it->m_value); + m.inc_ref(it->m_key); + m.inc_ref(it->m_value); + } for (obj_map >::iterator it = conv.m_specials.begin(); it != conv.m_specials.end(); it++) { @@ -78,6 +87,7 @@ public: dec_ref_map_key_values(m, m_const2bv); dec_ref_map_key_values(m, m_rm_const2bv); dec_ref_map_key_values(m, m_uf2bvuf); + dec_ref_map_key_values(m, m_subst_sorts); for (obj_map >::iterator it = m_specials.begin(); it != m_specials.end(); it++) {