From 6d75c31468d349676a0304f1aff7d420c6b263d3 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 29 Jun 2018 17:04:44 -0400 Subject: [PATCH] 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); } }