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

[verification] Some simplification.

parent b5e4b75d
No related merge requests found
...@@ -385,32 +385,27 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task ...@@ -385,32 +385,27 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
let call_prover ~cwd ~limit config env prover config_prover driver ?dataset let call_prover ~cwd ~limit config env prover config_prover driver ?dataset
definitions task = definitions task =
let problem_answer = match prover with
match prover with | Prover.Saver when Option.is_some dataset ->
| Prover.Saver when Option.is_some dataset -> let dataset = Option.value_exn dataset in
let dataset = Option.value_exn dataset in answer_saver_on_dataset limit config env config_prover ~dataset task
answer_saver_on_dataset limit config env config_prover ~dataset task | Saver ->
| Saver -> let task = Interpreter.interpret_task ~cwd env ~definitions task in
let task = Interpreter.interpret_task ~cwd env ~definitions task in let proof_strategy = Proof_strategy.apply_svm_prover_strategy in
let proof_strategy = Proof_strategy.apply_svm_prover_strategy in answer_saver limit config env config_prover ~proof_strategy task
answer_saver limit config env config_prover ~proof_strategy task | Aimos -> answer_aimos limit config env config_prover dataset task
| Aimos -> answer_aimos limit config env config_prover dataset task | (Marabou | Maraboupy | Pyrat | Nnenum | ABCrown) when Option.is_some dataset
| (Marabou | Maraboupy | 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 | Maraboupy | Pyrat | Nnenum | ABCrown ->
| Marabou | Maraboupy | Pyrat | Nnenum | ABCrown -> let task = Interpreter.interpret_task ~cwd env ~definitions task in
let task = Interpreter.interpret_task ~cwd env ~definitions task in let proof_strategy = Proof_strategy.apply_native_nn_prover_strategy env in
let proof_strategy = Proof_strategy.apply_native_nn_prover_strategy env in answer_generic limit config prover config_prover driver ~proof_strategy task
answer_generic limit config prover config_prover driver ~proof_strategy | CVC5 | AltErgo | Z3 ->
task let task = Interpreter.interpret_task ~cwd env ~definitions task in
| CVC5 | AltErgo | Z3 -> let proof_strategy = Proof_strategy.apply_classic_prover_strategy env in
let task = Interpreter.interpret_task ~cwd env ~definitions task in answer_generic limit config prover config_prover driver ~proof_strategy task
let proof_strategy = Proof_strategy.apply_classic_prover_strategy env in
answer_generic limit config prover config_prover driver ~proof_strategy
task
in
problem_answer
let open_file ?format env file = let open_file ?format env file =
match file with match file with
...@@ -443,14 +438,10 @@ let tasks_of_theory ~theories ~goals theory = ...@@ -443,14 +438,10 @@ let tasks_of_theory ~theories ~goals theory =
let task_goal_id = task_goal.pr_name.id_string in let task_goal_id = task_goal.pr_name.id_string in
List.exists goals_of_theory ~f:(String.equal task_goal_id)) List.exists goals_of_theory ~f:(String.equal task_goal_id))
let verify ?format (query : Verification_types.Query.t) = let verify ?format query =
let debug = Logging.(is_debug_level src_prover_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 prover = query.prover in let env, config = create_env query.Verification_types.Query.loadpath in
let theories =
match query.problem with GenericProblem { theories; _ } -> theories
in
let env, config = create_env query.loadpath in
let main = Whyconf.get_main config in let main = Whyconf.get_main config in
let limit = let limit =
let memlimit = let memlimit =
...@@ -470,8 +461,8 @@ let verify ?format (query : Verification_types.Query.t) = ...@@ -470,8 +461,8 @@ let verify ?format (query : Verification_types.Query.t) =
let dataset = query.dataset in let dataset = query.dataset in
let config_prover = let config_prover =
let altern = let altern =
let is_legacy_dataset_query = Option.is_some query.dataset in
let default = let default =
let is_legacy_dataset_query = Option.is_some query.dataset in
if Prover.has_vnnlib_support query.prover && is_legacy_dataset_query if Prover.has_vnnlib_support query.prover && is_legacy_dataset_query
then "VNNLIB" then "VNNLIB"
else "" (* Select the default one, w/o an alternative. *) else "" (* Select the default one, w/o an alternative. *)
...@@ -508,14 +499,12 @@ let verify ?format (query : Verification_types.Query.t) = ...@@ -508,14 +499,12 @@ let verify ?format (query : Verification_types.Query.t) =
Driver.load_driver_file_and_extras main env ~extra_dir:None driver Driver.load_driver_file_and_extras main env ~extra_dir:None driver
config_prover.extra_drivers config_prover.extra_drivers
in in
let filepath = let filepath, definitions, goals, theories =
match query.problem with GenericProblem { filepath; _ } -> filepath
in
let cwd, mstr_theory = open_file ?format env filepath in
let goals, definitions =
match query.problem with match query.problem with
| GenericProblem { goals; definitions; _ } -> (goals, definitions) | GenericProblem { filepath; definitions; goals; theories } ->
(filepath, definitions, goals, theories)
in in
let cwd, mstr_theory = open_file ?format env filepath in
let verification_result = let verification_result =
Wstdlib.Mstr.map Wstdlib.Mstr.map
(fun theory -> (fun theory ->
...@@ -523,7 +512,7 @@ let verify ?format (query : Verification_types.Query.t) = ...@@ -523,7 +512,7 @@ let verify ?format (query : Verification_types.Query.t) =
List.map List.map
~f:(fun task -> ~f:(fun task ->
let answer = let answer =
call_prover ~cwd ~limit main env prover config_prover driver call_prover ~cwd ~limit main env query.prover config_prover driver
?dataset definitions task ?dataset definitions task
in in
Verification_types.Answer.make answer) Verification_types.Answer.make answer)
......
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