Skip to content
Snippets Groups Projects
Commit 2e3169a2 authored by Michele Alberti's avatar Michele Alberti
Browse files

[log] Rework logging API and tag names. Also update the doc.

parent 8a00455e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 79 additions and 70 deletions
doc/usage.rst
+ 3
− 2
View file @ 2e3169a2
...@@ -63,8 +63,9 @@ verbosity level allows logging with all tags enabled. To enable a particular ...@@ -63,8 +63,9 @@ verbosity level allows logging with all tags enabled. To enable a particular
tag, use the option ``--ltag=TAG``, with ``TAG`` one of the following: tag, use the option ``--ltag=TAG``, with ``TAG`` one of the following:
* ``Autodetect``: display the output of the autodetect routine of CAISAR described in :ref:`prover-registration` * ``Autodetect``: display the output of the autodetect routine of CAISAR described in :ref:`prover-registration`
* ``Specification``: display the actual specification provided to the prover * ``ProverSpec``: display the actual specification provided to the prover
* ``CallProver``: display the actual command used to call the prover * ``ProverCall``: display the actual command used to call the prover
* ``StackTrace``: display the stack trace upon a CAISAR error
Built-in properties Built-in properties
------------------- -------------------
......
src/logging.ml
+ 8
− 2
View file @ 2e3169a2
...@@ -21,10 +21,16 @@ ...@@ -21,10 +21,16 @@
(**************************************************************************) (**************************************************************************)
let src_autodetect = Logs.Src.create "Autodetect" ~doc:"Prover autodetection" let src_autodetect = Logs.Src.create "Autodetect" ~doc:"Prover autodetection"
let src_spec = Logs.Src.create "Spec" ~doc:"Prover-tailored specification"
let src_call = Logs.Src.create "Call" ~doc:"Call prover" let src_prover_spec =
Logs.Src.create "ProverSpec" ~doc:"Prover-tailored specification"
let src_prover_call = Logs.Src.create "ProverCall" ~doc:"Prover call"
let src_stack_trace = Logs.Src.create "StackTrace" ~doc:"Print stack trace" let src_stack_trace = Logs.Src.create "StackTrace" ~doc:"Print stack trace"
let all_srcs () =
[ src_autodetect; src_prover_spec; src_prover_call; src_stack_trace ]
let is_debug_level src = let is_debug_level src =
match Logs.Src.level src with Some Debug -> true | _ -> false match Logs.Src.level src with Some Debug -> true | _ -> false
......
src/logging.mli
+ 10
− 7
View file @ 2e3169a2
...@@ -20,16 +20,19 @@ ...@@ -20,16 +20,19 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
(** {2 Debug Tags} *) (** {2 Sources} *)
val src_autodetect : Logs.src
val src_spec : Logs.src
val src_call : Logs.src
val src_autodetect : Logs.src
val src_prover_spec : Logs.src
val src_prover_call : Logs.src
val src_stack_trace : Logs.src val src_stack_trace : Logs.src
val all_srcs : unit -> Logs.src list
(** @return all available sources. *)
(** {2 Logs} *) (** {2 Logs} *)
val is_debug_level : Logs.src -> bool val is_debug_level : Logs.src -> bool
val setup : Fmt.style_renderer option -> Logs.level option -> Logs.src list -> unit
val setup :
Fmt.style_renderer option -> Logs.level option -> Logs.src list -> unit
src/main.ml
+ 1
− 1
View file @ 2e3169a2
...@@ -37,7 +37,7 @@ let () = ...@@ -37,7 +37,7 @@ let () =
(* -- Logs *) (* -- Logs *)
let log_tags = let log_tags =
let all_tags = Logs.Src.list () in let all_tags = Logging.all_srcs () in
let doc = let doc =
Fmt.str "Logging tags. Available $(docv)s: %s." Fmt.str "Logging tags. Available $(docv)s: %s."
(Arg.doc_alts (Arg.doc_alts
......
src/verification.ml
+ 2
− 3
View file @ 2e3169a2
...@@ -22,7 +22,6 @@ ...@@ -22,7 +22,6 @@
open Why3 open Why3
open Base open Base
module Filename = Caml.Filename
module File = struct module File = struct
type t = type t =
...@@ -164,7 +163,7 @@ let build_command config_prover ~nn_filename = ...@@ -164,7 +163,7 @@ let build_command config_prover ~nn_filename =
let log_prover_task driver task = let log_prover_task driver task =
let print fmt task = ignore (Driver.print_task_prepared driver fmt task) in let print fmt task = ignore (Driver.print_task_prepared driver fmt task) in
Logs.debug ~src:Logging.src_spec (fun m -> Logs.debug ~src:Logging.src_prover_spec (fun m ->
m "@[Prover-tailored specification:@.%a@]" print task) m "@[Prover-tailored specification:@.%a@]" print task)
let call_prover_on_task limit config command driver task = let call_prover_on_task limit config command driver task =
...@@ -302,7 +301,7 @@ let open_file ?format env file = ...@@ -302,7 +301,7 @@ let open_file ?format env file =
let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
file = file =
let debug = Logging.(is_debug_level src_call) in let debug = Logging.(is_debug_level src_prover_call) in
(if debug then Debug.(set_flag (lookup_flag "call_prover"))); (if debug then Debug.(set_flag (lookup_flag "call_prover")));
let env, config = create_env loadpath in let env, config = create_env loadpath in
let main = Whyconf.get_main config in let main = Whyconf.get_main config in
......
tests/cvc5.t
+ 2
− 2
View file @ 2e3169a2
...@@ -6,7 +6,7 @@ Test verify ...@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH $ PATH=$(pwd)/bin:$PATH
$ caisar verify -L . --format whyml --prover=CVC5 --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh $ caisar verify -L . --format whyml --prover=CVC5 --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory CVC5 > theory CVC5
> use TestNetworkONNX.AsTuple as TN > use TestNetworkONNX.AsTuple as TN
> use ieee_float.Float64 > use ieee_float.Float64
...@@ -17,7 +17,7 @@ Test verify ...@@ -17,7 +17,7 @@ Test verify
> (0.0:t) .< y1 .< (0.5:t) /\ (0.0:t) .< y2 .< (1.0:t) > (0.0:t) .< y1 .< (0.5:t) /\ (0.0:t) .< y2 .< (1.0:t)
> end > end
> EOF > EOF
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
;; produced by cvc5.drv ;; ;; produced by cvc5.drv ;;
(set-logic ALL) (set-logic ALL)
(set-info :smt-lib-version 2.6) (set-info :smt-lib-version 2.6)
......
tests/dataset.t
+ 22
− 22
View file @ 2e3169a2
...@@ -14,7 +14,7 @@ Test verify on dataset ...@@ -14,7 +14,7 @@ Test verify on dataset
$ PATH=$(pwd)/bin:$PATH $ PATH=$(pwd)/bin:$PATH
$ caisar verify -L . --format whyml --ltag=Spec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T > theory T
> use TestNetwork.AsArray as TN > use TestNetwork.AsArray as TN
> use ieee_float.Float64 > use ieee_float.Float64
...@@ -27,7 +27,7 @@ Test verify on dataset ...@@ -27,7 +27,7 @@ Test verify on dataset
> robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t) > robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
> end > end
> EOF > EOF
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver ;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver ;;; produced by VNN-LIB driver
;; X_0 ;; X_0
...@@ -99,7 +99,7 @@ Test verify on dataset ...@@ -99,7 +99,7 @@ Test verify on dataset
(and (>= Y_4 Y_1)) (and (>= Y_4 Y_1))
)) ))
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver ;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver ;;; produced by VNN-LIB driver
;; X_0 ;; X_0
...@@ -171,7 +171,7 @@ Test verify on dataset ...@@ -171,7 +171,7 @@ Test verify on dataset
(and (>= Y_4 Y_0)) (and (>= Y_4 Y_0))
)) ))
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver ;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver ;;; produced by VNN-LIB driver
;; X_0 ;; X_0
...@@ -243,7 +243,7 @@ Test verify on dataset ...@@ -243,7 +243,7 @@ Test verify on dataset
(and (>= Y_4 Y_1)) (and (>= Y_4 Y_1))
)) ))
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver ;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver ;;; produced by VNN-LIB driver
;; X_0 ;; X_0
...@@ -318,7 +318,7 @@ Test verify on dataset ...@@ -318,7 +318,7 @@ Test verify on dataset
Goal G: Unknown () Goal G: Unknown ()
Goal H: Unknown () Goal H: Unknown ()
$ caisar verify -L . --format whyml --ltag=Spec --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T > theory T
> use TestNetwork.AsArray as TN > use TestNetwork.AsArray as TN
> use ieee_float.Float64 > use ieee_float.Float64
...@@ -331,7 +331,7 @@ Test verify on dataset ...@@ -331,7 +331,7 @@ Test verify on dataset
> robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t) > robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
> end > end
> EOF > EOF
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.0 x0 <= 0.0
x1 >= 1.0 x1 >= 1.0
...@@ -344,7 +344,7 @@ Test verify on dataset ...@@ -344,7 +344,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375 x4 <= 0.776470588000000017103729987866245210170745849609375
+y0 -y1 >= 0 +y0 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.0 x0 <= 0.0
x1 >= 1.0 x1 >= 1.0
...@@ -357,7 +357,7 @@ Test verify on dataset ...@@ -357,7 +357,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375 x4 <= 0.776470588000000017103729987866245210170745849609375
+y2 -y1 >= 0 +y2 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.0 x0 <= 0.0
x1 >= 1.0 x1 >= 1.0
...@@ -370,7 +370,7 @@ Test verify on dataset ...@@ -370,7 +370,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375 x4 <= 0.776470588000000017103729987866245210170745849609375
+y3 -y1 >= 0 +y3 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.0 x0 <= 0.0
x1 >= 1.0 x1 >= 1.0
...@@ -383,7 +383,7 @@ Test verify on dataset ...@@ -383,7 +383,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375 x4 <= 0.776470588000000017103729987866245210170745849609375
+y4 -y1 >= 0 +y4 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625 x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625 x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0 x1 >= 0.0
...@@ -396,7 +396,7 @@ Test verify on dataset ...@@ -396,7 +396,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375 x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y1 -y0 >= 0 +y1 -y0 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625 x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625 x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0 x1 >= 0.0
...@@ -409,7 +409,7 @@ Test verify on dataset ...@@ -409,7 +409,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375 x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y2 -y0 >= 0 +y2 -y0 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625 x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625 x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0 x1 >= 0.0
...@@ -422,7 +422,7 @@ Test verify on dataset ...@@ -422,7 +422,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375 x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y3 -y0 >= 0 +y3 -y0 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625 x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625 x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0 x1 >= 0.0
...@@ -435,7 +435,7 @@ Test verify on dataset ...@@ -435,7 +435,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375 x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y4 -y0 >= 0 +y4 -y0 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375 x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375 x1 >= 0.9899999999999999911182158029987476766109466552734375
...@@ -448,7 +448,7 @@ Test verify on dataset ...@@ -448,7 +448,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375 x4 <= 0.7864705880000000259855141848674975335597991943359375
+y0 -y1 >= 0 +y0 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375 x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375 x1 >= 0.9899999999999999911182158029987476766109466552734375
...@@ -461,7 +461,7 @@ Test verify on dataset ...@@ -461,7 +461,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375 x4 <= 0.7864705880000000259855141848674975335597991943359375
+y2 -y1 >= 0 +y2 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375 x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375 x1 >= 0.9899999999999999911182158029987476766109466552734375
...@@ -474,7 +474,7 @@ Test verify on dataset ...@@ -474,7 +474,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375 x4 <= 0.7864705880000000259855141848674975335597991943359375
+y3 -y1 >= 0 +y3 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375 x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375 x1 >= 0.9899999999999999911182158029987476766109466552734375
...@@ -487,7 +487,7 @@ Test verify on dataset ...@@ -487,7 +487,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375 x4 <= 0.7864705880000000259855141848674975335597991943359375
+y4 -y1 >= 0 +y4 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375 x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875 x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0 x1 >= 0.0
...@@ -500,7 +500,7 @@ Test verify on dataset ...@@ -500,7 +500,7 @@ Test verify on dataset
x4 <= 0.049215686000000001543153160810106783173978328704833984375 x4 <= 0.049215686000000001543153160810106783173978328704833984375
+y1 -y0 >= 0 +y1 -y0 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375 x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875 x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0 x1 >= 0.0
...@@ -513,7 +513,7 @@ Test verify on dataset ...@@ -513,7 +513,7 @@ Test verify on dataset
x4 <= 0.049215686000000001543153160810106783173978328704833984375 x4 <= 0.049215686000000001543153160810106783173978328704833984375
+y2 -y0 >= 0 +y2 -y0 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375 x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875 x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0 x1 >= 0.0
...@@ -526,7 +526,7 @@ Test verify on dataset ...@@ -526,7 +526,7 @@ Test verify on dataset
x4 <= 0.049215686000000001543153160810106783173978328704833984375 x4 <= 0.049215686000000001543153160810106783173978328704833984375
+y3 -y0 >= 0 +y3 -y0 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375 x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875 x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0 x1 >= 0.0
......
tests/interpretation_acasxu.t
+ 3
− 3
View file @ 2e3169a2
...@@ -7,7 +7,7 @@ Test interpret on acasxu ...@@ -7,7 +7,7 @@ Test interpret on acasxu
$ PATH=$(pwd)/bin:$PATH $ PATH=$(pwd)/bin:$PATH
$ caisar verify --format whyml --prover PyRAT --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh $ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T > theory T
> use ieee_float.Float64 > use ieee_float.Float64
> use bool.Bool > use bool.Bool
...@@ -95,7 +95,7 @@ Test interpret on acasxu ...@@ -95,7 +95,7 @@ Test interpret on acasxu
> not (advises nn i clear_of_conflict) > not (advises nn i clear_of_conflict)
> end > end
> EOF > EOF
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0 -0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625 x0 <= 0.67985927880386987087746319957659579813480377197265625
-0.499999999999967081887319864108576439321041107177734375 <= x1 -0.499999999999967081887319864108576439321041107177734375 <= x1
...@@ -111,7 +111,7 @@ Test interpret on acasxu ...@@ -111,7 +111,7 @@ Test interpret on acasxu
x4 <= -0.450000000000000011102230246251565404236316680908203125 x4 <= -0.450000000000000011102230246251565404236316680908203125
y0 <= 3.991125645861615112153231166303157806396484375 y0 <= 3.991125645861615112153231166303157806396484375
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0 -0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625 x0 <= 0.67985927880386987087746319957659579813480377197265625
-0.499999999999967081887319864108576439321041107177734375 <= x1 -0.499999999999967081887319864108576439321041107177734375 <= x1
......
tests/interpretation_dataset.t
+ 5
− 5
View file @ 2e3169a2
...@@ -11,7 +11,7 @@ Test interpret on dataset ...@@ -11,7 +11,7 @@ Test interpret on dataset
$ PATH=$(pwd)/bin:$PATH $ PATH=$(pwd)/bin:$PATH
$ caisar verify --format whyml --prover Marabou --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh $ caisar verify --format whyml --prover Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T > theory T
> use ieee_float.Float64 > use ieee_float.Float64
> use bool.Bool > use bool.Bool
...@@ -53,7 +53,7 @@ Test interpret on dataset ...@@ -53,7 +53,7 @@ Test interpret on dataset
> robust nn dataset eps > robust nn dataset eps
> end > end
> EOF > EOF
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 1.0 x0 <= 1.0
x1 >= 0.0 x1 >= 0.0
...@@ -76,7 +76,7 @@ Test interpret on dataset ...@@ -76,7 +76,7 @@ Test interpret on dataset
x4 <= 1.151470588000000017103729987866245210170745849609375 x4 <= 1.151470588000000017103729987866245210170745849609375
+y0 -y1 >= 0 +y0 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 1.0 x0 <= 1.0
x1 >= 0.0 x1 >= 0.0
...@@ -99,7 +99,7 @@ Test interpret on dataset ...@@ -99,7 +99,7 @@ Test interpret on dataset
x4 <= 1.151470588000000017103729987866245210170745849609375 x4 <= 1.151470588000000017103729987866245210170745849609375
+y2 -y1 >= 0 +y2 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 1.0 x0 <= 1.0
x1 >= 0.0 x1 >= 0.0
...@@ -122,7 +122,7 @@ Test interpret on dataset ...@@ -122,7 +122,7 @@ Test interpret on dataset
x4 <= 1.159313725000000072640204962226562201976776123046875 x4 <= 1.159313725000000072640204962226562201976776123046875
+y1 -y0 >= 0 +y1 -y0 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 1.0 x0 <= 1.0
x1 >= 0.0 x1 >= 0.0
......
tests/marabou.t
+ 9
− 9
View file @ 2e3169a2
...@@ -6,7 +6,7 @@ Test verify ...@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH $ PATH=$(pwd)/bin:$PATH
$ caisar verify --format whyml --prover=Marabou --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh $ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T > theory T
> use ieee_float.Float64 > use ieee_float.Float64
> use bool.Bool > use bool.Bool
...@@ -41,17 +41,17 @@ Test verify ...@@ -41,17 +41,17 @@ Test verify
> (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1] > (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1]
> end > end
> EOF > EOF
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.5 x0 <= 0.5
y0 <= 0.0 y0 <= 0.0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.5 x0 <= 0.5
y0 >= 0.5 y0 >= 0.5
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.5 x0 <= 0.5
x1 >= 0.5 x1 >= 0.5
...@@ -59,21 +59,21 @@ Test verify ...@@ -59,21 +59,21 @@ Test verify
y0 <= 0.0 y0 <= 0.0
y0 <= 0.5 y0 <= 0.5
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.5 x0 <= 0.5
x1 >= 0.5 x1 >= 0.5
x1 <= 1.0 x1 <= 1.0
y1 <= 0.0 y1 <= 0.0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.5 x0 <= 0.5
x1 >= 0.5 x1 >= 0.5
x1 <= 1.0 x1 <= 1.0
y1 >= 0.5 y1 >= 0.5
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.5 x0 <= 0.5
x1 >= 0.5 x1 >= 0.5
...@@ -81,7 +81,7 @@ Test verify ...@@ -81,7 +81,7 @@ Test verify
+y1 -y0 >= 0 +y1 -y0 >= 0
+y0 -y1 >= 0 +y0 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0 x0 >= 0.0
x0 <= 0.5 x0 <= 0.5
x1 >= 0.5 x1 >= 0.5
...@@ -89,7 +89,7 @@ Test verify ...@@ -89,7 +89,7 @@ Test verify
+y1 -y0 >= 0 +y1 -y0 >= 0
+y0 -y1 >= 0 +y0 -y1 >= 0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.75 x0 >= 0.75
x0 <= 1.0 x0 <= 1.0
x1 >= 0.5 x1 >= 0.5
......
tests/pyrat.t
+ 9
− 9
View file @ 2e3169a2
...@@ -6,7 +6,7 @@ Test verify ...@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH $ PATH=$(pwd)/bin:$PATH
$ caisar verify --format whyml --prover=PyRAT --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT > theory PyRAT
> use TestNetwork.AsTuple > use TestNetwork.AsTuple
> use ieee_float.Float64 > use ieee_float.Float64
...@@ -30,52 +30,52 @@ Test verify ...@@ -30,52 +30,52 @@ Test verify
> ((0.0:t) .< (nn@@i)[0] \/ (0.5:t) .< (nn@@i)[0]) /\ (0.0:t) .< (nn@@i)[1] .< (0.5:t) > ((0.0:t) .< (nn@@i)[0] \/ (0.5:t) .< (nn@@i)[0]) /\ (0.0:t) .< (nn@@i)[1] .< (0.5:t)
> end > end
> EOF > EOF
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0 0.0 <= x0
x0 <= 0.5 x0 <= 0.5
0.0 < y0 0.0 < y0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0 0.0 <= x0
x0 <= 0.5 x0 <= 0.5
y0 < 0.5 y0 < 0.5
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0 0.0 <= x0
x0 <= 0.5 x0 <= 0.5
0.5 <= x1 0.5 <= x1
x1 <= 1.0 x1 <= 1.0
(0.0 < y0 or 0.5 < y0) (0.0 < y0 or 0.5 < y0)
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0 0.0 <= x0
x0 <= 0.5 x0 <= 0.5
0.5 <= x1 0.5 <= x1
x1 <= 1.0 x1 <= 1.0
0.0 < y1 0.0 < y1
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0 0.0 <= x0
x0 <= 0.5 x0 <= 0.5
0.5 <= x1 0.5 <= x1
x1 <= 1.0 x1 <= 1.0
y1 < 0.5 y1 < 0.5
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.375 <= x0 0.375 <= x0
x0 <= 0.75 x0 <= 0.75
0.5 <= x1 0.5 <= x1
x1 <= 1.0 x1 <= 1.0
(0.0 < y0 or 0.5 < y0) (0.0 < y0 or 0.5 < y0)
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.375 <= x0 0.375 <= x0
x0 <= 0.75 x0 <= 0.75
0.5 <= x1 0.5 <= x1
x1 <= 1.0 x1 <= 1.0
0.0 < y1 0.0 < y1
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.375 <= x0 0.375 <= x0
x0 <= 0.75 x0 <= 0.75
0.5 <= x1 0.5 <= x1
......
tests/pyrat_onnx.t
+ 3
− 3
View file @ 2e3169a2
...@@ -6,7 +6,7 @@ Test verify ...@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH $ PATH=$(pwd)/bin:$PATH
$ caisar verify --format whyml --prover=PyRAT --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT_ONNX > theory PyRAT_ONNX
> use ieee_float.Float64 > use ieee_float.Float64
> use bool.Bool > use bool.Bool
...@@ -23,12 +23,12 @@ Test verify ...@@ -23,12 +23,12 @@ Test verify
> (0.0:t) .< (nn@@i)[0] .< (0.5:t) > (0.0:t) .< (nn@@i)[0] .< (0.5:t)
> end > end
> EOF > EOF
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0 0.0 <= x0
x0 <= 0.5 x0 <= 0.5
0.0 < y0 0.0 < y0
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0 0.0 <= x0
x0 <= 0.5 x0 <= 0.5
y0 < 0.5 y0 < 0.5
......
tests/verify_json.t
+ 2
− 2
View file @ 2e3169a2
...@@ -14,8 +14,8 @@ Test verify-json ...@@ -14,8 +14,8 @@ Test verify-json
$ PATH=$(pwd)/bin:$PATH $ PATH=$(pwd)/bin:$PATH
$ caisar verify-json --ltag=Spec config.json 2>&1 <<EOF | ./filter_tmpdir.sh $ caisar verify-json --ltag=ProverSpec config.json 2>&1 <<EOF | ./filter_tmpdir.sh
[DEBUG]{Spec} Prover-tailored specification: [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver ;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver ;;; produced by VNN-LIB driver
;; X_0 ;; X_0
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment