From 1924184c50b9f1aaac01ce611f8b8d7d9e8e87c9 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 7 Nov 2023 14:31:22 +0100 Subject: [PATCH] Flambda compilation instructions --- FLAMBDA.md | 86 +++ alt-ergo-lib.opam | 3 - dune-project | 3 - src/bin/common/solving_loop.ml | 1 - src/lib/dune | 2 - src/lib/reasoners/th_util.ml | 8 +- src/lib/reasoners/th_util.mli | 3 +- src/lib/util/theories.ml | 1069 +++++++++++++++++++++++++++++++- src/lib/util/timers.ml | 11 +- 9 files changed, 1170 insertions(+), 16 deletions(-) create mode 100644 FLAMBDA.md diff --git a/FLAMBDA.md b/FLAMBDA.md new file mode 100644 index 0000000000..09d2d6d62f --- /dev/null +++ b/FLAMBDA.md @@ -0,0 +1,86 @@ +# FLAMBDA + +This document describes how to install Alt-Ergo with FLAMBDA 1 and 2 with opam. +Note that the FLAMBDA 2 instructions are incomplete: feel free to fix them if +you manage to install alt-ergo with it. + +We first describe how to set up an opam switch with flambda, then how to +configure the compilation procedure with flambda + +## Install with FLAMBDA + +### FLAMBDA 1 + +First, create a fresh empty switch and install the base + +``` +$ opam switch create flambda1 --empty +$ eval $(opam env) +$ opam install ocaml-variants.4.14.1+options ocaml-option-flambda +$ opam switch set-invariant ocaml.4.14.1 +``` + +If alt-ergo depends on a specific version of dolmen, do not forget about pinning +the right dolmen version before installing the dependencies. + +`$ opam install . --deps-only` + +Finally, you can build with `m bin`. + +### FLAMBDA 2 + +To install Alt-Ergo with FLambda, you first need to have: +- ocaml.4.14.1 installed on your current opam switch; +- [opam-custom-install](https://gitlab.ocamlpro.com/louis/opam-custom-install) installed on any switch. + +Create a new switch in which we will install the compiler: + +``` +$ opam switch create flambda-backend --empty --repositories=flambda2=git+https://github.com/ocaml-flambda/flambda2-opam.git,default +$ opam switch THE_4.14.1_SWITCH +``` + +Fetch the `flambda-backend` repository: + +``` +$ git clone https://github.com/ocaml-flambda/flambda-backend.git +$ cd flambda-backend +``` + +Once in the flambda directory, configure the build directory: + +``` +$ autoconf +$ ./configure --prefix=PATH_TO_THE_EMPTY_FLAMBDA_SWITCH --enable-middle-end=flambda2 --enable-legacy-library-layout +``` + +The last option `--enable-legacy-library-layout` is required for projects on the +4.14.1 OCaml version (and probably 4.14.0 too) because of the `Unix` module +dependency. Then, you can build the project and install it on the +flambda-backend switch. + +``` +$ make _install +$ opam switch flambda-backend +$ opam custom-install ocaml-variants.4.14.1+flambda2 -- make install_for_opam +$ opam reinstall --forget-pending +$ opam install ocaml.4.14.1 +``` + +## Build with flambda + +When you build alt-ergo, you can set compilation options through the +`OCAMLPARAM` variable. Here is an example on how to set options to the +compiler to build alt-ergo with extreme optimization: + +``` +$OCAMLPARAM='_,rounds=5,O3=1,inline=100,inline-max-unroll=5' make bin +``` + +You can find an exhaustive documentation +[here](https://v2.ocaml.org/manual/flambda.html). +You may also want to use `ulimit` if you plan to use your computer while +compiling. + +NB: this variable can also be set to the `opam install` commands installing the +dependencies to optimize them as well. \ No newline at end of file diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index b4e86e7ca4..da8ec854f8 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -25,14 +25,11 @@ depends: [ "seq" "fmt" {>= "0.9.0"} "stdlib-shims" - "ppx_blob" {>= "0.7.2"} "camlzip" {>= "1.07"} "odoc" {with-doc} - "ppx_deriving" "stdcompat" ] conflicts: [ - "ppxlib" {< "0.30.0"} "result" {< "1.5"} ] build: [ diff --git a/dune-project b/dune-project index cab2fcd37f..bfec98747c 100644 --- a/dune-project +++ b/dune-project @@ -85,14 +85,11 @@ See more details on http://alt-ergo.ocamlpro.com/" seq (fmt (>= 0.9.0)) stdlib-shims - (ppx_blob (>= 0.7.2)) (camlzip (>= 1.07)) (odoc :with-doc) - ppx_deriving stdcompat ) (conflicts - (ppxlib (< 0.30.0)) (result (< 1.5)) ) ) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 3d720dc0ab..4a0d6d80d8 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -27,7 +27,6 @@ (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) - open AltErgoLib open D_loop diff --git a/src/lib/dune b/src/lib/dune index 2d98a19bd8..04beebaaa3 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -26,8 +26,6 @@ fmt stdcompat ) - (preprocess (pps ppx_blob ppx_deriving.show ppx_deriving.enum ppx_deriving.fold)) - (preprocessor_deps (glob_files ../preludes/*.ae)) ; .mli only modules *also* need to be in this field (modules_without_implementation matching_types sig sig_rel) diff --git a/src/lib/reasoners/th_util.ml b/src/lib/reasoners/th_util.ml index fd86d5a77a..23307f58fc 100644 --- a/src/lib/reasoners/th_util.ml +++ b/src/lib/reasoners/th_util.ml @@ -36,7 +36,13 @@ type theory = | Th_adt | Th_arrays | Th_UF -[@@deriving show] + +let pp_theory fmt t = Fmt.string fmt @@ match t with + | Th_arith -> "Th_arith" + | Th_sum -> "Th_sum" + | Th_adt -> "Th_adt" + | Th_arrays -> "Th_arrays" + | Th_UF -> "Th_UF" type limit_kind = | Above diff --git a/src/lib/reasoners/th_util.mli b/src/lib/reasoners/th_util.mli index 40af9d4084..908ea384a2 100644 --- a/src/lib/reasoners/th_util.mli +++ b/src/lib/reasoners/th_util.mli @@ -36,7 +36,8 @@ type theory = | Th_adt | Th_arrays | Th_UF -[@@deriving show] + +val pp_theory : Format.formatter -> theory -> unit type limit_kind = | Above diff --git a/src/lib/util/theories.ml b/src/lib/util/theories.ml index dd1d0d3777..12ef14d7d8 100644 --- a/src/lib/util/theories.ml +++ b/src/lib/util/theories.ml @@ -16,6 +16,1069 @@ type prelude = Fpa | Ria | Nra +let fpa_ae = {| +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 + |} + +let ria_ae = +{| + +(*** Handling of real_of_int and real_is_int: ***) +theory Real_of_Int extends RIA = + axiom rii : forall x : real [real_is_int(x)]. real_is_int(x) = (x = real_of_int(int_floor(x))) + + 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 + + (* floor(x) ≤ i iff x < i + 1 *) + axiom int_floor_ub: + forall x, y : real, i : int + [ int_floor(x), not_theory_constant(x), int_floor(x) in ]?, i], y |-> real_of_int(i + 1) ] + { int_floor(x) <= i }. + x < y + + (* i <= floor(x) iff i <= x *) + axiom int_floor_lb: + forall x, y : real, i : int + [ int_floor(x), not_theory_constant(x), int_floor(x) in [i, ?[, y |-> real_of_int(i) ] + { i <= int_floor(x) }. + y <= x + + (* ceil(x) ≤ i iff x ≤ i *) + axiom int_ceil_ub: + forall x, y : real, i : int + [ int_ceil(x), not_theory_constant(x), int_ceil(x) in ]?, i], y |-> real_of_int(i) ] + { int_ceil(x) <= i }. + x <= y + + (* i <= ceil(x) iff i - 1 < x *) + axiom int_ceil_lb: + forall x, y : real, i : int + [ int_ceil(x), not_theory_constant(x), int_ceil(x) in [i, ?[, y |-> real_of_int(i - 1) ] + { i <= int_ceil(x) }. + y < x + + (* can add other axioms on strict ineqs on rationals ? *) + +end + +theory ABS extends RIA = + + 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 + |} + +let nra_ae = {| +theory Principal_Sqrt_real extends NRA = (* 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 + +theory Linearization extends NRA = + + (* 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 +|} + let pp_prelude ppf = function | Fpa -> Format.fprintf ppf "fpa" | Ria -> Format.fprintf ppf "ria" @@ -35,9 +1098,9 @@ let filename = Format.asprintf "/%a.ae" pp_prelude let content = function - | Fpa -> [%blob "src/preludes/fpa.ae"] - | Ria -> [%blob "src/preludes/ria.ae"] - | Nra -> [%blob "src/preludes/nra.ae"] + | Fpa -> fpa_ae + | Ria -> ria_ae + | Nra -> nra_ae let all_preludes = [ Fpa; Ria; Nra ] diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml index 0edeb3aab5..b48d9a0cbe 100644 --- a/src/lib/util/timers.ml +++ b/src/lib/util/timers.ml @@ -48,7 +48,11 @@ type ty_module = | M_Triggers | M_Simplex | M_Ite -[@@deriving enum] +(* [@@deriving enum] *) + +let max_ty_module = 14 + +let ty_module_to_enum = Obj.magic let all_modules = let l = [ @@ -94,7 +98,8 @@ type ty_function = | F_new_facts | F_apply_subst | F_instantiate -[@@deriving enum] + +let max_ty_function = 19 let all_functions = let l = [ @@ -162,6 +167,8 @@ let string_of_ty_function f = match f with | F_apply_subst -> "apply_subst" | F_instantiate -> "instantiate" +let ty_function_to_enum = Obj.magic + module TimerTable : sig (** The table of timers (module -> function -> float). *) type t