From 5c7d0380d3c2d5fba59d0da2f62f870feaf279cc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 24 Jan 2015 18:29:52 +0000 Subject: [PATCH] Fixes in the OCaml FPA API and example --- examples/ml/ml_example.ml | 93 ++--- scripts/mk_util.py | 2 +- src/api/ml/z3.ml | 25 +- src/api/ml/z3.mli | 754 +++++++++++++++++++------------------- 4 files changed, 436 insertions(+), 438 deletions(-) diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index 8a2d71d82..127a973aa 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -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)) - (* push(ctx); *) - (* Z3_assert_cnstr(ctx, c4); *) - (* check(ctx, Z3_L_TRUE); *) - (* Z3_pop(ctx, 1); *) + 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" + ); - (* // 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))) *) +(* 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 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 ( diff --git a/scripts/mk_util.py b/scripts/mk_util.py index af0c59355..2ed420c20 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 601da1cbc..fe78b65a6 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -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 ) = @@ -1857,11 +1858,11 @@ struct 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))) + (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))) + (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))) + (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))) @@ -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 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index ab2a14725..aa526417e 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -139,7 +139,7 @@ sig val get_size : ast_vector -> int (** Retrieves the i-th object in the vector. - @return An AST *) + @return An AST *) val get : ast_vector -> int -> ast (** Sets the i-th object in the vector. *) @@ -149,11 +149,11 @@ sig val resize : ast_vector -> int -> unit (** Add an ast to the back of the vector. The size - is increased by 1. *) + is increased by 1. *) val push : ast_vector -> ast -> unit (** Translates all ASTs in the vector to another context. - @return A new ASTVector *) + @return A new ASTVector *) val translate : ast_vector -> context -> ast_vector (** Retrieves a string representation of the vector. *) @@ -169,11 +169,11 @@ sig val mk_ast_map : context -> ast_map (** Checks whether the map contains a key. - @return True if the key in the map, false otherwise. *) + @return True if the key in the map, false otherwise. *) val contains : ast_map -> ast -> bool (** Finds the value associated with the key. - This function signs an error when the key is not a key in the map. *) + This function signs an error when the key is not a key in the map. *) val find : ast_map -> ast -> ast (** Stores or replaces a new key/value pair in the map. *) @@ -302,14 +302,14 @@ sig sig (** Parameters of func_decls *) type parameter = - P_Int of int + P_Int of int | P_Dbl of float | P_Sym of Symbol.symbol | P_Srt of Sort.sort | P_Ast of AST.ast | P_Fdl of func_decl | P_Rat of string - + (** The kind of the parameter. *) val get_kind : parameter -> Z3enums.parameter_kind @@ -723,7 +723,7 @@ sig (** The no-patterns. *) val get_no_patterns : quantifier -> Pattern.pattern list - (** The number of bound variables. *) + (** The number of bound variables. *) val get_num_bound : quantifier -> int (** The symbols for the bound variables. *) @@ -759,7 +759,7 @@ sig (** Create a Quantifier. *) val mk_quantifier : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier - (** A string representation of the quantifier. *) + (** A string representation of the quantifier. *) val to_string : quantifier -> string end @@ -1167,38 +1167,36 @@ sig val mk_const_s : context -> string -> Expr.expr (** Create an expression representing [t1 mod t2]. - The arguments must have int type. *) + The arguments must have int type. *) val mk_mod : context -> Expr.expr -> Expr.expr -> Expr.expr (** Create an expression representing [t1 rem t2]. - The arguments must have int type. *) + The arguments must have int type. *) val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr (** Create an integer numeral. *) val mk_numeral_s : context -> string -> Expr.expr (** Create an integer numeral. - @return A Term with the given value and sort Integer *) + @return A Term with the given value and sort Integer *) val mk_numeral_i : context -> int -> Expr.expr - (** 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 - and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1]. - The argument must be of integer sort. *) + (** 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 + and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1]. + The argument must be of integer sort. *) val mk_int2real : context -> Expr.expr -> Expr.expr - (** 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. - - The argument must be of integer sort. *) + (** 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. + + The argument must be of integer sort. *) val mk_int2bv : context -> int -> Expr.expr -> Expr.expr end @@ -1218,7 +1216,7 @@ sig val get_ratio : Expr.expr -> Ratio.ratio (** Returns a string representation in decimal notation. - The result has at most as many decimal places as indicated by the int argument.*) + 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 a numeral. *) @@ -1231,16 +1229,16 @@ sig val mk_const_s : context -> string -> Expr.expr (** Create a real numeral from a fraction. - @return A Term with rational value and sort Real - {!mk_numeral_s} *) + @return A Term with rational value and sort Real + {!mk_numeral_s} *) val mk_numeral_nd : context -> int -> int -> Expr.expr (** Create a real numeral. - @return A Term with the given value and sort Real *) + @return A Term with the given value and sort Real *) val mk_numeral_s : context -> string -> Expr.expr (** Create a real numeral. - @return A Term with the given value and sort Real *) + @return A Term with the given value and sort Real *) val mk_numeral_i : context -> int -> Expr.expr (** Creates an expression that checks whether a real number is an integer. *) @@ -1248,29 +1246,29 @@ sig (** Coerce a real to an integer. - The semantics of this function follows the SMT-LIB standard for the function to_int. - The argument must be of real sort. *) + The semantics of this function follows the SMT-LIB standard for the function to_int. + The argument must be of real sort. *) val mk_real2int : context -> Expr.expr -> Expr.expr (** Algebraic Numbers *) module AlgebraicNumber : sig (** Return a upper bound for a given real algebraic number. - The interval isolating the number is smaller than 1/10^precision. - {!is_algebraic_number} - @return A numeral Expr of sort Real *) + The interval isolating the number is smaller than 1/10^precision. + {!is_algebraic_number} + @return A numeral Expr of sort Real *) val to_upper : Expr.expr -> int -> Expr.expr - + (** Return a lower bound for the given real algebraic number. - The interval isolating the number is smaller than 1/10^precision. - {!is_algebraic_number} - @return A numeral Expr of sort Real *) + The interval isolating the number is smaller than 1/10^precision. + {!is_algebraic_number} + @return A numeral Expr of sort Real *) val to_lower : Expr.expr -> int -> Expr.expr - + (** Returns a string representation in decimal notation. - The result has at most as many decimal places as the int argument provided.*) + 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 a numeral. *) val numeral_to_string : Expr.expr -> string end @@ -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,339 +1826,339 @@ end (** Floating-Point Arithmetic *) module FloatingPoint : +sig + + (** Rounding Modes *) + module RoundingMode : sig + (** Create the RoundingMode sort. *) + val mk_sort : context -> Sort.sort - (** 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 - (** 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 a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) + val mk_round_nearest_ties_to_even : context -> Expr.expr - (** Create the quadruple-precision (128-bit) FloatingPoint sort. *) - val mk_sort_quadruple : context -> Sort.sort + (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) + val mk_rne : context -> Expr.expr - (** 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 RoundingMode sort which represents the NearestTiesToAway rounding mode. *) + val mk_round_nearest_ties_to_away : context -> 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 + (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) + val mk_rna : context -> Expr.expr - (** 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 + (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) + val mk_round_toward_positive : context -> Expr.expr - (** 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 + (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) + val mk_rtp : context -> 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 + (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) + val mk_round_toward_negative : context -> 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 + (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) + val mk_rtn : context -> 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 + (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) + val mk_round_toward_zero : context -> Expr.expr - (** 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 + (** 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_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr + + (** Conversion of a floating-point term into a signed bit-vector. *) + 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_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_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 + (** Functions to manipulate proof expressions *) module Proof : @@ -2654,7 +2648,7 @@ sig (** Function interpretations entries - An Entry object represents an element in the finite map used to a function interpretation. *) + An Entry object represents an element in the finite map used to a function interpretation. *) module FuncEntry : sig type func_entry @@ -2844,8 +2838,8 @@ sig val get_subgoal : apply_result -> int -> Goal.goal (** Convert a model for a subgoal into a model for the original - goal [g], that the ApplyResult was obtained from. - #return A model for [g] *) + goal [g], that the ApplyResult was obtained from. + #return A model for [g] *) val convert_model : apply_result -> int -> Model.model -> Model.model (** A string representation of the ApplyResult. *) @@ -2946,7 +2940,7 @@ sig type statistics (** Statistical data is organized into pairs of \[Key, Entry\], where every - Entry is either a floating point or integer value. + Entry is either a floating point or integer value. *) module Entry : sig @@ -2960,16 +2954,16 @@ sig (** The float-value of the entry. *) val get_float : statistics_entry -> float - + (** True if the entry is uint-valued. *) val is_int : statistics_entry -> bool - + (** True if the entry is float-valued. *) val is_float : statistics_entry -> bool - + (** The string representation of the the entry's value. *) val to_string_value : statistics_entry -> string - + (** The string representation of the entry (key and value) *) val to_string : statistics_entry -> string end