From 87592cdb43ee4c0247476cb0aabe3967dee2fd62 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Sep 2014 22:45:53 -0700 Subject: [PATCH] refactor(library): remove dead code --- src/library/decl_macros.h | 38 -------------------------------------- 1 file changed, 38 deletions(-) delete mode 100644 src/library/decl_macros.h diff --git a/src/library/decl_macros.h b/src/library/decl_macros.h deleted file mode 100644 index 543a2c11b..000000000 --- a/src/library/decl_macros.h +++ /dev/null @@ -1,38 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -/** - \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc. -*/ -#define MK_BUILTIN(Name, ClassName) \ -expr mk_##Name() { \ - LEAN_THREAD_PTR(expr) r; \ - if (!r.get()) \ - r.reset(new expr(mk_value(*(new ClassName())))); \ - return *r; \ -} - -/** - \brief Helper macro for generating "defined" constants. -*/ -#dEFINE MK_CONSTANT(Name, NameObj) \ -static name Name ## _name = NameObj; \ -expr mk_##Name() { \ - LEAN_THREAD_PTR(expr) r; \ - if (!r.get()) \ - r.reset(new expr(mk_constant(Name ## _name))); \ - return *r; \ -} \ -bool is_ ## Name(expr const & e) { \ - return is_constant(e) && const_name(e) == Name ## _name; \ -} - -#define MK_IS_BUILTIN(Name, Builtin) \ -bool Name(expr const & e) { \ - expr const & v = Builtin; \ - return e == v || (is_constant(e) && const_name(e) == to_value(v).get_name()); \ -}