mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix perf bug reported in #790

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-11-17 05:38:52 +02:00
parent 123b50ed3c
commit 1600823435
2 changed files with 25 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/ast/rewriter/bool_rewriter.cpp
View file

@ -456,6 +456,22 @@ bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, exp
return false; return false;
} }
void bool_rewriter::push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits) {
expr* narg;
if (m().is_not(arg, narg)) {
if (!neg_lits.is_marked(narg)) {
neg_lits.mark(narg);
new_args.push_back(arg);
}
}
else {
if (!pos_lits.is_marked(arg)) {
pos_lits.mark(arg);
new_args.push_back(arg);
}
}
}
/** /**
\brief Apply local context simplification at (OR args[0] ... args[num_args-1]) \brief Apply local context simplification at (OR args[0] ... args[num_args-1])
Basic idea: Basic idea:
@ -473,6 +489,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
bool modified = false; bool modified = false;
bool forward = true; bool forward = true;
unsigned rounds = 0; unsigned rounds = 0;
expr* narg;
while (true) { while (true) {
rounds++; rounds++;
@ -481,20 +498,13 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
verbose_stream() << "rounds: " << rounds << "\n"; verbose_stream() << "rounds: " << rounds << "\n";
#endif #endif
#define PUSH_NEW_ARG(ARG) { \
new_args.push_back(ARG); \
if (m().is_not(ARG)) \
neg_lits.mark(to_app(ARG)->get_arg(0)); \
else \
pos_lits.mark(ARG); \
}
#define PROCESS_ARG() \ #define PROCESS_ARG() \
{ \ { \
expr * arg = args[i]; \ expr * arg = args[i]; \
if (m().is_not(arg) && m().is_or(to_app(arg)->get_arg(0)) && \ if (m().is_not(arg, narg) && m().is_or(narg) && \
simp_nested_not_or(to_app(to_app(arg)->get_arg(0))->get_num_args(), \ simp_nested_not_or(to_app(narg)->get_num_args(), \
to_app(to_app(arg)->get_arg(0))->get_args(), \ to_app(narg)->get_args(), \
neg_lits, \ neg_lits, \
pos_lits, \ pos_lits, \
new_arg)) { \ new_arg)) { \
@ -515,11 +525,11 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
unsigned sz = to_app(arg)->get_num_args(); \ unsigned sz = to_app(arg)->get_num_args(); \
for (unsigned j = 0; j < sz; j++) { \ for (unsigned j = 0; j < sz; j++) { \
expr * arg_arg = to_app(arg)->get_arg(j); \ expr * arg_arg = to_app(arg)->get_arg(j); \
PUSH_NEW_ARG(arg_arg); \ push_new_arg(arg_arg, new_args, neg_lits, pos_lits); \
} \ } \
} \ } \
else { \ else { \
PUSH_NEW_ARG(arg); \ push_new_arg(arg, new_args, neg_lits, pos_lits); \
} \ } \
} }
@ -528,7 +538,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
static unsigned counter = 0; static unsigned counter = 0;
counter++; counter++;
if (counter % 10000 == 0) if (counter % 10000 == 0)
verbose_stream() << "local-ctx-cost: " << m_local_ctx_cost << "\n"; verbose_stream() << "local-ctx-cost: " << m_local_ctx_cost << " " << num_args << "\n";
#endif #endif
if (forward) { if (forward) {

2
src/ast/rewriter/bool_rewriter.h
View file

@ -75,6 +75,8 @@ class bool_rewriter {
bool local_ctx_simp(unsigned num_args, expr * const * args, expr_ref & result); bool local_ctx_simp(unsigned num_args, expr * const * args, expr_ref & result);
br_status try_ite_value(app * ite, app * val, expr_ref & result); br_status try_ite_value(app * ite, app * val, expr_ref & result);
void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits);
public: public:
bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); } bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); }
ast_manager & m() const { return m_manager; } ast_manager & m() const { return m_manager; }