From 1b300d35980f811a92fa07eec2ff75f9dcfcb435 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Dec 2013 12:55:51 -0800
Subject: [PATCH] chore(kernel/builtin): remove unnecessary functions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/builtin.cpp | 21 ---------------------
 src/kernel/builtin.h   |  3 ---
 2 files changed, 24 deletions(-)

diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 0629114c4b..95a6868e9a 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -161,16 +161,6 @@ MK_BUILTIN(if_fn, if_fn_value);
 expr read_if(deserializer & ) { return mk_if_fn(); }
 static register_deserializer_fn if_ds("if", read_if);
 MK_IS_BUILTIN(is_if_fn, mk_if_fn());
-bool is_if(expr const & n, expr & c, expr & t, expr & e) {
-    if (is_if(n)) {
-        c = arg(n, 2);
-        t = arg(n, 3);
-        e = arg(n, 4);
-        return true;
-    } else {
-        return false;
-    }
-}
 // =======================================
 
 MK_CONSTANT(implies_fn, name("implies"));
@@ -180,18 +170,7 @@ MK_CONSTANT(or_fn,      name("or"));
 MK_CONSTANT(not_fn,     name("not"));
 MK_CONSTANT(forall_fn,  name("forall"));
 MK_CONSTANT(exists_fn,  name("exists"));
-
 MK_CONSTANT(homo_eq_fn, name("eq"));
-bool is_homo_eq(expr const & e, expr & lhs, expr & rhs) {
-    if (is_homo_eq(e)) {
-        lhs = arg(e, 2);
-        rhs = arg(e, 3);
-        return true;
-    } else {
-        return false;
-    }
-}
-
 // Axioms
 MK_CONSTANT(mp_fn,          name("MP"));
 MK_CONSTANT(discharge_fn,   name("Discharge"));
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index c7464ff29a..35041187d9 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -53,7 +53,6 @@ bool is_false(expr const & e);
 expr mk_if_fn();
 bool is_if_fn(expr const & e);
 inline bool is_if(expr const & e) { return is_app(e) && is_if_fn(arg(e, 0)); }
-bool is_if(expr const & n, expr & c, expr & t, expr & e);
 /** \brief Return the term (if A c t e) */
 inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_app(mk_if_fn(), A, c, t, e); }
 inline expr If(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_if(A, c, t, e); }
@@ -75,7 +74,6 @@ inline expr Implies(std::initializer_list<expr> const & l) { return mk_implies(l
 expr mk_iff_fn();
 bool is_iff_fn(expr const & e);
 inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); }
-bool is_iff(expr const & e, expr & a1, expr & a2);
 /** \brief Return (e1 iff e2) */
 inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app(mk_iff_fn(), e1, e2); }
 inline expr mk_iff(unsigned num_args, expr const * args) { return mk_bin_rop(mk_iff_fn(), True, num_args, args); }
@@ -130,7 +128,6 @@ inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
 expr mk_homo_eq_fn();
 bool is_homo_eq_fn(expr const & e);
 inline bool is_homo_eq(expr const & e) { return is_app(e) && is_homo_eq_fn(arg(e, 0)); }
-bool is_homo_eq(expr const & e, expr & a1, expr & a2);
 /** \brief Return the term (homo_eq A l r) */
 inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); }
 inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); }