From b758d5b2b1fbf5efc2b606dc199cb00e01791b76 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Oct 2022 17:51:01 -0700 Subject: [PATCH] wip - proof checking, add support for distinct, other fixes --- src/math/lp/lar_solver.h | 44 ++++++++++------ src/sat/smt/CMakeLists.txt | 2 +- src/sat/smt/arith_theory_checker.h | 6 ++- src/sat/smt/distinct_theory_checker.h | 50 +++++++++++++++++++ src/sat/smt/euf_internalize.cpp | 22 ++++---- src/sat/smt/euf_proof.cpp | 5 ++ src/sat/smt/euf_proof_checker.cpp | 6 ++- src/sat/smt/euf_solver.h | 5 ++ ...checker.cpp => tseitin_theory_checker.cpp} | 18 +++++-- ...oof_checker.h => tseitin_theory_checker.h} | 4 +- 10 files changed, 124 insertions(+), 38 deletions(-) create mode 100644 src/sat/smt/distinct_theory_checker.h rename src/sat/smt/{tseitin_proof_checker.cpp => tseitin_theory_checker.cpp} (94%) rename src/sat/smt/{tseitin_proof_checker.h => tseitin_theory_checker.h} (95%) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index e7f8d0ea4..f13231610 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -295,70 +295,86 @@ class lar_solver : public column_namer { public: // this function just looks at the status bool is_feasible() const; + const map, default_eq>& fixed_var_table_int() const { return m_fixed_var_table_int; } + map, default_eq>& fixed_var_table_int() { return m_fixed_var_table_int; } + const map, default_eq>& fixed_var_table_real() const { return m_fixed_var_table_real; } + map, default_eq>& fixed_var_table_real() { return m_fixed_var_table_real; } bool find_in_fixed_tables(const rational& mpq, bool is_int, unsigned & j) const { - return is_int? fixed_var_table_int().find(mpq, j) : - fixed_var_table_real().find(mpq, j); + return is_int? fixed_var_table_int().find(mpq, j) : fixed_var_table_real().find(mpq, j); } template void remove_non_fixed_from_table(T&); + unsigned external_to_column_index(unsigned) const; + bool inside_bounds(lpvar, const impq&) const; + inline void set_column_value(unsigned j, const impq& v) { m_mpq_lar_core_solver.m_r_solver.update_x(j, v); } + inline void set_column_value_test(unsigned j, const impq& v) { set_column_value(j, v); } + unsigned get_total_iterations() const; + var_index add_named_var(unsigned ext_j, bool is_integer, const std::string&); + lp_status maximize_term(unsigned j_or_term, impq &term_max); - inline - core_solver_pretty_printer pp(std::ostream& out) const { return - core_solver_pretty_printer(m_mpq_lar_core_solver.m_r_solver, out); } + + inline core_solver_pretty_printer pp(std::ostream& out) const { + return core_solver_pretty_printer(m_mpq_lar_core_solver.m_r_solver, out); + } + void get_infeasibility_explanation(explanation &) const; + inline void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; } + inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; } + template void explain_implied_bound(const implied_bound & ib, lp_bound_propagator & bp) { unsigned i = ib.m_row_or_term_index; - int bound_sign = ib.m_is_lower_bound? 1: -1; - int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; + int bound_sign = (ib.m_is_lower_bound ? 1 : -1); + int j_sign = (ib.m_coeff_before_j_is_pos ? 1 : -1) * bound_sign; unsigned bound_j = ib.m_j; - if (tv::is_term(bound_j)) { + if (tv::is_term(bound_j)) bound_j = m_var_register.external_to_local(bound_j); - } - for (auto const& r : A_r().m_rows[i]) { + + for (auto const& r : get_row(i)) { unsigned j = r.var(); - if (j == bound_j) continue; + if (j == bound_j) + continue; mpq const& a = r.coeff(); - int a_sign = is_pos(a)? 1: -1; + int a_sign = is_pos(a) ? 1 : -1; int sign = j_sign * a_sign; const ul_pair & ul = m_columns_to_ul_pairs[j]; - auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness(); + auto witness = sign > 0 ? ul.upper_bound_witness() : ul.lower_bound_witness(); lp_assert(is_valid(witness)); bp.consume(a, witness); } } void set_value_for_nbasic_column(unsigned j, const impq& new_val); + inline unsigned get_base_column_in_row(unsigned row_index) const { return m_mpq_lar_core_solver.m_r_solver.get_base_column_in_row(row_index); } - // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); } constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side); void activate_check_on_equal(constraint_index, var_index&); diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 0b1e68e96..cef7f96c4 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -41,7 +41,7 @@ z3_add_component(sat_smt q_solver.cpp recfun_solver.cpp sat_th.cpp - tseitin_proof_checker.cpp + tseitin_theory_checker.cpp user_solver.cpp COMPONENT_DEPENDENCIES sat diff --git a/src/sat/smt/arith_theory_checker.h b/src/sat/smt/arith_theory_checker.h index f11e7ae29..65c647658 100644 --- a/src/sat/smt/arith_theory_checker.h +++ b/src/sat/smt/arith_theory_checker.h @@ -241,7 +241,7 @@ namespace arith { return true; if (check_ineq(m_ineq)) return true; - + IF_VERBOSE(3, display_row(verbose_stream() << "Failed to verify Farkas with reduced row ", m_ineq) << "\n"); // convert to expression, maybe follows from a cut. return false; } @@ -452,7 +452,9 @@ namespace arith { add_ineq(coeff, arg, sign); } else if (m.is_eq(arg, x, y)) { - if (sign) + if (is_bound && j + 1 == jst->get_num_args()) + add_conseq(coeff, arg, sign); + else if (sign) return check(); // it should be an implied equality else add_eq(x, y); diff --git a/src/sat/smt/distinct_theory_checker.h b/src/sat/smt/distinct_theory_checker.h new file mode 100644 index 000000000..a2fb366f7 --- /dev/null +++ b/src/sat/smt/distinct_theory_checker.h @@ -0,0 +1,50 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + distinct_proof_checker.h + +Abstract: + + Plugin for checking distinct internalization + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-07 + +Note: + + First version just trusts that distinct is internalized correctly. + + +--*/ +#pragma once + +#include "sat/smt/euf_proof_checker.h" +#include + +namespace distinct { + + class theory_checker : public euf::theory_checker_plugin { + ast_manager& m; + public: + theory_checker(ast_manager& m): + m(m) { + } + + expr_ref_vector clause(app* jst) override { + expr_ref_vector result(m); + result.append(jst->get_num_args(), jst->get_args()); + return result; + } + + bool check(app* jst) override { return true; } + + void register_plugins(euf::theory_checker& pc) override { + pc.register_plugin(symbol("distinct"), this); + } + + }; + +} diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 3c8956751..1bad6fc6b 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -216,10 +216,9 @@ namespace euf { void solver::add_not_distinct_axiom(app* e, enode* const* args) { SASSERT(m.is_distinct(e)); unsigned sz = e->get_num_args(); - sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id()); if (sz <= 1) { - s().mk_clause(0, nullptr, st); + s().mk_clause(0, nullptr, mk_distinct_status(0, nullptr)); return; } @@ -234,7 +233,7 @@ namespace euf { } } add_root(lits); - s().mk_clause(lits, st); + s().mk_clause(lits, mk_distinct_status(lits)); } else { // g(f(x_i)) = x_i @@ -252,13 +251,13 @@ namespace euf { expr_ref gapp(m.mk_app(g, fapp.get()), m); expr_ref eq = mk_eq(gapp, arg); sat::literal lit = mk_literal(eq); - s().add_clause(lit, st); + s().add_clause(lit, mk_distinct_status(lit)); eqs.push_back(mk_eq(fapp, a)); } pb_util pb(m); expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m); sat::literal lit = si.internalize(at_least2, m_is_redundant); - s().add_clause(lit, st); + s().add_clause(lit, mk_distinct_status(lit)); } } @@ -266,19 +265,19 @@ namespace euf { SASSERT(m.is_distinct(e)); static const unsigned distinct_max_args = 32; unsigned sz = e->get_num_args(); - sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id()); + if (sz <= 1) - return; + return; sort* srt = e->get_arg(0)->get_sort(); auto sort_sz = srt->get_num_elements(); if (sort_sz.is_finite() && sort_sz.size() < sz) - s().add_clause(0, nullptr, st); + s().add_clause(0, nullptr, mk_tseitin_status(0, nullptr)); else if (sz <= distinct_max_args) { for (unsigned i = 0; i < sz; ++i) { for (unsigned j = i + 1; j < sz; ++j) { expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr()); sat::literal lit = ~mk_literal(eq); - s().add_clause(lit, st); + s().add_clause(lit, mk_distinct_status(lit)); } } } @@ -294,20 +293,19 @@ namespace euf { n->mark_interpreted(); expr_ref eq = mk_eq(fapp, fresh); sat::literal lit = mk_literal(eq); - s().add_clause(lit, st); + s().add_clause(lit, mk_distinct_status(lit)); } } } void solver::axiomatize_basic(enode* n) { expr* e = n->get_expr(); - sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id()); expr* c = nullptr, * th = nullptr, * el = nullptr; if (!m.is_bool(e) && m.is_ite(e, c, th, el)) { expr_ref eq_th = mk_eq(e, th); sat::literal lit_th = mk_literal(eq_th); if (th == el) { - s().add_clause(lit_th, st); + s().add_clause(lit_th, mk_tseitin_status(lit_th)); } else { sat::literal lit_c = mk_literal(c); diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 78b207f94..4f2677208 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -237,6 +237,11 @@ namespace euf { th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("tseitin"), n, lits) : nullptr; return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph); } + + sat::status solver::mk_distinct_status(unsigned n, sat::literal const* lits) { + th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("distinct"), n, lits) : nullptr; + return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph); + } expr* smt_proof_hint::get_hint(euf::solver& s) const { ast_manager& m = s.get_manager(); diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index 98032a86b..c6218f2fe 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -25,7 +25,8 @@ Author: #include "sat/smt/euf_proof_checker.h" #include "sat/smt/arith_theory_checker.h" #include "sat/smt/q_theory_checker.h" -#include "sat/smt/tseitin_proof_checker.h" +#include "sat/smt/distinct_theory_checker.h" +#include "sat/smt/tseitin_theory_checker.h" namespace euf { @@ -287,6 +288,7 @@ namespace euf { add_plugin(alloc(eq_theory_checker, m)); add_plugin(alloc(res_checker, m, *this)); add_plugin(alloc(q::theory_checker, m)); + add_plugin(alloc(distinct::theory_checker, m)); add_plugin(alloc(smt_theory_checker_plugin, m, symbol("datatype"))); // no-op datatype proof checker add_plugin(alloc(tseitin::theory_checker, m)); } @@ -437,7 +439,7 @@ namespace euf { if (m_checker.check(clause, proof_hint, units)) { bool units_are_rup = true; for (expr* u : units) { - if (!check_rup(u)) { + if (!m.is_true(u) && !check_rup(u)) { std::cout << "unit " << mk_bounded_pp(u, m) << " is not rup\n"; units_are_rup = false; } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 62e7abcae..f4109bed1 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -407,8 +407,13 @@ namespace euf { smt_proof_hint* mk_smt_clause(symbol const& n, unsigned nl, literal const* lits); th_proof_hint* mk_cc_proof_hint(sat::literal_vector const& ante, app* a, app* b); th_proof_hint* mk_tc_proof_hint(sat::literal const* ternary_clause); + sat::status mk_tseitin_status(sat::literal a) { return mk_tseitin_status(1, &a); } sat::status mk_tseitin_status(sat::literal a, sat::literal b); sat::status mk_tseitin_status(unsigned n, sat::literal const* lits); + sat::status mk_distinct_status(sat::literal a) { return mk_distinct_status(1, &a); } + sat::status mk_distinct_status(sat::literal a, sat::literal b) { sat::literal lits[2] = { a, b }; return mk_distinct_status(2, lits); } + sat::status mk_distinct_status(sat::literal_vector const& lits) { return mk_distinct_status(lits.size(), lits.data()); } + sat::status mk_distinct_status(unsigned n, sat::literal const* lits); scoped_ptr m_proof_out; diff --git a/src/sat/smt/tseitin_proof_checker.cpp b/src/sat/smt/tseitin_theory_checker.cpp similarity index 94% rename from src/sat/smt/tseitin_proof_checker.cpp rename to src/sat/smt/tseitin_theory_checker.cpp index 19f6e8660..a15d0277b 100644 --- a/src/sat/smt/tseitin_proof_checker.cpp +++ b/src/sat/smt/tseitin_theory_checker.cpp @@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation Module Name: - tseitin_proof_checker.cpp + tseitin_theory_checker.cpp Abstract: @@ -27,7 +27,7 @@ TODOs: --*/ #include "ast/ast_pp.h" -#include "sat/smt/tseitin_proof_checker.h" +#include "sat/smt/tseitin_theory_checker.h" namespace tseitin { @@ -41,20 +41,28 @@ namespace tseitin { bool theory_checker::check(app* jst) { expr* main_expr = nullptr; unsigned max_depth = 0; + expr* a, * x, * y, * z, * u, * v; + for (expr* arg : *jst) { unsigned arg_depth = get_depth(arg); if (arg_depth > max_depth) { main_expr = arg; max_depth = arg_depth; } - if (arg_depth == max_depth && m.is_not(main_expr)) - main_expr = arg; + if (arg_depth == max_depth && m.is_not(main_expr)) { + if (m.is_not(arg, x) && m.is_not(main_expr, y) && + is_app(x) && is_app(y) && + to_app(x)->get_num_args() < to_app(y)->get_num_args()) + continue; + + main_expr = arg; + } } if (!main_expr) return false; - expr* a, * x, * y, *z, *u, *v; + // (or (and a b) (not a) (not b)) // (or (and (not a) b) a (not b)) diff --git a/src/sat/smt/tseitin_proof_checker.h b/src/sat/smt/tseitin_theory_checker.h similarity index 95% rename from src/sat/smt/tseitin_proof_checker.h rename to src/sat/smt/tseitin_theory_checker.h index 8bbacd53b..f9ed071bc 100644 --- a/src/sat/smt/tseitin_proof_checker.h +++ b/src/sat/smt/tseitin_theory_checker.h @@ -3,11 +3,11 @@ Copyright (c) 2022 Microsoft Corporation Module Name: - tseitin_proof_checker.h + tseitin_theory_checker.h Abstract: - Plugin for checking quantifier instantiations + Plugin for checking tseitin internalization Author: