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

[verification] Add other cases which abcrown may be used for.

parent 99f588dd
No related branches found
No related tags found
No related merge requests found
...@@ -240,7 +240,7 @@ let answer_generic limit config env prover config_prover driver ~proof_strategy ...@@ -240,7 +240,7 @@ let answer_generic limit config env prover config_prover driver ~proof_strategy
tasks. *) tasks. *)
match prover with match prover with
| Prover.Marabou -> Trans.apply Split.split_all task | Prover.Marabou -> Trans.apply Split.split_all task
| Pyrat | Nnenum -> Trans.apply Split.split_premises task | Pyrat | Nnenum | ABCrown -> Trans.apply Split.split_premises task
| _ -> [ task ] | _ -> [ task ]
in in
let command = let command =
...@@ -259,7 +259,7 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task ...@@ -259,7 +259,7 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task
match prover with match prover with
| Prover.Saver -> answer_saver limit config env config_prover dataset task | Prover.Saver -> answer_saver limit config env config_prover dataset task
| Aimos -> answer_aimos limit config env config_prover dataset task | Aimos -> answer_aimos limit config env config_prover dataset task
| (Marabou | Pyrat | Nnenum) when Option.is_some dataset -> | (Marabou | Pyrat | Nnenum | ABCrown) when Option.is_some dataset ->
let dataset = Unix.realpath (Option.value_exn dataset) in let dataset = Unix.realpath (Option.value_exn dataset) in
answer_dataset limit config env prover config_prover driver dataset task answer_dataset limit config env prover config_prover driver dataset task
| Marabou | Pyrat | Nnenum | ABCrown -> | Marabou | Pyrat | Nnenum | ABCrown ->
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment