mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

ML code simplification

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-12-22 23:37:07 +00:00
parent d6b7645d11
commit 0f656047c7
1 changed files with 2 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/api/ml/z3.ml
View file

@ -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)