mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Fixes in the OCaml FPA API and example
This commit is contained in:
Christoph M. Wintersteiger
parent
1c9051016a
commit
5c7d0380d3
|
|
@ -247,6 +247,8 @@ open Z3.FloatingPoint
|
|||
**)
|
||||
let fpa_example ( ctx : context ) =
|
||||
Printf.printf "FPAExample\n" ;
|
||||
(* let str = ref "" in *)
|
||||
(* (read_line ()) ; *)
|
||||
let double_sort = (FloatingPoint.mk_sort_double ctx) in
|
||||
let rm_sort = (FloatingPoint.RoundingMode.mk_sort ctx) in
|
||||
|
||||
|
|
@ -257,63 +259,64 @@ let fpa_example ( ctx : context ) =
|
|||
let s_y = (mk_string ctx "y") in
|
||||
let x = (mk_const ctx s_x double_sort) in
|
||||
let y = (mk_const ctx s_y double_sort)in
|
||||
Printf.printf "A\n" ;
|
||||
let n = (mk_numeral_f ctx 42.0 double_sort) in
|
||||
Printf.printf "B\n" ;
|
||||
let n = (FloatingPoint.mk_numeral_f ctx 42.0 double_sort) in
|
||||
let s_x_plus_y = (mk_string ctx "x_plus_y") in
|
||||
let x_plus_y = (mk_const ctx s_x_plus_y double_sort) in
|
||||
let c1 = (mk_eq ctx x_plus_y (mk_add ctx rm x y)) in
|
||||
let args = [ c1 ; (mk_eq ctx x_plus_y n) ] in
|
||||
let c2 = (Boolean.mk_and ctx args) in
|
||||
let args2 = [ c2 ; (Boolean.mk_not ctx (mk_eq ctx rm (RoundingMode.mk_rtz ctx))) ] in
|
||||
let args2 = [ c2 ; (Boolean.mk_not ctx (Boolean.mk_eq ctx rm (RoundingMode.mk_rtz ctx))) ] in
|
||||
let c3 = (Boolean.mk_and ctx args2) in
|
||||
let and_args = [ (Boolean.mk_not ctx (mk_is_zero ctx y)) ;
|
||||
(Boolean.mk_not ctx (mk_is_nan ctx y)) ;
|
||||
(Boolean.mk_not ctx (mk_is_infinite ctx y)) ] in
|
||||
let args3 = [ c3 ; (Boolean.mk_and ctx and_args) ] in
|
||||
let c4 = (Boolean.mk_and ctx args3) in
|
||||
(Printf.printf "c4: %s\n" (Expr.to_string c4)) ;
|
||||
(
|
||||
let solver = (mk_solver ctx None) in
|
||||
(Solver.add solver [ c4 ]) ;
|
||||
if (check solver []) != SATISFIABLE then
|
||||
raise (TestFailedException "")
|
||||
else
|
||||
Printf.printf "Test passed.\n"
|
||||
);
|
||||
|
||||
(Printf.printf "c4: %s\n" (Expr.to_string c4))
|
||||
(* push(ctx); *)
|
||||
(* Z3_assert_cnstr(ctx, c4); *)
|
||||
(* check(ctx, Z3_L_TRUE); *)
|
||||
(* Z3_pop(ctx, 1); *)
|
||||
|
||||
(* // Show that the following are equal: *)
|
||||
(* // (fp #b0 #b10000000001 #xc000000000000) *)
|
||||
(* // ((_ to_fp 11 53) #x401c000000000000)) *)
|
||||
(* // ((_ to_fp 11 53) RTZ 1.75 2))) *)
|
||||
(* // ((_ to_fp 11 53) RTZ 7.0))) *)
|
||||
|
||||
(* Z3_push(ctx); *)
|
||||
(* c1 = Z3_mk_fpa_fp(ctx, *)
|
||||
(* Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)), *)
|
||||
(* Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)), *)
|
||||
(* Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11))); *)
|
||||
(* c2 = Z3_mk_fpa_to_fp_bv(ctx, *)
|
||||
(* Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)), *)
|
||||
(* Z3_mk_fpa_sort(ctx, 11, 53)); *)
|
||||
(* c3 = Z3_mk_fpa_to_fp_real_int(ctx, *)
|
||||
(* Z3_mk_fpa_rtz(ctx), *)
|
||||
(* Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)), *)
|
||||
(* Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), *)
|
||||
(* Z3_mk_fpa_sort(ctx, 11, 53)); *)
|
||||
(* c4 = Z3_mk_fpa_to_fp_real(ctx, *)
|
||||
(* Z3_mk_fpa_rtz(ctx), *)
|
||||
(* Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)), *)
|
||||
(* Z3_mk_fpa_sort(ctx, 11, 53)); *)
|
||||
(* args3[0] = Z3_mk_eq(ctx, c1, c2); *)
|
||||
(* args3[1] = Z3_mk_eq(ctx, c1, c3); *)
|
||||
(* args3[2] = Z3_mk_eq(ctx, c1, c4); *)
|
||||
(* c5 = Z3_mk_and(ctx, 3, args3); *)
|
||||
|
||||
(* printf("c5: %s\n", Z3_ast_to_string(ctx, c5)); *)
|
||||
(* Z3_assert_cnstr(ctx, c5); *)
|
||||
(* check(ctx, Z3_L_TRUE); *)
|
||||
(* Z3_pop(ctx, 1); *)
|
||||
|
||||
(* Z3_del_context(ctx); *)
|
||||
(* Show that the following are equal: *)
|
||||
(* (fp #b0 #b10000000001 #xc000000000000) *)
|
||||
(* ((_ to_fp 11 53) #x401c000000000000)) *)
|
||||
(* ((_ to_fp 11 53) RTZ 1.75 2))) *)
|
||||
(* ((_ to_fp 11 53) RTZ 7.0))) *)
|
||||
|
||||
let solver = (mk_solver ctx None) in
|
||||
let c1 = (mk_fp ctx
|
||||
(mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1))
|
||||
(mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52))
|
||||
(mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11))) in
|
||||
let c2 = (mk_to_fp_bv ctx
|
||||
(mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64))
|
||||
(mk_sort ctx 11 53)) in
|
||||
let c3 = (mk_to_fp_int_real ctx
|
||||
(RoundingMode.mk_rtz ctx)
|
||||
(mk_numeral_string ctx "2" (Integer.mk_sort ctx))
|
||||
(mk_numeral_string ctx "1.75" (Real.mk_sort ctx))
|
||||
(FloatingPoint.mk_sort ctx 11 53)) in
|
||||
let c4 = (mk_to_fp_real ctx (RoundingMode.mk_rtz ctx)
|
||||
(mk_numeral_string ctx "7.0" (Real.mk_sort ctx))
|
||||
(FloatingPoint.mk_sort ctx 11 53)) in
|
||||
let args3 = [ (mk_eq ctx c1 c2) ;
|
||||
(mk_eq ctx c1 c3) ;
|
||||
(mk_eq ctx c1 c4) ] in
|
||||
let c5 = (Boolean.mk_and ctx args3) in
|
||||
(Printf.printf "c5: %s\n" (Expr.to_string c5)) ;
|
||||
(
|
||||
let solver = (mk_solver ctx None) in
|
||||
(Solver.add solver [ c5 ]) ;
|
||||
if (check solver []) != SATISFIABLE then
|
||||
raise (TestFailedException "")
|
||||
else
|
||||
Printf.printf "Test passed.\n"
|
||||
)
|
||||
|
||||
let _ =
|
||||
try (
|
||||
|
|
|
|||
|
|
@ -546,7 +546,7 @@ def parse_options():
|
|||
'b:df:sxhmcvtnp:gj',
|
||||
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
|
||||
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
|
||||
'githash=', 'x86'])
|
||||
'githash=', 'x86', 'ml'])
|
||||
except:
|
||||
print("ERROR: Invalid command line option")
|
||||
display_help(1)
|
||||
|
|
|
|||
|
|
@ -1479,9 +1479,9 @@ struct
|
|||
|
||||
let is_modulus ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MOD)
|
||||
|
||||
let is_inttoreal ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL)
|
||||
let is_int2real ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL)
|
||||
|
||||
let is_real_to_int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT)
|
||||
let is_real2int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT)
|
||||
|
||||
let is_real_is_int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IS_INT)
|
||||
|
||||
|
|
@ -1686,8 +1686,8 @@ struct
|
|||
let is_bv_rotateright ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_RIGHT)
|
||||
let is_bv_rotateleftextended ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_LEFT)
|
||||
let is_bv_rotaterightextended ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_RIGHT)
|
||||
let is_int_to_bv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_INT2BV)
|
||||
let is_bv_to_int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT)
|
||||
let is_int2bv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_INT2BV)
|
||||
let is_bv2int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT)
|
||||
let is_bv_carry ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CARRY)
|
||||
let is_bv_xor3 ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_XOR3)
|
||||
let get_size (x : sort ) = Z3native.get_bv_sort_size (Sort.gnc x) (Sort.gno x)
|
||||
|
|
@ -1847,6 +1847,7 @@ struct
|
|||
(sort_of_ptr ctx (Z3native.mk_fpa_sort_quadruple (context_gno ctx)))
|
||||
let mk_sort_128 ( ctx : context ) =
|
||||
(sort_of_ptr ctx (Z3native.mk_fpa_sort_128 (context_gno ctx)))
|
||||
|
||||
let mk_nan ( ctx : context ) ( s : sort ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_nan (context_gno ctx) (Sort.gno s)))
|
||||
let mk_inf ( ctx : context ) ( s : sort ) ( negative : bool ) =
|
||||
|
|
@ -1961,11 +1962,11 @@ struct
|
|||
expr_of_ptr ctx (Z3native.mk_fpa_to_fp_signed (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s))
|
||||
let mk_to_fp_unsigned ( ctx : context ) ( rm : expr) ( t : expr ) ( s : sort ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_to_fp_unsigned (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s))
|
||||
let mk_to_fp_ubv ( ctx : context ) ( rm : expr) ( t : expr ) ( size : int ) =
|
||||
let mk_to_ubv ( ctx : context ) ( rm : expr) ( t : expr ) ( size : int ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_to_ubv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size)
|
||||
let mk_to_fp_sbv ( ctx : context ) ( rm : expr) ( t : expr ) ( size : int ) =
|
||||
let mk_to_sbv ( ctx : context ) ( rm : expr) ( t : expr ) ( size : int ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_to_sbv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size)
|
||||
let mk_to_fp_real ( ctx : context ) ( t : expr ) =
|
||||
let mk_to_real ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_to_real (context_gno ctx) (Expr.gno t))
|
||||
|
||||
let get_ebits ( ctx : context ) ( s : sort ) =
|
||||
|
|
@ -1983,8 +1984,8 @@ struct
|
|||
|
||||
let mk_to_ieee_bv ( ctx : context ) ( t : expr ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_to_ieee_bv (context_gno ctx) (Expr.gno t)))
|
||||
let mk_to_fp_real_int ( ctx : context ) ( rm : expr ) ( exponent : expr ) ( significand : expr ) ( s : sort) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_to_fp_real_int (context_gno ctx) (Expr.gno rm) (Expr.gno exponent) (Expr.gno significand) (Sort.gno s)))
|
||||
let mk_to_fp_int_real ( ctx : context ) ( rm : expr ) ( exponent : expr ) ( significand : expr ) ( s : sort ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_to_fp_int_real (context_gno ctx) (Expr.gno rm) (Expr.gno exponent) (Expr.gno significand) (Sort.gno s)))
|
||||
|
||||
let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1183,7 +1183,6 @@ sig
|
|||
|
||||
(** Coerce an integer to a real.
|
||||
|
||||
|
||||
There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
|
||||
|
||||
You can take the floor of a real by creating an auxiliary integer Term [k] and
|
||||
|
|
@ -1193,7 +1192,6 @@ sig
|
|||
|
||||
(** Create an n-bit bit-vector from an integer argument.
|
||||
|
||||
|
||||
NB. This function is essentially treated as uninterpreted.
|
||||
So you cannot expect Z3 to precisely reflect the semantics of this function
|
||||
when solving constraints with this function.
|
||||
|
|
@ -1319,10 +1317,10 @@ sig
|
|||
val is_modulus : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether the term is a coercion of integer to real (unary) *)
|
||||
val is_inttoreal : Expr.expr -> bool
|
||||
val is_int2real : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether the term is a coercion of real to integer (unary) *)
|
||||
val is_real_to_int : Expr.expr -> bool
|
||||
val is_real2int : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether the term is a check that tests whether a real is integral (unary) *)
|
||||
val is_real_is_int : Expr.expr -> bool
|
||||
|
|
@ -1522,19 +1520,15 @@ sig
|
|||
Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. *)
|
||||
val is_bv_rotaterightextended : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether the term is a coercion from integer to bit-vector
|
||||
This function is not supported by the decision procedures. Only the most
|
||||
rudimentary simplification rules are applied to this function. *)
|
||||
|
||||
(** Indicates whether the term is a coercion from bit-vector to integer
|
||||
This function is not supported by the decision procedures. Only the most
|
||||
rudimentary simplification rules are applied to this function. *)
|
||||
val is_int_to_bv : Expr.expr -> bool
|
||||
val is_int2bv : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether the term is a coercion from integer to bit-vector
|
||||
This function is not supported by the decision procedures. Only the most
|
||||
rudimentary simplification rules are applied to this function. *)
|
||||
val is_bv_to_int : Expr.expr -> bool
|
||||
val is_bv2int : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether the term is a bit-vector carry
|
||||
Compute the carry bit in a full-adder. The meaning is given by the
|
||||
|
|
@ -1832,7 +1826,7 @@ end
|
|||
|
||||
(** Floating-Point Arithmetic *)
|
||||
module FloatingPoint :
|
||||
sig
|
||||
sig
|
||||
|
||||
(** Rounding Modes *)
|
||||
module RoundingMode :
|
||||
|
|
@ -2129,13 +2123,13 @@ module FloatingPoint :
|
|||
val mk_to_fp_unsigned : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
|
||||
|
||||
(** C1onversion of a floating-point term into an unsigned bit-vector. *)
|
||||
val mk_to_fp_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
|
||||
val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
|
||||
|
||||
(** Conversion of a floating-point term into a signed bit-vector. *)
|
||||
val mk_to_fp_sbv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
|
||||
val mk_to_sbv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
|
||||
|
||||
(** Conversion of a floating-point term into a real-numbered term. *)
|
||||
val mk_to_fp_real : context -> Expr.expr -> Expr.expr
|
||||
val mk_to_real : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. *)
|
||||
val get_ebits : context -> Sort.sort -> int
|
||||
|
|
@ -2159,11 +2153,11 @@ module FloatingPoint :
|
|||
val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. *)
|
||||
val mk_to_fp_real_int : context -> Expr.expr -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
|
||||
val mk_to_fp_int_real : context -> Expr.expr -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
|
||||
|
||||
(** The string representation of a numeral *)
|
||||
val numeral_to_string : Expr.expr -> string
|
||||
end
|
||||
end
|
||||
|
||||
|
||||
(** Functions to manipulate proof expressions *)
|
||||
|
|
|
|||
Loading…
Reference in a new issue