Merge pull request #6927 from tautschnig/bugfixes/arch

Document all architecture and back-end options

Author: tautschnig

src/goto-checker/solver_factory.h

@@ -99,25 +99,26 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
 #define OPT_SOLVER                                                             \
   "(smt1)" /* rejected, will eventually disappear */                           \
   "(smt2)"                                                                     \
-  "(fpa)" /* undocumented */                                                   \
+  "(fpa)"                                                                      \
   "(cvc3)"                                                                     \
   "(cvc4)(boolector)(yices)(z3)"                                               \
   "(mathsat)"                                                                  \
   "(cprover-smt2)"                                                             \
   "(incremental-smt2-solver):"                                                 \
   "(external-sat-solver):"                                                     \
-  "(no-sat-preprocessor)" /* undocumented */                                   \
+  "(no-sat-preprocessor)"                                                      \
   "(beautify)"                                                                 \
   "(dimacs)"                                                                   \
   "(refine)"                                                                   \
-  "(max-node-refinement):" /* undocumented */                                  \
-  "(refine-arrays)"        /* undocumented */                                  \
-  "(refine-arithmetic)"    /* undocumented */                                  \
+  "(max-node-refinement):"                                                     \
+  "(refine-arrays)"                                                            \
+  "(refine-arithmetic)"                                                        \
   "(outfile):"                                                                 \
   "(write-solver-stats-to):"
 
 #define HELP_SOLVER                                                            \
   " --external-sat-solver cmd    command to invoke SAT solver process\n"       \
+  " --no-sat-preprocessor        disable the SAT solver's simplifier\n"        \
   " --dimacs                     generate CNF in DIMACS format\n"              \
   " --beautify                   beautify the counterexample\n"                \
   "                              (greedy heuristic)\n"                         \
@@ -130,7 +131,12 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   " --mathsat                    use MathSAT\n"                                \
   " --yices                      use Yices\n"                                  \
   " --z3                         use Z3\n"                                     \
+  " --fpa                        use theory of floating-point arithmetic\n"    \
   " --refine                     use refinement procedure (experimental)\n"    \
+  " --refine-arrays              use refinement for arrays only\n"             \
+  " --refine-arithmetic          refinement of arithmetic expressions only\n"  \
+  " --max-node-refinement        maximum refinement iterations for\n"          \
+  "                              arithmetic expressions\n"                     \
   " --incremental-smt2-solver cmd\n"                                           \
   "                              command to invoke external SMT solver for\n"  \
   "                              incremental solving (experimental)\n"         \

src/util/config.h

@@ -32,23 +32,25 @@ class symbol_tablet;
 
 #define HELP_CONFIG_C_CPP                                                      \
   " -I path                      set include path (C/C++)\n"                   \
+  " --include file               set include file (C/C++)\n"                   \
   " -D macro                     define preprocessor macro (C/C++)\n"          \
-  " --c89/99/11                  set C language standard (default: "           \
+  " --c89, --c99, --c11          set C language standard (default: "           \
                                  << (configt::ansi_ct::default_c_standard()==  \
                                      configt::ansi_ct::c_standardt::C89?"c89": \
                                      configt::ansi_ct::default_c_standard()==  \
                                      configt::ansi_ct::c_standardt::C99?"c99": \
                                      configt::ansi_ct::default_c_standard()==  \
                           configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n"\
-  " --cpp98/03/11                set C++ language standard (default: "         \
+  " --cpp98, --cpp03, --cpp11    set C++ language standard (default: "         \
                                  << (configt::cppt::default_cpp_standard()==   \
                                    configt::cppt::cpp_standardt::CPP98?"cpp98":\
                                      configt::cppt::default_cpp_standard()==   \
                                    configt::cppt::cpp_standardt::CPP03?"cpp03":\
                                      configt::cppt::default_cpp_standard()==   \
                        configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n"\
   " --unsigned-char              make \"char\" unsigned by default\n"          \
-  " --round-to-nearest           rounding towards nearest even (default)\n"    \
+  " --round-to-nearest, --round-to-even\n"                                     \
+  "                              rounding towards nearest even (default)\n"    \
   " --round-to-plus-inf          rounding towards plus infinity\n"             \
   " --round-to-minus-inf         rounding towards minus infinity\n"            \
   " --round-to-zero              rounding towards zero\n"                      \
@@ -83,6 +85,8 @@ class symbol_tablet;
                                  << configt::this_architecture() << ")\n"      \
   " --os                         set operating system (default: "              \
                                  << configt::this_operating_system() << ")\n"  \
+  " --i386-linux, --i386-win32, --i386-macos, --ppc-macos\n"                   \
+  "   --win32, --winx64          set architecture and operating system\n"      \
   " --16, --32, --64             set width of int\n"                           \
   " --LP64, --ILP64, --LLP64,\n"                                               \
   "   --ILP32, --LP32            set width of int, long and pointers\n"        \