mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Add RUP checking mode to proof checker.
This commit is contained in:
parent
8cb118235a
commit
0f475f45b5
|
@ -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 <iostream>
|
||||
|
||||
|
@ -37,31 +37,68 @@ class smt_checker {
|
|||
|
||||
scoped_ptr<solver> 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) {}
|
||||
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue