From 4ca9b5087e44e3ffacc9e696ec1ba034f5ed3702 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 12 May 2023 12:17:36 +0200
Subject: [PATCH] [verification] Interpret task for classic provers also.
On such tasks, the interpretation should provide no effect.
---
src/verification.ml | 16 ++++++++++------
1 file changed, 10 insertions(+), 6 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index 48f0a47..8488a87 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -223,8 +223,9 @@ let answer_dataset limit config env prover config_prover driver dataset task =
in
(prover_answer, additional_info)
-let answer_generic limit config env prover config_prover driver ~strategy task =
- let tasks = strategy env task in
+let answer_generic limit config env prover config_prover driver ~proof_strategy
+ task =
+ let tasks = proof_strategy env task in
let answers =
List.concat_map tasks ~f:(fun task ->
let task = Driver.prepare_task driver task in
@@ -263,11 +264,14 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task
answer_dataset limit config env prover config_prover driver dataset task
| Marabou | Pyrat | Nnenum ->
let task = Interpretation.interpret_task ~cwd env task in
- let strategy = Proof_strategy.apply_native_nn_prover in
- answer_generic limit config env prover config_prover driver ~strategy task
+ let proof_strategy = Proof_strategy.apply_native_nn_prover in
+ answer_generic limit config env prover config_prover driver
+ ~proof_strategy task
| CVC5 ->
- let strategy = Proof_strategy.apply_classic_prover in
- answer_generic limit config env prover config_prover driver ~strategy task
+ let task = Interpretation.interpret_task ~cwd env task in
+ let proof_strategy = Proof_strategy.apply_classic_prover in
+ answer_generic limit config env prover config_prover driver
+ ~proof_strategy task
in
let id = Task.task_goal task in
{ id; prover_answer; additional_info }
--
GitLab