diff --git a/src/autodetect.ml b/src/autodetect.ml
index a7f5c262e029882bcaa7a9c30240bb6900ddbe0e..6d739a8214518f247b31de1baba29f4af8b8146a 100644
--- a/src/autodetect.ml
+++ b/src/autodetect.ml
@@ -23,8 +23,6 @@
open Why3
open Base
-let null = if Caml.Sys.unix then "/dev/null" else "NUL"
-
let rec lookup_file dirs filename =
match dirs with
| [] -> raise Caml.Not_found
@@ -32,7 +30,8 @@ let rec lookup_file dirs filename =
let file = Caml.Filename.concat dir filename in
if Caml.Sys.file_exists file then file else lookup_file dirs filename
-let autodetection ?(debug = false) () =
+let autodetection () =
+ let debug = Logging.(is_debug_level () || is_dtag_enabled Autodetect) in
if debug then Debug.set_flag Autodetection.debug;
let caisar_conf =
lookup_file Dirs.Sites.config "caisar-detection-data.conf"
@@ -50,6 +49,6 @@ let autodetection ?(debug = false) () =
}
:: acc)
in
- let config = Whyconf.init_config (Some null) in
+ let config = Whyconf.init_config (Some Caml.Filename.null) in
let provers = Autodetection.compute_builtin_prover provers config data in
Whyconf.set_provers config provers
diff --git a/src/autodetect.mli b/src/autodetect.mli
index ccd02cb04380aeb0a6a8fa50d1cc4010f42c9a20..540f357fe60835f3f0843ae15cd5cb34c938e3d5 100644
--- a/src/autodetect.mli
+++ b/src/autodetect.mli
@@ -20,7 +20,5 @@
(* *)
(**************************************************************************)
-val autodetection : ?debug:bool -> unit -> Why3.Whyconf.config
-(** Perform the autodetection of provers.
-
- @param debug activates debug information. *)
+val autodetection : unit -> Why3.Whyconf.config
+(** Perform the autodetection of provers. *)
diff --git a/src/convert_xgboost.ml b/src/convert_xgboost.ml
index c6cc71c31fa766dc2e1ce768fcee237b59da8476..5e54ede75d076da6e4daaf9e07d93496a85411e6 100644
--- a/src/convert_xgboost.ml
+++ b/src/convert_xgboost.ml
@@ -258,7 +258,7 @@ let prove_and_print ?memlimit ?timelimit env config prover task =
Fmt.pr "result: %a@." Why3.Call_provers.print_prover_answer answer.pr_answer
let verify ?memlimit ?timelimit ~xgboost ~dataset ~prover () =
- let env, config = Verification.create_env ~debug:false [] in
+ let env, config = Verification.create_env [] in
let task = None in
let th_real = Why3.Env.read_theory env [ "real" ] "Real" in
let task = Why3.Task.use_export task th_real in
diff --git a/src/dune b/src/dune
index 9d7cf5b389c6ee9705358ddf0ebdbc96b395fa61..013aad1ad73f2872edafa7fb997432b281d29898 100644
--- a/src/dune
+++ b/src/dune
@@ -9,6 +9,7 @@
logs.cli
logs.fmt
fmt.tty
+ fmt.cli
base
unix
str
diff --git a/src/logging.ml b/src/logging.ml
index ebe3f2dd672423f106bdba3c88cfddae78025f21..6158ee4f3008ff27a01519e4505b612471307d8d 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -20,47 +20,98 @@
(* *)
(**************************************************************************)
-module Category = struct
- type t = Specification [@@deriving show]
+type dtag =
+ | Autodetect
+ | Specification
+[@@deriving show { with_path = false }]
- let list_available () = [ Specification ]
- let of_string = function "specification" -> Some Specification | _ -> None
- let to_string = function Specification -> "specification"
-end
+let dtags_available () = [ Autodetect; Specification ]
+let dtag_defs_enabled = ref []
-let spec_tag_def =
- Logs.Tag.def ~doc:"Specification sent to prover." "specification" Fmt.string
+let dtag_def_auto =
+ Logs.Tag.def "autodetect" ~doc:"Prover autodetection" Fmt.string
-let spec_tag () = Logs.Tag.(empty |> add spec_tag_def "specification")
+let dtag_def_spec =
+ Logs.Tag.def "spec" ~doc:"Prover-tailored specification" Fmt.string
-let pp_header =
- let x =
- match Array.length Caml.Sys.argv with
- | 0 -> Caml.(Filename.basename Sys.executable_name)
- | _ -> Caml.(Filename.basename Sys.argv.(0))
+let dtag_def_of_dtag = function
+ | Autodetect -> dtag_def_auto
+ | Specification -> dtag_def_spec
+
+let dtag_auto = Logs.Tag.add dtag_def_auto "AUTO"
+let dtag_spec = Logs.Tag.add dtag_def_spec "SPEC"
+let add_dtag = function Autodetect -> dtag_auto | Specification -> dtag_spec
+let dtag dt = add_dtag dt Logs.Tag.empty
+
+let is_dtag_enabled dtag =
+ let dtag_def = dtag_def_of_dtag dtag in
+ List.memq dtag_def !dtag_defs_enabled
+
+let is_debug_level () =
+ match Logs.level () with Some Debug -> true | _ -> false
+
+let pp_header ~pp_h ppf (l, (h : string option)) =
+ match l with
+ | Logs.App -> (
+ match h with None -> () | h -> pp_h ppf Logs_fmt.app_style "" h)
+ | Logs.Error -> pp_h ppf Logs_fmt.err_style "ERROR" h
+ | Logs.Warning -> pp_h ppf Logs_fmt.warn_style "WARNING" h
+ | Logs.Info -> pp_h ppf Logs_fmt.info_style "INFO" h
+ | Logs.Debug -> pp_h ppf Logs_fmt.debug_style "DEBUG" h
+
+let pp_header ~space =
+ let pp_h ppf style default h =
+ Fmt.pf ppf "[%a%a]%s"
+ Fmt.(styled style string)
+ default
+ Fmt.(styled style (option (any ":" ++ string)))
+ h
+ (if space then " " else "")
in
- let pp_h ppf style h = Fmt.pf ppf "[%s][%a] " x Fmt.(styled style string) h in
- fun ppf (l, h) ->
- let open Logs_fmt in
- match l with
- | Logs.App -> Fmt.pf ppf "[%a] " Fmt.(styled app_style string) x
- | Logs.Error ->
- pp_h ppf err_style (match h with None -> "ERROR" | Some h -> h)
- | Logs.Warning ->
- pp_h ppf warn_style (match h with None -> "WARNING" | Some h -> h)
- | Logs.Info ->
- pp_h ppf info_style (match h with None -> "INFO" | Some h -> h)
- | Logs.Debug ->
- pp_h ppf debug_style (match h with None -> "DEBUG" | Some h -> h)
+ pp_header ~pp_h
-let specification_enabled = ref false
+let dtag_defs_available = List.map dtag_def_of_dtag (dtags_available ())
-let setup_log level categories =
- Fmt_tty.setup_std_outputs ~style_renderer:`Ansi_tty ();
- Logs.set_level level;
- let () =
- match categories with
- | Some [ Category.Specification ] -> specification_enabled := true
- | _ -> ()
+let reporter ppf =
+ let report _src level ~over k msgf =
+ let k _ =
+ over ();
+ k ()
+ in
+ let with_tags ~header ~tags k ppf fmt =
+ let tag =
+ Base.List.filter_map dtag_defs_available ~f:(fun td ->
+ Logs.Tag.find td tags)
+ |> List.hd
+ in
+ Fmt.kpf k ppf
+ ("%a{%a} @[" ^^ fmt ^^ "@]@.")
+ (pp_header ~space:false) (Logs.Debug, header)
+ Fmt.(styled Logs_fmt.debug_style string)
+ tag
+ in
+ msgf @@ fun ?header ?tags fmt ->
+ match tags with
+ | None ->
+ Fmt.kpf k ppf
+ ("%a@[" ^^ fmt ^^ "@]@.")
+ (pp_header ~space:true) (level, header)
+ | Some tags ->
+ let dtag_is_enabled =
+ not
+ Base.(
+ List.filter_map !dtag_defs_enabled ~f:(fun td ->
+ Logs.Tag.find td tags)
+ |> List.is_empty)
+ in
+ if is_debug_level () || dtag_is_enabled
+ then with_tags ~header ~tags k ppf fmt
+ else Fmt.kpf k Format.str_formatter fmt
in
- Logs.set_reporter (Logs_fmt.reporter ~pp_header ())
+ { Logs.report }
+
+let setup style_renderer level dtags =
+ dtag_defs_enabled := List.map dtag_def_of_dtag dtags;
+ Fmt_tty.setup_std_outputs ?style_renderer ();
+ Logs.set_level level;
+ Logs.set_reporter (reporter Fmt.stdout)
diff --git a/src/logging.mli b/src/logging.mli
index 04be9381f876e9e472d97626629fecf117a292c1..dea68e42a9a7fbc17157d4bf9357a3aedf038d5e 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -20,14 +20,18 @@
(* *)
(**************************************************************************)
-module Category : sig
- type t = Specification [@@deriving show]
+(** {2 Debug Tags} *)
- val list_available : unit -> t list
- val of_string : string -> t option
- val to_string : t -> string
-end
+type dtag =
+ | Autodetect
+ | Specification
+[@@deriving show { with_path = false }]
-val specification_enabled : bool ref
-val spec_tag : unit -> Logs.Tag.set
-val setup_log : Logs.level option -> Category.t list option -> unit
+val dtags_available : unit -> dtag list
+val dtag : dtag -> Logs.Tag.set
+val is_dtag_enabled : dtag -> bool
+
+(** {2 Logs} *)
+
+val is_debug_level : unit -> bool
+val setup : Fmt.style_renderer option -> Logs.level option -> dtag list -> unit
diff --git a/src/main.ml b/src/main.ml
index e82a636db6edfdbd1f8d720542d904d55a77a002..bf5ae617a7982acc22103e2c7dc7eb6225c7b35c 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -34,40 +34,35 @@ let () =
Marabou.init ();
Vnnlib.init ()
-(* -- Logs. *)
+(* -- Logs *)
-let log_categories =
- let all_categories = Logging.Category.list_available () in
+let log_debug_tags =
+ let all_debug_tags = Logging.dtags_available () in
let doc =
- Fmt.str "Logging categories. Available are $(docv)s: %a."
- (Fmt.list ~sep:Fmt.comma Fmt.string)
- (List.map ~f:Logging.Category.to_string all_categories)
+ Fmt.str "Logging debug tags. Available $(docv)s: %a."
+ (Fmt.list ~sep:Fmt.comma Logging.pp_dtag)
+ all_debug_tags
in
- let enum_log_categories =
- Arg.enum
- (List.map ~f:(fun c -> (Logging.Category.to_string c, c)) all_categories)
+ let enum_log_debug_tags =
+ Arg.enum (List.map ~f:(fun c -> (Logging.show_dtag c, c)) all_debug_tags)
in
Arg.(
value
- & opt (some (list enum_log_categories)) None
- & info [ "c"; "log-category" ] ~doc ~docv:"LOGTAG")
+ & opt_all enum_log_debug_tags []
+ & info [ "debug-tag"; "dtag" ] ~doc ~docv:"DTAG")
let setup_logs =
- Term.(const Logging.setup_log $ Logs_cli.level () $ log_categories)
+ Term.(
+ const Logging.setup $ Fmt_cli.style_renderer () $ Logs_cli.level ()
+ $ log_debug_tags)
-let log_level_is_debug () =
- match Logs.level () with Some Debug -> true | _ -> false
-
-(* -- Commands. *)
+(* -- Commands *)
let config detect () =
if detect
then (
Logs.debug (fun m -> m "Automatic detection");
- let config =
- let debug = log_level_is_debug () in
- Autodetect.autodetection ~debug ()
- in
+ let config = Autodetect.autodetection () in
let open Why3 in
let provers = Whyconf.get_provers config in
if not (Whyconf.Mprover.is_empty provers)
@@ -128,14 +123,13 @@ let log_theory_answer =
let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
files =
- let debug = log_level_is_debug () in
let memlimit = Option.map memlimit ~f:memlimit_of_string in
let timelimit = Option.map timelimit ~f:timelimit_of_string in
let theory_answers =
List.map files
~f:
- (Verification.verify ~debug ?format ~loadpath ?memlimit ?timelimit
- ?dataset prover ?prover_altern)
+ (Verification.verify ?format ~loadpath ?memlimit ?timelimit ?dataset
+ prover ?prover_altern)
in
List.iter theory_answers ~f:log_theory_answer;
theory_answers
@@ -429,5 +423,5 @@ let () =
Cmd.group ~default:default_cmd default_info
[ config_cmd; verify_cmd; verify_json_cmd; verify_xgboost_cmd ]
|> Cmd.eval ~catch:false |> Caml.exit
- with exn when not (log_level_is_debug ()) ->
+ with exn when not (Logging.is_debug_level ()) ->
Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
diff --git a/src/verification.ml b/src/verification.ml
index 54579457e7a652dd0e2cf9d6a199c6de87369bdc..2106b78de172ef8c5f40a49c2a0400b12586b01e 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -74,8 +74,8 @@ let () =
Language.register_onnx_support ();
Language.register_ovo_support ()
-let create_env ?(debug = false) loadpath =
- let config = Autodetect.autodetection ~debug () in
+let create_env loadpath =
+ let config = Autodetect.autodetection () in
let config =
let main = Whyconf.get_main config in
let dft_timelimit = 20.0 (* 20 seconds *) in
@@ -164,11 +164,13 @@ let build_command config_prover ~nn_filename =
let log_prover_task driver task =
let print fmt task = ignore (Driver.print_task_prepared driver fmt task) in
- Logs.info (fun m ->
- m ~tags:(Logging.spec_tag ()) "[SPEC]\n@[%a@]" print task)
+ Logs.app (fun m ->
+ m
+ ~tags:Logging.(dtag Specification)
+ "@[Prover-tailored specification:@.%a@]" print task)
let call_prover_on_task limit config command driver task =
- if !Logging.specification_enabled then log_prover_task driver task;
+ log_prover_task driver task;
let prover_call =
Driver.prove_task_prepared ~command ~config ~limit driver task
in
@@ -300,10 +302,11 @@ let open_file ?format env file =
let th = Json.theory_of_input env jin in
(Unix.getcwd () (* TODO *), Wstdlib.Mstr.singleton th.th_name.id_string th)
-let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
- prover ?prover_altern file =
- if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
- let env, config = create_env ~debug loadpath in
+let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
+ file =
+ (if Logging.is_debug_level ()
+ then Debug.(set_flag (lookup_flag "call_prover")));
+ let env, config = create_env loadpath in
let main = Whyconf.get_main config in
let limit =
let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
diff --git a/src/verification.mli b/src/verification.mli
index 645834243a14eae1befe979ff7e0083f3fc8656a..b6da390487261aa64221d12fbb7f76e7ff9d9f38 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -47,7 +47,6 @@ and additional_info = private
(** A prover answer per data point. *)
val verify :
- ?debug:bool ->
?format:string ->
loadpath:string list ->
?memlimit:int ->
@@ -61,7 +60,6 @@ val verify :
launches a verification of the given [file] with the provided [prover] and
[dataset].
- @param debug when set, enables debug information.
@param format is the [file] format.
@param loadpath is the additional loadpath.
@param memlimit
@@ -75,5 +73,4 @@ val verify :
for each theory, an [answer] for each goal of the theory, respecting the
order of appearance. *)
-val create_env :
- ?debug:bool -> string list -> Why3.Env.env * Why3.Whyconf.config
+val create_env : string list -> Why3.Env.env * Why3.Whyconf.config
diff --git a/tests/aimos.t b/tests/aimos.t
index 1d53b28be70d30bd8d289b5c4a8806518ca8a475..0ac820383c49c20deff4bb1dbcc441a94ab251a2 100644
--- a/tests/aimos.t
+++ b/tests/aimos.t
@@ -22,4 +22,4 @@ Test verify
> goal G: meta_robust model dataset (1.0:t) ("reluplex_rotation":string) ("config/custom_transformations.py":string) ("classif_min":string) (0:int) (0:int) (0:int)
> end
> EOF
- [caisar] Goal G: Valid
+ Goal G: Valid
diff --git a/tests/autodetect.t b/tests/autodetect.t
index cd2e8efe01d966b015262f540b62f7773338cf02..3aea5500e65117b0211a03840ad0ab3c3bce6be1 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -32,9 +32,7 @@ Test autodetect
$ PATH=$(pwd)/bin:$PATH
- $ caisar config -d -vv 2>&1 | ./filter_tmpdir.sh
- [caisar][DEBUG] Execution of command 'config'
- [caisar][DEBUG] Automatic detection
+ $ caisar config -d --dtag=Autodetect -v 2>&1 | ./filter_tmpdir.sh
<autodetect>Run: ($TESTCASE_ROOT/bin/nnenum.sh --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
@@ -57,14 +55,14 @@ Test autodetect
<autodetect>Found prover SAVer version v1.0, OK.
<autodetect>Found prover AIMOS version 1.0, OK.
<autodetect>11 prover(s) added
- [caisar] AIMOS 1.0
- Alt-Ergo 2.4.0
- CVC5 1.0.2
- Marabou 1.0.+
- PyRAT 1.1
- PyRAT 1.1 (ACAS)
- PyRAT 1.1 (VNNLIB)
- SAVer v1.0
- alpha-beta-CROWN dummy-version
- alpha-beta-CROWN dummy-version (ACAS)
- nnenum dummy-version
+ AIMOS 1.0
+ Alt-Ergo 2.4.0
+ CVC5 1.0.2
+ Marabou 1.0.+
+ PyRAT 1.1
+ PyRAT 1.1 (ACAS)
+ PyRAT 1.1 (VNNLIB)
+ SAVer v1.0
+ alpha-beta-CROWN dummy-version
+ alpha-beta-CROWN dummy-version (ACAS)
+ nnenum dummy-version
diff --git a/tests/cvc5.t b/tests/cvc5.t
index 2ce662deaa765ea13de7fb5eff82b7721333960f..e424af71308ed68f0b590f0be55b4efca0e28d34 100644
--- a/tests/cvc5.t
+++ b/tests/cvc5.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover=CVC5 - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --prover=CVC5 --dtag=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory CVC5
> use TestNetworkONNX.AsTuple as TN
> use ieee_float.Float64
@@ -17,262 +17,218 @@ Test verify
> (0.0:t) .< y1 .< (0.5:t) /\ (0.0:t) .< y2 .< (1.0:t)
> end
> EOF
- [caisar] Goal G: Unknown (unknown)
- $ caisar verify -L . --format whyml --prover=CVC5 --verbosity=info --log-category=specification - 2>&1 <<EOF | ./filter_tmpdir.sh
- > theory CVC5_oracle
- > use TestNetworkONNX.AsTuple as TN
- > use ieee_float.Float64
- >
- > goal G: forall x1 x2 x3.
- > (0.0:t) .< x1 .< (0.5:t) ->
- > let (y1,y2) = TN.nn_apply x1 x2 x3 in
- > (0.0:t) .< y1 .< (0.5:t) /\ (0.0:t) .< y2 .< (1.0:t)
- > end
- > EOF
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
;; produced by cvc5.drv ;;
- (set-logic ALL)
- (set-info :smt-lib-version 2.6)
- ;;; generated by SMT-LIB2 driver
- ;;; SMT-LIB2 driver: bit-vectors, common part
- ;;; SMT-LIB2: integer arithmetic
- ;;; SMT-LIB2: real arithmetic
- (define-fun fp.isFinite64 ((x Float64)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
- (define-fun fp.isIntegral64 ((x Float64)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
- (declare-sort uni 0)
-
- (declare-sort ty 0)
-
- ;; "sort"
- (declare-fun sort (ty
- uni) Bool)
-
- ;; "witness"
- (declare-fun witness (ty) uni)
-
- ;; "witness_sort"
- (assert (forall ((a ty)) (sort a (witness a))))
-
- ;; "int"
- (declare-fun int () ty)
-
- ;; "real"
- (declare-fun real () ty)
-
- ;; "t"
- (declare-fun t () ty)
-
- ;; "mode"
- (declare-fun mode () ty)
-
- ;; "add_div"
- (assert
- (forall ((x Real) (y Real) (z Real))
- (=>
- (not (= z 0.0))
- (= (/ (+ x y) z) (+ (/ x z) (/ y z))))))
-
- ;; "sub_div"
- (assert
- (forall ((x Real) (y Real) (z Real))
- (=>
- (not (= z 0.0))
- (= (/ (- x y) z) (- (/ x z) (/ y z))))))
-
- ;; "neg_div"
- (assert
- (forall ((x Real) (y Real))
- (=> (not (= y 0.0)) (= (/ (- x) y) (- (/ x y))))))
-
- ;; "assoc_mul_div"
- (assert
- (forall ((x Real) (y Real) (z Real))
- (=>
- (not (= z 0.0))
- (= (/ (* x y) z) (* x (/ y z))))))
-
- ;; "assoc_div_mul"
- (assert
- (forall ((x Real) (y Real) (z Real))
- (=>
- (and (not (= y 0.0)) (not (= z 0.0)))
- (= (/ (/ x y) z) (/ x (* y z))))))
-
- ;; "assoc_div_div"
- (assert
- (forall ((x Real) (y Real) (z Real))
- (=>
- (and (not (= y 0.0)) (not (= z 0.0)))
- (= (/ x (/ y z)) (/ (* x z) y)))))
-
- ;; "CompatOrderMult"
- (assert
- (forall ((x Real) (y Real) (z Real))
- (=> (<= x y) (=> (<= 0.0 z) (<= (* x z) (* y z))))))
-
- ;; "max_real"
- (declare-fun max_real () Real)
-
- ;; "max_int"
- (declare-fun max_int () Int)
-
- ;; "sqr"
- (declare-fun sqr (Real) Real)
-
- ;; "sqr'def"
- (assert (forall ((x Real)) (= (sqr x) (* x x))))
-
- ;; "sqrt"
- (declare-fun sqrt1 (Real) Real)
-
- ;; "Sqrt_positive"
- (assert
- (forall ((x Real))
- (=> (<= 0.0 x) (<= 0.0 (sqrt1 x)))))
-
- ;; "Sqrt_square"
- (assert
- (forall ((x Real))
- (=> (<= 0.0 x) (= (sqr (sqrt1 x)) x))))
-
- ;; "Square_sqrt"
- (assert
- (forall ((x Real))
- (=> (<= 0.0 x) (= (sqrt1 (* x x)) x))))
-
- ;; "Sqrt_mul"
- (assert
- (forall ((x Real) (y Real))
- (=>
- (and (<= 0.0 x) (<= 0.0 y))
- (= (sqrt1 (* x y)) (* (sqrt1 x) (sqrt1 y))))))
-
- ;; "Sqrt_le"
- (assert
- (forall ((x Real) (y Real))
- (=>
- (and (<= 0.0 x) (<= x y))
- (<= (sqrt1 x) (sqrt1 y)))))
-
- ;; "relu"
- (declare-fun relu (Float64) Float64)
-
- ;; "relu'def"
- (assert
- (forall ((a Float64))
- (ite (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) a)
- (= (relu a) a)
- (= (relu a) (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000)))))
-
- (declare-datatypes ((tuple2 2))
- ((par (a
- a1) ((Tuple2 (Tuple2_proj a)(Tuple2_proj1 a1))))))
-
- ;; "tuple2"
- (declare-fun tuple21 (ty
- ty) ty)
-
- ;; "Tuple2"
- (declare-fun Tuple21 (ty
- ty
- uni
- uni) uni)
-
- ;; "Tuple2_sort"
- (assert
- (forall ((a2 ty) (a3 ty))
- (forall ((x uni) (x1 uni))
- (sort (tuple21 a3 a2) (Tuple21 a3 a2 x x1)))))
-
- ;; "Tuple2_proj_1"
- (declare-fun Tuple2_proj_1 (ty
- ty
- uni) uni)
-
- ;; "Tuple2_proj_1_sort"
- (assert
- (forall ((a2 ty) (a3 ty))
- (forall ((x uni))
- (sort a3 (Tuple2_proj_1 a3 a2 x)))))
-
- ;; "Tuple2_proj_1'def"
- (assert
- (forall ((a2 ty) (a3 ty))
- (forall ((u uni) (u1 uni))
- (=>
- (sort a3 u)
- (= (Tuple2_proj_1 a3 a2 (Tuple21 a3 a2 u u1)) u)))))
-
- ;; "Tuple2_proj_2"
- (declare-fun Tuple2_proj_2 (ty
- ty
- uni) uni)
-
- ;; "Tuple2_proj_2_sort"
- (assert
- (forall ((a2 ty) (a3 ty))
- (forall ((x uni))
- (sort a2 (Tuple2_proj_2 a3 a2 x)))))
-
- ;; "Tuple2_proj_2'def"
- (assert
- (forall ((a2 ty) (a3 ty))
- (forall ((u uni) (u1 uni))
- (=>
- (sort a2 u1)
- (= (Tuple2_proj_2 a3 a2 (Tuple21 a3 a2 u u1)) u1)))))
-
- ;; "tuple2_inversion"
- (assert
- (forall ((a2 ty) (a3 ty))
- (forall ((u uni))
- (=>
- (sort (tuple21 a3 a2) u)
- (= u (Tuple21
- a3
- a2
- (Tuple2_proj_1 a3 a2 u)
- (Tuple2_proj_2 a3 a2 u)))))))
-
- ;; Goal "G"
- ;; File "stdin", line 5, characters 7-8
- (assert
- (not
- (forall ((x1 Float64) (x2 Float64) (x3 Float64))
- (=>
- (and
- (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) x1)
- (fp.lt x1 (fp #b0 #b01111111110 #b0000000000000000000000000000000000000000000000000000)))
- (match (let ((n_id_1_2 x3))
- (let ((n_id_1_1 x2))
- (let ((n_id_1_0 x1))
- (let ((n_id_2_1 (fp.add RNE (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_1_0 (fp #b1 #b01111111100 #b0010110110101110110001100000000000000000000000000000))) (fp.mul RNE n_id_1_1 (fp #b0 #b01111111100 #b0001010101101010011100100000000000000000000000000000))) (fp.mul RNE n_id_1_2 (fp #b1 #b01111111100 #b0001110001000101101000100000000000000000000000000000)))))
- (let ((n_id_2_0 (fp.add RNE (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_1_0 (fp #b1 #b01111111100 #b0010110110101110110001100000000000000000000000000000))) (fp.mul RNE n_id_1_1 (fp #b0 #b01111111100 #b0001010101101010011100100000000000000000000000000000))) (fp.mul RNE n_id_1_2 (fp #b1 #b01111111100 #b0001110001000101101000100000000000000000000000000000)))))
- (let ((n_id_3_1 (fp.add RNE n_id_2_1 (fp #b1 #b01111111110 #b0001011011111110000011100000000000000000000000000000))))
- (let ((n_id_3_0 (fp.add RNE n_id_2_0 (fp #b0 #b01111111101 #b0110010010001010001001100000000000000000000000000000))))
- (let ((n_id_4_1 (relu
- n_id_3_1)))
- (let ((n_id_4_0 (relu
- n_id_3_0)))
- (let ((n_id_5_1 (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_4_0 (fp #b1 #b01111111101 #b0111110011110010111010000000000000000000000000000000))) (fp.mul RNE n_id_4_1 (fp #b0 #b01111111110 #b0100011001000110100010000000000000000000000000000000)))))
- (let ((n_id_5_0 (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_4_0 (fp #b1 #b01111111101 #b0111110011110010111010000000000000000000000000000000))) (fp.mul RNE n_id_4_1 (fp #b0 #b01111111110 #b0100011001000110100010000000000000000000000000000000)))))
- (let ((n_id_6_1 (fp.add RNE n_id_5_1 (fp #b1 #b01111111110 #b0011101101010011010001100000000000000000000000000000))))
- (let ((n_id_6_0 (fp.add RNE n_id_5_0 (fp #b0 #b01111111110 #b0011000001100111100001000000000000000000000000000000))))
- (let ((y2 n_id_6_1))
- (let ((y1 n_id_6_0))
- (Tuple2
- y1
- y2)))))))))))))))) (
- ((Tuple2 x x4) (and
- (and
- (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) x)
- (fp.lt x (fp #b0 #b01111111110 #b0000000000000000000000000000000000000000000000000000)))
- (and
- (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) x4)
- (fp.lt x4 (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)))))))))))
-
- (check-sat)
- (get-info :reason-unknown)
-
- [caisar][INFO] Verification results for theory 'CVC5_oracle'
- [caisar] Goal G: Unknown (unknown)
+ (set-logic ALL)
+ (set-info :smt-lib-version 2.6)
+ ;;; generated by SMT-LIB2 driver
+ ;;; SMT-LIB2 driver: bit-vectors, common part
+ ;;; SMT-LIB2: integer arithmetic
+ ;;; SMT-LIB2: real arithmetic
+ (define-fun fp.isFinite64 ((x Float64)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
+ (define-fun fp.isIntegral64 ((x Float64)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
+ (declare-sort uni 0)
+
+ (declare-sort ty 0)
+
+ ;; "sort"
+ (declare-fun sort (ty
+ uni) Bool)
+
+ ;; "witness"
+ (declare-fun witness (ty) uni)
+
+ ;; "witness_sort"
+ (assert (forall ((a ty)) (sort a (witness a))))
+
+ ;; "int"
+ (declare-fun int () ty)
+
+ ;; "real"
+ (declare-fun real () ty)
+
+ ;; "t"
+ (declare-fun t () ty)
+
+ ;; "mode"
+ (declare-fun mode () ty)
+
+ ;; "add_div"
+ (assert
+ (forall ((x Real) (y Real) (z Real))
+ (=> (not (= z 0.0)) (= (/ (+ x y) z) (+ (/ x z) (/ y z))))))
+
+ ;; "sub_div"
+ (assert
+ (forall ((x Real) (y Real) (z Real))
+ (=> (not (= z 0.0)) (= (/ (- x y) z) (- (/ x z) (/ y z))))))
+
+ ;; "neg_div"
+ (assert
+ (forall ((x Real) (y Real))
+ (=> (not (= y 0.0)) (= (/ (- x) y) (- (/ x y))))))
+
+ ;; "assoc_mul_div"
+ (assert
+ (forall ((x Real) (y Real) (z Real))
+ (=> (not (= z 0.0)) (= (/ (* x y) z) (* x (/ y z))))))
+
+ ;; "assoc_div_mul"
+ (assert
+ (forall ((x Real) (y Real) (z Real))
+ (=>
+ (and (not (= y 0.0)) (not (= z 0.0)))
+ (= (/ (/ x y) z) (/ x (* y z))))))
+
+ ;; "assoc_div_div"
+ (assert
+ (forall ((x Real) (y Real) (z Real))
+ (=>
+ (and (not (= y 0.0)) (not (= z 0.0)))
+ (= (/ x (/ y z)) (/ (* x z) y)))))
+
+ ;; "CompatOrderMult"
+ (assert
+ (forall ((x Real) (y Real) (z Real))
+ (=> (<= x y) (=> (<= 0.0 z) (<= (* x z) (* y z))))))
+
+ ;; "max_real"
+ (declare-fun max_real () Real)
+
+ ;; "max_int"
+ (declare-fun max_int () Int)
+
+ ;; "sqr"
+ (declare-fun sqr (Real) Real)
+
+ ;; "sqr'def"
+ (assert (forall ((x Real)) (= (sqr x) (* x x))))
+
+ ;; "sqrt"
+ (declare-fun sqrt1 (Real) Real)
+
+ ;; "Sqrt_positive"
+ (assert (forall ((x Real)) (=> (<= 0.0 x) (<= 0.0 (sqrt1 x)))))
+
+ ;; "Sqrt_square"
+ (assert (forall ((x Real)) (=> (<= 0.0 x) (= (sqr (sqrt1 x)) x))))
+
+ ;; "Square_sqrt"
+ (assert (forall ((x Real)) (=> (<= 0.0 x) (= (sqrt1 (* x x)) x))))
+
+ ;; "Sqrt_mul"
+ (assert
+ (forall ((x Real) (y Real))
+ (=>
+ (and (<= 0.0 x) (<= 0.0 y))
+ (= (sqrt1 (* x y)) (* (sqrt1 x) (sqrt1 y))))))
+
+ ;; "Sqrt_le"
+ (assert
+ (forall ((x Real) (y Real))
+ (=> (and (<= 0.0 x) (<= x y)) (<= (sqrt1 x) (sqrt1 y)))))
+
+ ;; "relu"
+ (declare-fun relu (Float64) Float64)
+
+ ;; "relu'def"
+ (assert
+ (forall ((a Float64))
+ (ite (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) a)
+ (= (relu a) a)
+ (= (relu a) (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000)))))
+
+ (declare-datatypes ((tuple2 2))
+ ((par (a a1) ((Tuple2 (Tuple2_proj a)(Tuple2_proj1 a1))))))
+
+ ;; "tuple2"
+ (declare-fun tuple21 (ty
+ ty) ty)
+
+ ;; "Tuple2"
+ (declare-fun Tuple21 (ty
+ ty
+ uni
+ uni) uni)
+
+ ;; "Tuple2_sort"
+ (assert
+ (forall ((a2 ty) (a3 ty))
+ (forall ((x uni) (x1 uni)) (sort (tuple21 a3 a2) (Tuple21 a3 a2 x x1)))))
+
+ ;; "Tuple2_proj_1"
+ (declare-fun Tuple2_proj_1 (ty
+ ty
+ uni) uni)
+
+ ;; "Tuple2_proj_1_sort"
+ (assert
+ (forall ((a2 ty) (a3 ty))
+ (forall ((x uni)) (sort a3 (Tuple2_proj_1 a3 a2 x)))))
+
+ ;; "Tuple2_proj_1'def"
+ (assert
+ (forall ((a2 ty) (a3 ty))
+ (forall ((u uni) (u1 uni))
+ (=> (sort a3 u) (= (Tuple2_proj_1 a3 a2 (Tuple21 a3 a2 u u1)) u)))))
+
+ ;; "Tuple2_proj_2"
+ (declare-fun Tuple2_proj_2 (ty
+ ty
+ uni) uni)
+
+ ;; "Tuple2_proj_2_sort"
+ (assert
+ (forall ((a2 ty) (a3 ty))
+ (forall ((x uni)) (sort a2 (Tuple2_proj_2 a3 a2 x)))))
+
+ ;; "Tuple2_proj_2'def"
+ (assert
+ (forall ((a2 ty) (a3 ty))
+ (forall ((u uni) (u1 uni))
+ (=> (sort a2 u1) (= (Tuple2_proj_2 a3 a2 (Tuple21 a3 a2 u u1)) u1)))))
+
+ ;; "tuple2_inversion"
+ (assert
+ (forall ((a2 ty) (a3 ty))
+ (forall ((u uni))
+ (=>
+ (sort (tuple21 a3 a2) u)
+ (= u (Tuple21 a3 a2 (Tuple2_proj_1 a3 a2 u) (Tuple2_proj_2 a3 a2 u)))))))
+
+ ;; Goal "G"
+ ;; File "stdin", line 5, characters 7-8
+ (assert
+ (not
+ (forall ((x1 Float64) (x2 Float64) (x3 Float64))
+ (=>
+ (and
+ (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) x1)
+ (fp.lt x1 (fp #b0 #b01111111110 #b0000000000000000000000000000000000000000000000000000)))
+ (match (let ((n_id_1_2 x3))
+ (let ((n_id_1_1 x2))
+ (let ((n_id_1_0 x1))
+ (let ((n_id_2_1 (fp.add RNE (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_1_0 (fp #b1 #b01111111100 #b0010110110101110110001100000000000000000000000000000))) (fp.mul RNE n_id_1_1 (fp #b0 #b01111111100 #b0001010101101010011100100000000000000000000000000000))) (fp.mul RNE n_id_1_2 (fp #b1 #b01111111100 #b0001110001000101101000100000000000000000000000000000)))))
+ (let ((n_id_2_0 (fp.add RNE (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_1_0 (fp #b1 #b01111111100 #b0010110110101110110001100000000000000000000000000000))) (fp.mul RNE n_id_1_1 (fp #b0 #b01111111100 #b0001010101101010011100100000000000000000000000000000))) (fp.mul RNE n_id_1_2 (fp #b1 #b01111111100 #b0001110001000101101000100000000000000000000000000000)))))
+ (let ((n_id_3_1 (fp.add RNE n_id_2_1 (fp #b1 #b01111111110 #b0001011011111110000011100000000000000000000000000000))))
+ (let ((n_id_3_0 (fp.add RNE n_id_2_0 (fp #b0 #b01111111101 #b0110010010001010001001100000000000000000000000000000))))
+ (let ((n_id_4_1 (relu n_id_3_1)))
+ (let ((n_id_4_0 (relu n_id_3_0)))
+ (let ((n_id_5_1 (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_4_0 (fp #b1 #b01111111101 #b0111110011110010111010000000000000000000000000000000))) (fp.mul RNE n_id_4_1 (fp #b0 #b01111111110 #b0100011001000110100010000000000000000000000000000000)))))
+ (let ((n_id_5_0 (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_4_0 (fp #b1 #b01111111101 #b0111110011110010111010000000000000000000000000000000))) (fp.mul RNE n_id_4_1 (fp #b0 #b01111111110 #b0100011001000110100010000000000000000000000000000000)))))
+ (let ((n_id_6_1 (fp.add RNE n_id_5_1 (fp #b1 #b01111111110 #b0011101101010011010001100000000000000000000000000000))))
+ (let ((n_id_6_0 (fp.add RNE n_id_5_0 (fp #b0 #b01111111110 #b0011000001100111100001000000000000000000000000000000))))
+ (let ((y2 n_id_6_1))
+ (let ((y1 n_id_6_0)) (Tuple2 y1 y2)))))))))))))))) (
+ ((Tuple2 x x4) (and
+ (and
+ (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) x)
+ (fp.lt x (fp #b0 #b01111111110 #b0000000000000000000000000000000000000000000000000000)))
+ (and
+ (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) x4)
+ (fp.lt x4 (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)))))))))))
+
+ (check-sat)
+ (get-info :reason-unknown)
+
+ Goal G: Unknown (unknown)
diff --git a/tests/dataset.t b/tests/dataset.t
index 33e886ed577adfb7608d5b9dbdf8277ac72c1e18..6089fa8783e9ed024bf95608327e5802d1bab264 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -27,8 +27,8 @@ Test verify on dataset
> robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
> end
> EOF
- [caisar] Goal G: Unknown ()
- [caisar] Goal H: Unknown ()
+ Goal G: Unknown ()
+ Goal H: Unknown ()
$ caisar verify -L . --format whyml --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
@@ -43,5 +43,5 @@ Test verify on dataset
> robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
> end
> EOF
- [caisar] Goal G: Unknown ()
- [caisar] Goal H: Unknown ()
+ Goal G: Unknown ()
+ Goal H: Unknown ()
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 16b95f3aaa82ccbd840db8cd08a83bad462a7246..601fa4677969244b35966213dcd10d87df9378b1 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -7,7 +7,7 @@ Test interpret on acasxu
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover PyRAT --verbosity=info --log-category=specification - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover PyRAT --dtag=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -95,7 +95,7 @@ Test interpret on acasxu
> not (advises nn i clear_of_conflict)
> end
> EOF
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625
-0.499999999999967081887319864108576439321041107177734375 <= x1
@@ -111,7 +111,7 @@ Test interpret on acasxu
x4 <= -0.450000000000000011102230246251565404236316680908203125
y0 <= 3.991125645861615112153231166303157806396484375
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625
-0.499999999999967081887319864108576439321041107177734375 <= x1
@@ -131,6 +131,5 @@ Test interpret on acasxu
0.299999999999999988897769753748434595763683319091796875 <= x4
(((y0 >= y1 or y0 >= y2) or y0 >= y3) or y0 >= y4)
- [caisar][INFO] Verification results for theory 'T'
- [caisar] Goal P1: Unknown ()
- [caisar] Goal P3: Unknown ()
+ Goal P1: Unknown ()
+ Goal P3: Unknown ()
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index ea4b43ec83b5576861d422261f940138a71dbc79..fdbae74c333313102e5108c3956aa9ade2970982 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -11,7 +11,7 @@ Test interpret on dataset
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover Marabou --verbosity=info --log-category=specification - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover Marabou --dtag=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -53,7 +53,7 @@ Test interpret on dataset
> robust nn dataset eps
> end
> EOF
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -76,7 +76,7 @@ Test interpret on dataset
x4 <= 1.151470588000000017103729987866245210170745849609375
+y0 -y1 >= 0
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -99,7 +99,7 @@ Test interpret on dataset
x4 <= 1.151470588000000017103729987866245210170745849609375
+y2 -y1 >= 0
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -122,7 +122,7 @@ Test interpret on dataset
x4 <= 1.159313725000000072640204962226562201976776123046875
+y1 -y0 >= 0
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -145,5 +145,4 @@ Test interpret on dataset
x4 <= 1.159313725000000072640204962226562201976776123046875
+y2 -y0 >= 0
- [caisar][INFO] Verification results for theory 'T'
- [caisar] Goal G: Unknown ()
+ Goal G: Unknown ()
diff --git a/tests/marabou.t b/tests/marabou.t
index 77ba163cb9b56bbb617b773ef0e6d43e230fd398..231406ef49e589d25918f81abcee06da214e599c 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover=Marabou - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=Marabou --dtag=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -41,7 +41,63 @@ Test verify
> (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1]
> end
> EOF
- [caisar] Goal G: Unknown ()
- [caisar] Goal H: Unknown ()
- [caisar] Goal I: Unknown ()
- [caisar] Goal J: Unknown ()
+ [DEBUG]{SPEC} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ y0 <= 0.0
+
+ [DEBUG]{SPEC} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ y0 >= 0.5
+
+ [DEBUG]{SPEC} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ y0 <= 0.0
+ y0 <= 0.5
+
+ [DEBUG]{SPEC} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ y1 <= 0.0
+
+ [DEBUG]{SPEC} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ y1 >= 0.5
+
+ [DEBUG]{SPEC} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ +y1 -y0 >= 0
+ +y0 -y1 >= 0
+
+ [DEBUG]{SPEC} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ +y1 -y0 >= 0
+ +y0 -y1 >= 0
+
+ [DEBUG]{SPEC} Prover-tailored specification:
+ x0 >= 0.75
+ x0 <= 1.0
+ x1 >= 0.5
+ x1 <= 1.0
+ +y1 -y0 >= 0
+ +y0 -y1 >= 0
+
+ Goal G: Unknown ()
+ Goal H: Unknown ()
+ Goal I: Unknown ()
+ Goal J: Unknown ()
diff --git a/tests/pyrat.t b/tests/pyrat.t
index f9e4df2749311c5496ae7de9d3d409033f3af50f..ae8cb450f97dd9691ba50d553e0cd2c3d11500fd 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=PyRAT --dtag=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT
> use TestNetwork.AsTuple
> use ieee_float.Float64
@@ -30,68 +30,57 @@ Test verify
> ((0.0:t) .< (nn@@i)[0] \/ (0.5:t) .< (nn@@i)[0]) /\ (0.0:t) .< (nn@@i)[1] .< (0.5:t)
> end
> EOF
- [caisar] Goal G: Unknown ()
- [caisar] Goal H: Unknown ()
-
- $ caisar verify -L . --format whyml --prover=PyRAT --verbosity=info --log-category=specification - 2>&1 <<EOF | ./filter_tmpdir.sh
- > theory PyRAT_oracle
- > use TestNetwork.AsTuple
- > use ieee_float.Float64
- > use bool.Bool
- > use int.Int
- > use interpretation.Vector
- > use interpretation.NeuralNetwork
- >
- > constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
- >
- > goal H:
- > forall i: vector t.
- > has_length i 5 ->
- > ((0.0:t) .<= i[0] .<= (0.5:t) \/ (0.375:t) .<= i[0] .<= (0.75:t)) /\ (0.5:t) .<= i[1] .<= (1.0:t) ->
- > ((0.0:t) .< (nn@@i)[0] \/ (0.5:t) .< (nn@@i)[0]) /\ (0.0:t) .< (nn@@i)[1] .< (0.5:t)
- > end
- > EOF
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
+ 0.0 <= x0
+ x0 <= 0.5
+ 0.0 < y0
+
+ [DEBUG]{SPEC} Prover-tailored specification:
+ 0.0 <= x0
+ x0 <= 0.5
+ y0 < 0.5
+
+ [DEBUG]{SPEC} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
0.0 < y1
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
y1 < 0.5
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
0.0 < y1
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
y1 < 0.5
- [caisar][INFO] Verification results for theory 'PyRAT_oracle'
- [caisar] Goal H: Unknown ()
+ Goal G: Unknown ()
+ Goal H: Unknown ()
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index b38d1b17d59126cbe1a37caad36cbcbb709fea01..856cf83bafbf56c585d3bb74c6f5d699f4469dd9 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover=PyRAT --verbosity=info --log-category=specification - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=PyRAT --dtag=Specification - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT_ONNX
> use ieee_float.Float64
> use bool.Bool
@@ -23,15 +23,14 @@ Test verify
> (0.0:t) .< (nn@@i)[0] .< (0.5:t)
> end
> EOF
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.0 < y0
- [caisar][INFO] [SPEC]
+ [DEBUG]{SPEC} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
y0 < 0.5
- [caisar][INFO] Verification results for theory 'PyRAT_ONNX'
- [caisar] Goal G: Unknown ()
+ Goal G: Unknown ()
diff --git a/tests/saver.t b/tests/saver.t
index 56387c8ebdf9ac41f0bf45865f3295c16f63fad1..a05fc8d70b7392ac79a4251c7a461197041700d3 100644
--- a/tests/saver.t
+++ b/tests/saver.t
@@ -23,6 +23,6 @@ Test verify
> goal I: cond_robust model dataset (8.0:t)
> end
> EOF
- [caisar] Goal G: Valid (2/2)
- [caisar] Goal H: Invalid (1/2)
- [caisar] Goal I: Unknown (0/2)
+ Goal G: Valid (2/2)
+ Goal H: Invalid (1/2)
+ Goal I: Unknown (0/2)
diff --git a/tests/verify_json.t b/tests/verify_json.t
index 84575dbcee5f00539f317818b730665a5044f457..11090b9afb78f6817e4b3ac92582cfb900ecfa02 100644
--- a/tests/verify_json.t
+++ b/tests/verify_json.t
@@ -14,78 +14,77 @@ Test verify-json
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify-json config.json --verbosity=info --log-category=specification 2>&1 <<EOF | ./filter_tmpdir.sh
- [caisar][INFO] [SPEC]
+ $ caisar verify-json --dtag=Specification config.json 2>&1 <<EOF | ./filter_tmpdir.sh
+ [DEBUG]{SPEC} 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)
-
- ;; 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)
-
- ;; axiom_ge_x0
- (assert (>= X_0 0.0))
-
+ ;;; 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)
+
+ ;; 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)
+
+ ;; axiom_ge_x0
+ (assert (>= X_0 0.0))
+
;; axiom_le_x0
- (assert (<= X_0 0.299999999999999988897769753748434595763683319091796875))
-
+ (assert (<= X_0 0.299999999999999988897769753748434595763683319091796875))
+
;; axiom_ge_x1
- (assert (>= X_1 0.6999999999999999555910790149937383830547332763671875))
-
+ (assert (>= X_1 0.6999999999999999555910790149937383830547332763671875))
+
;; axiom_le_x1
- (assert (<= X_1 1.0))
-
+ (assert (<= X_1 1.0))
+
;; axiom_ge_x2
- (assert (>= X_2 0.484313724999999972720132745962473563849925994873046875))
-
+ (assert (>= X_2 0.484313724999999972720132745962473563849925994873046875))
+
;; axiom_le_x2
- (assert (<= X_2 1.0))
-
+ (assert (<= X_2 1.0))
+
;; axiom_ge_x3
- (assert (>= X_3 0.0))
-
+ (assert (>= X_3 0.0))
+
;; axiom_le_x3
- (assert (<= X_3 0.319607843000000002575688995420932769775390625))
-
+ (assert (<= X_3 0.319607843000000002575688995420932769775390625))
+
;; axiom_ge_x4
- (assert (>= X_4 0.476470588000000028205960234117810614407062530517578125))
-
+ (assert (>= X_4 0.476470588000000028205960234117810614407062530517578125))
+
;; axiom_le_x4
- (assert (<= X_4 1.0))
-
+ (assert (<= X_4 1.0))
+
;; Goal robust_record0_y1
- (assert
- (or
- (and (>= Y_0 Y_1))
- (and (>= Y_2 Y_1))
- (and (>= Y_3 Y_1))
- (and (>= Y_4 Y_1))
- ))
-
- [caisar][INFO] Verification results for theory 'JSON'
- [caisar] Goal property: Unknown ()
+ (assert
+ (or
+ (and (>= Y_0 Y_1))
+ (and (>= Y_2 Y_1))
+ (and (>= Y_3 Y_1))
+ (and (>= Y_4 Y_1))
+ ))
+
+ Goal property: Unknown ()