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

overhaul of proof format for new solver

Browse source 
This commit overhauls the proof format (in development) for the new core.

NOTE: this functionality is work in progress with a long way to go.
It is shielded by the sat.euf option, which is off by default and in pre-release state.
It is too early to fuzz or use it. It is pushed into master to shed light on road-map for certifying inferences of sat.euf.

It retires the ad-hoc extension of DRUP used by the SAT solver.
Instead it relies on SMT with ad-hoc extensions for proof terms.
It adds the following commands (consumed by proof_cmds.cpp):

- assume  - for input clauses
- learn   - when a clause is learned (or redundant clause is added)
- del     - when a clause is deleted.

The commands take a list of expressions of type Bool and the
last argument can optionally be of type Proof.
When the last argument is of type Proof it is provided as a hint
to justify the learned clause.

Proof hints can be checked using a self-contained proof
checker. The sat/smt/euf_proof_checker.h class provides
a plugin dispatcher for checkers.
It is instantiated with a checker for arithmetic lemmas,
so far for Farkas proofs.

Use example:
```
(set-option :sat.euf true)
(set-option :tactic.default_tactic smt)
(set-option :sat.smt.proof f.proof)
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(assert (< x y))
(assert (< y z))
(assert (< z x))
(check-sat)
```

Run z3 on a file with above content.
Then run z3 on f.proof

