diff --git a/src/interpretation/interpreter.ml b/src/interpretation/interpreter.ml
index d025ea0c143f56ac9e4126461c743c88de9acafe..95ce3397e5f9559e52fdc1b749077b92d4dcb147 100644
--- a/src/interpretation/interpreter.ml
+++ b/src/interpretation/interpreter.ml
@@ -87,7 +87,13 @@ let builtin_of_constant env known_map (name, value) =
Logging.user_error (fun m ->
m "'%s' does not appear to be a declared toplevel constant" name)
-let rec bounded_quant_aux engine vs ~cond : IRE.bounded_quant_result option =
+type bounded_quant_result = {
+ new_quant : Why3.Term.vsymbol list;
+ substitutions : Why3.Term.term Why3.Term.Mvs.t;
+ remaining_implication : Why3.Term.term;
+}
+
+let rec bounded_quant_aux engine vs ~cond : bounded_quant_result option =
match vs.Why3.Term.vs_ty with
| {
ty_node = Tyapp ({ ts_name = { id_string = "vector"; _ }; _ }, ty :: _);
@@ -115,11 +121,10 @@ let rec bounded_quant_aux engine vs ~cond : IRE.bounded_quant_result option =
ITypes.Vector (Language.create_vector env n)
in
let substitutions =
- [
- Why3.Term.Mvs.singleton vs
- (ITypes.term_of_op ~args engine op (Some vs.vs_ty));
- ]
+ Why3.Term.Mvs.singleton vs
+ (ITypes.term_of_op ~args engine op (Some vs.vs_ty))
in
+
Some
{ new_quant; substitutions; remaining_implication = Why3.Term.t_true }
| Tapp ({ ls_name = { id_string = "has_length"; _ }; _ }, _) -> None
@@ -152,7 +157,7 @@ let rec bounded_quant_aux engine vs ~cond : IRE.bounded_quant_result option =
| _ -> None
(* Only one vector for now *)
-let rec bounded_quant engine vsl ~cond : IRE.bounded_quant_result option =
+let rec bounded_quant engine vsl ~cond : bounded_quant_result option =
match vsl with
| ({
Why3.Term.vs_ty =
@@ -164,14 +169,32 @@ let rec bounded_quant engine vsl ~cond : IRE.bounded_quant_result option =
} as vs)
:: l -> (
match bounded_quant_aux engine vs ~cond with
- | None -> None
- | Some r -> Some { r with new_quant = r.new_quant @ l })
+ | None -> bounded_quant engine l ~cond
+ | Some r1 -> (
+ match bounded_quant engine l ~cond:r1.remaining_implication with
+ | None -> Some { r1 with new_quant = r1.new_quant @ l }
+ | Some r2 ->
+ Some
+ {
+ new_quant = r1.new_quant @ r2.new_quant;
+ substitutions =
+ Why3.Term.Mvs.set_union r1.substitutions r2.substitutions;
+ remaining_implication = r2.remaining_implication;
+ }))
| v :: l -> (
match bounded_quant engine l ~cond with
| None -> None
| Some r -> Some { r with new_quant = v :: r.new_quant })
| [] -> None
+let bounded_quant engine vsl ~cond : IRE.bounded_quant_result option =
+ Option.map (bounded_quant engine vsl ~cond) ~f:(fun r ->
+ {
+ IRE.new_quant = r.new_quant;
+ substitutions = [ r.substitutions ];
+ remaining_implication = r.remaining_implication;
+ })
+
let declare_language_lsymbols interpreter_env task =
(* Declare [Language] logic symbols only. *)
Why3.Term.Hls.fold
diff --git a/tests/acasxu.t b/tests/acasxu.t
index ea9afd20dbaaf5b378e482ca79d09e095ee19f88..5f4fb0653afd4b83ea3e5906550a3a00f5bc431b 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -112,6 +112,19 @@ Test verify on acasxu
> let o2 = (nn_onnx @@ i)[weak_left] in
> o1, o2
>
+ > let run2v2 (i: input) (j: input)
+ > requires { has_length i 5 }
+ > requires { has_length j 5 }
+ > requires { valid_input i }
+ > requires { intruder_distant_and_slow i }
+ > requires { intruder_distant_and_slow j }
+ > ensures { let o1, o2 = result in o1 .>= o2 /\ o2 .>= o1 } =
+ > let i_ = normalize_input i in
+ > let j_ = normalize_input j in
+ > let o1 = (nn_onnx @@ i_)[clear_of_conflict] in
+ > let o2 = (nn_onnx @@ j_)[clear_of_conflict] in
+ > o1, o2
+ >
> let run3 (j: input) (eps:t)
> requires { has_length j 5 }
> requires { valid_input j }
@@ -344,6 +357,84 @@ Test verify on acasxu
x4 <= 60.0
y0 <= y1 and y1 <= y0
+ [DEBUG]{InterpretGoal} Interpreted formula for goal 'run2v2'vc':
+ forall x:t, x1:t, x2:t, x3:t, x4:t, x5:t, x6:t, x7:t, x8:t, x9:t.
+ ((le (0.0:t) x /\ le x (60760.0:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t)) x1 /\
+ le x1 (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t)) x2 /\
+ le x2 (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (100.0:t) x3 /\ le x3 (1200.0:t)) /\ le (0.0:t) x4 /\ le x4 (1200.0:t)) /\
+ (le (55947.6909999999988940544426441192626953125:t) x /\
+ le (1145.0:t) x3 /\ le x4 (60.0:t)) /\
+ le (55947.6909999999988940544426441192626953125:t) x5 /\
+ le (1145.0:t) x8 /\ le x9 (60.0:t) ->
+ le
+ (nn_onnx
+ @@ vector (div RNE (sub RNE x5 (19791.0:t)) (60261.0:t))
+ (div RNE (sub RNE x6 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x7 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x8 (650.0:t)) (1100.0:t))
+ (div RNE (sub RNE x9 (600.0:t)) (1200.0:t)))
+ [0]
+ (nn_onnx
+ @@ vector (div RNE (sub RNE x (19791.0:t)) (60261.0:t))
+ (div RNE (sub RNE x1 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x2 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x3 (650.0:t)) (1100.0:t))
+ (div RNE (sub RNE x4 (600.0:t)) (1200.0:t)))
+ [0] /\
+ le
+ (nn_onnx
+ @@ vector (div RNE (sub RNE x (19791.0:t)) (60261.0:t))
+ (div RNE (sub RNE x1 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x2 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x3 (650.0:t)) (1100.0:t))
+ (div RNE (sub RNE x4 (600.0:t)) (1200.0:t)))
+ [0]
+ (nn_onnx
+ @@ vector (div RNE (sub RNE x5 (19791.0:t)) (60261.0:t))
+ (div RNE (sub RNE x6 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x7 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x8 (650.0:t)) (1100.0:t))
+ (div RNE (sub RNE x9 (600.0:t)) (1200.0:t)))
+ [0]
+ nn_onnx,
+ (Interpreter_types.Model
+ (Interpreter_types.ONNX, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
+ nn_ty_elt = t;
+ nn_filename =
+ "./../examples/acasxu/nets/onnx/ACASXU_1_1.onnx";
+ nn_format = <nier> }))
+ vector,
+ 5
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ 0.0 <= x0
+ x0 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x1
+ x1 <= 3.141592653589793115997963468544185161590576171875
+ -3.141592653589793115997963468544185161590576171875 <= x2
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ 100.0 <= x3
+ x3 <= 1200.0
+ 0.0 <= x4
+ x4 <= 1200.0
+ 55947.6909999999988940544426441192626953125 <= x0
+ 1145.0 <= x3
+ x4 <= 60.0
+ 55947.6909999999988940544426441192626953125 <= x5
+ 1145.0 <= x8
+ x9 <= 60.0
+ y0 <= y1 and y1 <= y0
+
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run3'vc':
forall x:t, x1:t, x2:t, x3:t, x4:t, eps:t.
((le (0.0:t) x /\ le x (60760.0:t)) /\
@@ -456,13 +547,14 @@ Test verify on acasxu
(373.9499200000000200816430151462554931640625:t))
(7.51888402010059753166615337249822914600372314453125:t))
(1500.0:t)
- vector, 5
nn_nnet,
(Interpreter_types.Model
(Interpreter_types.NNet, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
nn_ty_elt = t;
nn_filename = "./TestNetwork.nnet";
nn_format = Language.NNet }))
+ vector,
+ 5
[DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625
@@ -530,13 +622,14 @@ Test verify on acasxu
(nn_nnet @@ vector x x1 x2 x3 x4)[3]) /\
lt (nn_nnet @@ vector x x1 x2 x3 x4)[0]
(nn_nnet @@ vector x x1 x2 x3 x4)[4])
- vector, 5
nn_nnet,
(Interpreter_types.Model
(Interpreter_types.NNet, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
nn_ty_elt = t;
nn_filename = "./TestNetwork.nnet";
nn_format = Language.NNet }))
+ vector,
+ 5
[DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625
@@ -560,6 +653,7 @@ Test verify on acasxu
Goal runP1'vc: Unknown ()
Goal runP1v2'vc: Unknown ()
Goal run2'vc: Unknown ()
+ Goal run2v2'vc: Unknown ()
Goal run3'vc: Unknown ()
Goal P1: Unknown ()
Goal P3: Unknown ()
@@ -721,6 +815,72 @@ 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)
+
+ ;; X_8
+ (declare-const X_8 Real)
+
+ ;; X_9
+ (declare-const X_9 Real)
+
+ ;; Requires
+ (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 100.0))
+ (assert (<= X_3 1200.0))
+ (assert (>= X_4 0.0))
+ (assert (<= X_4 1200.0))
+
+ ;; Requires
+ (assert (>= X_0 55947.6909999999988940544426441192626953125))
+ (assert (>= X_3 1145.0))
+ (assert (<= X_4 60.0))
+
+ ;; Requires
+ (assert (>= X_5 55947.6909999999988940544426441192626953125))
+ (assert (>= X_8 1145.0))
+ (assert (<= X_9 60.0))
+
+ ;; Y_1
+ (declare-const Y_1 Real)
+
+ ;; Y_0
+ (declare-const Y_0 Real)
+
+ ;; Goal run2v2'vc
+ (assert (or (and (>= Y_0 Y_1))
+ (and (>= Y_1 Y_0))
+ ))
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ ;;; produced by PyRAT/VNN-LIB driver
+ ;;; produced by VNN-LIB driver
+ ;; X_0
+ (declare-const X_0 Real)
+
+ ;; X_1
+ (declare-const X_1 Real)
+
+ ;; X_2
+ (declare-const X_2 Real)
+
+ ;; X_3
+ (declare-const X_3 Real)
+
+ ;; X_4
+ (declare-const X_4 Real)
+
+ ;; X_5
+ (declare-const X_5 Real)
+
;; Requires
(assert (>= X_0 0.0))
(assert (<= X_0 60760.0))
@@ -923,6 +1083,7 @@ Test verify on acasxu
Goal runP1'vc: Unknown ()
Goal runP1v2'vc: Unknown ()
Goal run2'vc: Unknown ()
+ Goal run2v2'vc: Unknown ()
Goal run3'vc: Unknown ()
Goal P1: Unknown ()
Goal P3: Unknown ()
@@ -1008,6 +1169,44 @@ Test verify on acasxu
x4 <= 60.0
+y1 -y0 >= 0
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 60760.0
+ x1 >= -3.141592653589793115997963468544185161590576171875
+ x1 <= 3.141592653589793115997963468544185161590576171875
+ x2 >= -3.141592653589793115997963468544185161590576171875
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ x3 >= 100.0
+ x3 <= 1200.0
+ x4 >= 0.0
+ x4 <= 1200.0
+ x0 >= 55947.6909999999988940544426441192626953125
+ x3 >= 1145.0
+ x4 <= 60.0
+ x5 >= 55947.6909999999988940544426441192626953125
+ x8 >= 1145.0
+ x9 <= 60.0
+ +y0 -y1 >= 0
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 60760.0
+ x1 >= -3.141592653589793115997963468544185161590576171875
+ x1 <= 3.141592653589793115997963468544185161590576171875
+ x2 >= -3.141592653589793115997963468544185161590576171875
+ x2 <= 3.141592653589793115997963468544185161590576171875
+ x3 >= 100.0
+ x3 <= 1200.0
+ x4 >= 0.0
+ x4 <= 1200.0
+ x0 >= 55947.6909999999988940544426441192626953125
+ x3 >= 1145.0
+ x4 <= 60.0
+ x5 >= 55947.6909999999988940544426441192626953125
+ x8 >= 1145.0
+ x9 <= 60.0
+ +y1 -y0 >= 0
+
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 60760.0
@@ -1086,6 +1285,7 @@ Test verify on acasxu
Goal runP1'vc: Unknown ()
Goal runP1v2'vc: Unknown ()
Goal run2'vc: Unknown ()
+ Goal run2v2'vc: Unknown ()
Goal run3'vc: Unknown ()
Goal P1: Unknown ()
Goal P3: Unknown ()