mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

Use int64 for ocaml api functions that require it (#6150)

Browse source 
* Use int64 for ocaml api functions that require it

Signed-off-by: Stefan Muenzel <source@s.muenzel.net>

* Use elif

Signed-off-by: Stefan Muenzel <source@s.muenzel.net>
This commit is contained in:
Stefan Muenzel 2022-07-11 23:25:05 +07:00 committed by GitHub
parent 1f2346073a
commit 99212a2726
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 13 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
scripts/update_api.py
View file

@ -91,7 +91,7 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint',
# Mapping to ML types # Mapping to ML types
Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int64', UINT64 : 'int64', DOUBLE : 'float',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**', FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string', LBOOL : 'int' } BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string', LBOOL : 'int' }
@ -254,8 +254,10 @@ def param2pystr(p):
def param2ml(p): def param2ml(p):
k = param_kind(p) k = param_kind(p)
if k == OUT: if k == OUT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL or param_type(p) == INT64 or param_type(p) == UINT64: if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return "int" return "int"
elif param_type(p) == INT64 or param_type(p) == UINT64:
return "int64"
elif param_type(p) == STRING: elif param_type(p) == STRING:
return "string" return "string"
else: else:
@ -1252,9 +1254,9 @@ def ml_unwrap(t, ts, s):
elif t == UINT: elif t == UINT:
return '(' + ts + ') Unsigned_int_val(' + s + ')' return '(' + ts + ') Unsigned_int_val(' + s + ')'
elif t == INT64: elif t == INT64:
return '(' + ts + ') Long_val(' + s + ')' return '(' + ts + ') Int64_val(' + s + ')'
elif t == UINT64: elif t == UINT64:
return '(' + ts + ') Unsigned_long_val(' + s + ')' return '(' + ts + ') Int64_val(' + s + ')'
elif t == DOUBLE: elif t == DOUBLE:
return '(' + ts + ') Double_val(' + s + ')' return '(' + ts + ') Double_val(' + s + ')'
elif ml_has_plus_type(ts): elif ml_has_plus_type(ts):
@ -1271,7 +1273,7 @@ def ml_set_wrap(t, d, n):
elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == LBOOL: elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == LBOOL:
return d + ' = Val_int(' + n + ');' return d + ' = Val_int(' + n + ');'
elif t == INT64 or t == UINT64: elif t == INT64 or t == UINT64:
return d + ' = Val_long(' + n + ');' return d + ' = caml_copy_int64(' + n + ');'
elif t == DOUBLE: elif t == DOUBLE:
return d + '= caml_copy_double(' + n + ');' return d + '= caml_copy_double(' + n + ');'
elif t == STRING: elif t == STRING:

12
src/api/ml/z3.mli
View file

@ -927,10 +927,10 @@ end
module FiniteDomain : module FiniteDomain :
sig sig
(** Create a new finite domain sort. *) (** Create a new finite domain sort. *)
val mk_sort : context -> Symbol.symbol -> int -> Sort.sort val mk_sort : context -> Symbol.symbol -> int64 -> Sort.sort
(** Create a new finite domain sort. *) (** Create a new finite domain sort. *)
val mk_sort_s : context -> string -> int -> Sort.sort val mk_sort_s : context -> string -> int64 -> Sort.sort
(** Indicates whether the term is of an array sort. *) (** Indicates whether the term is of an array sort. *)
val is_finite_domain : Expr.expr -> bool val is_finite_domain : Expr.expr -> bool
@ -939,7 +939,7 @@ sig
val is_lt : Expr.expr -> bool val is_lt : Expr.expr -> bool
(** The size of the finite domain sort. *) (** The size of the finite domain sort. *)
val get_size : Sort.sort -> int val get_size : Sort.sort -> int64
end end
@ -2078,7 +2078,7 @@ sig
val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr
(** Create a numeral of FloatingPoint sort from a sign bit and two integers. *) (** Create a numeral of FloatingPoint sort from a sign bit and two integers. *)
val mk_numeral_i_u : context -> bool -> int -> int -> Sort.sort -> Expr.expr val mk_numeral_i_u : context -> bool -> int64 -> int64 -> Sort.sort -> Expr.expr
(** Create a numeral of FloatingPoint sort from a string *) (** Create a numeral of FloatingPoint sort from a string *)
val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr
@ -2303,7 +2303,7 @@ sig
val get_numeral_exponent_string : context -> Expr.expr -> bool -> string val get_numeral_exponent_string : context -> Expr.expr -> bool -> string
(** Return the exponent value of a floating-point numeral as a signed integer *) (** Return the exponent value of a floating-point numeral as a signed integer *)
val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int64
(** Return the exponent of a floating-point numeral as a bit-vector expression. (** Return the exponent of a floating-point numeral as a bit-vector expression.
Remark: NaN's do not have a bit-vector exponent, so they are invalid arguments. *) Remark: NaN's do not have a bit-vector exponent, so they are invalid arguments. *)
@ -2320,7 +2320,7 @@ sig
Remark: This function extracts the significand bits, without the Remark: This function extracts the significand bits, without the
hidden bit or normalization. Throws an exception if the hidden bit or normalization. Throws an exception if the
significand does not fit into an int. *) significand does not fit into an int. *)
val get_numeral_significand_uint : context -> Expr.expr -> bool * int val get_numeral_significand_uint : context -> Expr.expr -> bool * int64
(** Indicates whether a floating-point numeral is a NaN. *) (** Indicates whether a floating-point numeral is a NaN. *)
val is_numeral_nan : context -> Expr.expr -> bool val is_numeral_nan : context -> Expr.expr -> bool