Skip to content

Commit fb3f391

Browse files
tautschnigtautschnig
authored
Merge pull request #6680 from tautschnig/cleanup/opt_solver
Make CBMC and JBMC share solver-related command-line parsing
2 parents 9fec06a + e9680db commit fb3f391

File tree

6 files changed

+200
-267
lines changed

6 files changed

+200
-267
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 10 additions & 110 deletions
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,6 @@ void jbmc_parse_optionst::set_default_options(optionst &options)
105105
options.set_option("pretty-names", true);
106106
options.set_option("propagation", true);
107107
options.set_option("refine-strings", true);
108-
options.set_option("sat-preprocessor", true);
109108
options.set_option("simple-slice", true);
110109
options.set_option("simplify", true);
111110
options.set_option("simplify-if", true);
@@ -274,28 +273,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
274273
else if(cmdline.isset("arrays-uf-never"))
275274
options.set_option("arrays-uf", "never");
276275

277-
if(cmdline.isset("dimacs"))
278-
options.set_option("dimacs", true);
279-
280-
if(cmdline.isset("refine-arrays"))
281-
{
282-
options.set_option("refine", true);
283-
options.set_option("refine-arrays", true);
284-
}
285-
286-
if(cmdline.isset("refine-arithmetic"))
287-
{
288-
options.set_option("refine", true);
289-
options.set_option("refine-arithmetic", true);
290-
}
291-
292-
if(cmdline.isset("refine"))
293-
{
294-
options.set_option("refine", true);
295-
options.set_option("refine-arrays", true);
296-
options.set_option("refine-arithmetic", true);
297-
}
298-
299276
if(cmdline.isset("no-refine-strings"))
300277
options.set_option("refine-strings", false);
301278

@@ -322,84 +299,10 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
322299
"--max-nondet-string-length");
323300
}
324301

325-
if(cmdline.isset("max-node-refinement"))
326-
options.set_option(
327-
"max-node-refinement",
328-
cmdline.get_value("max-node-refinement"));
329-
330-
// SMT Options
331-
332-
if(cmdline.isset("smt1"))
333-
{
334-
log.error() << "--smt1 is no longer supported" << messaget::eom;
335-
exit(CPROVER_EXIT_USAGE_ERROR);
336-
}
337-
338-
if(cmdline.isset("smt2"))
339-
options.set_option("smt2", true);
340-
341-
if(cmdline.isset("fpa"))
342-
options.set_option("fpa", true);
343-
344-
bool solver_set=false;
345-
346-
if(cmdline.isset("boolector"))
347-
{
348-
options.set_option("boolector", true), solver_set=true;
349-
options.set_option("smt2", true);
350-
}
351-
352-
if(cmdline.isset("mathsat"))
353-
{
354-
options.set_option("mathsat", true), solver_set=true;
355-
options.set_option("smt2", true);
356-
}
357-
358-
if(cmdline.isset("cvc4"))
359-
{
360-
options.set_option("cvc4", true), solver_set=true;
361-
options.set_option("smt2", true);
362-
}
363-
364-
if(cmdline.isset("yices"))
365-
{
366-
options.set_option("yices", true), solver_set=true;
367-
options.set_option("smt2", true);
368-
}
369-
370-
if(cmdline.isset("z3"))
371-
{
372-
options.set_option("z3", true), solver_set=true;
373-
options.set_option("smt2", true);
374-
}
375-
376-
if(cmdline.isset("smt2") && !solver_set)
377-
{
378-
if(cmdline.isset("outfile"))
379-
{
380-
// outfile and no solver should give standard compliant SMT-LIB
381-
options.set_option("generic", true);
382-
}
383-
else
384-
{
385-
// the default smt2 solver
386-
options.set_option("z3", true);
387-
}
388-
}
389-
390-
if(cmdline.isset("beautify"))
391-
options.set_option("beautify", true);
392-
393-
if(cmdline.isset("no-sat-preprocessor"))
394-
options.set_option("sat-preprocessor", false);
395-
396302
options.set_option(
397303
"pretty-names",
398304
!cmdline.isset("no-pretty-names"));
399305

400-
if(cmdline.isset("outfile"))
401-
options.set_option("outfile", cmdline.get_value("outfile"));
402-
403306
if(cmdline.isset("graphml-witness"))
404307
{
405308
options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
@@ -457,6 +360,14 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
457360

458361
if(cmdline.isset("show-goto-symex-steps"))
459362
options.set_option("show-goto-symex-steps", true);
363+
364+
if(cmdline.isset("smt1"))
365+
{
366+
log.error() << "--smt1 is no longer supported" << messaget::eom;
367+
exit(CPROVER_EXIT_USAGE_ERROR);
368+
}
369+
370+
parse_solver_options(cmdline, options);
460371
}
461372

462373
/// invoke main modules
@@ -1114,20 +1025,9 @@ void jbmc_parse_optionst::help()
11141025
HELP_BMC
11151026
"\n"
11161027
"Backend options:\n"
1117-
" --object-bits n number of bits used for object addresses\n"
1118-
" --dimacs generate CNF in DIMACS format\n"
1119-
" --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1120-
" --localize-faults localize faults (experimental)\n"
1121-
" --smt1 use default SMT1 solver (obsolete)\n"
1122-
" --smt2 use default SMT2 solver (Z3)\n"
1123-
" --boolector use Boolector\n"
1124-
" --mathsat use MathSAT\n"
1125-
" --cvc4 use CVC4\n"
1126-
" --yices use Yices\n"
1127-
" --z3 use Z3\n"
1128-
" --refine use refinement procedure (experimental)\n"
1028+
HELP_CONFIG_BACKEND
1029+
HELP_SOLVER
11291030
HELP_STRING_REFINEMENT
1130-
" --outfile filename output formula to given file\n"
11311031
" --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
11321032
" --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
11331033
"\n"

‎jbmc/src/jbmc/jbmc_parse_options.h

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ class optionst;
4646
"(no-simplify)(full-slice)" \
4747
OPT_REACHABILITY_SLICER \
4848
"(debug-level):(no-propagation)(no-simplify-if)" \
49-
"(document-subgoals)(outfile):" \
49+
"(document-subgoals)" \
5050
"(object-bits):" \
5151
"(classpath):(cp):" \
5252
OPT_JAVA_JAR \
@@ -55,10 +55,8 @@ class optionst;
5555
"(no-assertions)(no-assumptions)" \
5656
OPT_XML_INTERFACE \
5757
OPT_JSON_INTERFACE \
58-
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
59-
"(no-sat-preprocessor)" \
60-
"(beautify)" \
61-
"(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
58+
"(smt1)" /* rejected, will eventually disappear */ \
59+
OPT_SOLVER \
6260
OPT_STRING_REFINEMENT \
6361
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
6462
OPT_SHOW_GOTO_FUNCTIONS \

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 10 additions & 141 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,6 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
106106
options.set_option("built-in-assertions", true);
107107
options.set_option("pretty-names", true);
108108
options.set_option("propagation", true);
109-
options.set_option("sat-preprocessor", true);
110109
options.set_option("simple-slice", true);
111110
options.set_option("simplify", true);
112111
options.set_option("simplify-if", true);
@@ -306,42 +305,15 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
306305
else if(cmdline.isset("arrays-uf-never"))
307306
options.set_option("arrays-uf", "never");
308307

309-
if(cmdline.isset("dimacs"))
310-
options.set_option("dimacs", true);
311-
312308
if(cmdline.isset("show-array-constraints"))
313309
options.set_option("show-array-constraints", true);
314310

315-
if(cmdline.isset("refine-arrays"))
316-
{
317-
options.set_option("refine", true);
318-
options.set_option("refine-arrays", true);
319-
}
320-
321-
if(cmdline.isset("refine-arithmetic"))
322-
{
323-
options.set_option("refine", true);
324-
options.set_option("refine-arithmetic", true);
325-
}
326-
327-
if(cmdline.isset("refine"))
328-
{
329-
options.set_option("refine", true);
330-
options.set_option("refine-arrays", true);
331-
options.set_option("refine-arithmetic", true);
332-
}
333-
334311
if(cmdline.isset("refine-strings"))
335312
{
336313
options.set_option("refine-strings", true);
337314
options.set_option("string-printable", cmdline.isset("string-printable"));
338315
}
339316

340-
if(cmdline.isset("max-node-refinement"))
341-
options.set_option(
342-
"max-node-refinement",
343-
cmdline.get_value("max-node-refinement"));
344-
345317
options.set_option(
346318
"symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
347319

@@ -369,104 +341,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
369341
}
370342
}
371343

