From ccd18283e7d3b5b26fe21bdbc4cacc958d5894f9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 1 Apr 2016 15:38:38 +0100 Subject: [PATCH] Moved extension_converter func_interp entry compression to func_interp. Relates to #547 --- src/model/func_interp.cpp | 55 +++++++++++++++++++++--- src/model/func_interp.h | 3 ++ src/tactic/extension_model_converter.cpp | 44 +------------------ src/tactic/extension_model_converter.h | 3 -- 4 files changed, 53 insertions(+), 52 deletions(-) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 90810f294..45bcd7780 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -104,11 +104,54 @@ void func_interp::reset_interp_cache() { m_manager.dec_ref(m_interp); m_interp = 0; } - + +bool func_interp::is_fi_entry_expr(expr * e, ptr_vector & args) { + args.reset(); + if (!is_app(e) || !m().is_ite(to_app(e))) + return false; + + app * a = to_app(e); + expr * c = a->get_arg(0); + expr * t = a->get_arg(1); + expr * f = a->get_arg(2); + + if ((m_arity == 0) || + (m_arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) || + (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity))) + return false; + + args.resize(m_arity, 0); + for (unsigned i = 0; i < m_arity; i++) { + expr * ci = (m_arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i); + + if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2) + return false; + + expr * a0 = to_app(ci)->get_arg(0); + expr * a1 = to_app(ci)->get_arg(1); + if (is_var(a0) && to_var(a0)->get_idx() == i) + args[i] = a1; + else if (is_var(a1) && to_var(a1)->get_idx() == i) + args[i] = a0; + else + return false; + } + + return true; +} + void func_interp::set_else(expr * e) { reset_interp_cache(); - m_manager.inc_ref(e); m_manager.dec_ref(m_else); + + ptr_vector args; + while (is_fi_entry_expr(e, args)) { + TRACE("func_interp", tout << "fi entry expr: " << mk_ismt2_pp(e, m()) << std::endl;); + insert_entry(args.c_ptr(), to_app(e)->get_arg(1)); + e = to_app(e)->get_arg(2); + } + + m_manager.inc_ref(e); m_else = e; } @@ -148,7 +191,7 @@ func_entry * func_interp::get_entry(expr * const * args) const { void func_interp::insert_entry(expr * const * args, expr * r) { reset_interp_cache(); - func_entry * entry = get_entry(args); + func_entry * entry = get_entry(args); if (entry != 0) { entry->set_result(m_manager, r); return; @@ -201,7 +244,7 @@ expr * func_interp::get_max_occ_result() const { for (; it != end; ++it) { func_entry * curr = *it; expr * r = curr->get_result(); - unsigned occs = 0; + unsigned occs = 0; num_occs.find(r, occs); occs++; num_occs.insert(r, occs); @@ -283,13 +326,13 @@ expr * func_interp::get_interp() const { return r; } -func_interp * func_interp::translate(ast_translation & translator) const { +func_interp * func_interp::translate(ast_translation & translator) const { func_interp * new_fi = alloc(func_interp, translator.to(), m_arity); ptr_vector::const_iterator it = m_entries.begin(); ptr_vector::const_iterator end = m_entries.end(); for (; it != end; ++it) { - func_entry * curr = *it; + func_entry * curr = *it; ptr_buffer new_args; for (unsigned i=0; iget_arg(i))); diff --git a/src/model/func_interp.h b/src/model/func_interp.h index 7ad2fefd8..d0d61546e 100644 --- a/src/model/func_interp.h +++ b/src/model/func_interp.h @@ -110,6 +110,9 @@ public: expr * get_interp() const; func_interp * translate(ast_translation & translator) const; + +private: + bool is_fi_entry_expr(expr * e, ptr_vector & args); }; #endif diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp index ebd530a58..cdd096455 100644 --- a/src/tactic/extension_model_converter.cpp +++ b/src/tactic/extension_model_converter.cpp @@ -43,41 +43,6 @@ static void display_decls_info(std::ostream & out, model_ref & md) { } } -bool extension_model_converter::is_fi_entry_expr(expr * e, unsigned arity, ptr_vector & args) { - args.reset(); - if (!is_app(e) || !m().is_ite(to_app(e))) - return false; - - app * a = to_app(e); - expr * c = a->get_arg(0); - expr * t = a->get_arg(1); - expr * f = a->get_arg(2); - - if ((arity == 0) || - (arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) || - (arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != arity))) - return false; - - args.resize(arity, 0); - for (unsigned i = 0; i < arity; i++) { - expr * ci = (arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i); - - if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2) - return false; - - expr * a0 = to_app(ci)->get_arg(0); - expr * a1 = to_app(ci)->get_arg(1); - if (is_var(a0) && to_var(a0)->get_idx() == i) - args[i] = a1; - else if (is_var(a1) && to_var(a1)->get_idx() == i) - args[i] = a0; - else - return false; - } - - return true; -} - void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { SASSERT(goal_idx == 0); TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); @@ -97,14 +62,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { } else { func_interp * new_fi = alloc(func_interp, m(), arity); - expr * e = val.get(); - ptr_vector args; - while (is_fi_entry_expr(e, arity, args)) { - TRACE("extension_mc", tout << "fi entry: " << mk_ismt2_pp(e, m()) << std::endl;); - new_fi->insert_entry(args.c_ptr(), to_app(e)->get_arg(1)); - e = to_app(e)->get_arg(2); - } - new_fi->set_else(e); + new_fi->set_else(val); md->register_decl(f, new_fi); } } diff --git a/src/tactic/extension_model_converter.h b/src/tactic/extension_model_converter.h index 9431906f3..46644eec2 100644 --- a/src/tactic/extension_model_converter.h +++ b/src/tactic/extension_model_converter.h @@ -43,9 +43,6 @@ public: void insert(func_decl * v, expr * def); virtual model_converter * translate(ast_translation & translator); - -private: - bool is_fi_entry_expr(expr * e, unsigned arity, ptr_vector & args); };