mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

adding q proof hints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-07 19:21:12 +02:00
parent 661a1624b4
commit 35639c5ac0
8 changed files with 71 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/cmd_context/extra_cmds/proof_cmds.cpp
View file

@ -152,6 +152,14 @@ public:
}
}
// extract a simplified verification condition in case proof validation does not work.
// quantifier instantiation can be validated as follows:
// If quantifier instantiation claims that (forall x . phi(x)) => psi using instantiation x -> t
// then check the simplified VC: phi(t) => psi.
// in case psi is the literal instantiation, then the clause is a propositional tautology.
// The VC function is a no-op if the proof hint does not have an associated vc generator.
m_checker.vc(proof_hint, clause);
m_solver->push();
for (expr* lit : clause)
m_solver->assert_expr(m.mk_not(lit));

6
src/sat/sat_proof_trim.cpp
View file

@ -40,10 +40,10 @@ namespace sat {
revive(cl, clp);
continue;
}
IF_VERBOSE(0, s.display(verbose_stream()));
IF_VERBOSE(10, s.display(verbose_stream()));
prune_trail(cl, clp);
IF_VERBOSE(0, verbose_stream() << cl << " " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} ");
IF_VERBOSE(0, s.display(verbose_stream() << "\n"));
IF_VERBOSE(10, verbose_stream() << cl << " " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} ");
IF_VERBOSE(10, s.display(verbose_stream() << "\n"));
del(cl, clp);
if (!in_core(cl, clp))
continue;

1
src/sat/smt/CMakeLists.txt
View file

