mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

remove old_simplify dependencies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-28 13:29:51 -07:00
parent 9e4b2a6795
commit f20e95184e
14 changed files with 26 additions and 343 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/CMakeLists.txt
View file

@ -68,9 +68,6 @@ add_subdirectory(cmd_context)
add_subdirectory(cmd_context/extra_cmds)
add_subdirectory(parsers/smt2)
add_subdirectory(ast/proof_checker)
## Simplifier module will be deleted in the future.
## It has been replaced with rewriter component.
add_subdirectory(ast/simplifier)
add_subdirectory(ast/fpa)
add_subdirectory(ast/macros)
add_subdirectory(ast/pattern)

9
src/ast/simplifier/CMakeLists.txt
View file

@ -2,11 +2,11 @@ z3_add_component(simplifier
SOURCES
arith_simplifier_params.cpp
# arith_simplifier_plugin.cpp
array_simplifier_params.cpp
# array_simplifier_params.cpp
# array_simplifier_plugin.cpp
# basic_simplifier_plugin.cpp
# bv_elim.cpp
bv_simplifier_params.cpp
# bv_simplifier_params.cpp
# bv_simplifier_plugin.cpp
# datatype_simplifier_plugin.cpp
# elim_bounds.cpp
@ -18,8 +18,5 @@ z3_add_component(simplifier
# simplifier_plugin.cpp
COMPONENT_DEPENDENCIES
rewriter
PYG_FILES
arith_simplifier_params_helper.pyg
array_simplifier_params_helper.pyg
bv_simplifier_params_helper.pyg
)

6
src/ast/simplifier/array_simplifier_params.h
View file

@ -21,11 +21,9 @@ Revision History:
#include "util/params.h"
struct array_simplifier_params {
bool m_array_canonize_simplify;
bool m_array_simplify; // temporary hack for disabling array simplifier plugin.
struct array_simplifier_params1 {
array_simplifier_params(params_ref const & p = params_ref()) {
array_simplifier_params1(params_ref const & p = params_ref()) {
updt_params(p);
}

2
src/ast/simplifier/bv_simplifier_params.cpp
View file

@ -33,4 +33,4 @@ void bv_simplifier_params::updt_params(params_ref const & _p) {
void bv_simplifier_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_hi_div0);
DISPLAY_PARAM(m_bv2int_distribute);
}
}

192
src/ast/simplifier/maximise_ac_sharing.cpp
View file

@ -1,192 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
maximise_ac_sharing.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-22.
Revision History:
--*/
#include "ast/simplifier/maximise_ac_sharing.h"
#include "ast/ast_pp.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
maximise_ac_sharing::ac_plugin::ac_plugin(symbol const & fname, ast_manager & m, maximise_ac_sharing & owner):
simplifier_plugin(fname, m),
m_owner(owner) {
}
void maximise_ac_sharing::ac_plugin::register_kind(decl_kind k) {
m_kinds.push_back(k);
}
maximise_ac_sharing::ac_plugin::~ac_plugin() {
}
bool maximise_ac_sharing::ac_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
decl_kind k = f->get_kind();
if (!f->is_associative())
return false;
if (num_args <= 2)
return false;
if (std::find(m_kinds.begin(), m_kinds.end(), k) == m_kinds.end())
return false;
ptr_buffer<expr, 128> _args;
expr * numeral = 0;
if (m_owner.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_manager) << "\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 (m_owner.contains(f, _args[i], _args[j])) {
TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";);
_args[i] = m_manager.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 {
m_owner.insert(f, _args[i], _args[i+1]);
_args[j] = m_manager.mk_app(f, _args[i], _args[i+1]);
}
}
num_args = j;
if (num_args == 1) {
if (numeral == 0) {
result = _args[0];
}
else {
result = m_manager.mk_app(f, numeral, _args[0]);
}
TRACE("ac_sharing_detail", tout << "result: " << mk_pp(result, m_manager) << "\n";);
return true;
}
}
UNREACHABLE();
return false;
}
bool maximise_ac_sharing::contains(func_decl * f, expr * arg1, expr * arg2) {
entry e(f, arg1, arg2);
return m_cache.contains(&e);
}
void maximise_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_manager.inc_ref(arg1);
m_manager.inc_ref(arg2);
}
maximise_ac_sharing::maximise_ac_sharing(ast_manager & m):
m_manager(m),
m_simplifier(m),
m_init(false) {
basic_simplifier_plugin* basic_simp = alloc(basic_simplifier_plugin,m);
m_simplifier.register_plugin(basic_simp);
}
maximise_ac_sharing::~maximise_ac_sharing() {
restore_entries(0);
}
void maximise_ac_sharing::operator()(expr * s, expr_ref & r, proof_ref & p) {
init();
m_simplifier.operator()(s, r, p);
}
void maximise_ac_sharing::push_scope() {
init();
m_scopes.push_back(m_entries.size());
m_region.push_scope();
}
void maximise_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 maximise_ac_sharing::restore_entries(unsigned old_lim) {
unsigned i = m_entries.size();
while (i != old_lim) {
--i;
entry * e = m_entries[i];
m_manager.dec_ref(e->m_arg1);
m_manager.dec_ref(e->m_arg2);
}
m_entries.shrink(old_lim);
}
void maximise_ac_sharing::reset() {
restore_entries(0);
m_entries.reset();
m_cache.reset();
m_simplifier.reset();
m_region.reset();
m_scopes.reset();
}
void maximise_bv_sharing::init_core() {
maximise_ac_sharing::ac_plugin * p = alloc(maximise_ac_sharing::ac_plugin, symbol("bv"), get_manager(), *this);
p->register_kind(OP_BADD);
p->register_kind(OP_BMUL);
p->register_kind(OP_BOR);
p->register_kind(OP_BAND);
register_plugin(p);
}
bool maximise_bv_sharing::is_numeral(expr * n) const {
return m_util.is_numeral(n);
}
maximise_bv_sharing::maximise_bv_sharing(ast_manager & m):
maximise_ac_sharing(m),
m_util(m) {
}

