Skip to content
Snippets Groups Projects
Commit f1b310a5 authored by François Bobot's avatar François Bobot
Browse files

[NN_prover] Can convert to ONNX output terms

parent ff4762ed
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/transformations/native_nn_prover.ml
+ 67
− 49
View file @ f1b310a5
......@@ -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)
......
tests/acasxu.t
+ 190
− 214
View file @ f1b310a5
......@@ -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:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment