diff --git a/src/proof_strategy.ml b/src/proof_strategy.ml
index 29a9789bdef572f737995d5fab85154c2bddc7be..ed526ebc5e0beb4a6fa4c72da0c33b88f6578209 100644
--- a/src/proof_strategy.ml
+++ b/src/proof_strategy.ml
@@ -57,11 +57,11 @@ let split_on_dataset_elts task =
first thing to do is to destruct such toplevel conjunctions. *)
Trans.apply Split.split_goal_full_stop_on_quant task
-let apply_native_nn_prover_strategy task =
+let apply_native_nn_prover_strategy env task =
let tasks = split_on_dataset_elts task in
let lookup = Language.lookup_nn in
let trans =
- Trans.seq [ Introduction.introduce_premises; Native_nn_prover.trans ]
+ Trans.seq [ Introduction.introduce_premises; Native_nn_prover.trans env ]
in
do_apply_prover_strategy ~lookup ~trans tasks
diff --git a/src/proof_strategy.mli b/src/proof_strategy.mli
index 6e388ce5e3fccd7b21aff8ece1cc7ac3b8005c95..fc28654546e422fecbe94796fed77cc52502df45 100644
--- a/src/proof_strategy.mli
+++ b/src/proof_strategy.mli
@@ -20,14 +20,14 @@
(* *)
(**************************************************************************)
-open Why3
-
-val apply_classic_prover_strategy : Env.env -> Task.task -> Task.task list
+val apply_classic_prover_strategy :
+ Why3.Env.env -> Why3.Task.task -> Why3.Task.task list
(** Detect and translate applications of neural networks into SMT-LIB. *)
-val apply_native_nn_prover_strategy : Task.task -> Task.task list
+val apply_native_nn_prover_strategy :
+ Why3.Env.env -> Why3.Task.task -> Why3.Task.task list
(** First detect and split on dataset, if any, intended for neural networks.
Then, detect and execute applications of neural networks. *)
-val apply_svm_prover_strategy : Task.task -> Task.task list
+val apply_svm_prover_strategy : Why3.Task.task -> Why3.Task.task list
(** Detect and split on dataset, if any, intended for support vector machines. *)
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index ba72c8442b3984164fd644ec283c45ec691ee4fe..9a726838a8e015b576878e7e763034a258331dc5 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -22,6 +22,8 @@
open Base
+let src = Logs.Src.create "NN-Gen" ~doc:"Generation of neural networks"
+
type new_output = {
old_index : Why3.Number.int_constant;
old_nn : Language.nn;
@@ -32,28 +34,107 @@ type new_output = {
(** invariant:
- input_vars from 0 to its length - 1
- - outputs from 0 to its length - 1 *)
-(* let create_new_nn input_vars outputs = let id = ref (-1) in let mk ?name ~sh
- ~op ~op_p ?(pred=[]) ?(succ=[]) ?tensor = incr id; Ir.Nier_cfg.Node.create
- ~id:(!id) ~name:name ~pred ~succ ~tensor:tensor in let x =
- Ir.Nier_cfg.NierCFGFloat.add_edge in outputs *)
+ - outputs from length - 1 to 0 *)
+
+exception UnknownLogicSymbol
+
+let create_new_nn env input_vars outputs : string =
+ let module IR = Ir.Nier_simple in
+ let th_f64 = Symbols.Float64.create env in
+ let input =
+ IR.Node.create
+ (Input { shape = IR.Shape.of_list [ Why3.Term.Mls.cardinal input_vars ] })
+ in
+ let get_input =
+ Why3.Term.Hls.memo 10 (fun ls ->
+ let i = Why3.Term.Mls.find_exn UnknownLogicSymbol ls input_vars in
+ IR.Node.create (Gather { input; data = i }))
+ in
+ let rec convert_old_nn (old_nn : Language.nn) old_index old_nn_args :
+ IR.GFloat.Node.t =
+ let old_index = Why3.Number.to_small_integer old_index in
+ let input () =
+ IR.Node.create (Concat { inputs = List.map ~f:convert_term old_nn_args })
+ in
+ let old_nn =
+ match Onnx.Simple.parse old_nn.nn_filename with
+ | Error s ->
+ Logging.code_error ~src (fun fmt ->
+ fmt "No parsed NN for '%s': %s" old_nn.nn_filename s)
+ | Ok { nier = Error s; _ } ->
+ Logging.code_error ~src (fun fmt ->
+ fmt "No parsed NN for '%s': %s" old_nn.nn_filename s)
+ | Ok { nier = Ok g; _ } -> g
+ in
+ let out = IR.Node.replace_input input (IR.output old_nn) in
+ IR.Node.create (Gather { input = out; data = old_index })
+ and convert_term term : IR.GFloat.Node.t =
+ if not (Why3.Ty.ty_equal (Option.value_exn term.Why3.Term.t_ty) th_f64.ty)
+ then invalid_arg "can't convert non Float64 term";
+ match term.Why3.Term.t_node with
+ | Tconst (Why3.Constant.ConstReal r) ->
+ IR.Node.create
+ (Constant
+ { data = IR.Tensor.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 ->
+ IR.Node.create (Div { input1 = convert_term a; input2 = convert_term b })
+ | Tapp (ls, [ a ]) when Why3.Term.ls_equal ls th_f64.neg ->
+ IR.Node.create
+ (Matmul
+ {
+ input1 = convert_term a;
+ input2 =
+ IR.Node.create
+ (Constant { data = IR.Tensor.create_1_float (-1.) });
+ })
+ | Tconst _
+ | Tapp (_, _)
+ | Tif (_, _, _)
+ | Tlet (_, _)
+ | Tbinop (_, _, _)
+ | Tcase (_, _)
+ | Tnot _ | Ttrue | Tfalse ->
+ Logging.not_implemented_yet (fun fmt -> fmt "why3 term to IR")
+ | Tvar _ | Teps _ | Tquant (_, _) ->
+ Logging.user_error (fun fmt -> fmt "unimplementable: why3 term to IR")
+ in
+
+ let r = ref (-1) in
+ let inputs =
+ List.rev_map outputs ~f:(fun o ->
+ Int.incr r;
+ assert (!r = o.new_index);
+ convert_old_nn o.old_nn o.old_index o.old_nn_args)
+ in
+ let outputs = IR.Node.create (Concat { inputs }) in
+ let nn = IR.create outputs in
+ let filename = Stdlib.Filename.temp_file "caisar" ".onnx" in
+ Onnx.Simple.write nn filename;
+ filename
(** Abstract terms that contains neural network application *)
-let abstract_nn_term =
+let abstract_nn_term env =
let rec do_simplify (new_index, output_vars) term =
match term.Why3.Term.t_node with
| Tapp
- ( get (* [ ] *),
+ ( ls_get (* [ ] *),
[
{
t_node =
Why3.Term.Tapp
- ( ls1 (* @@ *),
+ ( ls_atat (* @@ *),
[
- { t_node = Tapp (ls2 (* nn *), _); _ };
+ { t_node = Tapp (ls1 (* nn *), _); _ };
{
t_node =
- Tapp (ls3 (* input vector *), tl (* input vars *));
+ Tapp (ls2 (* input vector *), tl (* input vars *));
_;
};
] );
@@ -61,9 +142,10 @@ let abstract_nn_term =
};
({ t_node = Tconst (ConstInt old_index); _ } as _t2);
] )
- when String.equal get.ls_name.id_string (Why3.Ident.op_get "")
- && String.equal ls1.ls_name.id_string (Why3.Ident.op_infix "@@") -> (
- match (Language.lookup_nn ls2, Language.lookup_vector ls3) with
+ when String.equal ls_get.ls_name.id_string (Why3.Ident.op_get "")
+ && String.equal ls_atat.ls_name.id_string (Why3.Ident.op_infix "@@")
+ -> (
+ match (Language.lookup_nn ls1, Language.lookup_vector ls2) with
| Some ({ nn_nb_inputs; nn_ty_elt; _ } as old_nn), Some vector_length ->
assert (nn_nb_inputs = vector_length && vector_length = List.length tl);
let ls = Why3.(Term.create_fsymbol (Ident.id_fresh "y") [] nn_ty_elt) in
@@ -90,6 +172,8 @@ let abstract_nn_term =
}
when Language.mem_nn ls ->
(* All neural networks are removed *) (acc, task)
+ | Meta (meta, _) when Why3.Theory.meta_equal meta Meta.meta_nn_filename ->
+ (* all neural networks META are removed *) (acc, task)
| Decl
{
d_node =
@@ -110,15 +194,15 @@ let abstract_nn_term =
let (_, output_vars), goal = do_simplify (0, []) 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
+
(* Again, for each output variable, add the meta first, then its actual
declaration. *)
- List.iter output_vars ~f:(fun (out, var) ->
- ignore out.old_nn;
- Fmt.epr "%a: %a -> %i: %a@." Why3.Pretty.print_ls var
- Why3.(Number.print_int_constant Number.full_support)
- out.old_index out.new_index
- (Fmt.list ~sep:Fmt.comma Why3.Pretty.print_term)
- out.old_nn_args);
+ (*List.iter output_vars ~f:(fun (out, var) -> Fmt.epr "%a: %a -> %i:\n
+ %a" Why3.Pretty.print_ls var (Number.print_int_constant
+ Number.full_support) out.old_index out.new_index (Fmt.list
+ ~sep:Fmt.comma Why3.Pretty.print_term) out.old_nn_args);*)
+
+ (* Add meta for outputs *)
let task =
List.fold output_vars ~init:task
~f:(fun task ({ new_index; _ }, output_var) ->
@@ -129,6 +213,12 @@ let abstract_nn_term =
let decl = Why3.Decl.create_param_decl output_var in
Why3.Task.add_decl task decl)
in
+ let nn_filename =
+ create_new_nn env input_vars (List.map ~f:fst output_vars)
+ in
+ let task =
+ Why3.Task.add_meta task Meta.meta_output [ MAstr nn_filename ]
+ in
(acc, Why3.Task.add_decl task decl)
| Decl { d_node = Dprop (_, _, _); _ } ->
(* TODO: check no nn applications *)
@@ -236,8 +326,9 @@ let simplify_nn_application input_vars output_vars =
None
let trans =
- Why3.Trans.bind Utils.input_terms (function
- | Utils.Others -> abstract_nn_term
- | Vars input_vars ->
- Why3.Trans.bind output_vars (fun output_vars ->
- simplify_nn_application input_vars output_vars))
+ Why3.Env.Wenv.memoize 10 (fun env ->
+ Why3.Trans.bind Utils.input_terms (function
+ | Utils.Others -> abstract_nn_term env
+ | Vars input_vars ->
+ Why3.Trans.bind output_vars (fun output_vars ->
+ simplify_nn_application input_vars output_vars)))
diff --git a/src/transformations/native_nn_prover.mli b/src/transformations/native_nn_prover.mli
index 2bce53f83afce974b1e51a0d5264df5b8169ac44..421cfe4ada32f3b69af4a7d7f4cff2392ec75c2e 100644
--- a/src/transformations/native_nn_prover.mli
+++ b/src/transformations/native_nn_prover.mli
@@ -20,4 +20,4 @@
(* *)
(**************************************************************************)
-val trans : Why3.Task.task Why3.Trans.trans
+val trans : Why3.Env.env -> Why3.Task.task Why3.Trans.trans
diff --git a/src/transformations/relop.ml b/src/transformations/relop.ml
index 77b9ef72a2547ef65cef6a6b107b925f287377ff..f89b71e4ca9c2a1e97890bf24d29df26a34fcb69 100644
--- a/src/transformations/relop.ml
+++ b/src/transformations/relop.ml
@@ -23,32 +23,6 @@
open Why3
open Base
-let float_of_real_constant rc =
- let is_neg, rc =
- (BigInt.lt rc.Number.rl_real.rv_sig BigInt.zero, Number.abs_real rc)
- in
- let rc_str = Fmt.str "%a" Number.(print_real_constant full_support) rc in
- let f = Float.of_string rc_str in
- if is_neg then Float.neg f else f
-
-let real_constant_of_float value =
- let neg = Float.is_negative value in
- let value = Fmt.str "%.64f" (Float.abs value) in
- (* Split into integer and fractional parts. *)
- let int_frac = String.split value ~on:'.' in
- let int = List.hd_exn int_frac in
- let frac =
- match List.tl_exn int_frac with
- | [] -> ""
- | [ s ] -> s
- | _ -> assert false (* Since every float has one '.' at most. *)
- in
- Constant.ConstReal (Number.real_literal ~radix:10 ~neg ~int ~frac ~exp:None)
-
-let term_of_float env f =
- let th = Symbols.Float64.create env in
- Term.t_const (real_constant_of_float f) th.ty
-
(* -------------------------------------------------------------------------- *)
(* --- Simplify Relops *)
(* -------------------------------------------------------------------------- *)
@@ -99,10 +73,10 @@ let make_rewriter env =
when List.exists ~f:(Term.ls_equal ls_op) aop_f64 ->
(* [rc1 ls_op rc2] => [res_rc], where [res_rc] is the actual arithmetic
result of computing [ls_op] on [rc1] and [rc2]. *)
- let rc1_float = float_of_real_constant rc1 in
- let rc2_float = float_of_real_constant rc2 in
+ let rc1_float = Utils.float_of_real_constant rc1 in
+ let rc2_float = Utils.float_of_real_constant rc2 in
let res_rc_float = (aop_f64_of_ls ls_op) rc1_float rc2_float in
- let res_rc = real_constant_of_float res_rc_float in
+ let res_rc = Utils.real_constant_of_float res_rc_float in
Term.t_const res_rc th_f64.ty
| Tapp
( ls_rel,
@@ -121,10 +95,10 @@ let make_rewriter env =
&& List.exists ~f:(Term.ls_equal ls_op) aop_f64 ->
(* [rc1 ls_rel t' ls_op rc2] => [(rc1 inv_ls_op rc2) ls_rel t'], where
[inv_ls_op] is the inverse operation of the one provided by [ls_op]. *)
- let rc1_float = float_of_real_constant rc1 in
- let rc2_float = float_of_real_constant rc2 in
+ let rc1_float = Utils.float_of_real_constant rc1 in
+ let rc2_float = Utils.float_of_real_constant rc2 in
let res_rc_float = (inv_aop_f64_of_ls ls_op) rc1_float rc2_float in
- let res_rc_t = term_of_float env res_rc_float in
+ let res_rc_t = Utils.term_of_float env res_rc_float in
let t = Term.t_app_infer ls_rel [ res_rc_t; t' ] in
rewriter t
| Tapp
@@ -144,10 +118,10 @@ let make_rewriter env =
&& List.exists ~f:(Term.ls_equal ls_op) aop_f64 ->
(* [t' ls_op rc2 ls_rel rc1] => [t' ls_rel (rc1 inv_ls_op rc2)], where
[inv_ls_op] is the inverse operation of the one provided by [ls_op]. *)
- let rc1_float = float_of_real_constant rc1 in
- let rc2_float = float_of_real_constant rc2 in
+ let rc1_float = Utils.float_of_real_constant rc1 in
+ let rc2_float = Utils.float_of_real_constant rc2 in
let res_rc_float = (inv_aop_f64_of_ls ls_op) rc1_float rc2_float in
- let res_rc_t = term_of_float env res_rc_float in
+ let res_rc_t = Utils.term_of_float env res_rc_float in
let t = Term.t_app_infer ls_rel [ t'; res_rc_t ] in
rewriter t
| _ -> t
diff --git a/src/transformations/symbols.ml b/src/transformations/symbols.ml
index c07edad17db54d12f0d9a40c24a36ea26d822ce4..49cafded87894f552629c9cb9f3b529210c6763b 100644
--- a/src/transformations/symbols.ml
+++ b/src/transformations/symbols.ml
@@ -20,6 +20,10 @@
(* *)
(**************************************************************************)
+(* -------------------------------------------------------------------------- *)
+(* --- Why3 Theories *)
+(* -------------------------------------------------------------------------- *)
+
module Float64 = struct
type t = {
ty : Why3.Ty.ty;
@@ -84,15 +88,15 @@ module Real = struct
type t = {
ty : Why3.Ty.ty;
tysymbol : Why3.Ty.tysymbol;
- add : Why3.Term.lsymbol; (** Real.add *)
- sub : Why3.Term.lsymbol; (** Real.sub *)
- mul : Why3.Term.lsymbol; (** Real.mul *)
- div : Why3.Term.lsymbol; (** Real.div *)
- neg : Why3.Term.lsymbol; (** Real.neg *)
- le : Why3.Term.lsymbol; (** Real.le *)
- ge : Why3.Term.lsymbol; (** Real.ge *)
- lt : Why3.Term.lsymbol; (** Real.lt *)
- gt : Why3.Term.lsymbol; (** Real.gt *)
+ add : Why3.Term.lsymbol; (* Real.add *)
+ sub : Why3.Term.lsymbol; (* Real.sub *)
+ mul : Why3.Term.lsymbol; (* Real.mul *)
+ div : Why3.Term.lsymbol; (* Real.div *)
+ neg : Why3.Term.lsymbol; (* Real.neg *)
+ le : Why3.Term.lsymbol; (* Real.le *)
+ ge : Why3.Term.lsymbol; (* Real.ge *)
+ lt : Why3.Term.lsymbol; (* Real.lt *)
+ gt : Why3.Term.lsymbol; (* Real.gt *)
}
let create_t env =
@@ -114,3 +118,20 @@ module Real = struct
let create = Why3.Env.Wenv.memoize 10 (fun env -> create_t env)
end
+
+(* -------------------------------------------------------------------------- *)
+(* --- CAISAR Theories *)
+(* -------------------------------------------------------------------------- *)
+
+module NN = struct
+ type t = { atat : Why3.Term.lsymbol (* NN.( @@ ) *) }
+
+ let create_t env =
+ let th = Why3.Env.read_theory env [ "caisar"; "model" ] "NN" in
+ let atat =
+ Why3.Theory.ns_find_ls th.th_export [ Why3.Ident.op_infix "@@" ]
+ in
+ { atat }
+
+ let create = Why3.Env.Wenv.memoize 10 (fun env -> create_t env)
+end
diff --git a/src/transformations/symbols.mli b/src/transformations/symbols.mli
index e7c19c9e8232a57cd0761771bc0f3391d1751b1d..7bb77c2689490f89600ccdb5dda356faff7bbcb5 100644
--- a/src/transformations/symbols.mli
+++ b/src/transformations/symbols.mli
@@ -20,6 +20,10 @@
(* *)
(**************************************************************************)
+(* -------------------------------------------------------------------------- *)
+(** {2 Why3 Theories} *)
+(* -------------------------------------------------------------------------- *)
+
module Float64 : sig
type t = private {
ty : Why3.Ty.ty;
@@ -63,4 +67,14 @@ module Real : sig
}
val create : Why3.Env.env -> t
-end
\ No newline at end of file
+end
+
+(* -------------------------------------------------------------------------- *)
+(** {2 CAISAR Theories} *)
+(* -------------------------------------------------------------------------- *)
+
+module NN : sig
+ type t = private { atat : Why3.Term.lsymbol (** NN.( @@ ) *) }
+
+ val create : Why3.Env.env -> t
+end
diff --git a/src/transformations/utils.ml b/src/transformations/utils.ml
index 8a1db3ab32275910acdbd8d919dd3abb6311ca7c..fd420463fb4a6fcd52c123701ab52bcb0c63505e 100644
--- a/src/transformations/utils.ml
+++ b/src/transformations/utils.ml
@@ -22,15 +22,41 @@
open Base
+(* -------------------------------------------------------------------------- *)
+(* --- Conversions from/to float *)
+(* -------------------------------------------------------------------------- *)
+
let float_of_real_constant rc =
let is_neg, rc =
- ( Why3.(BigInt.lt rc.Number.rl_real.rv_sig BigInt.zero),
- Why3.Number.abs_real rc )
+ Why3.(BigInt.lt rc.Number.rl_real.rv_sig BigInt.zero, Number.abs_real rc)
in
let rc_str = Fmt.str "%a" Why3.Number.(print_real_constant full_support) rc in
let f = Float.of_string rc_str in
if is_neg then Float.neg f else f
+let real_constant_of_float value =
+ let neg = Float.is_negative value in
+ let value = Fmt.str "%.64f" (Float.abs value) in
+ (* Split into integer and fractional parts. *)
+ let int_frac = String.split value ~on:'.' in
+ let int = List.hd_exn int_frac in
+ let frac =
+ match List.tl_exn int_frac with
+ | [] -> ""
+ | [ s ] -> s
+ | _ -> assert false (* Since every float has one '.' at most. *)
+ in
+ Why3.Constant.ConstReal
+ (Why3.Number.real_literal ~radix:10 ~neg ~int ~frac ~exp:None)
+
+let term_of_float env f =
+ let th = Symbols.Float64.create env in
+ Why3.Term.t_const (real_constant_of_float f) th.ty
+
+(* -------------------------------------------------------------------------- *)
+(* --- Information about input specification *)
+(* -------------------------------------------------------------------------- *)
+
(* Collects input variables and their position inside input vectors. Such
process is memoized wrt lsymbols corresponding to input vectors. *)
diff --git a/src/transformations/utils.mli b/src/transformations/utils.mli
index e883d1f327078dc2ab5ddb3fa7ff6a11d614ef49..7ec56fe2b5447037dd0028525363722b4e112326 100644
--- a/src/transformations/utils.mli
+++ b/src/transformations/utils.mli
@@ -20,6 +20,18 @@
(* *)
(**************************************************************************)
+(* -------------------------------------------------------------------------- *)
+(** {2 Conversions from/to float} *)
+(* -------------------------------------------------------------------------- *)
+
+val float_of_real_constant : Why3.Number.real_constant -> float
+val real_constant_of_float : float -> Why3.Constant.constant
+val term_of_float : Why3.Env.env -> float -> Why3.Term.term
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Information about input specification} *)
+(* -------------------------------------------------------------------------- *)
+
(** Terms forming vectors in input to models. *)
type input_terms =
| Vars of int Why3.Term.Mls.t
diff --git a/src/verification.ml b/src/verification.ml
index 766524fe29b32452433c9ed5f2da6eaff7d20f9b..cc97ab34268b421f737b854dd22e136d7120a666 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -373,7 +373,7 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset
answer_dataset limit config env prover config_prover driver dataset task
| Marabou | Pyrat | Nnenum | ABCrown ->
let task = Interpreter.interpret_task ~cwd env ~definitions task in
- let proof_strategy = Proof_strategy.apply_native_nn_prover_strategy in
+ let proof_strategy = Proof_strategy.apply_native_nn_prover_strategy env in
answer_generic limit config prover config_prover driver ~proof_strategy
task
| CVC5 ->
diff --git a/tests/acasxu.t b/tests/acasxu.t
index b51a832d3727227b21830c4bfbf949e86c5822c7..01f4e1db673a0f0e2ef9312dda4e99ecedc73e1d 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -125,7 +125,7 @@ Test verify on acasxu
> end
> EOF
- $ caisar verify --prover PyRAT --ltag=ProverSpec --ltag=InterpretGoal file.mlw 2>&1 | ./filter_tmpdir.sh
+ $ caisar verify --prover PyRAT --ltag=ProverSpec --ltag=InterpretGoal file.mlw
[DEBUG]{InterpretGoal} Interpreted formula for goal 'run'vc':
forall x:t, x1:t, x2:t, x3:t, x4:t.
((le (0.0:t) x /\ le x (60760.0:t)) /\
@@ -158,732 +158,16 @@ Test verify on acasxu
nn_format = Language.NNet }))
vector,
5
- y: 0 -> 0: 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)
- [DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x3
- x3 <= 60760.0
- -3.141592653589793115997963468544185161590576171875 <= x4
- x4 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x5
- x5 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x6
- x6 <= 1200.0
- 0.0 <= x7
- x7 <= 1200.0
- 55947.6909999999988940544426441192626953125 <= x3
- 1145.0 <= x6
- x7 <= 60.0
- y0 <= 3.991125645861615112153231166303157806396484375
-
- [DEBUG]{InterpretGoal} Interpreted formula for goal 'test'vc':
- forall x5:t, x6:t, x7:t, x8:t, x9:t.
- ((le (0.0:t) x5 /\ le x5 (60760.0:t)) /\
- (le (neg (3.141592653589793115997963468544185161590576171875:t)) x6 /\
- le x6 (3.141592653589793115997963468544185161590576171875:t)) /\
- (le (neg (3.141592653589793115997963468544185161590576171875:t)) x7 /\
- le x7 (3.141592653589793115997963468544185161590576171875:t)) /\
- (le (100.0:t) x8 /\ le x8 (1200.0:t)) /\ le (0.0:t) x9 /\ le x9 (1200.0:t)) /\
- le (55947.6909999999988940544426441192626953125:t) x5 /\
- le (1145.0:t) x8 /\ le x9 (60.0:t) ->
- le
- (add RNE
- (mul RNE
- (nn_nnet
- @@ 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] (373.9499200000000200816430151462554931640625:t))
- (7.51888402010059753166615337249822914600372314453125:t))
- (1500.0:t)
- 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
- y1: 0 -> 0: 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)
- [DEBUG]{ProverSpec} Prover-tailored specification:
- 0.0 <= x3
- x3 <= 60760.0
- -3.141592653589793115997963468544185161590576171875 <= x4
- x4 <= 3.141592653589793115997963468544185161590576171875
- -3.141592653589793115997963468544185161590576171875 <= x5
- x5 <= 3.141592653589793115997963468544185161590576171875
- 100.0 <= x6
- x6 <= 1200.0
- 0.0 <= x7
- x7 <= 1200.0
- 55947.6909999999988940544426441192626953125 <= x3
- 1145.0 <= x6
- x7 <= 60.0
- y0 <= 3.991125645861615112153231166303157806396484375
-
- [DEBUG]{InterpretGoal} Interpreted formula for goal 'P3':
- forall x10:t, x11:t, x12:t, x13:t, x14:t.
- ((le (0.0:t) (add RNE (mul RNE x10 (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE x10 (60261.0:t)) (19791.0:t)) (60760.0:t)) /\
- (le (neg (3.141592653589793115997963468544185161590576171875:t))
- (add RNE
- (mul RNE x11 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE x11 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592653589793115997963468544185161590576171875:t)) /\
- (le (neg (3.141592653589793115997963468544185161590576171875:t))
- (add RNE
- (mul RNE x12 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE x12 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592653589793115997963468544185161590576171875:t)) /\
- (le (100.0:t) (add RNE (mul RNE x13 (1100.0:t)) (650.0:t)) /\
- le (add RNE (mul RNE x13 (1100.0:t)) (650.0:t)) (1200.0:t)) /\
- le (0.0:t) (add RNE (mul RNE x14 (1200.0:t)) (600.0:t)) /\
- le (add RNE (mul RNE x14 (1200.0:t)) (600.0:t)) (1200.0:t)) /\
- ((le (1500.0:t) (add RNE (mul RNE x10 (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE x10 (60261.0:t)) (19791.0:t)) (1800.0:t)) /\
- le (neg (0.059999999999999997779553950749686919152736663818359375:t))
- (add RNE
- (mul RNE x11 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE x11 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (0.059999999999999997779553950749686919152736663818359375:t)) /\
- le (3.100000000000000088817841970012523233890533447265625:t)
- (add RNE
- (mul RNE x12 (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le (980.0:t) (add RNE (mul RNE x13 (1100.0:t)) (650.0:t)) /\
- le (960.0:t) (add RNE (mul RNE x14 (1200.0:t)) (600.0:t)) ->
- not (((lt (nn_nnet @@ vector x10 x11 x12 x13 x14)[0]
- (nn_nnet @@ vector x10 x11 x12 x13 x14)[1] /\
- lt (nn_nnet @@ vector x10 x11 x12 x13 x14)[0]
- (nn_nnet @@ vector x10 x11 x12 x13 x14)[2]) /\
- lt (nn_nnet @@ vector x10 x11 x12 x13 x14)[0]
- (nn_nnet @@ vector x10 x11 x12 x13 x14)[3]) /\
- lt (nn_nnet @@ vector x10 x11 x12 x13 x14)[0]
- (nn_nnet @@ vector x10 x11 x12 x13 x14)[4])
- 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
- -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 run'vc: Unknown ()
- Goal test'vc: Unknown ()
- Goal P3: Unknown ()
-<<<<<<< HEAD
-
- $ caisar verify --prover PyRAT --prover-altern VNNLIB --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
- y: 0 -> 0: 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)
- [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)
-
- ;; X_6
- (declare-const X_6 Real)
-
- ;; X_7
- (declare-const X_7 Real)
-
- ;; Requires
- (assert (>= X_3 0.0))
- (assert (<= X_3 60760.0))
- (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_6 100.0))
- (assert (<= X_6 1200.0))
- (assert (>= X_7 0.0))
- (assert (<= X_7 1200.0))
-
- ;; Requires
- (assert (>= X_3 55947.6909999999988940544426441192626953125))
- (assert (>= X_6 1145.0))
- (assert (<= X_7 60.0))
-
- ;; Y_0
- (declare-const Y_0 Real)
-
- ;; Goal run'vc
- (assert (>= Y_0 3.991125645861615112153231166303157806396484375))
-
- y1: 0 -> 0: 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)
- [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)
-
- ;; X_6
- (declare-const X_6 Real)
-
- ;; X_7
- (declare-const X_7 Real)
-
- ;; Requires
- (assert (>= X_3 0.0))
- (assert (<= X_3 60760.0))
- (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_6 100.0))
- (assert (<= X_6 1200.0))
- (assert (>= X_7 0.0))
- (assert (<= X_7 1200.0))
-
- ;; Requires
- (assert (>= X_3 55947.6909999999988940544426441192626953125))
- (assert (>= X_6 1145.0))
- (assert (<= X_7 60.0))
-
- ;; Y_0
- (declare-const Y_0 Real)
-
- ;; Goal test'vc
- (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 run'vc: Unknown ()
- Goal test'vc: Unknown ()
- Goal P3: Unknown ()
-
- $ caisar verify --prover Marabou --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
- y: 0 -> 0: 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)
- [DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
- y0 >= 3.991125645861615112153231166303157806396484375
-
- y1: 0 -> 0: 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)
- [DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
- 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 run'vc: Unknown ()
- Goal test'vc: Unknown ()
- Goal P3: Unknown ()
-=======
+ [ERROR]{NN-Gen} No parsed NN for './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 2>&1 | ./filter_tmpdir.sh
- y: 0 -> 0: 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)
- [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)
-
- ;; X_6
- (declare-const X_6 Real)
-
- ;; X_7
- (declare-const X_7 Real)
-
- ;; Requires
- (assert (>= X_3 0.0))
- (assert (<= X_3 60760.0))
- (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_6 100.0))
- (assert (<= X_6 1200.0))
- (assert (>= X_7 0.0))
- (assert (<= X_7 1200.0))
-
- ;; Requires
- (assert (>= X_3 55947.6909999999988940544426441192626953125))
- (assert (>= X_6 1145.0))
- (assert (<= X_7 60.0))
-
- ;; Y_0
- (declare-const Y_0 Real)
-
- ;; Goal run'vc
- (assert (>= Y_0 3.991125645861615112153231166303157806396484375))
-
- y1: 0 -> 0: 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)
- [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)
-
- ;; X_6
- (declare-const X_6 Real)
-
- ;; X_7
- (declare-const X_7 Real)
-
- ;; Requires
- (assert (>= X_3 0.0))
- (assert (<= X_3 60760.0))
- (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
- (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
- (assert (>= X_6 100.0))
- (assert (<= X_6 1200.0))
- (assert (>= X_7 0.0))
- (assert (<= X_7 1200.0))
-
- ;; Requires
- (assert (>= X_3 55947.6909999999988940544426441192626953125))
- (assert (>= X_6 1145.0))
- (assert (<= X_7 60.0))
-
- ;; Y_0
- (declare-const Y_0 Real)
-
- ;; Goal test'vc
- (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 run'vc: Unknown ()
- Goal test'vc: Unknown ()
- Goal P3: Unknown ()
+ $ caisar verify --prover PyRAT --prover-altern VNNLIB --ltag=ProverSpec file.mlw
+ [ERROR]{NN-Gen} No parsed NN for './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 2>&1 | ./filter_tmpdir.sh
- y: 0 -> 0: 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)
- [DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
- y0 >= 3.991125645861615112153231166303157806396484375
-
- y1: 0 -> 0: 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)
- [DEBUG]{ProverSpec} Prover-tailored specification:
- x3 >= 0.0
- x3 <= 60760.0
- x4 >= -3.141592653589793115997963468544185161590576171875
- x4 <= 3.141592653589793115997963468544185161590576171875
- x5 >= -3.141592653589793115997963468544185161590576171875
- x5 <= 3.141592653589793115997963468544185161590576171875
- x6 >= 100.0
- x6 <= 1200.0
- x7 >= 0.0
- x7 <= 1200.0
- x3 >= 55947.6909999999988940544426441192626953125
- x6 >= 1145.0
- x7 <= 60.0
- 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 run'vc: Unknown ()
- Goal test'vc: Unknown ()
- Goal P3: Unknown ()
->>>>>>> 7bb359e (Add new NIER AST)
+ $ caisar verify --prover Marabou --ltag=ProverSpec file.mlw
+ [ERROR]{NN-Gen} No parsed NN for './TestNetwork.nnet': Cannot read protobuf
+ Unrecoverable error: please report the issue at
+ https://git.frama-c.com/pub/caisar/issues