372-
// SMT Options
373-
374-
if(cmdline.isset("smt1"))
375-
{
376-
log.error() << "--smt1 is no longer supported" << messaget::eom;
377-
exit(CPROVER_EXIT_USAGE_ERROR);
378-
}
379-
380-
if(cmdline.isset("smt2"))
381-
options.set_option("smt2", true);
382-
383-
if(cmdline.isset("fpa"))
384-
options.set_option("fpa", true);
385-
386-
bool solver_set=false;
387-
388-
if(cmdline.isset("boolector"))
389-
{
390-
options.set_option("boolector", true), solver_set=true;
391-
options.set_option("smt2", true);
392-
}
393-
394-
if(cmdline.isset("cprover-smt2"))
395-
{
396-
options.set_option("cprover-smt2", true), solver_set = true;
397-
options.set_option("smt2", true);
398-
}
399-
400-
if(cmdline.isset("mathsat"))
401-
{
402-
options.set_option("mathsat", true), solver_set=true;
403-
options.set_option("smt2", true);
404-
}
405-
406-
if(cmdline.isset("cvc4"))
407-
{
408-
options.set_option("cvc4", true), solver_set=true;
409-
options.set_option("smt2", true);
410-
}
411-
412-
if(cmdline.isset("incremental-smt2-solver"))
413-
{
414-
options.set_option(
415-
"incremental-smt2-solver", cmdline.get_value("incremental-smt2-solver")),
416-
solver_set = true;
417-
}
418-
419-
if(cmdline.isset("external-sat-solver"))
420-
{
421-
options.set_option(
422-
"external-sat-solver", cmdline.get_value("external-sat-solver")),
423-
solver_set = true;
424-
}
425-
426-
if(cmdline.isset("yices"))
427-
{
428-
options.set_option("yices", true), solver_set=true;
429-
options.set_option("smt2", true);
430-
}
431-
432-
if(cmdline.isset("z3"))
433-
{
434-
options.set_option("z3", true), solver_set=true;
435-
options.set_option("smt2", true);
436-
}
437-
438-
if(cmdline.isset("smt2") && !solver_set)
439-
{
440-
if(cmdline.isset("outfile"))
441-
{
442-
// outfile and no solver should give standard compliant SMT-LIB
443-
options.set_option("generic", true);
444-
}
445-
else
446-
{
447-
// the default smt2 solver
448-
options.set_option("z3", true);
449-
}
450-
}
451-
452-
if(cmdline.isset("write-solver-stats-to"))
453-
{
454-
options.set_option(
455-
"write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
456-
}
457-
458-
if(cmdline.isset("beautify"))
459-
options.set_option("beautify", true);
460-
461-
if(cmdline.isset("no-sat-preprocessor"))
462-
options.set_option("sat-preprocessor", false);
463-
464344
if(cmdline.isset("no-pretty-names"))
465345
options.set_option("pretty-names", false);
466346

467-
if(cmdline.isset("outfile"))
468-
options.set_option("outfile", cmdline.get_value("outfile"));
469-
470347
if(cmdline.isset("graphml-witness"))
471348
{
472349
options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
@@ -502,6 +379,14 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
502379

503380
// Options for process_goto_program
504381
options.set_option("rewrite-union", true);
382+
383+
if(cmdline.isset("smt1"))
384+
{
385+
log.error() << "--smt1 is no longer supported" << messaget::eom;
386+
exit(CPROVER_EXIT_USAGE_ERROR);
387+
}
388+
389+
parse_solver_options(cmdline, options);
505390
}
506391

507392
/// invoke main modules
@@ -1009,6 +894,7 @@ void cbmc_parse_optionst::help()
1009894
" --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1010895
" --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1011896
" (implies --trace)\n"
897+
" --localize-faults localize faults (experimental)\n"
1012898
"\n"
1013899
"C/C++ frontend options:\n"
1014900
" --preprocess stop after preprocessing\n"
@@ -1046,23 +932,8 @@ void cbmc_parse_optionst::help()
1046932
"\n"
1047933
"Backend options:\n"
1048934
HELP_CONFIG_BACKEND
1049-
" --dimacs generate CNF in DIMACS format\n"
1050-
" --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1051-
" --localize-faults localize faults (experimental)\n"
1052-
" --smt2 use default SMT2 solver (Z3)\n"
1053-
" --boolector use Boolector\n"
1054-
" --cprover-smt2 use CPROVER SMT2 solver\n"
1055-
" --cvc4 use CVC4\n"
1056-
" --mathsat use MathSAT\n"
1057-
" --yices use Yices\n"
1058-
" --z3 use Z3\n"
1059-
" --refine use refinement procedure (experimental)\n"
1060-
" --incremental-smt2-solver cmd\n"
1061-
" command to invoke external SMT solver for\n"
1062-
" incremental solving (experimental)\n"
1063-
" --external-sat-solver cmd command to invoke SAT solver process\n"
935+
HELP_SOLVER
1064936
HELP_STRING_REFINEMENT_CBMC
1065-
" --outfile filename output formula to given file\n"
1066937
" --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1067938
" --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1068939
"\n"
@@ -1075,8 +946,6 @@ void cbmc_parse_optionst::help()
1075946
HELP_FLUSH
1076947
" --verbosity # verbosity level\n"
1077948
HELP_TIMESTAMP
1078-
" --write-solver-stats-to json-file\n"
1079-
" collect the solver query complexity\n"
1080949
" --show-array-constraints show array theory constraints added\n"
1081950
" during post processing.\n"
1082951
" Requires --json-ui.\n"

0 commit comments

Comments
 (0)