From 14e6b5b50008134a0d92379a69a4d537a7f2b2d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Aug 2017 01:38:55 -0700 Subject: [PATCH] mising files Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/maximize_ac_sharing.cpp | 175 +++++++++++++++++++++++ src/ast/rewriter/maximize_ac_sharing.h | 125 ++++++++++++++++ 2 files changed, 300 insertions(+) create mode 100644 src/ast/rewriter/maximize_ac_sharing.cpp create mode 100644 src/ast/rewriter/maximize_ac_sharing.h diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp new file mode 100644 index 000000000..b560132db --- /dev/null +++ b/src/ast/rewriter/maximize_ac_sharing.cpp @@ -0,0 +1,175 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + maximize_ac_sharing.cpp + +Abstract: + + + +Author: + + Leonardo de Moura (leonardo) 2008-10-22. + +Revision History: + +--*/ + +#include "ast/rewriter/maximize_ac_sharing.h" +#include "ast/ast_pp.h" + + +void maximize_ac_sharing::register_kind(decl_kind k) { + m_kinds.push_back(k); +} + + +br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result, proof_ref& result_pr) { + decl_kind k = f->get_kind(); + if (!f->is_associative()) + return BR_FAILED; + if (num_args <= 2) + return BR_FAILED; + if (std::find(m_kinds.begin(), m_kinds.end(), k) == m_kinds.end()) + return BR_FAILED; + ptr_buffer _args; + expr * numeral = 0; + if (is_numeral(args[0])) { + numeral = args[0]; + for (unsigned i = 1; i < num_args; i++) + _args.push_back(args[i]); + num_args--; + } + else { + _args.append(num_args, args); + } + + TRACE("ac_sharing_detail", tout << "before-reuse: num_args: " << num_args << "\n";); + +#define MAX_NUM_ARGS_FOR_OPT 128 + + // Try to reuse already created circuits. + TRACE("ac_sharing_detail", tout << "args: "; for (unsigned i = 0; i < num_args; i++) tout << mk_pp(_args[i], m) << "\n";); + try_to_reuse: + if (num_args > 1 && num_args < MAX_NUM_ARGS_FOR_OPT) { + for (unsigned i = 0; i < num_args - 1; i++) { + for (unsigned j = i + 1; j < num_args; j++) { + if (contains(f, _args[i], _args[j])) { + TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";); + _args[i] = m.mk_app(f, _args[i], _args[j]); + SASSERT(num_args > 1); + for (unsigned w = j; w < num_args - 1; w++) { + _args[w] = _args[w+1]; + } + num_args--; + goto try_to_reuse; + } + } + } + } + + + // Create "tree-like circuit" + while (true) { + TRACE("ac_sharing_detail", tout << "tree-loop: num_args: " << num_args << "\n";); + unsigned j = 0; + for (unsigned i = 0; i < num_args; i += 2, j++) { + if (i == num_args - 1) { + _args[j] = _args[i]; + } + else { + insert(f, _args[i], _args[i+1]); + _args[j] = m.mk_app(f, _args[i], _args[i+1]); + } + } + num_args = j; + if (num_args == 1) { + if (numeral == 0) { + result = _args[0]; + } + else { + result = m.mk_app(f, numeral, _args[0]); + } + TRACE("ac_sharing_detail", tout << "result: " << mk_pp(result, m) << "\n";); + return BR_DONE; + } + } + + UNREACHABLE(); + return BR_FAILED; +} + +bool maximize_ac_sharing::contains(func_decl * f, expr * arg1, expr * arg2) { + entry e(f, arg1, arg2); + return m_cache.contains(&e); +} + +void maximize_ac_sharing::insert(func_decl * f, expr * arg1, expr * arg2) { + entry * e = new (m_region) entry(f, arg1, arg2); + m_entries.push_back(e); + m_cache.insert(e); + m.inc_ref(arg1); + m.inc_ref(arg2); +} + +maximize_ac_sharing::maximize_ac_sharing(ast_manager & m): + m(m), + m_init(false) { +} + +maximize_ac_sharing::~maximize_ac_sharing() { + restore_entries(0); +} + + +void maximize_ac_sharing::push_scope() { + init(); + m_scopes.push_back(m_entries.size()); + m_region.push_scope(); +} + +void maximize_ac_sharing::pop_scope(unsigned num_scopes) { + SASSERT(num_scopes <= m_scopes.size()); + unsigned new_lvl = m_scopes.size() - num_scopes; + unsigned old_lim = m_scopes[new_lvl]; + restore_entries(old_lim); + m_region.pop_scope(num_scopes); + m_scopes.shrink(new_lvl); +} + +void maximize_ac_sharing::restore_entries(unsigned old_lim) { + unsigned i = m_entries.size(); + while (i != old_lim) { + --i; + entry * e = m_entries[i]; + m.dec_ref(e->m_arg1); + m.dec_ref(e->m_arg2); + } + m_entries.shrink(old_lim); +} + +void maximize_ac_sharing::reset() { + restore_entries(0); + m_entries.reset(); + m_cache.reset(); + m_region.reset(); + m_scopes.reset(); +} + +void maximize_bv_sharing::init_core() { + register_kind(OP_BADD); + register_kind(OP_BMUL); + register_kind(OP_BOR); + register_kind(OP_BAND); +} + +bool maximize_bv_sharing::is_numeral(expr * n) const { + return m_util.is_numeral(n); +} + +maximize_bv_sharing::maximize_bv_sharing(ast_manager & m): + maximize_ac_sharing(m), + m_util(m) { +} diff --git a/src/ast/rewriter/maximize_ac_sharing.h b/src/ast/rewriter/maximize_ac_sharing.h new file mode 100644 index 000000000..c0ee0d09f --- /dev/null +++ b/src/ast/rewriter/maximize_ac_sharing.h @@ -0,0 +1,125 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + maximize_ac_sharing.h + +Abstract: + + + +Author: + + Leonardo de Moura (leonardo) 2008-10-22. + +Revision History: + +--*/ +#ifndef MAXIMIZE_AC_SHARING_H_ +#define MAXIMIZE_AC_SHARING_H_ + +#include "util/hashtable.h" +#include "util/region.h" +#include "ast/bv_decl_plugin.h" +#include "ast/rewriter/rewriter.h" + +/** + \brief Functor used to maximize the amount of shared terms in an expression. + The idea is to rewrite AC terms to maximize sharing. + Example: + + (f (bvadd a (bvadd b c)) (bvadd a (bvadd b d))) + + is rewritten to: + + (f (bvadd (bvadd a b) c) (bvadd (bvadd a b) d)) + + \warning This class uses an opportunistic heuristic to maximize sharing. + There is no guarantee that the optimal expression will be produced. +*/ +class maximize_ac_sharing : public default_rewriter_cfg { + + struct entry { + func_decl * m_decl; + expr * m_arg1; + expr * m_arg2; + + entry(func_decl * d = 0, expr * arg1 = 0, expr * arg2 = 0):m_decl(d), m_arg1(arg1), m_arg2(arg2) { + SASSERT((d == 0 && arg1 == 0 && arg2 == 0) || (d != 0 && arg1 != 0 && arg2 != 0)); + if (arg1->get_id() > arg2->get_id()) + std::swap(m_arg1, m_arg2); + } + + unsigned hash() const { + unsigned a = m_decl->get_id(); + unsigned b = m_arg1->get_id(); + unsigned c = m_arg2->get_id(); + mix(a,b,c); + return c; + } + + bool operator==(entry const & e) const { + return m_decl == e.m_decl && m_arg1 == e.m_arg1 && m_arg2 == e.m_arg2; + } + }; + + typedef ptr_hashtable, deref_eq > cache; + +protected: + void register_kind(decl_kind k); + +private: + ast_manager & m; + bool m_init; + region m_region; + cache m_cache; + ptr_vector m_entries; + unsigned_vector m_scopes; + svector m_kinds; //!< kinds to be processed + + bool contains(func_decl * f, expr * arg1, expr * arg2); + void insert(func_decl * f, expr * arg1, expr * arg2); + void restore_entries(unsigned old_lim); + void init() { + if (!m_init) { + init_core(); + m_init = true; + } + } +protected: + virtual void init_core() = 0; + virtual bool is_numeral(expr * n) const = 0; +public: + maximize_ac_sharing(ast_manager & m); + virtual ~maximize_ac_sharing(); + void push_scope(); + void pop_scope(unsigned num_scopes); + void reset(); + br_status reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr); + +}; + +class maximize_bv_sharing : public maximize_ac_sharing { + bv_util m_util; +protected: + virtual void init_core(); + virtual bool is_numeral(expr * n) const; +public: + maximize_bv_sharing(ast_manager & m); +}; + +class maximize_bv_sharing_rw : public rewriter_tpl { + maximize_bv_sharing m_cfg; +public: + maximize_bv_sharing_rw(ast_manager& m): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m) + {} + void push_scope() { m_cfg.push_scope(); } + void pop_scope(unsigned n) { m_cfg.pop_scope(n); } + void reset() { m_cfg.reset(); } +}; + +#endif /* MAXIMIZE_AC_SHARING_H_ */ +