mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

handle bind proof constructor and print lambda

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-04 11:59:59 -07:00
parent e52eed325c
commit 59e388ece1
2 changed files with 7 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
examples/tptp/tptp5.cpp
View file

@ -1338,9 +1338,10 @@ public:
} }
else if (e.is_quantifier()) { else if (e.is_quantifier()) {
bool is_forall = Z3_is_quantifier_forall(ctx, e); bool is_forall = Z3_is_quantifier_forall(ctx, e);
bool is_lambda = Z3_is_lambda(ctx, e);
unsigned nb = Z3_get_quantifier_num_bound(ctx, e); unsigned nb = Z3_get_quantifier_num_bound(ctx, e);
out << (is_forall?"!":"?") << "["; out << (is_lambda?"^":(is_forall?"!":"?")) << "[";
for (unsigned i = 0; i < nb; ++i) { for (unsigned i = 0; i < nb; ++i) {
Z3_symbol n = Z3_get_quantifier_bound_name(ctx, e, i); Z3_symbol n = Z3_get_quantifier_bound_name(ctx, e, i);
names.push_back(upper_case_var(z3::symbol(ctx, n))); names.push_back(upper_case_var(z3::symbol(ctx, n)));
@ -1680,6 +1681,9 @@ public:
case Z3_OP_PR_HYPER_RESOLVE: case Z3_OP_PR_HYPER_RESOLVE:
display_inference(out, "hyper_resolve", "thm", p); display_inference(out, "hyper_resolve", "thm", p);
break; break;
case Z3_OP_PR_BIND:
display_inference(out, "bind", "th", p);
break;
default: default:
out << "TBD: " << m_node_number << "\n" << p << "\n"; out << "TBD: " << m_node_number << "\n" << p << "\n";
throw failure_ex("rule not handled"); throw failure_ex("rule not handled");

12
src/ast/ast.cpp
View file

@ -3064,13 +3064,7 @@ bool ast_manager::is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector<exp
} }
bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const { bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
if (is_rewrite(e)) { return is_rewrite(e) && is_eq(to_app(e)->get_arg(0), r1, r2);
VERIFY (is_eq(to_app(e)->get_arg(0), r1, r2));
return true;
}
else {
return false;
}
} }
proof * ast_manager::mk_def_axiom(expr * ax) { proof * ast_manager::mk_def_axiom(expr * ax) {
@ -3081,9 +3075,7 @@ proof * ast_manager::mk_def_axiom(expr * ax) {
proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * proofs) { proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * proofs) {
SASSERT(num_proofs >= 2); SASSERT(num_proofs >= 2);
for (unsigned i = 0; i < num_proofs; i++) { DEBUG_CODE(for (unsigned i = 0; i < num_proofs; i++) SASSERT(has_fact(proofs[i])););
SASSERT(has_fact(proofs[i]));
}
ptr_buffer<expr> args; ptr_buffer<expr> args;
expr * fact; expr * fact;
expr * f1 = get_fact(proofs[0]); expr * f1 = get_fact(proofs[0]);