From 59e388ece17e7c363a38710b3d0a6d2c1eafe29b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 4 Jun 2020 11:59:59 -0700
Subject: [PATCH] handle bind proof constructor and print lambda

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/tptp/tptp5.cpp |  6 +++++-
 src/ast/ast.cpp         | 12 ++----------
 2 files changed, 7 insertions(+), 11 deletions(-)

diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index 1a1e31f0a..7323cad8e 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -1338,9 +1338,10 @@ public:
         }
         else if (e.is_quantifier()) {
             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);
 
-            out << (is_forall?"!":"?") << "[";
+            out << (is_lambda?"^":(is_forall?"!":"?")) << "[";
             for (unsigned i = 0; i < nb; ++i) {
                 Z3_symbol n = Z3_get_quantifier_bound_name(ctx, e, i);
                 names.push_back(upper_case_var(z3::symbol(ctx, n)));
@@ -1680,6 +1681,9 @@ public:
             case Z3_OP_PR_HYPER_RESOLVE:
                 display_inference(out, "hyper_resolve", "thm", p); 
                 break;
+            case Z3_OP_PR_BIND:
+                display_inference(out, "bind", "th", p);
+                break;
             default:
                 out << "TBD: " << m_node_number << "\n" << p << "\n";
                 throw failure_ex("rule not handled");
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 8bd125dd7..3e6646299 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -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 {
-    if (is_rewrite(e)) {
-        VERIFY (is_eq(to_app(e)->get_arg(0), r1, r2));
-        return true;
-    }
-    else {
-        return false;
-    }
+    return is_rewrite(e) && is_eq(to_app(e)->get_arg(0), r1, r2);
 }
 
 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) {
     SASSERT(num_proofs >= 2);
-    for (unsigned i = 0; i < num_proofs; i++) {
-        SASSERT(has_fact(proofs[i]));
-    }
+    DEBUG_CODE(for (unsigned i = 0; i < num_proofs; i++) SASSERT(has_fact(proofs[i])););
     ptr_buffer<expr> args;
     expr * fact;
     expr * f1 = get_fact(proofs[0]);