Skip to content

Commit c786a56

Browse files
kroeningkroening
committed
ebmc: use the help formatter
This enables the help formatter when showing the ebmc help.
1 parent 7995ac3 commit c786a56

File tree

1 file changed

+43
-43
lines changed

1 file changed

+43
-43
lines changed

‎src/ebmc/ebmc_parse_options.cpp

Lines changed: 43 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
1818

1919
#include <util/config.h>
2020
#include <util/exit_codes.h>
21+
#include <util/help_formatter.h>
2122

2223
#ifdef HAVE_INTERPOLATION
2324
#include "interpolation/interpolation_expr.h"
@@ -245,58 +246,57 @@ void ebmc_parse_optionst::help()
245246
"* * Version " EBMC_VERSION " * *\n"
246247
"* * University of Oxford, Computer Science Department * *\n"
247248
"* * [email protected] * *\n"
248-
"\n"
249+
"\n";
250+
251+
std::cout << help_formatter(
249252
"Usage: Purpose:\n"
250253
"\n"
251-
" ebmc [-?] [-h] [--help] show help\n"
252-
" ebmc file ... source file names\n"
254+
" {bebmc} [{y-?}] [{y-h}] [{y--help}] \t show help\n"
255+
" {bebmc} {ufile} {u...} \t source file names\n"
253256
"\n"
254257
"Additonal options:\n"
255-
" --bound <nr> set bound (default: 1)\n"
256-
// " --max-bound <nr> set maximum bound\n"
257-
" --module <module> set top module (deprecated)\n"
258-
" --top <module> set top module\n"
259-
" -p <expr> specify a property\n"
260-
" --outfile <file name> set output file name (default: stdout)\n"
261-
" --trace generate a trace for failing properties\n"
262-
" --vcd <file name> generate traces in VCD format\n"
263-
" --show-properties list the properties in the model\n"
264-
" --property <id> check the property with given ID\n"
265-
" -I path set include path\n"
266-
" --reset <expr> set up module reset\n"
258+
" {y--bound} {unr} \t set bound (default: 1)\n"
259+
" {y--module} {umodule} \t set top module (deprecated)\n"
260+
" {y--top} {umodule} \t set top module\n"
261+
" {y-p} {uexpr} \t specify a property\n"
262+
" {y--outfile} {ufile name} \t set output file name (default: stdout)\n"
263+
" {y--trace} \t generate a trace for failing properties\n"
264+
" {y--vcd} {ufile name} \t generate traces in VCD format\n"
265+
" {y--show-properties} \t list the properties in the model\n"
266+
" {y--property} {uid} \t check the property with given ID\n"
267+
" {y-I} {upath} \t set include path\n"
268+
" {y--reset} {uexpr} \t set up module reset\n"
267269
"\n"
268270
"Methods:\n"
269-
" --k-induction do k-induction with k=bound\n"
270-
" --bdd use (unbounded) BDD engine\n"
271-
" --ic3 [options] use IC3 engine with options described below\n"
272-
" --property <nm> check property named <nm>\n"
273-
" --constr use constraints specified in 'file.cnstr'\n"
274-
" --h print out help information\n"
275-
" --new-mode new mode is switched on\n"
276-
" --aiger print out the instance in aiger format\n"
271+
" {y--k-induction} \t do k-induction with k=bound\n"
272+
" {y--bdd} \t use (unbounded) BDD engine\n"
273+
" {y--ic3} \t use IC3 engine with options described below\n"
274+
" {y--constr} \t use constraints specified in 'file.cnstr'\n"
275+
" {y--new-mode} \t new mode is switched on\n"
276+
" {y--aiger} \t print out the instance in aiger format\n"
277277

278-
//" --interpolation use bit-level interpolants\n"
279-
//" --interpolation-word use word-level interpolants\n"
280-
//" --diameter perform recurrence diameter test\n"
278+
//" --interpolation \t use bit-level interpolants\n"
279+
//" --interpolation-word \t use word-level interpolants\n"
280+
//" --diameter \t perform recurrence diameter test\n"
281281
"\n"
282282
"Solvers:\n"
283-
" --aig bit-level SAT with AIGs\n"
284-
" --dimacs output bit-level CNF in DIMACS format\n"
285-
" --smt1 output word-level SMT 1 formula\n"
286-
" --smt2 output word-level SMT 2 formula\n"
287-
" --boolector use Boolector as solver\n"
288-
" --cvc4 use CVC4 as solver\n"
289-
" --mathsat use MathSAT as solver\n"
290-
" --yices use Yices as solver\n"
291-
" --z3 use Z3 as solver\n"
283+
" {y--aig} \t bit-level SAT with AIGs\n"
284+
" {y--dimacs} \t output bit-level CNF in DIMACS format\n"
285+
" {y--smt1} \t output word-level SMT 1 formula\n"
286+
" {y--smt2} \t output word-level SMT 2 formula\n"
287+
" {y--boolector} \t use Boolector as solver\n"
288+
" {y--cvc4} \t use CVC4 as solver\n"
289+
" {y--mathsat} \t use MathSAT as solver\n"
290+
" {y--yices} \t use Yices as solver\n"
291+
" {y--z3} \t use Z3 as solver\n"
292292
"\n"
293293
"Debugging options:\n"
294-
" --show-parse show parse trees\n"
295-
" --show-varmap show variable map\n"
296-
" --show-netlist show netlist\n"
297-
" --show-ldg show latch dependencies\n"
298-
" --smv-netlist show netlist in SMV format\n"
299-
" --dot-netlist show netlist in DOT format\n"
300-
" --show-trans show transition system\n"
301-
"\n";
294+
" {y--show-parse} \t show parse trees\n"
295+
" {y--show-varmap} \t show variable map\n"
296+
" {y--show-netlist} \t show netlist\n"
297+
" {y--show-ldg} \t show latch dependencies\n"
298+
" {y--smv-netlist} \t show netlist in SMV format\n"
299+
" {y--dot-netlist} \t show netlist in DOT format\n"
300+
" {y--show-trans} \t show transition system\n"
301+
"\n");
302302
}

0 commit comments

Comments
 (0)