diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 626f116ca..1c9abf78c 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -308,6 +308,9 @@ namespace datalog { bool context::array_blast() const { return m_params->xform_array_blast(); } bool context::array_blast_full() const { return m_params->xform_array_blast_full(); } bool context::elim_term_ite() const {return m_params->xform_elim_term_ite();} + unsigned context::blast_term_ite_inflation() const { + return m_params->xform_elim_term_ite_inflation(); + } void context::register_finite_sort(sort * s, sort_kind k) { diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 305123052..23926c3d1 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -281,6 +281,7 @@ namespace datalog { bool array_blast() const; bool array_blast_full() const; bool elim_term_ite() const; + unsigned blast_term_ite_inflation() const; void register_finite_sort(sort * s, sort_kind k); diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index 8650ac35e..ee842d28e 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -132,7 +132,8 @@ def_module_params('fp', ('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'), ('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"), ('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"), - ('xform.elim_term_ite', BOOL, False, "Eliminate term-ite expressions"), + ('xform.elim_term_ite', BOOL, False, 'Eliminate term-ite expressions'), + ('xform.elim_term_ite.inflation', UINT, 3, 'Maximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative)'), ('spacer.propagate', BOOL, True, 'Enable propagate/pushing phase'), ('spacer.max_level', UINT, UINT_MAX, "Maximum level to explore"), ('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"), diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp index 3b745445f..f0d9a8843 100644 --- a/src/muz/transforms/dl_mk_elim_term_ite.cpp +++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp @@ -20,43 +20,117 @@ Revision History: #include "muz/transforms/dl_mk_elim_term_ite.h" #include "tactic/core/blast_term_ite_tactic.h" #include "ast/ast_util.h" +#include "ast/expr_abstract.h" #include "tactic/tactic.h" #include "tactic/core/elim_term_ite_tactic.h" +namespace { + struct uninterp_const_collector { + app_ref_vector &m_consts; + uninterp_const_collector(app_ref_vector &v) : m_consts(v) {} + void operator()(var *v) {} + void operator()(quantifier *n) {} + void operator()(expr *a){} + void operator()(app *a){ + if (is_uninterp_const(a)) {m_consts.push_back(a);}; + } + }; + + void collect_uninterp_consts(expr *e, app_ref_vector &v) { + uninterp_const_collector c(v); + quick_for_each_expr(c, e); + } + + struct term_ite_proc { + class found{}; + ast_manager &m; + term_ite_proc(ast_manager &m) : m(m) {} + void operator()(var *v) {} + void operator()(quantifier *n) {} + void operator()(expr *a){} + void operator()(app *a){ + if (m.is_term_ite(a)) throw found(); + } + }; + + bool has_term_ite(expr *e, ast_manager& m) { + term_ite_proc f(m); + try { + quick_for_each_expr(f, e); + } catch (term_ite_proc::found) { + return true; + } + return false; + } + bool has_term_ite(expr_ref &e) { return has_term_ite(e, e.m());} + +} namespace datalog { mk_elim_term_ite::mk_elim_term_ite(context & ctx, unsigned priority) : rule_transformer::plugin(priority, false), m_ctx(ctx), m(ctx.get_manager()), - rm(ctx.get_rule_manager()) {} + rm(ctx.get_rule_manager()), + m_ground(m) {} mk_elim_term_ite::~mk_elim_term_ite() {} + expr_ref mk_elim_term_ite::ground(expr_ref &e) { + expr_free_vars fv; + fv(e); + if (m_ground.size() < fv.size()) + m_ground.resize(fv.size()); + for (unsigned i = 0, sz = fv.size(); i < sz; ++i) { + if (fv[i] && !m_ground.get(i)) + m_ground[i] = m.mk_fresh_const("c", fv[i]); + } + + var_subst vsub(m, false); + return vsub(e, m_ground.size(), m_ground.c_ptr()); + } + bool mk_elim_term_ite::elim(rule &r, rule_set &new_rules){ + m_ground.reset(); + + th_rewriter rw(m); unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); expr_ref_vector new_conjs(m); expr_ref tmp(m); - bool change = false; for (unsigned i = utsz; i < tsz; ++i) new_conjs.push_back(r.get_tail(i)); flatten_and(new_conjs); - expr_ref fml1(m), fml2(m), old_body(m), body(m), head(m); + expr_ref fml1(m), fml2(m), body(m), head(m); // blast ite - old_body = m.mk_and(new_conjs.size(), new_conjs.c_ptr()); - body = old_body; - blast_term_ite(body, 2); - change = old_body != body; - if (!change) { + body = m.mk_and(new_conjs.size(), new_conjs.c_ptr()); + if (!has_term_ite(body)) { + TRACE("dl_term_ite", tout << "No term-ite, skipping a rule\n";); new_rules.add_rule(&r); return false; } new_conjs.reset(); + blast_term_ite(body, m_ctx.blast_term_ite_inflation()); + // simplify body + rw(body); + if (!has_term_ite(body)) { + head = r.get_head(); + + fml2 = m.mk_implies(body, head); + proof_ref p(m); + rm.mk_rule(fml2, p, new_rules, r.name()); + rm.mk_rule_rewrite_proof(r, *new_rules.last()); + TRACE("dl_term_ite", tout << "No term-ite after blast_term_ite\n";); + return true; + } + + TRACE("dl_term_ite", + tout << "Rule has term-ite after blasting, starting elimination\n";); + body = ground(body); // elim ite tactic_ref elim_term_ite = mk_elim_term_ite_tactic(m); goal_ref goal = alloc(class goal, m); @@ -72,21 +146,33 @@ namespace datalog { if (new_goal->num_exprs() != sz) { new_conjs.reset(); new_goal->get_formulas(new_conjs); + flatten_and(new_conjs); } } - expr_ref_vector conjs(m); - for (unsigned i = 0; i < utsz; ++i) - conjs.push_back(r.get_tail(i)); + for (unsigned i = 0; i < utsz; ++i) { + tmp = r.get_tail(i); + tmp = ground(tmp); + conjs.push_back(tmp); + } conjs.append(new_conjs); body = mk_and(conjs); + rw(body); + head = r.get_head(); + head = ground(head); fml2 = m.mk_implies(body, head); + SASSERT(!has_term_ite(fml2)); + app_ref_vector consts(m); + collect_uninterp_consts(fml2, consts); + fml2 = mk_forall(m, consts.size(), consts.c_ptr(), fml2); proof_ref p(m); rm.mk_rule(fml2, p, new_rules, r.name()); + rm.mk_rule_rewrite_proof(r, *new_rules.last()); + TRACE("dl_term_ite", tout << "New rule: " << fml2 << "\n";); return true; } diff --git a/src/muz/transforms/dl_mk_elim_term_ite.h b/src/muz/transforms/dl_mk_elim_term_ite.h index 3d811b93c..231697a0b 100644 --- a/src/muz/transforms/dl_mk_elim_term_ite.h +++ b/src/muz/transforms/dl_mk_elim_term_ite.h @@ -29,7 +29,10 @@ namespace datalog { ast_manager &m; rule_manager &rm; + expr_ref_vector m_ground; + bool elim(rule &r, rule_set &new_rules); + expr_ref ground(expr_ref &e); public: mk_elim_term_ite(context &ctx, unsigned priority); ~mk_elim_term_ite() override; diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp index 7234f0bad..3ce2e6ee4 100644 --- a/src/muz/transforms/dl_transforms.cpp +++ b/src/muz/transforms/dl_transforms.cpp @@ -97,7 +97,7 @@ namespace datalog { transf.register_plugin(alloc(datalog::mk_magic_symbolic, ctx, 36020)); } - transf.register_plugin(alloc(datalog::mk_elim_term_ite, ctx, 34999)); + transf.register_plugin(alloc(datalog::mk_elim_term_ite, ctx, 35010)); ctx.transform_rules(transf); } }