mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

proof-checker: replace match_negated with ast_manager::is_complement

Browse source 
is_complement matches true and false, while match_negated does not

Necessary to handle uses of true-axiom
This commit is contained in:
Arie Gurfinkel 2018-05-21 10:45:07 -07:00
parent 9550fd1ec4
commit 6514741e3f
1 changed files with 74 additions and 75 deletions
Download patch file Download diff file Expand all files Collapse all files

149
src/ast/proofs/proof_checker.cpp
View file

@ -1,4 +1,3 @@
/*++ /*++
Copyright (c) 2015 Microsoft Corporation Copyright (c) 2015 Microsoft Corporation
@ -16,7 +15,7 @@ Copyright (c) 2015 Microsoft Corporation
#define SAME_OP(_d1_, _d2_) ((_d1_ == _d2_) || (IS_EQUIV(_d1_) && IS_EQUIV(_d2_))) #define SAME_OP(_d1_, _d2_) ((_d1_ == _d2_) || (IS_EQUIV(_d1_) && IS_EQUIV(_d2_)))
proof_checker::hyp_decl_plugin::hyp_decl_plugin() : proof_checker::hyp_decl_plugin::hyp_decl_plugin() :
m_cons(nullptr), m_cons(nullptr),
m_atom(nullptr), m_atom(nullptr),
m_nil(nullptr), m_nil(nullptr),
@ -59,13 +58,13 @@ func_decl * proof_checker::hyp_decl_plugin::mk_func_decl(decl_kind k) {
} }
func_decl * proof_checker::hyp_decl_plugin::mk_func_decl( func_decl * proof_checker::hyp_decl_plugin::mk_func_decl(
decl_kind k, unsigned num_parameters, parameter const * parameters, decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) { unsigned arity, sort * const * domain, sort * range) {
return mk_func_decl(k); return mk_func_decl(k);
} }
func_decl * proof_checker::hyp_decl_plugin::mk_func_decl( func_decl * proof_checker::hyp_decl_plugin::mk_func_decl(
decl_kind k, unsigned num_parameters, parameter const * parameters, decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) { unsigned num_args, expr * const * args, sort * range) {
return mk_func_decl(k); return mk_func_decl(k);
} }
@ -84,7 +83,7 @@ void proof_checker::hyp_decl_plugin::get_sort_names(svector<builtin_name> & sort
} }
} }
proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m), proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m),
m_dump_lemmas(false), m_logic("AUFLIA"), m_proof_lemma_id(0) { m_dump_lemmas(false), m_logic("AUFLIA"), m_proof_lemma_id(0) {
symbol fam_name("proof_hypothesis"); symbol fam_name("proof_hypothesis");
if (!m.has_plugin(fam_name)) { if (!m.has_plugin(fam_name)) {
@ -98,16 +97,16 @@ proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pi
bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) { bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
proof_ref curr(m); proof_ref curr(m);
m_todo.push_back(p); m_todo.push_back(p);
bool result = true; bool result = true;
while (result && !m_todo.empty()) { while (result && !m_todo.empty()) {
curr = m_todo.back(); curr = m_todo.back();
m_todo.pop_back(); m_todo.pop_back();
result = check1(curr.get(), side_conditions); result = check1(curr.get(), side_conditions);
if (!result) { if (!result) {
IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get());); IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get()););
UNREACHABLE(); UNREACHABLE();
} }
} }
m_hypotheses.reset(); m_hypotheses.reset();
@ -157,10 +156,10 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
} }
return false; return false;
} }
case PR_SPC_REWRITE: case PR_SPC_REWRITE:
case PR_SUPERPOSITION: case PR_SUPERPOSITION:
case PR_EQUALITY_RESOLUTION: case PR_EQUALITY_RESOLUTION:
case PR_SPC_RESOLUTION: case PR_SPC_RESOLUTION:
case PR_FACTORING: case PR_FACTORING:
case PR_SPC_DER: { case PR_SPC_DER: {
if (match_fact(p, fact)) { if (match_fact(p, fact)) {
@ -176,7 +175,7 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
side_conditions.push_back(rewrite_cond.get()); side_conditions.push_back(rewrite_cond.get());
return true; return true;
} }
return false; return false;
} }
default: default:
UNREACHABLE(); UNREACHABLE();
@ -201,7 +200,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
func_decl_ref f1(m), f2(m); func_decl_ref f1(m), f2(m);
expr_ref_vector terms1(m), terms2(m), terms(m); expr_ref_vector terms1(m), terms2(m), terms(m);
sort_ref_vector decls1(m), decls2(m); sort_ref_vector decls1(m), decls2(m);
if (match_proof(p, proofs)) { if (match_proof(p, proofs)) {
for (unsigned i = 0; i < proofs.size(); ++i) { for (unsigned i = 0; i < proofs.size(); ++i) {
add_premise(proofs.get(i)); add_premise(proofs.get(i));
@ -231,8 +230,8 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
return false; return false;
} }
case PR_REFLEXIVITY: { case PR_REFLEXIVITY: {
if (match_fact(p, fact) && if (match_fact(p, fact) &&
match_proof(p) && match_proof(p) &&
(match_equiv(fact, t1, t2) || match_oeq(fact, t1, t2)) && (match_equiv(fact, t1, t2) || match_oeq(fact, t1, t2)) &&
(t1.get() == t2.get())) { (t1.get() == t2.get())) {
return true; return true;
@ -245,7 +244,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
match_proof(p, p1) && match_proof(p, p1) &&
match_fact(p1.get(), fml) && match_fact(p1.get(), fml) &&
match_binary(fact.get(), d1, l1, r1) && match_binary(fact.get(), d1, l1, r1) &&
match_binary(fml.get(), d2, l2, r2) && match_binary(fml.get(), d2, l2, r2) &&
SAME_OP(d1.get(), d2.get()) && SAME_OP(d1.get(), d2.get()) &&
l1.get() == r2.get() && l1.get() == r2.get() &&
r1.get() == l2.get()) { r1.get() == l2.get()) {
@ -273,7 +272,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
} }
UNREACHABLE(); UNREACHABLE();
return false; return false;
} }
case PR_TRANSITIVITY_STAR: { case PR_TRANSITIVITY_STAR: {
if (match_fact(p, fact) && if (match_fact(p, fact) &&
match_binary(fact.get(), d1, t1, t2)) { match_binary(fact.get(), d1, t1, t2)) {
@ -294,14 +293,14 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
return false; return false;
} }
} }
return return
vertices.size() == 2 && vertices.size() == 2 &&
vertices.contains(t1->get_id()) && vertices.contains(t1->get_id()) &&
vertices.contains(t2->get_id()); vertices.contains(t2->get_id());
} }
UNREACHABLE(); UNREACHABLE();
return false; return false;
} }
case PR_MONOTONICITY: { case PR_MONOTONICITY: {
TRACE("proof_checker", tout << mk_bounded_pp(p, m, 3) << "\n";); TRACE("proof_checker", tout << mk_bounded_pp(p, m, 3) << "\n";);
if (match_fact(p, fact) && if (match_fact(p, fact) &&
@ -317,7 +316,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
if (term1 != term2) { if (term1 != term2) {
bool found = false; bool found = false;
for(unsigned j = 0; j < proofs.size() && !found; ++j) { for(unsigned j = 0; j < proofs.size() && !found; ++j) {
found = found =
match_fact(proofs[j].get(), fml) && match_fact(proofs[j].get(), fml) &&
match_binary(fml.get(), d2, s1, s2) && match_binary(fml.get(), d2, s1, s2) &&
SAME_OP(d1.get(), d2.get()) && SAME_OP(d1.get(), d2.get()) &&
@ -353,7 +352,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
for (unsigned i = 0; i < q1->get_num_decls(); ++i) { for (unsigned i = 0; i < q1->get_num_decls(); ++i) {
if (q1->get_decl_sort(i) != q2->get_decl_sort(i)) { if (q1->get_decl_sort(i) != q2->get_decl_sort(i)) {
// term is not well-typed. // term is not well-typed.
UNREACHABLE(); UNREACHABLE();
return false; return false;
} }
} }
@ -410,7 +409,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
side_conditions.push_back(fact.get()); side_conditions.push_back(fact.get());
return true; return true;
} }
IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m);); IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m););
return false; return false;
} }
case PR_REWRITE_STAR: { case PR_REWRITE_STAR: {
@ -428,8 +427,8 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
side_conditions.push_back(rewrite_cond.get()); side_conditions.push_back(rewrite_cond.get());
return true; return true;
} }
IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m);); IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m););
return false; return false;
} }
case PR_PULL_QUANT: { case PR_PULL_QUANT: {
if (match_proof(p) && if (match_proof(p) &&
@ -439,7 +438,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// TBD: check the enchilada. // TBD: check the enchilada.
return true; return true;
} }
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m);); IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m););
return false; return false;
} }
case PR_PUSH_QUANT: { case PR_PUSH_QUANT: {
@ -459,7 +458,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
} }
else { else {
return false; return false;
} }
} }
} }
UNREACHABLE(); UNREACHABLE();
@ -470,7 +469,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
match_fact(p, fact) && match_fact(p, fact) &&
match_iff(fact.get(), t1, t2)) { match_iff(fact.get(), t1, t2)) {
// TBD: // TBD:
// match_quantifier(t1.get(), is_forall1, decls1, body1) // match_quantifier(t1.get(), is_forall1, decls1, body1)
// filter out decls1 that occur in body1. // filter out decls1 that occur in body1.
// if list is empty, then t2 could be just body1. // if list is empty, then t2 could be just body1.
// otherwise t2 is also a quantifier. // otherwise t2 is also a quantifier.
@ -489,7 +488,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// TBD: check that terms are set of equalities. // TBD: check that terms are set of equalities.
// t2 is an instance of a predicate in terms1 // t2 is an instance of a predicate in terms1
return true; return true;
} }
IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";); IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";);
return false; return false;
} }
@ -511,7 +510,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
get_hypotheses(p1.get(), hypotheses); get_hypotheses(p1.get(), hypotheses);
if (hypotheses.size() == 1 && match_negated(hypotheses.get(0), fact)) { if (hypotheses.size() == 1 && match_negated(hypotheses.get(0), fact)) {
// Suppose fact is (or a b c) and hypothesis is (not (or a b c)) // Suppose fact is (or a b c) and hypothesis is (not (or a b c))
// That is, (or a b c) should be viewed as a 'quoted expression' and a unary clause, // That is, (or a b c) should be viewed as a 'quoted expression' and a unary clause,
// instead of a clause with three literals. // instead of a clause with three literals.
return true; return true;
} }
@ -535,7 +534,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
}); });
UNREACHABLE(); UNREACHABLE();
return false; return false;
} }
TRACE("proof_checker", tout << "Matched:\n"; TRACE("proof_checker", tout << "Matched:\n";
ast_ll_pp(tout, m, hypotheses[i].get()); ast_ll_pp(tout, m, hypotheses[i].get());
ast_ll_pp(tout, m, ors[j-1].get());); ast_ll_pp(tout, m, ors[j-1].get()););
@ -550,7 +549,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
proofs.size() == 2 && proofs.size() == 2 &&
match_fact(proofs[0].get(), fml1) && match_fact(proofs[0].get(), fml1) &&
match_fact(proofs[1].get(), fml2) && match_fact(proofs[1].get(), fml2) &&
match_negated(fml1.get(), fml2.get()) && m.is_complement(fml1.get(), fml2.get()) &&
m.is_false(fact.get())) { m.is_false(fact.get())) {
return true; return true;
} }
@ -564,7 +563,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
} }
bool found = false; bool found = false;
for (unsigned j = 0; !found && j < terms1.size(); ++j) { for (unsigned j = 0; !found && j < terms1.size(); ++j) {
if (match_negated(terms1.get(j), fml2)) { if (m.is_complement(terms1.get(j), fml2)) {
found = true; found = true;
if (j + 1 < terms1.size()) { if (j + 1 < terms1.size()) {
terms1[j] = terms1.get(terms1.size()-1); terms1[j] = terms1.get(terms1.size()-1);
@ -573,7 +572,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
} }
} }
if (!found) { if (!found) {
TRACE("pr_unit_bug", TRACE("pr_unit_bug",
tout << "Parents:\n"; tout << "Parents:\n";
for (unsigned i = 0; i < proofs.size(); i++) { for (unsigned i = 0; i < proofs.size(); i++) {
expr_ref p(m); expr_ref p(m);
@ -592,9 +591,9 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
} }
} }
switch(terms1.size()) { switch(terms1.size()) {
case 0: case 0:
return m.is_false(fact.get()); return m.is_false(fact.get());
case 1: case 1:
return fact.get() == terms1[0].get(); return fact.get() == terms1[0].get();
default: { default: {
if (match_or(fact.get(), terms2)) { if (match_or(fact.get(), terms2)) {
@ -617,7 +616,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
return false; return false;
} }
} }
} }
UNREACHABLE(); UNREACHABLE();
@ -635,7 +634,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
} }
UNREACHABLE(); UNREACHABLE();
return false; return false;
} }
case PR_IFF_FALSE: { case PR_IFF_FALSE: {
// iff_false(?rule(?p1, (not ?fml)), (iff ?fml false)) // iff_false(?rule(?p1, (not ?fml)), (iff ?fml false))
if (match_proof(p, p1) && if (match_proof(p, p1) &&
@ -678,11 +677,11 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
} }
case PR_DEF_INTRO: { case PR_DEF_INTRO: {
// def_intro(?fml) // def_intro(?fml)
// //
// ?fml: forall x . ~p(x) or e(x) and forall x . ~e(x) or p(x) // ?fml: forall x . ~p(x) or e(x) and forall x . ~e(x) or p(x)
// : forall x . ~cond(x) or f(x) = then(x) and forall x . cond(x) or f(x) = else(x) // : forall x . ~cond(x) or f(x) = then(x) and forall x . cond(x) or f(x) = else(x)
// : forall x . f(x) = e(x) // : forall x . f(x) = e(x)
// //
if (match_fact(p, fact) && if (match_fact(p, fact) &&
match_proof(p) && match_proof(p) &&
m.is_bool(fact.get())) { m.is_bool(fact.get())) {
@ -712,7 +711,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
return true; return true;
} }
UNREACHABLE(); UNREACHABLE();
return false; return false;
} }
case PR_NNF_POS: { case PR_NNF_POS: {
// TBD: // TBD:
@ -735,9 +734,9 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
is_forall = true; is_forall = true;
} }
if (is_quantifier(e)) { if (is_quantifier(e)) {
q = to_quantifier(e); q = to_quantifier(e);
// TBD check that quantifier is properly instantiated // TBD check that quantifier is properly instantiated
return is_forall == q->is_forall(); return is_forall == q->is_forall();
} }
} }
UNREACHABLE(); UNREACHABLE();
@ -788,7 +787,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
vs(premise, sub.size(), sub.c_ptr(), premise); vs(premise, sub.size(), sub.c_ptr(), premise);
} }
fmls.push_back(premise.get()); fmls.push_back(premise.get());
TRACE("proof_checker", TRACE("proof_checker",
tout << mk_pp(premise.get(), m) << "\n"; tout << mk_pp(premise.get(), m) << "\n";
for (unsigned j = 0; j < sub.size(); ++j) { for (unsigned j = 0; j < sub.size(); ++j) {
tout << mk_pp(sub[j], m) << " "; tout << mk_pp(sub[j], m) << " ";
@ -810,7 +809,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// ok // ok
} }
else { else {
IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" << IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" <<
mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";); mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";);
} }
fmls[i] = premise1; fmls[i] = premise1;
@ -825,7 +824,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
else { else {
premise0 = m.mk_iff(premise0, conclusion); premise0 = m.mk_iff(premise0, conclusion);
} }
side_conditions.push_back(premise0); side_conditions.push_back(premise0);
return true; return true;
} }
default: default:
@ -841,7 +840,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
(=> (and ln+1 ln+2 .. ln+m) l0) (=> (and ln+1 ln+2 .. ln+m) l0)
or in the most general (ground) form: or in the most general (ground) form:
(=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1)) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))
In other words we use the following (Prolog style) convention for Horn In other words we use the following (Prolog style) convention for Horn
implications: implications:
The head of a Horn implication is position 0, The head of a Horn implication is position 0,
the first conjunct in the body of an implication is position 1 the first conjunct in the body of an implication is position 1
@ -853,7 +852,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
app* a = to_app(e); app* a = to_app(e);
expr* head, *body; expr* head, *body;
expr_ref_vector args(m); expr_ref_vector args(m);
if (m.is_or(e)) { if (m.is_or(e)) {
SASSERT(position < a->get_num_args()); SASSERT(position < a->get_num_args());
args.append(a->get_num_args(), a->get_args()); args.append(a->get_num_args(), a->get_args());
lit = args[position].get(); lit = args[position].get();
@ -865,13 +864,13 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
unsigned num_heads = 1; unsigned num_heads = 1;
if (m.is_or(head)) { if (m.is_or(head)) {
num_heads = to_app(head)->get_num_args(); num_heads = to_app(head)->get_num_args();
heads = to_app(head)->get_args(); heads = to_app(head)->get_args();
} }
expr*const* bodies = &body; expr*const* bodies = &body;
unsigned num_bodies = 1; unsigned num_bodies = 1;
if (m.is_and(body)) { if (m.is_and(body)) {
num_bodies = to_app(body)->get_num_args(); num_bodies = to_app(body)->get_num_args();
bodies = to_app(body)->get_args(); bodies = to_app(body)->get_args();
} }
if (position < num_heads) { if (position < num_heads) {
args.append(num_heads, heads); args.append(num_heads, heads);
@ -884,7 +883,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
args.append(num_bodies, bodies); args.append(num_bodies, bodies);
lit = m.mk_not(args[position].get()); lit = m.mk_not(args[position].get());
args[position] = m.mk_true(); args[position] = m.mk_true();
e = m.mk_implies(m.mk_and(args.size(), args.c_ptr()), head); e = m.mk_implies(m.mk_and(args.size(), args.c_ptr()), head);
} }
} }
else if (position == 0) { else if (position == 0) {
@ -914,7 +913,7 @@ void proof_checker::add_premise(proof* p) {
} }
bool proof_checker::match_proof(proof const* p) const { bool proof_checker::match_proof(proof const* p) const {
return return
m.is_proof(p) && m.is_proof(p) &&
m.get_num_parents(p) == 0; m.get_num_parents(p) == 0;
} }
@ -927,7 +926,7 @@ bool proof_checker::match_proof(proof const* p, proof_ref& p0) const {
} }
return false; return false;
} }
bool proof_checker::match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const { bool proof_checker::match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const {
if (m.is_proof(p) && if (m.is_proof(p) &&
m.get_num_parents(p) == 2) { m.get_num_parents(p) == 2) {
@ -1055,7 +1054,7 @@ bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const {
bool proof_checker::match_negated(expr const* a, expr* b) const { bool proof_checker::match_negated(expr const* a, expr* b) const {
expr_ref t(m); expr_ref t(m);
return return
(match_not(a, t) && t.get() == b) || (match_not(a, t) && t.get() == b) ||
(match_not(b, t) && t.get() == a); (match_not(b, t) && t.get() == a);
} }
@ -1082,7 +1081,7 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
p = stack.back(); p = stack.back();
SASSERT(m.is_proof(p)); SASSERT(m.is_proof(p));
if (m_hypotheses.contains(p)) { if (m_hypotheses.contains(p)) {
stack.pop_back(); stack.pop_back();
continue; continue;
} }
if (is_hypothesis(p) && match_fact(p, hyp)) { if (is_hypothesis(p) && match_fact(p, hyp)) {
@ -1124,13 +1123,13 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
if (!m_hypotheses.find(p, h)) { if (!m_hypotheses.find(p, h)) {
UNREACHABLE(); UNREACHABLE();
} }
ptr_buffer<expr> hyps; ptr_buffer<expr> hyps;
ptr_buffer<expr> todo; ptr_buffer<expr> todo;
expr_mark mark; expr_mark mark;
todo.push_back(h); todo.push_back(h);
expr_ref a(m), b(m); expr_ref a(m), b(m);
while (!todo.empty()) { while (!todo.empty()) {
h = todo.back(); h = todo.back();
@ -1155,14 +1154,14 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
ast_ll_pp(tout << "Getting hypotheses from: ", m, p); ast_ll_pp(tout << "Getting hypotheses from: ", m, p);
tout << "Found hypotheses:\n"; tout << "Found hypotheses:\n";
for (unsigned i = 0; i < ante.size(); ++i) { for (unsigned i = 0; i < ante.size(); ++i) {
ast_ll_pp(tout, m, ante[i].get()); ast_ll_pp(tout, m, ante[i].get());
} }
}); });
} }
bool proof_checker::match_nil(expr const* e) const { bool proof_checker::match_nil(expr const* e) const {
return return
is_app(e) && is_app(e) &&
to_app(e)->get_family_id() == m_hyp_fid && to_app(e)->get_family_id() == m_hyp_fid &&
to_app(e)->get_decl_kind() == OP_NIL; to_app(e)->get_decl_kind() == OP_NIL;
@ -1203,7 +1202,7 @@ expr* proof_checker::mk_nil() {
} }
bool proof_checker::is_hypothesis(proof const* p) const { bool proof_checker::is_hypothesis(proof const* p) const {
return return
m.is_proof(p) && m.is_proof(p) &&
p->get_decl_kind() == PR_HYPOTHESIS; p->get_decl_kind() == PR_HYPOTHESIS;
} }
@ -1225,7 +1224,7 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
} }
else { else {
return result; return result;
} }
} }
void proof_checker::dump_proof(proof const* pr) { void proof_checker::dump_proof(proof const* pr) {
@ -1267,7 +1266,7 @@ void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecede
bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& coeff, expr_ref& sum, bool& is_strict) { bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& coeff, expr_ref& sum, bool& is_strict) {
arith_util a(m); arith_util a(m);
app* lit = lit0; app* lit = lit0;
if (m.is_not(lit)) { if (m.is_not(lit)) {
lit = to_app(lit->get_arg(0)); lit = to_app(lit->get_arg(0));
is_pos = !is_pos; is_pos = !is_pos;
@ -1307,25 +1306,25 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
} }
// //
// Multiplying by coefficients over strict // Multiplying by coefficients over strict
// and non-strict inequalities: // and non-strict inequalities:
// //
// (a <= b) * 2 // (a <= b) * 2
// (a - b <= 0) * 2 // (a - b <= 0) * 2
// (2a - 2b <= 0) // (2a - 2b <= 0)
// (a < b) * 2 <=> // (a < b) * 2 <=>
// (a +1 <= b) * 2 <=> // (a +1 <= b) * 2 <=>
// 2a + 2 <= 2b <=> // 2a + 2 <= 2b <=>
// 2a+2-2b <= 0 // 2a+2-2b <= 0
bool strict_ineq = bool strict_ineq =
is_pos?(a.is_gt(lit) || a.is_lt(lit)):(a.is_ge(lit) || a.is_le(lit)); is_pos?(a.is_gt(lit) || a.is_lt(lit)):(a.is_ge(lit) || a.is_le(lit));
if (is_int && strict_ineq) { if (is_int && strict_ineq) {
sum = a.mk_add(sum, sign1); sum = a.mk_add(sum, sign1);
} }
term = a.mk_mul(sign1, a0); term = a.mk_mul(sign1, a0);
sum = a.mk_add(sum, term); sum = a.mk_add(sum, term);
term = a.mk_mul(sign2, a1); term = a.mk_mul(sign2, a1);
@ -1357,7 +1356,7 @@ bool proof_checker::check_arith_proof(proof* p) {
} }
expr_ref fact(m); expr_ref fact(m);
proof_ref_vector proofs(m); proof_ref_vector proofs(m);
if (!match_fact(p, fact)) { if (!match_fact(p, fact)) {
UNREACHABLE(); UNREACHABLE();
return false; return false;
@ -1386,7 +1385,7 @@ bool proof_checker::check_arith_proof(proof* p) {
coeffs[i] = lc*coeffs[i]; coeffs[i] = lc*coeffs[i];
} }
} }
unsigned num_parents = m.get_num_parents(p); unsigned num_parents = m.get_num_parents(p);
for (unsigned i = 0; i < num_parents; i++) { for (unsigned i = 0; i < num_parents; i++) {
proof * a = m.get_parent(p, i); proof * a = m.get_parent(p, i);
@ -1395,11 +1394,11 @@ bool proof_checker::check_arith_proof(proof* p) {
return false; return false;
} }
} }
if (m.is_or(fact)) { if (m.is_or(fact)) {
app* disj = to_app(fact); app* disj = to_app(fact);
unsigned num_args = disj->get_num_args(); unsigned num_args = disj->get_num_args();
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
app* lit = to_app(disj->get_arg(i)); app* lit = to_app(disj->get_arg(i));
if (!check_arith_literal(false, lit, coeffs[offset++], sum, is_strict)) { if (!check_arith_literal(false, lit, coeffs[offset++], sum, is_strict)) {
return false; return false;
@ -1411,13 +1410,13 @@ bool proof_checker::check_arith_proof(proof* p) {
return false; return false;
} }
} }
if (!sum.get()) { if (!sum.get()) {
return false; return false;
} }
sort* s = m.get_sort(sum); sort* s = m.get_sort(sum);
if (is_strict) { if (is_strict) {
sum = autil.mk_lt(sum, autil.mk_numeral(rational(0), s)); sum = autil.mk_lt(sum, autil.mk_numeral(rational(0), s));
@ -1435,6 +1434,6 @@ bool proof_checker::check_arith_proof(proof* p) {
dump_proof(p); dump_proof(p);
return false; return false;
} }
return true; return true;
} }