124
src/ast/simplifier/maximise_ac_sharing.h
View file

@ -1,124 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
maximise_ac_sharing.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-22.
Revision History:
--*/
#ifndef MAXIMISE_AC_SHARING_H_
#define MAXIMISE_AC_SHARING_H_
#include "ast/simplifier/simplifier.h"
#include "util/hashtable.h"
#include "ast/bv_decl_plugin.h"
#include "util/region.h"
/**
\brief Functor used to maximise the amount of shared terms in an expression.
The idea is to rewrite AC terms to maximise 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 maximise sharing.
There is no guarantee that the optimal expression will be produced.
*/
class maximise_ac_sharing {
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:
class ac_plugin : public simplifier_plugin {
maximise_ac_sharing & m_owner;
svector<decl_kind> m_kinds; //!< kinds to be processed
public:
ac_plugin(symbol const & fname, ast_manager & m, maximise_ac_sharing & owner);
void register_kind(decl_kind k);
virtual ~ac_plugin();
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
};
friend class ac_plugin;
private:
ast_manager & m_manager;
simplifier m_simplifier;
bool m_init;
region m_region;
cache m_cache;
ptr_vector<entry> m_entries;
unsigned_vector m_scopes;
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;
void register_plugin(ac_plugin * p) { m_simplifier.register_plugin(p); }
public:
maximise_ac_sharing(ast_manager & m);
virtual ~maximise_ac_sharing();
void operator()(expr * s, expr_ref & r, proof_ref & p);
void push_scope();
void pop_scope(unsigned num_scopes);
void reset();
ast_manager & get_manager() { return m_manager; }
};
class maximise_bv_sharing : public maximise_ac_sharing {
bv_util m_util;
protected:
virtual void init_core();
virtual bool is_numeral(expr * n) const;
public:
maximise_bv_sharing(ast_manager & m);
};
#endif /* MAXIMISE_AC_SHARING_H_ */

1
src/smt/params/CMakeLists.txt
View file

@ -13,7 +13,6 @@ z3_add_component(smt_params
ast
bit_blaster
pattern
simplifier
PYG_FILES
smt_params_helper.pyg
)

4
src/smt/params/preprocessor_params.cpp
View file

@ -30,8 +30,6 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
void preprocessor_params::updt_params(params_ref const & p) {
pattern_inference_params::updt_params(p);
bv_simplifier_params::updt_params(p);
arith_simplifier_params::updt_params(p);
updt_local_params(p);
}
@ -40,8 +38,6 @@ void preprocessor_params::updt_params(params_ref const & p) {
void preprocessor_params::display(std::ostream & out) const {
pattern_inference_params::display(out);
bit_blaster_params::display(out);
bv_simplifier_params::display(out);
arith_simplifier_params::display(out);
DISPLAY_PARAM(m_lift_ite);
DISPLAY_PARAM(m_ng_lift_ite);

6
src/smt/params/preprocessor_params.h
View file

@ -21,8 +21,6 @@ Revision History:
#include "ast/pattern/pattern_inference_params.h"
#include "ast/rewriter/bit_blaster/bit_blaster_params.h"
#include "ast/simplifier/bv_simplifier_params.h"
#include "ast/simplifier/arith_simplifier_params.h"
enum lift_ite_kind {
LI_NONE,
@ -31,9 +29,7 @@ enum lift_ite_kind {
};
struct preprocessor_params : public pattern_inference_params,
public bit_blaster_params,
public bv_simplifier_params,
public arith_simplifier_params {
public bit_blaster_params {
lift_ite_kind m_lift_ite;
lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms
bool m_pull_cheap_ite_trees;

2
src/smt/params/theory_arith_params.cpp
View file

@ -42,6 +42,8 @@ void theory_arith_params::updt_params(params_ref const & _p) {
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_arith_expand_eqs);
DISPLAY_PARAM(m_arith_process_all_eqs);
DISPLAY_PARAM(m_arith_mode);
DISPLAY_PARAM(m_arith_auto_config_simplex); //!< force simplex solver in auto_config
DISPLAY_PARAM(m_arith_blands_rule_threshold);

4
src/smt/params/theory_arith_params.h
View file

@ -49,6 +49,8 @@ enum arith_pivot_strategy {
};
struct theory_arith_params {
bool m_arith_expand_eqs;
bool m_arith_process_all_eqs;
arith_solver_id m_arith_mode;
bool m_arith_auto_config_simplex; //!< force simplex solver in auto_config
unsigned m_arith_blands_rule_threshold;
@ -108,6 +110,8 @@ struct theory_arith_params {
theory_arith_params(params_ref const & p = params_ref()):
m_arith_expand_eqs(false),
m_arith_process_all_eqs(false),
m_arith_mode(AS_ARITH),
m_arith_auto_config_simplex(false),
m_arith_blands_rule_threshold(1000),

8
src/smt/params/theory_array_params.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef THEORY_ARRAY_PARAMS_H_
#define THEORY_ARRAY_PARAMS_H_
#include "ast/simplifier/array_simplifier_params.h"
#include "util/params.h"
enum array_solver_id {
AR_NO_ARRAY,
@ -28,7 +28,9 @@ enum array_solver_id {
AR_FULL
};
struct theory_array_params : public array_simplifier_params {
struct theory_array_params {
bool m_array_canonize_simplify;
bool m_array_simplify; // temporary hack for disabling array simplifier plugin.
array_solver_id m_array_mode;
bool m_array_weak;
bool m_array_extensional;
@ -40,6 +42,8 @@ struct theory_array_params : public array_simplifier_params {
unsigned m_array_lazy_ieq_delay;
theory_array_params():
m_array_canonize_simplify(false),
m_array_simplify(true),
m_array_mode(AR_FULL),
m_array_weak(false),
m_array_extensional(true),

6
src/smt/params/theory_bv_params.cpp
View file

@ -18,9 +18,12 @@ Revision History:
--*/
#include "smt/params/theory_bv_params.h"
#include "smt/params/smt_params_helper.hpp"
#include "ast/rewriter/bv_rewriter_params.hpp"
void theory_bv_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
bv_rewriter_params rp(_p);
m_hi_div0 = rp.hi_div0();
m_bv_reflect = p.bv_reflect();
m_bv_enable_int2bv2int = p.bv_enable_int2bv();
}
@ -29,9 +32,10 @@ void theory_bv_params::updt_params(params_ref const & _p) {
void theory_bv_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_bv_mode);
DISPLAY_PARAM(m_hi_div0);
DISPLAY_PARAM(m_bv_reflect);
DISPLAY_PARAM(m_bv_lazy_le);
DISPLAY_PARAM(m_bv_cc);
DISPLAY_PARAM(m_bv_blast_max_size);
DISPLAY_PARAM(m_bv_enable_int2bv2int);
}
}

2
src/smt/params/theory_bv_params.h
View file

@ -28,6 +28,7 @@ enum bv_solver_id {
struct theory_bv_params {
bv_solver_id m_bv_mode;
bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
bool m_bv_reflect;
bool m_bv_lazy_le;
bool m_bv_cc;
@ -35,6 +36,7 @@ struct theory_bv_params {
bool m_bv_enable_int2bv2int;
theory_bv_params(params_ref const & p = params_ref()):
m_bv_mode(BS_BLASTER),
m_hi_div0(false),
m_bv_reflect(true),
m_bv_lazy_le(false),
m_bv_cc(false),