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 HEAD
This commit is contained in:
commit
8c68aed69e
|
@ -30,7 +30,7 @@ namespace datalog {
|
|||
ast_manager & m;
|
||||
context & m_context;
|
||||
public:
|
||||
mk_partial_equivalence_transformer(context & ctx, unsigned priority=45000)
|
||||
mk_partial_equivalence_transformer(context & ctx, unsigned priority=30000)
|
||||
: plugin(priority),
|
||||
m(ctx.get_manager()),
|
||||
m_context(ctx) {}
|
||||
|
|
|
@ -307,8 +307,8 @@ namespace datalog {
|
|||
if (m_context.similarity_compressor()) {
|
||||
transf.register_plugin(alloc(mk_similarity_compressor, m_context));
|
||||
}
|
||||
transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
|
||||
transf.register_plugin(alloc(mk_rule_inliner, m_context));
|
||||
transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
|
||||
transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
|
||||
transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
|
||||
|
||||
|
|
|
@ -596,7 +596,7 @@ namespace qe {
|
|||
p = m_pols.back();
|
||||
if (!m_is_relevant(e)) {
|
||||
pop();
|
||||
insert(e, p, p?e:m.mk_not(e));
|
||||
insert(e, p, p?e:mk_not(m, e));
|
||||
continue;
|
||||
}
|
||||
if (!is_app(e)) {
|
||||
|
@ -634,7 +634,7 @@ namespace qe {
|
|||
}
|
||||
else {
|
||||
pop();
|
||||
insert(e, p, p?e:m.mk_not(e));
|
||||
insert(e, p, p?e:mk_not(m, e));
|
||||
}
|
||||
|
||||
}
|
||||
|
@ -1208,7 +1208,7 @@ namespace qe {
|
|||
}
|
||||
bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), fml);
|
||||
|
||||
fml = m.mk_not(m.mk_iff(q, fml));
|
||||
fml = mk_not(m, m.mk_iff(q, fml));
|
||||
ast_smt_pp pp(m);
|
||||
out << "; eliminate " << mk_pp(m_var, m) << "\n";
|
||||
out << "(push)\n";
|
||||
|
@ -1303,12 +1303,7 @@ namespace qe {
|
|||
}
|
||||
}
|
||||
TRACE("qe_verbose", tout << "No plugin for " << mk_ismt2_pp(e, m) << "\n";);
|
||||
if (p || m.is_not(e, e)) {
|
||||
result = e;
|
||||
}
|
||||
else {
|
||||
result = m.mk_not(e);
|
||||
}
|
||||
result = p?e:mk_not(m, e);
|
||||
}
|
||||
|
||||
void i_solver_context::mk_atom_fn::operator()(expr* e, bool p, expr_ref& result) {
|
||||
|
@ -1436,7 +1431,7 @@ namespace qe {
|
|||
m_fml = f;
|
||||
f = m_subfml;
|
||||
m_solver.assert_expr(f);
|
||||
}
|
||||
}
|
||||
m_root.init(f);
|
||||
TRACE("qe",
|
||||
for (unsigned i = 0; i < num_vars; ++i) tout << mk_ismt2_pp(vars[i], m) << "\n";
|
||||
|
@ -1591,7 +1586,7 @@ namespace qe {
|
|||
}
|
||||
m_literals.reset();
|
||||
while (node) {
|
||||
m_literals.push_back(m.mk_not(node->assignment()));
|
||||
m_literals.push_back(mk_not(m, node->assignment()));
|
||||
node = node->parent();
|
||||
}
|
||||
add_literal(l1);
|
||||
|
@ -1865,7 +1860,7 @@ namespace qe {
|
|||
//
|
||||
app* mk_eq_value(app* b, rational const& vl) {
|
||||
if (m.is_bool(b)) {
|
||||
if (vl.is_zero()) return m.mk_not(b);
|
||||
if (vl.is_zero()) return to_app(mk_not(m, b));
|
||||
if (vl.is_one()) return b;
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
@ -2604,12 +2599,12 @@ namespace qe {
|
|||
TRACE("qe", tout << "variables extracted" << mk_pp(result, m) << "\n";);
|
||||
|
||||
if (old_q->is_forall()) {
|
||||
result = m.mk_not(result);
|
||||
result = mk_not(m, result);
|
||||
}
|
||||
m_ctx.solve(result, vars);
|
||||
if (old_q->is_forall()) {
|
||||
expr* e = 0;
|
||||
result = m.is_not(result, e)?e:m.mk_not(result);
|
||||
result = m.is_not(result, e)?e:mk_not(m, result);
|
||||
}
|
||||
var_shifter shift(m);
|
||||
shift(result, vars.size(), result);
|
||||
|
|
|
@ -155,6 +155,8 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
|
|||
typedef obj_map<expr, interval> map;
|
||||
|
||||
ast_manager& m;
|
||||
params_ref m_params;
|
||||
bool m_propagate_eq;
|
||||
bv_util m_bv;
|
||||
vector<map> m_scopes;
|
||||
map *m_bound;
|
||||
|
@ -209,9 +211,19 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
|
|||
|
||||
public:
|
||||
|
||||
bv_bounds_simplifier(ast_manager& m) : m(m), m_bv(m) {
|
||||
bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) {
|
||||
m_scopes.push_back(map());
|
||||
m_bound = &m_scopes.back();
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
m_propagate_eq = p.get_bool("propagate_eq", false);
|
||||
}
|
||||
|
||||
static void get_param_descrs(param_descrs& r) {
|
||||
r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities");
|
||||
}
|
||||
|
||||
virtual ~bv_bounds_simplifier() {}
|
||||
|
@ -262,7 +274,7 @@ public:
|
|||
result = m.mk_true();
|
||||
} else if (!b.intersect(ctx, intr)) {
|
||||
result = m.mk_false();
|
||||
} else if (intr.l == intr.h) {
|
||||
} else if (m_propagate_eq && intr.l == intr.h) {
|
||||
result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
|
||||
}
|
||||
} else if (b.is_full() && b.tight) {
|
||||
|
@ -291,7 +303,7 @@ public:
|
|||
}
|
||||
|
||||
virtual simplifier * translate(ast_manager & m) {
|
||||
return alloc(bv_bounds_simplifier, m);
|
||||
return alloc(bv_bounds_simplifier, m, m_params);
|
||||
}
|
||||
|
||||
virtual unsigned scope_level() const {
|
||||
|
@ -302,5 +314,5 @@ public:
|
|||
}
|
||||
|
||||
tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) {
|
||||
return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m), p));
|
||||
return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m, p), p));
|
||||
}
|
||||
|
|
|
@ -198,6 +198,7 @@ struct ctx_simplify_tactic::imp {
|
|||
m_max_steps = p.get_uint("max_steps", UINT_MAX);
|
||||
m_max_depth = p.get_uint("max_depth", 1024);
|
||||
m_bail_on_blowup = p.get_bool("bail_on_blowup", false);
|
||||
m_simp->updt_params(p);
|
||||
}
|
||||
|
||||
void checkpoint() {
|
||||
|
@ -373,7 +374,7 @@ struct ctx_simplify_tactic::imp {
|
|||
if (new_arg != arg)
|
||||
modified = true;
|
||||
if (i < num_args - 1 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR))
|
||||
new_arg = m.mk_false();
|
||||
new_arg = OR ? m.mk_true() : m.mk_false();
|
||||
|
||||
if ((OR && m.is_false(new_arg)) ||
|
||||
(!OR && m.is_true(new_arg))) {
|
||||
|
@ -402,7 +403,7 @@ struct ctx_simplify_tactic::imp {
|
|||
if (new_arg != arg)
|
||||
modified = true;
|
||||
if (i > 0 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR))
|
||||
new_arg = m.mk_false();
|
||||
new_arg = OR ? m.mk_true() : m.mk_false();
|
||||
|
||||
if ((OR && m.is_false(new_arg)) ||
|
||||
(!OR && m.is_true(new_arg))) {
|
||||
|
@ -529,6 +530,37 @@ struct ctx_simplify_tactic::imp {
|
|||
return sz;
|
||||
}
|
||||
|
||||
void process_goal(goal & g) {
|
||||
SASSERT(scope_level() == 0);
|
||||
// go forwards
|
||||
unsigned old_lvl = scope_level();
|
||||
unsigned sz = g.size();
|
||||
expr_ref r(m);
|
||||
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
|
||||
m_depth = 0;
|
||||
simplify(g.form(i), r);
|
||||
if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !assert_expr(r, false)) {
|
||||
r = m.mk_false();
|
||||
}
|
||||
g.update(i, r, 0, g.dep(i));
|
||||
}
|
||||
pop(scope_level() - old_lvl);
|
||||
|
||||
// go backwards
|
||||
sz = g.size();
|
||||
for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
|
||||
m_depth = 0;
|
||||
--i;
|
||||
simplify(g.form(i), r);
|
||||
if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !assert_expr(r, false)) {
|
||||
r = m.mk_false();
|
||||
}
|
||||
g.update(i, r, 0, g.dep(i));
|
||||
}
|
||||
pop(scope_level() - old_lvl);
|
||||
SASSERT(scope_level() == 0);
|
||||
}
|
||||
|
||||
void process(expr * s, expr_ref & r) {
|
||||
TRACE("ctx_simplify_tactic", tout << "simplifying:\n" << mk_ismt2_pp(s, m) << "\n";);
|
||||
SASSERT(scope_level() == 0);
|
||||
|
@ -546,24 +578,22 @@ struct ctx_simplify_tactic::imp {
|
|||
|
||||
void operator()(goal & g) {
|
||||
SASSERT(g.is_well_sorted());
|
||||
bool proofs_enabled = g.proofs_enabled();
|
||||
m_occs.reset();
|
||||
m_occs(g);
|
||||
m_num_steps = 0;
|
||||
expr_ref r(m);
|
||||
proof * new_pr = 0;
|
||||
tactic_report report("ctx-simplify", g);
|
||||
unsigned sz = g.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
if (g.inconsistent())
|
||||
return;
|
||||
expr * t = g.form(i);
|
||||
process(t, r);
|
||||
if (proofs_enabled) {
|
||||
proof * pr = g.pr(i);
|
||||
new_pr = m.mk_modus_ponens(pr, m.mk_rewrite_star(t, r, 0, 0)); // TODO :-)
|
||||
if (g.proofs_enabled()) {
|
||||
expr_ref r(m);
|
||||
unsigned sz = g.size();
|
||||
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
|
||||
expr * t = g.form(i);
|
||||
process(t, r);
|
||||
proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(t, r, 0, 0)); // TODO :-)
|
||||
g.update(i, r, new_pr, g.dep(i));
|
||||
}
|
||||
g.update(i, r, new_pr, g.dep(i));
|
||||
}
|
||||
else {
|
||||
process_goal(g);
|
||||
}
|
||||
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-simplify :num-steps " << m_num_steps << ")\n";);
|
||||
SASSERT(g.is_well_sorted());
|
||||
|
@ -593,6 +623,7 @@ void ctx_simplify_tactic::get_param_descrs(param_descrs & r) {
|
|||
insert_max_memory(r);
|
||||
insert_max_steps(r);
|
||||
r.insert("max_depth", CPK_UINT, "(default: 1024) maximum term depth.");
|
||||
r.insert("propagate_eq", CPK_BOOL, "(default: false) enable equality propagation from bounds.");
|
||||
}
|
||||
|
||||
void ctx_simplify_tactic::operator()(goal_ref const & in,
|
||||
|
|
|
@ -34,6 +34,7 @@ public:
|
|||
virtual void pop(unsigned num_scopes) = 0;
|
||||
virtual simplifier * translate(ast_manager & m) = 0;
|
||||
virtual unsigned scope_level() const = 0;
|
||||
virtual void updt_params(params_ref const & p) {}
|
||||
void set_occs(goal_num_occurs& occs) { m_occs = &occs; };
|
||||
bool shared(expr* t) const;
|
||||
};
|
||||
|
|
|
@ -124,7 +124,7 @@ private:
|
|||
|
||||
};
|
||||
|
||||
tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
|
||||
static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
|
||||
params_ref simp2_p = p;
|
||||
simp2_p.set_bool("pull_cheap_ite", true);
|
||||
simp2_p.set_bool("push_ite_bv", false);
|
||||
|
@ -150,11 +150,7 @@ tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
|
|||
);
|
||||
}
|
||||
|
||||
tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p;
|
||||
main_p.set_bool("elim_and", true);
|
||||
main_p.set_bool("blast_distinct", true);
|
||||
|
||||
static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
|
||||
return and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_solve_eqs_tactic(m),
|
||||
|
|
Loading…
Reference in a new issue