From e9e4df8e1fd87e25d15165357608d6cfbd201e24 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 13 Apr 2021 11:23:55 +0200
Subject: [PATCH] Compute solver name list in help message.
---
main.ml | 12 ++++++++++--
1 file changed, 10 insertions(+), 2 deletions(-)
diff --git a/main.ml b/main.ml
index 5a7b015..6cdafd5 100644
--- a/main.ml
+++ b/main.ml
@@ -119,9 +119,17 @@ let verify_cmd =
let cmdname = "verify" in
let docv_solver = "SOLVER" in
let solver =
+ let solver_names =
+ List.map ~f:(fun s -> String.lowercase (Solver.show s)) Solver.defaults
+ in
let doc =
- "The solver to use for verification. \
- $(docv) must be either `pyrat' or `marabou'."
+ Format.asprintf
+ "The solver to use for verification. \
+ $(docv) must be chosen among: %a."
+ (Format.pp_print_list
+ ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ", ")
+ Format.pp_print_string)
+ solver_names
in
let solvers =
Arg.enum
--
GitLab