mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
wip - fixes to implied-eq proof hints
This commit is contained in:
parent
ffeb8f4572
commit
1b3684c9c1
|
@ -82,9 +82,9 @@ namespace arith {
|
|||
if (m_nla) m_nla->collect_statistics(st);
|
||||
}
|
||||
|
||||
void solver::explain_assumptions() {
|
||||
void solver::explain_assumptions(lp::explanation const& e) {
|
||||
unsigned i = 0;
|
||||
for (auto const & ev : m_explanation) {
|
||||
for (auto const & ev : e) {
|
||||
++i;
|
||||
auto idx = ev.ci();
|
||||
if (UINT_MAX == idx)
|
||||
|
@ -118,17 +118,17 @@ namespace arith {
|
|||
if (!ctx.use_drat())
|
||||
return nullptr;
|
||||
m_arith_hint.set_type(ctx, ty);
|
||||
explain_assumptions();
|
||||
explain_assumptions(m_explanation);
|
||||
if (lit != sat::null_literal)
|
||||
m_arith_hint.add_lit(rational(1), ~lit);
|
||||
return m_arith_hint.mk(ctx);
|
||||
}
|
||||
|
||||
arith_proof_hint const* solver::explain_implied_eq(euf::enode* a, euf::enode* b) {
|
||||
arith_proof_hint const* solver::explain_implied_eq(lp::explanation const& e, euf::enode* a, euf::enode* b) {
|
||||
if (!ctx.use_drat())
|
||||
return nullptr;
|
||||
m_arith_hint.set_type(ctx, hint_type::implied_eq_h);
|
||||
explain_assumptions();
|
||||
explain_assumptions(e);
|
||||
m_arith_hint.set_num_le(1); // TODO
|
||||
m_arith_hint.add_diseq(a, b);
|
||||
return m_arith_hint.mk(ctx);
|
||||
|
|
|
@ -320,7 +320,7 @@ namespace arith {
|
|||
reset_evidence();
|
||||
for (auto ev : e)
|
||||
set_evidence(ev.ci());
|
||||
auto* ex = explain_implied_eq(n1, n2);
|
||||
auto* ex = explain_implied_eq(e, n1, n2);
|
||||
auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, n1, n2, ex);
|
||||
ctx.propagate(n1, n2, jst->to_index());
|
||||
return true;
|
||||
|
@ -744,7 +744,7 @@ namespace arith {
|
|||
set_evidence(ci4);
|
||||
enode* x = var2enode(v1);
|
||||
enode* y = var2enode(v2);
|
||||
auto* ex = explain_implied_eq(x, y);
|
||||
auto* ex = explain_implied_eq(m_explanation, x, y);
|
||||
auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y, ex);
|
||||
ctx.propagate(x, y, jst->to_index());
|
||||
}
|
||||
|
|
|
@ -71,10 +71,10 @@ namespace arith {
|
|||
unsigned m_lit_head = 0, m_lit_tail = 0, m_eq_head = 0, m_eq_tail = 0;
|
||||
void reset() { m_lit_head = m_lit_tail; m_eq_head = m_eq_tail; }
|
||||
void add(euf::enode* a, euf::enode* b, bool is_eq) {
|
||||
if (m_eq_tail < m_eqs.size())
|
||||
m_eqs[m_eq_tail] = std::tuple(a, b, is_eq);
|
||||
else
|
||||
m_eqs.push_back(std::tuple(a, b, is_eq));
|
||||
if (m_eq_tail < m_eqs.size())
|
||||
m_eqs[m_eq_tail] = { a, b, is_eq };
|
||||
else
|
||||
m_eqs.push_back({a, b, is_eq });
|
||||
m_eq_tail++;
|
||||
}
|
||||
public:
|
||||
|
@ -476,9 +476,9 @@ namespace arith {
|
|||
arith_proof_hint_builder m_arith_hint;
|
||||
|
||||
arith_proof_hint const* explain(hint_type ty, sat::literal lit = sat::null_literal);
|
||||
arith_proof_hint const* explain_implied_eq(euf::enode* a, euf::enode* b);
|
||||
arith_proof_hint const* explain_implied_eq(lp::explanation const& e, euf::enode* a, euf::enode* b);
|
||||
arith_proof_hint const* explain_trichotomy(sat::literal le, sat::literal ge, sat::literal eq);
|
||||
void explain_assumptions();
|
||||
void explain_assumptions(lp::explanation const& e);
|
||||
|
||||
|
||||
public:
|
||||
|
|
Loading…
Reference in a new issue