diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 98417cc7b..0cab6ef2f 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -25,7 +25,9 @@ class ackermannize_bv_tactic : public tactic { public: ackermannize_bv_tactic(ast_manager& m, params_ref const& p) : m(m), m_p(p) - {} + { + updt_params(p); + } ~ackermannize_bv_tactic() override { } diff --git a/src/ackermannization/ackr_bound_probe.cpp b/src/ackermannization/ackr_bound_probe.cpp index 1c780386b..b518adccc 100644 --- a/src/ackermannization/ackr_bound_probe.cpp +++ b/src/ackermannization/ackr_bound_probe.cpp @@ -53,29 +53,9 @@ class ackr_bound_probe : public probe { void operator()(quantifier *) {} void operator()(var *) {} - void operator()(app * a) { - if (a->get_num_args() == 0) return; + void operator()(app * a) { m_ackr_helper.mark_non_select(a, m_non_select); - app_set* ts = nullptr; - if (m_ackr_helper.is_select(a)) { - app* sel = to_app(a->get_arg(0)); - if (!m_sel2terms.find(sel, ts)) { - ts = alloc(app_set); - m_sel2terms.insert(sel, ts); - } - } - else if (m_ackr_helper.is_uninterp_fn(a)) { - func_decl* const fd = a->get_decl(); - if (!m_fun2terms.find(fd, ts)) { - ts = alloc(app_set); - m_fun2terms.insert(fd, ts); - } - } - else { - return; - } - - ts->insert(a); + m_ackr_helper.insert(m_fun2terms, m_sel2terms, a); } }; diff --git a/src/ackermannization/ackr_helper.cpp b/src/ackermannization/ackr_helper.cpp index 3e8bc09f0..079782b31 100644 --- a/src/ackermannization/ackr_helper.cpp +++ b/src/ackermannization/ackr_helper.cpp @@ -19,10 +19,12 @@ double ackr_helper::calculate_lemma_bound(fun2terms_map const& occs1, sel2terms_map const& occs2) { double total = 0; for (auto const& kv : occs1) { - total += n_choose_2_chk(kv.m_value->size()); + total += n_choose_2_chk(kv.m_value->var_args.size()); + total += kv.m_value->const_args.size() * kv.m_value->var_args.size(); } for (auto const& kv : occs2) { - total += n_choose_2_chk(kv.m_value->size()); + total += n_choose_2_chk(kv.m_value->var_args.size()); + total += kv.m_value->const_args.size() * kv.m_value->var_args.size(); } return total; } diff --git a/src/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h index 422f74751..1bfa0d6ba 100644 --- a/src/ackermannization/ackr_helper.h +++ b/src/ackermannization/ackr_helper.h @@ -22,9 +22,13 @@ class ackr_helper { public: - typedef obj_hashtable app_set; + struct app_occ { + obj_hashtable const_args; + obj_hashtable var_args; + }; + typedef app_occ app_set; typedef obj_map fun2terms_map; - typedef obj_map sel2terms_map; + typedef obj_map sel2terms_map; ackr_helper(ast_manager& m) : m_bvutil(m), m_autil(m) {} @@ -88,13 +92,48 @@ public: static double calculate_lemma_bound(fun2terms_map const& occs1, sel2terms_map const& occs2); /** \brief Calculate n choose 2. **/ - inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); } + inline static unsigned n_choose_2(unsigned n) { return (n & 1) ? (n * (n >> 1)) : (n >> 1) * (n - 1); } /** \brief Calculate n choose 2 guarded for overflow. Returns infinity if unsafe. **/ inline static double n_choose_2_chk(unsigned n) { SASSERT(std::numeric_limits().max() & 32); return n & (1 << 16) ? std::numeric_limits().infinity() : n_choose_2(n); } + + void insert(fun2terms_map& f2t, sel2terms_map& s2t, app* a) { + if (a->get_num_args() == 0) return; + ast_manager& m = m_bvutil.get_manager(); + app_set* ts = nullptr; + bool is_const_args = true; + if (is_select(a)) { + app* sel = to_app(a->get_arg(0)); + if (!s2t.find(sel, ts)) { + ts = alloc(app_set); + s2t.insert(sel, ts); + } + } + else if (is_uninterp_fn(a)) { + func_decl* const fd = a->get_decl(); + if (!f2t.find(fd, ts)) { + ts = alloc(app_set); + f2t.insert(fd, ts); + } + is_const_args = m.is_value(a->get_arg(0)); + } + else { + return; + } + for (unsigned i = 1; is_const_args && i < a->get_num_args(); ++i) { + is_const_args &= m.is_value(a->get_arg(i)); + } + + if (is_const_args) { + ts->const_args.insert(a); + } + else { + ts->var_args.insert(a); + } + } private: bv_util m_bvutil; diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index 83c399f63..e351da9c9 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -153,10 +153,10 @@ void lackr::eager_enc() { } void lackr::ackr(app_set const* ts) { - const app_set::iterator r = ts->end(); - for (app_set::iterator j = ts->begin(); j != r; ++j) { + auto r = ts->var_args.end(); + for (auto j = ts->var_args.begin(); j != r; ++j) { app * const t1 = *j; - app_set::iterator k = j; + auto k = j; ++k; for (; k != r; ++k) { app * const t2 = *k; @@ -164,27 +164,46 @@ void lackr::ackr(app_set const* ts) { ackr(t1, t2); } } + for (app* t2 : ts->const_args) { + ackr(t1, t2); + } } } - -void lackr::abstract() { - for (auto const& kv : m_fun2terms) { +void lackr::abstract_fun(fun2terms_map const& apps) { + for (auto const& kv : apps) { func_decl* fd = kv.m_key; - for (app * t : *kv.m_value) { + for (app * t : kv.m_value->var_args) { + app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t)); + SASSERT(t->get_decl() == fd); + m_info->set_abstr(t, fc); + } + for (app * t : kv.m_value->const_args) { app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t)); SASSERT(t->get_decl() == fd); m_info->set_abstr(t, fc); } } - for (auto& kv : m_sel2terms) { +} + +void lackr::abstract_sel(sel2terms_map const& apps) { + for (auto const& kv : apps) { func_decl * fd = kv.m_key->get_decl(); - for (app * t : *kv.m_value) { + for (app * t : kv.m_value->const_args) { + app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t)); + m_info->set_abstr(t, fc); + } + for (app * t : kv.m_value->var_args) { app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t)); m_info->set_abstr(t, fc); } } +} + +void lackr::abstract() { + abstract_fun(m_fun2terms); + abstract_sel(m_sel2terms); m_info->seal(); // perform abstraction of the formulas for (expr * f : m_formulas) { @@ -194,28 +213,7 @@ void lackr::abstract() { } void lackr::add_term(app* a) { - app_set* ts = nullptr; - if (a->get_num_args() == 0) - return; - if (m_ackr_helper.is_select(a)) { - app* sel = to_app(a->get_arg(0)); - if (!m_sel2terms.find(sel, ts)) { - ts = alloc(app_set); - m_sel2terms.insert(sel, ts); - } - } - else if (m_ackr_helper.is_uninterp_fn(a)) { - func_decl* const fd = a->get_decl(); - if (!m_fun2terms.find(fd, ts)) { - ts = alloc(app_set); - m_fun2terms.insert(fd, ts); - } - } - else { - return; - } - TRACE("ackermannize", tout << "term(" << mk_ismt2_pp(a, m, 2) << ")\n";); - ts->insert(a); + m_ackr_helper.insert(m_fun2terms, m_sel2terms, a); } void lackr::push_abstraction() { diff --git a/src/ackermannization/lackr.h b/src/ackermannization/lackr.h index f6d77fc85..aad1fdfcd 100644 --- a/src/ackermannization/lackr.h +++ b/src/ackermannization/lackr.h @@ -123,5 +123,9 @@ class lackr { // Collect all uninterpreted terms, skipping 0-arity. // bool collect_terms(); + + void abstract_sel(sel2terms_map const& apps); + void abstract_fun(fun2terms_map const& apps); + }; #endif /* LACKR_H_ */ diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 515226387..b676cbe17 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -38,6 +38,7 @@ Notes: #include "tactic/arith/eq2bv_tactic.h" #include "tactic/bv/dt2bv_tactic.h" #include "tactic/generic_model_converter.h" +#include "ackermannization/ackermannize_bv_tactic.h" #include "sat/sat_solver/inc_sat_solver.h" #include "qe/qsat.h" #include "opt/opt_context.h" @@ -804,6 +805,7 @@ namespace opt { and_then(mk_simplify_tactic(m, m_params), mk_propagate_values_tactic(m), mk_solve_eqs_tactic(m), + mk_ackermannize_bv_tactic(m, m_params), // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints mk_simplify_tactic(m)); opt_params optp(m_params);