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

bypass stale rules as part of unbounded compression. Issue #624

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-27 09:38:23 -07:00
parent 50d334e4e9
commit 18a9b89e30
3 changed files with 100 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.h
View file

@ -838,6 +838,7 @@ inline bool is_func_decl(ast const * n) { return n->get_kind() == AST_FUNC_DECL
inline bool is_expr(ast const * n) { return !is_decl(n); } inline bool is_expr(ast const * n) { return !is_decl(n); }
inline bool is_app(ast const * n) { return n->get_kind() == AST_APP; } inline bool is_app(ast const * n) { return n->get_kind() == AST_APP; }
inline bool is_var(ast const * n) { return n->get_kind() == AST_VAR; } inline bool is_var(ast const * n) { return n->get_kind() == AST_VAR; }
inline bool is_var(ast const * n, unsigned& idx) { return is_var(n) && (idx = static_cast<var const*>(n)->get_idx(), true); }
inline bool is_quantifier(ast const * n) { return n->get_kind() == AST_QUANTIFIER; } inline bool is_quantifier(ast const * n) { return n->get_kind() == AST_QUANTIFIER; }
inline bool is_forall(ast const * n) { return is_quantifier(n) && static_cast<quantifier const *>(n)->is_forall(); } inline bool is_forall(ast const * n) { return is_quantifier(n) && static_cast<quantifier const *>(n)->is_forall(); }
inline bool is_exists(ast const * n) { return is_quantifier(n) && static_cast<quantifier const *>(n)->is_exists(); } inline bool is_exists(ast const * n) { return is_quantifier(n) && static_cast<quantifier const *>(n)->is_exists(); }

149
src/muz/transforms/dl_mk_unbound_compressor.cpp
View file

@ -43,12 +43,10 @@ namespace datalog {
bool mk_unbound_compressor::is_unbound_argument(rule * r, unsigned head_index) { bool mk_unbound_compressor::is_unbound_argument(rule * r, unsigned head_index) {
app * head = r->get_head(); app * head = r->get_head();
expr * head_arg = head->get_arg(head_index); expr * head_arg = head->get_arg(head_index);
if (!is_var(head_arg)) { unsigned var_idx;
return false; return
} is_var(head_arg, var_idx) &&
unsigned var_idx = to_var(head_arg)->get_idx(); rm.collect_tail_vars(r).contains(var_idx);
return rm.collect_tail_vars(r).contains(var_idx);
} }
void mk_unbound_compressor::add_task(func_decl * pred, unsigned arg_index) { void mk_unbound_compressor::add_task(func_decl * pred, unsigned arg_index) {
@ -74,9 +72,11 @@ namespace datalog {
func_decl * cpred = m_context.mk_fresh_head_predicate(parent_name, symbol(name_suffix.str().c_str()), func_decl * cpred = m_context.mk_fresh_head_predicate(parent_name, symbol(name_suffix.str().c_str()),
arity, domain.c_ptr(), pred); arity, domain.c_ptr(), pred);
m_pinned.push_back(cpred); m_pinned.push_back(cpred);
m_pinned.push_back(pred);
m_todo.push_back(ci); m_todo.push_back(ci);
m_map.insert(ci, cpred); m_map.insert(ci, cpred);
TRACE("dl", tout << "inserting: " << pred->get_name() << " " << arg_index << " for " << cpred->get_name() << "\n";);
} }
void mk_unbound_compressor::detect_tasks(rule_set const& source, unsigned rule_index) { void mk_unbound_compressor::detect_tasks(rule_set const& source, unsigned rule_index) {
@ -97,26 +97,25 @@ namespace datalog {
for (unsigned i = 0; i < n; i++) { for (unsigned i = 0; i < n; i++) {
expr * arg = head->get_arg(i); expr * arg = head->get_arg(i);
if (!is_var(arg)) { unsigned var_idx;
continue; if (is_var(arg, var_idx) &&
} !tail_vars.contains(var_idx) &&
unsigned var_idx = to_var(arg)->get_idx(); (1 == rm.get_counter().get(var_idx))) {
if (!tail_vars.contains(var_idx)) {
//unbound
unsigned occurence_cnt = rm.get_counter().get(var_idx);
SASSERT(occurence_cnt>0);
if (occurence_cnt == 1) {
TRACE("dl", r->display(m_context, tout << "Compress: ");); TRACE("dl", r->display(m_context, tout << "Compress: "););
add_task(head_pred, i); add_task(head_pred, i);
return; //we compress out the unbound arguments one by one break;
} //we compress out the unbound arguments one by one
} }
} }
} }
void mk_unbound_compressor::try_compress(rule_set const& source, unsigned rule_index) { //
start: // l_undef if nothing to compress.
// l_true if compressed.
// l_false if removed.
//
lbool mk_unbound_compressor::try_compress(rule_set const& source, unsigned rule_index) {
TRACE("dl", tout << rule_index << "\n";);
rule * r = m_rules.get(rule_index); rule * r = m_rules.get(rule_index);
var_idx_set& tail_vars = rm.collect_tail_vars(r); var_idx_set& tail_vars = rm.collect_tail_vars(r);
@ -130,28 +129,22 @@ namespace datalog {
unsigned arg_index; unsigned arg_index;
for (arg_index = 0; arg_index < head_arity; arg_index++) { for (arg_index = 0; arg_index < head_arity; arg_index++) {
expr * arg = head->get_arg(arg_index); expr * arg = head->get_arg(arg_index);
if (!is_var(arg)) { unsigned var_idx;
continue; if (is_var(arg, var_idx) &&
} !tail_vars.contains(var_idx) &&
unsigned var_idx = to_var(arg)->get_idx(); (rm.get_counter().get(var_idx) == 1) &&
if (!tail_vars.contains(var_idx)) { m_in_progress.contains(c_info(head_pred, arg_index))) {
//unbound
unsigned occurence_cnt = rm.get_counter().get(var_idx);
SASSERT(occurence_cnt>0);
if ( occurence_cnt==1 && m_in_progress.contains(c_info(head_pred, arg_index)) ) {
//we have found what to compress
break; break;
} }
} }
}
if (arg_index == head_arity) { if (arg_index == head_arity) {
//we didn't find anything to compress //we didn't find anything to compress
return; return l_undef;
} }
SASSERT(arg_index < head_arity); SASSERT(arg_index < head_arity);
c_info ci(head_pred, arg_index); c_info ci(head_pred, arg_index);
func_decl * cpred; func_decl * cpred = m_map.find(ci);
TRUSTME( m_map.find(ci, cpred) ); // VERIFY( m_map.find(ci, cpred) );
ptr_vector<expr> cargs; ptr_vector<expr> cargs;
for (unsigned i=0; i < head_arity; i++) { for (unsigned i=0; i < head_arity; i++) {
if (i != arg_index) { if (i != arg_index) {
@ -161,29 +154,34 @@ namespace datalog {
app_ref chead(m.mk_app(cpred, head_arity-1, cargs.c_ptr()), m); app_ref chead(m.mk_app(cpred, head_arity-1, cargs.c_ptr()), m);
m_modified = true;
if (r->get_tail_size()==0 && m_context.get_rule_manager().is_fact(chead)) { if (r->get_tail_size()==0 && m_context.get_rule_manager().is_fact(chead)) {
m_non_empty_rels.insert(cpred); m_non_empty_rels.insert(cpred);
m_context.add_fact(chead); m_context.add_fact(chead);
//remove the rule that became fact by placing the last rule on its place //remove the rule that became fact by placing the last rule on its place
m_head_occurrence_ctr.dec(m_rules.get(rule_index)->get_decl()); m_head_occurrence_ctr.dec(m_rules.get(rule_index)->get_decl());
m_rules.set(rule_index, m_rules.get(m_rules.size()-1)); unsigned new_size = m_rules.size() - 1;
m_rules.shrink(m_rules.size()-1); rule* last_rule = m_rules.get(new_size);
//since we moved the last rule to rule_index, we have to try to compress it as well TRACE("dl", tout << "remove\n"; r->display(m_context, tout);
if (rule_index<m_rules.size()) { tout << "shift\n"; last_rule->display(m_context, tout););
goto start; if (rule_index < new_size) {
m_rules.set(rule_index, last_rule);
} }
m_rules.shrink(new_size);
return l_false;
} }
else { else {
rule_ref new_rule(m_context.get_rule_manager().mk(r, chead), m_context.get_rule_manager()); rule_ref new_rule(m_context.get_rule_manager().mk(r, chead), m_context.get_rule_manager());
new_rule->set_accounting_parent_object(m_context, r); new_rule->set_accounting_parent_object(m_context, r);
m_head_occurrence_ctr.dec(m_rules.get(rule_index)->get_decl()); m_head_occurrence_ctr.dec(m_rules.get(rule_index)->get_decl());
TRACE("dl", tout << "remove\n"; r->display(m_context, tout);
tout << "set\n"; new_rule->display(m_context, tout););
m_rules.set(rule_index, new_rule); m_rules.set(rule_index, new_rule);
m_head_occurrence_ctr.inc(m_rules.get(rule_index)->get_decl()); m_head_occurrence_ctr.inc(m_rules.get(rule_index)->get_decl());
detect_tasks(source, rule_index); detect_tasks(source, rule_index);
return l_true;
} }
m_modified = true;
} }
void mk_unbound_compressor::mk_decompression_rule(rule * r, unsigned tail_index, unsigned arg_index, void mk_unbound_compressor::mk_decompression_rule(rule * r, unsigned tail_index, unsigned arg_index,
@ -191,8 +189,11 @@ namespace datalog {
{ {
app * orig_dtail = r->get_tail(tail_index); //dtail ~ decompressed tail app * orig_dtail = r->get_tail(tail_index); //dtail ~ decompressed tail
c_info ci(orig_dtail->get_decl(), arg_index); c_info ci(orig_dtail->get_decl(), arg_index);
func_decl * dtail_pred;
TRUSTME( m_map.find(ci, dtail_pred) ); TRACE("dl", tout << "retrieving: " << ci.first->get_name() << " " << ci.second << "\n";);
func_decl * dtail_pred; // = m_map.find(ci);
VERIFY( m_map.find(ci, dtail_pred) );
ptr_vector<expr> dtail_args; ptr_vector<expr> dtail_args;
unsigned orig_dtail_arity = orig_dtail->get_num_args(); unsigned orig_dtail_arity = orig_dtail->get_num_args();
for (unsigned i = 0; i < orig_dtail_arity; i++) { for (unsigned i = 0; i < orig_dtail_arity; i++) {
@ -228,19 +229,6 @@ namespace datalog {
m_context.get_rule_manager().fix_unbound_vars(res, true); m_context.get_rule_manager().fix_unbound_vars(res, true);
} }
void mk_unbound_compressor::add_decompression_rule(rule_set const& source, rule * r, unsigned tail_index, unsigned arg_index) {
rule_ref new_rule(m_context.get_rule_manager());
mk_decompression_rule(r, tail_index, arg_index, new_rule);
unsigned new_rule_index = m_rules.size();
m_rules.push_back(new_rule);
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule.get());
m_head_occurrence_ctr.inc(new_rule->get_decl());
detect_tasks(source, new_rule_index);
m_modified = true;
//TODO: avoid rule duplicity //TODO: avoid rule duplicity
//If two predicates are compressed in a rule, applying decompression //If two predicates are compressed in a rule, applying decompression
@ -252,21 +240,28 @@ namespace datalog {
//and each of these rules is again decompressed giving the same rule //and each of these rules is again decompressed giving the same rule
//P:- R1(x), S1(x) //P:- R1(x), S1(x)
//P:- R1(x), S1(x) //P:- R1(x), S1(x)
void mk_unbound_compressor::add_decompression_rule(rule_set const& source, rule * r, unsigned tail_index, unsigned arg_index) {
rule_ref new_rule(m_context.get_rule_manager());
mk_decompression_rule(r, tail_index, arg_index, new_rule);
unsigned new_rule_index = m_rules.size();
m_rules.push_back(new_rule);
TRACE("dl", r->display(m_context, tout); new_rule->display(m_context, tout); );
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule.get());
m_head_occurrence_ctr.inc(new_rule->get_decl());
detect_tasks(source, new_rule_index);
m_modified = true;
} }
void mk_unbound_compressor::replace_by_decompression_rule(rule_set const& source, unsigned rule_index, unsigned tail_index, unsigned arg_index) void mk_unbound_compressor::replace_by_decompression_rule(rule_set const& source, unsigned rule_index, unsigned tail_index, unsigned arg_index)
{ {
rule * r = m_rules.get(rule_index); rule * r = m_rules.get(rule_index);
rule_ref new_rule(m_context.get_rule_manager()); rule_ref new_rule(m_context.get_rule_manager());
mk_decompression_rule(r, tail_index, arg_index, new_rule); mk_decompression_rule(r, tail_index, arg_index, new_rule);
TRACE("dl", tout << "remove\n"; r->display(m_context, tout); tout << "set\n"; new_rule->display(m_context, tout););
m_rules.set(rule_index, new_rule); m_rules.set(rule_index, new_rule);
//we don't update the m_head_occurrence_ctr because the head predicate doesn't change //we don't update the m_head_occurrence_ctr because the head predicate doesn't change
detect_tasks(source, rule_index); detect_tasks(source, rule_index);
m_modified = true; m_modified = true;
} }
@ -279,6 +274,11 @@ namespace datalog {
unsigned utail_len = r->get_uninterpreted_tail_size(); unsigned utail_len = r->get_uninterpreted_tail_size();
unsigned tail_index = 0; unsigned tail_index = 0;
#if 0
if (utail_len == 1 && r->is_neg_tail(0)) {
tail_index = utail_len;
}
#endif
while (tail_index < utail_len) { while (tail_index < utail_len) {
app * t = r->get_tail(tail_index); app * t = r->get_tail(tail_index);
func_decl * t_pred = t->get_decl(); func_decl * t_pred = t->get_decl();
@ -291,7 +291,8 @@ namespace datalog {
compressed_tail_pred_arg_indexes.push_back(arg_index); compressed_tail_pred_arg_indexes.push_back(arg_index);
} }
} }
bool orig_rule_replaced = false; TRACE("dl", tout << compressed_tail_pred_arg_indexes.size() << "\n";);
bool replace_original_rule = false;
while (!compressed_tail_pred_arg_indexes.empty()) { while (!compressed_tail_pred_arg_indexes.empty()) {
unsigned arg_index = compressed_tail_pred_arg_indexes.back(); unsigned arg_index = compressed_tail_pred_arg_indexes.back();
compressed_tail_pred_arg_indexes.pop_back(); compressed_tail_pred_arg_indexes.pop_back();
@ -302,14 +303,16 @@ namespace datalog {
m_head_occurrence_ctr.get(t_pred)==0; m_head_occurrence_ctr.get(t_pred)==0;
if (can_remove_orig_rule || is_negated_predicate) { if (can_remove_orig_rule || is_negated_predicate) {
replace_original_rule = true;
replace_by_decompression_rule(source, rule_index, tail_index, arg_index); replace_by_decompression_rule(source, rule_index, tail_index, arg_index);
orig_rule_replaced = true; // NB. compressed_tail_pred_arg_indexes becomes stale after original rule is replaced.
break;
} }
else { else {
add_decompression_rule(source, r, tail_index, arg_index); add_decompression_rule(source, r, tail_index, arg_index);
} }
} }
if (orig_rule_replaced) { if (replace_original_rule) {
//update r with the new rule //update r with the new rule
rule * new_rule = m_rules.get(rule_index); rule * new_rule = m_rules.get(rule_index);
SASSERT(new_rule->get_uninterpreted_tail_size() >= utail_len); SASSERT(new_rule->get_uninterpreted_tail_size() >= utail_len);
@ -334,12 +337,13 @@ namespace datalog {
// TODO mc // TODO mc
m_modified = false; m_modified = false;
SASSERT(m_rules.empty());
rel_context_base* rel = m_context.get_rel_context(); rel_context_base* rel = m_context.get_rel_context();
if (rel) { if (rel) {
rel->collect_non_empty_predicates(m_non_empty_rels); rel->collect_non_empty_predicates(m_non_empty_rels);
} }
unsigned init_rule_cnt = source.get_num_rules(); unsigned init_rule_cnt = source.get_num_rules();
SASSERT(m_rules.empty());
for (unsigned i = 0; i < init_rule_cnt; i++) { for (unsigned i = 0; i < init_rule_cnt; i++) {
rule * r = source.get_rule(i); rule * r = source.get_rule(i);
m_rules.push_back(r); m_rules.push_back(r);
@ -358,11 +362,18 @@ namespace datalog {
} }
unsigned rule_index = 0; unsigned rule_index = 0;
while (rule_index < m_rules.size()) { while (rule_index < m_rules.size()) {
try_compress(source, rule_index); //m_rules.size() can change here switch (try_compress(source, rule_index)) {
if (rule_index<m_rules.size()) { case l_true:
add_decompression_rules(source, rule_index); //m_rules.size() can change here add_decompression_rules(source, rule_index); //m_rules.size() can be increased here
++rule_index;
break;
case l_false:
break;
case l_undef:
add_decompression_rules(source, rule_index); //m_rules.size() can be increased here
++rule_index;
break;
} }
rule_index++;
} }
} }

2
src/muz/transforms/dl_mk_unbound_compressor.h
View file

@ -74,7 +74,7 @@ namespace datalog {
void detect_tasks(rule_set const& source, unsigned rule_index); void detect_tasks(rule_set const& source, unsigned rule_index);
void add_task(func_decl * pred, unsigned arg_index); void add_task(func_decl * pred, unsigned arg_index);
void try_compress(rule_set const& source, unsigned rule_index); lbool try_compress(rule_set const& source, unsigned rule_index);
void add_decompression_rules(rule_set const& source, unsigned rule_index); void add_decompression_rules(rule_set const& source, unsigned rule_index);
void mk_decompression_rule(rule * r, unsigned tail_index, unsigned arg_index, rule_ref& res); void mk_decompression_rule(rule * r, unsigned tail_index, unsigned arg_index, rule_ref& res);
void add_decompression_rule(rule_set const& source, rule * r, unsigned tail_index, unsigned arg_index); void add_decompression_rule(rule_set const& source, rule * r, unsigned tail_index, unsigned arg_index);