mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

update proof formats for new core

Browse source 
- update proof format for quantifier instantiation to track original literals
- update proof replay tools with ability to extract proof object

The formats and features are subject to heavy revisions.

Example
```
(set-option :sat.euf true)
(set-option :sat.smt.proof eufproof.smt2)
(declare-fun f (Int) Int)
(declare-const x Int)
(assert (or (= (f (f (f x))) x) (= (f (f x)) x)))
(assert (not (= (f (f (f (f (f (f x)))))) x)))
(check-sat)
```

eufproof.smt2 is:
```
(declare-fun x () Int)
(declare-fun f (Int) Int)
(define-const $24 Int (f x))
(define-const $25 Int (f $24))
(define-const $26 Int (f $25))
(define-const $27 Bool (= $26 x))
(define-const $28 Bool (= $25 x))
(assume $27 $28)
(define-const $30 Int (f $26))
(define-const $31 Int (f $30))
(define-const $32 Int (f $31))
(define-const $33 Bool (= $32 x))
(assume (not $33))
(declare-fun rup () Proof)
(infer (not $33) rup)
(declare-fun euf (Bool Bool Proof Proof Proof Proof) Proof)
(declare-fun cc (Bool) Proof)
(define-const $42 Bool (= $32 $30))
(define-const $43 Proof (cc $42))
(define-const $40 Bool (= $31 $24))
(define-const $41 Proof (cc $40))
(define-const $38 Bool (= $30 $25))
(define-const $39 Proof (cc $38))
(define-const $36 Bool (= $24 $26))
(define-const $37 Proof (cc $36))
(define-const $34 Bool (not $33))
(define-const $44 Proof (euf $34 $28 $37 $39 $41 $43))
(infer (not $28) $33 $44)
(infer (not $28) rup)
(infer $27 rup)
(declare-fun euf (Bool Bool Proof Proof Proof) Proof)
(define-const $49 Bool (= $32 $26))
(define-const $50 Proof (cc $49))
(define-const $47 Bool (= $31 $25))
(define-const $48 Proof (cc $47))
(define-const $45 Bool (= $24 $30))
(define-const $46 Proof (cc $45))
(define-const $51 Proof (euf $34 $27 $46 $48 $50))
(infer $33 $51)
(infer rup)
```

Example of inspecting proof from Python:

```
from z3 import *

def parse(file):
    s = Solver()
    set_option("solver.proof.save", True)
    set_option("solver.proof.check", False)
    s.from_file(file)
    for step in s.proof().children():
        print(step)

parse("../eufproof.smt2")
```

Proof checking (self-validation) is on by default.
Proof saving is off by default.

You can use the proof logs and the proof terms to retrieve quantifier instantiations from the new core.

The self-checker contains a few built-in tuned checkers but falls back to self-checking inferred clauses using SMT.
This commit is contained in:
Nikolaj Bjorner 2022-09-28 10:40:43 -07:00
parent 9782d4a730
commit 107981f099
40 changed files with 295 additions and 153 deletions
Download patch file Download diff file Expand all files Collapse all files

47
src/sat/smt/arith_axioms.cpp
View file

