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