3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

First draft of elim_term_ite xform. Not working.

This commit is contained in:
Arie Gurfinkel 2018-06-29 17:04:44 -04:00
parent 7acea2791d
commit 6d75c31468
9 changed files with 171 additions and 5 deletions

View file

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

View file

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

View file

@ -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"),

View file

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

View file

@ -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<spacer_callback> 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;}

View file

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

View file

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

View file

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

View file

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