From f1b310a5ee0334c746a32eeed7593bcf25f4f75d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 4 Apr 2024 20:31:46 +0200
Subject: [PATCH] [NN_prover] Can convert to ONNX output terms
---
src/transformations/native_nn_prover.ml | 116 ++++---
tests/acasxu.t | 404 +++++++++++-------------
2 files changed, 257 insertions(+), 263 deletions(-)
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index f98ce39..347746b 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -25,10 +25,8 @@ open Base
let src = Logs.Src.create "NN-Gen" ~doc:"Generation of neural networks"
type new_output = {
- old_index : Why3.Number.int_constant;
- old_nn : Language.nn;
- new_index : int;
- old_nn_args : Why3.Term.term list;
+ index : int;
+ term : Why3.Term.term;
}
(** invariant:
@@ -52,6 +50,7 @@ let create_new_nn env input_vars outputs : string =
let i = Why3.Term.Mls.find_exn UnknownLogicSymbol ls input_vars in
Ir.Nier_simple.Node.gather_int input i)
in
+ let cache = Why3.Term.Hterm.create 17 in
let rec convert_old_nn (old_nn : Language.nn) old_index old_nn_args :
IR.GFloat.Node.t =
let old_index = Why3.Number.to_small_integer old_index in
@@ -97,6 +96,13 @@ let create_new_nn env input_vars outputs : string =
in
Ir.Nier_simple.Node.gather_int out old_index
and convert_term term : IR.GFloat.Node.t =
+ match Why3.Term.Hterm.find_opt cache term with
+ | None ->
+ let n = convert_term_aux term in
+ Why3.Term.Hterm.add cache term n;
+ n
+ | Some n -> n
+ and convert_term_aux term : IR.GFloat.Node.t =
if not (Why3.Ty.ty_equal (Option.value_exn term.Why3.Term.t_ty) th_f64.ty)
then
Logging.user_error ?loc:term.t_loc (fun m ->
@@ -175,8 +181,8 @@ let create_new_nn env input_vars outputs : string =
let outputs =
List.rev_map outputs ~f:(fun o ->
Int.decr r;
- assert (!r = o.new_index);
- convert_old_nn o.old_nn o.old_index o.old_nn_args)
+ assert (!r = o.index);
+ convert_term o.term)
in
let output = IR.Node.create (Concat { inputs = outputs; axis = 0 }) in
assert (
@@ -186,48 +192,53 @@ let create_new_nn env input_vars outputs : string =
Onnx.Simple.write nn filename;
filename
+let heuristic th_model th_nn term =
+ match term.Why3.Term.t_node with
+ | Tapp
+ ( ls_get (* [ ] *),
+ [
+ {
+ t_node =
+ Why3.Term.Tapp
+ ( ls_atat (* @@ *),
+ [
+ { t_node = Tapp (ls_nn (* nn *), _); _ };
+ {
+ t_node = Tapp (ls (* input vector *), tl (* input vars *));
+ _;
+ };
+ ] );
+ _;
+ };
+ { t_node = Tconst (ConstInt _); _ };
+ ] )
+ when String.equal ls_get.ls_name.id_string (Why3.Ident.op_get "")
+ && (Why3.Term.ls_equal ls_atat th_model.Symbols.Model.atat
+ || Why3.Term.ls_equal ls_atat th_nn.Symbols.NN.atat) -> (
+ match (Language.lookup_nn ls_nn, Language.lookup_vector ls) with
+ | Some { nn_nb_inputs; _ }, Some vector_length ->
+ assert (nn_nb_inputs = vector_length && vector_length = List.length tl);
+ true
+ | _, _ ->
+ Logging.code_error ~src (fun m ->
+ m "Neural network application without fixed NN or arguments: %a"
+ Why3.Pretty.print_term term))
+ | _ -> false
+
(** Abstract terms that contains neural network application *)
let abstract_nn_term env =
let th_model = Symbols.Model.create env in
let th_nn = Symbols.NN.create env in
+ let th_float64 = Symbols.Float64.create env in
let rec do_simplify (new_index, output_vars) term =
- match term.Why3.Term.t_node with
- | Tapp
- ( ls_get (* [ ] *),
- [
- {
- t_node =
- Why3.Term.Tapp
- ( ls_atat (* @@ *),
- [
- { t_node = Tapp (ls_nn (* nn *), _); _ };
- {
- t_node =
- Tapp (ls (* input vector *), tl (* input vars *));
- _;
- };
- ] );
- _;
- };
- { t_node = Tconst (ConstInt old_index); _ };
- ] )
- when String.equal ls_get.ls_name.id_string (Why3.Ident.op_get "")
- && (Why3.Term.ls_equal ls_atat th_model.atat
- || Why3.Term.ls_equal ls_atat th_nn.atat) -> (
- match (Language.lookup_nn ls_nn, Language.lookup_vector ls) with
- | Some ({ nn_nb_inputs; nn_ty_elt; _ } as old_nn), Some vector_length ->
- assert (nn_nb_inputs = vector_length && vector_length = List.length tl);
- let ls = Why3.(Term.create_fsymbol (Ident.id_fresh "y") [] nn_ty_elt) in
- let term = Why3.Term.fs_app ls [] nn_ty_elt in
- ( ( new_index + 1,
- ({ old_index; new_index; old_nn; old_nn_args = tl }, ls)
- :: output_vars ),
- term )
- | _, _ ->
- Logging.code_error ~src (fun m ->
- m "Neural network application without fixed NN or arguments: %a"
- Why3.Pretty.print_term term))
- | _ -> Why3.Term.t_map_fold do_simplify (new_index, output_vars) term
+ if heuristic th_model th_nn term
+ then
+ let ls =
+ Why3.(Term.create_fsymbol (Ident.id_fresh "y") [] th_float64.ty)
+ in
+ let term' = Why3.Term.fs_app ls [] th_float64.ty in
+ ((new_index + 1, ({ index = new_index; term }, ls) :: output_vars), term')
+ else Why3.Term.t_map_fold do_simplify (new_index, output_vars) term
in
Why3.Trans.fold_map
(fun task_hd (((index, input_vars) as acc), task) ->
@@ -242,9 +253,17 @@ let abstract_nn_term env =
| Decl
{
d_node =
- Dparam ({ ls_args = []; ls_constr = 0; ls_proj = false; _ } as ls);
+ Dparam
+ ({
+ ls_args = [];
+ ls_constr = 0;
+ ls_proj = false;
+ ls_value = Some ty;
+ _;
+ } as ls);
_;
- } ->
+ }
+ when Why3.Ty.ty_equal ty th_float64.ty ->
(* Add meta for input variable declarations. Note that each meta needs
to appear before the corresponding declaration in order to be
leveraged by prover printers. *)
@@ -270,13 +289,12 @@ let abstract_nn_term env =
(* Add meta for outputs *)
let task =
List.fold output_vars ~init:task
- ~f:(fun task ({ new_index; _ }, output_var) ->
+ ~f:(fun task ({ index; _ }, output_var) ->
let task =
Why3.Task.add_meta task Meta.meta_output
- [ MAls output_var; MAint new_index ]
+ [ MAls output_var; MAint index ]
in
- let decl = Why3.Decl.create_param_decl output_var in
- Why3.Task.add_decl task decl)
+ Why3.Task.add_param_decl task output_var)
in
let nn_filename =
create_new_nn env input_vars (List.map ~f:fst output_vars)
diff --git a/tests/acasxu.t b/tests/acasxu.t
index d098710..fb054b7 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -183,19 +183,19 @@ Test verify on acasxu
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x3
- x3 <= 60760.0
- -3.141592653589793115997963468544185161590576171875 <= x4
- x4 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x5
- x5 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x6
- x6 <= 1200.0
- 0.0 <= x7
- x7 <= 1200.0
- 55947.6909999999988940544426441192626953125 <= x3
- 1145.0 <= x6
- x7 <= 60.0
+ 0.0 <= x1
+ x1 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x2
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ -3.141592653589793115997963468544185161590576171875 <= x3
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ 100.0 <= x4
+ x4 <= 1200.0
+ 0.0 <= x5
+ x5 <= 1200.0
+ 55947.6909999999988940544426441192626953125 <= x1
+ 1145.0 <= x4
+ x5 <= 60.0
y0 <= 3.991125645861615112153231166303157806396484375
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run2'vc':
@@ -256,19 +256,19 @@ Test verify on acasxu
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x3
- x3 <= 60760.0
- -3.141592653589793115997963468544185161590576171875 <= x4
- x4 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x5
- x5 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x6
- x6 <= 1200.0
- 0.0 <= x7
- x7 <= 1200.0
- 55947.6909999999988940544426441192626953125 <= x3
- 1145.0 <= x6
- x7 <= 60.0
+ 0.0 <= x1
+ x1 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x2
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ -3.141592653589793115997963468544185161590576171875 <= x3
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ 100.0 <= x4
+ x4 <= 1200.0
+ 0.0 <= x5
+ x5 <= 1200.0
+ 55947.6909999999988940544426441192626953125 <= x1
+ 1145.0 <= x4
+ x5 <= 60.0
y0 <= y1 and y2 <= y3
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run3'vc':
@@ -330,21 +330,21 @@ Test verify on acasxu
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x3
- x3 <= 60760.0
- -3.141592653589793115997963468544185161590576171875 <= x4
- x4 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x5
- x5 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x6
- x6 <= 1200.0
- 0.0 <= x7
- x7 <= 1200.0
- 55947.6909999999988940544426441192626953125 <= x3
- 1145.0 <= x6
- x7 <= 60.0
- -1.0 <= x8
- x8 <= 1.0
+ 0.0 <= x1
+ x1 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x2
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ -3.141592653589793115997963468544185161590576171875 <= x3
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ 100.0 <= x4
+ x4 <= 1200.0
+ 0.0 <= x5
+ x5 <= 1200.0
+ 55947.6909999999988940544426441192626953125 <= x1
+ 1145.0 <= x4
+ x5 <= 60.0
+ -1.0 <= x6
+ x6 <= 1.0
y0 <= y1 and y2 <= y3
[DEBUG]{InterpretGoal} Interpreted formula for goal 'test'vc':
@@ -381,19 +381,19 @@ Test verify on acasxu
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x3
- x3 <= 60760.0
- -3.141592653589793115997963468544185161590576171875 <= x4
- x4 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x5
- x5 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x6
- x6 <= 1200.0
- 0.0 <= x7
- x7 <= 1200.0
- 55947.6909999999988940544426441192626953125 <= x3
- 1145.0 <= x6
- x7 <= 60.0
+ 0.0 <= x1
+ x1 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x2
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ -3.141592653589793115997963468544185161590576171875 <= x3
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ 100.0 <= x4
+ x4 <= 1200.0
+ 0.0 <= x5
+ x5 <= 1200.0
+ 55947.6909999999988940544426441192626953125 <= x1
+ 1145.0 <= x4
+ x5 <= 60.0
y0 <= 3.991125645861615112153231166303157806396484375
[DEBUG]{InterpretGoal} Interpreted formula for goal 'P3':
@@ -504,28 +504,22 @@ Test verify on acasxu
;; X_5
(declare-const X_5 Real)
- ;; X_6
- (declare-const X_6 Real)
-
- ;; X_7
- (declare-const X_7 Real)
-
;; Requires
- (assert (>= X_3 0.0))
- (assert (<= X_3 60760.0))
- (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_6 100.0))
- (assert (<= X_6 1200.0))
- (assert (>= X_7 0.0))
- (assert (<= X_7 1200.0))
+ (assert (>= X_1 0.0))
+ (assert (<= X_1 60760.0))
+ (assert (>= X_2 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_2 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_3 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_3 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_4 100.0))
+ (assert (<= X_4 1200.0))
+ (assert (>= X_5 0.0))
+ (assert (<= X_5 1200.0))
;; Requires
- (assert (>= X_3 55947.6909999999988940544426441192626953125))
- (assert (>= X_6 1145.0))
- (assert (<= X_7 60.0))
+ (assert (>= X_1 55947.6909999999988940544426441192626953125))
+ (assert (>= X_4 1145.0))
+ (assert (<= X_5 60.0))
;; Y_0
(declare-const Y_0 Real)
@@ -554,28 +548,22 @@ Test verify on acasxu
;; X_5
(declare-const X_5 Real)
- ;; X_6
- (declare-const X_6 Real)
-
- ;; X_7
- (declare-const X_7 Real)
-
;; Requires
- (assert (>= X_3 0.0))
- (assert (<= X_3 60760.0))
- (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_6 100.0))
- (assert (<= X_6 1200.0))
- (assert (>= X_7 0.0))
- (assert (<= X_7 1200.0))
+ (assert (>= X_1 0.0))
+ (assert (<= X_1 60760.0))
+ (assert (>= X_2 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_2 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_3 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_3 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_4 100.0))
+ (assert (<= X_4 1200.0))
+ (assert (>= X_5 0.0))
+ (assert (<= X_5 1200.0))
;; Requires
- (assert (>= X_3 55947.6909999999988940544426441192626953125))
- (assert (>= X_6 1145.0))
- (assert (<= X_7 60.0))
+ (assert (>= X_1 55947.6909999999988940544426441192626953125))
+ (assert (>= X_4 1145.0))
+ (assert (<= X_5 60.0))
;; Y_3
(declare-const Y_3 Real)
@@ -618,34 +606,28 @@ Test verify on acasxu
;; X_6
(declare-const X_6 Real)
- ;; X_7
- (declare-const X_7 Real)
-
- ;; X_8
- (declare-const X_8 Real)
-
;; Requires
- (assert (>= X_3 0.0))
- (assert (<= X_3 60760.0))
- (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_6 100.0))
- (assert (<= X_6 1200.0))
- (assert (>= X_7 0.0))
- (assert (<= X_7 1200.0))
+ (assert (>= X_1 0.0))
+ (assert (<= X_1 60760.0))
+ (assert (>= X_2 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_2 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_3 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_3 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_4 100.0))
+ (assert (<= X_4 1200.0))
+ (assert (>= X_5 0.0))
+ (assert (<= X_5 1200.0))
;; Requires
- (assert (>= X_3 55947.6909999999988940544426441192626953125))
- (assert (>= X_6 1145.0))
- (assert (<= X_7 60.0))
+ (assert (>= X_1 55947.6909999999988940544426441192626953125))
+ (assert (>= X_4 1145.0))
+ (assert (<= X_5 60.0))
;; H
- (assert (>= X_8 -1.0))
+ (assert (>= X_6 -1.0))
;; H
- (assert (<= X_8 1.0))
+ (assert (<= X_6 1.0))
;; Y_3
(declare-const Y_3 Real)
@@ -685,28 +667,22 @@ Test verify on acasxu
;; X_5
(declare-const X_5 Real)
- ;; X_6
- (declare-const X_6 Real)
-
- ;; X_7
- (declare-const X_7 Real)
-
;; Requires
- (assert (>= X_3 0.0))
- (assert (<= X_3 60760.0))
- (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_6 100.0))
- (assert (<= X_6 1200.0))
- (assert (>= X_7 0.0))
- (assert (<= X_7 1200.0))
+ (assert (>= X_1 0.0))
+ (assert (<= X_1 60760.0))
+ (assert (>= X_2 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_2 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_3 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_3 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_4 100.0))
+ (assert (<= X_4 1200.0))
+ (assert (>= X_5 0.0))
+ (assert (<= X_5 1200.0))
;; Requires
- (assert (>= X_3 55947.6909999999988940544426441192626953125))
- (assert (>= X_6 1145.0))
- (assert (<= X_7 60.0))
+ (assert (>= X_1 55947.6909999999988940544426441192626953125))
+ (assert (>= X_4 1145.0))
+ (assert (<= X_5 60.0))
;; Y_0
(declare-const Y_0 Real)
@@ -812,103 +788,103 @@ Test verify on acasxu
$ caisar verify --prover Marabou --ltag=ProverSpec file.mlw
[DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
+ x1 >= 0.0
+ x1 <= 60760.0
+ x2 >= -3.141592653589793115997963468544185161590576171875
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ x3 >= -3.141592653589793115997963468544185161590576171875
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ x4 >= 100.0
+ x4 <= 1200.0
+ x5 >= 0.0
+ x5 <= 1200.0
+ x1 >= 55947.6909999999988940544426441192626953125
+ x4 >= 1145.0
+ x5 <= 60.0
y0 >= 3.991125645861615112153231166303157806396484375
[DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
+ x1 >= 0.0
+ x1 <= 60760.0
+ x2 >= -3.141592653589793115997963468544185161590576171875
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ x3 >= -3.141592653589793115997963468544185161590576171875
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ x4 >= 100.0
+ x4 <= 1200.0
+ x5 >= 0.0
+ x5 <= 1200.0
+ x1 >= 55947.6909999999988940544426441192626953125
+ x4 >= 1145.0
+ x5 <= 60.0
+y0 -y1 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
+ x1 >= 0.0
+ x1 <= 60760.0
+ x2 >= -3.141592653589793115997963468544185161590576171875
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ x3 >= -3.141592653589793115997963468544185161590576171875
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ x4 >= 100.0
+ x4 <= 1200.0
+ x5 >= 0.0
+ x5 <= 1200.0
+ x1 >= 55947.6909999999988940544426441192626953125
+ x4 >= 1145.0
+ x5 <= 60.0
+y2 -y3 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
- x8 >= -1.0
- x8 <= 1.0
+ x1 >= 0.0
+ x1 <= 60760.0
+ x2 >= -3.141592653589793115997963468544185161590576171875
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ x3 >= -3.141592653589793115997963468544185161590576171875
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ x4 >= 100.0
+ x4 <= 1200.0
+ x5 >= 0.0
+ x5 <= 1200.0
+ x1 >= 55947.6909999999988940544426441192626953125
+ x4 >= 1145.0
+ x5 <= 60.0
+ x6 >= -1.0
+ x6 <= 1.0
+y0 -y1 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
- x8 >= -1.0
- x8 <= 1.0
+ x1 >= 0.0
+ x1 <= 60760.0
+ x2 >= -3.141592653589793115997963468544185161590576171875
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ x3 >= -3.141592653589793115997963468544185161590576171875
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ x4 >= 100.0
+ x4 <= 1200.0
+ x5 >= 0.0
+ x5 <= 1200.0
+ x1 >= 55947.6909999999988940544426441192626953125
+ x4 >= 1145.0
+ x5 <= 60.0
+ x6 >= -1.0
+ x6 <= 1.0
+y2 -y3 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
+ x1 >= 0.0
+ x1 <= 60760.0
+ x2 >= -3.141592653589793115997963468544185161590576171875
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ x3 >= -3.141592653589793115997963468544185161590576171875
+ x3 <= 3.141592653589793115997963468544185161590576171875
+ x4 >= 100.0
+ x4 <= 1200.0
+ x5 >= 0.0
+ x5 <= 1200.0
+ x1 >= 55947.6909999999988940544426441192626953125
+ x4 >= 1145.0
+ x5 <= 60.0
y0 >= 3.991125645861615112153231166303157806396484375
[DEBUG]{ProverSpec} Prover-tailored specification:
--
GitLab