mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix rule inlining, add WithParams to pass parameters directly to python API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-21 21:57:54 +09:00
parent a2f907c7d1
commit 54b00f357b
3 changed files with 35 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/api/python/z3/z3.py
View file

@ -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.

38
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -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; ti<pt_len; ++ti) {
for (unsigned ti=0; ti < pt_len; ++ti) {
func_decl * pred = r->get_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);

20
src/muz/transforms/dl_transforms.cpp
View file

@ -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));