diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index 50561ef60..b90daf29a 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -182,9 +182,9 @@ public: } m_solver->pop(1); std::cout << "(verified-smt"; - if (proof_hint) std::cout << " " << mk_bounded_pp(proof_hint, m, 4); + if (proof_hint) std::cout << "\n" << mk_bounded_pp(proof_hint, m, 4); for (expr* arg : clause) - std::cout << " " << mk_bounded_pp(arg, m); + std::cout << "\n " << mk_bounded_pp(arg, m); std::cout << ")\n"; add_clause(clause); } diff --git a/src/sat/smt/arith_proof_checker.h b/src/sat/smt/arith_proof_checker.h index 6f471f58e..0e5c891d5 100644 --- a/src/sat/smt/arith_proof_checker.h +++ b/src/sat/smt/arith_proof_checker.h @@ -143,17 +143,13 @@ namespace arith { SASSERT(m_todo.empty()); m_todo.push_back({ mul, e }); rational coeff1; - expr* e1, *e2, *e3; + expr* e1, *e2; for (unsigned i = 0; i < m_todo.size(); ++i) { auto [coeff, e] = m_todo[i]; - if (a.is_mul(e, e1, e2) && a.is_numeral(e1, coeff1)) + if (a.is_mul(e, e1, e2) && is_numeral(e1, coeff1)) m_todo.push_back({coeff*coeff1, e2}); - else if (a.is_mul(e, e1, e2) && a.is_uminus(e1, e3) && a.is_numeral(e3, coeff1)) - m_todo.push_back({-coeff*coeff1, e2}); - else if (a.is_mul(e, e1, e2) && a.is_uminus(e2, e3) && a.is_numeral(e3, coeff1)) - m_todo.push_back({ -coeff * coeff1, e1 }); - else if (a.is_mul(e, e1, e2) && a.is_numeral(e2, coeff1)) - m_todo.push_back({coeff*coeff1, e1}); + else if (a.is_mul(e, e1, e2) && is_numeral(e2, coeff1)) + m_todo.push_back({ coeff * coeff1, e1 }); else if (a.is_add(e)) for (expr* arg : *to_app(e)) m_todo.push_back({coeff, arg}); @@ -163,15 +159,21 @@ namespace arith { m_todo.push_back({coeff, e1}); m_todo.push_back({-coeff, e2}); } - else if (a.is_numeral(e, coeff1)) + else if (is_numeral(e, coeff1)) r.m_coeff += coeff*coeff1; - else if (a.is_uminus(e, e1) && a.is_numeral(e1, coeff1)) - r.m_coeff -= coeff*coeff1; else add(r, e, coeff); } m_todo.reset(); } + + bool is_numeral(expr* e, rational& n) { + if (a.is_numeral(e, n)) + return true; + if (a.is_uminus(e, e) && a.is_numeral(e, n)) + return n.neg(), true; + return false; + } bool check_ineq(row& r) { if (r.m_coeffs.empty() && r.m_coeff > 0) @@ -182,9 +184,12 @@ namespace arith { } // triangulate equalities, substitute results into m_ineq, m_conseq. - void reduce_eq() { + // check consistency of equalities (they may be inconsisent) + bool reduce_eq() { for (unsigned i = 0; i < m_eqs.size(); ++i) { auto& r = m_eqs[i]; + if (r.m_coeffs.empty() && r.m_coeff != 0) + return false; if (r.m_coeffs.empty()) continue; auto [v, coeff] = *r.m_coeffs.begin(); @@ -193,6 +198,7 @@ namespace arith { resolve(v, m_ineq, coeff, r); resolve(v, m_conseq, coeff, r); } + return true; } @@ -231,7 +237,8 @@ namespace arith { bool check_farkas() { if (check_ineq(m_ineq)) return true; - reduce_eq(); + if (!reduce_eq()) + return true; if (check_ineq(m_ineq)) return true; @@ -244,7 +251,8 @@ namespace arith { // after all inequalities in ineq have been added up // bool check_bound() { - reduce_eq(); + if (!reduce_eq()) + return true; if (check_ineq(m_conseq)) return true; if (m_ineq.m_coeffs.empty() || @@ -401,8 +409,10 @@ namespace arith { return false; } num_le = coeff.get_unsigned(); - if (!add_implied_ineq(false, jst)) + if (!add_implied_ineq(false, jst)) { + IF_VERBOSE(0, display(verbose_stream() << "did not add implied eq")); return false; + } ++j; continue; } @@ -418,10 +428,24 @@ namespace arith { if (num_le == 0) { // we processed all the first inequalities, // check that they imply one half of the implied equality. - if (!check()) - return false; - reset(); - VERIFY(add_implied_ineq(true, jst)); + if (!check()) { + // we might have added the wrong direction of the implied equality. + // so try the opposite inequality. + add_implied_ineq(true, jst); + add_implied_ineq(true, jst); + if (check()) { + reset(); + add_implied_ineq(false, jst); + } + else { + IF_VERBOSE(0, display(verbose_stream() << "failed to check implied eq ")); + return false; + } + } + else { + reset(); + VERIFY(add_implied_ineq(true, jst)); + } } } else diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index b37cd1e99..8ee1a1d28 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -46,7 +46,7 @@ namespace euf { * so it isn't necessarily an axiom over EUF, * We will here leave it to the EUF checker to perform resolution steps. */ - void solver::log_antecedents(literal l, literal_vector const& r, eq_proof_hint* hint) { + void solver::log_antecedents(literal l, literal_vector const& r, th_proof_hint* hint) { TRACE("euf", log_antecedents(tout, l, r);); if (!use_drat()) return; diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index f432443e9..e7a77df5c 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -19,6 +19,7 @@ Author: #include "ast/ast_pp.h" #include "ast/ast_util.h" #include "ast/ast_ll_pp.h" +#include "ast/arith_decl_plugin.h" #include "sat/smt/euf_proof_checker.h" #include "sat/smt/arith_proof_checker.h" #include "sat/smt/q_proof_checker.h" @@ -58,15 +59,29 @@ namespace euf { class eq_proof_checker : public proof_checker_plugin { ast_manager& m; + arith_util m_arith; + expr_ref_vector m_trail; basic_union_find m_uf; svector> m_expr2id; ptr_vector m_id2expr; - svector> m_diseqs; + svector> m_diseqs; unsigned m_ts = 0; void merge(expr* x, expr* y) { m_uf.merge(expr2id(x), expr2id(y)); IF_VERBOSE(10, verbose_stream() << "merge " << mk_bounded_pp(x, m) << " == " << mk_bounded_pp(y, m) << "\n"); + merge_numeral(x); + merge_numeral(y); + } + + void merge_numeral(expr* x) { + rational n; + expr* y; + if (m_arith.is_uminus(x, y) && m_arith.is_numeral(y, n)) { + y = m_arith.mk_numeral(-n, x->get_sort()); + m_trail.push_back(y); + m_uf.merge(expr2id(x), expr2id(y)); + } } bool are_equal(expr* x, expr* y) { @@ -118,7 +133,7 @@ namespace euf { } public: - eq_proof_checker(ast_manager& m): m(m) {} + eq_proof_checker(ast_manager& m): m(m), m_arith(m), m_trail(m) {} expr_ref_vector clause(app* jst) override { expr_ref_vector result(m); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 5994ee3be..c29652803 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -200,16 +200,36 @@ namespace euf { s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx)); } + /** + Retrieve set of literals r that imply r. + Since the set of literals are retrieved modulo multiple theories in a single implication + we lose theory specific justifications. For proof logging we use a catch all rule "smt" + for the case where an equality is derived using more than congruence closure. + To create fully decomposed justifications it will be necessary to augment the justification + data-structure with information about the equality that is implied by the theory. + Then each justification will imply an equality s = t assuming literals 'r'. + The theory lemma is then r -> s = t, where s = t is an equality that is available for the EUF hint. + The EUF hint is resolved against r -> s = t to eliminate s = t and to create the resulting explanation. + + Example: + x - 3 = 0 => x = 3 by arithmetic + x = 3 => f(x) = f(3) by EUF + resolve to produce clause x - 3 = 0 => f(x) = f(3) + */ + void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) { m_egraph.begin_explain(); m_explain.reset(); if (use_drat() && !probing) push(restore_size_trail(m_explain_cc, m_explain_cc.size())); auto* ext = sat::constraint_base::to_extension(idx); + bool has_theory = false; if (ext == this) get_antecedents(l, constraint::from_idx(idx), r, probing); - else + else { ext->get_antecedents(l, idx, r, probing); + has_theory = true; + } for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) { size_t* e = m_explain[qhead]; if (is_literal(e)) @@ -220,10 +240,20 @@ namespace euf { SASSERT(ext != this); sat::literal lit = sat::null_literal; ext->get_antecedents(lit, idx, r, probing); + has_theory = true; } } m_egraph.end_explain(); - eq_proof_hint* hint = (use_drat() && !probing) ? mk_hint(l, r) : nullptr; + th_proof_hint* hint = nullptr; + if (use_drat() && !probing) { + if (has_theory) { + r.push_back(~l); + hint = mk_smt_hint(symbol("smt"), r); + r.pop_back(); + } + else + hint = mk_hint(l, r); + } unsigned j = 0; for (sat::literal lit : r) if (s().lvl(lit) > 0) r[j++] = lit; diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index c18124491..bf18ca4bc 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -193,7 +193,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, eq_proof_hint* hint); + void log_antecedents(literal l, literal_vector const& r, th_proof_hint* hint); void log_justification(literal l, th_explain const& jst); typedef std::pair expr_pair; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index ca2f8f8f6..038cd337b 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -284,11 +284,15 @@ struct goal2sat::imp : public sat::sat_internalizer { if (v == sat::null_bool_var) { if (m.is_true(t)) { sat::literal tt = sat::literal(mk_bool_var(t), false); + if (m_euf && ensure_euf()->use_drat()) + ensure_euf()->set_bool_var2expr(tt.var(), t); mk_root_clause(tt); l = sign ? ~tt : tt; } else if (m.is_false(t)) { sat::literal ff = sat::literal(mk_bool_var(t), false); + if (m_euf && ensure_euf()->use_drat()) + ensure_euf()->set_bool_var2expr(ff.var(), t); mk_root_clause(~ff); l = sign ? ~ff : ff; }