From 006418e0277e1ef400f4bd96ee31c3f9579c4449 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Jul 2020 23:34:21 -0700 Subject: [PATCH] build Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 12 ++++++------ src/api/ml/z3.mli | 4 ++-- src/util/memory_manager.h | 6 +++--- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index f30201e16..d3a2d0e74 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -263,8 +263,8 @@ sig end val mk_func_decl : context -> Symbol.symbol -> Sort.sort list -> Sort.sort -> func_decl val mk_func_decl_s : context -> string -> Sort.sort list -> Sort.sort -> func_decl - val mk_rec_fun : context -> Symbol.symbol -> Sort.sort list -> Sort.sort -> func_decl - val mk_rec_fun_s : context -> string -> Sort.sort list -> Sort.sort -> func_decl + val mk_rec_func_decl : context -> Symbol.symbol -> Sort.sort list -> Sort.sort -> func_decl + val mk_rec_func_decl_s : context -> string -> Sort.sort list -> Sort.sort -> func_decl val add_rec_def : context -> func_decl -> Expr.expr list -> Expr.expr -> unit val mk_fresh_func_decl : context -> string -> Sort.sort list -> Sort.sort -> func_decl val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl @@ -341,11 +341,11 @@ end = struct let mk_func_decl_s (ctx:context) (name:string) (domain:Sort.sort list) (range:Sort.sort) = mk_func_decl ctx (Symbol.mk_string ctx name) domain range - let mk_rec_fun (ctx:context) (name:Symbol.symbol) (domain:Sort.sort list) (range:Sort.sort) = - Z3native.mk_rec_fun ctx name (List.length domain) domain range + let mk_rec_func_decl (ctx:context) (name:Symbol.symbol) (domain:Sort.sort list) (range:Sort.sort) = + Z3native.mk_rec_func_decl ctx name (List.length domain) domain range - let mk_rec_fun_s (ctx:context) (name:string) (domain:Sort.sort list) (range:Sort.sort) = - mk_rec_fun ctx (Symbol.mk_string ctx name) domain range + let mk_rec_func_decl_s (ctx:context) (name:string) (domain:Sort.sort list) (range:Sort.sort) = + mk_rec_func_decl ctx (Symbol.mk_string ctx name) domain range let add_rec_def (ctx:context) (f:func_decl) (args:Expr.expr list) (body:Expr.expr) = Z3native.add_rec_def ctx f (List.length args) args body diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index fbbf8735b..6b797c552 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -329,11 +329,11 @@ sig (** Creates a function declaration that can be used in a recursive function definition. {!add_rec_def} *) - val mk_rec_fun : context -> Symbol.symbol -> Sort.sort list -> Sort.sort -> func_decl + val mk_rec_func_decl : context -> Symbol.symbol -> Sort.sort list -> Sort.sort -> func_decl (** Creates a function declaration that can be used in a recursive function definition. {!add_rec_def} *) - val mk_rec_fun_s : context -> string -> Sort.sort list -> Sort.sort -> func_decl + val mk_rec_func_decl_s : context -> string -> Sort.sort list -> Sort.sort -> func_decl (** Registers a recursive function definition *) val add_rec_def : context -> func_decl -> Expr.expr list -> Expr.expr -> unit diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index 112f6e682..2faa4da7d 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -16,14 +16,14 @@ Author: Revision History: --*/ -#ifndef MEMORY_H_ +#pragma once #include #include #include "util/z3_exception.h" -#pragma once -# define __has_builtin(x) 0 +#ifndef __has_builtin +#define __has_builtin(x) 0 #endif