mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

track lia conflicts as cuts

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-28 17:40:56 -07:00
parent de1cf30ea8
commit 0606ca15d9
3 changed files with 18 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/arith_diagnostics.cpp
View file

@ -133,7 +133,7 @@ namespace arith {
return m_arith_hint.mk(ctx);
}
arith_proof_hint const* solver::explain_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
arith_proof_hint const* solver::explain_conflict(hint_type ty, sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
arith_proof_hint* hint = nullptr;
if (ctx.use_drat()) {
m_coeffs.reset();
@ -142,7 +142,7 @@ namespace arith {
m_coeffs.push_back(e.coeff());
}
m_arith_hint.set_type(ctx, hint_type::farkas_h);
m_arith_hint.set_type(ctx, ty);
if (m_coeffs.size() == core.size()) {
unsigned i = 0;
for (auto lit : core)
@ -206,6 +206,9 @@ namespace arith {
case hint_type::implied_eq_h:
name = "implied-eq";
break;
case hint_type::nla_h:
name = "nla";
break;
default:
name = "unknown-arithmetic";
break;

16
src/sat/smt/arith_solver.cpp
View file

@ -1155,7 +1155,7 @@ namespace arith {
case lp::lia_move::conflict:
TRACE("arith", tout << "conflict\n";);
// ex contains unsat core
set_conflict();
set_conflict(hint_type::cut_h);
return l_false;
case lp::lia_move::undef:
TRACE("arith", tout << "lia undef\n";);
@ -1187,15 +1187,15 @@ namespace arith {
void solver::get_infeasibility_explanation_and_set_conflict() {
m_explanation.clear();
lp().get_infeasibility_explanation(m_explanation);
set_conflict();
set_conflict(hint_type::farkas_h);
}
void solver::set_conflict() {
void solver::set_conflict(hint_type ty) {
literal_vector core;
set_conflict_or_lemma(core, true);
set_conflict_or_lemma(ty, core, true);
}
void solver::set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
void solver::set_conflict_or_lemma(hint_type ty, literal_vector const& core, bool is_conflict) {
reset_evidence();
m_core.append(core);
for (auto ev : m_explanation)
@ -1212,7 +1212,7 @@ namespace arith {
for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()));
++m_num_conflicts;
++m_stats.m_conflicts;
auto* hint = explain_conflict(m_core, m_eqs);
auto* hint = explain_conflict(ty, m_core, m_eqs);
ctx.set_conflict(euf::th_explain::conflict(*this, m_core, m_eqs, hint));
}
else {
@ -1221,7 +1221,7 @@ namespace arith {
for (literal& c : m_core)
c.neg();
add_redundant(m_core, explain(hint_type::farkas_h));
add_redundant(m_core, explain(ty));
}
}
@ -1428,7 +1428,7 @@ namespace arith {
lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower));
core.push_back(pos ? lit : ~lit);
}
set_conflict_or_lemma(core, false);
set_conflict_or_lemma(hint_type::nla_h, core, false);
}
lbool solver::check_nla() {

9
src/sat/smt/arith_solver.h
View file

@ -52,7 +52,8 @@ namespace arith {
farkas_h,
bound_h,
cut_h,
implied_eq_h
implied_eq_h,
nla_h
};
struct arith_proof_hint : public euf::th_proof_hint {
@ -457,8 +458,8 @@ namespace arith {
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs);
void get_infeasibility_explanation_and_set_conflict();
void set_conflict();
void set_conflict_or_lemma(literal_vector const& core, bool is_conflict);
void set_conflict(hint_type ty);
void set_conflict_or_lemma(hint_type ty, literal_vector const& core, bool is_conflict);
void set_evidence(lp::constraint_index idx);
void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, euf::th_proof_hint const* pma);
@ -470,7 +471,7 @@ namespace arith {
arith_proof_hint const* explain(hint_type ty, sat::literal lit = sat::null_literal);
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);
arith_proof_hint const* explain_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
arith_proof_hint const* explain_conflict(hint_type ty, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
void explain_assumptions(lp::explanation const& e);