Include dependency graph for solver_factory.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | solver_factoryt |
| class | solver_factoryt::solvert |
Macros | |
| #define | OPT_SOLVER |
| #define | HELP_SOLVER |
Functions | |
| void | parse_solver_options (const cmdlinet &cmdline, optionst &options) |
Parse solver-related command-line parameters in cmdline and set corresponding values in options. More... | |
Detailed Description
Solver Factory
Definition in file solver_factory.h.
Macro Definition Documentation
◆ HELP_SOLVER
| #define HELP_SOLVER |
Value:
" --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" \
" --smt1 use default SMT1 solver (obsolete)\n" \
" --smt2 use default SMT2 solver (Z3)\n" \
" --boolector use Boolector\n" \
" --cprover-smt2 use CPROVER SMT2 solver\n" \
" --cvc3 use CVC3\n" \
" --cvc4 use CVC4\n" \
" --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" \
" --outfile filename output formula to given file\n" \
" --write-solver-stats-to json-file\n" \
" collect the solver query complexity\n"
Definition at line 119 of file solver_factory.h.
◆ OPT_SOLVER
| #define OPT_SOLVER |
Value:
"(smt1)" /* rejected, will eventually disappear */ \
"(smt2)" \
"(fpa)" \
"(cvc3)" \
"(cvc4)(boolector)(yices)(z3)" \
"(mathsat)" \
"(cprover-smt2)" \
"(incremental-smt2-solver):" \
"(external-sat-solver):" \
"(no-sat-preprocessor)" \
"(beautify)" \
"(dimacs)" \
"(refine)" \
"(max-node-refinement):" \
"(refine-arrays)" \
"(refine-arithmetic)" \
"(outfile):" \
"(write-solver-stats-to):"
Definition at line 99 of file solver_factory.h.
Function Documentation
◆ parse_solver_options()
Parse solver-related command-line parameters in cmdline and set corresponding values in options.
Definition at line 537 of file solver_factory.cpp.
