From 083939ab0e245f0fe89a9de8d789cff1fa642918 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Jul 2016 14:11:21 -0700 Subject: [PATCH] add tactic to eliminate enumeration sorts in favor of bit-vectors Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/tactic/bv/CMakeLists.txt | 1 + src/ast/datatype_decl_plugin.cpp | 20 ++ src/ast/datatype_decl_plugin.h | 3 + src/tactic/bv/dt2bv_tactic.cpp | 304 +++++++++++++++++++++ src/tactic/bv/dt2bv_tactic.h | 32 +++ src/tactic/bv/elim_small_bv_tactic.cpp | 5 +- 6 files changed, 362 insertions(+), 3 deletions(-) create mode 100644 src/tactic/bv/dt2bv_tactic.cpp create mode 100644 src/tactic/bv/dt2bv_tactic.h diff --git a/contrib/cmake/src/tactic/bv/CMakeLists.txt b/contrib/cmake/src/tactic/bv/CMakeLists.txt index 42cff2bfc..b39d77a0a 100644 --- a/contrib/cmake/src/tactic/bv/CMakeLists.txt +++ b/contrib/cmake/src/tactic/bv/CMakeLists.txt @@ -7,6 +7,7 @@ z3_add_component(bv_tactics bvarray2uf_tactic.cpp bv_bounds_tactic.cpp bv_size_reduction_tactic.cpp + dt2bv_tactic.cpp elim_small_bv_tactic.cpp max_bv_sharing_tactic.cpp COMPONENT_DEPENDENCIES diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index eb15910bc..8bfd9b36d 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -933,6 +933,25 @@ bool datatype_util::is_recursive(sort * ty) { return r; } + +bool datatype_util::is_enum_sort(sort* s) { + if (!is_datatype(s)) { + return false; + } + bool r = false; + if (m_is_enum.find(s, r)) + return r; + ptr_vector const& cnstrs = *get_datatype_constructors(s); + r = true; + for (unsigned i = 0; r && i < cnstrs.size(); ++i) { + r = cnstrs[i]->get_arity() == 0; + } + m_is_enum.insert(s, r); + m_asts.push_back(s); + return r; +} + + void datatype_util::reset() { m_datatype2constructors.reset(); m_datatype2nonrec_constructor.reset(); @@ -941,6 +960,7 @@ void datatype_util::reset() { m_recognizer2constructor.reset(); m_accessor2constructor.reset(); m_is_recursive.reset(); + m_is_enum.reset(); std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc >()); m_vectors.reset(); m_asts.reset(); diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 8ef6fb557..019dd339e 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -173,6 +173,7 @@ class datatype_util { obj_map m_recognizer2constructor; obj_map m_accessor2constructor; obj_map m_is_recursive; + obj_map m_is_enum; ast_ref_vector m_asts; ptr_vector > m_vectors; @@ -184,6 +185,8 @@ public: ~datatype_util(); ast_manager & get_manager() const { return m_manager; } bool is_datatype(sort * s) const { return is_sort_of(s, m_family_id, DATATYPE_SORT); } + bool is_enum_sort(sort* s); + bool is_recursive(sort * ty); bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); } bool is_recognizer(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); } diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp new file mode 100644 index 000000000..022617c6d --- /dev/null +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -0,0 +1,304 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + dt2bv_tactic.cpp + +Abstract: + + Tactic that eliminates finite domain data-types. + +Author: + + nbjorner 2016-07-22 + +Revision History: + +--*/ + +#include "dt2bv_tactic.h" +#include "tactical.h" +#include "filter_model_converter.h" +#include "datatype_decl_plugin.h" +#include "bv_decl_plugin.h" +#include "rewriter_def.h" +#include "filter_model_converter.h" +#include "extension_model_converter.h" +#include "var_subst.h" +#include "ast_util.h" + +#if 0 + +enumeration types: + +a = x: + x = y + +forall x . phi + + f(x,y) = z -> + +#endif + + +class dt2bv_tactic : public tactic { + + ast_manager& m; + params_ref m_params; + datatype_util m_dt; + bv_util m_bv; + obj_hashtable m_fd_sorts; + obj_hashtable m_non_fd_sorts; + expr_ref_vector m_bounds; + ref m_ext; + ref m_filter; + unsigned m_num_transformed; + + struct rw_cfg : public default_rewriter_cfg { + dt2bv_tactic& m_t; + ast_manager& m; + params_ref m_params; + obj_map m_cache; + expr_ref_vector m_trail; + + rw_cfg(dt2bv_tactic& t, ast_manager & m, params_ref const & p) : + m_t(t), + m(m), + m_params(p), + m_trail(m) + {} + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + expr_ref a0(m), a1(m); + if (m.is_eq(f) && reduce_arg(args[0], a0) && reduce_arg(args[1], a1)) { + result = m.mk_eq(a0, a1); + return BR_DONE; + } + else { + return BR_FAILED; + } + } + + bool reduce_arg(expr* a, expr_ref& result) { + expr* b; + if (m_cache.find(a, b)) { + result = b; + return true; + } + + sort* s = get_sort(a); + if (!m_t.m_fd_sorts.contains(s)) { + return false; + } + unsigned bv_size = get_bv_size(s); + + if (is_var(a)) { + result = m.mk_var(to_var(a)->get_idx(), m_t.m_bv.mk_sort(bv_size)); + return true; + } + SASSERT(is_app(a)); + func_decl* f = to_app(a)->get_decl(); + if (m_t.m_dt.is_constructor(f)) { + unsigned idx = m_t.m_dt.get_constructor_idx(f); + result = m_t.m_bv.mk_numeral(idx, bv_size); + } + else { + // create a fresh variable, add bounds constraints for it. + unsigned nc = m_t.m_dt.get_datatype_num_constructors(s); + result = m.mk_fresh_const(f->get_name().str().c_str(), m_t.m_bv.mk_sort(bv_size)); + if (!is_power_of_two(nc)) { + m_t.m_bounds.push_back(m_t.m_bv.mk_ule(result, m_t.m_bv.mk_numeral(nc, bv_size))); + } + expr_ref f_def(m); + ptr_vector const& cs = *m_t.m_dt.get_datatype_constructors(s); + f_def = m.mk_const(cs[nc-1]); + for (unsigned i = nc - 1; i > 0; ) { + --i; + f_def = m.mk_ite(m.mk_eq(result, m_t.m_bv.mk_numeral(i,bv_size)), m.mk_const(cs[i]), f_def); + } + // update model converters. + m_t.m_ext->insert(f, f_def); + m_t.m_filter->insert(to_app(result)->get_decl()); + } + m_cache.insert(a, result); + ++m_t.m_num_transformed; + return true; + } + + ptr_buffer m_sorts; + + bool reduce_quantifier( + quantifier * q, + expr * old_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + m_sorts.reset(); + expr_ref_vector bounds(m); + bool found = false; + for (unsigned i = 0; i < q->get_num_decls(); ++i) { + sort* s = q->get_decl_sort(i); + if (m_t.m_fd_sorts.contains(s)) { + unsigned bv_size = get_bv_size(s); + m_sorts.push_back(m_t.m_bv.mk_sort(bv_size)); + unsigned nc = m_t.m_dt.get_datatype_num_constructors(s); + if (!is_power_of_two(nc)) { + bounds.push_back(m_t.m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_t.m_bv.mk_numeral(nc, bv_size))); + } + found = true; + } + else { + m_sorts.push_back(s); + } + } + if (!found) { + return false; + } + expr_ref new_body_ref(old_body, m), tmp(m); + if (!bounds.empty()) { + if (q->is_forall()) { + new_body_ref = m.mk_implies(mk_and(bounds), new_body_ref); + } + else { + bounds.push_back(new_body_ref); + new_body_ref = mk_and(bounds); + } + } + result = m.mk_quantifier(q->is_forall(), q->get_num_decls(), m_sorts.c_ptr(), q->get_decl_names(), new_body_ref, + q->get_weight(), q->get_qid(), q->get_skid(), + q->get_num_patterns(), new_patterns, + q->get_num_no_patterns(), new_no_patterns); + result_pr = 0; + return true; + } + + unsigned get_bv_size(sort* s) { + unsigned nc = m_t.m_dt.get_datatype_num_constructors(s); + unsigned bv_size = 1; + while ((unsigned)(1 << bv_size) < nc) { + ++bv_size; + } + return bv_size; + } + }; + + struct rw : public rewriter_tpl { + rw_cfg m_cfg; + + rw(dt2bv_tactic& t, ast_manager & m, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(t, m, p) { + } + }; + + + + bool is_fd(expr* a) { return is_fd(get_sort(a)); } + bool is_fd(sort* a) { return m_dt.is_enum_sort(a); } + + struct check_fd { + dt2bv_tactic& m_t; + ast_manager& m; + + check_fd(dt2bv_tactic& t): m_t(t), m(t.m) {} + + void operator()(app* a) { + if (m.is_eq(a)) { + return; + } + if (m_t.is_fd(a)) { + m_t.m_fd_sorts.insert(get_sort(a)); + } + else { + unsigned sz = a->get_num_args(); + for (unsigned i = 0; i < sz; ++i) { + if (m_t.is_fd(a->get_arg(i))) { + m_t.m_non_fd_sorts.insert(get_sort(a->get_arg(i))); + } + } + } + } + + void operator()(var * v) { + if (m_t.is_fd(v)) { + m_t.m_fd_sorts.insert(get_sort(v)); + } + } + + void operator()(quantifier* q) {} + }; + +public: + + dt2bv_tactic(ast_manager& m, params_ref const& p): + m(m), m_params(p), m_dt(m), m_bv(m), m_bounds(m) {} + + virtual tactic * translate(ast_manager & m) { + return alloc(dt2bv_tactic, m, m_params); + } + + virtual void updt_params(params_ref const & p) { + } + + virtual void collect_param_descrs(param_descrs & r) { + } + + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + mc = 0; pc = 0; core = 0; + bool produce_proofs = g->proofs_enabled(); + tactic_report report("dt2bv", *g); + unsigned size = g->size(); + expr_fast_mark1 visited; + check_fd proc(*this); + for (unsigned i = 0; i < size; ++i) { + quick_for_each_expr(proc, visited, g->form(i)); + } + obj_hashtable::iterator it = m_non_fd_sorts.begin(), end = m_non_fd_sorts.end(); + for (; it != end; ++it) { + m_fd_sorts.remove(*it); + } + if (!m_fd_sorts.empty()) { + m_bounds.reset(); + m_num_transformed = 0; + m_ext = alloc(extension_model_converter, m); + m_filter = alloc(filter_model_converter, m); + scoped_ptr r = alloc(rw, *this, m, m_params); + expr_ref new_curr(m); + proof_ref new_pr(m); + for (unsigned idx = 0; idx < size; idx++) { + (*r)(g->form(idx), new_curr, new_pr); + if (produce_proofs) { + proof * pr = g->pr(idx); + new_pr = m.mk_modus_ponens(pr, new_pr); + } + g->update(idx, new_curr, new_pr, g->dep(idx)); + } + for (unsigned i = 0; i < m_bounds.size(); ++i) { + g->assert_expr(m_bounds[i].get()); + } + mc = concat(m_ext.get(), m_filter.get()); + report_tactic_progress(":fd-num-translated", m_num_transformed); + } + g->inc_depth(); + result.push_back(g.get()); + TRACE("dt2bv", g->display(tout);); + SASSERT(g->is_well_sorted()); + } + + virtual void cleanup() { + m_fd_sorts.reset(); + m_non_fd_sorts.reset(); + m_bounds.reset(); + } + +}; + +tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p) { + return alloc(dt2bv_tactic, m, p); +} diff --git a/src/tactic/bv/dt2bv_tactic.h b/src/tactic/bv/dt2bv_tactic.h new file mode 100644 index 000000000..64d1d5497 --- /dev/null +++ b/src/tactic/bv/dt2bv_tactic.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + dt2bv_tactic.h + +Abstract: + + Tactic that eliminates finite domain data-types. + +Author: + + nbjorner 2016-07-22 + +Revision History: + +--*/ +#ifndef DT2BV_TACTIC_H_ +#define DT2BV_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("dt2bv", "eliminate finite domain data-types. Replace by bit-vectors.", "mk_dt2bv_tactic(m, p)") +*/ + +#endif diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 7db3a15ca..e395433f5 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -119,9 +119,8 @@ class elim_small_bv_tactic : public tactic { return res; } - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - result = m.mk_app(f, num, args); - TRACE("elim_small_bv_app", tout << "reduce " << mk_ismt2_pp(result, m) << std::endl; ); + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + TRACE("elim_small_bv_app", expr_ref tmp(m.mk_app(f, num, args), m); tout << "reduce " << tmp << std::endl; ); return BR_FAILED; }