mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

remove extension model converter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-17 17:25:35 -08:00
parent 0d15b6abb7
commit dc0b2a8acf
23 changed files with 69 additions and 151 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -21,7 +21,7 @@ Author:
#include "muz/dataflow/dataflow.h" #include "muz/dataflow/dataflow.h"
#include "muz/dataflow/reachability.h" #include "muz/dataflow/reachability.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h"
namespace datalog { namespace datalog {
rule_set * mk_coi_filter::operator()(rule_set const & source) { rule_set * mk_coi_filter::operator()(rule_set const & source) {
@ -90,10 +90,10 @@ namespace datalog {
// set to false each unreached predicate // set to false each unreached predicate
if (m_context.get_model_converter()) { if (m_context.get_model_converter()) {
extension_model_converter* mc0 = alloc(extension_model_converter, m); generic_model_converter* mc0 = alloc(generic_model_converter, m);
for (dataflow_engine<reachability_info>::iterator it = engine.begin(); it != engine.end(); it++) { for (auto const& kv : engine) {
if (!it->m_value.is_reachable()) { if (!kv.m_value.is_reachable()) {
mc0->insert(it->m_key, m.mk_false()); mc0->add(kv.m_key, m.mk_false());
} }
} }
m_context.add_model_converter(mc0); m_context.add_model_converter(mc0);
@ -127,7 +127,7 @@ namespace datalog {
if (res && m_context.get_model_converter()) { if (res && m_context.get_model_converter()) {
func_decl_set::iterator end = pruned_preds.end(); func_decl_set::iterator end = pruned_preds.end();
func_decl_set::iterator it = pruned_preds.begin(); 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) { for (; it != end; ++it) {
const rule_vector& rules = source.get_predicate_rules(*it); const rule_vector& rules = source.get_predicate_rules(*it);
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
@ -144,7 +144,7 @@ namespace datalog {
} }
expr_ref fml(m); expr_ref fml(m);
fml = m.mk_or(fmls.size(), fmls.c_ptr()); fml = m.mk_or(fmls.size(), fmls.c_ptr());
mc0->insert(*it, fml); mc0->add(*it, fml);
} }
m_context.add_model_converter(mc0); m_context.add_model_converter(mc0);
} }

1
src/tactic/CMakeLists.txt
View file

@ -1,7 +1,6 @@
z3_add_component(tactic z3_add_component(tactic
SOURCES SOURCES
equiv_proof_converter.cpp equiv_proof_converter.cpp
extension_model_converter.cpp
generic_model_converter.cpp generic_model_converter.cpp
goal.cpp goal.cpp
goal_num_occurs.cpp goal_num_occurs.cpp

6
src/tactic/arith/fix_dl_var_tactic.cpp
View file

@ -23,7 +23,7 @@ Revision History:
--*/ --*/
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "ast/rewriter/th_rewriter.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/arith_decl_plugin.h"
#include "ast/expr_substitution.h" #include "ast/expr_substitution.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
@ -270,8 +270,8 @@ class fix_dl_var_tactic : public tactic {
m_rw.set_substitution(&subst); m_rw.set_substitution(&subst);
if (m_produce_models) { if (m_produce_models) {
extension_model_converter * _mc = alloc(extension_model_converter, m); generic_model_converter * _mc = alloc(generic_model_converter, m);
_mc->insert(var->get_decl(), zero); _mc->add(var, zero);
mc = _mc; mc = _mc;
} }

13
src/tactic/arith/lia2pb_tactic.cpp
View file

@ -20,7 +20,6 @@ Revision History:
#include "tactic/arith/bound_manager.h" #include "tactic/arith/bound_manager.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "ast/for_each_expr.h" #include "ast/for_each_expr.h"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/expr_substitution.h" #include "ast/expr_substitution.h"
@ -224,12 +223,10 @@ class lia2pb_tactic : public tactic {
if (!check_num_bits()) if (!check_num_bits())
throw tactic_exception("lia2pb failed, number of necessary bits exceeds specified threshold (use option :lia2pb-total-bits to increase threshold)"); 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 * gmc = 0;
generic_model_converter * mc2 = 0;
if (m_produce_models) { if (m_produce_models) {
mc1 = alloc(extension_model_converter, m); gmc = alloc(generic_model_converter, m);
mc2 = alloc(generic_model_converter, m); mc = gmc;
mc = concat(mc2, mc1);
} }
expr_ref zero(m); expr_ref zero(m);
@ -259,7 +256,7 @@ class lia2pb_tactic : public tactic {
else else
def_args.push_back(m_util.mk_mul(m_util.mk_numeral(a, true), x_prime)); def_args.push_back(m_util.mk_mul(m_util.mk_numeral(a, true), x_prime));
if (m_produce_models) if (m_produce_models)
mc2->hide(x_prime->get_decl()); gmc->hide(x_prime->get_decl());
a *= rational(2); a *= rational(2);
} }
SASSERT(def_args.size() > 1); SASSERT(def_args.size() > 1);
@ -273,7 +270,7 @@ class lia2pb_tactic : public tactic {
TRACE("lia2pb", tout << mk_ismt2_pp(x, m) << " -> " << dep << "\n";); TRACE("lia2pb", tout << mk_ismt2_pp(x, m) << " -> " << dep << "\n";);
subst.insert(x, def, 0, dep); subst.insert(x, def, 0, dep);
if (m_produce_models) { if (m_produce_models) {
mc1->insert(to_app(x)->get_decl(), def); gmc->add(x, def);
} }
} }
} }

6
src/tactic/arith/nla2bv_tactic.cpp
View file

@ -26,7 +26,6 @@ Notes:
#include "util/optional.h" #include "util/optional.h"
#include "tactic/arith/bv2int_rewriter.h" #include "tactic/arith/bv2int_rewriter.h"
#include "tactic/arith/bv2real_rewriter.h" #include "tactic/arith/bv2real_rewriter.h"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "tactic/arith/bound_manager.h" #include "tactic/arith/bound_manager.h"
#include "util/obj_pair_hashtable.h" #include "util/obj_pair_hashtable.h"
@ -98,10 +97,9 @@ class nla2bv_tactic : public tactic {
reduce_bv2int(g); reduce_bv2int(g);
reduce_bv2real(g); reduce_bv2real(g);
TRACE("nla2bv", g.display(tout << "after reduce\n");); TRACE("nla2bv", g.display(tout << "after reduce\n"););
extension_model_converter * evc = alloc(extension_model_converter, m_manager); mc = m_fmc.get();
mc = concat(m_fmc.get(), evc);
for (unsigned i = 0; i < m_vars.size(); ++i) { 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) { for (unsigned i = 0; i < m_bv2real.num_aux_decls(); ++i) {
m_fmc->hide(m_bv2real.get_aux_decl(i)); m_fmc->hide(m_bv2real.get_aux_decl(i));

13
src/tactic/arith/normalize_bounds_tactic.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "tactic/arith/bound_manager.h" #include "tactic/arith/bound_manager.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/expr_substitution.h" #include "ast/expr_substitution.h"
@ -98,12 +97,10 @@ class normalize_bounds_tactic : public tactic {
return; return;
} }
extension_model_converter * mc1 = 0; generic_model_converter * gmc = 0;
generic_model_converter * mc2 = 0;
if (produce_models) { if (produce_models) {
mc1 = alloc(extension_model_converter, m); gmc = alloc(generic_model_converter, m);
mc2 = alloc(generic_model_converter, m); mc = gmc;
mc = concat(mc2, mc1);
} }
unsigned num_norm_bounds = 0; 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)); expr * def = m_util.mk_add(x_prime, m_util.mk_numeral(val, s));
subst.insert(x, def); subst.insert(x, def);
if (produce_models) { if (produce_models) {
mc1->insert(to_app(x)->get_decl(), def); gmc->add(to_app(x)->get_decl(), def);
mc2->hide(x_prime->get_decl()); gmc->hide(x_prime->get_decl());
} }
} }
} }

5
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -28,7 +28,6 @@ Revision History:
#include "tactic/core/simplify_tactic.h" #include "tactic/core/simplify_tactic.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "tactic/extension_model_converter.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/expr_replacer.h"
@ -776,11 +775,11 @@ struct purify_arith_proc {
} }
} }
if (produce_models && !m_sin_cos.empty()) { 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); mc = concat(mc.get(), emc);
obj_map<app, std::pair<expr*,expr*> >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end(); obj_map<app, std::pair<expr*,expr*> >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end();
for (; it != end; ++it) { 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), 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()))); u().mk_add(u().mk_acos(u().mk_uminus(it->m_value.second)), u().mk_pi())));
} }

