diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index 857e8c7ce65448bf2a2a6d9856f4b36658a42fde..8b646979ec30b1f29baeedb58d90f983794f2897 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -45,6 +45,40 @@ let tempfile =
Stdlib.Filename.concat dir (Fmt.str "caisar_%i.onnx" !c)
| None -> Stdlib.Filename.temp_file "caisar" ".onnx"
+let match_nn_app 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 c); _ };
+ ] )
+ 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; _ } as nn), Some vector_length ->
+ assert (nn_nb_inputs = vector_length && vector_length = List.length tl);
+ let c = Why3.Number.to_small_integer c in
+ Some (nn, tl, c)
+ | _, _ ->
+ Logging.code_error ~src (fun m ->
+ m "Neural network application without fixed NN or arguments: %a"
+ Why3.Pretty.print_term term))
+ | _ -> None
+
let create_new_nn env input_vars outputs : string =
let module IR = Nir in
let th_f64 = Symbols.Float64.create env in
@@ -102,7 +136,6 @@ let create_new_nn env input_vars outputs : string =
out
and convert_old_nn_at_old_index old_nn old_index old_nn_args =
let out = convert_old_nn old_nn old_nn_args in
- let old_index = Why3.Number.to_small_integer old_index in
Nir.Node.gather_int out old_index
and convert_term term =
match Why3.Term.Hterm.find_opt cache term with
@@ -116,72 +149,50 @@ let create_new_nn env input_vars outputs : string =
then
Logging.user_error ?loc:term.t_loc (fun m ->
m "Cannot convert non Float64 term %a" Why3.Pretty.print_term term);
- match term.Why3.Term.t_node with
- | Tconst (Why3.Constant.ConstReal r) ->
- IR.Node.create
- (Constant
- {
- data = IR.Gentensor.create_1_float (Utils.float_of_real_constant r);
- })
- | Tapp (ls, []) -> get_input ls
- | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.add ->
- IR.Node.create (Add { input1 = convert_term a; input2 = convert_term b })
- | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.sub ->
- IR.Node.create (Sub { input1 = convert_term a; input2 = convert_term b })
- | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.mul ->
- IR.Node.create (Mul { input1 = convert_term a; input2 = convert_term b })
- | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.div -> (
- match b.t_node with
+ match match_nn_app th_model th_nn term with
+ | Some (old_nn, tl, old_index) ->
+ convert_old_nn_at_old_index old_nn old_index tl
+ | None -> (
+ match term.Why3.Term.t_node with
| Tconst (Why3.Constant.ConstReal r) ->
- let f = Utils.float_of_real_constant r in
- Nir.Node.div_float (convert_term a) f
- | _ ->
IR.Node.create
- (Div { input1 = convert_term a; input2 = convert_term b }))
- | Tapp (ls, [ a ]) when Why3.Term.ls_equal ls th_f64.neg ->
- Nir.Node.mul_float (convert_term a) (-1.)
- | Tapp
- ( ls_get (* [ ] *),
- [
- {
- t_node =
- 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; _ } as old_nn), Some vector_length ->
- assert (nn_nb_inputs = vector_length && vector_length = List.length tl);
- convert_old_nn_at_old_index old_nn old_index tl
- | _, _ ->
- Logging.code_error ~src (fun m ->
- m "Neural network application without fixed NN or arguments: %a"
- Why3.Pretty.print_term term))
- | Tconst _
- | Tapp (_, _)
- | Tif (_, _, _)
- | Tlet (_, _)
- | Tbinop (_, _, _)
- | Tcase (_, _)
- | Tnot _ | Ttrue | Tfalse ->
- Logging.not_implemented_yet (fun m ->
- m "Why3 term to IR: %a" Why3.Pretty.print_term term)
- | Tvar _ | Teps _ | Tquant (_, _) ->
- Logging.not_implemented_yet (fun m ->
- m "Why3 term to IR (impossible?): %a" Why3.Pretty.print_term term)
+ (Constant
+ {
+ data =
+ IR.Gentensor.create_1_float (Utils.float_of_real_constant r);
+ })
+ | Tapp (ls, []) -> get_input ls
+ | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.add ->
+ IR.Node.create
+ (Add { input1 = convert_term a; input2 = convert_term b })
+ | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.sub ->
+ IR.Node.create
+ (Sub { input1 = convert_term a; input2 = convert_term b })
+ | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.mul ->
+ IR.Node.create
+ (Mul { input1 = convert_term a; input2 = convert_term b })
+ | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.div -> (
+ match b.t_node with
+ | Tconst (Why3.Constant.ConstReal r) ->
+ let f = Utils.float_of_real_constant r in
+ Nir.Node.div_float (convert_term a) f
+ | _ ->
+ IR.Node.create
+ (Div { input1 = convert_term a; input2 = convert_term b }))
+ | Tapp (ls, [ a ]) when Why3.Term.ls_equal ls th_f64.neg ->
+ Nir.Node.mul_float (convert_term a) (-1.)
+ | Tconst _
+ | Tapp (_, _)
+ | Tif (_, _, _)
+ | Tlet (_, _)
+ | Tbinop (_, _, _)
+ | Tcase (_, _)
+ | Tnot _ | Ttrue | Tfalse ->
+ Logging.not_implemented_yet (fun m ->
+ m "Why3 term to IR: %a" Why3.Pretty.print_term term)
+ | Tvar _ | Teps _ | Tquant (_, _) ->
+ Logging.not_implemented_yet (fun m ->
+ m "Why3 term to IR (impossible?): %a" Why3.Pretty.print_term term))
in
(* Start actual term conversion. *)
let outputs =
@@ -202,57 +213,69 @@ let create_new_nn env input_vars outputs : string =
filename
let check_if_new_nn_needed env input_vars outputs =
- let _, indexed_input_vars =
- Why3.Term.Mls.mapi_fold (fun _ _ i -> (i + 1, i)) input_vars 0
- in
- let outputs1 =
- List.mapi outputs ~f:(fun index (term, _) -> { index; term })
- in
- let outputs2 = List.mapi outputs ~f:(fun index (_, ls) -> (index, ls)) in
- (create_new_nn env indexed_input_vars outputs1, indexed_input_vars, outputs2)
+ let th_model = Symbols.Model.create env in
+ let th_nn = Symbols.NN.create env in
+ let exception New_NN_Needed in
+ try
+ (* outputs must be direct application, inputs must be lsymbols *)
+ let outputs =
+ List.map outputs ~f:(fun (term, ls) ->
+ match match_nn_app th_model th_nn term with
+ | None -> raise New_NN_Needed
+ | Some (nn, tl, c) ->
+ let tl =
+ List.map tl ~f:(function
+ | { t_node = Why3.Term.Tapp (ls, []); _ } -> ls
+ | _ -> raise New_NN_Needed)
+ in
+ (ls, nn, tl, c))
+ in
+ match outputs with
+ | [] -> raise New_NN_Needed
+ | (_, nn, tl, _) :: _ ->
+ (* with the same nn and arguments *)
+ if not
+ (List.for_all outputs ~f:(fun (_, nn', tl', _) ->
+ String.equal nn'.Language.nn_filename nn.Language.nn_filename
+ && List.equal Why3.Term.ls_equal tl tl'))
+ then raise New_NN_Needed;
+ assert (Why3.Term.Sls.equal (Why3.Term.Sls.of_list tl) input_vars);
+ let outputs =
+ List.map outputs ~f:(fun (ls, _, _, index) -> (index, ls))
+ in
+ let compare (a, _) (b, _) = Int.compare a b in
+ let outputs = List.sort outputs ~compare in
+ assert (List.is_sorted_strictly outputs ~compare);
+ let indexed_input_vars =
+ List.mapi tl ~f:(fun i x -> (x, i)) |> Why3.Term.Mls.of_list
+ in
+ (nn.nn_filename, indexed_input_vars, outputs)
+ with New_NN_Needed ->
+ let _, indexed_input_vars =
+ Why3.Term.Mls.mapi_fold (fun _ _ i -> (i + 1, i)) input_vars 0
+ in
+ let outputs1 =
+ List.mapi outputs ~f:(fun index (term, _) -> { index; term })
+ in
+ let outputs2 = List.mapi outputs ~f:(fun index (_, ls) -> (index, ls)) in
+ (create_new_nn env indexed_input_vars outputs1, indexed_input_vars, outputs2)
(* Choose the term pattern for starting the conversion to ONNX. *)
let has_start_pattern env term =
let th_model = Symbols.Model.create env in
let th_nn = Symbols.NN.create env in
let th_f = Symbols.Float64.create env in
- 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))
- | Tapp ({ ls_value = Some ty; _ }, []) ->
- (* input symbol *) Why3.Ty.ty_equal ty th_f.ty
- | Tapp (ls_app, _) ->
- List.mem
- [ th_f.add; th_f.sub; th_f.mul; th_f.div ]
- ~equal:Why3.Term.ls_equal ls_app
- | _ -> false
+ match match_nn_app th_model th_nn term with
+ | Some _ -> true
+ | None -> (
+ match term.Why3.Term.t_node with
+ | Tapp ({ ls_value = Some ty; _ }, []) ->
+ (* input symbol *) Why3.Ty.ty_equal ty th_f.ty
+ | Tapp (ls_app, _) ->
+ List.mem
+ [ th_f.add; th_f.sub; th_f.mul; th_f.div ]
+ ~equal:Why3.Term.ls_equal ls_app
+ | _ -> false)
(* Abstract terms that contains neural network applications. *)
let abstract_nn_term env =
diff --git a/tests/acasxu.t b/tests/acasxu.t
index a80abb726d3ebe8b28c2ee96bf7c3c459f0a9b04..f37dc0c1bd2381c3bc2270fbbd7a0ce63ac46d66 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -368,7 +368,7 @@ Test verify on acasxu
55947.6909999999988940544426441192626953125 <= x0
1145.0 <= x3
x4 <= 60.0
- y0 <= y1 and y1 <= y0
+ y1 <= y0 and y0 <= y1
[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.
@@ -447,7 +447,7 @@ Test verify on acasxu
55947.6909999999988940544426441192626953125 <= x5
1145.0 <= x8
x9 <= 60.0
- y0 <= y1 and y1 <= y0
+ y1 <= y0 and y0 <= y1
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run3'vc':
forall x:t, x1:t, x2:t, x3:t, x4:t, eps:t.
@@ -641,115 +641,18 @@ 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 = <nir> }))
- [DEBUG]{ProverSpec} Prover-tailored specification:
- -0.328421367053318091766556108268559910356998443603515625 <= x0
- x0 <= 0.67985927880386987087746319957659579813480377197265625
- -0.499999999999967081887319864108576439321041107177734375 <= x1
- x1 <= 0.499999999999967081887319864108576439321041107177734375
- -0.499999999999967081887319864108576439321041107177734375 <= x2
- x2 <= 0.499999999999967081887319864108576439321041107177734375
- -0.5 <= x3
- x3 <= 0.5
- -0.5 <= x4
- x4 <= 0.5
- 0.60000151009774149724051994780893437564373016357421875 <= x0
- 0.450000000000000011102230246251565404236316680908203125 <= x3
- x4 <= -0.450000000000000011102230246251565404236316680908203125
- y0 <= 3.991125645861615112153231166303157806396484375
-
- [DEBUG]{InterpretGoal} Interpreted formula for goal 'P3':
- forall x:t, x1:t, x2:t, x3:t, x4:t.
- ((le (0.0:t) (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) (60760.0:t)) /\
- (le (neg (3.141592653589793115997963468544185161590576171875:t))
- (add RNE
- (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592653589793115997963468544185161590576171875:t)) /\
- (le (neg (3.141592653589793115997963468544185161590576171875:t))
- (add RNE
- (mul RNE x2 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE x2 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592653589793115997963468544185161590576171875:t)) /\
- (le (100.0:t) (add RNE (mul RNE x3 (1100.0:t)) (650.0:t)) /\
- le (add RNE (mul RNE x3 (1100.0:t)) (650.0:t)) (1200.0:t)) /\
- le (0.0:t) (add RNE (mul RNE x4 (1200.0:t)) (600.0:t)) /\
- le (add RNE (mul RNE x4 (1200.0:t)) (600.0:t)) (1200.0:t)) /\
- ((le (1500.0:t) (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) (1800.0:t)) /\
- le (neg (0.059999999999999997779553950749686919152736663818359375:t))
- (add RNE
- (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (0.059999999999999997779553950749686919152736663818359375:t)) /\
- le (3.100000000000000088817841970012523233890533447265625:t)
- (add RNE
- (mul RNE x2 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le (980.0:t) (add RNE (mul RNE x3 (1100.0:t)) (650.0:t)) /\
- le (960.0:t) (add RNE (mul RNE x4 (1200.0:t)) (600.0:t)) ->
- not (((lt (nn_nnet @@ vector x x1 x2 x3 x4)[0]
- (nn_nnet @@ vector x x1 x2 x3 x4)[1] /\
- lt (nn_nnet @@ vector x x1 x2 x3 x4)[0]
- (nn_nnet @@ vector x x1 x2 x3 x4)[2]) /\
- lt (nn_nnet @@ vector x x1 x2 x3 x4)[0]
- (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 = <nir> }))
- [DEBUG]{ProverSpec} Prover-tailored specification:
- -0.328421367053318091766556108268559910356998443603515625 <= x0
- x0 <= 0.67985927880386987087746319957659579813480377197265625
- -0.499999999999967081887319864108576439321041107177734375 <= x1
- x1 <= 0.499999999999967081887319864108576439321041107177734375
- -0.499999999999967081887319864108576439321041107177734375 <= x2
- x2 <= 0.499999999999967081887319864108576439321041107177734375
- -0.5 <= x3
- x3 <= 0.5
- -0.5 <= x4
- x4 <= 0.5
- -0.303529646039727207806890874053351581096649169921875 <= x0
- x0 <= -0.298551301837009008810497334707179106771945953369140625
- -0.0095492965855130916563719978285007528029382228851318359375 <= x1
- x1 <= 0.0095492965855130916563719978285007528029382228851318359375
- 0.493380323584843072382000173092819750308990478515625 <= x2
- 0.299999999999999988897769753748434595763683319091796875 <= x3
- 0.299999999999999988897769753748434595763683319091796875 <= x4
- (((y0 >= y1 or y0 >= y2) or y0 >= y3) or y0 >= y4)
-
- Goal runP1'vc: Unknown ()
- Goal runP1v2'vc: Unknown ()
- Goal run2'vc: Unknown ()
- Goal run2v2'vc: Unknown ()
- Goal run3'vc: Unknown ()
- Goal robust_output'vc: Unknown ()
- Goal P1: Unknown ()
- Goal P3: Unknown ()
+ vector,
+ 5
+ [DEBUG]{NN-Gen-Term} new goal:le y10 (1500.0:t)
+ [ERROR]{NN-Gen} No parsed NN './TestNetwork.nnet': Cannot read protobuf
+ Unrecoverable error: please report the issue at
+ https://git.frama-c.com/pub/caisar/issues
$ caisar verify --prover PyRAT --prover-altern VNNLIB --ltag=ProverSpec file.mlw
[DEBUG]{ProverSpec} Prover-tailored specification:
@@ -874,15 +777,15 @@ Test verify on acasxu
(assert (>= X_3 1145.0))
(assert (<= X_4 60.0))
- ;; Y_1
- (declare-const Y_1 Real)
-
;; Y_0
(declare-const Y_0 Real)
+ ;; Y_1
+ (declare-const Y_1 Real)
+
;; Goal run2'vc
- (assert (or (and (>= Y_0 Y_1))
- (and (>= Y_1 Y_0))
+ (assert (or (and (>= Y_1 Y_0))
+ (and (>= Y_0 Y_1))
))
[DEBUG]{ProverSpec} Prover-tailored specification:
@@ -940,15 +843,15 @@ Test verify on acasxu
(assert (>= X_8 1145.0))
(assert (<= X_9 60.0))
- ;; Y_1
- (declare-const Y_1 Real)
-
;; Y_0
(declare-const Y_0 Real)
+ ;; Y_1
+ (declare-const Y_1 Real)
+
;; Goal run2v2'vc
- (assert (or (and (>= Y_0 Y_1))
- (and (>= Y_1 Y_0))
+ (assert (or (and (>= Y_1 Y_0))
+ (and (>= Y_0 Y_1))
))
[DEBUG]{ProverSpec} Prover-tailored specification:
@@ -1053,179 +956,9 @@ Test verify on acasxu
(and (>= Y_0 0.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)
-
- ;; H
- (assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
-
- ;; H
- (assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
-
- ;; H
- (assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
-
- ;; H
- (assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
-
- ;; H
- (assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
-
- ;; H
- (assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
-
- ;; H
- (assert (>= X_3 -0.5))
-
- ;; H
- (assert (<= X_3 0.5))
-
- ;; H
- (assert (>= X_4 -0.5))
-
- ;; H
- (assert (<= X_4 0.5))
-
- ;; H
- (assert (>= X_0 0.60000151009774149724051994780893437564373016357421875))
-
- ;; H
- (assert (>= X_3 0.450000000000000011102230246251565404236316680908203125))
-
- ;; H
- (assert (<= X_4 -0.450000000000000011102230246251565404236316680908203125))
-
- ;; Y_0
- (declare-const Y_0 Real)
-
- ;; Y_1
- (declare-const Y_1 Real)
-
- ;; Y_2
- (declare-const Y_2 Real)
-
- ;; Y_3
- (declare-const Y_3 Real)
-
- ;; Y_4
- (declare-const Y_4 Real)
-
- ;; Goal P1
- (assert (>= Y_0 3.991125645861615112153231166303157806396484375))
-
- [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)
-
- ;; H
- (assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
-
- ;; H
- (assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
-
- ;; H
- (assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
-
- ;; H
- (assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
-
- ;; H
- (assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
-
- ;; H
- (assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
-
- ;; H
- (assert (>= X_3 -0.5))
-
- ;; H
- (assert (<= X_3 0.5))
-
- ;; H
- (assert (>= X_4 -0.5))
-
- ;; H
- (assert (<= X_4 0.5))
-
- ;; H
- (assert (>= X_0 -0.303529646039727207806890874053351581096649169921875))
-
- ;; H
- (assert (<= X_0 -0.298551301837009008810497334707179106771945953369140625))
-
- ;; H
- (assert (>= X_1 -0.0095492965855130916563719978285007528029382228851318359375))
-
- ;; H
- (assert (<= X_1 0.0095492965855130916563719978285007528029382228851318359375))
-
- ;; H
- (assert (>= X_2 0.493380323584843072382000173092819750308990478515625))
-
- ;; H
- (assert (>= X_3 0.299999999999999988897769753748434595763683319091796875))
-
- ;; H
- (assert (>= X_4 0.299999999999999988897769753748434595763683319091796875))
-
- ;; Y_0
- (declare-const Y_0 Real)
-
- ;; Y_1
- (declare-const Y_1 Real)
-
- ;; Y_2
- (declare-const Y_2 Real)
-
- ;; Y_3
- (declare-const Y_3 Real)
-
- ;; Y_4
- (declare-const Y_4 Real)
-
- ;; Goal P3
- (assert (<= Y_0 Y_1))
- (assert (<= Y_0 Y_2))
- (assert (<= Y_0 Y_3))
- (assert (<= Y_0 Y_4))
-
- Goal runP1'vc: Unknown ()
- Goal runP1v2'vc: Unknown ()
- Goal run2'vc: Unknown ()
- Goal run2v2'vc: Unknown ()
- Goal run3'vc: Unknown ()
- Goal robust_output'vc: Unknown ()
- Goal P1: Unknown ()
- Goal P3: Unknown ()
+ [ERROR]{NN-Gen} No parsed NN './TestNetwork.nnet': Cannot read protobuf
+ Unrecoverable error: please report the issue at
+ https://git.frama-c.com/pub/caisar/issues
$ caisar verify --prover Marabou --ltag=ProverSpec file.mlw
[DEBUG]{ProverSpec} Prover-tailored specification:
@@ -1290,7 +1023,7 @@ Test verify on acasxu
x0 >= 55947.6909999999988940544426441192626953125
x3 >= 1145.0
x4 <= 60.0
- +y0 -y1 >= 0
+ +y1 -y0 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
@@ -1306,7 +1039,7 @@ Test verify on acasxu
x0 >= 55947.6909999999988940544426441192626953125
x3 >= 1145.0
x4 <= 60.0
- +y1 -y0 >= 0
+ +y0 -y1 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
@@ -1325,7 +1058,7 @@ Test verify on acasxu
x5 >= 55947.6909999999988940544426441192626953125
x8 >= 1145.0
x9 <= 60.0
- +y0 -y1 >= 0
+ +y1 -y0 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
@@ -1344,7 +1077,7 @@ Test verify on acasxu
x5 >= 55947.6909999999988940544426441192626953125
x8 >= 1145.0
x9 <= 60.0
- +y1 -y0 >= 0
+ +y0 -y1 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
@@ -1412,50 +1145,6 @@ Test verify on acasxu
x5 <= 0.375
y0 >= 0.0
- [DEBUG]{ProverSpec} Prover-tailored specification:
- x0 >= -0.328421367053318091766556108268559910356998443603515625
- x0 <= 0.67985927880386987087746319957659579813480377197265625
- x1 >= -0.499999999999967081887319864108576439321041107177734375
- x1 <= 0.499999999999967081887319864108576439321041107177734375
- x2 >= -0.499999999999967081887319864108576439321041107177734375
- x2 <= 0.499999999999967081887319864108576439321041107177734375
- x3 >= -0.5
- x3 <= 0.5
- x4 >= -0.5
- x4 <= 0.5
- x0 >= 0.60000151009774149724051994780893437564373016357421875
- x3 >= 0.450000000000000011102230246251565404236316680908203125
- x4 <= -0.450000000000000011102230246251565404236316680908203125
- y0 >= 3.991125645861615112153231166303157806396484375
-
- [DEBUG]{ProverSpec} Prover-tailored specification:
- x0 >= -0.328421367053318091766556108268559910356998443603515625
- x0 <= 0.67985927880386987087746319957659579813480377197265625
- x1 >= -0.499999999999967081887319864108576439321041107177734375
- x1 <= 0.499999999999967081887319864108576439321041107177734375
- x2 >= -0.499999999999967081887319864108576439321041107177734375
- x2 <= 0.499999999999967081887319864108576439321041107177734375
- x3 >= -0.5
- x3 <= 0.5
- x4 >= -0.5
- x4 <= 0.5
- x0 >= -0.303529646039727207806890874053351581096649169921875
- x0 <= -0.298551301837009008810497334707179106771945953369140625
- x1 >= -0.0095492965855130916563719978285007528029382228851318359375
- x1 <= 0.0095492965855130916563719978285007528029382228851318359375
- x2 >= 0.493380323584843072382000173092819750308990478515625
- x3 >= 0.299999999999999988897769753748434595763683319091796875
- x4 >= 0.299999999999999988897769753748434595763683319091796875
- +y0 -y1 <= 0
- +y0 -y2 <= 0
- +y0 -y3 <= 0
- +y0 -y4 <= 0
-
- Goal runP1'vc: Unknown ()
- Goal runP1v2'vc: Unknown ()
- Goal run2'vc: Unknown ()
- Goal run2v2'vc: Unknown ()
- Goal run3'vc: Unknown ()
- Goal robust_output'vc: Unknown ()
- Goal P1: Unknown ()
- Goal P3: Unknown ()
+ [ERROR]{NN-Gen} No parsed NN './TestNetwork.nnet': Cannot read protobuf
+ Unrecoverable error: please report the issue at
+ https://git.frama-c.com/pub/caisar/issues
diff --git a/tests/acasxu_ci.t b/tests/acasxu_ci.t
index b9b6cb3c669275ed2e370bf90f2a2fa7fe903e62..fb37f1d0e568eb018bf0570570125d23e43fbc26 100644
--- a/tests/acasxu_ci.t
+++ b/tests/acasxu_ci.t
@@ -325,7 +325,7 @@ Test verify on acasxu
55947.6909999999988940544426441192626953125 <= x0
1145.0 <= x3
x4 <= 60.0
- y0 <= y1 and y1 <= y0
+ y1 <= y0 and y0 <= y1
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run3'vc':
forall x:t, x1:t, x2:t, x3:t, x4:t, eps:t.
@@ -650,15 +650,15 @@ Test verify on acasxu
(assert (>= X_3 1145.0))
(assert (<= X_4 60.0))
- ;; Y_1
- (declare-const Y_1 Real)
-
;; Y_0
(declare-const Y_0 Real)
+ ;; Y_1
+ (declare-const Y_1 Real)
+
;; Goal run2'vc
- (assert (or (and (>= Y_0 Y_1))
- (and (>= Y_1 Y_0))
+ (assert (or (and (>= Y_1 Y_0))
+ (and (>= Y_0 Y_1))
))
[DEBUG]{ProverSpec} Prover-tailored specification:
@@ -847,7 +847,7 @@ Test verify on acasxu
x0 >= 55947.6909999999988940544426441192626953125
x3 >= 1145.0
x4 <= 60.0
- +y0 -y1 >= 0
+ +y1 -y0 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
@@ -863,7 +863,7 @@ Test verify on acasxu
x0 >= 55947.6909999999988940544426441192626953125
x3 >= 1145.0
x4 <= 60.0
- +y1 -y0 >= 0
+ +y0 -y1 >= 0
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0