@ -251,6 +251,17 @@ namespace arith {
if (hi_sup != end) mk_bound_axiom(b, *hi_sup);
}
void solver::add_farkas_clause(sat::literal l1, sat::literal l2) {
arith_proof_hint* bound_params = nullptr;
if (ctx.use_drat()) {
m_arith_hint.set_type(ctx, hint_type::farkas_h);
m_arith_hint.add_lit(rational(1), ~l1);
m_arith_hint.add_lit(rational(1), ~l2);
bound_params = m_arith_hint.mk(ctx);
}
add_clause(l1, l2, bound_params);
}
void solver::mk_bound_axiom(api_bound& b1, api_bound& b2) {
literal l1(b1.get_lit());
literal l2(b2.get_lit());
@ -263,55 +274,45 @@ namespace arith {
if (k1 == k2 && kind1 == kind2) return;
SASSERT(k1 != k2 || kind1 != kind2);
auto bin_clause = [&](sat::literal l1, sat::literal l2) {
arith_proof_hint* bound_params = nullptr;
if (ctx.use_drat()) {
m_arith_hint.set_type(ctx, hint_type::farkas_h);
m_arith_hint.add_lit(rational(1), ~l1);
m_arith_hint.add_lit(rational(1), ~l2);
bound_params = m_arith_hint.mk(ctx);
}
add_clause(l1, l2, bound_params);
};
if (kind1 == lp_api::lower_t) {
if (kind2 == lp_api::lower_t) {
if (k2 <= k1)
bin_clause(~l1, l2);
add_farkas_clause(~l1, l2);
else
bin_clause(l1, ~l2);
add_farkas_clause(l1, ~l2);
}
else if (k1 <= k2)
// k1 <= k2, k1 <= x or x <= k2
bin_clause(l1, l2);
add_farkas_clause(l1, l2);
else {
// k1 > hi_inf, k1 <= x => ~(x <= hi_inf)
bin_clause(~l1, ~l2);
add_farkas_clause(~l1, ~l2);
if (v_is_int && k1 == k2 + rational(1))
// k1 <= x or x <= k1-1
bin_clause(l1, l2);
add_farkas_clause(l1, l2);
}
}
else if (kind2 == lp_api::lower_t) {
if (k1 >= k2)
// k1 >= lo_inf, k1 >= x or lo_inf <= x
bin_clause(l1, l2);
add_farkas_clause(l1, l2);
else {
// k1 < k2, k2 <= x => ~(x <= k1)
bin_clause(~l1, ~l2);
add_farkas_clause(~l1, ~l2);
if (v_is_int && k1 == k2 - rational(1))
// x <= k1 or k1+l <= x
bin_clause(l1, l2);
add_farkas_clause(l1, l2);
}
}
else {
// kind1 == A_UPPER, kind2 == A_UPPER
if (k1 >= k2)
// k1 >= k2, x <= k2 => x <= k1
bin_clause(l1, ~l2);
add_farkas_clause(l1, ~l2);
else
// k1 <= hi_sup , x <= k1 => x <= hi_sup
bin_clause(~l1, l2);
add_farkas_clause(~l1, l2);
}
}
@ -421,9 +422,9 @@ namespace arith {
ge = mk_literal(a.mk_ge(diff, zero));
}
++m_stats.m_assert_diseq;
add_clause(~eq, le);
add_clause(~eq, ge);
add_clause(~le, ~ge, eq);
add_farkas_clause(~eq, le);
add_farkas_clause(~eq, ge);
add_clause(~le, ~ge, eq, explain_triangle_eq(le, ge, eq));
}

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

