Loading...
Searching...
No Matches
Solver Factory. More...
#include <solvers/flattening/boolbv.h>#include <solvers/smt2/smt2_dec.h>#include <fstream>#include <memory>
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. | |
Detailed Description
Solver Factory.
Definition in file solver_factory.h.
Macro Definition Documentation
◆ HELP_SOLVER
| #define HELP_SOLVER |
Value:
" {y--sat-solver} {usolver} \t use specified SAT solver\n" \
" {y--external-sat-solver} {ucmd} \t command to invoke SAT solver process\n" \
" {y--no-sat-preprocessor} \t disable the SAT solver's simplifier\n" \
" {y--dimacs} \t generate CNF in DIMACS format\n" \
" {y--beautify} \t beautify the counterexample (greedy heuristic)\n" \
" {y--smt1} \t use default SMT1 solver (obsolete)\n" \
" {y--smt2} \t use default SMT2 solver (Z3)\n" \
" {y--bitwuzla} \t use Bitwuzla\n" \
" {y--boolector} \t use Boolector\n" \
" {y--cprover-smt2} \t use CPROVER SMT2 solver\n" \
" {y--cvc3} \t use CVC3\n" \
" {y--cvc4} \t use CVC4\n" \
" {y--cvc5} \t use CVC5\n" \
" {y--mathsat} \t use MathSAT\n" \
" {y--yices} \t use Yices\n" \
" {y--z3} \t use Z3\n" \
" {y--fpa} \t use theory of floating-point arithmetic\n" \
" {y--refine} \t use refinement procedure (experimental)\n" \
" {y--refine-arrays} \t use refinement for arrays only\n" \
" {y--refine-arithmetic} \t refinement of arithmetic expressions only\n" \
" {y--max-node-refinement} \t " \
"maximum refinement iterations for arithmetic expressions\n" \
" {y--incremental-smt2-solver} {ucmd} \t " \
"command to invoke external SMT solver for incremental solving " \
"(experimental)\n" \
" {y--outfile} {ufilename} \t output formula to given file\n" \
" {y--dump-smt-formula} {ufilename} \t " \
"output smt incremental formula to the given file\n" \
" {y--write-solver-stats-to} {ujson-file} \t " \
"collect the solver query complexity\n"
Definition at line 120 of file solver_factory.h.
◆ OPT_SOLVER
| #define OPT_SOLVER |
Value:
"(smt1)" /* rejected, will eventually disappear */ \
"(smt2)" \
"(fpa)" \
"(cvc3)" \
"(cvc4)(cvc5)(bitwuzla)(boolector)(yices)(z3)" \
"(mathsat)" \
"(cprover-smt2)" \
"(incremental-smt2-solver):" \
"(sat-solver):" \
"(external-sat-solver):" \
"(no-sat-preprocessor)" \
"(beautify)" \
"(dimacs)" \
"(refine)" \
"(max-node-refinement):" \
"(refine-arrays)" \
"(refine-arithmetic)" \
"(outfile):" \
"(dump-smt-formula):" \
"(write-solver-stats-to):"
Definition at line 98 of file solver_factory.h.
