mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/z3prover/z3 into lev
This commit is contained in:
commit
6981918c33
|
@ -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,14 +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<proof> 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<proof> parents;
|
||||
for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i)
|
||||
{ parents.push_back(to_app(args.get(i))); }
|
||||
SASSERT(parents.size() == args.size() - 1);
|
||||
// rebuild unit resolution
|
||||
newp = m.mk_unit_resolution(parents.size(), parents.c_ptr());
|
||||
// XXX the old and new facts should be
|
||||
// equivalent. The test here is much
|
||||
|
@ -203,9 +209,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());
|
||||
|
|
|
@ -307,6 +307,10 @@ 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();}
|
||||
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) {
|
||||
|
|
|
@ -280,6 +280,8 @@ namespace datalog {
|
|||
bool xform_coi() const;
|
||||
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);
|
||||
|
||||
|
|
|
@ -132,10 +132,12 @@ 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.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"),
|
||||
('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"),
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
@ -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();
|
||||
|
@ -3059,7 +3062,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 +3313,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 +3359,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 +3554,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;);
|
||||
|
||||
|
|
|
@ -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;}
|
||||
|
||||
|
|
|
@ -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;}
|
||||
|
|
|
@ -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
|
||||
|
|
203
src/muz/transforms/dl_mk_elim_term_ite.cpp
Normal file
203
src/muz/transforms/dl_mk_elim_term_ite.cpp
Normal file
|
@ -0,0 +1,203 @@
|
|||
/*++
|
||||
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 "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()),
|
||||
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);
|
||||
|
||||
|
||||
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), body(m), head(m);
|
||||
|
||||
// blast ite
|
||||
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);
|
||||
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);
|
||||
flatten_and(new_conjs);
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref_vector conjs(m);
|
||||
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;
|
||||
}
|
||||
|
||||
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
|
||||
}
|
41
src/muz/transforms/dl_mk_elim_term_ite.h
Normal file
41
src/muz/transforms/dl_mk_elim_term_ite.h
Normal file
|
@ -0,0 +1,41 @@
|
|||
/*++
|
||||
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;
|
||||
|
||||
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;
|
||||
rule_set * operator()(const rule_set &source) override;
|
||||
};
|
||||
}
|
|
@ -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, 35010));
|
||||
ctx.transform_rules(transf);
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue