mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

Merge pull request #1518 from waywardmonkeys/const-proof-checker

Browse source 
Make proof_checker more const correct.
This commit is contained in:
Nikolaj Bjorner 2018-03-09 05:22:49 -05:00 • committed by GitHub
commit fc835ba01e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 51 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -922,7 +922,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
} }
} }
bool proof_checker::match_fact(proof* p, expr_ref& fact) { bool proof_checker::match_fact(proof const* p, expr_ref& fact) const {
if (m.is_proof(p) && if (m.is_proof(p) &&
m.has_fact(p)) { m.has_fact(p)) {
fact = m.get_fact(p); fact = m.get_fact(p);
@ -938,13 +938,13 @@ void proof_checker::add_premise(proof* p) {
} }
} }
bool proof_checker::match_proof(proof* p) { 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;
} }
bool proof_checker::match_proof(proof* p, proof_ref& p0) { bool proof_checker::match_proof(proof const* p, proof_ref& p0) const {
if (m.is_proof(p) && if (m.is_proof(p) &&
m.get_num_parents(p) == 1) { m.get_num_parents(p) == 1) {
p0 = m.get_parent(p, 0); p0 = m.get_parent(p, 0);
@ -953,7 +953,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0) {
return false; return false;
} }
bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) { 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) {
p0 = m.get_parent(p, 0); p0 = m.get_parent(p, 0);
@ -963,7 +963,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
return false; return false;
} }
bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) { bool proof_checker::match_proof(proof const* p, proof_ref_vector& parents) const {
if (m.is_proof(p)) { if (m.is_proof(p)) {
for (unsigned i = 0; i < m.get_num_parents(p); ++i) { for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
parents.push_back(m.get_parent(p, i)); parents.push_back(m.get_parent(p, i));
@ -974,7 +974,7 @@ bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
} }
bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) { bool proof_checker::match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const {
if (e->get_kind() == AST_APP && if (e->get_kind() == AST_APP &&
to_app(e)->get_num_args() == 2) { to_app(e)->get_num_args() == 2) {
d = to_app(e)->get_decl(); d = to_app(e)->get_decl();
@ -986,7 +986,7 @@ bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_r
} }
bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms) { bool proof_checker::match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const {
if (e->get_kind() == AST_APP) { if (e->get_kind() == AST_APP) {
d = to_app(e)->get_decl(); d = to_app(e)->get_decl();
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
@ -997,9 +997,9 @@ bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms)
return false; return false;
} }
bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) { bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) const {
if (is_quantifier(e)) { if (is_quantifier(e)) {
quantifier* q = to_quantifier(e); quantifier const* q = to_quantifier(e);
is_univ = q->is_forall(); is_univ = q->is_forall();
body = q->get_expr(); body = q->get_expr();
for (unsigned i = 0; i < q->get_num_decls(); ++i) { for (unsigned i = 0; i < q->get_num_decls(); ++i) {
@ -1010,7 +1010,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so
return false; return false;
} }
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) { bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const {
if (e->get_kind() == AST_APP && if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() && to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k && to_app(e)->get_decl_kind() == k &&
@ -1022,7 +1022,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
return false; return false;
} }
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) { bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const {
if (e->get_kind() == AST_APP && if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() && to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k) { to_app(e)->get_decl_kind() == k) {
@ -1035,7 +1035,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
} }
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) { bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t) const {
if (e->get_kind() == AST_APP && if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() && to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k && to_app(e)->get_decl_kind() == k &&
@ -1046,39 +1046,39 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
return false; return false;
} }
bool proof_checker::match_not(expr* e, expr_ref& t) { bool proof_checker::match_not(expr const* e, expr_ref& t) const {
return match_op(e, OP_NOT, t); return match_op(e, OP_NOT, t);
} }
bool proof_checker::match_or(expr* e, expr_ref_vector& terms) { bool proof_checker::match_or(expr const* e, expr_ref_vector& terms) const {
return match_op(e, OP_OR, terms); return match_op(e, OP_OR, terms);
} }
bool proof_checker::match_and(expr* e, expr_ref_vector& terms) { bool proof_checker::match_and(expr const* e, expr_ref_vector& terms) const {
return match_op(e, OP_AND, terms); return match_op(e, OP_AND, terms);
} }
bool proof_checker::match_iff(expr* e, expr_ref& t1, expr_ref& t2) { bool proof_checker::match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_IFF, t1, t2); return match_op(e, OP_IFF, t1, t2);
} }
bool proof_checker::match_equiv(expr* e, expr_ref& t1, expr_ref& t2) { bool proof_checker::match_equiv(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_oeq(e, t1, t2) || match_eq(e, t1, t2); return match_oeq(e, t1, t2) || match_eq(e, t1, t2);
} }
bool proof_checker::match_implies(expr* e, expr_ref& t1, expr_ref& t2) { bool proof_checker::match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_IMPLIES, t1, t2); return match_op(e, OP_IMPLIES, t1, t2);
} }
bool proof_checker::match_eq(expr* e, expr_ref& t1, expr_ref& t2) { bool proof_checker::match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_EQ, t1, t2) || match_iff(e, t1, t2); return match_op(e, OP_EQ, t1, t2) || match_iff(e, t1, t2);
} }
bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) { bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_OEQ, t1, t2); return match_op(e, OP_OEQ, t1, t2);
} }
bool proof_checker::match_negated(expr* a, expr* b) { 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) ||
@ -1186,14 +1186,14 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
} }
bool proof_checker::match_nil(expr* 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;
} }
bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const { bool proof_checker::match_cons(expr const* e, expr_ref& a, expr_ref& b) const {
if (is_app(e) && if (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_CONS) { to_app(e)->get_decl_kind() == OP_CONS) {
@ -1205,7 +1205,7 @@ bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
} }
bool proof_checker::match_atom(expr* e, expr_ref& a) const { bool proof_checker::match_atom(expr const* e, expr_ref& a) const {
if (is_app(e) && if (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_ATOM) { to_app(e)->get_decl_kind() == OP_ATOM) {
@ -1227,7 +1227,7 @@ expr* proof_checker::mk_nil() {
return m_nil.get(); return m_nil.get();
} }
bool proof_checker::is_hypothesis(proof* 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;
@ -1253,7 +1253,7 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
} }
} }
void proof_checker::dump_proof(proof * pr) { void proof_checker::dump_proof(proof const* pr) {
if (!m_dump_lemmas) if (!m_dump_lemmas)
return; return;
SASSERT(m.has_fact(pr)); SASSERT(m.has_fact(pr));

50
src/ast/proofs/proof_checker.h
View file

@ -77,39 +77,39 @@ private:
bool check1_spc(proof* p, expr_ref_vector& side_conditions); bool check1_spc(proof* p, expr_ref_vector& side_conditions);
bool check_arith_proof(proof* p); bool check_arith_proof(proof* p);
bool check_arith_literal(bool is_pos, app* lit, rational const& coeff, expr_ref& sum, bool& is_strict); bool check_arith_literal(bool is_pos, app* lit, rational const& coeff, expr_ref& sum, bool& is_strict);
bool match_fact(proof* p, expr_ref& fact); bool match_fact(proof const* p, expr_ref& fact) const;
void add_premise(proof* p); void add_premise(proof* p);
bool match_proof(proof* p); bool match_proof(proof const* p) const;
bool match_proof(proof* p, proof_ref& p0); bool match_proof(proof const* p, proof_ref& p0) const;
bool match_proof(proof* p, proof_ref& p0, proof_ref& p1); bool match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const;
bool match_proof(proof* p, proof_ref_vector& parents); bool match_proof(proof const* p, proof_ref_vector& parents) const;
bool match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2); bool match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const;
bool match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2); bool match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const;
bool match_op(expr* e, decl_kind k, expr_ref& t); bool match_op(expr const* e, decl_kind k, expr_ref& t) const;
bool match_op(expr* e, decl_kind k, expr_ref_vector& terms); bool match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const;
bool match_iff(expr* e, expr_ref& t1, expr_ref& t2); bool match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const;
bool match_implies(expr* e, expr_ref& t1, expr_ref& t2); bool match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const;
bool match_eq(expr* e, expr_ref& t1, expr_ref& t2); bool match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const;
bool match_oeq(expr* e, expr_ref& t1, expr_ref& t2); bool match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const;
bool match_not(expr* e, expr_ref& t); bool match_not(expr const* e, expr_ref& t) const;
bool match_or(expr* e, expr_ref_vector& terms); bool match_or(expr const* e, expr_ref_vector& terms) const;
bool match_and(expr* e, expr_ref_vector& terms); bool match_and(expr const* e, expr_ref_vector& terms) const;
bool match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms); bool match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const;
bool match_quantifier(expr*, bool& is_univ, sort_ref_vector&, expr_ref& body); bool match_quantifier(expr const*, bool& is_univ, sort_ref_vector&, expr_ref& body) const;
bool match_negated(expr* a, expr* b); bool match_negated(expr const* a, expr* b) const;
bool match_equiv(expr* a, expr_ref& t1, expr_ref& t2); bool match_equiv(expr const* a, expr_ref& t1, expr_ref& t2) const;
void get_ors(expr* e, expr_ref_vector& ors); void get_ors(expr* e, expr_ref_vector& ors);
void get_hypotheses(proof* p, expr_ref_vector& ante); void get_hypotheses(proof* p, expr_ref_vector& ante);
bool match_nil(expr* e) const; bool match_nil(expr const* e) const;
bool match_cons(expr* e, expr_ref& a, expr_ref& b) const; bool match_cons(expr const* e, expr_ref& a, expr_ref& b) const;
bool match_atom(expr* e, expr_ref& a) const; bool match_atom(expr const* e, expr_ref& a) const;
expr* mk_nil(); expr* mk_nil();
expr* mk_cons(expr* a, expr* b); expr* mk_cons(expr* a, expr* b);
expr* mk_atom(expr* e); expr* mk_atom(expr* e);
bool is_hypothesis(proof* p) const; bool is_hypothesis(proof const* p) const;
expr* mk_hyp(unsigned num_hyps, expr * const * hyps); expr* mk_hyp(unsigned num_hyps, expr * const * hyps);
void dump_proof(proof * pr); void dump_proof(proof const* pr);
void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent); void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent);
void set_false(expr_ref& e, unsigned idx, expr_ref& lit); void set_false(expr_ref& e, unsigned idx, expr_ref& lit);