From 0f656047c785b30f88353b5fbf06f232e5a2387c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 22 Dec 2015 23:37:07 +0000 Subject: [PATCH] ML code simplification --- src/api/ml/z3.ml | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 84c70001e..87ed4fb0a 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -537,22 +537,10 @@ end = struct let ast_of_func_decl f = match f with FuncDecl(x) -> x let create_ndr ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort list ) ( range : Sort.sort ) = - let res = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.inc_ref ; - dec_ref = Z3native.dec_ref } in - (z3obj_sno res ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ; - (z3obj_create res) ; - FuncDecl(res) + func_decl_of_ptr ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (List.length domain) (Sort.sort_lton domain) (Sort.gno range)) let create_pdr ( ctx : context) ( prefix : string ) ( domain : Sort.sort list ) ( range : Sort.sort ) = - let res = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.inc_ref ; - dec_ref = Z3native.dec_ref } in - (z3obj_sno res ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ; - (z3obj_create res) ; - FuncDecl(res) + func_decl_of_ptr ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (List.length domain) (Sort.sort_lton domain) (Sort.gno range)) let gc ( x : func_decl ) = match x with FuncDecl(a) -> (z3obj_gc a) let gnc ( x : func_decl ) = match x with FuncDecl(a) -> (z3obj_gnc a)