mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
wip - proof checker
This commit is contained in:
parent
ace727ee0f
commit
a2e0646eed
|
@ -42,6 +42,7 @@ Proof checker for clauses created during search.
|
|||
|
||||
#include "util/small_object_allocator.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "smt/smt_solver.h"
|
||||
#include "sat/sat_solver.h"
|
||||
#include "sat/sat_drat.h"
|
||||
|
@ -181,9 +182,9 @@ public:
|
|||
}
|
||||
m_solver->pop(1);
|
||||
std::cout << "(verified-smt";
|
||||
if (proof_hint) std::cout << " " << mk_pp(proof_hint, m);
|
||||
if (proof_hint) std::cout << " " << mk_bounded_pp(proof_hint, m, 4);
|
||||
for (expr* arg : clause)
|
||||
std::cout << " " << mk_pp(arg, m);
|
||||
std::cout << " " << mk_bounded_pp(arg, m);
|
||||
std::cout << ")\n";
|
||||
add_clause(clause);
|
||||
}
|
||||
|
|
|
@ -293,17 +293,13 @@ namespace euf {
|
|||
}
|
||||
|
||||
bool proof_checker::check(expr* e) {
|
||||
if (m_checked_clauses.contains(e))
|
||||
return true;
|
||||
if (!e || !is_app(e))
|
||||
return false;
|
||||
if (m_checked_clauses.contains(e))
|
||||
return true;
|
||||
app* a = to_app(e);
|
||||
proof_checker_plugin* p = nullptr;
|
||||
if (!m_map.find(a->get_decl()->get_name(), p))
|
||||
return false;
|
||||
if (!p->check(a))
|
||||
return false;
|
||||
return true;
|
||||
return m_map.find(a->get_decl()->get_name(), p) && p->check(a);
|
||||
}
|
||||
|
||||
expr_ref_vector proof_checker::clause(expr* e) {
|
||||
|
|
|
@ -234,9 +234,15 @@ namespace tseitin {
|
|||
bool proof_checker::equiv(expr* a, expr* b) {
|
||||
if (a == b)
|
||||
return true;
|
||||
expr* x, *y, *z, *u;
|
||||
if (m.is_eq(a, x, y) && m.is_eq(b, z, u))
|
||||
return x == u && y == z;
|
||||
return false;
|
||||
if (!is_app(a) || !is_app(b))
|
||||
return false;
|
||||
if (to_app(a)->get_decl() != to_app(b)->get_decl())
|
||||
return false;
|
||||
if (!to_app(a)->get_decl()->is_commutative())
|
||||
return false;
|
||||
if (to_app(a)->get_num_args() != 2)
|
||||
return false;
|
||||
return to_app(a)->get_arg(0) == to_app(b)->get_arg(1) &&
|
||||
to_app(a)->get_arg(1) == to_app(b)->get_arg(0);
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue