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

[prover] Use actual prover names for JSON deriving.

parent 7565cd45
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/prover.ml
+ 3
− 3
View file @ 9219d96d
...@@ -22,9 +22,9 @@ ...@@ -22,9 +22,9 @@
type t = type t =
| Marabou | Marabou
| Pyrat | Pyrat [@name "PyRAT"]
| Saver | Saver [@name "SAVer"]
| CVC5 | CVC5 [@name "cvc5"]
[@@deriving yojson, show] [@@deriving yojson, show]
let list_available () = [ Marabou; Pyrat; Saver; CVC5 ] let list_available () = [ Marabou; Pyrat; Saver; CVC5 ]
......
src/prover.mli
+ 3
− 3
View file @ 9219d96d
...@@ -22,9 +22,9 @@ ...@@ -22,9 +22,9 @@
type t = private type t = private
| Marabou | Marabou
| Pyrat | Pyrat [@name "PyRAT"]
| Saver | Saver [@name "SAVer"]
| CVC5 | CVC5 [@name "cvc5"]
[@@deriving yojson, show] [@@deriving yojson, show]
val list_available : unit -> t list val list_available : unit -> t list
......
tests/pyrat_verify_json.t
+ 1
− 1
View file @ 9219d96d
...@@ -4,7 +4,7 @@ Test verify-json ...@@ -4,7 +4,7 @@ Test verify-json
> EOF > EOF
$ cat - > config.json << EOF $ cat - > config.json << EOF
> {"prover":["Pyrat"],"model":"TestNetwork.nnet","property":{"dataset":"test_data.csv","normalization":["MinMax",{"clip":true,"min":0.0,"max":1.0}],"kind":["Robust",0.01]}} > {"prover":["PyRAT"],"model":"TestNetwork.nnet","property":{"dataset":"test_data.csv","normalization":["MinMax",{"clip":true,"min":0.0,"max":1.0}],"kind":["Robust",0.01]}}
> EOF > EOF
$ chmod u+x bin/pyrat.py $ chmod u+x bin/pyrat.py
......
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