From c7a7d40a8f69d3bc8ac54886a9a5f1d04d3562bc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Jul 2021 18:47:25 +0200 Subject: [PATCH] remove incorrect and inefficient default model conversion --- src/solver/solver.cpp | 15 ----- src/solver/solver.h | 3 +- src/solver/solver_params.pyg | 3 +- src/tactic/generic_model_converter.cpp | 62 --------------------- src/tactic/generic_model_converter.h | 4 +- src/tactic/horn_subsume_model_converter.cpp | 4 -- src/tactic/horn_subsume_model_converter.h | 2 - src/tactic/model_converter.h | 3 +- 8 files changed, 6 insertions(+), 90 deletions(-) diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 32cb0b940..b53e3daed 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -202,12 +202,6 @@ bool solver::is_literal(ast_manager& m, expr* e) { void solver::assert_expr(expr* f) { expr_ref fml(f, get_manager()); - if (m_enforce_model_conversion) { - model_converter_ref mc = get_model_converter(); - if (mc) { - (*mc)(fml); - } - } assert_expr_core(fml); } @@ -215,13 +209,6 @@ void solver::assert_expr(expr* f, expr* t) { ast_manager& m = get_manager(); expr_ref fml(f, m); expr_ref a(t, m); - if (m_enforce_model_conversion) { - model_converter_ref mc = get_model_converter(); - if (mc) { - (*mc)(fml); - // (*mc)(a); - } - } assert_expr_core2(fml, a); } @@ -241,14 +228,12 @@ void solver::collect_param_descrs(param_descrs & r) { void solver::reset_params(params_ref const & p) { m_params = p; solver_params sp(m_params); - m_enforce_model_conversion = sp.enforce_model_conversion(); m_cancel_backup_file = sp.cancel_backup_file(); } void solver::updt_params(params_ref const & p) { m_params.copy(p); solver_params sp(m_params); - m_enforce_model_conversion = sp.enforce_model_conversion(); m_cancel_backup_file = sp.cancel_backup_file(); } diff --git a/src/solver/solver.h b/src/solver/solver.h index b65dc2fe8..14fd49bce 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -49,10 +49,9 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p); */ class solver : public check_sat_result { params_ref m_params; - bool m_enforce_model_conversion; symbol m_cancel_backup_file; public: - solver(): m_enforce_model_conversion(false) {} + solver() {} ~solver() override {} /** diff --git a/src/solver/solver_params.pyg b/src/solver/solver_params.pyg index b852afbaa..21d0ab530 100644 --- a/src/solver/solver_params.pyg +++ b/src/solver/solver_params.pyg @@ -2,8 +2,7 @@ def_module_params('solver', description='solver parameters', export=True, - params=(('enforce_model_conversion', BOOL, False, "apply model transformation on new assertions"), - ('smtlib2_log', SYMBOL, '', "file to save solver interaction"), + params=(('smtlib2_log', SYMBOL, '', "file to save solver interaction"), ('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"), ('timeout', UINT, UINT_MAX, "timeout on the solver object; overwrites a global timeout"), )) diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 8ef21d9c9..2886eb6ab 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -139,68 +139,6 @@ void generic_model_converter::set_env(ast_pp_util* visitor) { } } -struct min_app_idx_proc { - unsigned m_min; - obj_map& m_idxs; - min_app_idx_proc(obj_map& idxs) : m_min(UINT_MAX), m_idxs(idxs) {} - void operator()(app * n) { - unsigned idx; - if (m_idxs.find(n->get_decl(), idx)) { - m_min = std::min(m_min, idx); - } - } - void operator()(var * n) {} - void operator()(quantifier * n) {} -}; - -void generic_model_converter::operator()(expr_ref& fml) { - min_app_idx_proc min_proc(m_first_idx); - for_each_expr(min_proc, fml); - unsigned min_idx = min_proc.m_min; - if (min_idx == UINT_MAX) return; - expr_ref_vector fmls(m); - fmls.push_back(fml); - for (unsigned i = m_entries.size(); i-- > min_idx;) { - entry const& e = m_entries[i]; - if (e.m_instruction != instruction::ADD) { - continue; - } - unsigned arity = e.m_f->get_arity(); - if (arity == 0) { - fmls.push_back(simplify_def(e)); - } - else { - expr_ref_vector args(m); - sort_ref_vector sorts(m); - svector names; - for (unsigned i = 0; i < arity; ++i) { - sorts.push_back(e.m_f->get_domain(i)); - names.push_back(symbol(i)); - args.push_back(m.mk_var(i, sorts.back())); - } - // TBD: check if order is correct with respect to quantifier binding ordering - expr_ref lhs(m.mk_app(e.m_f, arity, args.data()), m); - expr_ref body(m.mk_eq(lhs, e.m_def), m); - fmls.push_back(m.mk_forall(arity, sorts.data(), names.data(), body)); - } - if (m_first_idx[e.m_f] == i) { - m_first_idx.remove(e.m_f); - } - } - unsigned j = min_idx; - for (unsigned i = min_idx; i < m_entries.size(); ++i) { - entry& e = m_entries[i]; - if (e.m_instruction == instruction::HIDE) { - if (i != j) { - m_entries[j] = e; - } - ++j; - } - } - m_entries.shrink(j); - fml = mk_and(fmls); -} - void generic_model_converter::get_units(obj_map& units) { th_rewriter rw(m); expr_safe_replace rep(m); diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index 54268ac1b..e809fe734 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -54,6 +54,8 @@ public: void operator()(model_ref & md) override; + void operator()(expr_ref& fml) override { UNREACHABLE(); } + void cancel() override {} void display(std::ostream & out) override; @@ -64,8 +66,6 @@ public: void set_env(ast_pp_util* visitor) override; - void operator()(expr_ref& fml) override; - void get_units(obj_map& units) override; }; diff --git a/src/tactic/horn_subsume_model_converter.cpp b/src/tactic/horn_subsume_model_converter.cpp index 38e6a42c5..79b9a038f 100644 --- a/src/tactic/horn_subsume_model_converter.cpp +++ b/src/tactic/horn_subsume_model_converter.cpp @@ -169,10 +169,6 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod } -void horn_subsume_model_converter::operator()(expr_ref& fml) { - NOT_IMPLEMENTED_YET(); -} - void horn_subsume_model_converter::operator()(model_ref& mr) { func_decl_ref pred(m); diff --git a/src/tactic/horn_subsume_model_converter.h b/src/tactic/horn_subsume_model_converter.h index f007a63f3..41e59070e 100644 --- a/src/tactic/horn_subsume_model_converter.h +++ b/src/tactic/horn_subsume_model_converter.h @@ -72,8 +72,6 @@ public: void operator()(model_ref& _m) override; - void operator()(expr_ref& fml) override; - model_converter * translate(ast_translation & translator) override; ast_manager& get_manager() { return m; } diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h index 2b3a1b510..3ed9f298b 100644 --- a/src/tactic/model_converter.h +++ b/src/tactic/model_converter.h @@ -76,6 +76,8 @@ public: virtual void operator()(model_ref & m) = 0; virtual void operator()(labels_vec & r) {} + + virtual void operator()(expr_ref& fml) { UNREACHABLE(); } virtual model_converter * translate(ast_translation & translator) = 0; @@ -86,7 +88,6 @@ public: The operator has as side effect of adding definitions as assertions to the formula and removing these definitions from the model converter. */ - virtual void operator()(expr_ref& formula) { UNREACHABLE(); } virtual void get_units(obj_map& fmls) { UNREACHABLE(); } };