From f674765a87c0b83104c02d454ef2ea01848eb36a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 9 Apr 2024 17:59:22 +0200
Subject: [PATCH] [NN_prover] Keep only used inputs
---
src/transformations/native_nn_prover.ml | 43 +-
tests/acasxu.t | 592 ++++++------------------
2 files changed, 166 insertions(+), 469 deletions(-)
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index f8e4730..5acb447 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -276,35 +276,10 @@ let abstract_nn_term env =
let output_vars, goal = create_output_vars goal in
let pr = Why3.Decl.create_prsymbol (Why3.Ident.id_clone pr.pr_name) in
let decl = Why3.Decl.create_prop_decl Pgoal pr goal in
- (* Add default lower and upper bounds for each input variable. *)
- let task =
- Why3.Term.Mls.fold_left
- (fun task ls _ ->
- let task =
- Why3.Task.add_prop_decl task Paxiom
- (Why3.Decl.create_prsymbol
- (Why3.Ident.id_fresh "default_lower_bound"))
- (Why3.Term.ps_app th_float64.le
- [
- Utils.term_of_float env (-.Float.max_finite_value);
- Why3.Term.fs_app ls [] th_float64.ty;
- ])
- in
- let task =
- Why3.Task.add_prop_decl task Paxiom
- (Why3.Decl.create_prsymbol
- (Why3.Ident.id_fresh "default_upper_bound"))
- (Why3.Term.ps_app th_float64.le
- [
- Why3.Term.fs_app ls [] th_float64.ty;
- Utils.term_of_float env Float.max_finite_value;
- ])
- in
- task)
- task input_vars
- in
- (* Add meta for outputs. Again, for each output variable, add the meta
- first, then its actual declaration. *)
+
+ (* Again, for each output variable, add the meta first, then its actual
+ declaration. *)
+ (* Add meta for outputs *)
let task =
Why3.Term.Mterm.fold_left
(fun task _ (index, output_var) ->
@@ -320,6 +295,16 @@ let abstract_nn_term env =
(fun acc term (index, _) -> { index; term } :: acc)
[] output_vars
in
+ let used_ls =
+ List.fold
+ ~f:(fun acc out ->
+ Why3.Term.t_s_fold
+ (fun acc _ -> acc)
+ (fun acc ls -> Why3.Term.Sls.add ls acc)
+ acc out.term)
+ ~init:Why3.Term.Sls.empty output_vars
+ in
+ let input_vars = Why3.Term.Sls.inter input_vars used_ls in
let _, input_vars =
Why3.Term.Mls.mapi_fold (fun _ () i -> (i + 1, i)) input_vars 0
in
diff --git a/tests/acasxu.t b/tests/acasxu.t
index 9d0ec31..6747505 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -186,31 +186,19 @@ Test verify on acasxu
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x1
- x1 <= 60760.0
+ 0.0 <= x0
+ x0 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x1
+ x1 <= 3.141592653589793115997963468544185161590576171875
-3.141592653589793115997963468544185161590576171875 <= x2
x2 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x3
- x3 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x4
+ 100.0 <= x3
+ x3 <= 1200.0
+ 0.0 <= x4
x4 <= 1200.0
- 0.0 <= x5
- x5 <= 1200.0
- 55947.6909999999988940544426441192626953125 <= x1
- 1145.0 <= x4
- x5 <= 60.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x1
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x2
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x3
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x4
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x5
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ 55947.6909999999988940544426441192626953125 <= x0
+ 1145.0 <= x3
+ x4 <= 60.0
y0 <= 3.991125645861615112153231166303157806396484375
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run2'vc':
@@ -271,31 +259,19 @@ Test verify on acasxu
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x1
- x1 <= 60760.0
+ 0.0 <= x0
+ x0 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x1
+ x1 <= 3.141592653589793115997963468544185161590576171875
-3.141592653589793115997963468544185161590576171875 <= x2
x2 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x3
- x3 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x4
+ 100.0 <= x3
+ x3 <= 1200.0
+ 0.0 <= x4
x4 <= 1200.0
- 0.0 <= x5
- x5 <= 1200.0
- 55947.6909999999988940544426441192626953125 <= x1
- 1145.0 <= x4
- x5 <= 60.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x1
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x2
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x3
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x4
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x5
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ 55947.6909999999988940544426441192626953125 <= x0
+ 1145.0 <= x3
+ x4 <= 60.0
y0 <= y1 and y1 <= y0
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run3'vc':
@@ -357,35 +333,21 @@ Test verify on acasxu
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x1
- x1 <= 60760.0
+ 0.0 <= x0
+ x0 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x1
+ x1 <= 3.141592653589793115997963468544185161590576171875
-3.141592653589793115997963468544185161590576171875 <= x2
x2 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x3
- x3 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x4
+ 100.0 <= x3
+ x3 <= 1200.0
+ 0.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
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x1
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x2
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x3
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x4
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x5
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x6
- x6 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ 55947.6909999999988940544426441192626953125 <= x0
+ 1145.0 <= x3
+ x4 <= 60.0
+ -1.0 <= x5
+ x5 <= 1.0
y0 <= y1 and y1 <= y0
[DEBUG]{InterpretGoal} Interpreted formula for goal 'test'vc':
@@ -422,31 +384,19 @@ Test verify on acasxu
vector,
5
[DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x1
- x1 <= 60760.0
+ 0.0 <= x0
+ x0 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x1
+ x1 <= 3.141592653589793115997963468544185161590576171875
-3.141592653589793115997963468544185161590576171875 <= x2
x2 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x3
- x3 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x4
+ 100.0 <= x3
+ x3 <= 1200.0
+ 0.0 <= x4
x4 <= 1200.0
- 0.0 <= x5
- x5 <= 1200.0
- 55947.6909999999988940544426441192626953125 <= x1
- 1145.0 <= x4
- x5 <= 60.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x1
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x2
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x3
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x4
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 <= x5
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ 55947.6909999999988940544426441192626953125 <= x0
+ 1145.0 <= x3
+ x4 <= 60.0
y0 <= 3.991125645861615112153231166303157806396484375
[DEBUG]{InterpretGoal} Interpreted formula for goal 'P3':
@@ -554,61 +504,22 @@ Test verify on acasxu
;; X_4
(declare-const X_4 Real)
- ;; X_5
- (declare-const X_5 Real)
-
;; Requires
- (assert (>= X_1 0.0))
- (assert (<= X_1 60760.0))
+ (assert (>= X_0 0.0))
+ (assert (<= X_0 60760.0))
+ (assert (>= X_1 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_1 3.141592653589793115997963468544185161590576171875))
(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_3 100.0))
+ (assert (<= X_3 1200.0))
+ (assert (>= X_4 0.0))
(assert (<= X_4 1200.0))
- (assert (>= X_5 0.0))
- (assert (<= X_5 1200.0))
;; Requires
- (assert (>= X_1 55947.6909999999988940544426441192626953125))
- (assert (>= X_4 1145.0))
- (assert (<= X_5 60.0))
-
- ;; default_lower_bound
- (assert (>= X_0 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_0 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_1 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_1 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_2 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_2 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_3 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_3 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_4 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_4 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_5 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_5 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
+ (assert (>= X_0 55947.6909999999988940544426441192626953125))
+ (assert (>= X_3 1145.0))
+ (assert (<= X_4 60.0))
;; Y_0
(declare-const Y_0 Real)
@@ -634,61 +545,22 @@ Test verify on acasxu
;; X_4
(declare-const X_4 Real)
- ;; X_5
- (declare-const X_5 Real)
-
;; Requires
- (assert (>= X_1 0.0))
- (assert (<= X_1 60760.0))
+ (assert (>= X_0 0.0))
+ (assert (<= X_0 60760.0))
+ (assert (>= X_1 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_1 3.141592653589793115997963468544185161590576171875))
(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_3 100.0))
+ (assert (<= X_3 1200.0))
+ (assert (>= X_4 0.0))
(assert (<= X_4 1200.0))
- (assert (>= X_5 0.0))
- (assert (<= X_5 1200.0))
;; Requires
- (assert (>= X_1 55947.6909999999988940544426441192626953125))
- (assert (>= X_4 1145.0))
- (assert (<= X_5 60.0))
-
- ;; default_lower_bound
- (assert (>= X_0 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_0 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_1 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_1 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_2 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_2 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_3 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_3 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_4 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_4 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_5 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_5 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
+ (assert (>= X_0 55947.6909999999988940544426441192626953125))
+ (assert (>= X_3 1145.0))
+ (assert (<= X_4 60.0))
;; Y_1
(declare-const Y_1 Real)
@@ -722,73 +594,28 @@ Test verify on acasxu
;; X_5
(declare-const X_5 Real)
- ;; X_6
- (declare-const X_6 Real)
-
;; Requires
- (assert (>= X_1 0.0))
- (assert (<= X_1 60760.0))
+ (assert (>= X_0 0.0))
+ (assert (<= X_0 60760.0))
+ (assert (>= X_1 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_1 3.141592653589793115997963468544185161590576171875))
(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_3 100.0))
+ (assert (<= X_3 1200.0))
+ (assert (>= X_4 0.0))
(assert (<= X_4 1200.0))
- (assert (>= X_5 0.0))
- (assert (<= X_5 1200.0))
;; Requires
- (assert (>= X_1 55947.6909999999988940544426441192626953125))
- (assert (>= X_4 1145.0))
- (assert (<= X_5 60.0))
+ (assert (>= X_0 55947.6909999999988940544426441192626953125))
+ (assert (>= X_3 1145.0))
+ (assert (<= X_4 60.0))
;; H
- (assert (>= X_6 -1.0))
+ (assert (>= X_5 -1.0))
;; H
- (assert (<= X_6 1.0))
-
- ;; default_lower_bound
- (assert (>= X_0 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_0 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_1 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_1 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_2 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_2 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_3 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_3 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_4 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_4 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_5 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_5 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_6 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_6 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
+ (assert (<= X_5 1.0))
;; Y_0
(declare-const Y_0 Real)
@@ -819,61 +646,22 @@ Test verify on acasxu
;; X_4
(declare-const X_4 Real)
- ;; X_5
- (declare-const X_5 Real)
-
;; Requires
- (assert (>= X_1 0.0))
- (assert (<= X_1 60760.0))
+ (assert (>= X_0 0.0))
+ (assert (<= X_0 60760.0))
+ (assert (>= X_1 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_1 3.141592653589793115997963468544185161590576171875))
(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_3 100.0))
+ (assert (<= X_3 1200.0))
+ (assert (>= X_4 0.0))
(assert (<= X_4 1200.0))
- (assert (>= X_5 0.0))
- (assert (<= X_5 1200.0))
;; Requires
- (assert (>= X_1 55947.6909999999988940544426441192626953125))
- (assert (>= X_4 1145.0))
- (assert (<= X_5 60.0))
-
- ;; default_lower_bound
- (assert (>= X_0 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_0 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_1 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_1 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_2 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_2 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_3 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_3 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_4 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_4 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_lower_bound
- (assert (>= X_5 -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
-
- ;; default_upper_bound
- (assert (<= X_5 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
+ (assert (>= X_0 55947.6909999999988940544426441192626953125))
+ (assert (>= X_3 1145.0))
+ (assert (<= X_4 60.0))
;; Y_0
(declare-const Y_0 Real)
@@ -979,179 +767,103 @@ Test verify on acasxu
$ caisar verify --prover Marabou --ltag=ProverSpec file.mlw
[DEBUG]{ProverSpec} Prover-tailored specification:
- x1 >= 0.0
- x1 <= 60760.0
+ x0 >= 0.0
+ x0 <= 60760.0
+ x1 >= -3.141592653589793115997963468544185161590576171875
+ x1 <= 3.141592653589793115997963468544185161590576171875
x2 >= -3.141592653589793115997963468544185161590576171875
x2 <= 3.141592653589793115997963468544185161590576171875
- x3 >= -3.141592653589793115997963468544185161590576171875
- x3 <= 3.141592653589793115997963468544185161590576171875
- x4 >= 100.0
+ x3 >= 100.0
+ x3 <= 1200.0
+ x4 >= 0.0
x4 <= 1200.0
- x5 >= 0.0
- x5 <= 1200.0
- x1 >= 55947.6909999999988940544426441192626953125
- x4 >= 1145.0
- x5 <= 60.0
- x0 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ x0 >= 55947.6909999999988940544426441192626953125
+ x3 >= 1145.0
+ x4 <= 60.0
y0 >= 3.991125645861615112153231166303157806396484375
[DEBUG]{ProverSpec} Prover-tailored specification:
- x1 >= 0.0
- x1 <= 60760.0
+ x0 >= 0.0
+ x0 <= 60760.0
+ x1 >= -3.141592653589793115997963468544185161590576171875
+ x1 <= 3.141592653589793115997963468544185161590576171875
x2 >= -3.141592653589793115997963468544185161590576171875
x2 <= 3.141592653589793115997963468544185161590576171875
- x3 >= -3.141592653589793115997963468544185161590576171875
- x3 <= 3.141592653589793115997963468544185161590576171875
- x4 >= 100.0
+ x3 >= 100.0
+ x3 <= 1200.0
+ x4 >= 0.0
x4 <= 1200.0
- x5 >= 0.0
- x5 <= 1200.0
- x1 >= 55947.6909999999988940544426441192626953125
- x4 >= 1145.0
- x5 <= 60.0
- x0 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ x0 >= 55947.6909999999988940544426441192626953125
+ x3 >= 1145.0
+ x4 <= 60.0
+y0 -y1 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
- x1 >= 0.0
- x1 <= 60760.0
+ x0 >= 0.0
+ x0 <= 60760.0
+ x1 >= -3.141592653589793115997963468544185161590576171875
+ x1 <= 3.141592653589793115997963468544185161590576171875
x2 >= -3.141592653589793115997963468544185161590576171875
x2 <= 3.141592653589793115997963468544185161590576171875
- x3 >= -3.141592653589793115997963468544185161590576171875
- x3 <= 3.141592653589793115997963468544185161590576171875
- x4 >= 100.0
+ x3 >= 100.0
+ x3 <= 1200.0
+ x4 >= 0.0
x4 <= 1200.0
- x5 >= 0.0
- x5 <= 1200.0
- x1 >= 55947.6909999999988940544426441192626953125
- x4 >= 1145.0
- x5 <= 60.0
- x0 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ x0 >= 55947.6909999999988940544426441192626953125
+ x3 >= 1145.0
+ x4 <= 60.0
+y1 -y0 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
- x1 >= 0.0
- x1 <= 60760.0
+ x0 >= 0.0
+ x0 <= 60760.0
+ x1 >= -3.141592653589793115997963468544185161590576171875
+ x1 <= 3.141592653589793115997963468544185161590576171875
x2 >= -3.141592653589793115997963468544185161590576171875
x2 <= 3.141592653589793115997963468544185161590576171875
- x3 >= -3.141592653589793115997963468544185161590576171875
- x3 <= 3.141592653589793115997963468544185161590576171875
- x4 >= 100.0
+ x3 >= 100.0
+ x3 <= 1200.0
+ x4 >= 0.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
- x0 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x6 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x6 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ x0 >= 55947.6909999999988940544426441192626953125
+ x3 >= 1145.0
+ x4 <= 60.0
+ x5 >= -1.0
+ x5 <= 1.0
+y0 -y1 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
- x1 >= 0.0
- x1 <= 60760.0
+ x0 >= 0.0
+ x0 <= 60760.0
+ x1 >= -3.141592653589793115997963468544185161590576171875
+ x1 <= 3.141592653589793115997963468544185161590576171875
x2 >= -3.141592653589793115997963468544185161590576171875
x2 <= 3.141592653589793115997963468544185161590576171875
- x3 >= -3.141592653589793115997963468544185161590576171875
- x3 <= 3.141592653589793115997963468544185161590576171875
- x4 >= 100.0
+ x3 >= 100.0
+ x3 <= 1200.0
+ x4 >= 0.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
- x0 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x6 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x6 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ x0 >= 55947.6909999999988940544426441192626953125
+ x3 >= 1145.0
+ x4 <= 60.0
+ x5 >= -1.0
+ x5 <= 1.0
+y1 -y0 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
- x1 >= 0.0
- x1 <= 60760.0
+ x0 >= 0.0
+ x0 <= 60760.0
+ x1 >= -3.141592653589793115997963468544185161590576171875
+ x1 <= 3.141592653589793115997963468544185161590576171875
x2 >= -3.141592653589793115997963468544185161590576171875
x2 <= 3.141592653589793115997963468544185161590576171875
- x3 >= -3.141592653589793115997963468544185161590576171875
- x3 <= 3.141592653589793115997963468544185161590576171875
- x4 >= 100.0
+ x3 >= 100.0
+ x3 <= 1200.0
+ x4 >= 0.0
x4 <= 1200.0
- x5 >= 0.0
- x5 <= 1200.0
- x1 >= 55947.6909999999988940544426441192626953125
- x4 >= 1145.0
- x5 <= 60.0
- x0 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x0 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x1 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x2 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x3 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x4 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 >= -179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
- x5 <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
+ x0 >= 55947.6909999999988940544426441192626953125
+ x3 >= 1145.0
+ x4 <= 60.0
y0 >= 3.991125645861615112153231166303157806396484375
[DEBUG]{ProverSpec} Prover-tailored specification:
@@ -1185,11 +897,11 @@ Test verify on acasxu
$ python3 bin/inspect_onnx.py
caisar_0.onnx has 1 input nodes
- {'name': '38', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '6'}]}}}}
+ {'name': '38', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
caisar_1.onnx has 1 input nodes
- {'name': '134', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '6'}]}}}}
+ {'name': '134', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
caisar_2.onnx has 1 input nodes
- {'name': '298', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '7'}]}}}}
+ {'name': '298', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '6'}]}}}}
caisar_3.onnx has 1 input nodes
- {'name': '467', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '6'}]}}}}
+ {'name': '467', 'type': {'tensorType': {'elemType': 1, 'shape': {'dim': [{'dimValue': '5'}]}}}}
4 files checked
--
GitLab