From 89060b83a9971afe1cb1f970681f8d0ca4bf1b1a Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 12 Nov 2024 10:56:59 +0100 Subject: [PATCH] Remove deprecated cli options and preludes (#1265) * Remove deprecated options and preludes These features have been deprecated in v2.6.0. --- src/bin/common/parse_command.ml | 104 +- src/bin/js/options_interface.ml | 1 - src/bin/js/worker_interface.ml | 12 +- src/bin/js/worker_interface.mli | 1 - src/lib/structures/expr.ml | 3 +- src/lib/util/options.ml | 6 - src/lib/util/options.mli | 15 - src/lib/util/printer.ml | 8 +- src/lib/util/printer.mli | 2 - src/preludes/cram.t/run.t | 3 - src/preludes/dune | 20 - src/preludes/fpa-theory-2017-01-04-16h00.ae | 1027 ------------------ src/preludes/fpa-theory-2019-06-14-11h00.ae | 1050 ------------------- src/preludes/fpa-theory-2019-10-08-19h00.ae | 1038 ------------------ 14 files changed, 19 insertions(+), 3271 deletions(-) delete mode 100644 src/preludes/cram.t/run.t delete mode 100644 src/preludes/dune delete mode 100644 src/preludes/fpa-theory-2017-01-04-16h00.ae delete mode 100644 src/preludes/fpa-theory-2019-06-14-11h00.ae delete mode 100644 src/preludes/fpa-theory-2019-10-08-19h00.ae diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index a71fd83297..1205979221 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -149,7 +149,6 @@ module Debug = struct | Arith | Arrays | Bitv - | Sum | Ite | Cc | Combine @@ -165,20 +164,18 @@ module Debug = struct | Split | Triggers | Types - | Typing | Uf | Unsat_core | Use - | Warnings | Commands | Optimize [@@deriving eq] let all = [ - Debug; Ac; Adt; Arith; Arrays; Bitv; Sum; Ite; + Debug; Ac; Adt; Arith; Arrays; Bitv; Ite; Cc; Combine; Constr; Explanations; Fm; Fpa; Gc; Interpretation; Intervals; Matching; Sat; Split; Triggers; - Types; Typing; Uf; Unsat_core; Use; Warnings; + Types; Uf; Unsat_core; Use; Commands; Optimize ] @@ -189,7 +186,6 @@ module Debug = struct | Arith -> "arith" | Arrays -> "arrays" | Bitv -> "bitv" - | Sum -> "sum" | Ite -> "ite" | Cc -> "cc" | Combine -> "combine" @@ -205,11 +201,9 @@ module Debug = struct | Split -> "split" | Triggers -> "triggers" | Types -> "types" - | Typing -> "typing" | Uf -> "uf" | Unsat_core -> "unsat-core" | Use -> "use" - | Warnings -> "warnings" | Commands -> "commands" | Optimize -> "optimize" @@ -238,14 +232,6 @@ module Debug = struct | Bitv -> Options.set_debug_bitv true; set_level Bitv.src - | Sum -> - Printer.print_wrn - "The debug flag 'sum' is deprecated and is replaced by 'adt'. \ - It has the same effect as 'adt' and will be removed in a future \ - version."; - Options.set_debug_adt true; - set_level Adt.src; - set_level Adt_rel.src | Ite -> Options.set_debug_ite true; set_level Ite_rel.src @@ -290,10 +276,6 @@ module Debug = struct | Types -> Options.set_debug_types true; set_level S.types - | Typing -> - Printer.print_wrn - "The debug flag 'typing' has no effect. It will be removed in a \ - future version." | Uf -> Options.set_debug_uf true; set_level Uf.src @@ -303,11 +285,6 @@ module Debug = struct | Use -> Options.set_debug_use true; set_level Use.src - | Warnings -> - Printer.print_wrn - "The debug flag 'warning' is deprecated and will be removed in a \ - future version."; - Options.set_debug_warnings true | Commands -> Options.set_debug_commands true; set_level Commands.src @@ -442,7 +419,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation `Ok() let mk_output_opt - interpretation use_underscore objectives_in_interpretation unsat_core + interpretation objectives_in_interpretation unsat_core output_format model_type () () () () = set_infer_output_format (Option.is_none output_format); @@ -455,7 +432,6 @@ let mk_output_opt | Some v -> v in set_interpretation interpretation; - set_interpretation_use_underscore use_underscore; set_objectives_in_interpretation objectives_in_interpretation; set_unsat_core unsat_core; set_output_format output_format; @@ -529,7 +505,7 @@ let mk_term_opt disable_ites inline_lets rewriting no_term_like_pp let mk_theory_opt () no_contracongru no_fm no_nla no_tcp no_theory restricted tighten_vars - _use_fpa (theories) + (theories) = set_no_ac (not (List.exists (Theories.equal Theories.AC) theories)); set_no_fm no_fm; @@ -750,25 +726,10 @@ let parse_execution_opt = else match Config.lookup_prelude p with | Some p' -> - begin if Compat.String.starts_with ~prefix:"b-set-theory" p then - Printer.print_wrn ~header:true - "Support for the B set theory is deprecated since version \ - 2.5.0 and may be removed in a future version. If you are \ - actively using it, please make yourself known to the Alt-Ergo \ - developers by writing to ." - else if Compat.String.starts_with ~prefix:"fpa-theory" p then - Printer.print_wrn ~header:true - "@[Support for the FPA theory has been integrated as a \ - builtin theory prelude in version 2.5.0 and is enabled \ - by default.\ - This option and the '%s'@ prelude will \ be removed in a \ - later version.@]" p - end; - Ok p' | None -> Error ( - Format.asprintf + Fmt.str "cannot load prelude '%s': no such file" p) in @@ -1121,17 +1082,6 @@ let parse_output_opt = Term.term_result' term in - let use_underscore = - let doc = "Output \"_\" instead of fresh value in interpretation" in - let deprecated = - "this option will be removed as it does not produce a \ - SMTLIB-compliant output." - in - let docv = "VAL" in - Arg.(value & flag & info - ["interpretation-use-underscore";"use-underscore"] - ~docv ~docs:s_models ~doc ~deprecated) - in let objectives_in_interpretation = let doc = " inline pretty-printing of optimized expressions in the \ model instead of a dedicated section '(objectives \ @@ -1190,7 +1140,7 @@ let parse_output_opt = in Term.(ret (const mk_output_opt $ - interpretation $ use_underscore $ + interpretation $ objectives_in_interpretation $ unsat_core $ output_format $ model_type $ set_dump_models $ set_dump_models_on $ @@ -1444,12 +1394,6 @@ let parse_theory_opt = let doc = "Compute the best bounds for arithmetic variables." in Arg.(value & flag & info ["tighten-vars"] ~docs ~doc) in - let use_fpa = - let doc = "Floating-point builtins are always enabled and this option has - no effect anymore. It will be removed in a future version." in - let deprecated = "this option is always enabled" in - Arg.(value & flag & info ["use-fpa"] ~docs ~doc ~deprecated) in - let theories = let theory_enum = Theories.all @@ -1476,34 +1420,12 @@ let parse_theory_opt = (Arg.doc_alts_enum theory_enum) in let docv = "THEORY" in - let disable_theories = - Term.(const List.concat $ - Arg.( - value - & opt_all (list theory) [] - & info ["disable-theory"; "disable-theories"] ~docs ~doc ~docv - )) - in - let disable_adts = - let doc = "Disable Algebraic Datatypes theory. Deprecated alias for - `--disable-theories adt`." in - let deprecated = "use `--disable-theories ac` instead." in - Arg.(value & flag & info ["disable-adts"] ~docs ~doc ~deprecated) - in - let no_ac = - let doc = "Disable the AC theory of Associative and \ - Commutative function symbols. Deprecated alias for - `--disable-theories ac`." in - let deprecated = "use `--disable-theories ac` instead" in - Arg.(value & flag & info ["no-ac"] ~docs ~doc ~deprecated) - in - let mk_disable_theories disable_theories disable_adts no_ac = - let open Theories in - (if disable_adts then [ ADT ] else []) @ - (if no_ac then [ AC ] else []) @ - disable_theories - in - Term.(const mk_disable_theories $ disable_theories $ disable_adts $ no_ac) + Term.(const List.concat $ + Arg.( + value + & opt_all (list theory) [] + & info ["disable-theory"; "disable-theories"] ~docs ~doc ~docv + )) in let preludes enable_theories disable_theories = let theories = Theories.Set.of_list Theories.default in @@ -1535,7 +1457,7 @@ let parse_theory_opt = Term.(ret (const mk_theory_opt $ inequalities_plugin $ no_contracongru $ no_fm $ no_nla $ no_tcp $ no_theory $ restricted $ - tighten_vars $ use_fpa $ theories + tighten_vars $ theories ) ) diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml index 464e9c7a29..57479b2bbb 100644 --- a/src/bin/js/options_interface.ml +++ b/src/bin/js/options_interface.ml @@ -113,7 +113,6 @@ let set_options r = set_options_opt Options.set_debug_uf r.debug_uf; set_options_opt Options.set_debug_unsat_core r.debug_unsat_core; set_options_opt Options.set_debug_use r.debug_use; - set_options_opt Options.set_debug_warnings r.debug_warnings; set_options_opt Options.set_rule r.rule; set_options_opt Options.set_case_split_policy diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml index 21870d25e2..907151e449 100644 --- a/src/bin/js/worker_interface.ml +++ b/src/bin/js/worker_interface.ml @@ -181,7 +181,6 @@ type options = { debug_uf : bool option; debug_unsat_core : bool option; debug_use : bool option; - debug_warnings : bool option; rule : int option; case_split_policy : case_split_policy option; @@ -281,7 +280,6 @@ let init_options () = { debug_uf = None; debug_unsat_core = None; debug_use = None; - debug_warnings = None; rule = None; case_split_policy = None; @@ -395,12 +393,11 @@ let opt_dbg3_encoding = conv (fun dbg3 -> dbg3) (fun dbg3 -> dbg3) - (obj5 + (obj4 (opt "debug_types" bool) (opt "debug_uf" bool) (opt "debug_unsat_core" bool) (opt "debug_use" bool) - (opt "debug_warnings" bool) ) let opt1_encoding = @@ -551,8 +548,7 @@ let options_to_json opt = (opt.debug_types, opt.debug_uf, opt.debug_unsat_core, - opt.debug_use, - opt.debug_warnings) + opt.debug_use) in let all_opt1 = (opt.rule, @@ -677,8 +673,7 @@ let options_from_json options = let (debug_types, debug_uf, debug_unsat_core, - debug_use, - debug_warnings) = dbg_opt3 in + debug_use) = dbg_opt3 in let (rule, case_split_policy, enable_adts_cs, @@ -762,7 +757,6 @@ let options_from_json options = debug_uf; debug_unsat_core; debug_use; - debug_warnings; rule; case_split_policy; enable_adts_cs; diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli index c3f1c2bd30..723e0a84ea 100644 --- a/src/bin/js/worker_interface.mli +++ b/src/bin/js/worker_interface.mli @@ -78,7 +78,6 @@ type options = { debug_uf : bool option; debug_unsat_core : bool option; debug_use : bool option; - debug_warnings : bool option; rule : int option; case_split_policy : case_split_policy option; diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7945afddd0..25b56dc07f 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -1146,8 +1146,7 @@ let mk_forall_ter = let q = match form_view lem with Lemma q -> q | _ -> assert false in assert (equal q.main f (* should be true *)); if compare_quant q new_q <> 0 then raise Exit; - Printer.print_wrn ~warning:(Options.get_debug_warnings ()) - "(sub) axiom %s replaced with %s" name q.name; + Printer.print_wrn "(sub) axiom %s replaced with %s" name q.name; lem with Not_found | Exit -> let d = new_q.main.depth in (* + 1 ?? *) diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index cf9cdb0e4d..930ff56f19 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -175,7 +175,6 @@ let debug_types = ref false let debug_uf = ref false let debug_unsat_core = ref false let debug_use = ref false -let debug_warnings = ref false let debug_commands = ref false let debug_optimize = ref false let rule = ref (-1) @@ -204,7 +203,6 @@ let set_debug_types b = debug_types := b let set_debug_uf b = debug_uf := b let set_debug_unsat_core b = debug_unsat_core := b let set_debug_use b = debug_use := b -let set_debug_warnings b = debug_warnings := b let set_debug_commands b = debug_commands := b let set_debug_optimize b = debug_optimize := b let set_rule b = rule := b @@ -233,7 +231,6 @@ let get_debug_types () = !debug_types let get_debug_uf () = !debug_uf let get_debug_unsat_core () = !debug_unsat_core let get_debug_use () = !debug_use -let get_debug_warnings () = !debug_warnings let get_debug_commands () = !debug_commands let get_debug_optimize () = !debug_optimize let get_rule () = !rule @@ -361,7 +358,6 @@ let get_timelimit_per_goal () = !timelimit_per_goal let interpretation = ref INone let strict_mode = ref false let dump_models = ref false -let interpretation_use_underscore = ref false let objectives_in_interpretation = ref false let output_format = ref Native let model_type = ref Value @@ -371,7 +367,6 @@ let unsat_core = ref false let set_interpretation b = interpretation := b let set_strict_mode b = strict_mode := b let set_dump_models b = dump_models := b -let set_interpretation_use_underscore b = interpretation_use_underscore := b let set_objectives_in_interpretation b = objectives_in_interpretation := b let set_output_format b = output_format := b let set_model_type t = model_type := t @@ -400,7 +395,6 @@ let get_dump_models () = !dump_models let get_first_interpretation () = equal_mode !interpretation IFirst let get_every_interpretation () = equal_mode !interpretation IEvery let get_last_interpretation () = equal_mode !interpretation ILast -let get_interpretation_use_underscore () = !interpretation_use_underscore let get_objectives_in_interpretation () = !objectives_in_interpretation let get_output_format () = !output_format let get_output_smtlib () = diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index fdf8de25c8..8946e2e84b 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -173,9 +173,6 @@ val set_debug_unsat_core : bool -> unit (** Set [debug_use] accessible with {!val:get_debug_use} *) val set_debug_use : bool -> unit -(** Set [debug_warnings] accessible with {!val:get_debug_warnings} *) -val set_debug_warnings : bool -> unit - (** Set [debug_commands] accessible with {!val:get_debug_commands} *) val set_debug_commands : bool -> unit @@ -227,10 +224,6 @@ val set_strict_mode : bool -> unit (** [dump_models] accessible with {!val:get_dump_models}. *) val set_dump_models : bool -> unit -(** Set [interpretation_use_underscore] accessible with - {!val:get_interpretation_use_underscore} *) -val set_interpretation_use_underscore : bool -> unit - (** Set [objectives_in_interpretation] accessible with {!val:get_objectives_in_interpretation} *) val set_objectives_in_interpretation : bool -> unit @@ -469,9 +462,6 @@ val set_used_context_file : string -> unit (** Get the debugging flag. *) val get_debug : unit -> bool -(** Get the debugging flag of warnings. *) -val get_debug_warnings : unit -> bool - (** Get the debugging flag of commands. If enabled, Alt-Ergo will display all the commands that are sent to the solver. *) val get_debug_commands : unit -> bool @@ -746,11 +736,6 @@ val get_every_interpretation : unit -> bool val get_last_interpretation : unit -> bool (** Default to [false] *) -(** [true] if the interpretation_use_underscore is set to output _ - instead of fresh values *) -val get_interpretation_use_underscore : unit -> bool -(** Default to [false] *) - (** [true] if the objectives_in_interpretation is set to inline pretty-printing of optimized expressions in the model instead of a dedicated section '(objectives ...)'. Be aware that the model may diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml index 5a76274e00..6386b193df 100644 --- a/src/lib/util/printer.ml +++ b/src/lib/util/printer.ml @@ -227,12 +227,10 @@ let print_err ?(flushed=true) ?(header=(Options.get_output_with_headers ())) end else Format.ifprintf Format.err_formatter s -let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ())) - ?(warning=true) s = +let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ())) s = if Options.get_warning_as_error () then - print_err ~flushed ~header ~error:warning s + print_err ~flushed ~header ~error:true s else - if warning then begin let fmt = Options.Output.get_fmt_diagnostic () in Format.fprintf fmt "@[%s" (pp_smt clean_wrn_print); if header then @@ -242,8 +240,6 @@ let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ())) Format.fprintf fmt "@[[Warning] " ; if flushed || Options.get_output_with_forced_flush () then Format.kfprintf flush fmt s else Format.fprintf fmt s - end - else Format.ifprintf Format.err_formatter s let print_dbg ?(flushed=true) ?(header=(Options.get_output_with_headers ())) ?(module_name="") ?(function_name="") s = diff --git a/src/lib/util/printer.mli b/src/lib/util/printer.mli index 55245c69c4..98d1501e3e 100644 --- a/src/lib/util/printer.mli +++ b/src/lib/util/printer.mli @@ -47,13 +47,11 @@ val print_err : (** Print warning message on the warning formatter accessible with {!val:Options.get_fmt_wrn} and set by default to stderr. - Prints only if warning (true by default) is true. If header is set, prints a header "[Warning]". The wrn formatter is flushed after the print if flushed is set *) val print_wrn : ?flushed:bool -> ?header:bool -> - ?warning:bool -> ('a, Format.formatter, unit) format -> 'a (** Print debug message on the debug formatter accessible with diff --git a/src/preludes/cram.t/run.t b/src/preludes/cram.t/run.t deleted file mode 100644 index f7339f0e3b..0000000000 --- a/src/preludes/cram.t/run.t +++ /dev/null @@ -1,3 +0,0 @@ - $ alt-ergo ../fpa-theory-2017-01-04-16h00.ae - $ alt-ergo ../fpa-theory-2019-06-14-11h00.ae - $ alt-ergo ../fpa-theory-2019-10-08-19h00.ae diff --git a/src/preludes/dune b/src/preludes/dune deleted file mode 100644 index 8395d27632..0000000000 --- a/src/preludes/dune +++ /dev/null @@ -1,20 +0,0 @@ -(install - (package alt-ergo) - (section (site (alt-ergo preludes))) - (files - fpa-theory-2017-01-04-16h00.ae - fpa-theory-2019-06-14-11h00.ae - fpa-theory-2019-10-08-19h00.ae - ) -) - -(cram - (package alt-ergo) - (alias runtest-ci) - (deps - %{bin:alt-ergo} - fpa-theory-2017-01-04-16h00.ae - fpa-theory-2019-06-14-11h00.ae - fpa-theory-2019-10-08-19h00.ae - ) -) diff --git a/src/preludes/fpa-theory-2017-01-04-16h00.ae b/src/preludes/fpa-theory-2017-01-04-16h00.ae deleted file mode 100644 index 3c396a10ed..0000000000 --- a/src/preludes/fpa-theory-2017-01-04-16h00.ae +++ /dev/null @@ -1,1027 +0,0 @@ -(******************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2017 --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of the license indicated *) -(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) -(* present, please contact us to clarify licensing. *) -(* *) -(******************************************************************************) - -(* raise a real to a power of an integer. Fully interpreted on -constants such that the exponent is a machine integer*) - -function pow_real_int(x : real, y : int) : real = x **. y - -(* raise a real to a power of a real. Fully interpreted on constants -such that the exponent is a machine integer*) - -function pow_real_real(x : real, y : real) : real = x **. y - - -theory Simple_FPA extends FPA = - - - (* what happends if we add versions for partially bounded float(x) ? - whould this be better ? *) - - axiom rounding_operator_1 : - forall x : real. - forall i, j : real. - forall i2, j2 : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - x in [i, j], - i2 |-> float(m, p, mode, i), - j2 |-> float(m, p, mode, j) - ] - { - i <= x, - x <= j - }. - i2 <= float(m, p, mode, x) <= j2 - - - axiom integer_rounding_operator_1 : - forall x : real. - forall i, j : real. - forall i2, j2 : int. - forall mode : fpa_rounding_mode - [ - integer_round(mode, x), - is_theory_constant(mode), - x in [i, j], - i2 |-> integer_round(mode, i), - j2 |-> integer_round(mode, j) - ] - { - i <= x, - x <= j - }. - i2 <= integer_round(mode, x) <= j2 - - - (* add the version with x in ? -> o(x) - x in ? *) - axiom rounding_operator_absolute_error_1_NearestTiesToEven : - forall x : real. - forall i, j, k : real. - forall exp_min, prec : int - [ - float(prec, exp_min, NearestTiesToEven, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - x in [i, j], - k |-> - pow_real_int( - 2., - integer_log2( - max_real( - abs_real(i), - max_real( - abs_real(j), - pow_real_int(2., - exp_min + prec-1) - ) - ) - ) - prec (* we can improve by -1 for some rounding modes *) - ) - ] - { - i <= x, - x <= j - }. - - k <= float(prec, exp_min, NearestTiesToEven, x) - x <= k - - - axiom rounding_operator_absolute_error_1_ALL : - forall x : real. - forall i, j, k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - x in [i, j], - k |-> - pow_real_int( - 2., - integer_log2( - max_real( - abs_real(i), - max_real( - abs_real(j), - pow_real_int(2., - exp_min + prec-1) - ) - ) - ) - prec + 1(* we can improve by -1 for some rounding modes *) - ) - ] - { - i <= x, - x <= j - }. - - k <= float(prec, exp_min, mode, x) - x <= k - - axiom monotonicity_contrapositive_1 : - forall x, i, k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in [?, i[, - k |-> float(prec, exp_min, Up, i) - ] - { - float(prec, exp_min, mode, x) < i - }. - (*float(prec, exp_min, mode, x) < i ->*) - x < k - - - axiom monotonicity_contrapositive_2 : - forall x, i, k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in ]i, ?], - k |-> float(prec, exp_min, Down, i) - ] - { - float(prec, exp_min, mode, x) > i - }. - (*float(prec, exp_min, mode, x) > i ->*) - x > k - - (* Remark: should add semantic trigger 'x <= y' - or maybe also 'float(m,p,md,x) > float(m,p,md,y)' in future - version *) - (* same as old monotonicity_contrapositive_3 *) - axiom float_is_monotonic: - forall m, p : int. - forall md : fpa_rounding_mode. - forall x, y : real - [ - float(m,p,md,x), float(m,p,md,y), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(md) - ]. - x <= y -> float(m,p,md,x) <= float(m,p,md,y) - - - (* these two axioms are too expensive if put inside a theory *) - axiom monotonicity_contrapositive_4 : - forall x, y : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x),float(prec, exp_min, mode, y), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < float(prec, exp_min, mode, y) -> - x < float(prec, exp_min, mode, y) - - axiom monotonicity_contrapositive_5 : - forall x, y : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), float(prec, exp_min, mode, y), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, x) < y - - - axiom contrapositive_enabeler_1 : - forall x, i : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in [?, i] - ] - { float(prec, exp_min, mode, x) <= i }. - float(prec, exp_min, mode, x) = i or float(prec, exp_min, mode, x) < i - - axiom contrapositive_enabeler_2 : - forall x, i : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in [i, ?] - ] - { float(prec, exp_min, mode, x) >= i }. - float(prec, exp_min, mode, x) = i or float(prec, exp_min, mode, x) > i - - - axiom gradual_underflow_1: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) > float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)) > 0. - - axiom gradual_underflow_2: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) > - float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)) > 0. - - - axiom gradual_underflow_3: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)) < 0. - - axiom gradual_underflow_4: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < - float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)) < 0. - - - axiom float_of_float_same_formats: - forall x : real. - forall mode1, mode2 : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode1, float(prec, exp_min, mode2, x)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode1), - is_theory_constant(mode2) - ]. - float(prec, exp_min, mode1, float(prec, exp_min, mode2, x)) = - float(prec, exp_min, mode2, x) - - axiom float_of_float_different_formats: - forall x : real. - forall mode1, mode2 : fpa_rounding_mode. - forall exp_min1, prec1, exp_min2, prec2 : int - [ - float(prec1, exp_min1, mode1, float(prec2, exp_min2, mode2, x)), - is_theory_constant(prec1), - is_theory_constant(exp_min1), - is_theory_constant(prec2), - is_theory_constant(exp_min2), - is_theory_constant(mode1), - is_theory_constant(mode2) - ]. - prec2 <= prec1 -> - exp_min2 <= exp_min1 -> - float(prec1, exp_min1, mode1, float(prec2, exp_min2, mode2, x)) = - float(prec2, exp_min2, mode2, x) - - - axiom tighten_float_intervals_1__min_large : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in [i, ?], - k |-> float(m, p, Up, i) - ] - { - i <= float(m, p, mode, x) - }. - (*i < k -> not needed => subsumed *) - k <= float(m, p, mode, x) - - axiom tighten_float_intervals__2__min_strict : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in ]i, ?], - k |-> float(m, p, Up, i) - ] - { - i < float(m, p, mode, x) - }. (* we can improve even if this condition is not true, with epsilon *) - (*i < k -> not needed => subsumed*) - k <= float(m, p, mode, x) - - axiom tighten_float_intervals_3__max_large : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in [?, i], - k |-> float(m, p, Down, i) - ] - { - i >= float(m, p, mode, x) - }. - (*k < i -> not needed => subsumed*) - k >= float(m, p, mode, x) - - axiom tighten_float_intervals__4__max_strict : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in [?, i[, - k |-> float(m, p, Down, i) - ] - { - float(m, p, mode, x) < i - }. (* we can improve even if this condition is not true, with epsilon *) - (*k < i -> not needed => subsumed*) - float(m, p, mode, x) <= k - - - axiom float_of_minus_float: - forall x : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, - float(m, p, mode, x)), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode) - ]. - float(m, p, mode, - float(m, p, mode, x)) = - float(m, p, mode, float(m, p, mode, x)) - (* which can be directly simplified to - float(m, p, mode, x). Another axiom will do this *) - (* this axiom probably applies more generally to float(m, p, mode, - x) = - float(m, p, mode, x) *) - - - axiom float_of_int: - forall x : int. - forall k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, real_of_int(x)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - real_of_int(x) + pow_real_int(2., prec) in [0., ?], - real_of_int(x) - pow_real_int(2., prec) in [?, 0.], - k |-> pow_real_int(2., prec) - ] - { - -k <= real_of_int(x), - real_of_int(x) <= k - }. - float(prec, exp_min, mode, real_of_int(x)) = real_of_int(x) - - - axiom float_of_pos_pow_of_two: - forall x, y, i, k1, k2 : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x * float(m, p, mode, y)), - is_theory_constant(p), - is_theory_constant(m), - is_theory_constant(mode), - is_theory_constant(x), - x in [i , i], - k1 |-> abs_real(i), - k2 |-> pow_real_int(2., integer_log2(abs_real(i))) - ]. - k1 >= 1. -> - k1 = k2 -> (* is pow of 2 ?*) - float(m, p, mode, x * float(m, p, mode, y)) = x * float(m, p, mode, y) - -end - -(*** Handling of real_of_int: ***) -theory Real_of_Int extends FPA = - - axiom roi_add : - forall x, y : int [real_of_int(x+y)]. - real_of_int(x + y) = real_of_int(x) + real_of_int(y) - - axiom roi_sub : - forall x, y : int [real_of_int(x-y)]. - real_of_int(x - y) = real_of_int(x) - real_of_int(y) - - axiom roi_mult : - forall x, y : int [real_of_int(x*y)]. - real_of_int(x * y) = real_of_int(x) * real_of_int(y) - - axiom roi_monotonicity_1 : - forall x : int. - forall k : real. - forall i : int - [real_of_int(x), x in ]?, i], k |-> real_of_int(i)] - {x <= i}. - real_of_int(x) <= k - - axiom roi_monotonicity_2 : - forall x : int. - forall k : real. - forall i : int - [real_of_int(x), x in [i, ?[, k |-> real_of_int(i)] - {i <= x}. - k <= real_of_int(x) - - axiom real_of_int_to_int_1 : - forall x, k : int. - forall i : real - [real_of_int(x), real_of_int(x) in ]?, i], k |-> int_floor(i)] - {real_of_int(x) <= i}. - x <= k - - axiom real_of_int_to_int_2 : - forall x, k : int. - forall i : real - [real_of_int(x), real_of_int(x) in [i, ?[, k |-> int_ceil(i)] - {i <= real_of_int(x)}. - k <= x - - (* can add other axioms on strict ineqs on rationals ? *) - -end - -theory ABS extends FPA = - - axiom abs_real_pos : - forall x : real - [ - abs_real(x), - x in [0., ?[ - ] - {x >= 0.}. - abs_real(x) = x - - axiom abs_real_neg : - forall x : real - [ - abs_real(x), - x in ]?, 0.] - ] - {x <= 0.}. - abs_real(x) = -x - - case_split abs_real_cs: - forall x : real - [ - abs_real(x), - x in [?i,?j], - 0. in ]?i,?j[ - ]. - (* not of the form (a or not a) to avoid simplification of F.mk_or *) - x <= 0. or x >= 0. - - axiom abs_real_interval_1 : - forall x : real - [ - abs_real(x), - abs_real(x) in [?i, ?j], - 0. in ]?i, ?j[ - ]. - 0. <= abs_real(x) - - axiom abs_real_interval_2 : (* should block this axiom once the deduction is made, - but this needs to have i and j on the left-hand-side of semantic triggers *) - forall i, j, k : real. - forall x : real - [ - abs_real(x), - x in [i, j], - k |-> max_real (abs_real(i), abs_real(j)) - ] - {i <= x, x <= j}. - abs_real(x) <= k - - axiom abs_real_interval_3 : (* should block this axiom once the deduction is made, - but this needs to have i and j on the left-hand-side of semantic triggers *) - forall i : real. - forall x : real - [ - abs_real(x), - abs_real(x) in [?, i] - ] - { abs_real(x) <= i }. - - i <= x <= i - - axiom abs_real_from_square_large: - forall x, y : real[x*x,y*y]. (* semantic triggers mising *) - x*x <= y*y -> - abs_real(x) <= abs_real(y) - - axiom abs_real_from_square_strict: - forall x, y : real[x*x,y*y]. (* semantic triggers mising *) - x*x < y*y -> - abs_real(x) < abs_real(y) - - - axiom abs_real_greater_than_real : - forall x : real - [ - abs_real(x) - ]. - x <= abs_real(x) - - - (* TODO: add semantic triggers not_theory_constant(x) on axioms of abs_int *) - - axiom abs_int_pos : - forall x : int[abs_int(x) , x in [0, ?[ ] - {x >= 0}. - abs_int(x) = x - - axiom abs_int_neg : - forall x : int[abs_int(x), x in ]?, 0]] - {x <= 0}. - abs_int(x) = -x - - case_split abs_int_cs: - forall x : int [abs_int(x) , x in [?i,?j], 0 in ]?i,?j[]. - (* not of the form (a or not a) to avoid simplification of F.mk_or *) - x <= 0 or x >= 0 - - axiom abs_int_interval_1 : - forall x : int [abs_int(x), abs_int(x) in [?i, ?j], 0 in ]?i, ?j[]. - 0 <= abs_int(x) - - axiom abs_int_interval_2 : - forall i, j, k : int. - forall x : int [abs_int(x), x in [i, j], k |-> max_int (abs_int(i), abs_int(j))] - {i <= x , x <= j}. - abs_int(x) <= k - - axiom abs_int_interval_3 : - forall i : int. - forall x : int [abs_int(x), abs_int(x) in [?, i]] - { abs_int(x) <= i }. - - i <= x <= i - -end - - -theory NRA extends FPA = - - (* TODO: linearizations with strict inequalities are missing *) - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_1: - forall x, y: real. - forall a: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x >= 0. -> - x*a <= x*y - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_2: - forall x, y: real. - forall a: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x <= 0. -> - x*a >= x*y - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_3: - forall x, y: real. - forall b: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x >= 0. -> - x*y <= x*b - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_4: - forall x, y: real. - forall b: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x <= 0. -> - x*y >= x*b - - - (* commutativity of four axiomes above *) - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_5: - forall x, y: real. - forall a: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x >= 0. -> - a*x <= y*x - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_6: - forall x, y: real. - forall a: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x <= 0. -> - a*x >= y*x - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_7: - forall x, y: real. - forall b: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x >= 0. -> - y*x <= b*x - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_8: - forall x, y: real. - forall b: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x <= 0. -> - y*x >= b*x - - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_1: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [c, ?] - ] - {a/b >= c}. - b > 0. -> - a >= b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_2: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [c, ?] - ] - {a/b >= c}. - b < 0. -> - a <= b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_3: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c] - ] - {a/b <= c}. - b > 0. -> - a <= b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_4: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c] - ] - {a/b <= c}. - b < 0. -> - a >= b * c - - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_1: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in ]c, ?] - ] - {a/b > c}. - b > 0. -> - a > b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_2: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in ]c, ?] - ] - {a/b > c}. - b < 0. -> - a < b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_3: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c[ - ] - {a/b < c}. - b > 0. -> - a < b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_4: (* add the same thing for equality ?? *) - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c[ - ] - {a/b < c}. - b < 0. -> - a > b * c - - - axiom linearize_mult_zero_one_1: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ] - {0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - x*y <= y - - axiom linearize_mult_zero_one_2: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ]{0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - y*x <= y - - axiom linearize_mult_zero_one_3: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ]{0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= x*y - - axiom linearize_mult_zero_one_4: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ]{0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= y*x - - axiom linearize_mult_zero_one_5: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - x*y <= y - - axiom linearize_mult_zero_one_6: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - y*x <= y - - axiom linearize_mult_zero_one_7: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= x*y - - axiom linearize_mult_zero_one_8: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= y*x - -end - -theory Principal_Sqrt_real extends FPA = (* some axioms about sqrt: shoud add more *) - -axiom sqrt_bounds: - forall x, i, j : real - [sqrt_real(x), x in [i,j]] - (* x may be a constant. i.e. x = i = j and sqrt_real(x) is not exact *) - {i <= x, x <= j}. - sqrt_real_default(i) <= sqrt_real(x) <= sqrt_real_excess(j) - -axiom sqrt_real_is_positive: - forall x:real[sqrt_real(x)]. (* semantic triggers ? case-split ? *) - x >= 0. -> - sqrt_real(x) >= 0. - -axiom sqrt_real_is_positive_strict: - forall x:real[sqrt_real(x)]. (* semantic triggers ? case-split ? *) - x > 0. -> - sqrt_real(x) > 0. - -axiom square_of_sqrt_real: - forall x:real[sqrt_real(x)]. (* semantic triggers ? case-split ? *) - x >= 0. -> - sqrt_real(x) * sqrt_real(x) = x - -axiom sqrt_real_of_square: - forall x:real[sqrt_real(x * x)]. (* semantic triggers ? case-split ? *) - x >= 0. -> - sqrt_real(x * x) = x - - -axiom sqrt_real_monotonicity: - forall x, y:real[sqrt_real(x), sqrt_real(y)]. - (* semantic triggers ? case-split ? *) - x >= 0. -> - y >= 0. -> - x <= y -> - sqrt_real(x) <= sqrt_real(y) - -(* what about contrapositive of sqrt_real_monotonicity *) - -axiom sqrt_real_monotonicity_strict: - forall x, y:real[sqrt_real(x), sqrt_real(y)]. - (* semantic triggers ? case-split ? *) - x >= 0. -> - y >= 0. -> - x < y -> - sqrt_real(x) < sqrt_real(y) - -(* what about contrapositive of sqrt_real_monotonicity_strict *) - -end diff --git a/src/preludes/fpa-theory-2019-06-14-11h00.ae b/src/preludes/fpa-theory-2019-06-14-11h00.ae deleted file mode 100644 index bbc40b0b01..0000000000 --- a/src/preludes/fpa-theory-2019-06-14-11h00.ae +++ /dev/null @@ -1,1050 +0,0 @@ -(******************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2017 --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of the license indicated *) -(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) -(* present, please contact us to clarify licensing. *) -(* *) -(******************************************************************************) - -(* raise a real to a power of an integer. Fully interpreted on -constants such that the exponent is a machine integer*) - -function pow_real_int(x : real, y : int) : real = x **. y - -(* raise a real to a power of a real. Fully interpreted on constants -such that the exponent is a machine integer*) - -function pow_real_real(x : real, y : real) : real = x **. y - -theory Simple_FPA extends FPA = - - - (* what happends if we add versions for partially bounded float(x) ? - whould this be better ? *) - - axiom rounding_operator_1 : - forall x : real. - forall i, j : real. - forall i2, j2 : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - x in [i, j], - i2 |-> float(m, p, mode, i), - j2 |-> float(m, p, mode, j) - ] - { - i <= x, - x <= j - }. - i2 <= float(m, p, mode, x) <= j2 - - - axiom integer_rounding_operator_1 : - forall x : real. - forall i, j : real. - forall i2, j2 : int. - forall mode : fpa_rounding_mode - [ - integer_round(mode, x), - is_theory_constant(mode), - x in [i, j], - i2 |-> integer_round(mode, i), - j2 |-> integer_round(mode, j) - ] - { - i <= x, - x <= j - }. - i2 <= integer_round(mode, x) <= j2 - - - (* add the version with x in ? -> o(x) - x in ? *) - axiom rounding_operator_absolute_error_1_NearestTiesToEven : - forall x : real. - forall i, j, k : real. - forall exp_min, prec : int - [ - float(prec, exp_min, NearestTiesToEven, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - x in [i, j], - k |-> - pow_real_int( - 2., - integer_log2( - max_real( - abs_real(i), - max_real( - abs_real(j), - pow_real_int(2., - exp_min + prec-1) - ) - ) - ) - prec (* we can improve by -1 for some rounding modes *) - ) - ] - { - i <= x, - x <= j - }. - - k <= float(prec, exp_min, NearestTiesToEven, x) - x <= k - - - axiom rounding_operator_absolute_error_1_ALL : - forall x : real. - forall i, j, k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - x in [i, j], - k |-> - pow_real_int( - 2., - integer_log2( - max_real( - abs_real(i), - max_real( - abs_real(j), - pow_real_int(2., - exp_min + prec-1) - ) - ) - ) - prec + 1(* we can improve by -1 for some rounding modes *) - ) - ] - { - i <= x, - x <= j - }. - - k <= float(prec, exp_min, mode, x) - x <= k - - axiom monotonicity_contrapositive_1 : - forall x, i, k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in [?, i[, - k |-> float(prec, exp_min, Up, i) - ] - { - float(prec, exp_min, mode, x) < i - }. - (*float(prec, exp_min, mode, x) < i ->*) - x < k - - - axiom monotonicity_contrapositive_2 : - forall x, i, k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in ]i, ?], - k |-> float(prec, exp_min, Down, i) - ] - { - float(prec, exp_min, mode, x) > i - }. - (*float(prec, exp_min, mode, x) > i ->*) - x > k - - (* Remark: should add semantic trigger 'x <= y' - or maybe also 'float(m,p,md,x) > float(m,p,md,y)' in future - version *) - (* same as old monotonicity_contrapositive_3 *) - axiom float_is_monotonic: - forall m, p : int. - forall md : fpa_rounding_mode. - forall x, y : real - [ - float(m,p,md,x), float(m,p,md,y), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(md) - ]. - x <= y -> float(m,p,md,x) <= float(m,p,md,y) - - - (* these two axioms are too expensive if put inside a theory *) - axiom monotonicity_contrapositive_4 : - forall x, y : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x),float(prec, exp_min, mode, y), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < float(prec, exp_min, mode, y) -> - x < float(prec, exp_min, mode, y) - - axiom monotonicity_contrapositive_5 : - forall x, y : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), float(prec, exp_min, mode, y), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, x) < y - - - axiom contrapositive_enabeler_1 : - forall x, i : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in [?, i] - ] - { float(prec, exp_min, mode, x) <= i }. - float(prec, exp_min, mode, x) = i or float(prec, exp_min, mode, x) < i - - axiom contrapositive_enabeler_2 : - forall x, i : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in [i, ?] - ] - { float(prec, exp_min, mode, x) >= i }. - float(prec, exp_min, mode, x) = i or float(prec, exp_min, mode, x) > i - - - axiom gradual_underflow_1: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) > float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)) > 0. - - axiom gradual_underflow_2: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) > - float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)) > 0. - - - axiom gradual_underflow_3: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)) < 0. - - axiom gradual_underflow_4: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < - float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)) < 0. - - - axiom float_of_float_same_formats: - forall x : real. - forall mode1, mode2 : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode1, float(prec, exp_min, mode2, x)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode1), - is_theory_constant(mode2) - ]. - float(prec, exp_min, mode1, float(prec, exp_min, mode2, x)) = - float(prec, exp_min, mode2, x) - - axiom float_of_float_different_formats: - forall x : real. - forall mode1, mode2 : fpa_rounding_mode. - forall exp_min1, prec1, exp_min2, prec2 : int - [ - float(prec1, exp_min1, mode1, float(prec2, exp_min2, mode2, x)), - is_theory_constant(prec1), - is_theory_constant(exp_min1), - is_theory_constant(prec2), - is_theory_constant(exp_min2), - is_theory_constant(mode1), - is_theory_constant(mode2) - ]. - prec2 <= prec1 -> - exp_min2 <= exp_min1 -> - float(prec1, exp_min1, mode1, float(prec2, exp_min2, mode2, x)) = - float(prec2, exp_min2, mode2, x) - - - axiom tighten_float_intervals_1__min_large : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in [i, ?], - k |-> float(m, p, Up, i) - ] - { - i <= float(m, p, mode, x) - }. - (*i < k -> not needed => subsumed *) - k <= float(m, p, mode, x) - - axiom tighten_float_intervals__2__min_strict : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in ]i, ?], - k |-> float(m, p, Up, i) - ] - { - i < float(m, p, mode, x) - }. (* we can improve even if this condition is not true, with epsilon *) - (*i < k -> not needed => subsumed*) - k <= float(m, p, mode, x) - - axiom tighten_float_intervals_3__max_large : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in [?, i], - k |-> float(m, p, Down, i) - ] - { - i >= float(m, p, mode, x) - }. - (*k < i -> not needed => subsumed*) - k >= float(m, p, mode, x) - - axiom tighten_float_intervals__4__max_strict : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in [?, i[, - k |-> float(m, p, Down, i) - ] - { - float(m, p, mode, x) < i - }. (* we can improve even if this condition is not true, with epsilon *) - (*k < i -> not needed => subsumed*) - float(m, p, mode, x) <= k - - - axiom float_of_minus_float: - forall x : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, - float(m, p, mode, x)), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode) - ]. - float(m, p, mode, - float(m, p, mode, x)) = - float(m, p, mode, float(m, p, mode, x)) - (* which can be directly simplified to - float(m, p, mode, x). Another axiom will do this *) - (* this axiom probably applies more generally to float(m, p, mode, - x) = - float(m, p, mode, x) *) - - - axiom float_of_int: - forall x : int. - forall k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, real_of_int(x)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - real_of_int(x) + pow_real_int(2., prec) in [0., ?], - real_of_int(x) - pow_real_int(2., prec) in [?, 0.], - k |-> pow_real_int(2., prec) - ] - { - -k <= real_of_int(x), - real_of_int(x) <= k - }. - float(prec, exp_min, mode, real_of_int(x)) = real_of_int(x) - - - axiom float_of_pos_pow_of_two: - forall x, y, i, k1, k2 : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x * float(m, p, mode, y)), - is_theory_constant(p), - is_theory_constant(m), - is_theory_constant(mode), - is_theory_constant(x), - x in [i , i], - k1 |-> abs_real(i), - k2 |-> pow_real_int(2., integer_log2(abs_real(i))) - ]. - k1 >= 1. -> - k1 = k2 -> (* is pow of 2 ?*) - float(m, p, mode, x * float(m, p, mode, y)) = x * float(m, p, mode, y) - - - axiom tighten_open_float_bounds : - forall x : real. - forall i, j, i2, j2 : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in ]i, j[, - i2 |-> float(m, p, Up, i + pow_real_int(2.,2 * (- p))), - j2 |-> float(m, p, Down, j - pow_real_int(2.,2 * (- p))) - (* pow_real_int(2.,2 * (- p)) is smaller than any gap between two successive floats *) - ] - { - float(m, p, mode, x) > i, - float(m, p, mode, x) < j - }. - i = float(m, p, mode, i) -> - j = float(m, p, mode, j) -> - i2 <= float(m, p, mode, x) <= j2 - -end - -(*** Handling of real_of_int: ***) -theory Real_of_Int extends FPA = - - axiom roi_add : - forall x, y : int [real_of_int(x+y)]. - real_of_int(x + y) = real_of_int(x) + real_of_int(y) - - axiom roi_sub : - forall x, y : int [real_of_int(x-y)]. - real_of_int(x - y) = real_of_int(x) - real_of_int(y) - - axiom roi_mult : - forall x, y : int [real_of_int(x*y)]. - real_of_int(x * y) = real_of_int(x) * real_of_int(y) - - axiom roi_monotonicity_1 : - forall x : int. - forall k : real. - forall i : int - [real_of_int(x), x in ]?, i], k |-> real_of_int(i)] - {x <= i}. - real_of_int(x) <= k - - axiom roi_monotonicity_2 : - forall x : int. - forall k : real. - forall i : int - [real_of_int(x), x in [i, ?[, k |-> real_of_int(i)] - {i <= x}. - k <= real_of_int(x) - - axiom real_of_int_to_int_1 : - forall x, k : int. - forall i : real - [real_of_int(x), real_of_int(x) in ]?, i], k |-> int_floor(i)] - {real_of_int(x) <= i}. - x <= k - - axiom real_of_int_to_int_2 : - forall x, k : int. - forall i : real - [real_of_int(x), real_of_int(x) in [i, ?[, k |-> int_ceil(i)] - {i <= real_of_int(x)}. - k <= x - - (* can add other axioms on strict ineqs on rationals ? *) - -end - -theory ABS extends FPA = - - axiom abs_real_pos : - forall x : real - [ - abs_real(x), - x in [0., ?[ - ] - {x >= 0.}. - abs_real(x) = x - - axiom abs_real_neg : - forall x : real - [ - abs_real(x), - x in ]?, 0.] - ] - {x <= 0.}. - abs_real(x) = -x - - case_split abs_real_cs: - forall x : real - [ - abs_real(x), - x in [?i,?j], - 0. in ]?i,?j[ - ]. - (* not of the form (a or not a) to avoid simplification of F.mk_or *) - x <= 0. or x >= 0. - - axiom abs_real_interval_1 : - forall x : real - [ - abs_real(x), - abs_real(x) in [?i, ?j], - 0. in ]?i, ?j[ - ]. - 0. <= abs_real(x) - - axiom abs_real_interval_2 : (* should block this axiom once the deduction is made, - but this needs to have i and j on the left-hand-side of semantic triggers *) - forall i, j, k : real. - forall x : real - [ - abs_real(x), - x in [i, j], - k |-> max_real (abs_real(i), abs_real(j)) - ] - {i <= x, x <= j}. - abs_real(x) <= k - - axiom abs_real_interval_3 : (* should block this axiom once the deduction is made, - but this needs to have i and j on the left-hand-side of semantic triggers *) - forall i : real. - forall x : real - [ - abs_real(x), - abs_real(x) in [?, i] - ] - { abs_real(x) <= i }. - - i <= x <= i - - axiom abs_real_from_square_large: - forall x, y : real[x*x,y*y]. (* semantic triggers mising *) - x*x <= y*y -> - abs_real(x) <= abs_real(y) - - axiom abs_real_from_square_strict: - forall x, y : real[x*x,y*y]. (* semantic triggers mising *) - x*x < y*y -> - abs_real(x) < abs_real(y) - - - axiom abs_real_greater_than_real : - forall x : real - [ - abs_real(x) - ]. - x <= abs_real(x) - - - (* TODO: add semantic triggers not_theory_constant(x) on axioms of abs_int *) - - axiom abs_int_pos : - forall x : int[abs_int(x) , x in [0, ?[ ] - {x >= 0}. - abs_int(x) = x - - axiom abs_int_neg : - forall x : int[abs_int(x), x in ]?, 0]] - {x <= 0}. - abs_int(x) = -x - - case_split abs_int_cs: - forall x : int [abs_int(x) , x in [?i,?j], 0 in ]?i,?j[]. - (* not of the form (a or not a) to avoid simplification of F.mk_or *) - x <= 0 or x >= 0 - - axiom abs_int_interval_1 : - forall x : int [abs_int(x), abs_int(x) in [?i, ?j], 0 in ]?i, ?j[]. - 0 <= abs_int(x) - - axiom abs_int_interval_2 : - forall i, j, k : int. - forall x : int [abs_int(x), x in [i, j], k |-> max_int (abs_int(i), abs_int(j))] - {i <= x , x <= j}. - abs_int(x) <= k - - axiom abs_int_interval_3 : - forall i : int. - forall x : int [abs_int(x), abs_int(x) in [?, i]] - { abs_int(x) <= i }. - - i <= x <= i - -end - - -theory NRA extends FPA = - - (* TODO: linearizations with strict inequalities are missing *) - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_1: - forall x, y: real. - forall a: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x >= 0. -> - x*a <= x*y - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_2: - forall x, y: real. - forall a: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x <= 0. -> - x*a >= x*y - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_3: - forall x, y: real. - forall b: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x >= 0. -> - x*y <= x*b - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_4: - forall x, y: real. - forall b: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x <= 0. -> - x*y >= x*b - - - (* commutativity of four axiomes above *) - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_5: - forall x, y: real. - forall a: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x >= 0. -> - a*x <= y*x - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_6: - forall x, y: real. - forall a: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x <= 0. -> - a*x >= y*x - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_7: - forall x, y: real. - forall b: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x >= 0. -> - y*x <= b*x - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_8: - forall x, y: real. - forall b: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x <= 0. -> - y*x >= b*x - - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_1: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [c, ?] - ] - {a/b >= c}. - b > 0. -> - a >= b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_2: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [c, ?] - ] - {a/b >= c}. - b < 0. -> - a <= b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_3: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c] - ] - {a/b <= c}. - b > 0. -> - a <= b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_4: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c] - ] - {a/b <= c}. - b < 0. -> - a >= b * c - - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_1: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in ]c, ?] - ] - {a/b > c}. - b > 0. -> - a > b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_2: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in ]c, ?] - ] - {a/b > c}. - b < 0. -> - a < b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_3: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c[ - ] - {a/b < c}. - b > 0. -> - a < b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_4: (* add the same thing for equality ?? *) - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c[ - ] - {a/b < c}. - b < 0. -> - a > b * c - - - axiom linearize_mult_zero_one_1: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ] - {0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - x*y <= y - - axiom linearize_mult_zero_one_2: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ]{0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - y*x <= y - - axiom linearize_mult_zero_one_3: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ]{0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= x*y - - axiom linearize_mult_zero_one_4: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ]{0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= y*x - - axiom linearize_mult_zero_one_5: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - x*y <= y - - axiom linearize_mult_zero_one_6: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - y*x <= y - - axiom linearize_mult_zero_one_7: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= x*y - - axiom linearize_mult_zero_one_8: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= y*x - -end - -theory Principal_Sqrt_real extends FPA = (* some axioms about sqrt: shoud add more *) - -axiom sqrt_bounds: - forall x, i, j : real - [sqrt_real(x), x in [i,j]] - (* x may be a constant. i.e. x = i = j and sqrt_real(x) is not exact *) - {i <= x, x <= j}. - sqrt_real_default(i) <= sqrt_real(x) <= sqrt_real_excess(j) - -axiom sqrt_real_is_positive: - forall x:real[sqrt_real(x)]. (* semantic triggers ? case-split ? *) - x >= 0. -> - sqrt_real(x) >= 0. - -axiom sqrt_real_is_positive_strict: - forall x:real[sqrt_real(x)]. (* semantic triggers ? case-split ? *) - x > 0. -> - sqrt_real(x) > 0. - -axiom square_of_sqrt_real: - forall x:real[sqrt_real(x)]. (* semantic triggers ? case-split ? *) - x >= 0. -> - sqrt_real(x) * sqrt_real(x) = x - -axiom sqrt_real_of_square: - forall x:real[sqrt_real(x * x)]. (* semantic triggers ? case-split ? *) - x >= 0. -> - sqrt_real(x * x) = x - - -axiom sqrt_real_monotonicity: - forall x, y:real[sqrt_real(x), sqrt_real(y)]. - (* semantic triggers ? case-split ? *) - x >= 0. -> - y >= 0. -> - x <= y -> - sqrt_real(x) <= sqrt_real(y) - -(* what about contrapositive of sqrt_real_monotonicity *) - -axiom sqrt_real_monotonicity_strict: - forall x, y:real[sqrt_real(x), sqrt_real(y)]. - (* semantic triggers ? case-split ? *) - x >= 0. -> - y >= 0. -> - x < y -> - sqrt_real(x) < sqrt_real(y) - -(* what about contrapositive of sqrt_real_monotonicity_strict *) - -end diff --git a/src/preludes/fpa-theory-2019-10-08-19h00.ae b/src/preludes/fpa-theory-2019-10-08-19h00.ae deleted file mode 100644 index 982f85f78f..0000000000 --- a/src/preludes/fpa-theory-2019-10-08-19h00.ae +++ /dev/null @@ -1,1038 +0,0 @@ -(******************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2017 --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of the license indicated *) -(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) -(* present, please contact us to clarify licensing. *) -(* *) -(******************************************************************************) - -theory Simple_FPA extends FPA = - - - (* what happends if we add versions for partially bounded float(x) ? - whould this be better ? *) - - axiom rounding_operator_1 : - forall x : real. - forall i, j : real. - forall i2, j2 : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - x in [i, j], - i2 |-> float(m, p, mode, i), - j2 |-> float(m, p, mode, j) - ] - { - i <= x, - x <= j - }. - i2 <= float(m, p, mode, x) <= j2 - - - axiom integer_rounding_operator_1 : - forall x : real. - forall i, j : real. - forall i2, j2 : int. - forall mode : fpa_rounding_mode - [ - integer_round(mode, x), - is_theory_constant(mode), - x in [i, j], - i2 |-> integer_round(mode, i), - j2 |-> integer_round(mode, j) - ] - { - i <= x, - x <= j - }. - i2 <= integer_round(mode, x) <= j2 - - - (* add the version with x in ? -> o(x) - x in ? *) - axiom rounding_operator_absolute_error_1_NearestTiesToEven : - forall x : real. - forall i, j, k : real. - forall exp_min, prec : int - [ - float(prec, exp_min, NearestTiesToEven, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - x in [i, j], - k |-> - 2 **. ( - integer_log2( - max_real( - abs_real(i), - max_real( - abs_real(j), - 2 **. (- exp_min + prec-1) - ) - ) - ) - prec (* we can improve by -1 for some rounding modes *) - ) - ] - { - i <= x, - x <= j - }. - - k <= float(prec, exp_min, NearestTiesToEven, x) - x <= k - - - axiom rounding_operator_absolute_error_1_ALL : - forall x : real. - forall i, j, k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - x in [i, j], - k |-> - 2 **. ( - integer_log2( - max_real( - abs_real(i), - max_real( - abs_real(j), - 2 **. (- exp_min + prec-1) - ) - ) - ) - prec + 1(* we can improve by -1 for some rounding modes *) - ) - ] - { - i <= x, - x <= j - }. - - k <= float(prec, exp_min, mode, x) - x <= k - - axiom monotonicity_contrapositive_1 : - forall x, i, k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in [?, i[, - k |-> float(prec, exp_min, Up, i) - ] - { - float(prec, exp_min, mode, x) < i - }. - (*float(prec, exp_min, mode, x) < i ->*) - x < k - - - axiom monotonicity_contrapositive_2 : - forall x, i, k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in ]i, ?], - k |-> float(prec, exp_min, Down, i) - ] - { - float(prec, exp_min, mode, x) > i - }. - (*float(prec, exp_min, mode, x) > i ->*) - x > k - - (* Remark: should add semantic trigger 'x <= y' - or maybe also 'float(m,p,md,x) > float(m,p,md,y)' in future - version *) - (* same as old monotonicity_contrapositive_3 *) - axiom float_is_monotonic: - forall m, p : int. - forall md : fpa_rounding_mode. - forall x, y : real - [ - float(m,p,md,x), float(m,p,md,y), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(md) - ]. - x <= y -> float(m,p,md,x) <= float(m,p,md,y) - - - (* these two axioms are too expensive if put inside a theory *) - axiom monotonicity_contrapositive_4 : - forall x, y : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x),float(prec, exp_min, mode, y), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < float(prec, exp_min, mode, y) -> - x < float(prec, exp_min, mode, y) - - axiom monotonicity_contrapositive_5 : - forall x, y : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), float(prec, exp_min, mode, y), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, x) < y - - - axiom contrapositive_enabeler_1 : - forall x, i : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in [?, i] - ] - { float(prec, exp_min, mode, x) <= i }. - float(prec, exp_min, mode, x) = i or float(prec, exp_min, mode, x) < i - - axiom contrapositive_enabeler_2 : - forall x, i : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, x), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - float(prec, exp_min, mode, x) in [i, ?] - ] - { float(prec, exp_min, mode, x) >= i }. - float(prec, exp_min, mode, x) = i or float(prec, exp_min, mode, x) > i - - - axiom gradual_underflow_1: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) > float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)) > 0. - - axiom gradual_underflow_2: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) > - float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)) > 0. - - - axiom gradual_underflow_3: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) - float(prec, exp_min, mode, y)) < 0. - - axiom gradual_underflow_4: - forall x, y : real. (* semantic triggers are missing! can we do better ? i.e. >= cst *) - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode) - ]. - float(prec, exp_min, mode, x) < - float(prec, exp_min, mode, y) -> - float(prec, exp_min, mode, float(prec, exp_min, mode, x) + float(prec, exp_min, mode, y)) < 0. - - - axiom float_of_float_same_formats: - forall x : real. - forall mode1, mode2 : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode1, float(prec, exp_min, mode2, x)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode1), - is_theory_constant(mode2) - ]. - float(prec, exp_min, mode1, float(prec, exp_min, mode2, x)) = - float(prec, exp_min, mode2, x) - - axiom float_of_float_different_formats: - forall x : real. - forall mode1, mode2 : fpa_rounding_mode. - forall exp_min1, prec1, exp_min2, prec2 : int - [ - float(prec1, exp_min1, mode1, float(prec2, exp_min2, mode2, x)), - is_theory_constant(prec1), - is_theory_constant(exp_min1), - is_theory_constant(prec2), - is_theory_constant(exp_min2), - is_theory_constant(mode1), - is_theory_constant(mode2) - ]. - prec2 <= prec1 -> - exp_min2 <= exp_min1 -> - float(prec1, exp_min1, mode1, float(prec2, exp_min2, mode2, x)) = - float(prec2, exp_min2, mode2, x) - - - axiom tighten_float_intervals_1__min_large : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in [i, ?], - k |-> float(m, p, Up, i) - ] - { - i <= float(m, p, mode, x) - }. - (*i < k -> not needed => subsumed *) - k <= float(m, p, mode, x) - - axiom tighten_float_intervals__2__min_strict : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in ]i, ?], - k |-> float(m, p, Up, i) - ] - { - i < float(m, p, mode, x) - }. (* we can improve even if this condition is not true, with epsilon *) - (*i < k -> not needed => subsumed*) - k <= float(m, p, mode, x) - - axiom tighten_float_intervals_3__max_large : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in [?, i], - k |-> float(m, p, Down, i) - ] - { - i >= float(m, p, mode, x) - }. - (*k < i -> not needed => subsumed*) - k >= float(m, p, mode, x) - - axiom tighten_float_intervals__4__max_strict : (* add a semantic trigger on o(i) - i *) - forall x : real. - forall i, k : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in [?, i[, - k |-> float(m, p, Down, i) - ] - { - float(m, p, mode, x) < i - }. (* we can improve even if this condition is not true, with epsilon *) - (*k < i -> not needed => subsumed*) - float(m, p, mode, x) <= k - - - axiom float_of_minus_float: - forall x : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, - float(m, p, mode, x)), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode) - ]. - float(m, p, mode, - float(m, p, mode, x)) = - float(m, p, mode, float(m, p, mode, x)) - (* which can be directly simplified to - float(m, p, mode, x). Another axiom will do this *) - (* this axiom probably applies more generally to float(m, p, mode, - x) = - float(m, p, mode, x) *) - - - axiom float_of_int: - forall x : int. - forall k : real. - forall mode : fpa_rounding_mode. - forall exp_min, prec : int - [ - float(prec, exp_min, mode, real_of_int(x)), - is_theory_constant(prec), - is_theory_constant(exp_min), - is_theory_constant(mode), - real_of_int(x) + (2 **. prec) in [0., ?], - real_of_int(x) - (2 **. prec) in [?, 0.], - k |-> 2 **. prec - ] - { - -k <= real_of_int(x), - real_of_int(x) <= k - }. - float(prec, exp_min, mode, real_of_int(x)) = real_of_int(x) - - - axiom float_of_pos_pow_of_two: - forall x, y, i, k1, k2 : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x * float(m, p, mode, y)), - is_theory_constant(p), - is_theory_constant(m), - is_theory_constant(mode), - is_theory_constant(x), - x in [i , i], - k1 |-> abs_real(i), - k2 |-> 2 **. (integer_log2(abs_real(i))) - ]. - k1 >= 1. -> - k1 = k2 -> (* is pow of 2 ?*) - float(m, p, mode, x * float(m, p, mode, y)) = x * float(m, p, mode, y) - - - axiom tighten_open_float_bounds : - forall x : real. - forall i, j, i2, j2 : real. - forall mode : fpa_rounding_mode. - forall p, m : int - [ - float(m, p, mode, x), - is_theory_constant(m), - is_theory_constant(p), - is_theory_constant(mode), - float(m, p, mode, x) in ]i, j[, - i2 |-> float(m, p, Up, i + (2 **. (2 * (- p)))), - j2 |-> float(m, p, Down, j - (2 **. (2 * (- p)))) - (* pow_real_int(2.,2 * (- p)) is smaller than any gap between two successive floats *) - ] - { - float(m, p, mode, x) > i, - float(m, p, mode, x) < j - }. - i = float(m, p, mode, i) -> - j = float(m, p, mode, j) -> - i2 <= float(m, p, mode, x) <= j2 - -end - -(*** Handling of real_of_int: ***) -theory Real_of_Int extends FPA = - - axiom roi_add : - forall x, y : int [real_of_int(x+y)]. - real_of_int(x + y) = real_of_int(x) + real_of_int(y) - - axiom roi_sub : - forall x, y : int [real_of_int(x-y)]. - real_of_int(x - y) = real_of_int(x) - real_of_int(y) - - axiom roi_mult : - forall x, y : int [real_of_int(x*y)]. - real_of_int(x * y) = real_of_int(x) * real_of_int(y) - - axiom roi_monotonicity_1 : - forall x : int. - forall k : real. - forall i : int - [real_of_int(x), x in ]?, i], k |-> real_of_int(i)] - {x <= i}. - real_of_int(x) <= k - - axiom roi_monotonicity_2 : - forall x : int. - forall k : real. - forall i : int - [real_of_int(x), x in [i, ?[, k |-> real_of_int(i)] - {i <= x}. - k <= real_of_int(x) - - axiom real_of_int_to_int_1 : - forall x, k : int. - forall i : real - [real_of_int(x), real_of_int(x) in ]?, i], k |-> int_floor(i)] - {real_of_int(x) <= i}. - x <= k - - axiom real_of_int_to_int_2 : - forall x, k : int. - forall i : real - [real_of_int(x), real_of_int(x) in [i, ?[, k |-> int_ceil(i)] - {i <= real_of_int(x)}. - k <= x - - (* can add other axioms on strict ineqs on rationals ? *) - -end - -theory ABS extends FPA = - - axiom abs_real_pos : - forall x : real - [ - abs_real(x), - x in [0., ?[ - ] - {x >= 0.}. - abs_real(x) = x - - axiom abs_real_neg : - forall x : real - [ - abs_real(x), - x in ]?, 0.] - ] - {x <= 0.}. - abs_real(x) = -x - - case_split abs_real_cs: - forall x : real - [ - abs_real(x), - x in [?i,?j], - 0. in ]?i,?j[ - ]. - (* not of the form (a or not a) to avoid simplification of F.mk_or *) - x <= 0. or x >= 0. - - axiom abs_real_interval_1 : - forall x : real - [ - abs_real(x), - abs_real(x) in [?i, ?j], - 0. in ]?i, ?j[ - ]. - 0. <= abs_real(x) - - axiom abs_real_interval_2 : (* should block this axiom once the deduction is made, - but this needs to have i and j on the left-hand-side of semantic triggers *) - forall i, j, k : real. - forall x : real - [ - abs_real(x), - x in [i, j], - k |-> max_real (abs_real(i), abs_real(j)) - ] - {i <= x, x <= j}. - abs_real(x) <= k - - axiom abs_real_interval_3 : (* should block this axiom once the deduction is made, - but this needs to have i and j on the left-hand-side of semantic triggers *) - forall i : real. - forall x : real - [ - abs_real(x), - abs_real(x) in [?, i] - ] - { abs_real(x) <= i }. - - i <= x <= i - - axiom abs_real_from_square_large: - forall x, y : real[x*x,y*y]. (* semantic triggers mising *) - x*x <= y*y -> - abs_real(x) <= abs_real(y) - - axiom abs_real_from_square_strict: - forall x, y : real[x*x,y*y]. (* semantic triggers mising *) - x*x < y*y -> - abs_real(x) < abs_real(y) - - - axiom abs_real_greater_than_real : - forall x : real - [ - abs_real(x) - ]. - x <= abs_real(x) - - - (* TODO: add semantic triggers not_theory_constant(x) on axioms of abs_int *) - - axiom abs_int_pos : - forall x : int[abs_int(x) , x in [0, ?[ ] - {x >= 0}. - abs_int(x) = x - - axiom abs_int_neg : - forall x : int[abs_int(x), x in ]?, 0]] - {x <= 0}. - abs_int(x) = -x - - case_split abs_int_cs: - forall x : int [abs_int(x) , x in [?i,?j], 0 in ]?i,?j[]. - (* not of the form (a or not a) to avoid simplification of F.mk_or *) - x <= 0 or x >= 0 - - axiom abs_int_interval_1 : - forall x : int [abs_int(x), abs_int(x) in [?i, ?j], 0 in ]?i, ?j[]. - 0 <= abs_int(x) - - axiom abs_int_interval_2 : - forall i, j, k : int. - forall x : int [abs_int(x), x in [i, j], k |-> max_int (abs_int(i), abs_int(j))] - {i <= x , x <= j}. - abs_int(x) <= k - - axiom abs_int_interval_3 : - forall i : int. - forall x : int [abs_int(x), abs_int(x) in [?, i]] - { abs_int(x) <= i }. - - i <= x <= i - -end - - -theory NRA extends FPA = - - (* TODO: linearizations with strict inequalities are missing *) - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_1: - forall x, y: real. - forall a: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x >= 0. -> - x*a <= x*y - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_2: - forall x, y: real. - forall a: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x <= 0. -> - x*a >= x*y - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_3: - forall x, y: real. - forall b: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x >= 0. -> - x*y <= x*b - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_4: - forall x, y: real. - forall b: real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x <= 0. -> - x*y >= x*b - - - (* commutativity of four axiomes above *) - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_5: - forall x, y: real. - forall a: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x >= 0. -> - a*x <= y*x - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_6: - forall x, y: real. - forall a: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [a,?] - ] - {a <= y}. - x <= 0. -> - a*x >= y*x - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_7: - forall x, y: real. - forall b: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x >= 0. -> - y*x <= b*x - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_mult_8: - forall x, y: real. - forall b: real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - | - x*y, - not_theory_constant(x), - not_theory_constant(y), - y in [?,b] - ] - {y <= b}. - x <= 0. -> - y*x >= b*x - - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_1: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [c, ?] - ] - {a/b >= c}. - b > 0. -> - a >= b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_2: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [c, ?] - ] - {a/b >= c}. - b < 0. -> - a <= b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_3: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c] - ] - {a/b <= c}. - b > 0. -> - a <= b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_4: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c] - ] - {a/b <= c}. - b < 0. -> - a >= b * c - - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_1: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in ]c, ?] - ] - {a/b > c}. - b > 0. -> - a > b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_2: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in ]c, ?] - ] - {a/b > c}. - b < 0. -> - a < b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_3: - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c[ - ] - {a/b < c}. - b > 0. -> - a < b * c - - (* needs more semantic triggers, case-split, and discarding of linear terms*) - axiom linearize_div_strict_4: (* add the same thing for equality ?? *) - forall a, b, c : real - [ - a/b, - not_theory_constant(b), - a/b in [?, c[ - ] - {a/b < c}. - b < 0. -> - a > b * c - - - axiom linearize_mult_zero_one_1: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ] - {0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - x*y <= y - - axiom linearize_mult_zero_one_2: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ]{0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - y*x <= y - - axiom linearize_mult_zero_one_3: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ]{0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= x*y - - axiom linearize_mult_zero_one_4: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - x in [0., 1.] - ]{0. <= x, x <= 1.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= y*x - - axiom linearize_mult_zero_one_5: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - x*y <= y - - axiom linearize_mult_zero_one_6: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y >= 0. -> - y*x <= y - - axiom linearize_mult_zero_one_7: - forall x, y : real - [ - x*y, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= x*y - - axiom linearize_mult_zero_one_8: - forall x, y : real - [ - y*x, - not_theory_constant(x), - not_theory_constant(y), - -x in [0., 1.] - ]{-1. <= x, x <= 0.}. (* needs cs on y an sem trigger on y *) - y <= 0. -> - y <= y*x - -end - -theory Principal_Sqrt_real extends FPA = (* some axioms about sqrt: shoud add more *) - -axiom sqrt_bounds: - forall x, i, j : real - [sqrt_real(x), x in [i,j]] - (* x may be a constant. i.e. x = i = j and sqrt_real(x) is not exact *) - {i <= x, x <= j}. - sqrt_real_default(i) <= sqrt_real(x) <= sqrt_real_excess(j) - -axiom sqrt_real_is_positive: - forall x:real[sqrt_real(x)]. (* semantic triggers ? case-split ? *) - x >= 0. -> - sqrt_real(x) >= 0. - -axiom sqrt_real_is_positive_strict: - forall x:real[sqrt_real(x)]. (* semantic triggers ? case-split ? *) - x > 0. -> - sqrt_real(x) > 0. - -axiom square_of_sqrt_real: - forall x:real[sqrt_real(x)]. (* semantic triggers ? case-split ? *) - x >= 0. -> - sqrt_real(x) * sqrt_real(x) = x - -axiom sqrt_real_of_square: - forall x:real[sqrt_real(x * x)]. (* semantic triggers ? case-split ? *) - x >= 0. -> - sqrt_real(x * x) = x - - -axiom sqrt_real_monotonicity: - forall x, y:real[sqrt_real(x), sqrt_real(y)]. - (* semantic triggers ? case-split ? *) - x >= 0. -> - y >= 0. -> - x <= y -> - sqrt_real(x) <= sqrt_real(y) - -(* what about contrapositive of sqrt_real_monotonicity *) - -axiom sqrt_real_monotonicity_strict: - forall x, y:real[sqrt_real(x), sqrt_real(y)]. - (* semantic triggers ? case-split ? *) - x >= 0. -> - y >= 0. -> - x < y -> - sqrt_real(x) < sqrt_real(y) - -(* what about contrapositive of sqrt_real_monotonicity_strict *) - -end