From 11477f1ed14d0af2e613ba58cef1ce3f1851b5a1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Dec 2020 10:40:17 -0800 Subject: [PATCH] fixes in new solver fix logging and lemma signs in arith_solver, move logging of drat equalities to euf --- src/sat/smt/arith_solver.cpp | 36 +++++++++++++++++++++--------------- src/sat/smt/bv_solver.cpp | 8 ++------ src/sat/smt/euf_proof.cpp | 27 +++++++++++++++++++++++++++ src/sat/smt/euf_solver.cpp | 11 ++--------- src/sat/smt/euf_solver.h | 2 ++ src/shell/drat_frontend.cpp | 8 ++++---- 6 files changed, 58 insertions(+), 34 deletions(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index e3022c9a2..f6f14cda0 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1120,9 +1120,12 @@ namespace arith { void solver::set_conflict_or_lemma(literal_vector const& core, bool is_conflict) { reset_evidence(); m_core.append(core); + TRACE("arith", + tout << "Core - " << is_conflict << "\n"; + for (literal c : m_core) tout << literal2expr(c) << "\n";); + ++m_num_conflicts; ++m_stats.m_conflicts; - TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n");); for (auto const& ev : m_explanation) set_evidence(ev.ci(), m_core, m_eqs); DEBUG_CODE( @@ -1134,6 +1137,11 @@ namespace arith { m_core.push_back(eq_internalize(eq.first, eq.second)); for (literal& c : m_core) c.neg(); + TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"); + tout << "Clause\n"; + for (literal c : m_core) tout << literal2expr(c) << "\n"; + ); + add_clause(m_core); } @@ -1322,25 +1330,23 @@ namespace arith { for (auto const& ineq : m_lemma.ineqs()) { bool is_lower = true, pos = true, is_eq = false; switch (ineq.cmp()) { - case lp::LE: is_lower = false; pos = false; break; - case lp::LT: is_lower = true; pos = true; break; - case lp::GE: is_lower = true; pos = false; break; - case lp::GT: is_lower = false; pos = true; break; - case lp::EQ: is_eq = true; pos = false; break; - case lp::NE: is_eq = true; pos = true; break; + case lp::LE: is_lower = false; pos = false; break; + case lp::LT: is_lower = true; pos = true; break; + case lp::GE: is_lower = true; pos = false; break; + case lp::GT: is_lower = false; pos = true; break; + case lp::EQ: is_eq = true; pos = false; break; + case lp::NE: is_eq = true; pos = true; break; default: UNREACHABLE(); } TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";); - app_ref atom(m); // TBD utility: lp::lar_term term = mk_term(ineq.m_poly); // then term is used instead of ineq.m_term - if (is_eq) { - core.push_back(~mk_eq(ineq.term(), ineq.rs())); - } - else { - // create term >= 0 (or term <= 0) - core.push_back(~ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower))); - } + sat::literal lit; + if (is_eq) + lit = mk_eq(ineq.term(), ineq.rs()); + else + lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower)); + core.push_back(pos ? lit : ~lit); } set_conflict_or_lemma(core, false); } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index f8d24147a..f42725a65 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -345,12 +345,8 @@ namespace bv { if (c.m_kind != bv_justification::kind_t::bit2ne) { expr* e1 = var2expr(c.m_v1); expr* e2 = var2expr(c.m_v2); - eq = m.mk_eq(e1, e2); - ctx.get_drat().def_begin('e', eq->get_id(), std::string("=")); - ctx.get_drat().def_add_arg(e1->get_id()); - ctx.get_drat().def_add_arg(e2->get_id()); - ctx.get_drat().def_end(); - ctx.get_drat().bool_def(leq.var(), eq->get_id()); + eq = m.mk_eq(e1, e2); + ctx.drat_eq_def(leq, eq); } static unsigned s_count = 0; diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index a848bb791..26f8bee23 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -126,5 +126,32 @@ namespace euf { } } + void solver::log_justification(literal l, th_propagation const& jst) { + literal_vector lits; + for (auto lit : euf::th_propagation::lits(jst)) + lits.push_back(~lit); + lits.push_back(l); + unsigned nv = s().num_vars(); + expr_ref_vector eqs(m); + for (auto eq : euf::th_propagation::eqs(jst)) { + ++nv; + literal lit(nv, false); + eqs.push_back(m.mk_eq(eq.first->get_expr(), eq.second->get_expr())); + drat_eq_def(lit, eqs.back()); + lits.push_back(lit); + } + + get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id())); + } + + void solver::drat_eq_def(literal lit, expr* eq) { + expr *a = nullptr, *b = nullptr; + VERIFY(m.is_eq(eq, a, b)); + get_drat().def_begin('e', eq->get_id(), std::string("=")); + get_drat().def_add_arg(a->get_id()); + get_drat().def_add_arg(b->get_id()); + get_drat().def_end(); + get_drat().bool_def(lit.var(), eq->get_id()); + } } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 206e8889f..d8efbeb67 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -211,15 +211,8 @@ namespace euf { for (auto eq : euf::th_propagation::eqs(jst)) add_antecedent(eq.first, eq.second); - if (!probing && use_drat()) { - literal_vector lits; - for (auto lit : euf::th_propagation::lits(jst)) - lits.push_back(~lit); - lits.push_back(l); - get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id())); - for (auto eq : euf::th_propagation::eqs(jst)) - IF_VERBOSE(0, verbose_stream() << "drat-log with equalities is TBD " << eq.first->get_expr_id() << "\n"); - } + if (!probing && use_drat()) + log_justification(l, jst); } void solver::add_antecedent(enode* a, enode* b) { diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 03faac300..7daa88dca 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -156,6 +156,7 @@ namespace euf { // proofs void log_antecedents(std::ostream& out, literal l, literal_vector const& r); void log_antecedents(literal l, literal_vector const& r); + void log_justification(literal l, th_propagation const& jst); void drat_log_decl(func_decl* f); void drat_log_expr(expr* n); void drat_log_expr1(expr* n); @@ -293,6 +294,7 @@ namespace euf { bool use_drat() { return s().get_config().m_drat && (init_drat(), true); } sat::drat& get_drat() { return s().get_drat(); } void drat_bool_def(sat::bool_var v, expr* n); + void drat_eq_def(sat::literal lit, expr* eq); // decompile bool extract_pb(std::function& card, diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp index 6778187d2..b7262e18c 100644 --- a/src/shell/drat_frontend.cpp +++ b/src/shell/drat_frontend.cpp @@ -203,12 +203,12 @@ public: } if (name == "Real" && sz == 4) { arith_util au(m); - rational num = sexpr->get_child(2)->get_numeral(); - rational den = sexpr->get_child(3)->get_numeral(); - result = au.mk_numeral(num/den, false); + rational r = sexpr->get_child(2)->get_numeral(); + // rational den = sexpr->get_child(3)->get_numeral(); + result = au.mk_numeral(r, false); return; } - if (name == "Int" && sz == 3) { + if (name == "Int" && sz == 4) { arith_util au(m); rational num = sexpr->get_child(2)->get_numeral(); result = au.mk_numeral(num, true);