From 0f475f45b5adc62de1172f2ab2ba2e1dd64a81ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Aug 2022 09:45:19 -0700 Subject: [PATCH] Add RUP checking mode to proof checker. --- src/cmd_context/extra_cmds/proof_cmds.cpp | 62 ++++++++++++++++++----- src/sat/smt/arith_diagnostics.cpp | 4 +- src/sat/smt/arith_proof_checker.h | 16 ++++-- 3 files changed, 63 insertions(+), 19 deletions(-) diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index cd263554a..6213e7cd3 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -25,8 +25,8 @@ Notes: #include "ast/ast_util.h" #include "cmd_context/cmd_context.h" #include "smt/smt_solver.h" -// include "sat/sat_solver.h" -// include "sat/sat_drat.h" +#include "sat/sat_solver.h" +#include "sat/sat_drat.h" #include "sat/smt/euf_proof_checker.h" #include @@ -37,31 +37,68 @@ class smt_checker { scoped_ptr m_solver; -#if 0 - sat::solver sat_solver; + symbol m_rup; + sat::solver m_sat_solver; sat::drat m_drat; sat::literal_vector m_units; - sat::literal_vector m_drup_units; + sat::literal_vector m_clause; void add_units() { auto const& units = m_drat.units(); for (unsigned i = m_units.size(); i < units.size(); ++i) m_units.push_back(units[i].first); } -#endif public: smt_checker(ast_manager& m): m(m), - m_checker(m) - // sat_solver(m_params, m.limit()), - // m_drat(sat_solver) + m_checker(m), + m_sat_solver(m_params, m.limit()), + m_drat(m_sat_solver) { + m_params.set_bool("drat.check_unsat", true); + m_sat_solver.updt_params(m_params); + m_drat.updt_config(); m_solver = mk_smt_solver(m, m_params, symbol()); + m_rup = symbol("rup"); + } + + bool is_rup(expr* proof_hint) { + return + proof_hint && + is_app(proof_hint) && + to_app(proof_hint)->get_name() == m_rup; + } + + void mk_clause(expr_ref_vector const& clause) { + m_clause.reset(); + for (expr* e : clause) { + bool sign = false; + while (m.is_not(e, e)) + sign = !sign; + m_clause.push_back(sat::literal(e->get_id(), sign)); + } + } + + bool check_rup(expr_ref_vector const& clause) { + add_units(); + mk_clause(clause); + return m_drat.is_drup(m_clause.size(), m_clause.data(), m_units); + } + + void add_clause(expr_ref_vector const& clause) { + mk_clause(clause); + m_drat.add(m_clause, sat::status::input()); } void check(expr_ref_vector const& clause, expr* proof_hint) { + + if (is_rup(proof_hint) && check_rup(clause)) { + std::cout << "(verified-rup)\n"; + return; + } + if (m_checker.check(clause, proof_hint)) { if (is_app(proof_hint)) std::cout << "(verified-" << to_app(proof_hint)->get_name() << ")\n"; @@ -90,15 +127,16 @@ public: } void assume(expr_ref_vector const& clause) { + add_clause(clause); m_solver->assert_expr(mk_or(clause)); } }; class proof_cmds_imp : public proof_cmds { - ast_manager& m; + ast_manager& m; expr_ref_vector m_lits; - expr_ref m_proof_hint; - smt_checker m_checker; + expr_ref m_proof_hint; + smt_checker m_checker; public: proof_cmds_imp(ast_manager& m): m(m), m_lits(m), m_proof_hint(m), m_checker(m) {} diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index d702806d0..3c3235df1 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -158,14 +158,14 @@ namespace arith { sort_ref_vector sorts(m); for (unsigned i = m_lit_head; i < m_lit_tail; ++i) { auto const& [coeff, lit] = a.m_arith_hint.lit(i); - args.push_back(arith.mk_int(coeff*lc)); + args.push_back(arith.mk_int(abs(coeff*lc))); args.push_back(s.literal2expr(lit)); } for (unsigned i = m_eq_head; i < m_eq_tail; ++i) { auto const& [x, y, is_eq] = a.m_arith_hint.eq(i); expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m); if (!is_eq) eq = m.mk_not(eq); - args.push_back(arith.mk_int(lc)); + args.push_back(arith.mk_int(1)); args.push_back(eq); } for (expr* arg : args) diff --git a/src/sat/smt/arith_proof_checker.h b/src/sat/smt/arith_proof_checker.h index 0f223081b..d1d0c089c 100644 --- a/src/sat/smt/arith_proof_checker.h +++ b/src/sat/smt/arith_proof_checker.h @@ -370,7 +370,10 @@ namespace arith { expr* x, *y; for (expr* arg : *jst) { if (even) { - VERIFY(a.is_numeral(arg, coeff)); + if (!a.is_numeral(arg, coeff)) { + IF_VERBOSE(0, verbose_stream() << "not numeral " << mk_pp(jst, m) << "\n"); + return false; + } } else { bool sign = m.is_not(arg, arg); @@ -387,13 +390,16 @@ namespace arith { } even = !even; } - // display(verbose_stream()); - // todo: correlate with literals in clause, literals that are not in clause should have RUP property. - return check_farkas(); + if (check_farkas()) + return true; + + IF_VERBOSE(0, verbose_stream() << "did not check farkas\n" << mk_pp(jst, m) << "\n"); + return false; } // todo: rules for bounds and implied-by - + + IF_VERBOSE(0, verbose_stream() << "did not check " << mk_pp(jst, m) << "\n"); return false; }