mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

optimize rule processing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-26 12:02:19 -07:00
parent c58b4f9a53
commit b644fb9875
6 changed files with 55 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

59
src/ast/expr_abstract.cpp
View file

@ -20,52 +20,50 @@ Notes:
#include "expr_abstract.h" #include "expr_abstract.h"
#include "map.h" #include "map.h"
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
ast_ref_vector pinned(m);
ptr_vector<expr> stack;
obj_map<expr, expr*> map;
expr * curr = 0, *b = 0; expr * curr = 0, *b = 0;
SASSERT(n->get_ref_count() > 0); SASSERT(n->get_ref_count() > 0);
stack.push_back(n); m_stack.push_back(n);
for (unsigned i = 0; i < num_bound; ++i) { for (unsigned i = 0; i < num_bound; ++i) {
b = bound[i]; b = bound[i];
expr* v = m.mk_var(base + num_bound - i - 1, m.get_sort(b)); expr* v = m.mk_var(base + num_bound - i - 1, m.get_sort(b));
pinned.push_back(v); m_pinned.push_back(v);
map.insert(b, v); m_map.insert(b, v);
} }
while(!stack.empty()) { while(!m_stack.empty()) {
curr = stack.back(); curr = m_stack.back();
if (map.contains(curr)) { if (m_map.contains(curr)) {
stack.pop_back(); m_stack.pop_back();
continue; continue;
} }
switch(curr->get_kind()) { switch(curr->get_kind()) {
case AST_VAR: { case AST_VAR: {
map.insert(curr, curr); m_map.insert(curr, curr);
stack.pop_back(); m_stack.pop_back();
break; break;
} }
case AST_APP: { case AST_APP: {
app* a = to_app(curr); app* a = to_app(curr);
bool all_visited = true; bool all_visited = true;
ptr_vector<expr> args; m_args.reset();
for (unsigned i = 0; i < a->get_num_args(); ++i) { for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (!map.find(a->get_arg(i), b)) { if (!m_map.find(a->get_arg(i), b)) {
stack.push_back(a->get_arg(i)); m_stack.push_back(a->get_arg(i));
all_visited = false; all_visited = false;
} }
else { else {
args.push_back(b); m_args.push_back(b);
} }
} }
if (all_visited) { if (all_visited) {
b = m.mk_app(a->get_decl(), args.size(), args.c_ptr()); b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());
pinned.push_back(b); m_pinned.push_back(b);
map.insert(curr, b); m_map.insert(curr, b);
stack.pop_back(); m_stack.pop_back();
} }
break; break;
} }
@ -81,17 +79,24 @@ void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* cons
} }
expr_abstract(m, new_base, num_bound, bound, q->get_expr(), result1); expr_abstract(m, new_base, num_bound, bound, q->get_expr(), result1);
b = m.update_quantifier(q, patterns.size(), patterns.c_ptr(), result1.get()); b = m.update_quantifier(q, patterns.size(), patterns.c_ptr(), result1.get());
pinned.push_back(b); m_pinned.push_back(b);
map.insert(curr, b); m_map.insert(curr, b);
stack.pop_back(); m_stack.pop_back();
break; break;
} }
default: default:
UNREACHABLE(); UNREACHABLE();
} }
} }
if (!map.find(n, b)) { VERIFY (m_map.find(n, b));
UNREACHABLE();
}
result = b; result = b;
m_pinned.reset();
m_map.reset();
m_stack.reset();
m_args.reset();
}
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
expr_abstractor abs(m);
abs(base, num_bound, bound, n, result);
} }

11
src/ast/expr_abstract.h
View file

@ -21,6 +21,17 @@ Notes:
#include"ast.h" #include"ast.h"
class expr_abstractor {
ast_manager& m;
expr_ref_vector m_pinned;
ptr_vector<expr> m_stack, m_args;
obj_map<expr, expr*> m_map;
public:
expr_abstractor(ast_manager& m): m(m), m_pinned(m) {}
void operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result);
};
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result); void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result);
#endif #endif

16
src/ast/rewriter/var_subst.cpp
View file