15
src/tactic/arith/recover_01_tactic.cpp
View file

@ -32,7 +32,6 @@ Revision History:
--*/ --*/
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/expr_substitution.h" #include "ast/expr_substitution.h"
@ -112,8 +111,7 @@ class recover_01_tactic : public tactic {
} }
// temporary fields used by operator() and process // temporary fields used by operator() and process
extension_model_converter * mc1; generic_model_converter * gmc;
generic_model_converter * mc2;
expr_substitution * subst; expr_substitution * subst;
goal_ref new_goal; goal_ref new_goal;
obj_map<expr, expr *> bool2int; obj_map<expr, expr *> 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)); expr * bool_def = m.mk_eq(var, m_util.mk_numeral(rational(1), true));
subst->insert(atom, bool_def); subst->insert(atom, bool_def);
if (m_produce_models) { if (m_produce_models) {
mc2->hide(to_app(var)->get_decl()); gmc->hide(var);
mc1->insert(to_app(atom)->get_decl(), bool_def); gmc->add(to_app(atom)->get_decl(), bool_def);
} }
m.inc_ref(atom); m.inc_ref(atom);
m.inc_ref(var); 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";); TRACE("recover_01", tout << x->get_name() << " --> " << mk_ismt2_pp(x_def, m) << "\n";);
subst->insert(m.mk_const(x), x_def); subst->insert(m.mk_const(x), x_def);
if (m_produce_models) { if (m_produce_models) {
mc1->insert(x, x_def); gmc->add(x, x_def);
} }
return true; return true;
} }
@ -328,9 +326,8 @@ class recover_01_tactic : public tactic {
} }
if (m_produce_models) { if (m_produce_models) {
mc1 = alloc(extension_model_converter, m); gmc = alloc(generic_model_converter, m);
mc2 = alloc(generic_model_converter, m); mc = gmc;
mc = concat(mc2, mc1);
} }
dec_ref_key_values(m, bool2int); dec_ref_key_values(m, bool2int);