@ -133,6 +133,16 @@ namespace arith {
return m_arith_hint.mk(ctx);
}
arith_proof_hint const* solver::explain_triangle_eq(sat::literal le, sat::literal ge, sat::literal eq) {
if (!ctx.use_drat())
return nullptr;
m_arith_hint.set_type(ctx, hint_type::implied_eq_h);
m_arith_hint.add_lit(rational(1), le);
m_arith_hint.add_lit(rational(1), ge);
m_arith_hint.add_lit(rational(1), ~eq);
return m_arith_hint.mk(ctx);
}
expr* arith_proof_hint::get_hint(euf::solver& s) const {
ast_manager& m = s.get_manager();
family_id fid = m.get_family_id("arith");

10
src/sat/smt/arith_proof_checker.h
View file

@ -383,14 +383,13 @@ namespace arith {
neg.mark(e, true);
else
pos.mark(e, true);
if (jst->get_name() != m_farkas &&
jst->get_name() != m_bound &&
jst->get_name() != m_implied_eq) {
bool is_bound = jst->get_name() == m_bound;
bool is_implied_eq = jst->get_name() == m_implied_eq;
bool is_farkas = jst->get_name() == m_farkas;
if (!is_farkas && !is_bound && !is_implied_eq) {
IF_VERBOSE(0, verbose_stream() << "unhandled inference " << mk_pp(jst, m) << "\n");
return false;
}
bool is_bound = jst->get_name() == m_bound;
bool even = true;
rational coeff;
expr* x, * y;
@ -436,7 +435,6 @@ namespace arith {
if (check())
return true;
IF_VERBOSE(0, verbose_stream() << "did not check condition\n" << mk_pp(jst, m) << "\n"; display(verbose_stream()); );
return false;
}

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

@ -322,6 +322,7 @@ namespace arith {
void mk_bound_axiom(api_bound& b1, api_bound& b2);
void mk_power0_axioms(app* t, app* n);
void flush_bound_axioms();
void add_farkas_clause(sat::literal l1, sat::literal l2);
// bounds
struct compare_bounds {
@ -473,6 +474,7 @@ namespace arith {
arith_proof_hint const* explain(hint_type ty, sat::literal lit = sat::null_literal);
arith_proof_hint const* explain_implied_eq(euf::enode* a, euf::enode* b);
arith_proof_hint const* explain_triangle_eq(sat::literal le, sat::literal ge, sat::literal eq);
void explain_assumptions();

26
src/sat/smt/euf_proof.cpp
View file

@ -92,16 +92,20 @@ namespace euf {
expr* eq_proof_hint::get_hint(euf::solver& s) const {
ast_manager& m = s.get_manager();
func_decl_ref cc(m);
func_decl_ref cc(m), cc_comm(m);
sort* proof = m.mk_proof_sort();
ptr_buffer<sort> sorts;
expr_ref_vector args(m);
if (m_cc_head < m_cc_tail) {
sort* sorts[2] = { m.mk_bool_sort(), m.mk_bool_sort() };
cc = m.mk_func_decl(symbol("cc"), 2, sorts, proof);
sort* sorts[1] = { m.mk_bool_sort() };
cc_comm = m.mk_func_decl(symbol("comm"), 1, sorts, proof);
cc = m.mk_func_decl(symbol("cc"), 1, sorts, proof);
}
auto cc_proof = [&](bool comm, expr* eq) {
return m.mk_app(cc, m.mk_bool_val(comm), eq);
if (comm)
return m.mk_app(cc_comm, eq);
else
return m.mk_app(cc, eq);
};
auto compare_ts = [](cc_justification_record const& a,
cc_justification_record const& b) {
@ -168,11 +172,11 @@ namespace euf {
if (!visit_clause(out, n, lits))
return;
if (st.is_asserted())
display_redundant(out, n, lits, status2proof_hint(st));
display_inferred(out, n, lits, status2proof_hint(st));
else if (st.is_deleted())
display_deleted(out, n, lits);
else if (st.is_redundant())
display_redundant(out, n, lits, status2proof_hint(st));
display_inferred(out, n, lits, status2proof_hint(st));
else if (st.is_input())
display_assume(out, n, lits);
else
@ -228,10 +232,12 @@ namespace euf {
display_literals(out << "(assume", n, lits) << ")\n";
}
void solver::display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) {
if (proof_hint)
visit_expr(out, proof_hint);
display_hint(display_literals(out << "(learn", n, lits), proof_hint) << ")\n";
void solver::display_inferred(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) {
expr_ref hint(proof_hint, m);
if (!hint)
hint = m.mk_const(symbol("smt"), m.mk_proof_sort());
visit_expr(out, hint);
display_hint(display_literals(out << "(infer", n, lits), hint) << ")\n";
}
void solver::display_deleted(std::ostream& out, unsigned n, literal const* lits) {

44
src/sat/smt/euf_proof_checker.cpp
View file

@ -20,6 +20,7 @@ Author:
#include "ast/ast_ll_pp.h"
#include "sat/smt/euf_proof_checker.h"
#include "sat/smt/arith_proof_checker.h"
#include <iostream>
namespace euf {
@ -57,6 +58,7 @@ namespace euf {
ast_manager& m;
basic_union_find m_uf;
svector<std::pair<unsigned, unsigned>> m_expr2id;
ptr_vector<expr> m_id2expr;
svector<std::pair<expr*,expr*>> m_diseqs;
unsigned m_ts = 0;
@ -108,10 +110,10 @@ namespace euf {
if (ts != m_ts) {
id = m_uf.mk_var();
m_expr2id.setx(e->get_id(), {m_ts, id}, {0,0});
m_id2expr.setx(id, e, nullptr);
}
return id;
}
}
public:
eq_proof_checker(ast_manager& m): m(m) {}
@ -149,15 +151,17 @@ namespace euf {
if (!is_app(arg))
return false;
app* a = to_app(arg);
if (a->get_num_args() != 2)
if (a->get_num_args() != 1)
return false;
if (a->get_name() != symbol("cc"))
if (!m.is_eq(a->get_arg(0), x, y))
return false;
if (!m.is_eq(a->get_arg(1), x, y))
bool is_cc = a->get_name() == symbol("cc");
bool is_comm = a->get_name() == symbol("comm");
if (!is_cc && !is_comm)
return false;
if (!is_app(x) || !is_app(y))
return false;
if (!congruence(m.is_true(a->get_arg(0)), to_app(x), to_app(y))) {
if (!congruence(!is_cc, to_app(x), to_app(y))) {
IF_VERBOSE(0, verbose_stream() << "not congruent " << mk_pp(a, m) << "\n");
return false;
}
@ -167,9 +171,27 @@ namespace euf {
return false;
}
}
// check if a disequality is violated.
for (auto const& [a, b] : m_diseqs)
if (are_equal(a, b))
return true;
return true;
// check if some equivalence class contains two distinct values.
for (unsigned v = 0; v < m_uf.get_num_vars(); ++v) {
if (v != m_uf.find(v))
continue;
unsigned r = v;
expr* val = nullptr;
do {
expr* e = m_id2expr[v];
if (val && m.are_distinct(e, val))
return true;
if (m.is_value(e))
val = e;
v = m_uf.next(v);
}
while (r != v);
}
return false;
}
@ -201,8 +223,12 @@ namespace euf {
units.reset();
app* a = to_app(e);
proof_checker_plugin* p = nullptr;
if (m_map.find(a->get_decl()->get_name(), p))
return p->check(clause, a, units);
if (!m_map.find(a->get_decl()->get_name(), p))
return false;
if (p->check(clause, a, units))
return true;
std::cout << "(missed-hint " << mk_pp(e, m) << ")\n";
return false;
}

2
src/sat/smt/euf_solver.h
View file

@ -197,7 +197,7 @@ namespace euf {
void on_proof(unsigned n, literal const* lits, sat::status st);
std::ostream& display_literals(std::ostream& out, unsigned n, sat::literal const* lits);
void display_assume(std::ostream& out, unsigned n, literal const* lits);
void display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint);
void display_inferred(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint);
void display_deleted(std::ostream& out, unsigned n, literal const* lits);
std::ostream& display_hint(std::ostream& out, expr* proof_hint);
expr_ref status2proof_hint(sat::status st);

2
src/sat/smt/q_ematch.cpp
View file

@ -387,7 +387,7 @@ namespace q {
m_qs.log_instantiation(lits, &j);
euf::th_proof_hint* ph = nullptr;
if (ctx.use_drat())
ph = q_proof_hint::mk(ctx, j.m_clause.size(), j.m_binding);
ph = q_proof_hint::mk(ctx, lits, j.m_clause.size(), j.m_binding);
m_qs.add_clause(lits, ph);
}

17
src/sat/smt/q_mbi.cpp
View file

@ -70,19 +70,10 @@ namespace q {
m_max_cex += ctx.get_config().m_mbqi_max_cexs;
for (auto const& [qlit, fml, inst, generation] : m_instantiations) {
euf::solver::scoped_generation sg(ctx, generation + 1);
sat::literal lit = ctx.mk_literal(fml);
euf::th_proof_hint* ph = nullptr;
if (!inst.empty()) {
ph = q_proof_hint::mk(ctx, inst.size(), inst.data());
sat::literal_vector lits;
lits.push_back(~qlit);
lits.push_back(~lit);
m_qs.add_clause(lits, ph);
}
else {
m_qs.add_clause(~qlit, ~lit);
}
m_qs.log_instantiation(~qlit, ~lit);
sat::literal lit = ~ctx.mk_literal(fml);
auto* ph = q_proof_hint::mk(ctx, ~qlit, lit, inst.size(), inst.data());
m_qs.add_clause(~qlit, lit, ph);
m_qs.log_instantiation(~qlit, lit);
}
m_instantiations.reset();
if (result != l_true)

45
src/sat/smt/q_solver.cpp
View file

@ -364,36 +364,49 @@ namespace q {
}
}
q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned n, euf::enode* const* bindings) {
auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n));
q_proof_hint* ph = new (mem) q_proof_hint();
ph->m_num_bindings = n;
q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings) {
auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, lits.size()));
q_proof_hint* ph = new (mem) q_proof_hint(n, lits.size());
for (unsigned i = 0; i < n; ++i)
ph->m_bindings[i] = bindings[i]->get_expr();
for (unsigned i = 0; i < lits.size(); ++i)
ph->m_literals[i] = lits[i];
return ph;
}
q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned n, expr* const* bindings) {
auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n));
q_proof_hint* ph = new (mem) q_proof_hint();
ph->m_num_bindings = n;
q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings) {
auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, 2));
q_proof_hint* ph = new (mem) q_proof_hint(n, 2);
for (unsigned i = 0; i < n; ++i)
ph->m_bindings[i] = bindings[i];
ph->m_literals[0] = l1;
ph->m_literals[1] = l2;
return ph;
}
expr* q_proof_hint::get_hint(euf::solver& s) const {
ast_manager& m = s.get_manager();
expr_ref_vector args(m);
sort_ref_vector sorts(m);
for (unsigned i = 0; i < m_num_bindings; ++i) {
args.push_back(m_bindings[i]);
sorts.push_back(args.back()->get_sort());
}
ptr_buffer<sort> sorts;
expr_ref binding(m);
sort* range = m.mk_proof_sort();
func_decl* d = m.mk_func_decl(symbol("inst"), args.size(), sorts.data(), range);
expr* r = m.mk_app(d, args);
return r;
func_decl* d;
for (unsigned i = 0; i < m_num_bindings; ++i)
args.push_back(m_bindings[i]);
for (expr* arg : args)
sorts.push_back(arg->get_sort());
d = m.mk_func_decl(symbol("bind"), args.size(), sorts.data(), range);
binding = m.mk_app(d, args);
args.reset();
sorts.reset();
for (unsigned i = 0; i < m_num_literals; ++i)
args.push_back(s.literal2expr(~m_literals[i]));
args.push_back(binding);
for (expr* arg : args)
sorts.push_back(arg->get_sort());
d = m.mk_func_decl(symbol("inst"), args.size(), sorts.data(), range);
return m.mk_app(d, args);
}
}

19
src/sat/smt/q_solver.h
View file

@ -30,12 +30,19 @@ namespace euf {
namespace q {
struct q_proof_hint : public euf::th_proof_hint {
unsigned m_num_bindings;
expr* m_bindings[0];
q_proof_hint() {}
static size_t get_obj_size(unsigned num_bindings) { return sizeof(q_proof_hint) + num_bindings*sizeof(expr*); }
static q_proof_hint* mk(euf::solver& s, unsigned n, euf::enode* const* bindings);
static q_proof_hint* mk(euf::solver& s, unsigned n, expr* const* bindings);
unsigned m_num_bindings;
unsigned m_num_literals;
sat::literal* m_literals;
expr* m_bindings[0];
q_proof_hint(unsigned b, unsigned l) {
m_num_bindings = b;
m_num_literals = l;
m_literals = reinterpret_cast<sat::literal*>(m_bindings + m_num_bindings);
}
static size_t get_obj_size(unsigned num_bindings, unsigned num_lits) { return sizeof(q_proof_hint) + num_bindings*sizeof(expr*) + num_lits*sizeof(sat::literal); }
static q_proof_hint* mk(euf::solver& s, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings);
static q_proof_hint* mk(euf::solver& s, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings);
expr* get_hint(euf::solver& s) const override;
};

15
src/sat/smt/sat_th.cpp
View file

@ -143,20 +143,16 @@ namespace euf {
is_new = true;
return is_new;
}
bool th_euf_solver::add_clause(sat::literal a, sat::literal b) {
sat::literal lits[2] = { a, b };
return add_clause(2, lits);
}
bool th_euf_solver::add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps) {
bool th_euf_solver::add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps) {
SASSERT(ps);
sat::literal lits[2] = { a, b };
return add_clause(2, lits, ps);
}
bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) {
bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, th_proof_hint const* ps) {
sat::literal lits[3] = { a, b, c };
return add_clause(3, lits);
return add_clause(3, lits, ps);
}
bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) {
@ -165,6 +161,7 @@ namespace euf {
}
bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) {
//SASSERT(!ctx.use_drat() || ps); - very far from true, and isn't a requirement
bool was_true = false;
for (unsigned i = 0; i < n; ++i)
was_true |= is_true(lits[i]);

5
src/sat/smt/sat_th.h
View file

@ -160,9 +160,8 @@ namespace euf {
bool add_unit(sat::literal lit);
bool add_units(sat::literal_vector const& lits);
bool add_clause(sat::literal lit) { return add_unit(lit); }
bool add_clause(sat::literal a, sat::literal b);
bool add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps);
bool add_clause(sat::literal a, sat::literal b, sat::literal c);
bool add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps = nullptr);
bool add_clause(sat::literal a, sat::literal b, sat::literal c, th_proof_hint const* ps = nullptr);
bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d);
bool add_clause(sat::literal_vector const& lits, th_proof_hint const* ps = nullptr) { return add_clause(lits.size(), lits.data(), ps); }
bool add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps = nullptr);