mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
commit
7a9bd72e2e
|
@ -1378,7 +1378,7 @@ class PythonInstallComponent(Component):
|
|||
MakeRuleCmd.make_install_directory(out, self.pythonPkgDir, in_prefix=self.in_prefix_install)
|
||||
|
||||
# Sym-link or copy libz3 into python package directory
|
||||
if IS_WINDOWS or self.is_osx_hack():
|
||||
if IS_WINDOWS or IS_OSX:
|
||||
MakeRuleCmd.install_files(out,
|
||||
self.libz3Component.dll_file(),
|
||||
os.path.join(self.pythonPkgDir,
|
||||
|
|
|
@ -467,13 +467,8 @@ end = struct
|
|||
let to_string ( x : sort ) = Z3native.sort_to_string (gnc x) (gno x)
|
||||
|
||||
let mk_uninterpreted ( ctx : context ) ( s : Symbol.symbol ) =
|
||||
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_uninterpreted_sort (context_gno ctx) (Symbol.gno s))) ;
|
||||
(z3obj_create res) ;
|
||||
Sort(res)
|
||||
let n = (Z3native.mk_uninterpreted_sort (context_gno ctx) (Symbol.gno s)) in
|
||||
Sort(z3_native_object_of_ast_ptr ctx n)
|
||||
|
||||
let mk_uninterpreted_s ( ctx : context ) ( s : string ) =
|
||||
mk_uninterpreted ctx (Symbol.mk_string ( ctx : context ) s)
|
||||
|
@ -537,22 +532,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)
|
||||
|
|
Loading…
Reference in a new issue