mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
1d9e0feb84
|
@ -479,15 +479,15 @@ bool compare_nodes(ast const * n1, ast const * n2) {
|
|||
return
|
||||
q1->get_kind() == q2->get_kind() &&
|
||||
q1->get_num_decls() == q2->get_num_decls() &&
|
||||
q1->get_expr() == q2->get_expr() &&
|
||||
q1->get_weight() == q2->get_weight() &&
|
||||
q1->get_num_patterns() == q2->get_num_patterns() &&
|
||||
compare_arrays(q1->get_decl_sorts(),
|
||||
q2->get_decl_sorts(),
|
||||
q1->get_num_decls()) &&
|
||||
compare_arrays(q1->get_decl_names(),
|
||||
q2->get_decl_names(),
|
||||
q1->get_num_decls()) &&
|
||||
q1->get_expr() == q2->get_expr() &&
|
||||
q1->get_weight() == q2->get_weight() &&
|
||||
q1->get_num_patterns() == q2->get_num_patterns() &&
|
||||
((q1->get_qid().is_numerical() && q2->get_qid().is_numerical()) ||
|
||||
(q1->get_qid() == q2->get_qid())) &&
|
||||
compare_arrays(q1->get_patterns(),
|
||||
|
@ -542,22 +542,6 @@ inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_v
|
|||
} }
|
||||
}
|
||||
|
||||
unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init) {
|
||||
return ast_array_hash<ast>(ns, sz, init);
|
||||
}
|
||||
unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init) {
|
||||
return ast_array_hash<app>(ns, sz, init);
|
||||
}
|
||||
unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init) {
|
||||
return ast_array_hash<expr>(ns, sz, init);
|
||||
}
|
||||
unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init) {
|
||||
return ast_array_hash<sort>(ns, sz, init);
|
||||
}
|
||||
unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init) {
|
||||
return ast_array_hash<func_decl>(ns, sz, init);
|
||||
}
|
||||
|
||||
unsigned get_node_hash(ast const * n) {
|
||||
unsigned a, b, c;
|
||||
|
||||
|
|
|
@ -970,11 +970,6 @@ inline quantifier const * to_quantifier(ast const * n) { SASSERT(is_quantifier(n
|
|||
unsigned get_node_hash(ast const * n);
|
||||
bool compare_nodes(ast const * n1, ast const * n2);
|
||||
unsigned get_node_size(ast const * n);
|
||||
unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init);
|
||||
unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init);
|
||||
unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init);
|
||||
unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init);
|
||||
unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init);
|
||||
|
||||
// This is the internal comparison functor for hash-consing AST nodes.
|
||||
struct ast_eq_proc {
|
||||
|
|
|
@ -278,7 +278,6 @@ struct mbp_array_tg::impl {
|
|||
m_tg.get_terms(terms, false);
|
||||
for (unsigned i = 0; i < terms.size(); i++) {
|
||||
term = terms.get(i);
|
||||
SASSERT(!m.is_distinct(term));
|
||||
if (m_seen.is_marked(term)) continue;
|
||||
if (m_tg.is_cgr(term)) continue;
|
||||
TRACE("mbp_tg", tout << "processing " << expr_ref(term, m););
|
||||
|
|
|
@ -43,32 +43,106 @@ struct mbp_basic_tg::impl {
|
|||
void mark_seen(expr *t) { m_seen.mark(t); }
|
||||
bool is_seen(expr *t) { return m_seen.is_marked(t); }
|
||||
|
||||
//Split on all ite terms, irrespective of whether
|
||||
//they contain variables/are c-ground
|
||||
// Split on all ite terms, irrespective of whether
|
||||
// they contain variables/are c-ground
|
||||
bool apply() {
|
||||
if (!m_use_mdl) return false;
|
||||
std::function<bool(expr *)> should_split, is_true, is_false;
|
||||
if (!m_use_mdl) {
|
||||
should_split = [&](expr *t) { return m_tg.has_val_in_class(t); };
|
||||
is_true = [&](expr *t) {
|
||||
return m_tg.has_val_in_class(t) && m_mdl.is_true(t);
|
||||
};
|
||||
is_false = [&](expr *t) {
|
||||
return m_tg.has_val_in_class(t) && m_mdl.is_false(t);
|
||||
};
|
||||
} else {
|
||||
should_split = [](expr *t) { return true; };
|
||||
is_true = [&](expr *t) { return m_mdl.is_true(t); };
|
||||
is_false = [&](expr *t) { return m_mdl.is_false(t); };
|
||||
}
|
||||
|
||||
expr *c, *th, *el;
|
||||
expr_ref nterm(m);
|
||||
bool progress = false;
|
||||
TRACE("mbp_tg", tout << "Iterating over terms of tg";);
|
||||
// Not resetting terms because get_terms calls resize on terms
|
||||
m_tg.get_terms(terms, false);
|
||||
for (expr* term : terms) {
|
||||
if (is_seen(term))
|
||||
continue;
|
||||
if (m.is_ite(term, c, th, el)) {
|
||||
for (expr *term : terms) {
|
||||
if (is_seen(term)) continue;
|
||||
if (m.is_ite(term, c, th, el) && should_split(c)) {
|
||||
mark_seen(term);
|
||||
progress = true;
|
||||
if (m_mdl.is_true(c)) {
|
||||
m_tg.add_lit(c);
|
||||
m_tg.add_eq(term, th);
|
||||
}
|
||||
else {
|
||||
} else {
|
||||
nterm = mk_not(m, c);
|
||||
m_tg.add_lit(nterm);
|
||||
m_tg.add_eq(term, el);
|
||||
}
|
||||
}
|
||||
if (m.is_implies(term, c, th)) {
|
||||
if (is_true(th) || is_false(c)) {
|
||||
mark_seen(term);
|
||||
progress = true;
|
||||
if (is_true(th))
|
||||
m_tg.add_lit(th);
|
||||
else if (is_false(c))
|
||||
m_tg.add_lit(c);
|
||||
m_tg.add_eq(term, m.mk_true());
|
||||
} else if (is_true(c) && is_false(th)) {
|
||||
mark_seen(term);
|
||||
progress = true;
|
||||
m_tg.add_eq(term, m.mk_false());
|
||||
}
|
||||
}
|
||||
if (m.is_or(term) || m.is_and(term)) {
|
||||
bool is_or = m.is_or(term);
|
||||
app *c = to_app(term);
|
||||
bool t = is_or ? any_of(*c, is_true) : all_of(*c, is_true);
|
||||
bool f = is_or ? all_of(*c, is_false) : all_of(*c, is_false);
|
||||
if (t || f) {
|
||||
mark_seen(term);
|
||||
progress = true;
|
||||
m_tg.add_eq(term, t ? m.mk_true() : m.mk_false());
|
||||
if (f) {
|
||||
for (auto a : *c) {
|
||||
if (is_false(a)) {
|
||||
m_tg.add_lit(mk_not(m, a));
|
||||
if (!is_or) break;
|
||||
}
|
||||
}
|
||||
} else {
|
||||
for (auto a : *c) {
|
||||
if (is_true(a)) {
|
||||
m_tg.add_lit(a);
|
||||
if (is_or) break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
if (m_use_mdl && m.is_distinct(term)) {
|
||||
mark_seen(term);
|
||||
progress = true;
|
||||
bool eq = false;
|
||||
app *c = to_app(term);
|
||||
for (auto a1 : *c) {
|
||||
for (auto a2 : *c) {
|
||||
if (a1 == a2) continue;
|
||||
if (m_mdl.are_equal(a1, a2)) {
|
||||
m_tg.add_eq(a1, a2);
|
||||
eq = true;
|
||||
break;
|
||||
} else
|
||||
m_tg.add_deq(a1, a2);
|
||||
}
|
||||
}
|
||||
if (eq)
|
||||
m_tg.add_eq(term, m.mk_false());
|
||||
else
|
||||
m_tg.add_eq(term, m.mk_true());
|
||||
}
|
||||
}
|
||||
return progress;
|
||||
}
|
||||
|
|
|
@ -158,7 +158,6 @@ struct mbp_dt_tg::impl {
|
|||
m_tg.get_terms(terms, false);
|
||||
for (unsigned i = 0; i < terms.size(); i++) {
|
||||
term = terms.get(i);
|
||||
SASSERT(!m.is_distinct(term));
|
||||
if (is_seen(term)) continue;
|
||||
if (m_tg.is_cgr(term)) continue;
|
||||
if (is_app(term) &&
|
||||
|
|
|
@ -178,7 +178,7 @@ class mbp_qel::impl {
|
|||
|
||||
std::function<bool(expr *)> non_core = [&](expr *e) {
|
||||
if (is_app(e) && is_partial_eq(to_app(e))) return true;
|
||||
if (m.is_ite(e)) return true;
|
||||
if (m.is_ite(e) || m.is_or(e) || m.is_implies(e) || m.is_and(e) || m.is_distinct(e)) return true;
|
||||
return red_vars.is_marked(e);
|
||||
};
|
||||
|
||||
|
|
|
@ -67,6 +67,8 @@ namespace smt {
|
|||
m_ge(ge) {
|
||||
}
|
||||
|
||||
~arith_eq_relevancy_eh() override {}
|
||||
|
||||
void operator()(relevancy_propagator & rp) override {
|
||||
if (!rp.is_relevant(m_n1))
|
||||
return;
|
||||
|
|
|
@ -3565,7 +3565,6 @@ namespace smt {
|
|||
try {
|
||||
internalize_assertions();
|
||||
} catch (cancel_exception&) {
|
||||
VERIFY(resource_limits_exceeded());
|
||||
return l_undef;
|
||||
}
|
||||
expr_ref_vector theory_assumptions(m);
|
||||
|
@ -3637,7 +3636,6 @@ namespace smt {
|
|||
TRACE("unsat_core_bug", tout << asms << '\n';);
|
||||
init_assumptions(asms);
|
||||
} catch (cancel_exception&) {
|
||||
VERIFY(resource_limits_exceeded());
|
||||
return l_undef;
|
||||
}
|
||||
TRACE("before_search", display(tout););
|
||||
|
@ -3664,7 +3662,6 @@ namespace smt {
|
|||
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
|
||||
init_assumptions(asms);
|
||||
} catch (cancel_exception&) {
|
||||
VERIFY(resource_limits_exceeded());
|
||||
return l_undef;
|
||||
}
|
||||
for (auto const& clause : clauses) init_clause(clause);
|
||||
|
|
|
@ -123,7 +123,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
struct relevancy_propagator_imp : public relevancy_propagator {
|
||||
unsigned m_qhead;
|
||||
unsigned m_qhead = 0;
|
||||
expr_ref_vector m_relevant_exprs;
|
||||
uint_set m_is_relevant;
|
||||
typedef list<relevancy_eh *> relevancy_ehs;
|
||||
|
@ -144,14 +144,18 @@ namespace smt {
|
|||
unsigned m_trail_lim;
|
||||
};
|
||||
svector<scope> m_scopes;
|
||||
bool m_propagating;
|
||||
bool m_propagating = false;
|
||||
|
||||
relevancy_propagator_imp(context & ctx):
|
||||
relevancy_propagator(ctx), m_qhead(0), m_relevant_exprs(ctx.get_manager()),
|
||||
m_propagating(false) {}
|
||||
relevancy_propagator(ctx), m_relevant_exprs(ctx.get_manager()) {}
|
||||
|
||||
~relevancy_propagator_imp() override {
|
||||
undo_trail(0);
|
||||
ast_manager & m = get_manager();
|
||||
unsigned i = m_trail.size();
|
||||
while (i != 0) {
|
||||
--i;
|
||||
m.dec_ref(m_trail[i].get_node());
|
||||
}
|
||||
}
|
||||
|
||||
relevancy_ehs * get_handlers(expr * n) {
|
||||
|
|
|
@ -41,13 +41,14 @@ namespace smt {
|
|||
/**
|
||||
\brief Fallback for the two previous methods.
|
||||
*/
|
||||
virtual void operator()(relevancy_propagator & rp) {}
|
||||
virtual void operator()(relevancy_propagator & rp) = 0;
|
||||
};
|
||||
|
||||
class simple_relevancy_eh : public relevancy_eh {
|
||||
expr * m_target;
|
||||
public:
|
||||
simple_relevancy_eh(expr * t):m_target(t) {}
|
||||
~simple_relevancy_eh() override {}
|
||||
void operator()(relevancy_propagator & rp) override;
|
||||
};
|
||||
|
||||
|
@ -60,6 +61,7 @@ namespace smt {
|
|||
expr * m_target;
|
||||
public:
|
||||
pair_relevancy_eh(expr * s1, expr * s2, expr * t):m_source1(s1), m_source2(s2), m_target(t) {}
|
||||
~pair_relevancy_eh() override {}
|
||||
void operator()(relevancy_propagator & rp) override;
|
||||
};
|
||||
|
||||
|
|
|
@ -546,7 +546,7 @@ namespace smt {
|
|||
|
||||
expr_ref def2(m.mk_app(f, args2.size(), args2.data()), m);
|
||||
ctx.get_rewriter()(def2);
|
||||
expr* def1 = mk_default(map);
|
||||
expr_ref def1(mk_default(map), m);
|
||||
ctx.internalize(def1, false);
|
||||
ctx.internalize(def2, false);
|
||||
return try_assign_eq(def1, def2);
|
||||
|
@ -561,7 +561,7 @@ namespace smt {
|
|||
SASSERT(is_const(cnst));
|
||||
TRACE("array", tout << mk_bounded_pp(cnst->get_expr(), m) << "\n";);
|
||||
expr* val = cnst->get_arg(0)->get_expr();
|
||||
expr* def = mk_default(cnst->get_expr());
|
||||
expr_ref def(mk_default(cnst->get_expr()), m);
|
||||
ctx.internalize(def, false);
|
||||
return try_assign_eq(val, def);
|
||||
}
|
||||
|
@ -598,7 +598,7 @@ namespace smt {
|
|||
return false;
|
||||
m_stats.m_num_default_lambda_axiom++;
|
||||
expr* e = arr->get_expr();
|
||||
expr* def = mk_default(e);
|
||||
expr_ref def(mk_default(e), m);
|
||||
quantifier* lam = m.is_lambda_def(arr->get_decl());
|
||||
TRACE("array", tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n");
|
||||
expr_ref_vector args(m);
|
||||
|
|
Loading…
Reference in a new issue