@ -57,10 +57,10 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
m_used.process(q->get_pattern(i)); m_used.process(q->get_pattern(i));
unsigned num_no_patterns = q->get_num_no_patterns(); unsigned num_no_patterns = q->get_num_no_patterns();
for (unsigned i = 0; i < num_no_patterns; i++) for (unsigned i = 0; i < num_no_patterns; i++)
used.process(q->get_no_pattern(i)); m_used.process(q->get_no_pattern(i));
unsigned num_decls = q->get_num_decls(); unsigned num_decls = q->get_num_decls();
if (used.uses_all_vars(num_decls)) { if (m_used.uses_all_vars(num_decls)) {
q->set_no_unused_vars(); q->set_no_unused_vars();
result = q; result = q;
return; return;
@ -69,7 +69,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
ptr_buffer<sort> used_decl_sorts; ptr_buffer<sort> used_decl_sorts;
buffer<symbol> used_decl_names; buffer<symbol> used_decl_names;
for (unsigned i = 0; i < num_decls; ++i) { for (unsigned i = 0; i < num_decls; ++i) {
if (used.contains(num_decls - i - 1)) { if (m_used.contains(num_decls - i - 1)) {
used_decl_sorts.push_back(q->get_decl_sort(i)); used_decl_sorts.push_back(q->get_decl_sort(i));
used_decl_names.push_back(q->get_decl_name(i)); used_decl_names.push_back(q->get_decl_name(i));
} }
@ -78,10 +78,10 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
unsigned num_removed = 0; unsigned num_removed = 0;
expr_ref_buffer var_mapping(m); expr_ref_buffer var_mapping(m);
int next_idx = 0; int next_idx = 0;
unsigned sz = used.get_max_found_var_idx_plus_1(); unsigned sz = m_used.get_max_found_var_idx_plus_1();
for (unsigned i = 0; i < num_decls; ++i) { for (unsigned i = 0; i < num_decls; ++i) {
sort * s = used.contains(i); sort * s = m_used.contains(i);
if (s) { if (s) {
var_mapping.push_back(m.mk_var(next_idx, s)); var_mapping.push_back(m.mk_var(next_idx, s));
next_idx++; next_idx++;
@ -94,7 +94,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
// (VAR 0) is in the first position of var_mapping. // (VAR 0) is in the first position of var_mapping.
for (unsigned i = num_decls; i < sz; i++) { for (unsigned i = num_decls; i < sz; i++) {
sort * s = used.contains(i); sort * s = m_used.contains(i);
if (s) if (s)
var_mapping.push_back(m.mk_var(i - num_removed, s)); var_mapping.push_back(m.mk_var(i - num_removed, s));
else else
@ -122,11 +122,11 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
expr_ref_buffer new_no_patterns(m); expr_ref_buffer new_no_patterns(m);
for (unsigned i = 0; i < num_patterns; i++) { for (unsigned i = 0; i < num_patterns; i++) {
subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp); m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
new_patterns.push_back(tmp); new_patterns.push_back(tmp);
} }
for (unsigned i = 0; i < num_no_patterns; i++) { for (unsigned i = 0; i < num_no_patterns; i++) {
subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp); m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
new_no_patterns.push_back(tmp); new_no_patterns.push_back(tmp);
} }

4
src/muz_qe/dl_context.cpp
View file

@ -49,7 +49,6 @@ Revision History:
#include"dl_mk_quantifier_abstraction.h" #include"dl_mk_quantifier_abstraction.h"
#include"dl_mk_quantifier_instantiation.h" #include"dl_mk_quantifier_instantiation.h"
#include"datatype_decl_plugin.h" #include"datatype_decl_plugin.h"
#include"expr_abstract.h"
namespace datalog { namespace datalog {
@ -227,6 +226,7 @@ namespace datalog {
m_var_subst(m), m_var_subst(m),
m_rule_manager(*this), m_rule_manager(*this),
m_elim_unused_vars(m), m_elim_unused_vars(m),
m_abstractor(m),
m_transf(*this), m_transf(*this),
m_trail(*this), m_trail(*this),
m_pinned(m), m_pinned(m),
@ -307,7 +307,7 @@ namespace datalog {
} }
else { else {
ptr_vector<sort> sorts; ptr_vector<sort> sorts;
expr_abstract(m, 0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result); m_abstractor(0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
get_free_vars(result, sorts); get_free_vars(result, sorts);
if (sorts.empty()) { if (sorts.empty()) {
result = fml; result = fml;

2
src/muz_qe/dl_context.h
View file

@ -45,6 +45,7 @@ Revision History:
#include"model2expr.h" #include"model2expr.h"
#include"smt_params.h" #include"smt_params.h"
#include"dl_rule_transformer.h" #include"dl_rule_transformer.h"
#include"expr_abstract.h"
namespace datalog { namespace datalog {
@ -85,6 +86,7 @@ namespace datalog {
var_subst m_var_subst; var_subst m_var_subst;
rule_manager m_rule_manager; rule_manager m_rule_manager;
unused_vars_eliminator m_elim_unused_vars; unused_vars_eliminator m_elim_unused_vars;
expr_abstractor m_abstractor;
rule_transformer m_transf; rule_transformer m_transf;
trail_stack<context> m_trail; trail_stack<context> m_trail;
ast_ref_vector m_pinned; ast_ref_vector m_pinned;

1
src/muz_qe/dl_mk_array_blast.h
View file

@ -38,7 +38,6 @@ namespace datalog {
rule_manager& rm; rule_manager& rm;
params_ref m_params; params_ref m_params;
th_rewriter m_rewriter; th_rewriter m_rewriter;
ptr_vector<sort> m_vars;
mk_interp_tail_simplifier m_simplifier; mk_interp_tail_simplifier m_simplifier;
typedef obj_map<app, var*> defs_t; typedef obj_map<app, var*> defs_t;