5
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -24,7 +24,6 @@ Notes:
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/expr_replacer.h"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "ast/ast_smt2_pp.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 { struct bv_size_reduction_tactic::imp {
typedef rational numeral; typedef rational numeral;
typedef extension_model_converter bv_size_reduction_mc; typedef generic_model_converter bv_size_reduction_mc;
ast_manager & m; ast_manager & m;
bv_util m_util; bv_util m_util;
@ -267,7 +266,7 @@ struct bv_size_reduction_tactic::imp {
if (m_produce_models) { if (m_produce_models) {
if (!m_mc) if (!m_mc)
m_mc = alloc(bv_size_reduction_mc, m); 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) if (!m_fmc && new_const)
m_fmc = alloc(generic_model_converter, m); m_fmc = alloc(generic_model_converter, m);
if (new_const) if (new_const)

11
src/tactic/bv/bvarray2uf_rewriter.cpp
View file

@ -37,7 +37,6 @@ bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref con
m_bindings(m), m_bindings(m),
m_bv_util(m), m_bv_util(m),
m_array_util(m), m_array_util(m),
m_emc(0),
m_fmc(0), m_fmc(0),
extra_assertions(m) { extra_assertions(m) {
updt_params(p); 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); 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; ); 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 (is_uninterp_const(e)) {
if (m_emc) if (m_fmc)
m_emc->insert(to_app(e)->get_decl(), m_fmc->add(e, m_array_util.mk_as_array(bv_f));
m_array_util.mk_as_array(bv_f));
} }
else if (m_fmc) else if (m_fmc)
m_fmc->hide(bv_f); 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); 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; ); TRACE("bvarray2uf_rw", tout << mk_ismt2_pp(e, m_manager) << " -> " << bv_f->get_name() << std::endl; );
if (is_uninterp_const(e)) { if (is_uninterp_const(e)) {
if (m_emc) if (m_fmc)
m_emc->insert(e->get_decl(), m_fmc->add(e, m_array_util.mk_as_array(bv_f));
m_array_util.mk_as_array(bv_f));
} }
else if (m_fmc) else if (m_fmc)
m_fmc->hide(bv_f); m_fmc->hide(bv_f);

6
src/tactic/bv/bvarray2uf_rewriter.h
View file

@ -21,7 +21,6 @@ Notes:
#define BVARRAY2UF_REWRITER_H_ #define BVARRAY2UF_REWRITER_H_
#include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter.h"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
class bvarray2uf_rewriter_cfg : public default_rewriter_cfg { 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; sort_ref_vector m_bindings;
bv_util m_bv_util; bv_util m_bv_util;
array_util m_array_util; array_util m_array_util;
extension_model_converter * m_emc;
generic_model_converter * m_fmc; generic_model_converter * m_fmc;
obj_map<expr, func_decl*> m_arrays_fs; obj_map<expr, func_decl*> m_arrays_fs;
@ -59,7 +57,7 @@ public:
expr_ref_vector extra_assertions; 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: protected:
sort * get_index_sort(expr * e); sort * get_index_sort(expr * e);
@ -79,7 +77,7 @@ struct bvarray2uf_rewriter : public rewriter_tpl<bvarray2uf_rewriter_cfg> {
m_cfg(m, p) { 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 #endif

6
src/tactic/bv/bvarray2uf_tactic.cpp
View file

@ -20,7 +20,6 @@ Notes:
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/expr_replacer.h"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
@ -68,10 +67,9 @@ class bvarray2uf_tactic : public tactic {
m_produce_models = g->models_enabled(); m_produce_models = g->models_enabled();
if (m_produce_models) { if (m_produce_models) {
extension_model_converter * emc = alloc(extension_model_converter, m_manager);
generic_model_converter * fmc = alloc(generic_model_converter, m_manager); generic_model_converter * fmc = alloc(generic_model_converter, m_manager);
mc = concat(emc, fmc); mc = fmc;
m_rw.set_mcs(emc, fmc); m_rw.set_mcs(fmc);
} }

6
src/tactic/bv/dt2bv_tactic.cpp
View file

@ -26,7 +26,6 @@ Revision History:
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/rewriter_def.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "tactic/extension_model_converter.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/rewriter/enum2bv_rewriter.h" #include "ast/rewriter/enum2bv_rewriter.h"
@ -134,7 +133,6 @@ public:
for (sort* s : m_non_fd_sorts) for (sort* s : m_non_fd_sorts)
m_fd_sorts.remove(s); m_fd_sorts.remove(s);
if (!m_fd_sorts.empty()) { if (!m_fd_sorts.empty()) {
ref<extension_model_converter> ext = alloc(extension_model_converter, m);
ref<generic_model_converter> filter = alloc(generic_model_converter, m); ref<generic_model_converter> filter = alloc(generic_model_converter, m);
enum2bv_rewriter rw(m, m_params); enum2bv_rewriter rw(m, m_params);
rw.set_is_fd(&m_is_fd); rw.set_is_fd(&m_is_fd);
@ -155,9 +153,9 @@ public:
for (auto const& kv : rw.enum2bv()) for (auto const& kv : rw.enum2bv())
filter->hide(kv.m_value); filter->hide(kv.m_value);
for (auto const& kv : rw.enum2def()) 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()); report_tactic_progress(":fd-num-translated", rw.num_translated());
} }
g->inc_depth(); g->inc_depth();

14
src/tactic/core/reduce_args_tactic.cpp
View file

@ -22,7 +22,6 @@ Notes:
#include "ast/has_free_vars.h" #include "ast/has_free_vars.h"
#include "util/map.h" #include "util/map.h"
#include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/rewriter_def.h"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
/** /**
@ -394,13 +393,10 @@ struct reduce_args_tactic::imp {
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
var_ref_vector new_vars(m_manager); var_ref_vector new_vars(m_manager);
ptr_buffer<expr> new_eqs; ptr_buffer<expr> new_eqs;
extension_model_converter * e_mc = alloc(extension_model_converter, m_manager);
generic_model_converter * f_mc = alloc(generic_model_converter, m_manager); generic_model_converter * f_mc = alloc(generic_model_converter, m_manager);
decl2arg2func_map::iterator it = decl2arg2funcs.begin(); for (auto const& kv : decl2arg2funcs) {
decl2arg2func_map::iterator end = decl2arg2funcs.end(); func_decl * f = kv.m_key;
for (; it != end; ++it) { arg2func * map = kv.m_value;
func_decl * f = it->m_key;
arg2func * map = it->m_value;
expr * def = 0; expr * def = 0;
SASSERT(decl2args.contains(f)); SASSERT(decl2args.contains(f));
bit_vector & bv = decl2args.find(f); bit_vector & bv = decl2args.find(f);
@ -438,9 +434,9 @@ struct reduce_args_tactic::imp {
} }
} }
SASSERT(def); 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) { void operator()(goal & g, model_converter_ref & mc) {

15
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/ --*/
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/expr_replacer.h"
#include "tactic/extension_model_converter.h" #include "tactic/generic_model_converter.h"
#include "ast/occurs.h" #include "ast/occurs.h"
#include "util/cooperate.h" #include "util/cooperate.h"
#include "tactic/goal_shared_occs.h" #include "tactic/goal_shared_occs.h"
@ -26,7 +26,7 @@ Revision History:
class solve_eqs_tactic : public tactic { class solve_eqs_tactic : public tactic {
struct imp { struct imp {
typedef extension_model_converter gmc; typedef generic_model_converter gmc;
ast_manager & m_manager; ast_manager & m_manager;
expr_replacer * m_r; expr_replacer * m_r;
@ -509,10 +509,8 @@ class solve_eqs_tactic : public tactic {
expr_ref new_def(m()); expr_ref new_def(m());
proof_ref new_pr(m()); proof_ref new_pr(m());
expr_dependency_ref new_dep(m()); expr_dependency_ref new_dep(m());
unsigned size = m_ordered_vars.size(); for (app * v : m_ordered_vars) {
for (unsigned idx = 0; idx < size; idx++) {
checkpoint(); checkpoint();
expr * v = m_ordered_vars[idx];
expr * def = 0; expr * def = 0;
proof * pr = 0; proof * pr = 0;
expr_dependency * dep = 0; expr_dependency * dep = 0;
@ -609,16 +607,13 @@ class solve_eqs_tactic : public tactic {
if (m_produce_models) { if (m_produce_models) {
if (mc.get() == 0) if (mc.get() == 0)
mc = alloc(gmc, m()); mc = alloc(gmc, m());
ptr_vector<app>::iterator it = m_ordered_vars.begin(); for (app * v : m_ordered_vars) {
ptr_vector<app>::iterator end = m_ordered_vars.end();
for (; it != end; ++it) {
app * v = *it;
expr * def = 0; expr * def = 0;
proof * pr; proof * pr;
expr_dependency * dep; expr_dependency * dep;
m_norm_subst->find(v, def, pr, dep); m_norm_subst->find(v, def, pr, dep);
SASSERT(def != 0); SASSERT(def != 0);
static_cast<gmc*>(mc.get())->insert(v->get_decl(), def); static_cast<gmc*>(mc.get())->add(v, def);
} }
} }
} }

48
src/tactic/extension_model_converter.h
View file

@ -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

2
src/tactic/generic_model_converter.cpp
View file

@ -27,7 +27,7 @@ void generic_model_converter::operator()(model_ref & md, unsigned goal_idx) {
std::cout << "model converter\n"; std::cout << "model converter\n";
TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout);); TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout););
model_evaluator ev(*(md.get())); model_evaluator ev(*(md.get()));
ev.set_model_completion(false); ev.set_model_completion(true);
ev.set_expand_array_equalities(false); ev.set_expand_array_equalities(false);
expr_ref val(m); expr_ref val(m);
unsigned arity; unsigned arity;

2
src/tactic/generic_model_converter.h
View file

@ -44,6 +44,8 @@ public:
void add(func_decl * d, expr* e) { m_entries.push_back(entry(d, e, m, ADD)); } 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); virtual void operator()(model_ref & md, unsigned goal_idx);
virtual void operator()(svector<symbol> & labels, unsigned goal_idx) {} virtual void operator()(svector<symbol> & labels, unsigned goal_idx) {}

14
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -22,7 +22,6 @@ Notes:
#include "tactic/tactic.h" #include "tactic/tactic.h"
#include "ast/rewriter/pb2bv_rewriter.h" #include "ast/rewriter/pb2bv_rewriter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "tactic/extension_model_converter.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "model/model_smt2_pp.h" #include "model/model_smt2_pp.h"
#include "tactic/arith/bound_manager.h" #include "tactic/arith/bound_manager.h"
@ -215,17 +214,16 @@ private:
} }
void extend_model(model_ref& mdl) { void extend_model(model_ref& mdl) {
extension_model_converter ext(m); generic_model_converter ext(m);
obj_map<func_decl, func_decl*>::iterator it = m_int2bv.begin(), end = m_int2bv.end(); for (auto const& kv : m_int2bv) {
for (; it != end; ++it) {
rational offset; rational offset;
VERIFY (m_bv2offset.find(it->m_value, offset)); VERIFY (m_bv2offset.find(kv.m_value, offset));
expr_ref value(m_bv.mk_bv2int(m.mk_const(it->m_value)), m); expr_ref value(m_bv.mk_bv2int(m.mk_const(kv.m_value)), m);
if (!offset.is_zero()) { if (!offset.is_zero()) {
value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true)); value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true));
} }
TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";); TRACE("int2bv", tout << mk_pp(kv.m_key, m) << " " << value << "\n";);
ext.insert(it->m_key, value); ext.add(kv.m_key, value);
} }
ext(mdl, 0); ext(mdl, 0);
} }

