From 264d6732bb7f92acf6c7538413f8580a4f4604d9 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 19 Apr 2021 17:03:55 +0200
Subject: [PATCH] Avoid to index subgoals when not needed.
---
engine.ml | 41 ++++++++++++++++++++++++++++-------------
1 file changed, 28 insertions(+), 13 deletions(-)
diff --git a/engine.ml b/engine.ml
index 735dc72..e86821d 100644
--- a/engine.ml
+++ b/engine.ml
@@ -18,8 +18,9 @@ type task = {
(* Original goal name. *)
goalname: string;
(* Subgoal identifier.
- Typically a goal is translated to multiple subgoals by a solver. *)
- subgoal: int;
+ Typically a goal is translated to multiple subgoals by a solver.
+ [None] means the goal has no subgoals. *)
+ subgoal: int option;
(* The formula to verify. *)
formula: string;
(* Verification result.
@@ -70,6 +71,20 @@ let check_compatibility solver model =
let tasks_of_property solver { axioms; goals } =
let module S = (val solver: Solver.S) in
+ let make_task goalname subgoal formula =
+ let id =
+ Format.sprintf "%s%s"
+ goalname
+ (Option.value_map subgoal
+ ~default:""
+ ~f:(fun idx -> Format.sprintf ".%d" idx))
+ in
+ { id;
+ goalname;
+ subgoal;
+ formula = Format.asprintf "%a" S.pretty formula;
+ result = None; }
+ in
let hypothesis =
match axioms with
| [] ->
@@ -86,14 +101,9 @@ let tasks_of_property solver { axioms; goals } =
~f:(fun { name; formula; } ->
let elts = S.(repr (translate ~hypothesis ~goal:formula)) in
let tasks =
- List.mapi
- elts
- ~f:(fun idx elt ->
- { id = Format.sprintf "%s.%d" name idx;
- goalname = name;
- subgoal = idx;
- formula = Format.asprintf "%a" S.pretty elt;
- result = None; })
+ if List.length elts = 1
+ then [ make_task name None (List.hd_exn elts) ]
+ else List.mapi elts ~f:(fun idx elt -> make_task name (Some idx) elt)
in
Hashtbl.set table ~key:name ~data:tasks);
table
@@ -174,8 +184,13 @@ let exec_tasks ~raw_options solver config model tasks_htbl =
tasks
~f:(fun task ->
Logs.app (fun m ->
- m "Verifying goal `%s', subgoal %d (%s)."
- task.goalname task.subgoal task.id);
+ m "Verifying goal `%s'%s."
+ task.goalname
+ (Option.value_map task.subgoal
+ ~default:""
+ ~f:(fun subgoal ->
+ Format.sprintf ", subgoal %d (%s)"
+ subgoal task.id)));
let res_exec_task =
(* Build the required command-line. *)
build_command ~raw_options solver config model task
@@ -190,7 +205,7 @@ let exec_tasks ~raw_options solver config model tasks_htbl =
else begin
(* Extract and pretty-print verification result. *)
let result = extract_result solver ~log ~output in
- Logs.app (fun m -> m "Result %s: %a."
+ Logs.app (fun m -> m "Result of `%s': %a."
task.id Solver.Result.pretty result);
Sys.remove output;
if Solver.Result.equal result Solver.Result.Failure
--
GitLab