@ -36,6 +36,7 @@ z3_add_component(sat_smt
q_mam.cpp
q_mbi.cpp
q_model_fixer.cpp
q_proof_checker.cpp
q_queue.cpp
q_solver.cpp
recfun_solver.cpp

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

@ -103,14 +103,18 @@ namespace dt {
*/
void solver::assert_eq_axiom(enode* n1, expr* e2, literal antecedent) {
expr* e1 = n1->get_expr();
euf::th_proof_hint* ph = nullptr;
if (ctx.use_drat()) {
// todo
}
if (antecedent == sat::null_literal)
add_unit(eq_internalize(e1, e2));
add_unit(eq_internalize(e1, e2), ph);
else if (s().value(antecedent) == l_true) {
euf::enode* n2 = e_internalize(e2);
ctx.propagate(n1, n2, euf::th_explain::propagate(*this, antecedent, n1, n2));
ctx.propagate(n1, n2, euf::th_explain::propagate(*this, antecedent, n1, n2, ph));
}
else
add_clause(~antecedent, eq_internalize(e1, e2));
add_clause(~antecedent, eq_internalize(e1, e2), ph);
}
/**

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

@ -21,6 +21,7 @@ Author:
#include "ast/ast_ll_pp.h"
#include "sat/smt/euf_proof_checker.h"
#include "sat/smt/arith_proof_checker.h"
#include "sat/smt/q_proof_checker.h"
#include <iostream>
namespace euf {
@ -240,7 +241,7 @@ namespace euf {
return false;
return pc.check(proof1) && pc.check(proof2);
}
expr_ref_vector clause(app* jst) override {
expr_ref_vector result(m);
auto x = jst->args3();
@ -272,6 +273,7 @@ namespace euf {
add_plugin(alloc(arith::proof_checker, m));
add_plugin(alloc(eq_proof_checker, m));
add_plugin(alloc(res_proof_checker, m, *this));
add_plugin(alloc(q::proof_checker, m));
}
proof_checker::~proof_checker() {
@ -290,8 +292,7 @@ namespace euf {
bool proof_checker::check(expr* e) {
if (m_checked_clauses.contains(e))
return true;
return true;
if (!e || !is_app(e))
return false;
app* a = to_app(e);
@ -309,12 +310,17 @@ namespace euf {
expr_ref_vector* rr;
if (m_checked_clauses.find(e, rr))
return *rr;
SASSERT(is_app(e) && m_map.contains(to_app(e)->get_decl()->get_name()));
expr_ref_vector r = m_map[to_app(e)->get_decl()->get_name()]->clause(to_app(e));
SASSERT(is_app(e) && m_map.contains(to_app(e)->get_name()));
expr_ref_vector r = m_map[to_app(e)->get_name()]->clause(to_app(e));
m_checked_clauses.insert(e, alloc(expr_ref_vector, r));
return r;
}
void proof_checker::vc(expr* e, expr_ref_vector& clause) {
SASSERT(is_app(e) && m_map.contains(to_app(e)->get_name()));
m_map[to_app(e)->get_name()]->vc(to_app(e), clause);
}
bool proof_checker::check(expr_ref_vector const& clause1, expr* e, expr_ref_vector & units) {
if (!check(e))
return false;

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

@ -30,6 +30,7 @@ namespace euf {
virtual bool check(app* jst) = 0;
virtual expr_ref_vector clause(app* jst) = 0;
virtual void register_plugins(proof_checker& pc) = 0;
virtual void vc(app* jst, expr_ref_vector& clause) { }
};
class proof_checker {
@ -44,6 +45,7 @@ namespace euf {
void register_plugin(symbol const& rule, proof_checker_plugin*);
bool check(expr* jst);
expr_ref_vector clause(expr* jst);
void vc(expr* jst, expr_ref_vector& clause);
bool check(expr_ref_vector const& clause, expr* e, expr_ref_vector& units);
};

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

@ -129,9 +129,9 @@ namespace euf {
return sat::status::th(m_is_redundant, get_id(), ps);
}
bool th_euf_solver::add_unit(sat::literal lit) {
bool th_euf_solver::add_unit(sat::literal lit, th_proof_hint const* ps) {
bool was_true = is_true(lit);
ctx.s().add_clause(1, &lit, mk_status());
ctx.s().add_clause(1, &lit, mk_status(ps));
ctx.add_root(lit);
return !was_true;
}
@ -155,9 +155,9 @@ namespace euf {
return add_clause(3, lits, ps);
}
bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) {
bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d, th_proof_hint const* ps) {
sat::literal lits[4] = { a, b, c, d };
return add_clause(4, lits);
return add_clause(4, lits, ps);
}
bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) {
@ -251,46 +251,46 @@ namespace euf {
return new (sat::constraint_base::ptr2mem(mem)) th_explain(n_lits, lits, n_eqs, eqs, c, enode_pair(x, y), pma);
}
th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* pma) {
return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), consequent, nullptr, nullptr, pma);
th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* ph) {
return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), consequent, nullptr, nullptr, ph);
}
th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma) {
return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), sat::null_literal, x, y, pma);
th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* ph) {
return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), sat::null_literal, x, y, ph);
}
th_explain* th_explain::propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma) {
return mk(th, 0, nullptr, eqs.size(), eqs.data(), sat::null_literal, x, y, pma);
th_explain* th_explain::propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* ph) {
return mk(th, 0, nullptr, eqs.size(), eqs.data(), sat::null_literal, x, y, ph);
}
th_explain* th_explain::propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) {
return mk(th, 1, &lit, 0, nullptr, sat::null_literal, x, y);
th_explain* th_explain::propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y, th_proof_hint const* ph) {
return mk(th, 1, &lit, 0, nullptr, sat::null_literal, x, y, ph);
}
th_explain* th_explain::conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs) {
return conflict(th, lits.size(), lits.data(), eqs.size(), eqs.data());
th_explain* th_explain::conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, th_proof_hint const* ph) {
return conflict(th, lits.size(), lits.data(), eqs.size(), eqs.data(), ph);
}
th_explain* th_explain::conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) {
return mk(th, n_lits, lits, n_eqs, eqs, sat::null_literal, nullptr, nullptr);
th_explain* th_explain::conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, th_proof_hint const* ph) {
return mk(th, n_lits, lits, n_eqs, eqs, sat::null_literal, nullptr, nullptr, ph);
}
th_explain* th_explain::conflict(th_euf_solver& th, enode_pair_vector const& eqs) {
return conflict(th, 0, nullptr, eqs.size(), eqs.data());
th_explain* th_explain::conflict(th_euf_solver& th, enode_pair_vector const& eqs, th_proof_hint const* ph) {
return conflict(th, 0, nullptr, eqs.size(), eqs.data(), ph);
}
th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit) {
return conflict(th, 1, &lit, 0, nullptr);
th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit, th_proof_hint const* ph) {
return conflict(th, 1, &lit, 0, nullptr, ph);
}
th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) {
th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y, th_proof_hint const* ph) {
enode_pair eq(x, y);
return conflict(th, 1, &lit, 1, &eq);
return conflict(th, 1, &lit, 1, &eq, ph);
}
th_explain* th_explain::conflict(th_euf_solver& th, euf::enode* x, euf::enode* y) {
th_explain* th_explain::conflict(th_euf_solver& th, euf::enode* x, euf::enode* y, th_proof_hint const* ph) {
enode_pair eq(x, y);
return conflict(th, 0, nullptr, 1, &eq);
return conflict(th, 0, nullptr, 1, &eq, ph);
}
std::ostream& th_explain::display(std::ostream& out) const {

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

@ -157,12 +157,12 @@ namespace euf {
sat::status mk_status(th_proof_hint const* ps = nullptr);
bool add_unit(sat::literal lit);
bool add_unit(sat::literal lit, th_proof_hint const* ps = nullptr);
bool add_units(sat::literal_vector const& lits);
bool add_clause(sat::literal lit) { return add_unit(lit); }
bool add_clause(sat::literal lit, th_proof_hint const* ps = nullptr) { return add_unit(lit, ps); }
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 a, sat::literal b, sat::literal c, sat::literal d, th_proof_hint const* ps = nullptr);
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);
void add_equiv(sat::literal a, sat::literal b);
@ -233,21 +233,21 @@ namespace euf {
sat::literal* m_literals;
enode_pair* m_eqs;
static size_t get_obj_size(unsigned num_lits, unsigned num_eqs);
th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq, th_proof_hint const* pma = nullptr);
static th_explain* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y, th_proof_hint const* pma = nullptr);
th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq, th_proof_hint const* ph = nullptr);
static th_explain* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y, th_proof_hint const* ph = nullptr);
public:
static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs);
static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, th_proof_hint const* ph = nullptr);
static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits) { return conflict(th, lits.size(), lits.data(), 0, nullptr); }
static th_explain* conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs);
static th_explain* conflict(th_euf_solver& th, enode_pair_vector const& eqs);
static th_explain* conflict(th_euf_solver& th, sat::literal lit);
static th_explain* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
static th_explain* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y);
static th_explain* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
static th_explain* propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma = nullptr);
static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* pma = nullptr);
static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma = nullptr);
static th_explain* conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, th_proof_hint const* ph = nullptr);
static th_explain* conflict(th_euf_solver& th, enode_pair_vector const& eqs, th_proof_hint const* ph = nullptr);
static th_explain* conflict(th_euf_solver& th, sat::literal lit, th_proof_hint const* ph = nullptr);
static th_explain* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr);
static th_explain* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr);
static th_explain* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr);
static th_explain* propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr);
static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* ph = nullptr);
static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr);
sat::ext_constraint_idx to_index() const {
return sat::constraint_base::mem2base(this);