5
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -25,7 +25,6 @@ Notes:
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "model/model_smt2_pp.h" #include "model/model_smt2_pp.h"
#include "tactic/tactic.h" #include "tactic/tactic.h"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "tactic/portfolio/enum2bv_solver.h" #include "tactic/portfolio/enum2bv_solver.h"
#include "solver/solver_na2as.h" #include "solver/solver_na2as.h"
@ -172,9 +171,9 @@ public:
} }
void extend_model(model_ref& mdl) { void extend_model(model_ref& mdl) {
extension_model_converter ext(m); generic_model_converter ext(m);
for (auto const& kv : m_rewriter.enum2def()) 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); ext(mdl, 0);
} }

1
src/tactic/sine_filter.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "ast/datatype_decl_plugin.h" #include "ast/datatype_decl_plugin.h"
#include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/rewriter_def.h"
#include "tactic/extension_model_converter.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "util/obj_pair_hashtable.h" #include "util/obj_pair_hashtable.h"

6
src/tactic/ufbv/macro_finder_tactic.cpp
View file

@ -19,7 +19,7 @@ Notes:
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "ast/macros/macro_manager.h" #include "ast/macros/macro_manager.h"
#include "ast/macros/macro_finder.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" #include "tactic/ufbv/macro_finder_tactic.h"
class macro_finder_tactic : public tactic { class macro_finder_tactic : public tactic {
@ -69,12 +69,12 @@ class macro_finder_tactic : public tactic {
produce_proofs ? new_proofs.get(i) : 0, produce_proofs ? new_proofs.get(i) : 0,
unsat_core_enabled ? new_deps.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(); unsigned num = mm.get_num_macros();
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
expr_ref f_interp(mm.get_manager()); expr_ref f_interp(mm.get_manager());
func_decl * f = mm.get_macro_interpretation(i, f_interp); func_decl * f = mm.get_macro_interpretation(i, f_interp);
evmc->insert(f, f_interp); evmc->add(f, f_interp);
} }
mc = evmc; mc = evmc;

6
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -17,9 +17,9 @@ Notes:
--*/ --*/
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "tactic/generic_model_converter.h"
#include "ast/macros/macro_manager.h" #include "ast/macros/macro_manager.h"
#include "ast/macros/macro_finder.h" #include "ast/macros/macro_finder.h"
#include "tactic/extension_model_converter.h"
#include "ast/macros/quasi_macros.h" #include "ast/macros/quasi_macros.h"
#include "tactic/ufbv/quasi_macros_tactic.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_proofs ? proofs.get(i) : 0,
produce_unsat_cores ? deps.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(); unsigned num = mm.get_num_macros();
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
expr_ref f_interp(mm.get_manager()); expr_ref f_interp(mm.get_manager());
func_decl * f = mm.get_macro_interpretation(i, f_interp); func_decl * f = mm.get_macro_interpretation(i, f_interp);
evmc->insert(f, f_interp); evmc->add(f, f_interp);
} }
mc = evmc; mc = evmc;