mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

streamlining proof generation (initial step of removing ast-manager dependency). Detect error in model creation when declaring constant with non-zero arity. See #1223

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-23 21:16:46 -07:00
parent 77bbae65f5
commit f63439603d
20 changed files with 129 additions and 153 deletions
Download patch file Download diff file Expand all files Collapse all files

90
src/ast/ast.cpp
View file

@ -2626,7 +2626,7 @@ bool ast_manager::is_fully_interp(sort * s) const {
// -----------------------------------
proof * ast_manager::mk_proof(family_id fid, decl_kind k, unsigned num_args, expr * const * args) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(fid, k, num_args, args);
}
@ -2662,8 +2662,7 @@ proof * ast_manager::mk_goal(expr * f) {
}
proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) {
if (m_proof_mode == PGM_DISABLED)
return m_undef_proof;
if (!p1 || !p2) return nullptr;
SASSERT(has_fact(p1));
SASSERT(has_fact(p2));
CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_iff(get_fact(p2)) || is_oeq(get_fact(p2))),
@ -2684,13 +2683,13 @@ proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) {
}
proof * ast_manager::mk_reflexivity(expr * e) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_REFLEXIVITY, mk_eq(e, e));
}
proof * ast_manager::mk_oeq_reflexivity(expr * e) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_REFLEXIVITY, mk_oeq(e, e));
}
@ -2705,8 +2704,7 @@ proof * ast_manager::mk_commutativity(app * f) {
\brief Given a proof of p, return a proof of (p <=> true)
*/
proof * ast_manager::mk_iff_true(proof * pr) {
if (m_proof_mode == PGM_DISABLED)
return m_undef_proof;
if (!pr) return pr;
SASSERT(has_fact(pr));
SASSERT(is_bool(get_fact(pr)));
return mk_app(m_basic_family_id, PR_IFF_TRUE, pr, mk_iff(get_fact(pr), mk_true()));
@ -2716,8 +2714,7 @@ proof * ast_manager::mk_iff_true(proof * pr) {
\brief Given a proof of (not p), return a proof of (p <=> false)
*/
proof * ast_manager::mk_iff_false(proof * pr) {
if (m_proof_mode == PGM_DISABLED)
return m_undef_proof;
if (!pr) return pr;
SASSERT(has_fact(pr));
SASSERT(is_not(get_fact(pr)));
expr * p = to_app(get_fact(pr))->get_arg(0);
@ -2725,10 +2722,7 @@ proof * ast_manager::mk_iff_false(proof * pr) {
}
proof * ast_manager::mk_symmetry(proof * p) {
if (m_proof_mode == PGM_DISABLED)
return m_undef_proof;
if (!p)
return p;
if (!p) return p;
if (is_reflexivity(p))
return p;
if (is_symmetry(p))
@ -2741,8 +2735,6 @@ proof * ast_manager::mk_symmetry(proof * p) {
}
proof * ast_manager::mk_transitivity(proof * p1, proof * p2) {
if (m_proof_mode == PGM_DISABLED)
return m_undef_proof;
if (!p1)
return p2;
if (!p2)
@ -2787,7 +2779,7 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2, proof * p3, proof *
}
proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
SASSERT(num_proofs > 0);
proof * r = proofs[0];
@ -2797,9 +2789,9 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs
}
proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs, expr * n1, expr * n2) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
if (fine_grain_proofs())
if (proofs_enabled())
return mk_transitivity(num_proofs, proofs);
SASSERT(num_proofs > 0);
if (num_proofs == 1)
@ -2817,7 +2809,7 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs
}
proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
SASSERT(f1->get_num_args() == f2->get_num_args());
SASSERT(f1->get_decl() == f2->get_decl());
@ -2828,7 +2820,7 @@ proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned
}
proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
SASSERT(get_sort(f1) == get_sort(f2));
sort * s = get_sort(f1);
@ -2837,7 +2829,7 @@ proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proo
}
proof * ast_manager::mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
SASSERT(get_sort(f1) == get_sort(f2));
sort * s = get_sort(f1);
@ -2846,7 +2838,7 @@ proof * ast_manager::mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs,
}
proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
if (!p) {
return 0;
@ -2858,7 +2850,7 @@ proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p)
}
proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof * p) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
SASSERT(q1->get_num_decls() == q2->get_num_decls());
SASSERT(has_fact(p));
@ -2867,25 +2859,25 @@ proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof
}
proof * ast_manager::mk_distributivity(expr * s, expr * r) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_DISTRIBUTIVITY, mk_eq(s, r));
}
proof * ast_manager::mk_rewrite(expr * s, expr * t) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_REWRITE, mk_eq(s, t));
}
proof * ast_manager::mk_oeq_rewrite(expr * s, expr * t) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_REWRITE, mk_oeq(s, t));
}
proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
@ -2894,37 +2886,37 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr
}
proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
}
proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
}
proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_PUSH_QUANT, mk_iff(q, e));
}
proof * ast_manager::mk_elim_unused_vars(quantifier * q, expr * e) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e));
}
proof * ast_manager::mk_der(quantifier * q, expr * e) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_DER, mk_iff(q, e));
}
proof * ast_manager::mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
vector<parameter> params;
for (unsigned i = 0; i < num_bind; ++i) {
@ -2959,7 +2951,7 @@ bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
}
proof * ast_manager::mk_def_axiom(expr * ax) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_DEF_AXIOM, ax);
}
@ -3001,7 +2993,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
new_lits.push_back(lit);
}
DEBUG_CODE({
for (unsigned i = 1; m_proof_mode == PGM_FINE && i < num_proofs; i++) {
for (unsigned i = 1; proofs_enabled() && i < num_proofs; i++) {
CTRACE("mk_unit_resolution_bug", !found.get(i, false),
for (unsigned j = 0; j < num_proofs; j++) {
if (j == i) tout << "Index " << i << " was not found:\n";
@ -3080,14 +3072,11 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
}
proof * ast_manager::mk_hypothesis(expr * h) {
if (m_proof_mode == PGM_DISABLED)
return m_undef_proof;
return mk_app(m_basic_family_id, PR_HYPOTHESIS, h);
}
proof * ast_manager::mk_lemma(proof * p, expr * lemma) {
if (m_proof_mode == PGM_DISABLED)
return m_undef_proof;
if (!p) return p;
SASSERT(has_fact(p));
CTRACE("mk_lemma", !is_false(get_fact(p)), tout << mk_ll_pp(p, *this) << "\n";);
SASSERT(is_false(get_fact(p)));
@ -3100,7 +3089,7 @@ proof * ast_manager::mk_def_intro(expr * new_def) {
}
proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
@ -3109,10 +3098,7 @@ proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, pr
}
proof * ast_manager::mk_iff_oeq(proof * p) {
if (m_proof_mode == PGM_DISABLED)
return m_undef_proof;
if (!p)
return p;
if (!p) return p;
SASSERT(has_fact(p));
SASSERT(is_iff(get_fact(p)) || is_oeq(get_fact(p)));
@ -3136,7 +3122,7 @@ bool ast_manager::check_nnf_proof_parents(unsigned num_proofs, proof * const * p
}
proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
check_nnf_proof_parents(num_proofs, proofs);
ptr_buffer<expr> args;
@ -3146,7 +3132,7 @@ proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof *
}
proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
check_nnf_proof_parents(num_proofs, proofs);
ptr_buffer<expr> args;
@ -3156,7 +3142,7 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
}
proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
@ -3165,7 +3151,7 @@ proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof
}
proof * ast_manager::mk_skolemization(expr * q, expr * e) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
SASSERT(is_bool(q));
SASSERT(is_bool(e));
@ -3173,7 +3159,7 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
}
proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
@ -3182,7 +3168,7 @@ proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof
}
proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
SASSERT(has_fact(p));
SASSERT(is_and(get_fact(p)));
@ -3193,7 +3179,7 @@ proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
}
proof * ast_manager::mk_not_or_elim(proof * p, unsigned i) {
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
SASSERT(has_fact(p));
SASSERT(is_not(get_fact(p)));
@ -3216,7 +3202,7 @@ proof * ast_manager::mk_th_lemma(
unsigned num_params, parameter const* params
)
{
if (m_proof_mode == PGM_DISABLED)
if (proofs_disabled())
return m_undef_proof;
ptr_buffer<expr> args;

8
src/ast/ast.h
View file

@ -1396,8 +1396,7 @@ public:
enum proof_gen_mode {
PGM_DISABLED,
PGM_COARSE,
PGM_FINE
PGM_ENABLED
};
// -----------------------------------
@ -2088,15 +2087,14 @@ protected:
proof * mk_proof(family_id fid, decl_kind k, expr * arg1, expr * arg2);
proof * mk_proof(family_id fid, decl_kind k, expr * arg1, expr * arg2, expr * arg3);
proof * mk_undef_proof() const { return m_undef_proof; }
public:
bool proofs_enabled() const { return m_proof_mode != PGM_DISABLED; }
bool proofs_disabled() const { return m_proof_mode == PGM_DISABLED; }
bool coarse_grain_proofs() const { return m_proof_mode == PGM_COARSE; }
bool fine_grain_proofs() const { return m_proof_mode == PGM_FINE; }
proof_gen_mode proof_mode() const { return m_proof_mode; }
void toggle_proof_mode(proof_gen_mode m) { m_proof_mode = m; } // APIs for creating proof objects return [undef]
proof * mk_undef_proof() const { return m_undef_proof; }
bool is_proof(expr const * n) const { return is_app(n) && to_app(n)->get_decl()->get_range() == m_proof_sort; }

4
src/ast/normal_forms/pull_quant.cpp
View file

@ -229,7 +229,7 @@ struct pull_quant::imp {
proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg)));
}
pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r);
if (m_manager.fine_grain_proofs()) {
if (m_manager.proofs_enabled()) {
app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
proof * p1 = proofs.empty() ? 0 : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
proof * p2 = r1 == r ? 0 : m_manager.mk_pull_quant(r1, to_quantifier(r));
@ -240,7 +240,7 @@ struct pull_quant::imp {
expr_ref new_expr(m_manager);
pull_quant1(to_quantifier(n)->get_expr(), new_expr);
pull_quant1(to_quantifier(n), new_expr, r);
if (m_manager.fine_grain_proofs()) {
if (m_manager.proofs_enabled()) {
quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
proof * p1 = 0;
if (n != q1) {

6
src/ast/pattern/pattern_inference.cpp
View file

@ -606,7 +606,7 @@ bool pattern_inference_cfg::reduce_quantifier(
result = m.update_quantifier_weight(tmp, new_weight);
TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";);
}
if (m.fine_grain_proofs())
if (m.proofs_enabled())
result_pr = m.mk_rewrite(q, new_q);
return true;
}
@ -671,7 +671,7 @@ bool pattern_inference_cfg::reduce_quantifier(
quantifier_ref new_q(m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body), m);
if (weight != q->get_weight())
new_q = m.update_quantifier_weight(new_q, weight);
if (m.fine_grain_proofs()) {
if (m.proofs_enabled()) {
proof* new_body_pr = m.mk_reflexivity(new_body);
result_pr = m.mk_quant_intro(q, new_q, new_body_pr);
}
@ -689,7 +689,7 @@ bool pattern_inference_cfg::reduce_quantifier(
warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str());
}
new_q = m.update_quantifier(result2, new_patterns.size(), (expr**) new_patterns.c_ptr(), result2->get_expr());
if (m.fine_grain_proofs()) {
if (m.proofs_enabled()) {
result_pr = m.mk_transitivity(new_pr, m.mk_quant_intro(result2, new_q, m.mk_reflexivity(new_q->get_expr())));
}
TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m) << "\n";);

2
src/ast/scoped_proof.h
View file

@ -37,7 +37,7 @@ public:
class scoped_proof : public scoped_proof_mode {
public:
scoped_proof(ast_manager& m): scoped_proof_mode(m, PGM_FINE) {}
scoped_proof(ast_manager& m): scoped_proof_mode(m, PGM_ENABLED) {}
};
class scoped_no_proof : public scoped_proof_mode {