From 7acea2791da8f23fac4a9a18d97c03a4635818ea Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 29 Jun 2018 08:54:08 -0400 Subject: [PATCH 1/5] -tr:spacer.expand-add --> -tr:spacer_progress --- src/muz/spacer/spacer_context.cpp | 12 ++++++------ src/muz/spacer/spacer_pdr.cpp | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 07dc1a372..2ca8a8f55 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -948,7 +948,7 @@ void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only) << " " << head ()->get_name () << " " << mk_pp (l, m) << "\n";); - STRACE ("spacer.expand-add", + STRACE ("spacer_progress", tout << "** add-lemma: " << pp_level (lvl) << " " << head ()->get_name () << " " << mk_epp (l, m) << "\n"; @@ -1300,7 +1300,7 @@ bool pred_transformer::is_qblocked (pob &n) { // solver->get_itp_core(core); // expr_ref c(m); // c = mk_and(core); - // STRACE("spacer.expand-add", tout << "core: " << mk_epp(c,m) << "\n";); + // STRACE("spacer_progress", tout << "core: " << mk_epp(c,m) << "\n";); // } return res == l_false; } @@ -3059,7 +3059,7 @@ lbool context::solve_core (unsigned from_lvl) m_stats.m_max_depth = std::max(m_stats.m_max_depth, lvl); IF_VERBOSE(1,verbose_stream() << "Entering level "<< lvl << "\n";); - STRACE("spacer.expand-add", tout << "\n* LEVEL " << lvl << "\n";); + STRACE("spacer_progress", tout << "\n* LEVEL " << lvl << "\n";); IF_VERBOSE(1, if (m_params.print_statistics ()) { @@ -3310,7 +3310,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) << " fvsz: " << n.get_free_vars_size() << "\n" << mk_pp(n.post(), m) << "\n";); - STRACE ("spacer.expand-add", + STRACE ("spacer_progress", tout << "** expand-pob: " << n.pt().head()->get_name() << " level: " << n.level() << " depth: " << (n.depth () - m_pob_queue.min_depth ()) << "\n" @@ -3356,7 +3356,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) } if (/* XXX noop */ n.pt().is_qblocked(n)) { - STRACE("spacer.expand-add", + STRACE("spacer_progress", tout << "This pob can be blocked by instantiation\n";); } @@ -3551,7 +3551,7 @@ bool context::propagate(unsigned min_prop_lvl, if (m_simplify_formulas_pre) { simplify_formulas(); } - STRACE ("spacer.expand-add", tout << "Propagating\n";); + STRACE ("spacer_progress", tout << "Propagating\n";); IF_VERBOSE (1, verbose_stream () << "Propagating: " << std::flush;); diff --git a/src/muz/spacer/spacer_pdr.cpp b/src/muz/spacer/spacer_pdr.cpp index 4e6b37a0a..04b001151 100644 --- a/src/muz/spacer/spacer_pdr.cpp +++ b/src/muz/spacer/spacer_pdr.cpp @@ -236,7 +236,7 @@ lbool context::gpdr_solve_core() { for (lvl = 0; lvl < max_level; ++lvl) { checkpoint(); IF_VERBOSE(1,verbose_stream() << "GPDR Entering level "<< lvl << "\n";); - STRACE("spacer.expand-add", tout << "\n* LEVEL " << lvl << "\n";); + STRACE("spacer_progress", tout << "\n* LEVEL " << lvl << "\n";); m_expanded_lvl = infty_level(); m_stats.m_max_query_lvl = lvl; if (gpdr_check_reachability(lvl, ms)) {return l_true;} From 6d75c31468d349676a0304f1aff7d420c6b263d3 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 29 Jun 2018 17:04:44 -0400 Subject: [PATCH 2/5] First draft of elim_term_ite xform. Not working. --- src/muz/base/dl_context.cpp | 1 + src/muz/base/dl_context.h | 1 + src/muz/base/fp_params.pyg | 3 +- src/muz/spacer/spacer_context.cpp | 7 +- src/muz/spacer/spacer_context.h | 4 +- src/muz/transforms/CMakeLists.txt | 2 + src/muz/transforms/dl_mk_elim_term_ite.cpp | 117 +++++++++++++++++++++ src/muz/transforms/dl_mk_elim_term_ite.h | 38 +++++++ src/muz/transforms/dl_transforms.cpp | 3 + 9 files changed, 171 insertions(+), 5 deletions(-) create mode 100644 src/muz/transforms/dl_mk_elim_term_ite.cpp create mode 100644 src/muz/transforms/dl_mk_elim_term_ite.h diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index d851ec586..626f116ca 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -307,6 +307,7 @@ namespace datalog { bool context::instantiate_quantifiers() const { return m_params->xform_instantiate_quantifiers(); } 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();} 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 6e6bc80dc..305123052 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -280,6 +280,7 @@ namespace datalog { bool xform_coi() const; bool array_blast() const; bool array_blast_full() const; + bool elim_term_ite() 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 981b99de7..8650ac35e 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -132,10 +132,11 @@ 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"), ('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"), - ('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"), + ('spacer.blast_term_ite_inflation', UINT, 3, 'Maximum inflation for non-Boolean ite-terms expansion: 0 (none), k (multiplicative)'), ('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"), ('bmc.linear_unrolling_depth', UINT, UINT_MAX, "Maximal level to explore"), ('spacer.iuc.split_farkas_literals', BOOL, False, "Split Farkas literals"), diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 2ca8a8f55..693812a31 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1683,7 +1683,10 @@ void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule) // rewrite and simplify th_rewriter rw(m); rw(trans); - if (ctx.blast_term_ite()) {blast_term_ite(trans, 3); rw(trans);} + if (ctx.blast_term_ite_inflation() > 0) { + blast_term_ite(trans, ctx.blast_term_ite_inflation()); + rw(trans); + } TRACE("spacer_init_rule", tout << mk_pp(trans, m) << "\n";); // allow quantifiers in init rule @@ -2265,7 +2268,7 @@ void context::updt_params() { m_use_euf_gen = m_params.spacer_use_euf_gen(); m_use_ctp = m_params.spacer_ctp(); m_use_inc_clause = m_params.spacer_use_inc_clause(); - m_blast_term_ite = m_params.spacer_blast_term_ite(); + m_blast_term_ite_inflation = m_params.spacer_blast_term_ite_inflation(); m_use_ind_gen = m_params.spacer_use_inductive_generalizer(); m_use_array_eq_gen = m_params.spacer_use_array_eq_generalizer(); m_validate_lemmas = m_params.spacer_validate_lemmas(); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 36f898ed1..48c27f96d 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -940,7 +940,6 @@ class context { bool m_use_euf_gen; bool m_use_ctp; bool m_use_inc_clause; - bool m_blast_term_ite; bool m_use_ind_gen; bool m_use_array_eq_gen; bool m_validate_lemmas; @@ -962,6 +961,7 @@ class context { unsigned m_push_pob_max_depth; unsigned m_max_level; unsigned m_restart_initial_threshold; + unsigned m_blast_term_ite_inflation; scoped_ptr_vector m_callbacks; json_marshaller m_json_marshaller; @@ -1036,7 +1036,7 @@ public: bool simplify_pob() {return m_simplify_pob;} bool use_ctp() {return m_use_ctp;} bool use_inc_clause() {return m_use_inc_clause;} - bool blast_term_ite() {return m_blast_term_ite;} + unsigned blast_term_ite_inflation() {return m_blast_term_ite_inflation;} bool elim_aux() {return m_elim_aux;} bool reach_dnf() {return m_reach_dnf;} diff --git a/src/muz/transforms/CMakeLists.txt b/src/muz/transforms/CMakeLists.txt index 5e8829d42..e92aa1c2f 100644 --- a/src/muz/transforms/CMakeLists.txt +++ b/src/muz/transforms/CMakeLists.txt @@ -1,3 +1,4 @@ + z3_add_component(transforms SOURCES dl_mk_array_blast.cpp @@ -23,6 +24,7 @@ z3_add_component(transforms dl_transforms.cpp dl_mk_array_eq_rewrite.cpp dl_mk_array_instantiation.cpp + dl_mk_elim_term_ite.cpp COMPONENT_DEPENDENCIES dataflow hilbert diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp new file mode 100644 index 000000000..3b745445f --- /dev/null +++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp @@ -0,0 +1,117 @@ +/*++ +Copyright (c) 2018 Arie Gurfinkel + +Module Name: + + dl_mk_elim_term_ite.h + +Abstract: + + Remove term-ite expressions from the rules + +Author: + + Arie Gurfinkel (agurfinkel) + +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 "tactic/tactic.h" +#include "tactic/core/elim_term_ite_tactic.h" + +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()) {} + + mk_elim_term_ite::~mk_elim_term_ite() {} + + bool mk_elim_term_ite::elim(rule &r, rule_set &new_rules){ + 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); + + // 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) { + new_rules.add_rule(&r); + return false; + } + new_conjs.reset(); + + // elim ite + tactic_ref elim_term_ite = mk_elim_term_ite_tactic(m); + goal_ref goal = alloc(class goal, m); + goal_ref_buffer result; + flatten_and(body, new_conjs); + for (auto *e : new_conjs) { + goal->assert_expr(e); + } + unsigned sz = goal->num_exprs(); + (*elim_term_ite)(goal, result); + if (result.size() == 1) { + goal_ref new_goal = result[0]; + if (new_goal->num_exprs() != sz) { + new_conjs.reset(); + new_goal->get_formulas(new_conjs); + } + } + + + expr_ref_vector conjs(m); + for (unsigned i = 0; i < utsz; ++i) + conjs.push_back(r.get_tail(i)); + conjs.append(new_conjs); + + body = mk_and(conjs); + head = r.get_head(); + + fml2 = m.mk_implies(body, head); + proof_ref p(m); + rm.mk_rule(fml2, p, new_rules, r.name()); + + return true; + } + + + + rule_set * mk_elim_term_ite::operator()(rule_set const & source) { + if (!m_ctx.elim_term_ite ()) {return nullptr;} + + rule_set* rules = alloc(rule_set, m_ctx); + rules->inherit_predicates(source); + bool change = false; + for (auto *rule : source) { + if (m_ctx.canceled()) { + change = false; + break; + } + change |= elim(*rule, *rules); + } + if (!change) { + dealloc(rules); + rules = nullptr; + } + return rules; + } + + +} diff --git a/src/muz/transforms/dl_mk_elim_term_ite.h b/src/muz/transforms/dl_mk_elim_term_ite.h new file mode 100644 index 000000000..3d811b93c --- /dev/null +++ b/src/muz/transforms/dl_mk_elim_term_ite.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2018 Arie Gurfinkel + +Module Name: + + dl_mk_elim_term_ite.h + +Abstract: + + Remove term-ite expressions from the rules + +Author: + + Arie Gurfinkel (agurfinkel) + +Revision History: + +--*/ +#pragma once + +#include "muz/base/dl_context.h" +#include "muz/base/dl_rule_set.h" +#include "muz/base/dl_rule_transformer.h" +#include "tactic/equiv_proof_converter.h" + +namespace datalog { + class mk_elim_term_ite : public rule_transformer::plugin { + context &m_ctx; + ast_manager &m; + rule_manager &rm; + + bool elim(rule &r, rule_set &new_rules); + public: + mk_elim_term_ite(context &ctx, unsigned priority); + ~mk_elim_term_ite() override; + rule_set * operator()(const rule_set &source) override; + }; +} diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp index d4b9506e8..7234f0bad 100644 --- a/src/muz/transforms/dl_transforms.cpp +++ b/src/muz/transforms/dl_transforms.cpp @@ -35,6 +35,7 @@ Revision History: #include "muz/transforms/dl_mk_scale.h" #include "muz/transforms/dl_mk_array_eq_rewrite.h" #include "muz/transforms/dl_mk_array_instantiation.h" +#include "muz/transforms/dl_mk_elim_term_ite.h" #include "muz/base/fp_params.hpp" namespace datalog { @@ -95,6 +96,8 @@ namespace datalog { if (ctx.get_params().xform_magic()) { transf.register_plugin(alloc(datalog::mk_magic_symbolic, ctx, 36020)); } + + transf.register_plugin(alloc(datalog::mk_elim_term_ite, ctx, 34999)); ctx.transform_rules(transf); } } From 5d1149adb2c5781605b7613a9312311c1357bc20 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 30 Jun 2018 14:33:04 -0400 Subject: [PATCH 3/5] Transformation to eliminate term-ite expressions from DL rules --- src/muz/base/dl_context.cpp | 3 + src/muz/base/dl_context.h | 1 + src/muz/base/fp_params.pyg | 3 +- src/muz/transforms/dl_mk_elim_term_ite.cpp | 108 ++++++++++++++++++--- src/muz/transforms/dl_mk_elim_term_ite.h | 3 + src/muz/transforms/dl_transforms.cpp | 2 +- 6 files changed, 107 insertions(+), 13 deletions(-) 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); } } From 8502f1fe36aba6ca81fba77090f9f4baf13228e2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 2 Jul 2018 21:37:30 -0400 Subject: [PATCH 4/5] Fix in proof_util:elim_aux_assertions Replace assertions/hypotheses of aux variables with PR_TRUE. Rebuild unit resolution as needed. This makes the transformation stable against new proof rules. --- src/ast/proofs/proof_utils.h | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h index 729a30eb0..1fd6eb449 100644 --- a/src/ast/proofs/proof_utils.h +++ b/src/ast/proofs/proof_utils.h @@ -164,10 +164,12 @@ public: // skip (asserted m_aux) else if (m.is_asserted(arg, a) && a == m_aux.get()) { dirty = true; + args.push_back(m.mk_true_proof()); } // skip (hypothesis m_aux) else if (m.is_hypothesis(arg, a) && a == m_aux.get()) { dirty = true; + args.push_back(m.mk_true_proof()); } else if (is_app(arg) && cache.find(to_app(arg), r)) { dirty |= (arg != r); args.push_back(r); @@ -188,13 +190,18 @@ public: app_ref newp(m); if (!dirty) { newp = p; } else if (m.is_unit_resolution(p)) { - if (args.size() == 2) - // unit resolution with m_aux that got collapsed to nothing - { newp = to_app(args.get(0)); } + ptr_buffer parents; + for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i) { + app *arg = to_app(args.get(i)); + if (!m.is_true(m.get_fact(arg))) + parents.push_back(arg); + } + // unit resolution that collapsed to nothing + if (parents.size() == 1) { + newp = parents.get(0); + } else { - ptr_vector parents; - for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i) - { parents.push_back(to_app(args.get(i))); } + // rebuild unit resolution SASSERT(parents.size() == args.size() - 1); newp = m.mk_unit_resolution(parents.size(), parents.c_ptr()); // XXX the old and new facts should be @@ -203,9 +210,11 @@ public: SASSERT(m.get_fact(newp) == args.back()); pinned.push_back(newp); } - } else if (matches_fact(args, a)) { + } + else if (matches_fact(args, a)) { newp = to_app(a); - } else { + } + else { expr_ref papp(m); mk_app(p->get_decl(), args, papp); newp = to_app(papp.get()); From 27fc564d09f8576600401d5931beb37740ea9def Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 2 Jul 2018 23:23:58 -0400 Subject: [PATCH 5/5] Remove bad assertion --- src/ast/proofs/proof_utils.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h index 1fd6eb449..e3ad8d06e 100644 --- a/src/ast/proofs/proof_utils.h +++ b/src/ast/proofs/proof_utils.h @@ -202,7 +202,6 @@ public: } else { // rebuild unit resolution - SASSERT(parents.size() == args.size() - 1); newp = m.mk_unit_resolution(parents.size(), parents.c_ptr()); // XXX the old and new facts should be // equivalent. The test here is much