mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
added FPA ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
89bfbd38c8
commit
65ccc9a8ea
|
|
@ -19,6 +19,7 @@ open Z3.Arithmetic.Integer
|
|||
open Z3.Arithmetic.Real
|
||||
open Z3.BitVector
|
||||
|
||||
|
||||
exception TestFailedException of string
|
||||
|
||||
(**
|
||||
|
|
@ -73,7 +74,6 @@ let model_converter_test ( ctx : context ) =
|
|||
*)
|
||||
let basic_tests ( ctx : context ) =
|
||||
Printf.printf "BasicTests\n" ;
|
||||
(* let qi = (mk_int ctx 1) in *)
|
||||
let fname = (mk_string ctx "f") in
|
||||
let x = (mk_string ctx "x") in
|
||||
let y = (mk_string ctx "y") in
|
||||
|
|
@ -167,8 +167,8 @@ let basic_tests ( ctx : context ) =
|
|||
let rn = Real.mk_numeral_nd ctx 42 43 in
|
||||
let inum = (get_numerator rn) in
|
||||
let iden = get_denominator rn in
|
||||
Printf.printf "Numerator: %s Denominator: %s\n" (Real.to_string inum) (Real.to_string iden) ;
|
||||
if ((Real.to_string inum) <> "42" || (Real.to_string iden) <> "43") then
|
||||
Printf.printf "Numerator: %s Denominator: %s\n" (Real.numeral_to_string inum) (Real.numeral_to_string iden) ;
|
||||
if ((Real.numeral_to_string inum) <> "42" || (Real.numeral_to_string iden) <> "43") then
|
||||
raise (TestFailedException "")
|
||||
else
|
||||
Printf.printf "Test passed.\n"
|
||||
|
|
@ -190,7 +190,7 @@ let basic_tests ( ctx : context ) =
|
|||
(* Error handling test. *)
|
||||
try (
|
||||
let i = Integer.mk_numeral_s ctx "1/2" in
|
||||
raise (TestFailedException (to_string i)) (* unreachable *)
|
||||
raise (TestFailedException (numeral_to_string i)) (* unreachable *)
|
||||
)
|
||||
with Z3native.Exception(_) -> (
|
||||
Printf.printf "Exception caught, OK.\n"
|
||||
|
|
@ -199,7 +199,7 @@ let basic_tests ( ctx : context ) =
|
|||
(**
|
||||
A basic example of how to use quantifiers.
|
||||
**)
|
||||
let quantifierExample1 ( ctx : context ) =
|
||||
let quantifier_example1 ( ctx : context ) =
|
||||
Printf.printf "QuantifierExample\n" ;
|
||||
let is = (Integer.mk_sort ctx) in
|
||||
let types = [ is; is; is ] in
|
||||
|
|
@ -239,6 +239,82 @@ let quantifierExample1 ( ctx : context ) =
|
|||
else if (is_const (Quantifier.expr_of_quantifier x)) then
|
||||
raise (TestFailedException "") (* unreachable *)
|
||||
|
||||
|
||||
open Z3.FloatingPoint
|
||||
|
||||
(**
|
||||
A basic example of floating point arithmetic
|
||||
**)
|
||||
let fpa_example ( ctx : context ) =
|
||||
Printf.printf "FPAExample\n" ;
|
||||
let double_sort = (FloatingPoint.mk_sort_double ctx) in
|
||||
let rm_sort = (FloatingPoint.RoundingMode.mk_sort ctx) in
|
||||
|
||||
(** Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode). *)
|
||||
let s_rm = (mk_string ctx "rm") in
|
||||
let rm = (mk_const ctx s_rm rm_sort) in
|
||||
let s_x = (mk_string ctx "x") in
|
||||
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 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 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))
|
||||
(* 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); *)
|
||||
|
||||
|
||||
let _ =
|
||||
try (
|
||||
if not (Log.open_ "z3.log") then
|
||||
|
|
@ -259,7 +335,8 @@ let _ =
|
|||
Printf.printf "int sort: %s\n" (Sort.to_string ints);
|
||||
Printf.printf "real sort: %s\n" (Sort.to_string rs);
|
||||
basic_tests ctx ;
|
||||
quantifierExample1 ctx ;
|
||||
quantifier_example1 ctx ;
|
||||
fpa_example ctx ;
|
||||
Printf.printf "Disposing...\n";
|
||||
Gc.full_major ()
|
||||
);
|
||||
|
|
|
|||
|
|
@ -159,7 +159,7 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I
|
|||
|
||||
# Mapping to ML types
|
||||
Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
|
||||
STRING : 'string', STRING_PTR : 'char**',
|
||||
FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
|
||||
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' }
|
||||
|
||||
next_type_id = FIRST_OBJ_ID
|
||||
|
|
|
|||
206
src/api/ml/z3.ml
206
src/api/ml/z3.ml
|
|
@ -362,7 +362,9 @@ struct
|
|||
| REAL_SORT
|
||||
| UNINTERPRETED_SORT
|
||||
| FINITE_DOMAIN_SORT
|
||||
| RELATION_SORT -> Sort(q)
|
||||
| RELATION_SORT
|
||||
| FLOATING_POINT_SORT
|
||||
| ROUNDING_MODE_SORT -> Sort(q)
|
||||
| UNKNOWN_SORT -> raise (Z3native.Exception "Unknown sort kind encountered")
|
||||
|
||||
let ast_of_sort s = match s with Sort(x) -> x
|
||||
|
|
@ -745,7 +747,8 @@ end = struct
|
|||
Expr(z3_native_object_of_ast_ptr ctx no)
|
||||
else
|
||||
if (Z3native.is_numeral_ast (context_gno ctx) no) then
|
||||
if (sk == INT_SORT || sk == REAL_SORT || sk == BV_SORT) then
|
||||
if (sk == INT_SORT || sk == REAL_SORT || sk == BV_SORT ||
|
||||
sk == FLOATING_POINT_SORT || sk == ROUNDING_MODE_SORT) then
|
||||
Expr(z3_native_object_of_ast_ptr ctx no)
|
||||
else
|
||||
raise (Z3native.Exception "Unsupported numeral object")
|
||||
|
|
@ -1507,7 +1510,7 @@ struct
|
|||
(Big_int.big_int_of_string s)
|
||||
else raise (Z3native.Exception "Conversion failed.")
|
||||
|
||||
let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
|
||||
let mk_const ( ctx : context ) ( name : Symbol.symbol ) =
|
||||
Expr.mk_const ctx name (mk_sort ctx)
|
||||
|
|
@ -1554,7 +1557,7 @@ struct
|
|||
let to_decimal_string ( x : expr ) ( precision : int ) =
|
||||
Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision
|
||||
|
||||
let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
|
||||
let mk_const ( ctx : context ) ( name : Symbol.symbol ) =
|
||||
Expr.mk_const ctx name (mk_sort ctx)
|
||||
|
|
@ -1591,7 +1594,7 @@ struct
|
|||
let to_decimal_string ( x : expr ) ( precision : int ) =
|
||||
Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision
|
||||
|
||||
let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
end
|
||||
end
|
||||
|
||||
|
|
@ -1692,7 +1695,7 @@ struct
|
|||
let (r, v) = Z3native.get_numeral_int (Expr.gnc x) (Expr.gno x) in
|
||||
if r then v
|
||||
else raise (Z3native.Exception "Conversion failed.")
|
||||
let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( size : int ) =
|
||||
Expr.mk_const ctx name (mk_sort ctx size)
|
||||
let mk_const_s ( ctx : context ) ( name : string ) ( size : int ) =
|
||||
|
|
@ -1796,6 +1799,197 @@ struct
|
|||
end
|
||||
|
||||
|
||||
module FloatingPoint =
|
||||
struct
|
||||
module RoundingMode =
|
||||
struct
|
||||
let mk_sort ( ctx : context ) =
|
||||
(sort_of_ptr ctx (Z3native.mk_fpa_rounding_mode_sort (context_gno ctx)))
|
||||
let is_fprm ( x : expr ) =
|
||||
(Sort.get_sort_kind (Expr.get_sort(x))) == ROUNDING_MODE_SORT
|
||||
let mk_round_nearest_ties_to_even ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_round_nearest_ties_to_even (context_gno ctx)))
|
||||
let mk_rne ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_rne (context_gno ctx)))
|
||||
let mk_round_nearest_ties_to_away ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_round_nearest_ties_to_away (context_gno ctx)))
|
||||
let mk_rna ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_rna (context_gno ctx)))
|
||||
let mk_round_toward_positive ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_round_toward_positive (context_gno ctx)))
|
||||
let mk_rtp ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_rtp (context_gno ctx)))
|
||||
let mk_round_toward_negative ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_round_toward_negative (context_gno ctx)))
|
||||
let mk_rtn ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_rtn (context_gno ctx)))
|
||||
let mk_round_toward_zero ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_round_toward_zero (context_gno ctx)))
|
||||
let mk_rtz ( ctx : context ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_rtz (context_gno ctx)))
|
||||
end
|
||||
|
||||
let mk_sort ( ctx : context ) ( ebits : int ) ( sbits : int ) =
|
||||
(sort_of_ptr ctx (Z3native.mk_fpa_sort (context_gno ctx) ebits sbits))
|
||||
let mk_sort_half ( ctx : context ) =
|
||||
(sort_of_ptr ctx (Z3native.mk_fpa_sort_half (context_gno ctx)))
|
||||
let mk_sort_16 ( ctx : context ) =
|
||||
(sort_of_ptr ctx (Z3native.mk_fpa_sort_16 (context_gno ctx)))
|
||||
let mk_sort_single ( ctx : context ) =
|
||||
(sort_of_ptr ctx (Z3native.mk_fpa_sort_single (context_gno ctx)))
|
||||
let mk_sort_32 ( ctx : context ) =
|
||||
(sort_of_ptr ctx (Z3native.mk_fpa_sort_32 (context_gno ctx)))
|
||||
let mk_sort_double ( ctx : context ) =
|
||||
(sort_of_ptr ctx (Z3native.mk_fpa_sort_double (context_gno ctx)))
|
||||
let mk_sort_64 ( ctx : context ) =
|
||||
(sort_of_ptr ctx (Z3native.mk_fpa_sort_64 (context_gno ctx)))
|
||||
let mk_sort_quadruple ( ctx : context ) =
|
||||
(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 ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_inf (context_gno ctx) (Sort.gno s) negative))
|
||||
let mk_zero ( ctx : context ) ( s : sort ) ( negative : bool ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_zero (context_gno ctx) (Sort.gno s) negative))
|
||||
|
||||
let mk_fp ( ctx : context ) ( sign : expr ) ( exponent : expr ) ( significand : expr ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_fp (context_gno ctx) (Expr.gno sign) (Expr.gno exponent) (Expr.gno significand)))
|
||||
let mk_numeral_f ( ctx : context ) ( value : float ) ( s : sort ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_numeral_double (context_gno ctx) value (Sort.gno s)))
|
||||
let mk_numeral_i ( ctx : context ) ( value : int ) ( s : sort ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_numeral_int (context_gno ctx) value (Sort.gno s)))
|
||||
let mk_numeral_i_u ( ctx : context ) ( sign : bool ) ( exponent : int ) ( significand : int ) ( s : sort ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_fpa_numeral_int64_uint64 (context_gno ctx) sign exponent significand (Sort.gno s)))
|
||||
let mk_numeral_s ( ctx : context ) ( v : string ) ( s : sort ) =
|
||||
(expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno s)))
|
||||
|
||||
let is_fp ( x : expr ) = (Sort.get_sort_kind (Expr.get_sort x)) == FLOATING_POINT_SORT
|
||||
let is_abs ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_ABS)
|
||||
let is_neg ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_NEG)
|
||||
let is_add ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_ADD)
|
||||
let is_sub ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_SUB)
|
||||
let is_mul ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_MUL)
|
||||
let is_div ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_DIV)
|
||||
let is_fma ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_FMA)
|
||||
let is_sqrt ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_SQRT)
|
||||
let is_rem ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_REM)
|
||||
let is_round_to_integral ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_ROUND_TO_INTEGRAL)
|
||||
let is_min ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_MIN)
|
||||
let is_max ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_MAX)
|
||||
let is_leq ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_LE)
|
||||
let is_lt ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_LT)
|
||||
let is_geq ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_GE)
|
||||
let is_gt ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_GT)
|
||||
let is_eq ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_EQ)
|
||||
let is_is_normal ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_NORMAL)
|
||||
let is_is_subnormal ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_SUBNORMAL)
|
||||
let is_is_zero ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_ZERO)
|
||||
let is_is_infinite ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_INF)
|
||||
let is_is_nan ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_NAN)
|
||||
let is_is_negative ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_NEGATIVE)
|
||||
let is_is_positive ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_POSITIVE)
|
||||
let is_to_fp ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_FP)
|
||||
let is_to_fp_unsigned ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_FP_UNSIGNED)
|
||||
let is_to_ubv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_UBV)
|
||||
let is_to_sbv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_SBV)
|
||||
let is_to_real ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_REAL)
|
||||
let is_to_ieee_bv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_IEEE_BV)
|
||||
|
||||
let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( s : sort ) =
|
||||
Expr.mk_const ctx name s
|
||||
let mk_const_s ( ctx : context ) ( name : string ) ( s : sort ) =
|
||||
mk_const ctx (Symbol.mk_string ctx name) s
|
||||
|
||||
let mk_abs ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_abs (context_gno ctx) (Expr.gno t))
|
||||
let mk_neg ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_neg (context_gno ctx) (Expr.gno t))
|
||||
let mk_add ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_add (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_sub ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_sub (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_mul ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_mul (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_div ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_div (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_fma ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_fma (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2) (Expr.gno t3))
|
||||
let mk_sqrt ( ctx : context ) ( rm : expr ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_sqrt (context_gno ctx) (Expr.gno rm) (Expr.gno t))
|
||||
let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_rem (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_round_to_integral ( ctx : context ) ( rm : expr ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_round_to_integral (context_gno ctx) (Expr.gno rm) (Expr.gno t))
|
||||
let mk_min ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_min (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_max ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_max (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_leq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_leq (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_lt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_geq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_geq (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_gt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_eq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_eq (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
|
||||
let mk_is_normal ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_is_normal (context_gno ctx) (Expr.gno t))
|
||||
let mk_is_subnormal ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_is_subnormal (context_gno ctx) (Expr.gno t))
|
||||
let mk_is_zero ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_is_zero (context_gno ctx) (Expr.gno t))
|
||||
let mk_is_infinite ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_is_infinite (context_gno ctx) (Expr.gno t))
|
||||
let mk_is_nan ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_is_nan (context_gno ctx) (Expr.gno t))
|
||||
let mk_is_negative ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_is_negative (context_gno ctx) (Expr.gno t))
|
||||
let mk_is_positive ( ctx : context ) ( t : expr ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_is_positive (context_gno ctx) (Expr.gno t))
|
||||
let mk_to_fp_bv ( ctx : context ) ( t : expr ) ( s : sort ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_to_fp_bv (context_gno ctx) (Expr.gno t) (Sort.gno s))
|
||||
let mk_to_fp_float ( ctx : context ) ( rm : expr) ( t : expr ) ( s : sort ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_to_fp_float (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s))
|
||||
let mk_to_fp_real ( ctx : context ) ( rm : expr ) ( t : expr ) ( s : sort ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_to_fp_real (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s))
|
||||
let mk_to_fp_signed ( ctx : context ) ( rm : expr) ( t : expr ) ( s : sort ) =
|
||||
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 ) =
|
||||
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 ) =
|
||||
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 ) =
|
||||
expr_of_ptr ctx (Z3native.mk_fpa_to_real (context_gno ctx) (Expr.gno t))
|
||||
|
||||
let get_ebits ( ctx : context ) ( s : sort ) =
|
||||
(Z3native.fpa_get_ebits (context_gno ctx) (Sort.gno s))
|
||||
let get_sbits ( ctx : context ) ( s : sort ) =
|
||||
(Z3native.fpa_get_sbits (context_gno ctx) (Sort.gno s))
|
||||
let get_numeral_sign ( ctx : context ) ( t : expr ) =
|
||||
(Z3native.fpa_get_numeral_sign (context_gno ctx) (Expr.gno t))
|
||||
let get_numeral_significand_string ( ctx : context ) ( t : expr ) =
|
||||
(Z3native.fpa_get_numeral_significand_string (context_gno ctx) (Expr.gno t))
|
||||
let get_numeral_exponent_string ( ctx : context ) ( t : expr ) =
|
||||
(Z3native.fpa_get_numeral_exponent_string (context_gno ctx) (Expr.gno t))
|
||||
let get_numeral_exponent_int ( ctx : context ) ( t : expr ) =
|
||||
(Z3native.fpa_get_numeral_exponent_int64 (context_gno ctx) (Expr.gno t))
|
||||
|
||||
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 numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
|
||||
end
|
||||
|
||||
|
||||
module Proof =
|
||||
struct
|
||||
let is_true ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRUE)
|
||||
|
|
|
|||
|
|
@ -1157,8 +1157,8 @@ sig
|
|||
(** Get a big_int from an integer numeral *)
|
||||
val get_big_int : Expr.expr -> Big_int.big_int
|
||||
|
||||
(** Returns a string representation of the numeral. *)
|
||||
val to_string : Expr.expr -> string
|
||||
(** Returns a string representation of a numeral. *)
|
||||
val numeral_to_string : Expr.expr -> string
|
||||
|
||||
(** Creates an integer constant. *)
|
||||
val mk_const : context -> Symbol.symbol -> Expr.expr
|
||||
|
|
@ -1221,8 +1221,8 @@ sig
|
|||
The result has at most as many decimal places as indicated by the int argument.*)
|
||||
val to_decimal_string : Expr.expr-> int -> string
|
||||
|
||||
(** Returns a string representation of the numeral. *)
|
||||
val to_string : Expr.expr-> string
|
||||
(** Returns a string representation of a numeral. *)
|
||||
val numeral_to_string : Expr.expr-> string
|
||||
|
||||
(** Creates a real constant. *)
|
||||
val mk_const : context -> Symbol.symbol -> Expr.expr
|
||||
|
|
@ -1271,8 +1271,8 @@ sig
|
|||
The result has at most as many decimal places as the int argument provided.*)
|
||||
val to_decimal_string : Expr.expr -> int -> string
|
||||
|
||||
(** Returns a string representation of the numeral. *)
|
||||
val to_string : Expr.expr -> string
|
||||
(** Returns a string representation of a numeral. *)
|
||||
val numeral_to_string : Expr.expr -> string
|
||||
end
|
||||
end
|
||||
|
||||
|
|
@ -1551,8 +1551,8 @@ sig
|
|||
(** Retrieve the int value. *)
|
||||
val get_int : Expr.expr -> int
|
||||
|
||||
(** Returns a string representation of the numeral. *)
|
||||
val to_string : Expr.expr -> string
|
||||
(** Returns a string representation of a numeral. *)
|
||||
val numeral_to_string : Expr.expr -> string
|
||||
|
||||
(** Creates a bit-vector constant. *)
|
||||
val mk_const : context -> Symbol.symbol -> int -> Expr.expr
|
||||
|
|
@ -1830,6 +1830,342 @@ sig
|
|||
val mk_numeral : context -> string -> int -> Expr.expr
|
||||
end
|
||||
|
||||
(** Floating-Point Arithmetic *)
|
||||
module FloatingPoint :
|
||||
sig
|
||||
|
||||
(** Rounding Modes *)
|
||||
module RoundingMode :
|
||||
sig
|
||||
(** Create the RoundingMode sort. *)
|
||||
val mk_sort : context -> Sort.sort
|
||||
|
||||
(** Indicates whether the terms is of floating-point rounding mode sort. *)
|
||||
val is_fprm : Expr.expr -> bool
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *)
|
||||
val mk_round_nearest_ties_to_even : context -> Expr.expr
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *)
|
||||
val mk_rne : context -> Expr.expr
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *)
|
||||
val mk_round_nearest_ties_to_away : context -> Expr.expr
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *)
|
||||
val mk_rna : context -> Expr.expr
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *)
|
||||
val mk_round_toward_positive : context -> Expr.expr
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *)
|
||||
val mk_rtp : context -> Expr.expr
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *)
|
||||
val mk_round_toward_negative : context -> Expr.expr
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *)
|
||||
val mk_rtn : context -> Expr.expr
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *)
|
||||
val mk_round_toward_zero : context -> Expr.expr
|
||||
|
||||
(** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *)
|
||||
val mk_rtz : context -> Expr.expr
|
||||
end
|
||||
|
||||
(** Create a FloatingPoint sort. *)
|
||||
val mk_sort : context -> int -> int -> Sort.sort
|
||||
|
||||
(** Create the half-precision (16-bit) FloatingPoint sort.*)
|
||||
val mk_sort_half : context -> Sort.sort
|
||||
|
||||
(** Create the half-precision (16-bit) FloatingPoint sort. *)
|
||||
val mk_sort_16 : context -> Sort.sort
|
||||
|
||||
(** Create the single-precision (32-bit) FloatingPoint sort.*)
|
||||
val mk_sort_single : context -> Sort.sort
|
||||
|
||||
(** Create the single-precision (32-bit) FloatingPoint sort. *)
|
||||
val mk_sort_32 : context -> Sort.sort
|
||||
|
||||
(** Create the double-precision (64-bit) FloatingPoint sort. *)
|
||||
val mk_sort_double : context -> Sort.sort
|
||||
|
||||
(** Create the double-precision (64-bit) FloatingPoint sort. *)
|
||||
val mk_sort_64 : context -> Sort.sort
|
||||
|
||||
(** Create the quadruple-precision (128-bit) FloatingPoint sort. *)
|
||||
val mk_sort_quadruple : context -> Sort.sort
|
||||
|
||||
(** Create the quadruple-precision (128-bit) FloatingPoint sort. *)
|
||||
val mk_sort_128 : context -> Sort.sort
|
||||
|
||||
(** Create a floating-point NaN of a given FloatingPoint sort. *)
|
||||
val mk_nan : context -> Sort.sort -> Expr.expr
|
||||
|
||||
(** Create a floating-point infinity of a given FloatingPoint sort. *)
|
||||
val mk_inf : context -> Sort.sort -> bool -> Expr.expr
|
||||
|
||||
(** Create a floating-point zero of a given FloatingPoint sort. *)
|
||||
val mk_zero : context -> Sort.sort -> bool -> Expr.expr
|
||||
|
||||
(** Create an expression of FloatingPoint sort from three bit-vector expressions.
|
||||
|
||||
This is the operator named `fp' in the SMT FP theory definition.
|
||||
Note that \c sign is required to be a bit-vector of size 1. Significand and exponent
|
||||
are required to be greater than 1 and 2 respectively. The FloatingPoint sort
|
||||
of the resulting expression is automatically determined from the bit-vector sizes
|
||||
of the arguments. *)
|
||||
val mk_fp : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Create a numeral of FloatingPoint sort from a float.
|
||||
|
||||
This function is used to create numerals that fit in a float value.
|
||||
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. *)
|
||||
val mk_numeral_f : context -> float -> Sort.sort -> Expr.expr
|
||||
|
||||
(** Create a numeral of FloatingPoint sort from a signed integer. *)
|
||||
val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr
|
||||
|
||||
(** 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
|
||||
|
||||
(** Create a numeral of FloatingPoint sort from a string *)
|
||||
val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr
|
||||
|
||||
(** Indicates whether the terms is of floating-point sort. *)
|
||||
val is_fp : Expr.expr -> bool
|
||||
|
||||
|
||||
(** Indicates whether an expression is a floating-point abs expression *)
|
||||
val is_abs : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point neg expression *)
|
||||
val is_neg : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point add expression *)
|
||||
val is_add : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point sub expression *)
|
||||
val is_sub : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point mul expression *)
|
||||
val is_mul : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point div expression *)
|
||||
val is_div : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point fma expression *)
|
||||
val is_fma : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point sqrt expression *)
|
||||
val is_sqrt : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point rem expression *)
|
||||
val is_rem : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point round_to_integral expression *)
|
||||
val is_round_to_integral : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point min expression *)
|
||||
val is_min : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point max expression *)
|
||||
val is_max : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point leq expression *)
|
||||
val is_leq : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point lt expression *)
|
||||
val is_lt : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point geqexpression *)
|
||||
val is_geq : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point gt expression *)
|
||||
val is_gt : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point eq expression *)
|
||||
val is_eq : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point is_normal expression *)
|
||||
val is_is_normal : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point is_subnormal expression *)
|
||||
val is_is_subnormal : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point is_zero expression *)
|
||||
val is_is_zero : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point is_infinite expression *)
|
||||
val is_is_infinite : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point is_nan expression *)
|
||||
val is_is_nan : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point is_negative expression *)
|
||||
val is_is_negative : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point is_positive expression *)
|
||||
val is_is_positive : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point to_fp expression *)
|
||||
val is_to_fp : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point to_fp_unsigned expression *)
|
||||
val is_to_fp_unsigned : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point to_ubv expression *)
|
||||
val is_to_ubv : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point to_sbv expression *)
|
||||
val is_to_sbv : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point to_real expression *)
|
||||
val is_to_real : Expr.expr -> bool
|
||||
|
||||
(** Indicates whether an expression is a floating-point to_ieee_bv expression *)
|
||||
val is_to_ieee_bv : Expr.expr -> bool
|
||||
|
||||
|
||||
(** Returns a string representation of a numeral. *)
|
||||
val numeral_to_string : Expr.expr -> string
|
||||
|
||||
(** Creates a floating-point constant. *)
|
||||
val mk_const : context -> Symbol.symbol -> Sort.sort -> Expr.expr
|
||||
|
||||
(** Creates a floating-point constant. *)
|
||||
val mk_const_s : context -> string -> Sort.sort -> Expr.expr
|
||||
|
||||
(** Floating-point absolute value *)
|
||||
val mk_abs : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point negation *)
|
||||
val mk_neg : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point addition *)
|
||||
val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point subtraction *)
|
||||
val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point multiplication *)
|
||||
val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point division *)
|
||||
val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point fused multiply-add. *)
|
||||
val mk_fma : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point square root *)
|
||||
val mk_sqrt : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point remainder *)
|
||||
val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point roundToIntegral.
|
||||
|
||||
Rounds a floating-point number to the closest integer,
|
||||
again represented as a floating-point number. *)
|
||||
val mk_round_to_integral : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Minimum of floating-point numbers. *)
|
||||
val mk_min : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Maximum of floating-point numbers. *)
|
||||
val mk_max : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point less than or equal. *)
|
||||
val mk_leq : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point less than. *)
|
||||
val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point greater than or equal. *)
|
||||
val mk_geq : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point greater than. *)
|
||||
val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Floating-point equality. *)
|
||||
val mk_eq : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Predicate indicating whether t is a normal floating-point number. *)
|
||||
val mk_is_normal : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Predicate indicating whether t is a subnormal floating-point number. *)
|
||||
val mk_is_subnormal : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero. *)
|
||||
val mk_is_zero : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Predicate indicating whether t is a floating-point number representing +oo or -oo. *)
|
||||
val mk_is_infinite : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Predicate indicating whether t is a NaN. *)
|
||||
val mk_is_nan : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Predicate indicating whether t is a negative floating-point number. *)
|
||||
val mk_is_negative : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Predicate indicating whether t is a positive floating-point number. *)
|
||||
val mk_is_positive : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. *)
|
||||
val mk_to_fp_bv : context -> Expr.expr -> Sort.sort -> Expr.expr
|
||||
|
||||
(** Conversion of a FloatingPoint term into another term of different FloatingPoint sort. *)
|
||||
val mk_to_fp_float : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
|
||||
|
||||
(** Conversion of a term of real sort into a term of FloatingPoint sort. *)
|
||||
val mk_to_fp_real : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
|
||||
|
||||
(** Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort. *)
|
||||
val mk_to_fp_signed : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
|
||||
|
||||
(** Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort. *)
|
||||
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
|
||||
|
||||
(** Conversion of a floating-point term into a signed bit-vector. *)
|
||||
val mk_to_fp_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
|
||||
|
||||
(** Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. *)
|
||||
val get_ebits : context -> Sort.sort -> int
|
||||
|
||||
(** Retrieves the number of bits reserved for the significand in a FloatingPoint sort. *)
|
||||
val get_sbits : context -> Sort.sort -> int
|
||||
|
||||
(** Retrieves the sign of a floating-point literal. *)
|
||||
val get_numeral_sign : context -> Expr.expr -> bool * int
|
||||
|
||||
(** Return the significand value of a floating-point numeral as a string. *)
|
||||
val get_numeral_significand_string : context -> Expr.expr -> string
|
||||
|
||||
(** Return the exponent value of a floating-point numeral as a string *)
|
||||
val get_numeral_exponent_string : context -> Expr.expr -> string
|
||||
|
||||
(** Return the exponent value of a floating-point numeral as a signed integer *)
|
||||
val get_numeral_exponent_int : context -> Expr.expr -> bool * int
|
||||
|
||||
(** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *)
|
||||
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
|
||||
|
||||
(** The string representation of a numeral *)
|
||||
val numeral_to_string : Expr.expr -> string
|
||||
end
|
||||
|
||||
|
||||
(** Functions to manipulate proof expressions *)
|
||||
module Proof :
|
||||
sig
|
||||
|
|
|
|||
Loading…
Reference in a new issue