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:

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

Definition at line 121 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):"                                                 \
  "(external-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.

Function Documentation

◆ parse_solver_options()

void parse_solver_options	(	const cmdlinet &	cmdline,
		optionst &	options
	)

Parse solver-related command-line parameters in cmdline and set corresponding values in options.

Definition at line 699 of file solver_factory.cpp.

Classes