From 6e47499e267e5c7101c80ad405e333cbf953bb07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 10:09:18 -0700 Subject: [PATCH] fix #4434 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_array_eq_rewrite.cpp | 6 +- .../transforms/dl_mk_array_instantiation.cpp | 516 ++++++++---------- src/muz/transforms/dl_mk_backwards.cpp | 4 +- src/muz/transforms/dl_mk_coalesce.cpp | 8 +- .../dl_mk_interp_tail_simplifier.cpp | 5 +- src/muz/transforms/dl_mk_loop_counter.cpp | 4 +- src/muz/transforms/dl_mk_magic_sets.cpp | 4 +- src/muz/transforms/dl_mk_magic_symbolic.cpp | 4 +- .../dl_mk_quantifier_abstraction.cpp | 5 +- .../dl_mk_quantifier_instantiation.cpp | 5 +- src/muz/transforms/dl_mk_scale.cpp | 4 +- src/muz/transforms/dl_mk_slice.cpp | 5 +- .../transforms/dl_mk_subsumption_checker.cpp | 8 +- 13 files changed, 268 insertions(+), 310 deletions(-) diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp index c8a3d4357..c37370d14 100644 --- a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp +++ b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp @@ -38,14 +38,14 @@ namespace datalog { rule_set * mk_array_eq_rewrite::operator()(rule_set const & source) { m_src_set = &source; - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); result->inherit_predicates(source); - m_dst = result; + m_dst = result.get(); m_src_manager = &source.get_rule_manager(); for (rule * rp : source) { instantiate_rule(*rp, *result); } - return result; + return result.detach(); } void mk_array_eq_rewrite::instantiate_rule(const rule& r, rule_set & dest) diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp index a94383453..9c962d774 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.cpp +++ b/src/muz/transforms/dl_mk_array_instantiation.cpp @@ -27,7 +27,7 @@ Revision History: namespace datalog { - mk_array_instantiation::mk_array_instantiation( + mk_array_instantiation::mk_array_instantiation( context & ctx, unsigned priority): plugin(priority), m(ctx.get_manager()), @@ -35,289 +35,253 @@ namespace datalog { m_a(m), eq_classes(m), ownership(m) - { - } - - rule_set * mk_array_instantiation::operator()(rule_set const & source) - { - std::cout<<"Array Instantiation called with parameters :" - <<" enforce="<display(std::cout); - return result; - } - - void mk_array_instantiation::instantiate_rule(const rule& r, rule_set & dest) - { - //Reset everything - selects.reset(); - eq_classes.reset(); - cnt = src_manager->get_counter().get_max_rule_var(r)+1; - done_selects.reset(); - ownership.reset(); - - expr_ref_vector phi(m); - expr_ref_vector preds(m); - expr_ref new_head = create_head(to_app(r.get_head())); - unsigned nb_predicates = r.get_uninterpreted_tail_size(); - unsigned tail_size = r.get_tail_size(); - for(unsigned i=0;i::iterator it = done_selects.begin(); it!=done_selects.end(); ++it) - { - expr_ref tmp(m); - tmp = &it->get_key(); - new_tail.push_back(m.mk_eq(it->get_value(), tmp)); - } - proof_ref pr(m); - src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail.size(), new_tail.c_ptr()), new_head), pr, dest, r.name()); - } - - expr_ref mk_array_instantiation::create_head(app* old_head) - { - expr_ref_vector new_args(m); - for(unsigned i=0;iget_num_args();i++) - { - expr*arg = old_head->get_arg(i); - if(m_a.is_array(get_sort(arg))) - { - for(unsigned k=0; k< m_ctx.get_params().xform_instantiate_arrays_nb_quantifier();k++) - { - expr_ref_vector dummy_args(m); - dummy_args.push_back(arg); - for(unsigned i=0;i()); - selects[arg].push_back(select); - } - if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) - new_args.push_back(arg); - } - else - new_args.push_back(arg); - } - return create_pred(old_head, new_args); - } - - - void mk_array_instantiation::retrieve_selects(expr* e) - { - //If the expression is not a function application, we ignore it - if (!is_app(e)) { - return; - } - app*f=to_app(e); - //Call the function recursively on all arguments - unsigned nbargs = f->get_num_args(); - for(unsigned i=0;iget_arg(i)); - } - //If it is a select, then add it to selects - if(m_a.is_select(f)) - { - SASSERT(!m_a.is_array(get_sort(e))); - selects.insert_if_not_there(f->get_arg(0), ptr_vector()); - selects[f->get_arg(0)].push_back(e); - } - //If it is a condition between arrays, for example the result of a store, then add it to the equiv_classes - if(m_a.is_store(f)) - { - eq_classes.merge(e, f->get_arg(0)); - } - else if(m.is_eq(f) && m_a.is_array(get_sort(f->get_arg(0)))) - { - eq_classes.merge(f->get_arg(0), f->get_arg(1)); - } - } - - - expr_ref_vector mk_array_instantiation::getId(app*old_pred, const expr_ref_vector& n_args) - { - expr_ref_vector res(m); - for(unsigned i=0;iget_num_args();j++) - { - res.push_back(select->get_arg(j)); + rule_set * mk_array_instantiation::operator()(rule_set const & source) { + std::cout<<"Array Instantiation called with parameters :" + <<" enforce="< result = alloc(rule_set, m_ctx); + dst = result.get(); + unsigned nbrules = source.get_num_rules(); + src_manager = &source.get_rule_manager(); + for(unsigned i = 0; i < nbrules; i++) { + rule & r = *source.get_rule(i); + instantiate_rule(r, *result); } - } + std::cout<<"\n\nOutput rules = \n"; + result->display(std::cout); + return result.detach(); } - return res; - } - expr_ref mk_array_instantiation::create_pred(app*old_pred, expr_ref_vector& n_args) - { - expr_ref_vector new_args(m); - new_args.append(n_args); - new_args.append(getId(old_pred, n_args)); - for(unsigned i=0;iget_decl()->get_name().str()+"!inst").c_str()), new_sorts.size(), new_sorts.c_ptr(), old_pred->get_decl()->get_range()); - m_ctx.register_predicate(fun_decl, false); - if(src_set->is_output_predicate(old_pred->get_decl())) - dst->set_output_predicate(fun_decl); - res=m.mk_app(fun_decl,new_args.size(), new_args.c_ptr()); - return res; - } + void mk_array_instantiation::instantiate_rule(const rule& r, rule_set & dest) { + //Reset everything + selects.reset(); + eq_classes.reset(); + cnt = src_manager->get_counter().get_max_rule_var(r)+1; + done_selects.reset(); + ownership.reset(); - var * mk_array_instantiation::mk_select_var(expr* select) - { - var*result; - if(!done_selects.find(select, result)) - { - ownership.push_back(select); - result = m.mk_var(cnt, get_sort(select)); - cnt++; - done_selects.insert(select, result); - } - return result; - } - - expr_ref mk_array_instantiation::rewrite_select(expr*array, expr*select) - { - app*s = to_app(select); - expr_ref res(m); - expr_ref_vector args(m); - args.push_back(array); - for(unsigned i=1; iget_num_args();i++) - { - args.push_back(s->get_arg(i)); - } - res = m_a.mk_select(args.size(), args.c_ptr()); - return res; - } - - expr_ref_vector mk_array_instantiation::retrieve_all_selects(expr*array) - { - expr_ref_vector all_selects(m); - for(expr_equiv_class::iterator it = eq_classes.begin(array); - it != eq_classes.end(array); ++it) - { - selects.insert_if_not_there(*it, ptr_vector()); - ptr_vector& select_ops = selects[*it]; - for(unsigned i=0;iget_num_args(); - //Stores, for each old position, the list of a new possible arguments - vector arg_correspondance; - for(unsigned i=0;iget_arg(i), m); - if(m_a.is_array(get_sort(arg))) - { - vector arg_possibilities(m_ctx.get_params().xform_instantiate_arrays_nb_quantifier(), retrieve_all_selects(arg)); - arg_correspondance.append(arg_possibilities); - if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) - { - expr_ref_vector tmp(m); - tmp.push_back(arg); - arg_correspondance.push_back(tmp); + expr_ref_vector phi(m); + expr_ref_vector preds(m); + expr_ref new_head = create_head(to_app(r.get_head())); + unsigned nb_predicates = r.get_uninterpreted_tail_size(); + unsigned tail_size = r.get_tail_size(); + for(unsigned i=0;i chosen(arg_correspondance.size(), 0u); - while(true) - { - expr_ref_vector new_args(m); - for(unsigned i=0;i::iterator it = done_selects.begin(); it!=done_selects.end(); ++it) { + expr_ref tmp(m); + tmp = &it->get_key(); + new_tail.push_back(m.mk_eq(it->get_value(), tmp)); + } + proof_ref pr(m); + src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail.size(), new_tail.c_ptr()), new_head), pr, dest, r.name()); + } + + expr_ref mk_array_instantiation::create_head(app* old_head) { + expr_ref_vector new_args(m); + for(unsigned i=0;iget_num_args();i++) { + expr*arg = old_head->get_arg(i); + if(m_a.is_array(get_sort(arg))) { + for(unsigned k=0; k< m_ctx.get_params().xform_instantiate_arrays_nb_quantifier();k++) { + expr_ref_vector dummy_args(m); + dummy_args.push_back(arg); + for(unsigned i=0;i()); + selects[arg].push_back(select); + } + if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) + new_args.push_back(arg); + } + else + new_args.push_back(arg); + } + return create_pred(old_head, new_args); + } + + + void mk_array_instantiation::retrieve_selects(expr* e) { + //If the expression is not a function application, we ignore it + if (!is_app(e)) { + return; + } + app*f=to_app(e); + //Call the function recursively on all arguments + unsigned nbargs = f->get_num_args(); + for(unsigned i=0;iget_arg(i)); + } + //If it is a select, then add it to selects + if(m_a.is_select(f)) { + SASSERT(!m_a.is_array(get_sort(e))); + selects.insert_if_not_there(f->get_arg(0), ptr_vector()); + selects[f->get_arg(0)].push_back(e); + } + //If it is a condition between arrays, for example the result of a store, then add it to the equiv_classes + if(m_a.is_store(f)) { + eq_classes.merge(e, f->get_arg(0)); + } + else if(m.is_eq(f) && m_a.is_array(get_sort(f->get_arg(0)))) { + eq_classes.merge(f->get_arg(0), f->get_arg(1)); + } + } + + + expr_ref_vector mk_array_instantiation::getId(app*old_pred, const expr_ref_vector& n_args) + { + expr_ref_vector res(m); + for(unsigned i=0;iget_num_args();j++) { + res.push_back(select->get_arg(j)); + } + } + } + return res; + } + + expr_ref mk_array_instantiation::create_pred(app*old_pred, expr_ref_vector& n_args) + { + expr_ref_vector new_args(m); + new_args.append(n_args); + new_args.append(getId(old_pred, n_args)); + for(unsigned i=0;iget_decl()->get_name().str()+"!inst").c_str()), new_sorts.size(), new_sorts.c_ptr(), old_pred->get_decl()->get_range()); + m_ctx.register_predicate(fun_decl, false); + if(src_set->is_output_predicate(old_pred->get_decl())) + dst->set_output_predicate(fun_decl); + res=m.mk_app(fun_decl,new_args.size(), new_args.c_ptr()); + return res; + } + + var * mk_array_instantiation::mk_select_var(expr* select) + { + var*result; + if(!done_selects.find(select, result)) { + ownership.push_back(select); + result = m.mk_var(cnt, get_sort(select)); + cnt++; + done_selects.insert(select, result); + } + return result; + } + + expr_ref mk_array_instantiation::rewrite_select(expr*array, expr*select) + { + app*s = to_app(select); + expr_ref res(m); + expr_ref_vector args(m); + args.push_back(array); + for(unsigned i=1; iget_num_args();i++) { + args.push_back(s->get_arg(i)); + } + res = m_a.mk_select(args.size(), args.c_ptr()); + return res; + } + + expr_ref_vector mk_array_instantiation::retrieve_all_selects(expr*array) + { + expr_ref_vector all_selects(m); + for(expr_equiv_class::iterator it = eq_classes.begin(array); + it != eq_classes.end(array); ++it) { + selects.insert_if_not_there(*it, ptr_vector()); + ptr_vector& select_ops = selects[*it]; + for(unsigned i=0;iget_num_args(); + //Stores, for each old position, the list of a new possible arguments + vector arg_correspondance; + for(unsigned i=0;iget_arg(i), m); + if(m_a.is_array(get_sort(arg))) { + vector arg_possibilities(m_ctx.get_params().xform_instantiate_arrays_nb_quantifier(), retrieve_all_selects(arg)); + arg_correspondance.append(arg_possibilities); + if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) { + expr_ref_vector tmp(m); + tmp.push_back(arg); + arg_correspondance.push_back(tmp); + } + } + else { + expr_ref_vector tmp(m); + tmp.push_back(arg); + arg_correspondance.push_back(tmp); + } + } + //Now, we need to deal with every combination + + expr_ref_vector res(m); + + svector chosen(arg_correspondance.size(), 0u); + while(true) { + expr_ref_vector new_args(m); + for(unsigned i=0;i=arg_correspondance[pos].size()); + chosen[pos]++; } - }while(chosen[pos]+1>=arg_correspondance[pos].size()); - chosen[pos]++; } - } } diff --git a/src/muz/transforms/dl_mk_backwards.cpp b/src/muz/transforms/dl_mk_backwards.cpp index 0aa3c4d9a..4899ed126 100644 --- a/src/muz/transforms/dl_mk_backwards.cpp +++ b/src/muz/transforms/dl_mk_backwards.cpp @@ -33,7 +33,7 @@ namespace datalog { rule_set * mk_backwards::operator()(rule_set const & source) { context& ctx = source.get_context(); rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, ctx); + scoped_ptr result = alloc(rule_set, ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); @@ -72,7 +72,7 @@ namespace datalog { } } TRACE("dl", result->display(tout);); - return result; + return result.detach(); } }; diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp index 6613b6551..2ff4372c4 100644 --- a/src/muz/transforms/dl_mk_coalesce.cpp +++ b/src/muz/transforms/dl_mk_coalesce.cpp @@ -172,7 +172,7 @@ namespace datalog { } rule_set * mk_coalesce::operator()(rule_set const & source) { - rule_set* rules = alloc(rule_set, m_ctx); + scoped_ptr rules = alloc(rule_set, m_ctx); rules->inherit_predicates(source); rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules(); for (; it != end; ++it) { @@ -181,8 +181,8 @@ namespace datalog { for (unsigned i = 0; i < d_rules.size(); ++i) { rule_ref r1(d_rules[i].get(), rm); for (unsigned j = i + 1; j < d_rules.size(); ++j) { - if (same_body(*r1.get(), *d_rules[j].get())) { - merge_rules(r1, *d_rules[j].get()); + if (same_body(*r1.get(), *d_rules.get(j))) { + merge_rules(r1, *d_rules.get(j)); d_rules[j] = d_rules.back(); d_rules.pop_back(); --j; @@ -191,7 +191,7 @@ namespace datalog { rules->add_rule(r1.get()); } } - return rules; + return rules.detach(); } }; diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 5ad3f67d2..eccbd0921 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -602,17 +602,16 @@ namespace datalog { return nullptr; } - rule_set * res = alloc(rule_set, m_context); + scoped_ptr res = alloc(rule_set, m_context); if (transform_rules(source, *res)) { res->inherit_predicates(source); TRACE("dl", source.display(tout); res->display(tout);); } else { - dealloc(res); res = nullptr; } - return res; + return res.detach(); } }; diff --git a/src/muz/transforms/dl_mk_loop_counter.cpp b/src/muz/transforms/dl_mk_loop_counter.cpp index e0895981f..b22d9fa3b 100644 --- a/src/muz/transforms/dl_mk_loop_counter.cpp +++ b/src/muz/transforms/dl_mk_loop_counter.cpp @@ -68,7 +68,7 @@ namespace datalog { m_old2new.reset(); m_new2old.reset(); rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); @@ -118,7 +118,7 @@ namespace datalog { // model converter: remove references to extra argument. // proof converter: remove references to extra argument as well. - return result; + return result.detach(); } rule_set * mk_loop_counter::revert(rule_set const & source) { diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp index b951cfd28..85c88716c 100644 --- a/src/muz/transforms/dl_mk_magic_sets.cpp +++ b/src/muz/transforms/dl_mk_magic_sets.cpp @@ -345,7 +345,7 @@ namespace datalog { var_idx_set empty_var_idx_set; adorn_literal(goal_head, empty_var_idx_set); - rule_set * result = alloc(rule_set, m_context); + scoped_ptr result = alloc(rule_set, m_context); result->inherit_predicates(source); while (!m_todo.empty()) { @@ -373,7 +373,7 @@ namespace datalog { rule * back_to_goal_rule = m_context.get_rule_manager().mk(goal_head, 1, &adn_goal_head, nullptr); result->add_rule(back_to_goal_rule); - return result; + return result.detach(); } }; diff --git a/src/muz/transforms/dl_mk_magic_symbolic.cpp b/src/muz/transforms/dl_mk_magic_symbolic.cpp index acdf0bff0..ac4efd448 100644 --- a/src/muz/transforms/dl_mk_magic_symbolic.cpp +++ b/src/muz/transforms/dl_mk_magic_symbolic.cpp @@ -72,7 +72,7 @@ namespace datalog { } context& ctx = source.get_context(); rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, ctx); + scoped_ptr result = alloc(rule_set, ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); @@ -109,7 +109,7 @@ namespace datalog { } TRACE("dl", result->display(tout);); - return result; + return result.detach(); } app_ref mk_magic_symbolic::mk_query(app* q) { diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index dacb32d1b..f956ca429 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -329,7 +329,7 @@ namespace datalog { if (m_ctx.get_model_converter()) { m_mc = alloc(qa_model_converter, m); } - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); for (unsigned i = 0; i < sz; ++i) { tail.reset(); @@ -354,7 +354,6 @@ namespace datalog { // proof converter: proofs are not necessarily preserved using this transformation. if (m_old2new.empty()) { - dealloc(result); dealloc(m_mc); result = nullptr; } @@ -363,7 +362,7 @@ namespace datalog { } m_mc = nullptr; - return result; + return result.detach(); } diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 0a183b923..032b4b19c 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -264,7 +264,7 @@ namespace datalog { expr_ref_vector conjs(m); quantifier_ref_vector qs(m); - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); bool instantiated = false; @@ -286,10 +286,9 @@ namespace datalog { result->inherit_predicates(source); } else { - dealloc(result); result = nullptr; } - return result; + return result.detach(); } diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index 95397fa67..84e48d514 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -120,7 +120,7 @@ namespace datalog { return nullptr; } rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); @@ -166,7 +166,7 @@ namespace datalog { } m_trail.reset(); m_cache.reset(); - return result; + return result.detach(); } app_ref mk_scale::mk_pred(unsigned sigma_idx, app* q) { diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index b2f464931..b4b64de24 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -841,11 +841,10 @@ namespace datalog { m_mc = smc.get(); reset(); saturate(src); - rule_set* result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); declare_predicates(src, *result); if (m_predicates.empty()) { // nothing could be sliced. - dealloc(result); return nullptr; } TRACE("dl", display(tout);); @@ -859,7 +858,7 @@ namespace datalog { } m_ctx.add_proof_converter(spc.get()); m_ctx.add_model_converter(smc.get()); - return result; + return result.detach(); } }; diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index 4c5a08eb5..e277a93b4 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -343,11 +343,10 @@ namespace datalog { scan_for_total_rules(source); m_have_new_total_rule = false; - rule_set * res = alloc(rule_set, m_context); + scoped_ptr res = alloc(rule_set, m_context); bool modified = transform_rules(source, *res); if (!m_have_new_total_rule && !modified) { - dealloc(res); return nullptr; } @@ -358,13 +357,12 @@ namespace datalog { while (m_have_new_total_rule) { m_have_new_total_rule = false; - rule_set * old = res; + scoped_ptr old = res; res = alloc(rule_set, m_context); transform_rules(*old, *res); - dealloc(old); } - return res; + return res.detach(); } };