```
(verified-smt)
(verified-smt)
(verified-smt)
(verified-farkas)
(verified-smt)
```
This commit is contained in:
Nikolaj Bjorner 2022-08-28 17:44:33 -07:00
parent 9922c766b9
commit e2f4fc2307
37 changed files with 809 additions and 1078 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -21,130 +21,21 @@ Author:
namespace euf {
void solver::init_drat() {
if (!m_drat_initialized) {
void solver::init_proof() {
if (!m_proof_initialized) {
get_drat().add_theory(get_id(), symbol("euf"));
get_drat().add_theory(m.get_basic_family_id(), symbol("bool"));
}
m_drat_initialized = true;
}
void solver::def_add_arg(unsigned arg) {
auto* out = get_drat().out();
if (out)
(*out) << " " << arg;
}
void solver::def_end() {
auto* out = get_drat().out();
if (out)
(*out) << " 0\n";
}
void solver::def_begin(char id, unsigned n, std::string const& name) {
auto* out = get_drat().out();
if (out)
(*out) << id << " " << n << " " << name;
}
void solver::bool_def(bool_var v, unsigned n) {
auto* out = get_drat().out();
if (out)
(*out) << "b " << v << " " << n << " 0\n";
}
void solver::drat_log_params(func_decl* f) {
for (unsigned i = f->get_num_parameters(); i-- > 0; ) {
auto const& p = f->get_parameter(i);
if (!p.is_ast())
continue;
ast* a = p.get_ast();
if (is_func_decl(a))
drat_log_decl(to_func_decl(a));
if (!m_proof_out && s().get_config().m_drat &&
(get_config().m_lemmas2console || s().get_config().m_smt_proof.is_non_empty_string())) {
TRACE("euf", tout << "init-proof\n");
m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out);
if (get_config().m_lemmas2console)
get_drat().set_clause_eh(*this);
if (s().get_config().m_smt_proof.is_non_empty_string())
get_drat().set_clause_eh(*this);
}
}
void solver::drat_log_expr1(expr* e) {
if (is_app(e)) {
app* a = to_app(e);
drat_log_params(a->get_decl());
drat_log_decl(a->get_decl());
std::stringstream strm;
strm << mk_ismt2_func(a->get_decl(), m);
def_begin('e', e->get_id(), strm.str());
for (expr* arg : *a)
def_add_arg(arg->get_id());
def_end();
}
else if (is_var(e)) {
var* v = to_var(e);
def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
def_add_arg(v->get_idx());
def_end();
}
else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
std::stringstream strm;
strm << "(" << (is_forall(q) ? "forall" : (is_exists(q) ? "exists" : "lambda"));
for (unsigned i = 0; i < q->get_num_decls(); ++i)
strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";
strm << ")";
def_begin('q', q->get_id(), strm.str());
def_add_arg(q->get_expr()->get_id());
def_end();
}
else
UNREACHABLE();
m_drat_asts.insert(e);
push(insert_obj_trail<ast>(m_drat_asts, e));
}
void solver::drat_log_expr(expr* e) {
if (m_drat_asts.contains(e))
return;
ptr_vector<expr>::scoped_stack _sc(m_drat_todo);
m_drat_todo.push_back(e);
while (!m_drat_todo.empty()) {
e = m_drat_todo.back();
unsigned sz = m_drat_todo.size();
if (is_app(e))
for (expr* arg : *to_app(e))
if (!m_drat_asts.contains(arg))
m_drat_todo.push_back(arg);
if (is_quantifier(e)) {
expr* arg = to_quantifier(e)->get_expr();
if (!m_drat_asts.contains(arg))
m_drat_todo.push_back(arg);
}
if (m_drat_todo.size() != sz)
continue;
if (!m_drat_asts.contains(e))
drat_log_expr1(e);
m_drat_todo.pop_back();
}
}
void solver::drat_bool_def(sat::bool_var v, expr* e) {
if (!use_drat())
return;
drat_log_expr(e);
bool_def(v, e->get_id());
}
void solver::drat_log_decl(func_decl* f) {
if (f->get_family_id() != null_family_id)
return;
if (m_drat_asts.contains(f))
return;
m_drat_asts.insert(f);
push(insert_obj_trail< ast>(m_drat_asts, f));
std::ostringstream strm;
smt2_pp_environment_dbg env(m);
ast_smt2_pp(strm, f, env);
def_begin('f', f->get_small_id(), strm.str());
def_end();
m_proof_initialized = true;
}
/**
@ -183,16 +74,19 @@ namespace euf {
}
}
void solver::set_tmp_bool_var(bool_var b, expr* e) {
m_bool_var2expr.setx(b, e, nullptr);
}
void solver::log_justification(literal l, th_explain const& jst) {
literal_vector lits;
unsigned nv = s().num_vars();
expr_ref_vector eqs(m);
unsigned nv = s().num_vars();
auto add_lit = [&](enode_pair const& eq) {
++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());
return lit;
set_tmp_bool_var(nv, eqs.back());
return literal(nv, false);
};
for (auto lit : euf::th_explain::lits(jst))
@ -208,68 +102,133 @@ namespace euf {
get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id(), jst.get_pragma()));
}
void solver::drat_eq_def(literal lit, expr* eq) {
expr *a = nullptr, *b = nullptr;
VERIFY(m.is_eq(eq, a, b));
drat_log_expr(a);
drat_log_expr(b);
def_begin('e', eq->get_id(), std::string("="));
def_add_arg(a->get_id());
def_add_arg(b->get_id());
def_end();
bool_def(lit.var(), eq->get_id());
void solver::on_clause(unsigned n, literal const* lits, sat::status st) {
TRACE("euf", tout << "on-clause " << n << "\n");
on_lemma(n, lits, st);
on_proof(n, lits, st);
}
void solver::on_clause(unsigned n, literal const* lits, sat::status st) {
void solver::on_proof(unsigned n, literal const* lits, sat::status st) {
if (!m_proof_out)
return;
flet<bool> _display_all_decls(m_display_all_decls, true);
std::ostream& out = *m_proof_out;
if (!visit_clause(out, n, lits))
return;
if (st.is_asserted())
display_redundant(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));
else if (st.is_input())
display_assume(out, n, lits);
else
UNREACHABLE();
out.flush();
}
void solver::on_lemma(unsigned n, literal const* lits, sat::status st) {
if (!get_config().m_lemmas2console)
return;
if (!st.is_redundant() && !st.is_asserted())
return;
if (!visit_clause(n, lits))
std::ostream& out = std::cout;
if (!visit_clause(out, n, lits))
return;
std::function<symbol(int)> ppth = [&](int th) {
return m.get_family_name(th);
};
if (!st.is_sat())
std::cout << "; " << sat::status_pp(st, ppth) << "\n";
out << "; " << sat::status_pp(st, ppth) << "\n";
display_clause(n, lits);
display_assert(out, n, lits);
}
void solver::on_instantiation(unsigned n, sat::literal const* lits, unsigned k, euf::enode* const* bindings) {
std::ostream& out = std::cout;
for (unsigned i = 0; i < k; ++i)
visit_expr(out, bindings[i]->get_expr());
VERIFY(visit_clause(out, n, lits));
out << "(instantiate";
display_literals(out, n, lits);
for (unsigned i = 0; i < k; ++i)
display_expr(out << " :binding ", bindings[i]->get_expr());
out << ")\n";
}
bool solver::visit_clause(unsigned n, literal const* lits) {
bool solver::visit_clause(std::ostream& out, unsigned n, literal const* lits) {
for (unsigned i = 0; i < n; ++i) {
expr* e = bool_var2expr(lits[i].var());
if (!e)
return false;
visit_expr(e);
visit_expr(out, e);
}
return true;
}
void solver::display_clause(unsigned n, literal const* lits) {
std::cout << "(assert (or";
void solver::display_assert(std::ostream& out, unsigned n, literal const* lits) {
display_literals(out << "(assert (or", n, lits) << "))\n";
}
void solver::display_assume(std::ostream& out, unsigned n, literal const* lits) {
display_literals(out << "(assume", n, lits) << ")\n";
}
void solver::display_redundant(std::ostream& out, unsigned n, literal const* lits, expr_ref& proof_hint) {
if (proof_hint)
visit_expr(out, proof_hint);
display_hint(display_literals(out << "(learn", n, lits), proof_hint) << ")\n";
}
void solver::display_deleted(std::ostream& out, unsigned n, literal const* lits) {
display_literals(out << "(del", n, lits) << ")\n";
}
std::ostream& solver::display_hint(std::ostream& out, expr* proof_hint) {
if (proof_hint)
return display_expr(out << " ", proof_hint);
else
return out;
}
expr_ref solver::status2proof_hint(sat::status st) {
if (st.is_sat())
return expr_ref(m.mk_const("rup", m.mk_proof_sort()), m); // provable by reverse unit propagation
auto* h = reinterpret_cast<euf::th_proof_hint const*>(st.get_hint());
if (!h)
return expr_ref(m);
expr* e = h->get_hint(*this);
if (e)
return expr_ref(e, m);
return expr_ref(m);
}
std::ostream& solver::display_literals(std::ostream& out, unsigned n, literal const* lits) {
for (unsigned i = 0; i < n; ++i) {
expr* e = bool_var2expr(lits[i].var());
if (lits[i].sign())
m_clause_visitor.display_expr_def(std::cout << " (not ", e) << ")";
display_expr(out << " (not ", e) << ")";
else
m_clause_visitor.display_expr_def(std::cout << " ", e);
display_expr(out << " ", e);
}
std::cout << "))\n";
return out;
}
void solver::visit_expr(expr* e) {
void solver::visit_expr(std::ostream& out, expr* e) {
m_clause_visitor.collect(e);
m_clause_visitor.display_skolem_decls(std::cout);
m_clause_visitor.define_expr(std::cout, e);
if (m_display_all_decls)
m_clause_visitor.display_decls(out);
else
m_clause_visitor.display_skolem_decls(out);
m_clause_visitor.define_expr(out, e);
}
void solver::display_expr(expr* e) {
m_clause_visitor.display_expr_def(std::cout, e);
std::ostream& solver::display_expr(std::ostream& out, expr* e) {
return m_clause_visitor.display_expr_def(out, e);
}
}