From 54b00f357b8cd1277058fc1c6d88c5d7ebf977b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Feb 2018 21:57:54 +0900 Subject: [PATCH] fix rule inlining, add WithParams to pass parameters directly to python API Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 14 +++++++++ src/muz/transforms/dl_mk_rule_inliner.cpp | 38 +++++++---------------- src/muz/transforms/dl_transforms.cpp | 20 ++++++------ 3 files changed, 35 insertions(+), 37 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 641dba59c..d303b477d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7447,6 +7447,20 @@ def With(t, *args, **keys): p = args2params(args, keys, t.ctx) return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx) +def WithParams(t, p): + """Return a tactic that applies tactic `t` using the given configuration options. + + >>> x, y = Ints('x y') + >>> p = ParamsRef() + >>> p.set("som", True) + >>> t = With(Tactic('simplify'), p) + >>> t((x + 1)*(y + 2) == 0) + [[2*x + y + x*y == -2]] + """ + ctx = keys.pop('ctx', None) + t = _to_tactic(t, ctx) + return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx) + def Repeat(t, max=4294967295, ctx=None): """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index a9d2c7090..4088d607c 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -410,15 +410,11 @@ namespace datalog { const rule_stratifier::comp_vector& comps = candidate_inlined_set->get_stratifier().get_strats(); rule_stratifier::comp_vector::const_iterator cend = comps.end(); - for (rule_stratifier::comp_vector::const_iterator it = comps.begin(); it!=cend; ++it) { - rule_stratifier::item_set * stratum = *it; + for (rule_stratifier::item_set * stratum : comps) { SASSERT(stratum->size()==1); func_decl * pred = *stratum->begin(); - - const rule_vector& pred_rules = candidate_inlined_set->get_predicate_rules(pred); - rule_vector::const_iterator iend = pred_rules.end(); - for (rule_vector::const_iterator iit = pred_rules.begin(); iit!=iend; ++iit) { - transform_rule(orig, *iit, m_inlined_rules); + for (rule * r : candidate_inlined_set->get_predicate_rules(pred)) { + transform_rule(orig, r, m_inlined_rules); } } @@ -426,7 +422,7 @@ namespace datalog { for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) { rule* r = m_inlined_rules.get_rule(i); - datalog::del_rule(m_mc, *r, true); + datalog::del_rule(m_mc, *r, false); } } @@ -455,9 +451,7 @@ namespace datalog { func_decl * pred = r->get_decl(i); const rule_vector& pred_rules = m_inlined_rules.get_predicate_rules(pred); - rule_vector::const_iterator iend = pred_rules.end(); - for (rule_vector::const_iterator iit = pred_rules.begin(); iit!=iend; ++iit) { - rule * inl_rule = *iit; + for (rule * inl_rule : pred_rules) { rule_ref inl_result(m_rm); if (try_to_inline_rule(*r.get(), *inl_rule, i, inl_result)) { todo.push_back(inl_result); @@ -475,9 +469,8 @@ namespace datalog { bool something_done = false; - rule_set::iterator rend = orig.end(); - for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) { - rule_ref r(*rit, m_rm); + for (rule* rl : orig) { + rule_ref r(rl, m_rm); func_decl * pred = r->get_decl(); // if inlining is allowed, then we are eliminating @@ -508,15 +501,10 @@ namespace datalog { bool mk_rule_inliner::is_oriented_rewriter(rule * r, rule_stratifier const& strat) { func_decl * head_pred = r->get_decl(); unsigned head_strat = strat.get_predicate_strat(head_pred); - unsigned head_arity = head_pred->get_arity(); - - unsigned pt_len = r->get_positive_tail_size(); - for (unsigned ti=0; tiget_decl(ti); - unsigned pred_strat = strat.get_predicate_strat(pred); SASSERT(pred_strat<=head_strat); @@ -855,13 +843,9 @@ namespace datalog { return nullptr; } - rule_set::iterator end = source.end(); - for (rule_set::iterator it = source.begin(); it != end; ++ it) { - if (has_quantifier(**it)) { - return nullptr; - } - } - + for (rule const* r : source) + if (has_quantifier(*r)) + return nullptr; if (m_context.get_model_converter()) { hsmc = alloc(horn_subsume_model_converter, m); diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp index 95b0f6cd6..d456d95f9 100644 --- a/src/muz/transforms/dl_transforms.cpp +++ b/src/muz/transforms/dl_transforms.cpp @@ -59,7 +59,7 @@ namespace datalog { transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, ctx, 37000)); if (ctx.get_params().datalog_subsumption()) { - transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 35005)); + transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 35005)); } transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 35000)); transf.register_plugin(alloc(datalog::mk_coi_filter, ctx, 34990)); @@ -67,20 +67,20 @@ namespace datalog { //and another round of inlining if (ctx.get_params().datalog_subsumption()) { - transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34975)); + transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34975)); } transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34970)); transf.register_plugin(alloc(datalog::mk_coi_filter, ctx, 34960)); transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, ctx, 34950)); - + if (ctx.get_params().datalog_subsumption()) { - transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34940)); - transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930)); - transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34920)); - transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34910)); - transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34900)); - transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34890)); - transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34880)); + transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34940)); + transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930)); + transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34920)); + transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34910)); + transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34900)); + transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34890)); + transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34880)); } else { transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930));