From dc0b2a8acfd91e77d8b7bb9a6bc49263a0dd7125 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Nov 2017 17:25:35 -0800 Subject: [PATCH] remove extension model converter Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_coi_filter.cpp | 14 +++--- src/tactic/CMakeLists.txt | 1 - src/tactic/arith/fix_dl_var_tactic.cpp | 6 +-- src/tactic/arith/lia2pb_tactic.cpp | 13 ++--- src/tactic/arith/nla2bv_tactic.cpp | 6 +-- src/tactic/arith/normalize_bounds_tactic.cpp | 13 ++--- src/tactic/arith/purify_arith_tactic.cpp | 5 +- src/tactic/arith/recover_01_tactic.cpp | 15 +++--- src/tactic/bv/bv_size_reduction_tactic.cpp | 5 +- src/tactic/bv/bvarray2uf_rewriter.cpp | 11 ++--- src/tactic/bv/bvarray2uf_rewriter.h | 6 +-- src/tactic/bv/bvarray2uf_tactic.cpp | 6 +-- src/tactic/bv/dt2bv_tactic.cpp | 6 +-- src/tactic/core/reduce_args_tactic.cpp | 14 ++---- src/tactic/core/solve_eqs_tactic.cpp | 15 ++---- src/tactic/extension_model_converter.h | 48 ------------------- src/tactic/generic_model_converter.cpp | 2 +- src/tactic/generic_model_converter.h | 2 + .../portfolio/bounded_int2bv_solver.cpp | 14 +++--- src/tactic/portfolio/enum2bv_solver.cpp | 5 +- src/tactic/sine_filter.cpp | 1 - src/tactic/ufbv/macro_finder_tactic.cpp | 6 +-- src/tactic/ufbv/quasi_macros_tactic.cpp | 6 +-- 23 files changed, 69 insertions(+), 151 deletions(-) delete mode 100644 src/tactic/extension_model_converter.h diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 31188bf43..a75c08ec4 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -21,7 +21,7 @@ Author: #include "muz/dataflow/dataflow.h" #include "muz/dataflow/reachability.h" #include "ast/ast_pp.h" -#include "tactic/extension_model_converter.h" +#include "tactic/generic_model_converter.h" namespace datalog { rule_set * mk_coi_filter::operator()(rule_set const & source) { @@ -90,10 +90,10 @@ namespace datalog { // set to false each unreached predicate if (m_context.get_model_converter()) { - extension_model_converter* mc0 = alloc(extension_model_converter, m); - for (dataflow_engine::iterator it = engine.begin(); it != engine.end(); it++) { - if (!it->m_value.is_reachable()) { - mc0->insert(it->m_key, m.mk_false()); + generic_model_converter* mc0 = alloc(generic_model_converter, m); + for (auto const& kv : engine) { + if (!kv.m_value.is_reachable()) { + mc0->add(kv.m_key, m.mk_false()); } } m_context.add_model_converter(mc0); @@ -127,7 +127,7 @@ namespace datalog { if (res && m_context.get_model_converter()) { func_decl_set::iterator end = pruned_preds.end(); func_decl_set::iterator it = pruned_preds.begin(); - extension_model_converter* mc0 = alloc(extension_model_converter, m); + generic_model_converter* mc0 = alloc(generic_model_converter, m); for (; it != end; ++it) { const rule_vector& rules = source.get_predicate_rules(*it); expr_ref_vector fmls(m); @@ -144,7 +144,7 @@ namespace datalog { } expr_ref fml(m); fml = m.mk_or(fmls.size(), fmls.c_ptr()); - mc0->insert(*it, fml); + mc0->add(*it, fml); } m_context.add_model_converter(mc0); } diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt index 04900fcbe..8e1ae8cd5 100644 --- a/src/tactic/CMakeLists.txt +++ b/src/tactic/CMakeLists.txt @@ -1,7 +1,6 @@ z3_add_component(tactic SOURCES equiv_proof_converter.cpp - extension_model_converter.cpp generic_model_converter.cpp goal.cpp goal_num_occurs.cpp diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 7ff7bd835..2abfc32ea 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -23,7 +23,7 @@ Revision History: --*/ #include "tactic/tactical.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/extension_model_converter.h" +#include "tactic/generic_model_converter.h" #include "ast/arith_decl_plugin.h" #include "ast/expr_substitution.h" #include "ast/ast_smt2_pp.h" @@ -270,8 +270,8 @@ class fix_dl_var_tactic : public tactic { m_rw.set_substitution(&subst); if (m_produce_models) { - extension_model_converter * _mc = alloc(extension_model_converter, m); - _mc->insert(var->get_decl(), zero); + generic_model_converter * _mc = alloc(generic_model_converter, m); + _mc->add(var, zero); mc = _mc; } diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index a339db51b..89c43e647 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -20,7 +20,6 @@ Revision History: #include "tactic/arith/bound_manager.h" #include "ast/rewriter/th_rewriter.h" #include "ast/for_each_expr.h" -#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h" #include "ast/arith_decl_plugin.h" #include "ast/expr_substitution.h" @@ -224,12 +223,10 @@ class lia2pb_tactic : public tactic { if (!check_num_bits()) throw tactic_exception("lia2pb failed, number of necessary bits exceeds specified threshold (use option :lia2pb-total-bits to increase threshold)"); - extension_model_converter * mc1 = 0; - generic_model_converter * mc2 = 0; + generic_model_converter * gmc = 0; if (m_produce_models) { - mc1 = alloc(extension_model_converter, m); - mc2 = alloc(generic_model_converter, m); - mc = concat(mc2, mc1); + gmc = alloc(generic_model_converter, m); + mc = gmc; } expr_ref zero(m); @@ -259,7 +256,7 @@ class lia2pb_tactic : public tactic { else def_args.push_back(m_util.mk_mul(m_util.mk_numeral(a, true), x_prime)); if (m_produce_models) - mc2->hide(x_prime->get_decl()); + gmc->hide(x_prime->get_decl()); a *= rational(2); } SASSERT(def_args.size() > 1); @@ -273,7 +270,7 @@ class lia2pb_tactic : public tactic { TRACE("lia2pb", tout << mk_ismt2_pp(x, m) << " -> " << dep << "\n";); subst.insert(x, def, 0, dep); if (m_produce_models) { - mc1->insert(to_app(x)->get_decl(), def); + gmc->add(x, def); } } } diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 00cb02cf6..547af63bf 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -26,7 +26,6 @@ Notes: #include "util/optional.h" #include "tactic/arith/bv2int_rewriter.h" #include "tactic/arith/bv2real_rewriter.h" -#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h" #include "tactic/arith/bound_manager.h" #include "util/obj_pair_hashtable.h" @@ -98,10 +97,9 @@ class nla2bv_tactic : public tactic { reduce_bv2int(g); reduce_bv2real(g); TRACE("nla2bv", g.display(tout << "after reduce\n");); - extension_model_converter * evc = alloc(extension_model_converter, m_manager); - mc = concat(m_fmc.get(), evc); + mc = m_fmc.get(); for (unsigned i = 0; i < m_vars.size(); ++i) { - evc->insert(m_vars[i].get(), m_defs[i].get()); + m_fmc->add(m_vars[i].get(), m_defs[i].get()); } for (unsigned i = 0; i < m_bv2real.num_aux_decls(); ++i) { m_fmc->hide(m_bv2real.get_aux_decl(i)); diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index 90f92f3f7..8f95dac8a 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -21,7 +21,6 @@ Revision History: #include "tactic/tactical.h" #include "tactic/arith/bound_manager.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h" #include "ast/arith_decl_plugin.h" #include "ast/expr_substitution.h" @@ -98,12 +97,10 @@ class normalize_bounds_tactic : public tactic { return; } - extension_model_converter * mc1 = 0; - generic_model_converter * mc2 = 0; + generic_model_converter * gmc = 0; if (produce_models) { - mc1 = alloc(extension_model_converter, m); - mc2 = alloc(generic_model_converter, m); - mc = concat(mc2, mc1); + gmc = alloc(generic_model_converter, m); + mc = gmc; } unsigned num_norm_bounds = 0; @@ -120,8 +117,8 @@ class normalize_bounds_tactic : public tactic { expr * def = m_util.mk_add(x_prime, m_util.mk_numeral(val, s)); subst.insert(x, def); if (produce_models) { - mc1->insert(to_app(x)->get_decl(), def); - mc2->hide(x_prime->get_decl()); + gmc->add(to_app(x)->get_decl(), def); + gmc->hide(x_prime->get_decl()); } } } diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 144a13bcd..af2b3581f 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -28,7 +28,6 @@ Revision History: #include "tactic/core/simplify_tactic.h" #include "ast/rewriter/th_rewriter.h" #include "tactic/generic_model_converter.h" -#include "tactic/extension_model_converter.h" #include "ast/ast_smt2_pp.h" #include "ast/rewriter/expr_replacer.h" @@ -776,11 +775,11 @@ struct purify_arith_proc { } } if (produce_models && !m_sin_cos.empty()) { - extension_model_converter* emc = alloc(extension_model_converter, m()); + generic_model_converter* emc = alloc(generic_model_converter, m()); mc = concat(mc.get(), emc); obj_map >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end(); for (; it != end; ++it) { - emc->insert(it->m_key->get_decl(), + emc->add(it->m_key->get_decl(), m().mk_ite(u().mk_ge(it->m_value.first, mk_real_zero()), u().mk_acos(it->m_value.second), u().mk_add(u().mk_acos(u().mk_uminus(it->m_value.second)), u().mk_pi()))); } diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index bd03f6901..9425b90ef 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -32,7 +32,6 @@ Revision History: --*/ #include "tactic/tactical.h" #include "ast/rewriter/th_rewriter.h" -#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h" #include "ast/arith_decl_plugin.h" #include "ast/expr_substitution.h" @@ -112,8 +111,7 @@ class recover_01_tactic : public tactic { } // temporary fields used by operator() and process - extension_model_converter * mc1; - generic_model_converter * mc2; + generic_model_converter * gmc; expr_substitution * subst; goal_ref new_goal; obj_map bool2int; @@ -205,8 +203,8 @@ class recover_01_tactic : public tactic { expr * bool_def = m.mk_eq(var, m_util.mk_numeral(rational(1), true)); subst->insert(atom, bool_def); if (m_produce_models) { - mc2->hide(to_app(var)->get_decl()); - mc1->insert(to_app(atom)->get_decl(), bool_def); + gmc->hide(var); + gmc->add(to_app(atom)->get_decl(), bool_def); } m.inc_ref(atom); m.inc_ref(var); @@ -288,7 +286,7 @@ class recover_01_tactic : public tactic { TRACE("recover_01", tout << x->get_name() << " --> " << mk_ismt2_pp(x_def, m) << "\n";); subst->insert(m.mk_const(x), x_def); if (m_produce_models) { - mc1->insert(x, x_def); + gmc->add(x, x_def); } return true; } @@ -328,9 +326,8 @@ class recover_01_tactic : public tactic { } if (m_produce_models) { - mc1 = alloc(extension_model_converter, m); - mc2 = alloc(generic_model_converter, m); - mc = concat(mc2, mc1); + gmc = alloc(generic_model_converter, m); + mc = gmc; } dec_ref_key_values(m, bool2int); diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index c62e1177d..4435bf6a3 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -24,7 +24,6 @@ Notes: #include "tactic/tactical.h" #include "ast/bv_decl_plugin.h" #include "ast/rewriter/expr_replacer.h" -#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h" #include "ast/ast_smt2_pp.h" @@ -51,7 +50,7 @@ tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) { struct bv_size_reduction_tactic::imp { typedef rational numeral; - typedef extension_model_converter bv_size_reduction_mc; + typedef generic_model_converter bv_size_reduction_mc; ast_manager & m; bv_util m_util; @@ -267,7 +266,7 @@ struct bv_size_reduction_tactic::imp { if (m_produce_models) { if (!m_mc) m_mc = alloc(bv_size_reduction_mc, m); - m_mc->insert(v->get_decl(), new_def); + m_mc->add(v, new_def); if (!m_fmc && new_const) m_fmc = alloc(generic_model_converter, m); if (new_const) diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index 1d96ffc35..c9efc16d6 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -37,7 +37,6 @@ bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref con m_bindings(m), m_bv_util(m), m_array_util(m), - m_emc(0), m_fmc(0), extra_assertions(m) { updt_params(p); @@ -115,9 +114,8 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) { bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range); TRACE("bvarray2uf_rw", tout << "for " << mk_ismt2_pp(e, m_manager) << " new func_decl is " << mk_ismt2_pp(bv_f, m_manager) << std::endl; ); if (is_uninterp_const(e)) { - if (m_emc) - m_emc->insert(to_app(e)->get_decl(), - m_array_util.mk_as_array(bv_f)); + if (m_fmc) + m_fmc->add(e, m_array_util.mk_as_array(bv_f)); } else if (m_fmc) m_fmc->hide(bv_f); @@ -191,9 +189,8 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range); TRACE("bvarray2uf_rw", tout << mk_ismt2_pp(e, m_manager) << " -> " << bv_f->get_name() << std::endl; ); if (is_uninterp_const(e)) { - if (m_emc) - m_emc->insert(e->get_decl(), - m_array_util.mk_as_array(bv_f)); + if (m_fmc) + m_fmc->add(e, m_array_util.mk_as_array(bv_f)); } else if (m_fmc) m_fmc->hide(bv_f); diff --git a/src/tactic/bv/bvarray2uf_rewriter.h b/src/tactic/bv/bvarray2uf_rewriter.h index 0fe5762ae..9984d3469 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.h +++ b/src/tactic/bv/bvarray2uf_rewriter.h @@ -21,7 +21,6 @@ Notes: #define BVARRAY2UF_REWRITER_H_ #include "ast/rewriter/rewriter.h" -#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h" class bvarray2uf_rewriter_cfg : public default_rewriter_cfg { @@ -30,7 +29,6 @@ class bvarray2uf_rewriter_cfg : public default_rewriter_cfg { sort_ref_vector m_bindings; bv_util m_bv_util; array_util m_array_util; - extension_model_converter * m_emc; generic_model_converter * m_fmc; obj_map m_arrays_fs; @@ -59,7 +57,7 @@ public: expr_ref_vector extra_assertions; - void set_mcs(extension_model_converter * emc, generic_model_converter * fmc) { m_emc = emc; m_fmc = fmc; } + void set_mcs(generic_model_converter * fmc) { m_fmc = fmc; } protected: sort * get_index_sort(expr * e); @@ -79,7 +77,7 @@ struct bvarray2uf_rewriter : public rewriter_tpl { m_cfg(m, p) { } - void set_mcs(extension_model_converter * emc, generic_model_converter * fmc) { m_cfg.set_mcs(emc, fmc); } + void set_mcs(generic_model_converter * fmc) { m_cfg.set_mcs(fmc); } }; #endif diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index af74a2d8f..3598a767c 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -20,7 +20,6 @@ Notes: #include "tactic/tactical.h" #include "ast/bv_decl_plugin.h" #include "ast/rewriter/expr_replacer.h" -#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h" #include "ast/ast_smt2_pp.h" @@ -68,10 +67,9 @@ class bvarray2uf_tactic : public tactic { m_produce_models = g->models_enabled(); if (m_produce_models) { - extension_model_converter * emc = alloc(extension_model_converter, m_manager); generic_model_converter * fmc = alloc(generic_model_converter, m_manager); - mc = concat(emc, fmc); - m_rw.set_mcs(emc, fmc); + mc = fmc; + m_rw.set_mcs(fmc); } diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 6a1de26fe..0d83e313a 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -26,7 +26,6 @@ Revision History: #include "ast/bv_decl_plugin.h" #include "ast/rewriter/rewriter_def.h" #include "tactic/generic_model_converter.h" -#include "tactic/extension_model_converter.h" #include "ast/rewriter/var_subst.h" #include "ast/ast_util.h" #include "ast/rewriter/enum2bv_rewriter.h" @@ -134,7 +133,6 @@ public: for (sort* s : m_non_fd_sorts) m_fd_sorts.remove(s); if (!m_fd_sorts.empty()) { - ref ext = alloc(extension_model_converter, m); ref filter = alloc(generic_model_converter, m); enum2bv_rewriter rw(m, m_params); rw.set_is_fd(&m_is_fd); @@ -155,9 +153,9 @@ public: for (auto const& kv : rw.enum2bv()) filter->hide(kv.m_value); for (auto const& kv : rw.enum2def()) - ext->insert(kv.m_key, kv.m_value); + filter->add(kv.m_key, kv.m_value); - mc = concat(filter.get(), ext.get()); + mc = filter.get(); report_tactic_progress(":fd-num-translated", rw.num_translated()); } g->inc_depth(); diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index aaf85eacd..a7a73ae61 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -22,7 +22,6 @@ Notes: #include "ast/has_free_vars.h" #include "util/map.h" #include "ast/rewriter/rewriter_def.h" -#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h" /** @@ -394,13 +393,10 @@ struct reduce_args_tactic::imp { ptr_buffer new_args; var_ref_vector new_vars(m_manager); ptr_buffer new_eqs; - extension_model_converter * e_mc = alloc(extension_model_converter, m_manager); generic_model_converter * f_mc = alloc(generic_model_converter, m_manager); - decl2arg2func_map::iterator it = decl2arg2funcs.begin(); - decl2arg2func_map::iterator end = decl2arg2funcs.end(); - for (; it != end; ++it) { - func_decl * f = it->m_key; - arg2func * map = it->m_value; + for (auto const& kv : decl2arg2funcs) { + func_decl * f = kv.m_key; + arg2func * map = kv.m_value; expr * def = 0; SASSERT(decl2args.contains(f)); bit_vector & bv = decl2args.find(f); @@ -438,9 +434,9 @@ struct reduce_args_tactic::imp { } } SASSERT(def); - e_mc->insert(f, def); + f_mc->add(f, def); } - return concat(f_mc, e_mc); + return f_mc; } void operator()(goal & g, model_converter_ref & mc) { diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 65d474182..c4f315985 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include "tactic/tactical.h" #include "ast/rewriter/expr_replacer.h" -#include "tactic/extension_model_converter.h" +#include "tactic/generic_model_converter.h" #include "ast/occurs.h" #include "util/cooperate.h" #include "tactic/goal_shared_occs.h" @@ -26,7 +26,7 @@ Revision History: class solve_eqs_tactic : public tactic { struct imp { - typedef extension_model_converter gmc; + typedef generic_model_converter gmc; ast_manager & m_manager; expr_replacer * m_r; @@ -509,10 +509,8 @@ class solve_eqs_tactic : public tactic { expr_ref new_def(m()); proof_ref new_pr(m()); expr_dependency_ref new_dep(m()); - unsigned size = m_ordered_vars.size(); - for (unsigned idx = 0; idx < size; idx++) { + for (app * v : m_ordered_vars) { checkpoint(); - expr * v = m_ordered_vars[idx]; expr * def = 0; proof * pr = 0; expr_dependency * dep = 0; @@ -609,16 +607,13 @@ class solve_eqs_tactic : public tactic { if (m_produce_models) { if (mc.get() == 0) mc = alloc(gmc, m()); - ptr_vector::iterator it = m_ordered_vars.begin(); - ptr_vector::iterator end = m_ordered_vars.end(); - for (; it != end; ++it) { - app * v = *it; + for (app * v : m_ordered_vars) { expr * def = 0; proof * pr; expr_dependency * dep; m_norm_subst->find(v, def, pr, dep); SASSERT(def != 0); - static_cast(mc.get())->insert(v->get_decl(), def); + static_cast(mc.get())->add(v, def); } } } diff --git a/src/tactic/extension_model_converter.h b/src/tactic/extension_model_converter.h deleted file mode 100644 index 26f1611ef..000000000 --- a/src/tactic/extension_model_converter.h +++ /dev/null @@ -1,48 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - extension_model_converter.h - -Abstract: - - Model converter that introduces new interpretations into a model. - It used to be called elim_var_model_converter - - TBD: special case of generic_model_converter - -Author: - - Leonardo (leonardo) 2011-10-21 - -Notes: - ---*/ -#ifndef EXTENSION_MODEL_CONVERTER_H_ -#define EXTENSION_MODEL_CONVERTER_H_ - -#include "ast/ast.h" -#include "tactic/model_converter.h" - -class extension_model_converter : public model_converter { - func_decl_ref_vector m_vars; - expr_ref_vector m_defs; -public: - extension_model_converter(ast_manager & m): m_vars(m), m_defs(m) { - } - - virtual ~extension_model_converter(); - - ast_manager & m() const { return m_vars.get_manager(); } - - virtual void operator()(model_ref & md, unsigned goal_idx); - - virtual void display(std::ostream & out); - - // register a variable that was eliminated - void insert(func_decl * v, expr * def); - - virtual model_converter * translate(ast_translation & translator); -}; -#endif diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 629004869..03361cac1 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -27,7 +27,7 @@ void generic_model_converter::operator()(model_ref & md, unsigned goal_idx) { std::cout << "model converter\n"; TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout);); model_evaluator ev(*(md.get())); - ev.set_model_completion(false); + ev.set_model_completion(true); ev.set_expand_array_equalities(false); expr_ref val(m); unsigned arity; diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index c58d0d029..014725bb0 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -43,6 +43,8 @@ public: void hide(func_decl * f) { m_entries.push_back(entry(f, 0, m, HIDE)); } void add(func_decl * d, expr* e) { m_entries.push_back(entry(d, e, m, ADD)); } + + void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); m_entries.push_back(entry(to_app(d)->get_decl(), e, m, ADD)); } virtual void operator()(model_ref & md, unsigned goal_idx); diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index ef8012dd9..bc7c5d49c 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -22,7 +22,6 @@ Notes: #include "tactic/tactic.h" #include "ast/rewriter/pb2bv_rewriter.h" #include "tactic/generic_model_converter.h" -#include "tactic/extension_model_converter.h" #include "ast/ast_pp.h" #include "model/model_smt2_pp.h" #include "tactic/arith/bound_manager.h" @@ -215,17 +214,16 @@ private: } void extend_model(model_ref& mdl) { - extension_model_converter ext(m); - obj_map::iterator it = m_int2bv.begin(), end = m_int2bv.end(); - for (; it != end; ++it) { + generic_model_converter ext(m); + for (auto const& kv : m_int2bv) { rational offset; - VERIFY (m_bv2offset.find(it->m_value, offset)); - expr_ref value(m_bv.mk_bv2int(m.mk_const(it->m_value)), m); + VERIFY (m_bv2offset.find(kv.m_value, offset)); + expr_ref value(m_bv.mk_bv2int(m.mk_const(kv.m_value)), m); if (!offset.is_zero()) { value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true)); } - TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";); - ext.insert(it->m_key, value); + TRACE("int2bv", tout << mk_pp(kv.m_key, m) << " " << value << "\n";); + ext.add(kv.m_key, value); } ext(mdl, 0); } diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 19b5374ac..50fb7d925 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -25,7 +25,6 @@ Notes: #include "ast/ast_pp.h" #include "model/model_smt2_pp.h" #include "tactic/tactic.h" -#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h" #include "tactic/portfolio/enum2bv_solver.h" #include "solver/solver_na2as.h" @@ -172,9 +171,9 @@ public: } void extend_model(model_ref& mdl) { - extension_model_converter ext(m); + generic_model_converter ext(m); for (auto const& kv : m_rewriter.enum2def()) - ext.insert(kv.m_key, kv.m_value); + ext.add(kv.m_key, kv.m_value); ext(mdl, 0); } diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 1e0eabac6..64689602c 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -21,7 +21,6 @@ Revision History: #include "tactic/generic_model_converter.h" #include "ast/datatype_decl_plugin.h" #include "ast/rewriter/rewriter_def.h" -#include "tactic/extension_model_converter.h" #include "ast/rewriter/var_subst.h" #include "ast/ast_util.h" #include "util/obj_pair_hashtable.h" diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 3a482f37c..7a1838452 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -19,7 +19,7 @@ Notes: #include "tactic/tactical.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" -#include "tactic/extension_model_converter.h" +#include "tactic/generic_model_converter.h" #include "tactic/ufbv/macro_finder_tactic.h" class macro_finder_tactic : public tactic { @@ -69,12 +69,12 @@ class macro_finder_tactic : public tactic { produce_proofs ? new_proofs.get(i) : 0, unsat_core_enabled ? new_deps.get(i) : 0); - extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager()); + generic_model_converter * evmc = alloc(generic_model_converter, mm.get_manager()); unsigned num = mm.get_num_macros(); for (unsigned i = 0; i < num; i++) { expr_ref f_interp(mm.get_manager()); func_decl * f = mm.get_macro_interpretation(i, f_interp); - evmc->insert(f, f_interp); + evmc->add(f, f_interp); } mc = evmc; diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 925b5a5e3..ee3cd14ec 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -17,9 +17,9 @@ Notes: --*/ #include "tactic/tactical.h" +#include "tactic/generic_model_converter.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" -#include "tactic/extension_model_converter.h" #include "ast/macros/quasi_macros.h" #include "tactic/ufbv/quasi_macros_tactic.h" @@ -81,12 +81,12 @@ class quasi_macros_tactic : public tactic { produce_proofs ? proofs.get(i) : 0, produce_unsat_cores ? deps.get(i) : 0); - extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager()); + generic_model_converter * evmc = alloc(generic_model_converter, mm.get_manager()); unsigned num = mm.get_num_macros(); for (unsigned i = 0; i < num; i++) { expr_ref f_interp(mm.get_manager()); func_decl * f = mm.get_macro_interpretation(i, f_interp); - evmc->insert(f, f_interp); + evmc->add(f, f_interp); } mc = evmc;