diff --git a/CHANGES.md b/CHANGES.md index 8ff9fe7cf5..22703c9a7f 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,9 @@ ## unreleased + - Support parsing and reasoning over most SMT-LIB FPA Theory symbols (except + fp.rem, fp.to_fp, and bv/fp conversion operations), usable with + `--enable-theory smt.float`. Add a prelude axiomatizing the semantics of the + FPA Theory symbols, adapted from Why3's generated axiomatization. (#1364) - Support the `int.pow2` function, which takes an integer `n` and computes `ae.pow_int 2 n` (#1365) - Support parsing of SMT-LIB FPA Theory literals and add the theory `smt.float` diff --git a/src/lib/dune b/src/lib/dune index b3771a7eb1..a0a4926056 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -37,7 +37,7 @@ ; reasoners Ac Arith Arrays_rel Bitv Ccx Shostak Relation Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel - Instances IntervalCalculus Intervals_intf Intervals_core Intervals + Fpa Fpa_rel Instances IntervalCalculus Intervals_intf Intervals_core Intervals Ite_rel Matching Matching_types Polynome Satml_frontend Satml Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Domains Domains_intf Rel_utils Bitlist diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index b9a064e8e9..7cb3095ad1 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -155,33 +155,39 @@ let builtin_term t = Dl.Typer.T.builtin_term t let builtin_ty t = Dl.Typer.T.builtin_ty t -let ty (ty_cst : DE.ty_cst) ty = - let name = get_basename ty_cst.path in - DStd.Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@ fun env s -> - builtin_ty @@ Dolmen_type.Base.app0 (module Dl.Typer.T) env s ty - let fpa_rounding_mode, rounding_modes, add_rounding_modes = - match DT.view Fpa_rounding.fpa_rounding_mode_dty with - | `App (`Generic ty_cst, []) -> - let constrs = Fpa_rounding.d_constrs in - let add_constrs map = - List.fold_left - (fun map (c : DE.term_cst) -> - let name = get_basename c.path in - DStd.Id.Map.add - { name = DStd.Name.simple name; ns = Term } - (fun env _ -> - builtin_term - @@ Dolmen_type.Base.term_app_cst (module Dl.Typer.T) env c) - map) - map constrs - in - Cache.store_ty ty_cst Fpa_rounding.fpa_rounding_mode; - ( Fpa_rounding.fpa_rounding_mode_dty, - constrs, - fun map -> - map |> ty ty_cst Fpa_rounding.fpa_rounding_mode_dty |> add_constrs ) - | _ -> assert false + let smt_constrs = + DE.Term.Const.Float. + [ "RNE", roundNearestTiesToEven; + "RNA", roundNearestTiesToAway; + "RTP", roundTowardPositive; + "RTN", roundTowardNegative; + "RTZ", roundTowardZero ] + in + let constrs = List.map snd smt_constrs in + let add_constrs map = + List.fold_left + (fun map (name, c) -> + DStd.Id.Map.add + { name = DStd.Name.simple name; ns = Term } + (fun env _ -> + builtin_term + @@ Dolmen_type.Base.term_app_cst (module Dl.Typer.T) env c) + map) + map smt_constrs + in + ( DE.Ty.roundingMode, + constrs, + fun map -> + map + |> DStd.Id.Map.add + { name = DStd.Name.simple "RoundingMode"; ns = Sort } + (fun env s -> + builtin_ty + @@ Dolmen_type.Base.app0 + (module Dl.Typer.T) + env s DE.Ty.roundingMode) + |> add_constrs ) module Const = struct open DE @@ -343,6 +349,16 @@ let smt_fpa_builtins = let ty = DT.arrow [DT.int] DT.int in DE.Id.mk ~name:"int.pow2" ~builtin:Int_pow2 (DStd.Path.global "int.pow2") ty in + let ae_float_cst = + let name = E.FP.Names.ae_float in + let ty = DT.(arrow [int; int; fpa_rounding_mode; real] real) in + DE.Id.mk ~name ~builtin:Float (DStd.Path.global name) ty + in + let sqrt_real_cst = + let name = "sqrt_real" in + let ty = DT.arrow [DT.real] DT.real in + DE.Id.mk ~name ~builtin:Sqrt_real (DStd.Path.global name) ty + in let other_builtins = DStd.Id.Map.empty |> add_rounding_modes in fun env s -> match s with @@ -369,6 +385,12 @@ let smt_fpa_builtins = | Id { ns = Term; name = Simple "int.pow2" } -> Dl.Typer.T.builtin_term @@ Dolmen_type.Base.term_app_cst (module Dl.Typer.T) env int_pow2_cst + | Id { ns = Term; name = Simple "ae.float" } -> + Dl.Typer.T.builtin_term + @@ Dolmen_type.Base.term_app_cst (module Dl.Typer.T) env ae_float_cst + | Id { ns = Term; name = Simple "sqrt_real" } -> + Dl.Typer.T.builtin_term + @@ Dolmen_type.Base.term_app_cst (module Dl.Typer.T) env sqrt_real_cst | Dl.Typer.T.Id id -> begin match DStd.Id.Map.find_exn id other_builtins env s with | e -> e @@ -439,6 +461,8 @@ let rec dty_to_ty ?(update = false) ?(is_var = false) dty = Ty.Tbitv n | `Float (e, s) when Options.get_smt_lib_fpa () -> Ty.Tfloat (e, s) | `App (`Builtin B.Unit, []) -> Ty.tunit + | `App (`Builtin (B.Float B.Float.RoundingMode), []) -> + Fpa_rounding.fpa_rounding_mode | `App (`Builtin _, [ty]) -> aux ty | `App (`Generic c, l) -> handle_ty_app ~update c l | `Var ty_v when update -> Cache.find_update_ty ty_v @@ -456,6 +480,11 @@ and handle_ty_app ?(update = false) ty_c l = match Cache.find_ty ty_c with | Tadt (hs, _) -> Tadt (hs, tyl) | Text (_, s) -> Text (tyl, s) + | Tvar { path = Absolute { name; _ } | Local { name; _ }; _ } as tv + when Compat.List.is_empty tyl && String.equal name E.FP.Names.t -> + (* To get the generic abstract float type from the axiomatization which is + stored as type varialbe `ae.fp.t`. *) + tv | _ -> assert false (** Handles a simple type declaration. *) @@ -482,13 +511,17 @@ let mk_ty_decl (ty_c : DE.ty_cst) = in let ty = Ty.t_adt ~body:(Some cs) ty_c tyvl in Cache.store_ty ty_c ty - | None | Some Abstract -> - let ty_params = - [] - (* List.init ty_c.id_ty.arity (fun _ -> Ty.fresh_tvar ()) *) - in - let ty = Ty.text ty_params ty_c in - Cache.store_ty ty_c ty + | None | Some Abstract -> ( + match ty_c with + | { path = Absolute { name; _ }; _ } + when Options.get_smt_lib_fpa () && String.equal name E.FP.Names.t -> + (* Storing the generic abstract float type from the axiomatization as a + type variable `ae.fp.t`, so that axioms defined for it can apply for + specific instances of the Float(es,sb) type. *) + Cache.store_ty ty_c (Ty.named_tvar E.FP.Names.t) + | _ -> + let ty = Ty.text [] ty_c in + Cache.store_ty ty_c ty) (** Handles term declaration by storing the eventual present type variables in the cache as well as the symbol associated to the term. *) @@ -779,23 +812,37 @@ let rec mk_expr ?(loc = Loc.dummy) ?(name_base = "") ?(toplevel = false) | B.Adt (Constructor _) -> let ty = dty_to_ty term_ty in E.mk_constr tcst [] ty - | B.Float cst when Options.get_smt_lib_fpa () -> begin + | B.Float cst -> begin match cst with - | Plus_infinity { e; s } -> E.float Fp_value.Plus_infinity e s - | Minus_infinity { e; s } -> E.float Fp_value.Minus_infinity e s - | Plus_zero { e; s } -> E.float Fp_value.Plus_zero e s - | Minus_zero { e; s } -> E.float Fp_value.Minus_zero e s - | NaN { e; s } -> E.float Fp_value.NaN e s - | RoundingMode | RoundNearestTiesToEven | RoundNearestTiesToAway - | RoundTowardPositive | RoundTowardNegative | RoundTowardZero | T _ - | Fp _ | Abs _ | Neg _ | Add _ | Sub _ | Mul _ | Div _ | Fma _ - | Sqrt _ | Rem _ | RoundToIntegral _ | Min _ | Max _ | Leq _ | Lt _ - | Geq _ | Gt _ | Eq _ | IsNormal _ | IsSubnormal _ | IsZero _ - | IsInfinite _ | IsNaN _ | IsNegative _ | IsPositive _ + | RoundNearestTiesToEven -> mk_rounding B.Float.RoundNearestTiesToEven + | RoundNearestTiesToAway -> mk_rounding B.Float.RoundNearestTiesToAway + | RoundTowardPositive -> mk_rounding B.Float.RoundTowardPositive + | RoundTowardNegative -> mk_rounding B.Float.RoundTowardNegative + | RoundTowardZero -> mk_rounding B.Float.RoundTowardZero + | Plus_infinity { e; s } when Options.get_smt_lib_fpa () -> + E.float Fp_value.Plus_infinity e s + | Minus_infinity { e; s } when Options.get_smt_lib_fpa () -> + E.float Fp_value.Minus_infinity e s + | Plus_zero { e; s } when Options.get_smt_lib_fpa () -> + E.float Fp_value.Plus_zero e s + | Minus_zero { e; s } when Options.get_smt_lib_fpa () -> + E.float Fp_value.Minus_zero e s + | NaN { e; s } when Options.get_smt_lib_fpa () -> + E.float Fp_value.NaN e s + | RoundingMode | T _ | Fp _ | Abs _ | Neg _ | Add _ | Sub _ | Mul _ + | Div _ | Fma _ | Sqrt _ | Rem _ | RoundToIntegral _ | Min _ | Max _ + | Leq _ | Lt _ | Geq _ | Gt _ | Eq _ | IsNormal _ | IsSubnormal _ + | IsZero _ | IsInfinite _ | IsNaN _ | IsNegative _ | IsPositive _ | Ieee_format_to_fp _ | To_fp _ | Of_real _ | Of_sbv _ | Of_ubv _ | To_ubv _ | To_sbv _ | To_real _ -> unsupported "Literal Floating-Point Arithmetic term %a" DE.Term.print term + | Plus_infinity _ | Minus_infinity _ | Plus_zero _ | Minus_zero _ + | NaN _ -> + unsupported + "Constant term %a (Enable the SMT-LIB FPA with `-enable-theory \ + smt.float` to be able to use float literals)" + DE.Term.print term end | _ -> unsupported "Constant term %a" DE.Term.print term end @@ -1159,22 +1206,107 @@ let rec mk_expr ?(loc = Loc.dummy) ?(name_base = "") ?(toplevel = false) (* Floating-point builtins *) | B.Float builtin, args -> ( match builtin, args with - | RoundNearestTiesToEven, _ -> mk_rounding NearestTiesToEven - | RoundNearestTiesToAway, _ -> mk_rounding NearestTiesToAway - | RoundTowardPositive, _ -> mk_rounding Up - | RoundTowardNegative, _ -> mk_rounding Down - | RoundTowardZero, _ -> mk_rounding ToZero - | Fp { e; s }, [sign_t; exp_t; sig_t] when Options.get_smt_lib_fpa () - -> - E.FP.fp (mk sign_t) (mk exp_t) (mk sig_t) e s - | Ieee_format_to_fp { e; s }, [bv_t] when Options.get_smt_lib_fpa () - -> - E.FP.ieee_format_to_fp (mk bv_t) e s + (* SMT-LIB FPA theory operations *) + | _ when Options.get_smt_lib_fpa () -> begin + match builtin, args with + | Fp { e = eb; s = sb }, [sign_t; exp_t; sig_t] -> + E.FP.fp (mk sign_t) (mk exp_t) (mk sig_t) eb sb + | Ieee_format_to_fp { e = eb; s = sb }, [bv_t] -> + E.FP.ieee_format_to_fp (mk bv_t) eb sb + (* arithmetic with rounding mode *) + | Add { e = eb; s = sb }, [mode; x; y] -> + E.FP.add ~eb ~sb ~mode:(mk mode) (mk x) (mk y) + | Sub { e = eb; s = sb }, [mode; x; y] -> + E.FP.sub ~eb ~sb ~mode:(mk mode) (mk x) (mk y) + | Mul { e = eb; s = sb }, [mode; x; y] -> + E.FP.mul ~eb ~sb ~mode:(mk mode) (mk x) (mk y) + | Div { e = eb; s = sb }, [mode; x; y] -> + E.FP.div ~eb ~sb ~mode:(mk mode) (mk x) (mk y) + | Fma { e = eb; s = sb }, [mode; x; y; z] -> + E.FP.fma ~eb ~sb ~mode:(mk mode) (mk x) (mk y) (mk z) + | Sqrt { e = eb; s = sb }, [mode; x] -> + E.FP.sqrt ~eb ~sb ~mode:(mk mode) (mk x) + | RoundToIntegral { e = eb; s = sb }, [mode; x] -> + E.FP.round_to_integral ~eb ~sb ~mode:(mk mode) (mk x) + | Of_real { e = eb; s = sb }, [mode; x] -> + E.FP.of_real ~eb ~sb ~mode:(mk mode) (mk x) + (* arithmetic without rounding mode *) + | Abs { e = eb; s = sb }, [x] -> E.FP.abs ~eb ~sb (mk x) + | Neg { e = eb; s = sb }, [x] -> E.FP.neg ~eb ~sb (mk x) + | Rem { e = _; s = _ }, [_x; _y] -> + (* TODO: rem is not currently in the axiomatization, its semantics + need to be either axiomatized or implemented in Alt-Ergo. It is + treated as an uninterpreted symbol in the meantime. *) + let ty = dty_to_ty term_ty in + let sy = Sy.name (get_basename tcst.path) in + E.mk_term sy (List.map mk args) ty + | Min { e = eb; s = sb }, [x; y] -> E.FP.min ~eb ~sb (mk x) (mk y) + | Max { e = eb; s = sb }, [x; y] -> E.FP.max ~eb ~sb (mk x) (mk y) + (* comparisons *) + | Leq { e = eb; s = sb }, [x; y] -> E.FP.le ~eb ~sb (mk x) (mk y) + | Lt { e = eb; s = sb }, [x; y] -> E.FP.lt ~eb ~sb (mk x) (mk y) + | Geq { e = eb; s = sb }, [x; y] -> E.FP.ge ~eb ~sb (mk x) (mk y) + | Gt { e = eb; s = sb }, [x; y] -> E.FP.gt ~eb ~sb (mk x) (mk y) + | Eq { e = eb; s = sb }, [x; y] -> E.FP.eq ~eb ~sb (mk x) (mk y) + (* predicates *) + | IsNormal { e = eb; s = sb }, [x] -> E.FP.is_normal ~eb ~sb (mk x) + | IsSubnormal { e = eb; s = sb }, [x] -> + E.FP.is_subnormal ~eb ~sb (mk x) + | IsZero { e = eb; s = sb }, [x] -> E.FP.is_zero ~eb ~sb (mk x) + | IsInfinite { e = eb; s = sb }, [x] -> + E.FP.is_infinite ~eb ~sb (mk x) + | IsNaN { e = eb; s = sb }, [x] -> E.FP.is_nan ~eb ~sb (mk x) + | IsNegative { e = eb; s = sb }, [x] -> + E.FP.is_negative ~eb ~sb (mk x) + | IsPositive { e = eb; s = sb }, [x] -> + E.FP.is_positive ~eb ~sb (mk x) + (* real conversion *) + | To_real { e = eb; s = sb }, [x] -> E.FP.to_real ~eb ~sb (mk x) + (* TODO: FP <-> FP and BV <-> FP conversion, treated as + uninterpreted in the meantime. *) + | ( ( To_fp { e1 = _; s1 = _; e2 = _; s2 = _ } + | Of_sbv { m = _; e = _; s = _ } + | Of_ubv { m = _; e = _; s = _ } + | To_ubv { m = _; e = _; s = _ } + | To_sbv { m = _; e = _; s = _ } ), + [_; _] ) -> + let ty = dty_to_ty term_ty in + let sy = Sy.name (get_basename tcst.path) in + E.mk_term sy (List.map mk args) ty + (* can't be applied *) + | (RoundingMode | T _ | Fp _), _ + | ( ( Plus_infinity _ | Minus_infinity _ | Plus_zero _ + | Minus_zero _ | NaN _ ), + _ ) + | RoundNearestTiesToEven, _ + | RoundNearestTiesToAway, _ + | RoundTowardPositive, _ + | RoundTowardNegative, _ + | RoundTowardZero, _ + (* wrong arity *) + | ( ( Ieee_format_to_fp _ | To_fp _ | Of_sbv _ | Of_ubv _ | To_ubv _ + | To_sbv _ | Add _ | Sub _ | Mul _ | Div _ | Fma _ | Sqrt _ + | RoundToIntegral _ | Of_real _ | Abs _ | Neg _ | Rem _ | Min _ + | Max _ | Leq _ | Lt _ | Geq _ | Gt _ | Eq _ | IsNormal _ + | IsSubnormal _ | IsZero _ | IsInfinite _ | IsNaN _ + | IsNegative _ | IsPositive _ | To_real _ ), + _ ) -> + invalid_app_term () + end + (* can't be applied *) | (RoundingMode | T _ | Fp _), _ | ( ( Plus_infinity _ | Minus_infinity _ | Plus_zero _ | Minus_zero _ | NaN _ ), - _ ) -> + _ ) + (* rounding modes are now matched as literals since we use the SMT-LIB + FP theory ones provided by dolmen *) + | RoundNearestTiesToEven, _ + | RoundNearestTiesToAway, _ + | RoundTowardPositive, _ + | RoundTowardNegative, _ + | RoundTowardZero, _ -> invalid_app_term () + (* not supported without [Options.get_smt_lib_fpa ()] *) | ( ( Abs _ | Neg _ | Add _ | Sub _ | Mul _ | Div _ | Fma _ | Sqrt _ | Rem _ | RoundToIntegral _ | Min _ | Max _ | Leq _ | Lt _ | Geq _ | Gt _ | Eq _ | IsNormal _ | IsSubnormal _ | IsZero _ diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 8cc6e020c8..1780156ecc 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -289,18 +289,30 @@ struct in P.add p (P.mult_const coef p3), ctx (*** : partial handling of some arith/FPA operators **) - | Sy.Op Float, [prec; exp; mode; x] -> + | Sy.Op Float, [prec; exp; mode; x] -> ( let prec = E.int_view prec and exp = E.int_view exp in - let mode = E.rounding_mode_view mode in - let aux_func e = - let res, _, _ = Fpa_rounding.float_of_rational prec exp mode e in - res - in - mk_partial_interpretation_1 aux_func coef p ty t x, ctx + match E.rounding_mode_view mode with + | Some mode -> + let aux_func e = + let res, _, _ = Fpa_rounding.float_of_rational prec exp mode e in + res + in + mk_partial_interpretation_1 aux_func coef p ty t x, ctx + | None -> + (* If the rounding mode is not a literal, treat it as an uninterpreted + function. If [Options.get_smt_lib_fpa ()], fpa_rel will update it + when the rounding mode is substituted with a literal. *) + P.add (P.create [coef, X.term_embed t] Q.zero ty) p, ctx) | Sy.Op Sy.Integer_round, [mode; x] -> - let aux_func = - Fpa_rounding.round_to_integer (E.rounding_mode_view mode) + let mode = + match E.rounding_mode_view mode with + | Some mode -> mode + | None -> + Fmt.failwith + "integer_round: The given term %a is not a constant rounding mode" + E.print mode in + let aux_func = Fpa_rounding.round_to_integer mode in mk_partial_interpretation_1 aux_func coef p ty t x, ctx | Sy.Op (Sy.Abs_int | Sy.Abs_real), [x] -> mk_partial_interpretation_1 Q.abs coef p ty t x, ctx diff --git a/src/lib/reasoners/fpa.ml b/src/lib/reasoners/fpa.ml new file mode 100644 index 0000000000..6b38c4b5a0 --- /dev/null +++ b/src/lib/reasoners/fpa.ml @@ -0,0 +1,151 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +module E = Expr +module Sy = Symbols + +type 'r abstract = + | Alien of 'r + | Literal of int * int * Fp_value.t + +module Shostak (X : sig + include Sig.X + + val extract : r -> r abstract option + + val embed : r abstract -> r +end) = +struct + type t = X.r abstract + + type r = X.r + + let name = "Fpa" + + let timer = Timers.M_Fpa + + (*BISECT-IGNORE-BEGIN*) + module Debug = struct + let solve r1 r2 = + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa" ~function_name:"solve" + "solve %a = %a" X.print r1 X.print r2 + + let unsolvable r1 r2 = + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa" ~function_name:"solve" + "%a <> %a: distinct literals, unsolvable" X.print r1 X.print r2 + end + (*BISECT-IGNORE-END*) + + let is_mine_symb = function + | Sy.Float _ -> Options.get_smt_lib_fpa () + | _ -> false + + let embed r = match X.extract r with Some v -> v | None -> Alien r + + let is_mine v = X.embed v + + let make t = + let { E.f; ty; _ } = E.term_view t in + match f, ty with + | Sy.Float fp_val, Ty.Tfloat (eb, sb) -> + is_mine (Literal (eb, sb, fp_val)), [] + | _ -> Util.internal_error "%a is not a floating-point literal" E.print t + + let type_info = function + | Alien r -> X.type_info r + | Literal (eb, sb, _) -> Ty.Tfloat (eb, sb) + + let equal s1 s2 = + match s1, s2 with + | Alien r1, Alien r2 -> X.equal r1 r2 + | Literal (eb1, sb1, v1), Literal (eb2, sb2, v2) -> + eb1 = eb2 && sb1 = sb2 && Fp_value.equal v1 v2 + | _ -> false + + let hash = function + | Alien r -> X.hash r + | Literal (eb, sb, v) -> Hashtbl.hash (eb, sb) + (17 * Hashtbl.hash v) + + let compare s1 s2 = + match embed s1, embed s2 with + | Alien r1, Alien r2 -> X.str_cmp r1 r2 + | Alien _, _ -> 1 + | _, Alien _ -> -1 + | Literal (eb1, sb1, v1), Literal (eb2, sb2, v2) -> + let c = Int.compare eb1 eb2 in + if c <> 0 + then c + else + let c = Int.compare sb1 sb2 in + if c <> 0 then c else Fp_value.compare v1 v2 + + let print ppf = function + | Alien r -> X.print ppf r + | Literal (eb, sb, v) -> Fp_value.pp_smtlib eb sb ppf v + + let leaves = function Alien r -> X.leaves r | Literal _ -> [] + + let is_constant = function Alien r -> X.is_constant r | Literal _ -> true + + let subst p v t = + match t with + | Literal _ -> is_mine t + | Alien r -> if X.equal p r then v else X.subst p v r + + let fully_interpreted = function + | Sy.Float _ -> Options.get_smt_lib_fpa () + | _ -> false + + let abstract_selectors t acc = + match t with Literal _ -> is_mine t, acc | Alien _ -> assert false + + let color _ = assert false + + let term_extract r = + match embed r with + | Literal (eb, sb, fp_val) -> Some (E.float fp_val eb sb), false + | Alien _ -> None, false + + let solve r1 r2 pb = + Debug.solve r1 r2; + match embed r1, embed r2 with + | Literal (_, _, l1), Literal (_, _, l2) -> + if Fp_value.equal l1 l2 + then pb + else ( + Debug.unsolvable r1 r2; + raise Util.Unsolvable) + | Alien _, Alien _ -> + Sig. + { pb with + sbt = (if X.str_cmp r1 r2 > 0 then r1, r2 else r2, r1) :: pb.sbt + } + | Alien _, Literal _ -> Sig.{ pb with sbt = (r1, r2) :: pb.sbt } + | Literal _, Alien _ -> Sig.{ pb with sbt = (r2, r1) :: pb.sbt } + + let assign_value _ _ _ = None + + let to_model_term r = + match embed r with + | Literal (eb, sb, fp_val) -> Some (E.float fp_val eb sb) + | Alien _ -> None +end diff --git a/src/lib/reasoners/fpa.mli b/src/lib/reasoners/fpa.mli new file mode 100644 index 0000000000..f35d9b9667 --- /dev/null +++ b/src/lib/reasoners/fpa.mli @@ -0,0 +1,29 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +type 'r abstract = + | Alien of 'r + | Literal of int * int * Fp_value.t + +module Shostak (X : sig + include Sig.X + + val extract : r -> r abstract option + + val embed : r abstract -> r +end) : Sig.SHOSTAK with type r = X.r and type t = X.r abstract diff --git a/src/lib/reasoners/fpa_rel.ml b/src/lib/reasoners/fpa_rel.ml new file mode 100644 index 0000000000..7d12a29c7c --- /dev/null +++ b/src/lib/reasoners/fpa_rel.ml @@ -0,0 +1,663 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +module X = Shostak.Combine +module E = Expr +module Sy = Symbols +module Ex = Explanation +module Q = Numbers.Q +module Z = Numbers.Z +module MX = Shostak.MXH +module SX = Shostak.SXH +module Names = E.FP.Names + +let src = Logs.Src.create ~doc:"Fpa_rel" __MODULE__ + +module Log = (val Logs.src_log src : Logs.LOG) + +let timer = Timers.M_Fpa + +module IntPairSet = Set.Make (struct + type t = int * int + + let compare (a1, b1) (a2, b2) = + let c = Int.compare a1 a2 in + if c <> 0 then c else Int.compare b1 b2 +end) + +(* Literals needed by the FPA theory axioms generated by why3 *) +type precision_literals = + { max_int_z : Z.t; + pow2sb : Z.t; + half_pow2sb : Z.t; + abs_err_rne_denom : Z.t; + abs_err_denom : Z.t + } + +let is_fpa_ty = function Ty.Tfloat _ -> true | _ -> false + +module Domain = struct + (* Status of a predicate for a given FP value *) + type status = + | Unknown + | True of Ex.t + | False of Ex.t + + exception Inconsistent of Ex.t + + (* Domain representing the status of each predicate for a given FP value *) + type t = + { is_nan : status; + is_zero : status; + is_infinite : status; + is_positive : status; + is_negative : status + } + + let unknown = + { is_nan = Unknown; + is_zero = Unknown; + is_infinite = Unknown; + is_positive = Unknown; + is_negative = Unknown + } + + let pp_status ppf = function + | Unknown -> Fmt.pf ppf "?" + | True _ -> Fmt.pf ppf "T" + | False _ -> Fmt.pf ppf "F" + + let pp ppf d = + Fmt.pf ppf "{nan=%a zero=%a inf=%a pos=%a neg=%a}" pp_status d.is_nan + pp_status d.is_zero pp_status d.is_infinite pp_status d.is_positive + pp_status d.is_negative + + let status_equal ts1 ts2 = + match ts1, ts2 with + | Unknown, Unknown | True _, True _ | False _, False _ -> true + | _ -> false + + let equal d1 d2 = + status_equal d1.is_nan d2.is_nan + && status_equal d1.is_zero d2.is_zero + && status_equal d1.is_infinite d2.is_infinite + && status_equal d1.is_positive d2.is_positive + && status_equal d1.is_negative d2.is_negative + + let merge_status st1 st2 = + match st1, st2 with + | Unknown, st | st, Unknown -> st + | True ex1, True ex2 -> True (Ex.union ex1 ex2) + | False ex1, False ex2 -> False (Ex.union ex1 ex2) + | True ex1, False ex2 | False ex2, True ex1 -> + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa_rel" ~function_name:"merge_status" + "conflict: %a and %a" pp_status (True ex1) pp_status (False ex2); + raise (Inconsistent (Ex.union ex1 ex2)) + + type pred = + | Nan + | Zero + | Infinite + | Positive + | Negative + + let pp_pred ppf = function + | Nan -> Fmt.string ppf "nan" + | Zero -> Fmt.string ppf "zero" + | Infinite -> Fmt.string ppf "infinite" + | Positive -> Fmt.string ppf "positive" + | Negative -> Fmt.string ppf "negative" + + let get_pred_status p d = + match p with + | Nan -> d.is_nan + | Zero -> d.is_zero + | Infinite -> d.is_infinite + | Positive -> d.is_positive + | Negative -> d.is_negative + + let upd_pred_status p st d = + let st = merge_status (get_pred_status p d) st in + match p with + | Nan -> { d with is_nan = st } + | Zero -> { d with is_zero = st } + | Infinite -> { d with is_infinite = st } + | Positive -> { d with is_positive = st } + | Negative -> { d with is_negative = st } + + (* When [p] is true, the predicates in [exclusive_of p] must be false. *) + let exclusive_of = function + | Nan -> [Zero; Infinite; Positive; Negative] + | Zero -> [Nan; Infinite] + | Infinite -> [Nan; Zero] + | Positive -> [Nan; Negative] + | Negative -> [Nan; Positive] + + let pred_of_name name = + if String.equal name Names.is_nan + then Some Nan + else if String.equal name Names.is_zero + then Some Zero + else if String.equal name Names.is_infinite + then Some Infinite + else if String.equal name Names.is_positive + then Some Positive + else if String.equal name Names.is_negative + then Some Negative + else None + + let rec apply p ~ex ~is_true d = + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa_rel" ~function_name:"apply" + "apply %a = %b to %a" pp_pred p is_true pp d; + let st = if is_true then True ex else False ex in + let d = upd_pred_status p st d in + let d = + (* if [p] became true, then the predicates in [exclusive_of p] are must be + false *) + match st with + | True _ -> + (* Because `ex` is the same as the `ex_st` in [True ex_st] *) + let neg_st = False ex in + List.fold_left + (fun d p -> upd_pred_status p neg_st d) + d (exclusive_of p) + | False _ -> d + | Unknown -> assert false + in + match d.is_nan, d.is_positive, d.is_negative with + | Unknown, False ex_p, False ex_n -> + (* not positive & not negative -> NaN *) + apply Nan ~ex:(Ex.union ex_p ex_n) ~is_true:true d + | False ex_nan, Unknown, False ex_n -> + (* not NaN & not negative -> positive *) + apply Positive ~ex:(Ex.union ex_nan ex_n) ~is_true:true d + | False ex_nan, False ex_p, Unknown -> + (* not NaN & not positive -> negative *) + apply Negative ~ex:(Ex.union ex_nan ex_p) ~is_true:true d + | _ -> d + + let merge ~ex d1 d2 = + let apply_if_known p st d = + match st with + | Unknown -> d + | True ex2 -> apply p ~ex:(Ex.union ex ex2) ~is_true:true d + | False ex2 -> apply p ~ex:(Ex.union ex ex2) ~is_true:false d + in + apply_if_known Nan d2.is_nan d1 + |> apply_if_known Zero d2.is_zero + |> apply_if_known Infinite d2.is_infinite + |> apply_if_known Positive d2.is_positive + |> apply_if_known Negative d2.is_negative + + let set_pred p is_neg ex d = apply p ~ex ~is_true:(not is_neg) d + + (* Deduce literal FP value equality from predicates *) + let deduce_fpval_eq d = + match d.is_nan with + | True ex -> Some (Fp_value.NaN, ex) + | _ -> ( + match d.is_zero, d.is_infinite, d.is_positive, d.is_negative with + | True ex_z, _, True ex_p, _ -> + (* is_zero & is_positive -> = plus_zero *) + Some (Fp_value.Plus_zero, Ex.union ex_z ex_p) + | True ex_z, _, _, True ex_n -> + (* is_zero & is_negative -> = minus_zero *) + Some (Fp_value.Minus_zero, Ex.union ex_z ex_n) + | _, True ex_inf, True ex_p, _ -> + (* is_infinite & is_positive -> = plus_infinity *) + Some (Fp_value.Plus_infinity, Ex.union ex_inf ex_p) + | _, True ex_inf, _, True ex_n -> + (* is_infinite & is_negative -> = minus_infinity *) + Some (Fp_value.Minus_infinity, Ex.union ex_inf ex_n) + | _ -> None) +end + +module Domains = struct + type t = + { domains : Domain.t MX.t; + changed : SX.t + } + + type _ Uf.id += Id : t Uf.id + + exception Inconsistent = Domain.Inconsistent + + let empty = { domains = MX.empty; changed = SX.empty } + + let filter_ty = is_fpa_ty + + let pp ppf t = + Fmt.( + iter_bindings ~sep:semi MX.iter + (box @@ pair ~sep:(any " ->@ ") X.print Domain.pp) + |> braces) + ppf t.domains + + let get r t = + match MX.find_opt r t.domains with Some d -> d | None -> Domain.unknown + + let add_changed r d nd t = + if Domain.equal d nd + then t + else ( + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa_rel" ~function_name:"add_changed" + "domain of %a: %a -> %a" X.print r Domain.pp d Domain.pp nd; + { domains = MX.add r nd t.domains; changed = SX.add r t.changed }) + + let new_pred r pred is_neg ex t = + let d = get r t in + let nd = Domain.set_pred pred is_neg ex d in + add_changed r d nd t + + let init r t = + if MX.mem r t.domains then t else { t with changed = SX.add r t.changed } + + let subst ~ex r nr t = + match MX.find_opt r t.domains with + | None -> + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa_rel" ~function_name:"subst" + "%a (no domain) -> %a" X.print r X.print nr; + t + | Some d -> + let nd = get nr t in + let mergedd = Domain.merge ~ex d nd in + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa_rel" ~function_name:"subst" + "%a -> %a: %a merged with %a = %a" X.print r X.print nr Domain.pp d + Domain.pp nd Domain.pp mergedd; + let t = + { domains = MX.remove r t.domains; changed = SX.remove r t.changed } + in + add_changed nr nd mergedd t + + let flush_changed_domains f acc t = + let acc = SX.fold (fun r acc -> f acc r (get r t)) t.changed acc in + acc, { t with changed = SX.empty } +end + +module AEFloat_arg_watch = struct + type args = + { eb : int; + sb : int; + mode : X.r; + ex : Ex.t + } + + type t = + { apps : args E.Map.t; + (* ae.float application -> its (eb, sb, mode) arguments *) + watched_args : E.Set.t MX.t; + (* mode value -> ae.float applications that use it as an argument *) + ready : (int * int * E.t * Ex.t) E.Map.t + (* Mapping of ae.float applications to their literal (eb, sb, mode) + arguments that are now known *) + } + + type _ Uf.id += Id : t Uf.id + + exception Inconsistent of Ex.t + + let empty = + { apps = E.Map.empty; watched_args = MX.empty; ready = E.Map.empty } + + let pp ppf t = + Fmt.pf ppf "{float_watch: %d pending, %d ready}" (E.Map.cardinal t.apps) + (E.Map.cardinal t.ready) + + let filter_ty _ = true + + let init _ t = t + + let add_by_arg r term watched_args = + let s = + match MX.find_opt r watched_args with Some s -> s | None -> E.Set.empty + in + MX.add r (E.Set.add term s) watched_args + + let int_lit_view r = E.int_view (Option.get (X.to_model_term r)) + + let mode_lit_view r = Option.get (X.to_model_term r) + + (* [ready_value] is only called when [mode] is known to be a literal. *) + let ready_value eb sb mode ex = eb, sb, mode_lit_view mode, ex + + let register term r_eb r_sb r_mode ~ex t = + if E.Map.mem term t.apps || E.Map.mem term t.ready + then t + else + let eb = int_lit_view r_eb in + let sb = int_lit_view r_sb in + if X.is_constant r_mode + then + { t with ready = E.Map.add term (ready_value eb sb r_mode ex) t.ready } + else + { t with + apps = E.Map.add term { eb; sb; mode = r_mode; ex } t.apps; + watched_args = add_by_arg r_mode term t.watched_args + } + + let subst ~ex rr nrr t = + match MX.find_opt rr t.watched_args with + | None -> t + | Some terms -> + let t = { t with watched_args = MX.remove rr t.watched_args } in + let nrr_lit = X.is_constant nrr in + E.Set.fold + (fun term t -> + match E.Map.find_opt term t.apps with + | None -> t + | Some { eb; sb; mode; ex = ex0 } -> + assert (X.equal mode rr); + let ex = Ex.union ex0 ex in + if nrr_lit + then + { apps = E.Map.remove term t.apps; + watched_args = t.watched_args; + ready = E.Map.add term (ready_value eb sb nrr ex) t.ready + } + else + { t with + apps = E.Map.add term { eb; sb; mode = nrr; ex } t.apps; + watched_args = add_by_arg nrr term t.watched_args + }) + terms t + + let flush_ready t = E.Map.bindings t.ready, { t with ready = E.Map.empty } +end + +type t = + { pending_types : IntPairSet.t; + pending_literals : (E.t * E.t) list; + literals_cache : (int * int, precision_literals) Hashtbl.t; + new_terms : E.Set.t + } + +let empty uf = + ( { pending_types = IntPairSet.empty; + pending_literals = []; + literals_cache = Hashtbl.create 16; + new_terms = E.Set.empty + }, + Uf.domains uf + |> Uf.GlobalDomains.add (module Domains) Domains.empty + |> Uf.GlobalDomains.add (module AEFloat_arg_watch) AEFloat_arg_watch.empty ) + +let pow2 n = Z.shift_left Z.one n + +let mk_eq_fact ?(ex = Ex.empty) lhs rhs = + Literal.LTerm (E.mk_eq ~iff:false lhs rhs), ex, Th_util.Other + +let int_literal_fact eb_t sb_t name literal (terms, facts) = + let lhs = E.mk_term (Sy.name name) [eb_t; sb_t] Ty.Tint in + E.Set.add lhs terms, mk_eq_fact lhs (E.Ints.of_Z literal) :: facts + +let real_literal_fact eb_t sb_t name literal (terms, facts) = + let lhs = E.mk_term (Sy.name name) [eb_t; sb_t] Ty.Treal in + E.Set.add lhs terms, mk_eq_fact lhs (E.Reals.of_Z literal) :: facts + +let get_literals env eb sb = + match Hashtbl.find_opt env.literals_cache (eb, sb) with + | Some c -> c + | None -> + let bias = (1 lsl (eb - 1)) - 1 in + let emax = bias + 1 in + let min_exp = emax + sb - 3 in + let c = + { pow2sb = pow2 sb; + max_int_z = Z.sub (pow2 emax) (pow2 (emax - sb)); + half_pow2sb = pow2 (sb - 1); + abs_err_rne_denom = pow2 (min_exp + 1); + abs_err_denom = pow2 min_exp + } + in + Hashtbl.add env.literals_cache (eb, sb) c; + c + +let type_literal_facts env eb sb = + let c = get_literals env eb sb in + let eb_t = E.Ints.of_int eb in + let sb_t = E.Ints.of_int sb in + (E.Set.empty, []) + |> int_literal_fact eb_t sb_t E.FP.Names.pow2sb c.pow2sb + |> int_literal_fact eb_t sb_t E.FP.Names.max_int c.max_int_z + |> real_literal_fact eb_t sb_t E.FP.Names.max_real c.max_int_z + |> real_literal_fact eb_t sb_t E.FP.Names.pow2sb_real c.pow2sb + |> real_literal_fact eb_t sb_t E.FP.Names.half_pow2sb_real c.half_pow2sb + |> real_literal_fact eb_t sb_t E.FP.Names.abs_err_rne_denom + c.abs_err_rne_denom + |> real_literal_fact eb_t sb_t E.FP.Names.abs_err_denom c.abs_err_denom + +let mk_fp_literal_facts eb_t sb_t term ~is_nan ~is_zero ~is_infinite + ~is_positive ~is_negative = + let mk_fact name b = + ( E.mk_term (Sy.name name) [eb_t; sb_t; term] Ty.Tbool, + if b then E.vrai else E.faux ) + in + [ mk_fact Names.is_nan is_nan; + mk_fact Names.is_zero is_zero; + mk_fact Names.is_infinite is_infinite; + mk_fact Names.is_positive is_positive; + mk_fact Names.is_negative is_negative ] + +let fp_literal_facts eb sb term v = + let eb_t = E.Ints.of_int eb in + let sb_t = E.Ints.of_int sb in + match v with + | Fp_value.NaN -> + mk_fp_literal_facts eb_t sb_t term ~is_nan:true ~is_zero:false + ~is_infinite:false ~is_positive:false ~is_negative:false + | Plus_infinity -> + mk_fp_literal_facts eb_t sb_t term ~is_nan:false ~is_zero:false + ~is_infinite:true ~is_positive:true ~is_negative:false + | Minus_infinity -> + mk_fp_literal_facts eb_t sb_t term ~is_nan:false ~is_zero:false + ~is_infinite:true ~is_positive:false ~is_negative:true + | Plus_zero -> + mk_fp_literal_facts eb_t sb_t term ~is_nan:false ~is_zero:true + ~is_infinite:false ~is_positive:true ~is_negative:false + | Minus_zero -> + mk_fp_literal_facts eb_t sb_t term ~is_nan:false ~is_zero:true + ~is_infinite:false ~is_positive:false ~is_negative:true + | Finite q -> + let to_real_term = + E.mk_term (Sy.name Names.to_real) [eb_t; sb_t; term] Ty.Treal + in + (to_real_term, E.Reals.of_Q q) + :: mk_fp_literal_facts eb_t sb_t term ~is_nan:false ~is_zero:false + ~is_infinite:false + ~is_positive:(Q.sign q > 0) + ~is_negative:(Q.sign q < 0) + +let process_pred uf ex a domains = + match E.lit_view a with + | E.Pred (t, is_neg) -> ( + let { E.f; xs; _ } = E.term_view t in + match xs with + | [_; _; x] when is_fpa_ty (E.type_info x) -> ( + match f with + | Sy.Name { hs; _ } -> ( + let name = Hstring.view hs in + match Domain.pred_of_name name with + | Some pred -> + let r, ex_r = Uf.find uf x in + let ex = Ex.union ex ex_r in + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa_rel" + ~function_name:"process_pred" "%s(%a) = %b (repr %a)" name E.print + x (not is_neg) X.print r; + Domains.new_pred r pred is_neg ex domains + | None -> domains) + | _ -> domains) + | _ -> domains) + | _ -> domains + +let mk_eq_fpval_fact rr fp_val ex = + let eb, sb = + match X.type_info rr with Ty.Tfloat (eb, sb) -> eb, sb | _ -> assert false + in + let fp_r, _ = X.make (E.float fp_val eb sb) in + let eq = Shostak.L.(view @@ mk_eq rr fp_r) in + Literal.LSem eq, ex, Th_util.Other + +let flush_domain_facts domains = + Domains.flush_changed_domains + (fun acc rr d -> + match Domain.deduce_fpval_eq d with + | None -> acc + | Some (fp_val, ex) -> + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa_rel" + ~function_name:"flush_domain_facts" "deduced: %a = %a" X.print rr + Fp_value.pp fp_val; + mk_eq_fpval_fact rr fp_val ex :: acc) + [] domains + +let register_aefloat_arg_watch uf term ds = + match E.term_view term with + | { E.f = Sy.Op Float; xs = [eb; sb; mode; _x]; _ } -> + let eb, _ = Uf.find uf eb in + let sb, _ = Uf.find uf sb in + let mode, ex = Uf.find uf mode in + let fw = Uf.GlobalDomains.find (module AEFloat_arg_watch) ds in + let fw = AEFloat_arg_watch.register term eb sb mode ~ex fw in + Uf.GlobalDomains.add (module AEFloat_arg_watch) fw ds + | _ -> ds + +let add env uf _r term = + if not (Options.get_smt_lib_fpa ()) + then env, Uf.domains uf, [] + else + let { E.f; ty; _ } = E.term_view term in + match ty with + | Ty.Tfloat (eb, sb) -> + let env = + if + not + (IntPairSet.mem (eb, sb) env.pending_types + || Hashtbl.mem env.literals_cache (eb, sb)) + then + { env with pending_types = IntPairSet.add (eb, sb) env.pending_types } + else env + in + let env = + match f with + | Sy.Float v -> + if Options.get_debug_fpa () > 0 + then + Printer.print_dbg ~module_name:"Fpa_rel" ~function_name:"add" + "queueing literal facts for %a" E.print term; + { env with + pending_literals = + fp_literal_facts eb sb term v @ env.pending_literals + } + | _ -> env + in + env, Uf.domains uf, [] + | Ty.Treal -> + (* ae.float applies ae.round on reals *) + let ds = register_aefloat_arg_watch uf term (Uf.domains uf) in + env, ds, [] + | _ -> env, Uf.domains uf, [] + +let mk_aefloat_eq_fact term (eb, sb, mode, ex) = + match E.term_view term with + | { E.xs = [_; _; _; x]; _ } -> + let repl = + E.mk_term (Sy.Op Float) + [E.Ints.of_int eb; E.Ints.of_int sb; mode; x] + Ty.Treal + in + mk_eq_fact ~ex term repl + | _ -> assert false + +let assume env uf la = + if not (Options.get_smt_lib_fpa ()) + then env, Uf.domains uf, { Sig_rel.assume = []; remove = [] } + else + let ds = Uf.domains uf in + let new_terms, prec_facts = + IntPairSet.fold + (fun (eb, sb) (terms_acc, facts_acc) -> + let terms, facts = type_literal_facts env eb sb in + E.Set.union terms terms_acc, facts @ facts_acc) + env.pending_types (E.Set.empty, []) + in + let eval_facts = + List.map (fun (lhs, rhs) -> mk_eq_fact lhs rhs) env.pending_literals + in + let env = + { env with + pending_types = IntPairSet.empty; + pending_literals = []; + new_terms = E.Set.union new_terms env.new_terms + } + in + let domains = Uf.GlobalDomains.find (module Domains) ds in + let domains = + try + List.fold_left + (fun domains (_, root, ex, _) -> + match root with + | None -> domains + | Some a -> process_pred uf ex a domains) + domains la + with Domain.Inconsistent ex -> + raise_notrace (Ex.Inconsistent (ex, Uf.cl_extract uf)) + in + let pred_facts, domains = flush_domain_facts domains in + let ds = Uf.GlobalDomains.add (module Domains) domains ds in + let aefloat_arg_watch = + Uf.GlobalDomains.find (module AEFloat_arg_watch) ds + in + let ready, aefloat_arg_watch = + AEFloat_arg_watch.flush_ready aefloat_arg_watch + in + let aefloat_facts = + List.map (fun (term, p) -> mk_aefloat_eq_fact term p) ready + in + let ds = + Uf.GlobalDomains.add (module AEFloat_arg_watch) aefloat_arg_watch ds + in + ( env, + ds, + { Sig_rel.assume = prec_facts @ eval_facts @ pred_facts @ aefloat_facts; + remove = [] + } ) + +let query _ _ _ = Th_util.Unknown + +let case_split _env _uf ~for_model:_ = [] + +let optimizing_objective _env _uf _o = None + +let new_terms env = env.new_terms + +let instantiate ~do_syntactic_matching:_ _ env _ _ = env, [] + +let assume_th_elt t _ _ = t diff --git a/src/lib/reasoners/fpa_rel.mli b/src/lib/reasoners/fpa_rel.mli new file mode 100644 index 0000000000..003a4a09e8 --- /dev/null +++ b/src/lib/reasoners/fpa_rel.mli @@ -0,0 +1,21 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +include Sig_rel.RELATION + +val src : Logs.src diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml index fcad0a5fa2..fe6d75945d 100644 --- a/src/lib/reasoners/relation.ml +++ b/src/lib/reasoners/relation.ml @@ -39,6 +39,8 @@ module Rel4 : Sig_rel.RELATION = Adt_rel module Rel5 : Sig_rel.RELATION = Ite_rel +module Rel6 : Sig_rel.RELATION = Fpa_rel + (* This value is unused. *) let timer = Timers.M_None @@ -47,7 +49,8 @@ type t = r2 : Rel2.t; r3 : Rel3.t; r4 : Rel4.t; - r5 : Rel5.t + r5 : Rel5.t; + r6 : Rel6.t } let empty uf = @@ -56,7 +59,8 @@ let empty uf = let r3, doms3 = Rel3.empty (Uf.set_domains uf doms2) in let r4, doms4 = Rel4.empty (Uf.set_domains uf doms3) in let r5, doms5 = Rel5.empty (Uf.set_domains uf doms4) in - { r1; r2; r3; r4; r5 }, doms5 + let r6, doms6 = Rel6.empty (Uf.set_domains uf doms5) in + { r1; r2; r3; r4; r5; r6 }, doms6 let ( |@| ) l1 l2 = if l1 == [] then l2 else if l2 == [] then l1 else List.rev_append l1 l2 @@ -83,10 +87,14 @@ let assume env uf sa = Timers.with_timer Rel5.timer Timers.F_assume @@ fun () -> Rel5.assume env.r5 (Uf.set_domains uf doms4) sa in - ( { r1 = env1; r2 = env2; r3 = env3; r4 = env4; r5 = env5 }, - doms5, - ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5; - remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 + let env6, doms6, ({ assume = a6; remove = rm6 } : _ Sig_rel.result) = + Timers.with_timer Rel6.timer Timers.F_assume @@ fun () -> + Rel6.assume env.r6 (Uf.set_domains uf doms5) sa + in + ( { r1 = env1; r2 = env2; r3 = env3; r4 = env4; r5 = env5; r6 = env6 }, + doms6, + ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6; + remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 } : _ Sig_rel.result) ) @@ -97,7 +105,8 @@ let assume_th_elt env th_elt dep = let env3 = Rel3.assume_th_elt env.r3 th_elt dep in let env4 = Rel4.assume_th_elt env.r4 th_elt dep in let env5 = Rel5.assume_th_elt env.r5 th_elt dep in - { r1 = env1; r2 = env2; r3 = env3; r4 = env4; r5 = env5 } + let env6 = Rel6.assume_th_elt env.r6 th_elt dep in + { r1 = env1; r2 = env2; r3 = env3; r4 = env4; r5 = env5; r6 = env6 } let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a k = @@ -113,7 +122,8 @@ let query env uf a = try_query (module Rel2) env.r2 uf a @@ fun () -> try_query (module Rel3) env.r3 uf a @@ fun () -> try_query (module Rel4) env.r4 uf a @@ fun () -> - try_query (module Rel5) env.r5 uf a @@ fun () -> Th_util.Unknown + try_query (module Rel5) env.r5 uf a @@ fun () -> + try_query (module Rel6) env.r6 uf a @@ fun () -> Th_util.Unknown let case_split env uf ~for_model = Options.exec_thread_yield (); @@ -122,7 +132,8 @@ let case_split env uf ~for_model = let seq3 = Rel3.case_split env.r3 uf ~for_model in let seq4 = Rel4.case_split env.r4 uf ~for_model in let seq5 = Rel5.case_split env.r5 uf ~for_model in - let splits = [seq1; seq2; seq3; seq4; seq5] in + let seq6 = Rel6.case_split env.r6 uf ~for_model in + let splits = [seq1; seq2; seq3; seq4; seq5; seq6] in let splits = List.fold_left ( |@| ) [] splits in List.fast_sort (fun (_, _, sz1) (_, _, sz2) -> @@ -144,7 +155,8 @@ let optimizing_objective env uf o = [ Rel1.optimizing_objective env.r1 uf; Rel2.optimizing_objective env.r2 uf; Rel3.optimizing_objective env.r3 uf; - Rel4.optimizing_objective env.r4 uf ] + Rel4.optimizing_objective env.r4 uf; + Rel6.optimizing_objective env.r6 uf ] let add env uf r t = Options.exec_thread_yield (); @@ -153,7 +165,10 @@ let add env uf r t = let r3, doms3, eqs3 = Rel3.add env.r3 (Uf.set_domains uf doms2) r t in let r4, doms4, eqs4 = Rel4.add env.r4 (Uf.set_domains uf doms3) r t in let r5, doms5, eqs5 = Rel5.add env.r5 (Uf.set_domains uf doms4) r t in - { r1; r2; r3; r4; r5 }, doms5, eqs1 |@| eqs2 |@| eqs3 |@| eqs4 |@| eqs5 + let r6, doms6, eqs6 = Rel6.add env.r6 (Uf.set_domains uf doms5) r t in + ( { r1; r2; r3; r4; r5; r6 }, + doms6, + eqs1 |@| eqs2 |@| eqs3 |@| eqs4 |@| eqs5 |@| eqs6 ) let instantiate ~do_syntactic_matching t_match env uf selector = Options.exec_thread_yield (); @@ -172,7 +187,10 @@ let instantiate ~do_syntactic_matching t_match env uf selector = let r5, l5 = Rel5.instantiate ~do_syntactic_matching t_match env.r5 uf selector in - { r1; r2; r3; r4; r5 }, l5 |@| l4 |@| l3 |@| l2 |@| l1 + let r6, l6 = + Rel6.instantiate ~do_syntactic_matching t_match env.r6 uf selector + in + { r1; r2; r3; r4; r5; r6 }, l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1 let new_terms env = Rel1.new_terms env.r1 @@ -180,3 +198,4 @@ let new_terms env = |> Expr.Set.union @@ Rel3.new_terms env.r3 |> Expr.Set.union @@ Rel4.new_terms env.r4 |> Expr.Set.union @@ Rel5.new_terms env.r5 + |> Expr.Set.union @@ Rel6.new_terms env.r6 diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 31f2600c46..4ebc426e63 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -50,6 +50,10 @@ module rec CX : sig val extract3 : r -> ADT.t option val embed3 : ADT.t -> r + + val extract4 : r -> FPA.t option + + val embed4 : FPA.t -> r end = struct type rview = | Term of Expr.t @@ -57,6 +61,7 @@ end = struct | Arith of ARITH.t | Bitv of BITV.t | Adt of ADT.t + | Fpa of FPA.t type r = { v : rview; @@ -75,6 +80,7 @@ end = struct | Arith t -> fprintf fmt "%a" ARITH.print t | Bitv t -> fprintf fmt "%a" BITV.print t | Adt t -> fprintf fmt "%a" ADT.print t + | Fpa t -> fprintf fmt "%a" FPA.print t | Term t -> fprintf fmt "%a" Expr.print t | Ac t -> fprintf fmt "%a" AC.print t end @@ -83,6 +89,7 @@ end = struct | Arith t -> fprintf fmt "Arith(%s):[%a]" ARITH.name ARITH.print t | Bitv t -> fprintf fmt "Bitv(%s):[%a]" BITV.name BITV.print t | Adt t -> fprintf fmt "Adt(%s):[%a]" ADT.name ADT.print t + | Fpa t -> fprintf fmt "Fpa(%s):[%a]" FPA.name FPA.print t | Term t -> fprintf fmt "FT:[%a]" Expr.print t | Ac t -> fprintf fmt "Ac:[%a]" AC.print t end @@ -152,6 +159,7 @@ end = struct | Arith x -> 1 + (10 * ARITH.hash x) | Bitv x -> 3 + (10 * BITV.hash x) | Adt x -> 6 + (10 * ADT.hash x) + | Fpa x -> 7 + (10 * FPA.hash x) | Ac ac -> 9 + (10 * AC.hash ac) | Term t -> 8 + (10 * Expr.hash t) in @@ -162,6 +170,7 @@ end = struct | Arith x, Arith y -> ARITH.equal x y | Bitv x, Bitv y -> BITV.equal x y | Adt x, Adt y -> ADT.equal x y + | Fpa x, Fpa y -> FPA.equal x y | Term x, Term y -> Expr.equal x y | Ac x, Ac y -> AC.equal x y | _ -> false @@ -187,6 +196,8 @@ end = struct let embed3 x = hcons { v = Adt x; id = -1000 (* dummy *) } + let embed4 x = hcons { v = Fpa x; id = -1000 (* dummy *) } + let ac_embed ({ Sig.l; _ } as t) = match l with | [] -> assert false @@ -204,6 +215,8 @@ end = struct let extract3 = function { v = Adt r; _ } -> Some r | _ -> None + let extract4 = function { v = Fpa r; _ } -> Some r | _ -> None + let ac_extract = function { v = Ac t; _ } -> Some t | _ -> None let term_extract r = @@ -211,6 +224,7 @@ end = struct | Arith _ -> ARITH.term_extract r | Bitv _ -> BITV.term_extract r | Adt _ -> ADT.term_extract r + | Fpa _ -> FPA.term_extract r | Ac _ -> None, false (* SYLVAIN : TODO *) | Term t -> Some t, true @@ -220,6 +234,7 @@ end = struct | Arith _ -> ARITH.to_model_term r | Bitv _ -> BITV.to_model_term r | Adt _ -> ADT.to_model_term r + | Fpa _ -> FPA.to_model_term r | Term t when Expr.is_model_term t -> Some t | Ac _ | Term _ -> None in @@ -235,6 +250,7 @@ end = struct | { v = Arith t; _ } -> ARITH.type_info t | { v = Bitv t; _ } -> BITV.type_info t | { v = Adt t; _ } -> ADT.type_info t + | { v = Fpa t; _ } -> FPA.type_info t | { v = Ac x; _ } -> AC.type_info x | { v = Term t; _ } -> Expr.type_info t @@ -247,6 +263,7 @@ end = struct | Arith _ -> -3 | Bitv _ -> -4 | Adt _ -> -5 + | Fpa _ -> -6 let compare_tag a b = theory_num a - theory_num b @@ -258,6 +275,7 @@ end = struct | Arith _, Arith _ -> ARITH.compare a b | Bitv _, Bitv _ -> BITV.compare a b | Adt _, Adt _ -> ADT.compare a b + | Fpa _, Fpa _ -> FPA.compare a b | Term x, Term y -> Expr.compare x y | Ac x, Ac y -> AC.compare x y | va, vb -> compare_tag va vb @@ -294,6 +312,7 @@ end = struct | Arith t -> ARITH.leaves t | Bitv t -> BITV.leaves t | Adt t -> ADT.leaves t + | Fpa t -> FPA.leaves t | Ac t -> r :: AC.leaves t | Term _ -> [r] @@ -302,6 +321,7 @@ end = struct | Arith t -> ARITH.is_constant t | Bitv t -> BITV.is_constant t | Adt t -> ADT.is_constant t + | Fpa t -> FPA.is_constant t | Term t -> begin let Expr.{ f; xs; _ } = Expr.term_view t in (* Constant terms that have no theories. *) @@ -319,6 +339,7 @@ end = struct | Arith t -> ARITH.subst p v t | Bitv t -> BITV.subst p v t | Adt t -> ADT.subst p v t + | Fpa t -> FPA.subst p v t | Ac t -> if equal p r then v else AC.subst p v t | Term _ -> if equal p r then v else r @@ -329,17 +350,20 @@ end = struct ( ARITH.is_mine_symb sb, not_restricted && BITV.is_mine_symb sb, not_restricted && ADT.is_mine_symb sb, + FPA.is_mine_symb sb, AC.is_mine_symb sb ) with - | true, false, false, false -> + | true, false, false, false, false -> Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () -> ARITH.make t - | false, true, false, false -> + | false, true, false, false, false -> Timers.with_timer Timers.M_Bitv Timers.F_make @@ fun () -> BITV.make t - | false, false, true, false -> + | false, false, true, false, false -> Timers.with_timer Timers.M_Adt Timers.F_make @@ fun () -> ADT.make t - | false, false, false, true -> + | false, false, false, true, false -> + Timers.with_timer FPA.timer Timers.F_make @@ fun () -> FPA.make t + | false, false, false, false, true -> Timers.with_timer Timers.M_AC Timers.F_make @@ fun () -> AC.make t - | false, false, false, false -> term_embed t, [] + | false, false, false, false, false -> term_embed t, [] | _ -> assert false let fully_interpreted sb = @@ -348,19 +372,21 @@ end = struct ( ARITH.is_mine_symb sb, not_restricted && BITV.is_mine_symb sb, not_restricted && ADT.is_mine_symb sb, + FPA.is_mine_symb sb, AC.is_mine_symb sb ) with - | true, false, false, false -> ARITH.fully_interpreted sb - | false, true, false, false -> BITV.fully_interpreted sb - | false, false, true, false -> ADT.fully_interpreted sb - | false, false, false, true -> AC.fully_interpreted sb - | false, false, false, false -> false + | true, false, false, false, false -> ARITH.fully_interpreted sb + | false, true, false, false, false -> BITV.fully_interpreted sb + | false, false, true, false, false -> ADT.fully_interpreted sb + | false, false, false, true, false -> FPA.fully_interpreted sb + | false, false, false, false, true -> AC.fully_interpreted sb + | false, false, false, false, false -> false | _ -> assert false let is_solvable_theory_symbol sb = ARITH.is_mine_symb sb || (not (Options.get_restricted ())) - && (BITV.is_mine_symb sb || ADT.is_mine_symb sb) + && (BITV.is_mine_symb sb || ADT.is_mine_symb sb || FPA.is_mine_symb sb) let is_a_leaf r = match r.v with Term _ | Ac _ -> true | _ -> false @@ -387,6 +413,7 @@ end = struct | Arith a -> ARITH.abstract_selectors a acc | Bitv a -> BITV.abstract_selectors a acc | Adt a -> ADT.abstract_selectors a acc + | Fpa a -> FPA.abstract_selectors a acc | Term _ -> a, acc | Ac a -> AC.abstract_selectors a acc @@ -476,6 +503,9 @@ end = struct | Ty.Tadt _ when not (Options.get_disable_adts ()) -> Timers.with_timer ADT.timer Timers.F_solve @@ fun () -> ADT.solve ra rb pb + | Ty.Tfloat _ -> + Timers.with_timer FPA.timer Timers.F_solve @@ fun () -> + FPA.solve ra rb pb | _ -> Timers.with_timer Timers.M_Combine Timers.F_solve @@ fun () -> solve_uninterpreted ra rb pb @@ -516,6 +546,7 @@ end = struct | _, Ty.Tbitv _ -> BITV.assign_value r distincts eq | _, Ty.Tadt _ when not (Options.get_disable_adts ()) -> ADT.assign_value r distincts eq + | _, Ty.Tfloat _ -> FPA.assign_value r distincts eq | Term _t, Ty.Tbool -> if is_bool_const r then None @@ -585,6 +616,15 @@ Adt.Shostak (struct let embed = embed3 end) +and FPA : (Sig.SHOSTAK with type r = CX.r and type t = CX.r Fpa.abstract) = +Fpa.Shostak (struct + include CX + + let extract = extract4 + + let embed = embed4 +end) + (* Its signature is not Sig.SHOSTAK because it does not provide a solver *) and AC : (Ac.S with type r = CX.r) = Ac.Make (CX) @@ -626,6 +666,7 @@ end module Arith = ARITH module Bitv = BITV module Adt = ADT +module Fpa = FPA module Polynome = TARITH module Ac = AC diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli index b3c4fce686..8ff8dd817c 100644 --- a/src/lib/reasoners/shostak.mli +++ b/src/lib/reasoners/shostak.mli @@ -45,6 +45,9 @@ module Bitv : module Adt : Sig.SHOSTAK with type r = Combine.r and type t = Combine.r Adt.abstract +module Fpa : + Sig.SHOSTAK with type r = Combine.r and type t = Combine.r Fpa.abstract + module Ac : Ac.S with type r = Combine.r and type t = Combine.r Sig.ac module MXH : Map.S with type key = Combine.r diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 3d2dd0c3ea..bce4865b2c 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -2793,34 +2793,24 @@ let reinit_cache () = Labels.clear labels; HC.reinit_cache () -type const = - | Int of int - | RoundingMode of Fpa_rounding.rounding_mode - let z_to_int z = match Z.to_int z with | n -> n | exception Z.Overflow -> Fmt.failwith "error when trying to convert %a to an int" Z.pp_print z -let const_view t = - match term_view t with - | { f = Int n; _ } -> Int (z_to_int n) - | { f = Op (Constr c); ty; _ } when Ty.equal ty Fpa_rounding.fpa_rounding_mode - -> - let c = Fmt.str "%a" DE.Term.Const.print c in - RoundingMode (Fpa_rounding.rounding_mode_of_smt c) - | _ -> Fmt.failwith "unsupported constant: %a" print t - let int_view t = - match const_view t with - | Int n -> n + match term_view t with + | { f = Int n; _ } -> z_to_int n | _ -> Fmt.failwith "The given term %a is not an integer" print t let rounding_mode_view t = - match const_view t with - | RoundingMode m -> m - | _ -> Fmt.failwith "The given term %a is not a rounding mode" print t + match term_view t with + | { f = Op (Constr c); ty; _ } when Ty.equal ty Fpa_rounding.fpa_rounding_mode + -> + let c = Fmt.str "%a" DE.Term.Const.print c in + Some (Fpa_rounding.rounding_mode_of_smt c) + | _ -> None (****************************************************************************) (* Helpers to build typed terms *) @@ -3126,6 +3116,80 @@ end https://smt-lib.org/theories-FloatingPoint.shtml *) module FP = struct + module Names = struct + (* float conversion function *) + let ae_float = "ae.float" + + (* generic float type *) + let t = "ae.fp.t" + + (* arithmetic with rounding mode *) + let add = "ae.fp.add" + + let sub = "ae.fp.sub" + + let mul = "ae.fp.mul" + + let div = "ae.fp.div" + + let fma = "ae.fp.fma" + + let sqrt = "ae.fp.sqrt" + + let round_to_integral = "ae.fp.roundToIntegral" + + let of_real = "ae.fp.from_real" + + (* arithmetic without rounding mode *) + let abs = "ae.fp.abs" + + let neg = "ae.fp.neg" + + let min = "ae.fp.min" + + let max = "ae.fp.max" + + (* comparisons *) + let le = "ae.fp.le" + + let lt = "ae.fp.lt" + + let eq = "ae.fp.eq" + + (* predicates *) + let is_normal = "ae.fp.is_normal" + + let is_subnormal = "ae.fp.is_subnormal" + + let is_zero = "ae.fp.is_zero" + + let is_infinite = "ae.fp.is_infinite" + + let is_nan = "ae.fp.is_nan" + + let is_negative = "ae.fp.is_negative" + + let is_positive = "ae.fp.is_positive" + + (* real conversion *) + let to_real = "ae.fp.to_real" + + (* precision-dependent literals *) + let pow2sb = "ae.fp.pow2sb" + + let max_int = "ae.fp.max_int" + + let max_real = "ae.fp.max_real" + + let pow2sb_real = "ae.fp.pow2sb_real" + + let half_pow2sb_real = "ae.fp.half_pow2sb_real" + + let abs_err_rne_denom = "ae.fp.abs_err_rne_denom" + + let abs_err_denom = "ae.fp.abs_err_denom" + end + let bv_literal_to_z t = match t.f, t.xs with | Sy.Bitv (_, z), [] -> z @@ -3137,14 +3201,85 @@ module FP = struct let neg = Z.equal (bv_literal_to_z sign_t) Z.one in let biased_exp = z_to_int (bv_literal_to_z exp_t) in let mantissa = bv_literal_to_z sig_t in - float (Fp_value.mk_fp_literal ~neg ~biased_exp ~mantissa e) e s + float (Fp_value.mk_fp_literal ~neg ~biased_exp ~mantissa ~e ~s) e s let ieee_format_to_fp bv_t e s = let bv_z = bv_literal_to_z bv_t in let mantissa = Z.extract bv_z 0 (s - 1) in let biased_exp = z_to_int (Z.extract bv_z (s - 1) e) in let neg = Z.testbit bv_z (e + s - 1) in - float (Fp_value.mk_fp_literal ~neg ~biased_exp ~mantissa e) e s + float (Fp_value.mk_fp_literal ~neg ~biased_exp ~mantissa ~e ~s) e s + + let fp_prelude_op eb sb name args ret_ty = + let eb = Ints.of_int eb in + let sb = Ints.of_int sb in + mk_term (Sy.name name) (eb :: sb :: args) ret_ty + + (* arithmetic with rounding mode *) + let add ~eb ~sb ~mode x y = + fp_prelude_op eb sb Names.add [mode; x; y] (Ty.Tfloat (eb, sb)) + + let sub ~eb ~sb ~mode x y = + fp_prelude_op eb sb Names.sub [mode; x; y] (Ty.Tfloat (eb, sb)) + + let mul ~eb ~sb ~mode x y = + fp_prelude_op eb sb Names.mul [mode; x; y] (Ty.Tfloat (eb, sb)) + + let div ~eb ~sb ~mode x y = + fp_prelude_op eb sb Names.div [mode; x; y] (Ty.Tfloat (eb, sb)) + + let fma ~eb ~sb ~mode x y z = + fp_prelude_op eb sb Names.fma [mode; x; y; z] (Ty.Tfloat (eb, sb)) + + let sqrt ~eb ~sb ~mode x = + fp_prelude_op eb sb Names.sqrt [mode; x] (Ty.Tfloat (eb, sb)) + + let round_to_integral ~eb ~sb ~mode x = + fp_prelude_op eb sb Names.round_to_integral [mode; x] (Ty.Tfloat (eb, sb)) + + let of_real ~eb ~sb ~mode x = + fp_prelude_op eb sb Names.of_real [mode; x] (Ty.Tfloat (eb, sb)) + + (* arithmetic without rounding mode *) + let abs ~eb ~sb x = fp_prelude_op eb sb Names.abs [x] (Ty.Tfloat (eb, sb)) + + let neg ~eb ~sb x = fp_prelude_op eb sb Names.neg [x] (Ty.Tfloat (eb, sb)) + + let min ~eb ~sb x y = + fp_prelude_op eb sb Names.min [x; y] (Ty.Tfloat (eb, sb)) + + let max ~eb ~sb x y = + fp_prelude_op eb sb Names.max [x; y] (Ty.Tfloat (eb, sb)) + + (* comparisons *) + let le ~eb ~sb x y = fp_prelude_op eb sb Names.le [x; y] Ty.Tbool + + let lt ~eb ~sb x y = fp_prelude_op eb sb Names.lt [x; y] Ty.Tbool + + let ge ~eb ~sb x y = le ~eb ~sb y x + + let gt ~eb ~sb x y = lt ~eb ~sb y x + + let eq ~eb ~sb x y = fp_prelude_op eb sb Names.eq [x; y] Ty.Tbool + + (* predicates *) + let is_normal ~eb ~sb x = fp_prelude_op eb sb Names.is_normal [x] Ty.Tbool + + let is_subnormal ~eb ~sb x = + fp_prelude_op eb sb Names.is_subnormal [x] Ty.Tbool + + let is_zero ~eb ~sb x = fp_prelude_op eb sb Names.is_zero [x] Ty.Tbool + + let is_infinite ~eb ~sb x = fp_prelude_op eb sb Names.is_infinite [x] Ty.Tbool + + let is_nan ~eb ~sb x = fp_prelude_op eb sb Names.is_nan [x] Ty.Tbool + + let is_negative ~eb ~sb x = fp_prelude_op eb sb Names.is_negative [x] Ty.Tbool + + let is_positive ~eb ~sb x = fp_prelude_op eb sb Names.is_positive [x] Ty.Tbool + + (* real conversion *) + let to_real ~eb ~sb x = fp_prelude_op eb sb Names.to_real [x] Ty.Treal end (** Constructors from the smtlib theory of functional arrays with extensionality diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 6b48c3189a..6607ddd8aa 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -184,10 +184,9 @@ val int_view : t -> int @raise Failure if the expression is not a constant integer. *) -val rounding_mode_view : t -> Fpa_rounding.rounding_mode -(** Extracts the rounding mode value of the expression, if there is one. - - @raise Failure if the expression is not a constant rounding mode.*) +val rounding_mode_view : t -> Fpa_rounding.rounding_mode option +(** Extracts the rounding mode value of the expression, if there is one. Return + [None] if the expression is not a constant rounding mode. *) (** pretty printing *) @@ -682,9 +681,151 @@ end https://smt-lib.org/theories-FloatingPoint.shtml *) module FP : sig + module Names : sig + (** {2 Float conversion functions} *) + + val ae_float : string + + (** {2 Generic float type} *) + + val t : string + + (** {2 Arithmetic with rounding mode} *) + + val add : string + + val sub : string + + val mul : string + + val div : string + + val fma : string + + val sqrt : string + + val round_to_integral : string + + val of_real : string + + (** {2 Arithmetic without rounding mode} *) + + val abs : string + + val neg : string + + val min : string + + val max : string + + (** {2 Comparisons} *) + + val le : string + + val lt : string + + val eq : string + + (** {2 Predicates} *) + + val is_normal : string + + val is_subnormal : string + + val is_zero : string + + val is_infinite : string + + val is_nan : string + + val is_negative : string + + val is_positive : string + + (** {2 Real conversion} *) + + val to_real : string + + (** {2 Precision-dependent literals} *) + + val pow2sb : string + + val max_int : string + + val max_real : string + + val pow2sb_real : string + + val half_pow2sb_real : string + + val abs_err_rne_denom : string + + val abs_err_denom : string + end + val fp : t -> t -> t -> int -> int -> t val ieee_format_to_fp : t -> int -> int -> t + + (** {2 Arithmetic with rounding mode} *) + + val add : eb:int -> sb:int -> mode:t -> t -> t -> t + + val sub : eb:int -> sb:int -> mode:t -> t -> t -> t + + val mul : eb:int -> sb:int -> mode:t -> t -> t -> t + + val div : eb:int -> sb:int -> mode:t -> t -> t -> t + + val fma : eb:int -> sb:int -> mode:t -> t -> t -> t -> t + + val sqrt : eb:int -> sb:int -> mode:t -> t -> t + + val round_to_integral : eb:int -> sb:int -> mode:t -> t -> t + + val of_real : eb:int -> sb:int -> mode:t -> t -> t + + (** {2 Arithmetic without rounding mode} *) + + val abs : eb:int -> sb:int -> t -> t + + val neg : eb:int -> sb:int -> t -> t + + val min : eb:int -> sb:int -> t -> t -> t + + val max : eb:int -> sb:int -> t -> t -> t + + (** {2 Comparisons} *) + + val le : eb:int -> sb:int -> t -> t -> t + + val lt : eb:int -> sb:int -> t -> t -> t + + val ge : eb:int -> sb:int -> t -> t -> t + + val gt : eb:int -> sb:int -> t -> t -> t + + val eq : eb:int -> sb:int -> t -> t -> t + + (** {2 Predicates} *) + + val is_normal : eb:int -> sb:int -> t -> t + + val is_subnormal : eb:int -> sb:int -> t -> t + + val is_zero : eb:int -> sb:int -> t -> t + + val is_infinite : eb:int -> sb:int -> t -> t + + val is_nan : eb:int -> sb:int -> t -> t + + val is_negative : eb:int -> sb:int -> t -> t + + val is_positive : eb:int -> sb:int -> t -> t + + (** {2 Real conversion} *) + + val to_real : eb:int -> sb:int -> t -> t end (** Constructors from the smtlib theory of functional arrays with extensionality diff --git a/src/lib/structures/fp_value.ml b/src/lib/structures/fp_value.ml index b3c67bd586..9647522db0 100644 --- a/src/lib/structures/fp_value.ml +++ b/src/lib/structures/fp_value.ml @@ -18,40 +18,79 @@ (** Literal floating-point values. *) +module Q = Numbers.Q + type t = | Plus_infinity | Minus_infinity | Plus_zero | Minus_zero | NaN - | Finite of - { neg : bool; - biased_exp : int; - significand : Z.t - } + | Finite of Q.t let compare v1 v2 = Util.compare_algebraic v1 v2 (function - | Finite f1, Finite f2 -> - let c = Bool.compare f1.neg f2.neg in - if c <> 0 - then c - else - let c = Int.compare f1.biased_exp f2.biased_exp in - if c <> 0 then c else Z.compare f1.significand f2.significand + | Finite q1, Finite q2 -> Q.compare q1 q2 | ( _, ( Plus_infinity | Minus_infinity | Plus_zero | Minus_zero | NaN | Finite _ ) ) -> assert false) +let equal v1 v2 = + match v1, v2 with + | Plus_infinity, Plus_infinity + | Minus_infinity, Minus_infinity + | Plus_zero, Plus_zero + | Minus_zero, Minus_zero + | NaN, NaN -> + true + | Finite q1, Finite q2 when Q.equal q1 q2 -> true + | _, _ -> false + +(* This works because we know that [q] is always dyadic since its created from + an SMT-LIB float literal. *) +let hex_of_q q = + let sign = if Q.sign q < 0 then "-" else "" in + let num = Z.abs (Q.num q) in + let k = Z.numbits (Q.den q) - 1 in + Fmt.str "%s0x%sp-%d" sign (Z.format "%x" num) k + let pp ppf = function | Plus_infinity -> Fmt.pf ppf "+oo" | Minus_infinity -> Fmt.pf ppf "-oo" | Plus_zero -> Fmt.pf ppf "+zero" | Minus_zero -> Fmt.pf ppf "-zero" | NaN -> Fmt.pf ppf "NaN" - | Finite { neg; biased_exp; significand } -> - Fmt.pf ppf "fp[%b;%d;%s]" neg biased_exp (Z.to_string significand) + | Finite q -> Fmt.pf ppf "fp[%s]" (hex_of_q q) + +(* bias = 2^(eb-1) - 1 *) +let fp_bias eb = (1 lsl (eb - 1)) - 1 + +(* min_exp = bias + sb - 2 *) +let fp_min_exp eb sb = fp_bias eb + sb - 2 + +(* rational value -> (neg, biased_exp, significand) *) +let q_to_bvs eb sb q = + let bias = fp_bias eb in + let min_exp = fp_min_exp eb sb in + let neg = Q.sign q < 0 in + (* (_, m, e) with m*2^e = |q|, e = max(floor(log2|q|) + 1 - sb, -min_exp). *) + let _, m, e = + Fpa_rounding.float_of_rational sb min_exp + Dolmen.Std.Builtin.Float.RoundNearestTiesToEven (Q.abs q) + in + (* hidden_bit = 2^(sb-1), m >= hidden_bit -> normal *) + let hidden_bit = Z.shift_left Z.one (sb - 1) in + let biased_exp, significand = + if Z.compare m hidden_bit >= 0 + then + (* normal: biased_exp = (e + sb - 1) + bias; strip the hidden bit. *) + e + (sb - 1) + bias, Z.sub m hidden_bit + else + (* subnormal: biased_exp = 0; m is the bare significand. *) + 0, m + in + neg, biased_exp, significand let pp_smtlib eb sb ppf = function | Plus_infinity -> Fmt.pf ppf "(_ +oo %d %d)" eb sb @@ -59,14 +98,37 @@ let pp_smtlib eb sb ppf = function | Plus_zero -> Fmt.pf ppf "(_ +zero %d %d)" eb sb | Minus_zero -> Fmt.pf ppf "(_ -zero %d %d)" eb sb | NaN -> Fmt.pf ppf "(_ NaN %d %d)" eb sb - | Finite { neg; biased_exp; significand } -> + | Finite q -> + let neg, biased_exp, significand = q_to_bvs eb sb q in let bfmt n = Fmt.str "%%0%db" n in let sign_s = if neg then "1" else "0" in let exp_s = Z.format (bfmt eb) (Z.of_int biased_exp) in let sig_s = Z.format (bfmt (sb - 1)) significand in Fmt.pf ppf "(fp #b%s #b%s #b%s)" sign_s exp_s sig_s -let mk_fp_literal ~neg ~biased_exp ~mantissa e = +(* (neg, biased_exp, significand) -> rational value *) +let bvs_to_q ~neg ~biased_exp ~mantissa eb sb = + let bias = fp_bias eb in + let significand_full, exp_shift = + if biased_exp > 0 + then + (* normal: significand_full = 2^(sb-1) + mantissa (restore hidden bit), + exp_shift = biased_exp - bias - (sb-1) (actual_exp - (sb-1)) *) + Z.add (Z.shift_left Z.one (sb - 1)) mantissa, biased_exp - bias - (sb - 1) + else + (* subnormal: significand_full = mantissa (no hidden bit), exp_shift = 1 - + bias - (sb-1) = -min_exp (fixed actual_exp) *) + mantissa, -fp_min_exp eb sb + in + (* significand_full * 2^exp_shift *) + let abs_q = + if exp_shift >= 0 + then Q.mult_2exp (Q.from_z significand_full) exp_shift + else Q.div_2exp (Q.from_z significand_full) (-exp_shift) + in + if neg then Q.minus abs_q else abs_q + +let mk_fp_literal ~neg ~biased_exp ~mantissa ~e ~s = let max_exp = (1 lsl e) - 1 in (* TODO: these transformations should not be done this early as they can affect matching (we are transforming terms received from the parser into @@ -83,4 +145,4 @@ let mk_fp_literal ~neg ~biased_exp ~mantissa e = then (* zero exponent + zero significand: signed zero *) if neg then Minus_zero else Plus_zero - else Finite { neg; biased_exp; significand = mantissa } + else Finite (bvs_to_q ~neg ~biased_exp ~mantissa e s) diff --git a/src/lib/structures/fp_value.mli b/src/lib/structures/fp_value.mli index 63f9a27ff9..eb60cb8cad 100644 --- a/src/lib/structures/fp_value.mli +++ b/src/lib/structures/fp_value.mli @@ -24,14 +24,12 @@ type t = | Plus_zero | Minus_zero | NaN - | Finite of - { neg : bool; - biased_exp : int; - significand : Z.t - } + | Finite of Numbers.Q.t val compare : t -> t -> int +val equal : t -> t -> bool + val pp : t Fmt.t (** [pp ppf v] prints the concrete FP value [v] in the Alt-Ergo native format. *) @@ -40,8 +38,10 @@ val pp_smtlib : int -> int -> t Fmt.t (** [pp_smtlib eb sb ppf v] prints the concrete FP value [v] of precision [(eb, sb)] in the SMT-LIB format. *) -val mk_fp_literal : neg:bool -> biased_exp:int -> mantissa:Z.t -> int -> t -(** [mk_fp_literal neg biased_exp mantissa e] creates a floating-point literal - with the geiven parameters, where [neg] is the sign bit, [biased_exp] is the - biased exponent, [mantissa] is the mantissa bits (without the hidden bit), - [e] is the exponent width. *) +val mk_fp_literal : + neg:bool -> biased_exp:int -> mantissa:Z.t -> e:int -> s:int -> t +(** [mk_fp_literal ~neg ~biased_exp ~mantissa ~e ~s] creates a floating-point + literal where [neg] is the sign bit, [biased_exp] is the biased exponent, + [mantissa] is the significand bits (without the hidden bit), [e] is the + exponent width, and [s] is the significand width (including the hidden bit). +*) diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index 89634f9d93..0473e2d92e 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -29,46 +29,51 @@ module DStd = Dolmen.Std module DE = DStd.Expr module Q = Numbers.Q module Z = Numbers.Z +module RM = DStd.Builtin.Float -(** The five standard rounding modes of the SMTLIB. Note that the SMTLIB defines - these rounding modes to be the only possible modes. - - Note: keep the constructors in the same order as in the definition in - [rounding_mode_to_int] so that it gets simplified to the identity. *) -type rounding_mode = - | NearestTiesToEven - | ToZero - | Up - | Down - | NearestTiesToAway - -let[@inline] rounding_mode_to_int = function - | NearestTiesToEven -> 0 - | ToZero -> 1 - | Up -> 2 - | Down -> 3 - | NearestTiesToAway -> 4 +type rounding_mode = unit Dolmen.Std.Builtin.Float.t +(** We reuse Dolmen's own representation of the rounding modes (the type + [Dolmen.Std.Builtin.Float.t], restricted to its five nullary "Round*" + constructors). + + TODO: group rounding modes in their own enum in Dolmen *) + +let[@inline] rounding_mode_to_int : unit RM.t -> int = function + | RM.RoundNearestTiesToEven -> 0 + | RM.RoundTowardZero -> 1 + | RM.RoundTowardPositive -> 2 + | RM.RoundTowardNegative -> 3 + | RM.RoundNearestTiesToAway -> 4 + | _ -> invalid_arg "rounding_mode_to_int: not a rounding mode" let compare_rounding_mode rm1 rm2 = Int.compare (rounding_mode_to_int rm1) (rounding_mode_to_int rm2) -let constrs = [NearestTiesToEven; ToZero; Up; Down; NearestTiesToAway] - -let to_smt_string = function - | NearestTiesToEven -> "RNE" - | ToZero -> "RTZ" - | Up -> "RTP" - | Down -> "RTN" - | NearestTiesToAway -> "RNA" +let constrs = + RM. + [ RoundNearestTiesToEven; + RoundTowardZero; + RoundTowardPositive; + RoundTowardNegative; + RoundNearestTiesToAway ] + +let to_smt_string : unit RM.t -> string = function + | RM.RoundNearestTiesToEven -> "RNE" + | RM.RoundTowardZero -> "RTZ" + | RM.RoundTowardPositive -> "RTP" + | RM.RoundTowardNegative -> "RTN" + | RM.RoundNearestTiesToAway -> "RNA" + | _ -> invalid_arg "to_smt_string: not a rounding mode" let pp_rounding_mode = Fmt.of_to_string to_smt_string -let to_ae_string = function - | NearestTiesToEven -> "NearestTiesToEven" - | ToZero -> "ToZero" - | Up -> "Up" - | Down -> "Down" - | NearestTiesToAway -> "NearestTiesToAway" +let to_ae_string : unit RM.t -> string = function + | RM.RoundNearestTiesToEven -> "NearestTiesToEven" + | RM.RoundTowardZero -> "ToZero" + | RM.RoundTowardPositive -> "Up" + | RM.RoundTowardNegative -> "Down" + | RM.RoundNearestTiesToAway -> "NearestTiesToAway" + | _ -> invalid_arg "to_ae_string: not a rounding mode" let fpa_rounding_mode_ae_type_name = "fpa_rounding_mode" @@ -176,12 +181,12 @@ let signed_one y = assert (tmp <> 0); if tmp > 0 then Z.one else Z.m_one -let round_big_int (mode : rounding_mode) y = +let round_big_int (mode : unit RM.t) y = match mode with - | Up -> Q.num (Q.ceiling y) - | Down -> Q.num (Q.floor y) - | ToZero -> Q.truncate y - | NearestTiesToEven -> + | RM.RoundTowardPositive -> Q.num (Q.ceiling y) + | RM.RoundTowardNegative -> Q.num (Q.floor y) + | RM.RoundTowardZero -> Q.truncate y + | RM.RoundNearestTiesToEven -> let z = Q.truncate y in let diff = Q.abs (Q.sub y (Q.from_z z)) in if Q.sign diff = 0 @@ -195,7 +200,7 @@ let round_big_int (mode : rounding_mode) y = else if Z.testbit z 0 then Z.add z (signed_one y) else z - | NearestTiesToAway -> + | RM.RoundNearestTiesToAway -> let z = Q.truncate y in let diff = Q.abs (Q.sub y (Q.from_z z)) in if Q.sign diff = 0 @@ -203,6 +208,7 @@ let round_big_int (mode : rounding_mode) y = else if Q.compare diff half < 0 then z else Z.add z (signed_one y) + | _ -> invalid_arg "round_big_int: not a rounding mode" let to_mantissa_exp prec exp mode x = let sign_x = Q.sign x in @@ -218,7 +224,7 @@ let to_mantissa_exp prec exp mode x = r_y, e' module MQ = Map.Make (struct - type t = int * int * rounding_mode * Q.t + type t = int * int * unit RM.t * Q.t let compare (prec1, exp1, mode1, x1) (prec2, exp2, mode2, x2) = let c = Q.compare x1 x2 in diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli index 62cb48cea3..ee96307d0d 100644 --- a/src/lib/structures/fpa_rounding.mli +++ b/src/lib/structures/fpa_rounding.mli @@ -27,17 +27,10 @@ module DE = Dolmen.Std.Expr -(** The rounding modes for the Floating Point Arithmetic theory. In the legacy - frontend, the rounding mode type was `fpa_rounding_mode` and defined 5 - rounding modes (see the [rounding_mode] type below). The SMT2 standard - defines the exact same rounding modes, but with different identifiers. *) - -type rounding_mode = - | NearestTiesToEven - | ToZero - | Up - | Down - | NearestTiesToAway +type rounding_mode = unit Dolmen.Std.Builtin.Float.t +(** We reuse Dolmen's own representation of the rounding modes (the type + [Dolmen.Std.Builtin.Float.t], restricted to its five nullary "Round*" + constructors). *) val compare_rounding_mode : rounding_mode -> rounding_mode -> int diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 08d25b05d9..42302118c8 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -148,6 +148,8 @@ let print = fst (print_generic None) None let fresh_tvar () = Tvar (DE.Ty.Var.mk "A") +let named_tvar name = Tvar (DE.Ty.Var.mk name) + let rec compare t1 t2 = match t1, t2 with | Tvar v1, Tvar v2 -> DE.Ty.Var.compare v1 v2 diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index bdd96818b1..78070f65ab 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -121,6 +121,9 @@ val tunit : t val fresh_tvar : unit -> t (** Wrap the {!val:fresh_var} function to return a type. *) +val named_tvar : string -> t +(** Create a type variable with a specific name. *) + val fresh_empty_text : unit -> t (** Return a fesh abstract type. *) diff --git a/src/lib/util/theories.ml b/src/lib/util/theories.ml index 5d6ceb2ef2..694f53aafa 100644 --- a/src/lib/util/theories.ml +++ b/src/lib/util/theories.ml @@ -67,24 +67,33 @@ let pp ppf = function | ADT -> Format.fprintf ppf "adt" | AC -> Format.fprintf ppf "ac" -let filename = Format.asprintf "/%a.ae" pp_prelude +let prelude_filename = function + | Fpa -> "fpa.ae" + | Ria -> "ria.ae" + | Nra -> "nra.ae" + | SmtFloat -> "smt-lib-fpa.smt2" -let get_prelude name = +let filename th = Fmt.str "/%s" (prelude_filename th) + +let get_prelude prelude = + let name = prelude_filename prelude in match Preludes.read name with | Some content -> content | None -> failwith (Fmt.str "Missing internal prelude: %s" name) -let fpa_prelude = get_prelude "fpa.ae" +let fpa_prelude = get_prelude Fpa + +let ria_prelude = get_prelude Ria -let ria_prelude = get_prelude "ria.ae" +let nra_prelude = get_prelude Nra -let nra_prelude = get_prelude "nra.ae" +let smt_lib_fpa_prelude = get_prelude SmtFloat let content = function | Fpa -> Some fpa_prelude | Ria -> Some ria_prelude | Nra -> Some nra_prelude - | SmtFloat -> None + | SmtFloat -> Some smt_lib_fpa_prelude let all_preludes = [Fpa; Ria; Nra; SmtFloat] diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml index 6d4acda0dd..ed12541d29 100644 --- a/src/lib/util/timers.ml +++ b/src/lib/util/timers.ml @@ -45,6 +45,7 @@ type ty_module = | M_Triggers | M_Simplex | M_Ite + | M_Fpa let[@inline] ty_module_to_enum = function | M_None -> 0 @@ -62,8 +63,9 @@ let[@inline] ty_module_to_enum = function | M_Triggers -> 12 | M_Simplex -> 13 | M_Ite -> 14 + | M_Fpa -> 15 -let max_ty_module = 14 +let max_ty_module = 15 let all_modules = let l = @@ -81,7 +83,8 @@ let all_modules = M_Expr; M_Triggers; M_Simplex; - M_Ite ] + M_Ite; + M_Fpa ] in assert (List.length l = max_ty_module + 1); l @@ -179,6 +182,7 @@ let string_of_ty_module k = | M_Triggers -> "Triggers" | M_Simplex -> "Simplex" | M_Ite -> "Ite" + | M_Fpa -> "Fpa" let string_of_ty_function f = match f with diff --git a/src/lib/util/timers.mli b/src/lib/util/timers.mli index e85dd91b0a..e6e558b1fb 100644 --- a/src/lib/util/timers.mli +++ b/src/lib/util/timers.mli @@ -41,6 +41,7 @@ type ty_module = | M_Triggers | M_Simplex | M_Ite + | M_Fpa type ty_function = | F_add diff --git a/src/preludes/smt-lib-fpa.smt2 b/src/preludes/smt-lib-fpa.smt2 new file mode 100644 index 0000000000..d46f030145 --- /dev/null +++ b/src/preludes/smt-lib-fpa.smt2 @@ -0,0 +1,1931 @@ +; This axiomatization is based on axiomatization generated by Why3's Alt-Ergo +; driver, the axioms were rewritten to take as arguments the type parameters +; of the Float type (eb, sb), and to use Alt-Ergo's builtin `int.pow2` symbol +; instead of an axiomatized one. Triggers were also added to all axioms (that +; did not already have axioms). +(set-logic ALL) +(set-info :smt-lib-version 2.6) +; --- interpreted type-dependent constants --- +(declare-fun ae.fp.max_int (Int Int) Int) +(declare-fun ae.fp.max_real (Int Int) Real) +(declare-fun ae.fp.pow2sb (Int Int) Int) +(declare-fun ae.fp.pow2sb_real (Int Int) Real) +(declare-fun ae.fp.half_pow2sb_real (Int Int) Real) +(declare-fun ae.fp.abs_err_rne_denom (Int Int) Real) +(declare-fun ae.fp.abs_err_denom (Int Int) Real) +; --- +(declare-sort ae.fp.t 0) +(declare-fun ae.fp.to_real (Int Int ae.fp.t) Real) +(declare-fun ae.fp.is_finite (Int Int ae.fp.t) Bool) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (<= (- (ae.fp.max_real eb sb)) (ae.fp.to_real eb sb x))) + :pattern ((ae.fp.is_finite eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (<= (ae.fp.to_real eb sb x) (ae.fp.max_real eb sb))) + :pattern ((ae.fp.is_finite eb sb x))))) +(declare-fun ae.fp.zero (Int Int) ae.fp.t) +(declare-fun ae.fp.add (Int Int RoundingMode ae.fp.t ae.fp.t) ae.fp.t) +(declare-fun ae.fp.sub (Int Int RoundingMode ae.fp.t ae.fp.t) ae.fp.t) +(declare-fun ae.fp.mul (Int Int RoundingMode ae.fp.t ae.fp.t) ae.fp.t) +(declare-fun ae.fp.div (Int Int RoundingMode ae.fp.t ae.fp.t) ae.fp.t) +(declare-fun ae.fp.abs (Int Int ae.fp.t) ae.fp.t) +(declare-fun ae.fp.neg (Int Int ae.fp.t) ae.fp.t) +(declare-fun ae.fp.fma (Int Int RoundingMode ae.fp.t ae.fp.t ae.fp.t) + ae.fp.t) +(declare-fun ae.fp.sqrt (Int Int RoundingMode ae.fp.t) ae.fp.t) +(declare-fun ae.fp.roundToIntegral (Int Int RoundingMode ae.fp.t) ae.fp.t) +(declare-fun ae.fp.min (Int Int ae.fp.t ae.fp.t) ae.fp.t) +(declare-fun ae.fp.max (Int Int ae.fp.t ae.fp.t) ae.fp.t) +(declare-fun ae.fp.le (Int Int ae.fp.t ae.fp.t) Bool) +(declare-fun ae.fp.lt (Int Int ae.fp.t ae.fp.t) Bool) +(declare-fun ae.fp.eq (Int Int ae.fp.t ae.fp.t) Bool) +(declare-fun ae.fp.is_zero (Int Int ae.fp.t) Bool) +(declare-fun ae.fp.is_infinite (Int Int ae.fp.t) Bool) +(declare-fun ae.fp.is_nan (Int Int ae.fp.t) Bool) +(declare-fun ae.fp.is_positive (Int Int ae.fp.t) Bool) +(declare-fun ae.fp.is_negative (Int Int ae.fp.t) Bool) +(define-fun is_plus_infinity ((eb Int) (sb Int) (x ae.fp.t)) Bool + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_positive eb sb x))) +(define-fun is_minus_infinity ((eb Int) (sb Int) (x ae.fp.t)) Bool + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_negative eb sb x))) +(define-fun is_not_nan ((eb Int) (sb Int) (x ae.fp.t)) Bool + (or (ae.fp.is_finite eb sb x) (ae.fp.is_infinite eb sb x))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (is_not_nan eb sb x) + (not (ae.fp.is_nan eb sb x))) + :pattern ((ae.fp.is_finite eb sb x)) :pattern ((ae.fp.is_infinite eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (not (ae.fp.is_nan eb sb x)) + (is_not_nan eb sb x)) + :pattern ((ae.fp.is_nan eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (not (ae.fp.is_finite eb sb x)) + (or (ae.fp.is_infinite eb sb x) (ae.fp.is_nan eb sb x))) + :pattern ((ae.fp.is_finite eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (or (ae.fp.is_infinite eb sb x) (ae.fp.is_nan eb sb x)) + (not (ae.fp.is_finite eb sb x))) + :pattern ((ae.fp.is_infinite eb sb x)) :pattern ((ae.fp.is_nan eb sb x))))) +(assert (forall ((eb Int) (sb Int)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_positive eb sb (ae.fp.zero eb sb))) + :pattern ((ae.fp.zero eb sb))))) +(assert (forall ((eb Int) (sb Int)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_zero eb sb (ae.fp.zero eb sb))) + :pattern ((ae.fp.zero eb sb))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_zero eb sb x) + (ae.fp.is_finite eb sb x)) + :pattern ((ae.fp.is_zero eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_zero eb sb x) + (= (ae.fp.to_real eb sb x) 0.0)) + :pattern ((ae.fp.is_zero eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (= (ae.fp.to_real eb sb x) 0.0)) + (ae.fp.is_zero eb sb x)) + :pattern ((ae.fp.is_zero eb sb x))))) +(declare-fun ae.fp.of_int (Int Int RoundingMode Int) ae.fp.t) +(declare-fun ae.fp.to_int (Int Int RoundingMode ae.fp.t) Int) +(assert (forall ((eb Int) (sb Int) (m RoundingMode)) + (! (=> (and (< 1 eb) (< 1 sb)) + (= (ae.fp.zero eb sb) (ae.fp.of_int eb sb m 0))) + :pattern ((ae.fp.of_int eb sb m 0))))) +(assert (forall ((eb Int) (sb Int)) + (! (=> (and (< 1 eb) (< 1 sb)) + (= (ae.fp.max_int eb sb) + (- (int.pow2 (int.pow2 (- eb 1))) + (int.pow2 (- (int.pow2 (- eb 1)) sb))))) + :pattern ((ae.fp.max_int eb sb))))) +(assert (forall ((eb Int) (sb Int)) + (! (=> (and (< 1 eb) (< 1 sb)) + (= (ae.fp.max_real eb sb) (to_real (ae.fp.max_int eb sb)))) + :pattern ((ae.fp.max_real eb sb))))) +(define-fun in_range ((eb Int) (sb Int) (x Real)) Bool + (<= (- (ae.fp.max_real eb sb)) x (ae.fp.max_real eb sb))) +(define-fun in_int_range ((eb Int) (sb Int) (i Int)) Bool + (<= (- (ae.fp.max_int eb sb)) i (ae.fp.max_int eb sb))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (in_range eb sb (ae.fp.to_real eb sb x))) + :pattern ((ae.fp.is_finite eb sb x))))) +(define-fun no_overflow ((eb Int) (sb Int) (m RoundingMode) (x Real)) Bool + (in_range eb sb (ae.float eb sb m x))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x Real)) + (! (=> (and (< 1 eb) (< 1 sb)) (in_range eb sb x) + (no_overflow eb sb m x)) + :pattern ((ae.float eb sb m x))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (= (ae.float eb sb m (ae.fp.to_real eb sb x)) + (ae.fp.to_real eb sb x))) + :pattern ((ae.float eb sb m (ae.fp.to_real eb sb x)))))) +(assert (forall ((eb Int) (sb Int) (x Real)) + (! (=> (and (< 1 eb) (< 1 sb)) (<= (ae.float eb sb RTN x) x)) + :pattern ((ae.float eb sb RTN x))))) +(assert (forall ((eb Int) (sb Int) (x Real)) + (! (=> (and (< 1 eb) (< 1 sb)) (<= x (ae.float eb sb RTP x))) + :pattern ((ae.float eb sb RTP x))))) +(assert (forall ((eb Int) (sb Int) (x Real)) + (! (=> (and (< 1 eb) (< 1 sb)) + (= (ae.float eb sb RTN (- x)) (- (ae.float eb sb RTP x)))) + :pattern ((ae.float eb sb RTN (- x)))))) +(assert (forall ((eb Int) (sb Int) (x Real)) + (! (=> (and (< 1 eb) (< 1 sb)) + (= (ae.float eb sb RTP (- x)) (- (ae.float eb sb RTN x)))) + :pattern ((ae.float eb sb RTP (- x)))))) +(assert (forall ((eb Int) (sb Int)) + (! (=> (and (< 1 eb) (< 1 sb)) (= (ae.fp.pow2sb eb sb) (int.pow2 sb))) + :pattern ((ae.fp.pow2sb eb sb))))) +(define-fun in_safe_int_range ((eb Int) (sb Int) (i Int)) Bool + (<= (- (ae.fp.pow2sb eb sb)) i (ae.fp.pow2sb eb sb))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (i Int)) + (! (=> (and (< 1 eb) (< 1 sb)) (in_safe_int_range eb sb i) + (= (ae.float eb sb m (to_real i)) (to_real i))) + :pattern ((ae.float eb sb m (to_real i)))))) +(declare-fun ae.fp.from_real (Int Int RoundingMode Real) ae.fp.t) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (r Real)) + (! (=> (and (< 1 eb) (< 1 sb)) (in_range eb sb (ae.float eb sb m r)) + (ae.fp.is_finite eb sb (ae.fp.from_real eb sb m r))) + :pattern ((ae.fp.from_real eb sb m r))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (r Real)) + (! (=> (and (< 1 eb) (< 1 sb)) (in_range eb sb (ae.float eb sb m r)) + (= (ae.fp.to_real eb sb (ae.fp.from_real eb sb m r)) + (ae.float eb sb m r))) + :pattern ((ae.fp.from_real eb sb m r))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (r Real)) + (! (=> (and (< 1 eb) (< 1 sb)) + (< (ae.float eb sb m r) (- (ae.fp.max_real eb sb))) + (ae.fp.is_infinite eb sb (ae.fp.from_real eb sb m r))) + :pattern ((ae.fp.from_real eb sb m r))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (r Real)) + (! (=> (and (< 1 eb) (< 1 sb)) + (< (ae.float eb sb m r) (- (ae.fp.max_real eb sb))) + (ae.fp.is_negative eb sb (ae.fp.from_real eb sb m r))) + :pattern ((ae.fp.from_real eb sb m r))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (r Real)) + (! (=> (and (< 1 eb) (< 1 sb)) + (< (ae.fp.max_real eb sb) (ae.float eb sb m r)) + (ae.fp.is_infinite eb sb (ae.fp.from_real eb sb m r))) + :pattern ((ae.fp.from_real eb sb m r))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (r Real)) + (! (=> (and (< 1 eb) (< 1 sb)) + (< (ae.fp.max_real eb sb) (ae.float eb sb m r)) + (ae.fp.is_positive eb sb (ae.fp.from_real eb sb m r))) + :pattern ((ae.fp.from_real eb sb m r))))) +(define-fun same_sign ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) Bool + (or (and (ae.fp.is_positive eb sb x) (ae.fp.is_positive eb sb y)) + (and (ae.fp.is_negative eb sb x) (ae.fp.is_negative eb sb y)))) +(define-fun diff_sign ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) Bool + (or (and (ae.fp.is_positive eb sb x) (ae.fp.is_negative eb sb y)) + (and (ae.fp.is_negative eb sb x) (ae.fp.is_positive eb sb y)))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) (not (ae.fp.is_zero eb sb x)) + (ae.fp.eq eb sb x y) (= x y)) + :pattern ((ae.fp.eq eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) (= x y) (ae.fp.eq eb sb x y)) + :pattern ((ae.fp.eq eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.eq eb sb x x)) + :pattern ((ae.fp.is_finite eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.eq eb sb x y) + (ae.fp.eq eb sb y x)) + :pattern ((ae.fp.eq eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t) (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.eq eb sb x y) + (ae.fp.eq eb sb y z) (ae.fp.eq eb sb x z)) + :pattern ((ae.fp.eq eb sb x y) (ae.fp.eq eb sb y z))))) +(assert (forall ((eb Int) (sb Int)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.eq eb sb (ae.fp.zero eb sb) + (ae.fp.neg eb sb (ae.fp.zero eb sb)))) + :pattern ((ae.fp.zero eb sb))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (ae.fp.eq eb sb x y) + (= (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + :pattern ((ae.fp.eq eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (= (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.eq eb sb x y)) + :pattern ((ae.fp.eq eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.eq eb sb x y) + (is_not_nan eb sb x)) + :pattern ((ae.fp.eq eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.eq eb sb x y) + (is_not_nan eb sb y)) + :pattern ((ae.fp.eq eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.eq eb sb x y) + (or (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (same_sign eb sb x y))))) + :pattern ((ae.fp.eq eb sb x y))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (ae.fp.lt eb sb x y) + (< (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + :pattern ((ae.fp.lt eb sb x y))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (< (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.lt eb sb x y)) + :pattern ((ae.fp.lt eb sb x y))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (ae.fp.le eb sb x y) + (<= (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + :pattern ((ae.fp.le eb sb x y))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (<= (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.le eb sb x y)) + :pattern ((ae.fp.le eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t) (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.le eb sb x y) (ae.fp.lt eb sb y z)) + (ae.fp.lt eb sb x z)) + :pattern ((ae.fp.le eb sb x y) (ae.fp.lt eb sb y z))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t) (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.lt eb sb x y) (ae.fp.le eb sb y z)) + (ae.fp.lt eb sb x z)) + :pattern ((ae.fp.lt eb sb x y) (ae.fp.le eb sb y z))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.le eb sb x y) (ae.fp.le eb sb y x)) + (ae.fp.eq eb sb x y)) + :pattern ((ae.fp.le eb sb x y) (ae.fp.le eb sb y x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (not (ae.fp.lt eb sb x y)) + (and (is_not_nan eb sb x) (is_not_nan eb sb y))) + (ae.fp.le eb sb y x)) + :pattern ((ae.fp.lt eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (not (ae.fp.lt eb sb y x)) + (and (is_not_nan eb sb x) (is_not_nan eb sb y))) + (ae.fp.le eb sb x y)) + :pattern ((ae.fp.lt eb sb y x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.le eb sb x y) + (or (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (or (and (is_minus_infinity eb sb x) (is_not_nan eb sb y)) + (and (is_not_nan eb sb x) (is_plus_infinity eb sb y))))) + :pattern ((ae.fp.le eb sb x y))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.lt eb sb x y) + (or (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (or + (and (is_minus_infinity eb sb x) + (and (is_not_nan eb sb y) (not (is_minus_infinity eb sb y)))) + (and (is_not_nan eb sb x) + (and (not (is_plus_infinity eb sb x)) + (is_plus_infinity eb sb y)))))) + :pattern ((ae.fp.lt eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t) (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.lt eb sb x y) + (ae.fp.lt eb sb y z) (ae.fp.is_finite eb sb y)) + :pattern ((ae.fp.lt eb sb x y) (ae.fp.lt eb sb y z))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_positive eb sb x) (<= 0.0 (ae.fp.to_real eb sb x))) + :pattern ((ae.fp.is_positive eb sb x)) + :pattern ((<= 0.0 (ae.fp.to_real eb sb x)))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (< 0.0 (ae.fp.to_real eb sb x)) (ae.fp.is_positive eb sb x)) + :pattern ((ae.fp.is_positive eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_negative eb sb x) (<= (ae.fp.to_real eb sb x) 0.0)) + :pattern ((ae.fp.is_negative eb sb x)) + :pattern ((<= (ae.fp.to_real eb sb x) 0.0))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (< (ae.fp.to_real eb sb x) 0.0) (ae.fp.is_negative eb sb x)) + :pattern ((ae.fp.is_negative eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (not (and (ae.fp.is_positive eb sb x) (ae.fp.is_negative eb sb x)))) + :pattern ((ae.fp.is_positive eb sb x)) :pattern ((ae.fp.is_negative eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (is_not_nan eb sb x) + (or (ae.fp.is_positive eb sb x) (ae.fp.is_negative eb sb x))) + :pattern ((ae.fp.is_finite eb sb x)) :pattern ((ae.fp.is_infinite eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t) (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (diff_sign eb sb x y) (diff_sign eb sb y z)) + (same_sign eb sb x z)) + :pattern ((ae.fp.is_positive eb sb x) (ae.fp.is_negative eb sb y) (ae.fp.is_positive eb sb z)) :pattern ((ae.fp.is_negative eb sb x) (ae.fp.is_positive eb sb y) (ae.fp.is_negative eb sb z))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) + (< (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) 0.0))) + (diff_sign eb sb x y)) + :pattern ((ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) (same_sign eb sb x y))) + (<= 0.0 (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))) + :pattern ((ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y))))) +(define-fun product_sign ((eb Int) (sb Int) (z ae.fp.t) (x ae.fp.t) + (y ae.fp.t)) Bool + (and (=> (same_sign eb sb x y) (ae.fp.is_positive eb sb z)) + (=> (diff_sign eb sb x y) (ae.fp.is_negative eb sb z)))) +(define-fun overflow_value ((eb Int) (sb Int) (m RoundingMode) + (x ae.fp.t)) Bool + (and (=> (= m RNE) (ae.fp.is_infinite eb sb x)) + (=> (= m RNA) (ae.fp.is_infinite eb sb x)) + (=> (= m RTP) + (ite (ae.fp.is_positive eb sb x) (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_finite eb sb x) + (= (ae.fp.to_real eb sb x) (- (ae.fp.max_real eb sb)))))) + (=> (= m RTN) + (ite (ae.fp.is_positive eb sb x) + (and (ae.fp.is_finite eb sb x) + (= (ae.fp.to_real eb sb x) (ae.fp.max_real eb sb))) + (ae.fp.is_infinite eb sb x))) + (=> (= m RTZ) + (ite (ae.fp.is_positive eb sb x) + (and (ae.fp.is_finite eb sb x) + (= (ae.fp.to_real eb sb x) (ae.fp.max_real eb sb))) + (and (ae.fp.is_finite eb sb x) + (= (ae.fp.to_real eb sb x) (- (ae.fp.max_real eb sb)))))))) +(define-fun sign_zero_result ((eb Int) (sb Int) (m RoundingMode) + (x ae.fp.t)) Bool + (=> (ae.fp.is_zero eb sb x) + (and (=> (= m RNE) (ae.fp.is_positive eb sb x)) + (=> (= m RNA) (ae.fp.is_positive eb sb x)) + (=> (= m RTP) (ae.fp.is_positive eb sb x)) + (=> (= m RTN) (ae.fp.is_negative eb sb x)) + (=> (= m RTZ) (ae.fp.is_positive eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) + (no_overflow eb sb m + (+ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + (ae.fp.is_finite eb sb (ae.fp.add eb sb m x y))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) + (no_overflow eb sb m + (+ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + (= (ae.fp.to_real eb sb (ae.fp.add eb sb m x y)) + (ae.float eb sb m + (+ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.add eb sb m x y)) + (ae.fp.is_finite eb sb x)) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.add eb sb m x y)) + (ae.fp.is_finite eb sb y)) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.add eb sb m x y)) + (no_overflow eb sb m + (+ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.add eb sb m x y)) + (= (ae.fp.to_real eb sb (ae.fp.add eb sb m x y)) + (ae.float eb sb m + (+ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) + (no_overflow eb sb m + (- (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + (ae.fp.is_finite eb sb (ae.fp.sub eb sb m x y))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) + (no_overflow eb sb m + (- (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + (= (ae.fp.to_real eb sb (ae.fp.sub eb sb m x y)) + (ae.float eb sb m + (- (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.sub eb sb m x y)) + (ae.fp.is_finite eb sb x)) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.sub eb sb m x y)) + (ae.fp.is_finite eb sb y)) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.sub eb sb m x y)) + (no_overflow eb sb m + (- (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.sub eb sb m x y)) + (= (ae.fp.to_real eb sb (ae.fp.sub eb sb m x y)) + (ae.float eb sb m + (- (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) + (no_overflow eb sb m + (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + (ae.fp.is_finite eb sb (ae.fp.mul eb sb m x y))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) + (no_overflow eb sb m + (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + (= (ae.fp.to_real eb sb (ae.fp.mul eb sb m x y)) + (ae.float eb sb m + (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.mul eb sb m x y)) + (ae.fp.is_finite eb sb x)) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.mul eb sb m x y)) + (ae.fp.is_finite eb sb y)) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.mul eb sb m x y)) + (no_overflow eb sb m + (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.mul eb sb m x y)) + (= (ae.fp.to_real eb sb (ae.fp.mul eb sb m x y)) + (ae.float eb sb m + (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) (not (ae.fp.is_zero eb sb y)) + (no_overflow eb sb m + (/ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + (ae.fp.is_finite eb sb (ae.fp.div eb sb m x y))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) (not (ae.fp.is_zero eb sb y)) + (no_overflow eb sb m + (/ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))) + (= (ae.fp.to_real eb sb (ae.fp.div eb sb m x y)) + (ae.float eb sb m + (/ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.div eb sb m x y)) + (or + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) (not (ae.fp.is_zero eb sb y)))) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_infinite eb sb y) + (= (ae.fp.to_real eb sb (ae.fp.div eb sb m x y)) 0.0))))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.div eb sb m x y)) + (ae.fp.is_finite eb sb y) + (no_overflow eb sb m + (/ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.div eb sb m x y)) + (ae.fp.is_finite eb sb y) + (= (ae.fp.to_real eb sb (ae.fp.div eb sb m x y)) + (ae.float eb sb m + (/ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb (ae.fp.neg eb sb x))) + :pattern ((ae.fp.neg eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (= (ae.fp.to_real eb sb (ae.fp.neg eb sb x)) + (- (ae.fp.to_real eb sb x)))) + :pattern ((ae.fp.neg eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.neg eb sb x)) + (ae.fp.is_finite eb sb x)) + :pattern ((ae.fp.neg eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.neg eb sb x)) + (= (ae.fp.to_real eb sb (ae.fp.neg eb sb x)) + (- (ae.fp.to_real eb sb x)))) + :pattern ((ae.fp.neg eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb (ae.fp.abs eb sb x))) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (= (ae.fp.to_real eb sb (ae.fp.abs eb sb x)) + (ite (>= (ae.fp.to_real eb sb x) 0.0) (ae.fp.to_real eb sb x) + (- (ae.fp.to_real eb sb x))))) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_positive eb sb (ae.fp.abs eb sb x))) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.abs eb sb x)) + (ae.fp.is_finite eb sb x)) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.abs eb sb x)) + (= (ae.fp.to_real eb sb (ae.fp.abs eb sb x)) + (ite (>= (ae.fp.to_real eb sb x) 0.0) (ae.fp.to_real eb sb x) + (- (ae.fp.to_real eb sb x))))) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (not (ae.fp.is_negative eb sb (ae.fp.abs eb sb x)))) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) (ae.fp.is_finite eb sb z) + (no_overflow eb sb m + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z))) + (ae.fp.is_finite eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) (ae.fp.is_finite eb sb z) + (no_overflow eb sb m + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z))) + (= (ae.fp.to_real eb sb (ae.fp.fma eb sb m x y z)) + (ae.float eb sb m + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z))))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.fma eb sb m x y z)) + (ae.fp.is_finite eb sb x)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.fma eb sb m x y z)) + (ae.fp.is_finite eb sb y)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.fma eb sb m x y z)) + (ae.fp.is_finite eb sb z)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.fma eb sb m x y z)) + (no_overflow eb sb m + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z)))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (or (= m RNE) (= m RNA)) + (ae.fp.is_finite eb sb (ae.fp.fma eb sb m x y z)) + (= (ae.fp.to_real eb sb (ae.fp.fma eb sb m x y z)) + (ae.float eb sb m + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z))))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (<= 0.0 (ae.fp.to_real eb sb x)) + (ae.fp.is_finite eb sb (ae.fp.sqrt eb sb m x))) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (<= 0.0 (ae.fp.to_real eb sb x)) + (= (ae.fp.to_real eb sb (ae.fp.sqrt eb sb m x)) + (ae.float eb sb m (sqrt_real (ae.fp.to_real eb sb x))))) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.sqrt eb sb m x)) + (ae.fp.is_finite eb sb x)) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.sqrt eb sb m x)) + (<= 0.0 (ae.fp.to_real eb sb x))) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.is_finite eb sb (ae.fp.sqrt eb sb m x)) + (= (ae.fp.to_real eb sb (ae.fp.sqrt eb sb m x)) + (ae.float eb sb m (sqrt_real (ae.fp.to_real eb sb x))))) + :pattern ((ae.fp.sqrt eb sb m x))))) +(define-fun same_sign_real ((eb Int) (sb Int) (x ae.fp.t) (r Real)) Bool + (or (and (ae.fp.is_positive eb sb x) (< 0.0 r)) + (and (ae.fp.is_negative eb sb x) (< r 0.0)))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (or (ae.fp.is_nan eb sb x) (ae.fp.is_nan eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.add eb sb m x y))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_infinite eb sb y)) + (ae.fp.is_infinite eb sb (ae.fp.add eb sb m x y))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_infinite eb sb y)) + (same_sign eb sb (ae.fp.add eb sb m x y) y)) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_finite eb sb y)) + (ae.fp.is_infinite eb sb (ae.fp.add eb sb m x y))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_finite eb sb y)) + (same_sign eb sb (ae.fp.add eb sb m x y) x)) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (same_sign eb sb x y))) + (ae.fp.is_infinite eb sb (ae.fp.add eb sb m x y))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (same_sign eb sb x y))) + (same_sign eb sb (ae.fp.add eb sb m x y) x)) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (diff_sign eb sb x y))) + (ae.fp.is_nan eb sb (ae.fp.add eb sb m x y))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) + (not + (no_overflow eb sb m + (+ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))))) + (same_sign_real eb sb (ae.fp.add eb sb m x y) + (+ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) + (not + (no_overflow eb sb m + (+ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))))) + (overflow_value eb sb m (ae.fp.add eb sb m x y))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (same_sign eb sb x y) + (same_sign eb sb (ae.fp.add eb sb m x y) x)) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (not (same_sign eb sb x y)) + (sign_zero_result eb sb m (ae.fp.add eb sb m x y))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (or (ae.fp.is_nan eb sb x) (ae.fp.is_nan eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.sub eb sb m x y))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_infinite eb sb y)) + (ae.fp.is_infinite eb sb (ae.fp.sub eb sb m x y))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_infinite eb sb y)) + (diff_sign eb sb (ae.fp.sub eb sb m x y) y)) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_finite eb sb y)) + (ae.fp.is_infinite eb sb (ae.fp.sub eb sb m x y))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_finite eb sb y)) + (same_sign eb sb (ae.fp.sub eb sb m x y) x)) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (same_sign eb sb x y))) + (ae.fp.is_nan eb sb (ae.fp.sub eb sb m x y))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (diff_sign eb sb x y))) + (ae.fp.is_infinite eb sb (ae.fp.sub eb sb m x y))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (diff_sign eb sb x y))) + (same_sign eb sb (ae.fp.sub eb sb m x y) x)) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) + (not + (no_overflow eb sb m + (- (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))))) + (same_sign_real eb sb (ae.fp.sub eb sb m x y) + (- (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) + (not + (no_overflow eb sb m + (- (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))))) + (overflow_value eb sb m (ae.fp.sub eb sb m x y))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (diff_sign eb sb x y) + (same_sign eb sb (ae.fp.sub eb sb m x y) x)) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_finite eb sb y)) + (not (diff_sign eb sb x y)) + (sign_zero_result eb sb m (ae.fp.sub eb sb m x y))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (or (ae.fp.is_nan eb sb x) (ae.fp.is_nan eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.mul eb sb m x y))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_zero eb sb x) (ae.fp.is_infinite eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.mul eb sb m x y))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_infinite eb sb y) (not (ae.fp.is_zero eb sb x)))) + (ae.fp.is_infinite eb sb (ae.fp.mul eb sb m x y))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_zero eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.mul eb sb m x y))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_finite eb sb y) (not (ae.fp.is_zero eb sb y)))) + (ae.fp.is_infinite eb sb (ae.fp.mul eb sb m x y))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_infinite eb sb y)) + (ae.fp.is_infinite eb sb (ae.fp.mul eb sb m x y))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) + (not + (no_overflow eb sb m + (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)))))) + (overflow_value eb sb m (ae.fp.mul eb sb m x y))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (let ((r (ae.fp.mul eb sb m x y))) + (=> (not (ae.fp.is_nan eb sb r)) (product_sign eb sb r x y)))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (or (ae.fp.is_nan eb sb x) (ae.fp.is_nan eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.div eb sb m x y))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (ae.fp.is_infinite eb sb y)) + (ae.fp.is_zero eb sb (ae.fp.div eb sb m x y))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_finite eb sb y)) + (ae.fp.is_infinite eb sb (ae.fp.div eb sb m x y))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_infinite eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.div eb sb m x y))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) + (and (not (ae.fp.is_zero eb sb y)) + (not + (no_overflow eb sb m + (/ (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y))))))) + (overflow_value eb sb m (ae.fp.div eb sb m x y))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_zero eb sb y) (not (ae.fp.is_zero eb sb x)))) + (ae.fp.is_infinite eb sb (ae.fp.div eb sb m x y))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_zero eb sb x) (ae.fp.is_zero eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.div eb sb m x y))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (let ((r (ae.fp.div eb sb m x y))) + (=> (not (ae.fp.is_nan eb sb r)) (product_sign eb sb r x y)))) + :pattern ((ae.fp.div eb sb m x y))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_nan eb sb x) + (ae.fp.is_nan eb sb (ae.fp.neg eb sb x))) + :pattern ((ae.fp.neg eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_infinite eb sb x) + (ae.fp.is_infinite eb sb (ae.fp.neg eb sb x))) + :pattern ((ae.fp.neg eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (not (ae.fp.is_nan eb sb x)) + (diff_sign eb sb x (ae.fp.neg eb sb x))) + :pattern ((ae.fp.neg eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_nan eb sb x) + (ae.fp.is_nan eb sb (ae.fp.abs eb sb x))) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_infinite eb sb x) + (ae.fp.is_infinite eb sb (ae.fp.abs eb sb x))) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (not (ae.fp.is_nan eb sb x)) + (ae.fp.is_positive eb sb (ae.fp.abs eb sb x))) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (or (ae.fp.is_nan eb sb x) + (or (ae.fp.is_nan eb sb y) (ae.fp.is_nan eb sb z))) + (ae.fp.is_nan eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_zero eb sb x) (ae.fp.is_infinite eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) (ae.fp.is_zero eb sb y)) + (ae.fp.is_nan eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (not (ae.fp.is_zero eb sb x)) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_finite eb sb z)))) + (ae.fp.is_infinite eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (not (ae.fp.is_zero eb sb x)) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_finite eb sb z)))) + (product_sign eb sb (ae.fp.fma eb sb m x y z) x y)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (not (ae.fp.is_zero eb sb x)) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_infinite eb sb z)))) + (product_sign eb sb z x y) + (ae.fp.is_infinite eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (not (ae.fp.is_zero eb sb x)) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_infinite eb sb z)))) + (product_sign eb sb z x y) + (same_sign eb sb (ae.fp.fma eb sb m x y z) z)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (not (ae.fp.is_zero eb sb x)) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_infinite eb sb z)))) + (not (product_sign eb sb z x y)) + (ae.fp.is_nan eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_finite eb sb y) + (and (not (ae.fp.is_zero eb sb y)) (ae.fp.is_finite eb sb z)))) + (ae.fp.is_infinite eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_finite eb sb y) + (and (not (ae.fp.is_zero eb sb y)) (ae.fp.is_finite eb sb z)))) + (product_sign eb sb (ae.fp.fma eb sb m x y z) x y)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_finite eb sb y) + (and (not (ae.fp.is_zero eb sb y)) + (ae.fp.is_infinite eb sb z)))) (product_sign eb sb z x y) + (ae.fp.is_infinite eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_finite eb sb y) + (and (not (ae.fp.is_zero eb sb y)) + (ae.fp.is_infinite eb sb z)))) (product_sign eb sb z x y) + (same_sign eb sb (ae.fp.fma eb sb m x y z) z)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_finite eb sb y) + (and (not (ae.fp.is_zero eb sb y)) + (ae.fp.is_infinite eb sb z)))) + (not (product_sign eb sb z x y)) + (ae.fp.is_nan eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_finite eb sb z))) + (ae.fp.is_infinite eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_finite eb sb z))) + (product_sign eb sb (ae.fp.fma eb sb m x y z) x y)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) (ae.fp.is_infinite eb sb z))) + (ae.fp.is_infinite eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) (ae.fp.is_infinite eb sb z))) + (same_sign eb sb (ae.fp.fma eb sb m x y z) z)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_infinite eb sb z))) + (product_sign eb sb z x y) + (ae.fp.is_infinite eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_infinite eb sb z))) + (product_sign eb sb z x y) + (same_sign eb sb (ae.fp.fma eb sb m x y z) z)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_infinite eb sb x) + (and (ae.fp.is_infinite eb sb y) (ae.fp.is_infinite eb sb z))) + (not (product_sign eb sb z x y)) + (ae.fp.is_nan eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) + (and (ae.fp.is_finite eb sb z) + (not + (no_overflow eb sb m + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z))))))) + (same_sign_real eb sb (ae.fp.fma eb sb m x y z) + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z)))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) + (and (ae.fp.is_finite eb sb z) + (not + (no_overflow eb sb m + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z))))))) + (overflow_value eb sb m (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) (ae.fp.is_finite eb sb z))) + (product_sign eb sb z x y) + (same_sign eb sb (ae.fp.fma eb sb m x y z) z)) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) (ae.fp.is_finite eb sb z))) + (not (product_sign eb sb z x y)) + (= + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z)) 0.0) (= m RTN) + (ae.fp.is_negative eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t) + (y ae.fp.t) + (z ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) + (and (ae.fp.is_finite eb sb y) (ae.fp.is_finite eb sb z))) + (not (product_sign eb sb z x y)) + (= + (+ (* (ae.fp.to_real eb sb x) (ae.fp.to_real eb sb y)) + (ae.fp.to_real eb sb z)) 0.0) (not (= m RTN)) + (ae.fp.is_positive eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_nan eb sb x) + (ae.fp.is_nan eb sb (ae.fp.sqrt eb sb m x))) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (is_plus_infinity eb sb x) + (is_plus_infinity eb sb (ae.fp.sqrt eb sb m x))) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (is_minus_infinity eb sb x) + (ae.fp.is_nan eb sb (ae.fp.sqrt eb sb m x))) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (< (ae.fp.to_real eb sb x) 0.0)) + (ae.fp.is_nan eb sb (ae.fp.sqrt eb sb m x))) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_zero eb sb x) + (same_sign eb sb (ae.fp.sqrt eb sb m x) x)) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.is_finite eb sb x) (< 0.0 (ae.fp.to_real eb sb x))) + (ae.fp.is_positive eb sb (ae.fp.sqrt eb sb m x))) + :pattern ((ae.fp.sqrt eb sb m x))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (n RoundingMode) (i Int) + (j Int)) + (! (=> (and (< 1 eb) (< 1 sb)) (in_safe_int_range eb sb i) + (in_safe_int_range eb sb j) (in_safe_int_range eb sb (+ i j)) + (ae.fp.eq eb sb (ae.fp.of_int eb sb m (+ i j)) + (ae.fp.add eb sb n (ae.fp.of_int eb sb m i) + (ae.fp.of_int eb sb m j)))) + :pattern ((ae.fp.add eb sb n (ae.fp.of_int eb sb m i) (ae.fp.of_int eb sb m j)))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (n RoundingMode) (i Int) + (j Int)) + (! (=> (and (< 1 eb) (< 1 sb)) (in_safe_int_range eb sb i) + (in_safe_int_range eb sb j) (in_safe_int_range eb sb (- i j)) + (ae.fp.eq eb sb (ae.fp.of_int eb sb m (- i j)) + (ae.fp.sub eb sb n (ae.fp.of_int eb sb m i) + (ae.fp.of_int eb sb m j)))) + :pattern ((ae.fp.sub eb sb n (ae.fp.of_int eb sb m i) (ae.fp.of_int eb sb m j)))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (n RoundingMode) (i Int) + (j Int)) + (! (=> (and (< 1 eb) (< 1 sb)) (in_safe_int_range eb sb i) + (in_safe_int_range eb sb j) (in_safe_int_range eb sb (* i j)) + (ae.fp.eq eb sb (ae.fp.of_int eb sb m (* i j)) + (ae.fp.mul eb sb n (ae.fp.of_int eb sb m i) + (ae.fp.of_int eb sb m j)))) + :pattern ((ae.fp.mul eb sb n (ae.fp.of_int eb sb m i) (ae.fp.of_int eb sb m j)))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.le eb sb y x) + (ae.fp.eq eb sb (ae.fp.min eb sb x y) y)) + :pattern ((ae.fp.min eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.le eb sb x y) + (ae.fp.eq eb sb (ae.fp.min eb sb x y) x)) + :pattern ((ae.fp.min eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.le eb sb y x) + (ae.fp.eq eb sb (ae.fp.max eb sb x y) x)) + :pattern ((ae.fp.max eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.le eb sb x y) + (ae.fp.eq eb sb (ae.fp.max eb sb x y) y)) + :pattern ((ae.fp.max eb sb x y))))) +(declare-fun ae.fp.is_int (Int Int ae.fp.t) Bool) +(assert (forall ((eb Int) (sb Int)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb (ae.fp.zero eb sb))) + :pattern ((ae.fp.zero eb sb))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x Int)) + (! (=> (and (< 1 eb) (< 1 sb)) (in_int_range eb sb x) + (ae.fp.is_int eb sb (ae.fp.of_int eb sb m x))) + :pattern ((ae.fp.of_int eb sb m x))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (i ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb i) + (or + (ae.fp.le eb sb i + (ae.fp.neg eb sb (ae.fp.of_int eb sb m (ae.fp.pow2sb eb sb)))) + (ae.fp.le eb sb (ae.fp.of_int eb sb m (ae.fp.pow2sb eb sb)) i)) + (ae.fp.is_int eb sb i)) + :pattern ((ae.fp.is_finite eb sb i) (ae.fp.of_int eb sb m (ae.fp.pow2sb eb sb)))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_int eb sb (ae.fp.roundToIntegral eb sb m x))) + :pattern ((ae.fp.roundToIntegral eb sb m x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.eq eb sb x y) + (ae.fp.is_int eb sb x) (ae.fp.is_int eb sb y)) + :pattern ((ae.fp.eq eb sb x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t) (m RoundingMode)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (ae.fp.is_int eb sb y) + (ae.fp.is_finite eb sb (ae.fp.add eb sb m x y)) + (ae.fp.is_int eb sb (ae.fp.add eb sb m x y))) + :pattern ((ae.fp.add eb sb m x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t) (m RoundingMode)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (ae.fp.is_int eb sb y) + (ae.fp.is_finite eb sb (ae.fp.sub eb sb m x y)) + (ae.fp.is_int eb sb (ae.fp.sub eb sb m x y))) + :pattern ((ae.fp.sub eb sb m x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t) (m RoundingMode)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (ae.fp.is_int eb sb y) + (ae.fp.is_finite eb sb (ae.fp.mul eb sb m x y)) + (ae.fp.is_int eb sb (ae.fp.mul eb sb m x y))) + :pattern ((ae.fp.mul eb sb m x y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t) (z ae.fp.t) + (m RoundingMode)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (ae.fp.is_int eb sb y) (ae.fp.is_int eb sb z) + (ae.fp.is_finite eb sb (ae.fp.fma eb sb m x y z)) + (ae.fp.is_int eb sb (ae.fp.fma eb sb m x y z))) + :pattern ((ae.fp.fma eb sb m x y z))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (ae.fp.is_int eb sb (ae.fp.neg eb sb x))) + :pattern ((ae.fp.neg eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (ae.fp.is_int eb sb (ae.fp.abs eb sb x))) + :pattern ((ae.fp.abs eb sb x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (m RoundingMode) + (mqt RoundingMode)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (ae.fp.eq eb sb x + (ae.fp.of_int eb sb mqt (ae.fp.to_int eb sb m x)))) + :pattern ((ae.fp.of_int eb sb mqt (ae.fp.to_int eb sb m x)))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (in_int_range eb sb (ae.fp.to_int eb sb m x))) + :pattern ((ae.fp.to_int eb sb m x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (ae.fp.is_finite eb sb x)) + :pattern ((ae.fp.is_int eb sb x))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (= (ae.fp.to_real eb sb x) (to_real (ae.fp.to_int eb sb m x)))) + :pattern ((ae.fp.to_int eb sb m x))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (i ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb i) + (ae.fp.eq eb sb (ae.fp.roundToIntegral eb sb m i) i)) + :pattern ((ae.fp.roundToIntegral eb sb m i))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_negative eb sb x) + (= (ae.fp.roundToIntegral eb sb RTZ x) + (ae.fp.roundToIntegral eb sb RTP x))) + :pattern ((ae.fp.roundToIntegral eb sb RTZ x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_positive eb sb x) + (= (ae.fp.roundToIntegral eb sb RTZ x) + (ae.fp.roundToIntegral eb sb RTN x))) + :pattern ((ae.fp.roundToIntegral eb sb RTZ x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.le eb sb x (ae.fp.roundToIntegral eb sb RTP x))) + :pattern ((ae.fp.roundToIntegral eb sb RTP x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.le eb sb x y) (ae.fp.is_int eb sb y)) + (ae.fp.le eb sb (ae.fp.roundToIntegral eb sb RTP x) y)) + :pattern ((ae.fp.roundToIntegral eb sb RTP x) (ae.fp.is_int eb sb y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (= (ae.fp.to_real eb sb (ae.fp.roundToIntegral eb sb RTP x)) + (to_real (- (to_int (- (ae.fp.to_real eb sb x))))))) + :pattern ((ae.fp.roundToIntegral eb sb RTP x))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (= (ae.fp.to_int eb sb m (ae.fp.roundToIntegral eb sb RTP x)) + (- (to_int (- (ae.fp.to_real eb sb x)))))) + :pattern ((ae.fp.to_int eb sb m (ae.fp.roundToIntegral eb sb RTP x)))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.le eb sb (ae.fp.roundToIntegral eb sb RTN x) x)) + :pattern ((ae.fp.roundToIntegral eb sb RTN x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (and (ae.fp.le eb sb y x) (ae.fp.is_int eb sb y)) + (ae.fp.le eb sb y (ae.fp.roundToIntegral eb sb RTN x))) + :pattern ((ae.fp.roundToIntegral eb sb RTN x) (ae.fp.is_int eb sb y))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (= (ae.fp.to_real eb sb (ae.fp.roundToIntegral eb sb RTN x)) + (to_real (to_int (ae.fp.to_real eb sb x))))) + :pattern ((ae.fp.roundToIntegral eb sb RTN x))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (= (ae.fp.to_int eb sb m (ae.fp.roundToIntegral eb sb RTN x)) + (to_int (ae.fp.to_real eb sb x)))) + :pattern ((ae.fp.to_int eb sb m (ae.fp.roundToIntegral eb sb RTN x)))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.lt eb sb + (ae.fp.sub eb sb RNE x (ae.fp.roundToIntegral eb sb RTN x)) + (ae.fp.sub eb sb RNE (ae.fp.roundToIntegral eb sb RTP x) x)) + (= (ae.fp.roundToIntegral eb sb RNA x) + (ae.fp.roundToIntegral eb sb RTN x))) + :pattern ((ae.fp.roundToIntegral eb sb RNA x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.lt eb sb + (ae.fp.sub eb sb RNE (ae.fp.roundToIntegral eb sb RTP x) x) + (ae.fp.sub eb sb RNE x (ae.fp.roundToIntegral eb sb RTN x))) + (= (ae.fp.roundToIntegral eb sb RNA x) + (ae.fp.roundToIntegral eb sb RTP x))) + :pattern ((ae.fp.roundToIntegral eb sb RNA x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.eq eb sb + (ae.fp.sub eb sb RNE x (ae.fp.roundToIntegral eb sb RTN x)) + (ae.fp.sub eb sb RNE (ae.fp.roundToIntegral eb sb RTP x) x)) + (ae.fp.is_negative eb sb x) + (= (ae.fp.roundToIntegral eb sb RNA x) + (ae.fp.roundToIntegral eb sb RTN x))) + :pattern ((ae.fp.roundToIntegral eb sb RNA x))))) +(assert (forall ((eb Int) (sb Int) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (ae.fp.eq eb sb + (ae.fp.sub eb sb RNE (ae.fp.roundToIntegral eb sb RTP x) x) + (ae.fp.sub eb sb RNE x (ae.fp.roundToIntegral eb sb RTN x))) + (ae.fp.is_positive eb sb x) + (= (ae.fp.roundToIntegral eb sb RNA x) + (ae.fp.roundToIntegral eb sb RTP x))) + :pattern ((ae.fp.roundToIntegral eb sb RNA x))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) + (= (ae.fp.to_int eb sb m x) + (ae.fp.to_int eb sb m (ae.fp.roundToIntegral eb sb m x)))) + :pattern ((ae.fp.roundToIntegral eb sb m x))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb y) (ae.fp.le eb sb x y) + (<= (ae.fp.to_int eb sb m x) (ae.fp.to_int eb sb m y))) + :pattern ((ae.fp.to_int eb sb m x) (ae.fp.to_int eb sb m y))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (i Int)) + (! (=> (and (< 1 eb) (< 1 sb)) (in_safe_int_range eb sb i) + (= (ae.fp.to_int eb sb m (ae.fp.of_int eb sb m i)) i)) + :pattern ((ae.fp.to_int eb sb m (ae.fp.of_int eb sb m i)))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t) (y ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.eq eb sb x y) + (= (ae.fp.to_int eb sb m x) (ae.fp.to_int eb sb m y))) + :pattern ((ae.fp.to_int eb sb m x) (ae.fp.to_int eb sb m y))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_int eb sb x) + (= (ae.fp.to_int eb sb m (ae.fp.neg eb sb x)) + (- (ae.fp.to_int eb sb m x)))) + :pattern ((ae.fp.to_int eb sb m (ae.fp.neg eb sb x)))))) +(assert (forall ((eb Int) (sb Int) (m RoundingMode) (x ae.fp.t)) + (! (=> (and (< 1 eb) (< 1 sb)) (ae.fp.is_finite eb sb x) + (ae.fp.is_finite eb sb (ae.fp.roundToIntegral eb sb m x))) + :pattern ((ae.fp.roundToIntegral eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (x Real)) + (! (=> (and (< 1 eb) (< 1 sb)) (no_overflow eb sb RNE x) + (<= + (- x + (* (/ 1.0 (ae.fp.pow2sb_real eb sb)) (ite (>= x 0.0) x (- x))) + (/ 1.0 (ae.fp.abs_err_rne_denom eb sb))) + (ae.float eb sb RNE x))) + :pattern ((ae.float eb sb RNE x))))) +(assert (forall ((eb Int) + (sb Int) + (x Real)) + (! (=> (and (< 1 eb) (< 1 sb)) (no_overflow eb sb RNE x) + (<= (ae.float eb sb RNE x) + (+ x + (* (/ 1.0 (ae.fp.pow2sb_real eb sb)) (ite (>= x 0.0) x (- x))) + (/ 1.0 (ae.fp.abs_err_rne_denom eb sb))))) + :pattern ((ae.float eb sb RNE x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x Real)) + (! (=> (and (< 1 eb) (< 1 sb)) (no_overflow eb sb m x) + (<= + (- x + (* (/ 1.0 (ae.fp.half_pow2sb_real eb sb)) + (ite (>= x 0.0) x (- x))) + (/ 1.0 (ae.fp.abs_err_denom eb sb))) (ae.float eb sb m x))) + :pattern ((ae.float eb sb m x))))) +(assert (forall ((eb Int) + (sb Int) + (m RoundingMode) + (x Real)) + (! (=> (and (< 1 eb) (< 1 sb)) (no_overflow eb sb m x) + (<= (ae.float eb sb m x) + (+ x + (* (/ 1.0 (ae.fp.half_pow2sb_real eb sb)) + (ite (>= x 0.0) x (- x))) + (/ 1.0 (ae.fp.abs_err_denom eb sb))))) + :pattern ((ae.float eb sb m x))))) diff --git a/tests/cram.t/fp_literals.smt2 b/tests/cram.t/fp_literals.smt2 deleted file mode 100644 index 575f6c1f0d..0000000000 --- a/tests/cram.t/fp_literals.smt2 +++ /dev/null @@ -1,45 +0,0 @@ -(set-logic QF_FP) - -(push 1) -(assert (not (or - (= (_ +oo 8 24) (fp #b0 #b11111111 #b00000000000000000000000)) - (= (_ +oo 8 24) ((_ to_fp 8 24) #b01111111100000000000000000000000)) -))) -(check-sat) -(pop 1) - -(push 1) -(assert (not (or - (= (_ -oo 8 24) (fp #b1 #b11111111 #b00000000000000000000000)) - (= (_ -oo 8 24) ((_ to_fp 8 24) #b11111111100000000000000000000000)) -))) -(check-sat) -(pop 1) - -(push 1) -(assert (not (or - (= (_ +zero 8 24) (fp #b0 #b00000000 #b00000000000000000000000)) - (= (_ +zero 8 24) ((_ to_fp 8 24) #b00000000000000000000000000000000)) -))) -(check-sat) -(pop 1) - -(push 1) -(assert (not (or - (= (_ -zero 8 24) (fp #b1 #b00000000 #b00000000000000000000000)) - (= (_ -zero 8 24) ((_ to_fp 8 24) #b10000000000000000000000000000000)) -))) -(check-sat) -(pop 1) - -(push 1) -(assert (not (= (_ NaN 8 24) (_ NaN 8 24)))) -(check-sat) -(pop 1) - -(push 1) -(assert (not (= (fp #b0 #b01111111 #b00000000000000000000000) - ((_ to_fp 8 24) #b00111111100000000000000000000000)))) -(check-sat) -(pop 1) - diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 6d05a397c4..88f320b78b 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -142,20 +142,3 @@ Tableaux solver. unknown (error ":1.62: the selected solver does not support optimization") -Testing Alt-Ergo's support for parsing smt-lib FPA literals, this test ought to -be moved to ./tests/float when we have a proper support for enabling and -disabling theories in smt-lib files with `set-option` - $ alt-ergo -o smtlib2 --enable-theory smt.float fp_literals.smt2 2>/dev/null - - unsat - - unsat - - unsat - - unsat - - unsat - - unsat - diff --git a/tests/float/smt-lib-fpa/run.t b/tests/float/smt-lib-fpa/run.t new file mode 100644 index 0000000000..0891d2a167 --- /dev/null +++ b/tests/float/smt-lib-fpa/run.t @@ -0,0 +1,145 @@ +Testing Alt-Ergo's support for parsing smt-lib FPA literals. + + $ alt-ergo -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (assert (not (or + > (= (_ +oo 8 24) (fp #b0 #b11111111 #b00000000000000000000000)) + > (= (_ +oo 8 24) ((_ to_fp 8 24) #b01111111100000000000000000000000)) + > ))) + > (check-sat) + > EOF + + unsat + + $ alt-ergo -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (assert (not (or + > (= (_ -oo 8 24) (fp #b1 #b11111111 #b00000000000000000000000)) + > (= (_ -oo 8 24) ((_ to_fp 8 24) #b11111111100000000000000000000000)) + > ))) + > (check-sat) + > EOF + + unsat + + $ alt-ergo -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (assert (not (or + > (= (_ +zero 8 24) (fp #b0 #b00000000 #b00000000000000000000000)) + > (= (_ +zero 8 24) ((_ to_fp 8 24) #b00000000000000000000000000000000)) + > ))) + > (check-sat) + > EOF + + unsat + $ alt-ergo -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (assert (not (or + > (= (_ -zero 8 24) (fp #b1 #b00000000 #b00000000000000000000000)) + > (= (_ -zero 8 24) ((_ to_fp 8 24) #b10000000000000000000000000000000)) + > ))) + > (check-sat) + > EOF + + unsat + $ alt-ergo -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (assert (not (= (_ NaN 8 24) (_ NaN 8 24)))) + > (check-sat) + > EOF + + unsat + $ alt-ergo -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (assert (not (= (fp #b0 #b01111111 #b00000000000000000000000) + > ((_ to_fp 8 24) #b00111111100000000000000000000000)))) + > (check-sat) + > EOF + + unsat + +Testing Alt-Ergo's symbolic reasoning over smt-lib FPA symbols. + $ alt-ergo -t 1 -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (declare-const x (_ FloatingPoint 8 24)) + > (assert (fp.isPositive x)) + > (assert (fp.isNegative x)) + > (check-sat) + > EOF + + unsat + + $ alt-ergo -t 1 -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (declare-const x (_ FloatingPoint 8 24)) + > (assert (fp.isNegative (fp.abs x))) + > (check-sat) + > EOF + + unsat + + $ alt-ergo -t 1 -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (declare-const x (_ FloatingPoint 8 24)) + > (declare-const y (_ FloatingPoint 8 24)) + > (assert (fp.isZero x)) + > (assert (fp.isZero y)) + > (assert (fp.isInfinite (fp.add roundNearestTiesToEven x y))) + > (check-sat) + > EOF + + unsat + + $ alt-ergo -t 1 -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (declare-const x (_ FloatingPoint 8 24)) + > (declare-const y (_ FloatingPoint 8 24)) + > (assert (fp.isZero x)) + > (assert (fp.isZero y)) + > (assert (fp.lt x y)) + > (assert (fp.leq y x)) + > (check-sat) + > EOF + + unsat + + $ alt-ergo -t 1 -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic QF_FP) + > (declare-const x (_ FloatingPoint 8 24)) + > (declare-const y (_ FloatingPoint 8 24)) + > (declare-const z (_ FloatingPoint 8 24)) + > (assert (fp.isZero x)) + > (assert (fp.isZero y)) + > (assert (fp.isZero z)) + > (assert (fp.lt (fp.fma roundNearestTiesToEven x y z) z)) + > (check-sat) + > EOF + + unsat + + $ alt-ergo -t 1 -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic ALL) + > (assert (not (= + > (_ +oo 11 53) + > (fp.fma roundNearestTiesToEven + > (fp (_ bv1 1) (_ bv1 11) (_ bv0 52)) + > (fp (_ bv1 1) (_ bv2047 11) (_ bv0 52)) + > (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)) + > ) + > ))) + > (check-sat) + > EOF + + unsat + + $ alt-ergo -t 1 -o smtlib2 --enable-theory smt.float 2>/dev/null < (set-logic ALL) + > (declare-fun x () Float64) + > (declare-fun y () Float64) + > (assert (= x (fp (_ bv0 1) #b10011100010 (_ bv0 52)))) + > (assert (= y (fp (_ bv1 1) #b11111000100 (_ bv0 52)))) + > (assert (not (= (_ -oo 11 53) (fp.mul roundNearestTiesToEven x y)))) + > (check-sat) + > EOF + + unsat