mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 03:15:50 +00:00
mising files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
c03be16039
commit
14e6b5b500
2 changed files with 300 additions and 0 deletions
175
src/ast/rewriter/maximize_ac_sharing.cpp
Normal file
175
src/ast/rewriter/maximize_ac_sharing.cpp
Normal file
|
|
@ -0,0 +1,175 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
maximize_ac_sharing.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<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<expr, 128> _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) {
|
||||
}
|
||||
125
src/ast/rewriter/maximize_ac_sharing.h
Normal file
125
src/ast/rewriter/maximize_ac_sharing.h
Normal file
|
|
@ -0,0 +1,125 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
maximize_ac_sharing.h
|
||||
|
||||
Abstract:
|
||||
|
||||
<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<entry, obj_ptr_hash<entry>, deref_eq<entry> > cache;
|
||||
|
||||
protected:
|
||||
void register_kind(decl_kind k);
|
||||
|
||||
private:
|
||||
ast_manager & m;
|
||||
bool m_init;
|
||||
region m_region;
|
||||
cache m_cache;
|
||||
ptr_vector<entry> m_entries;
|
||||
unsigned_vector m_scopes;
|
||||
svector<decl_kind> 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> {
|
||||
maximize_bv_sharing m_cfg;
|
||||
public:
|
||||
maximize_bv_sharing_rw(ast_manager& m):
|
||||
rewriter_tpl<maximize_bv_sharing>(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_ */
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue