solve.cpp File Reference

#include <solve.h>
#include <solver_config.h>
#include <solvers/smt/array_conv.h>
#include <solvers/smt/fp/fp_conv.h>
#include <solvers/smt/smt_array.h>
#include <solvers/smt/smt_conv.h>
#include <solvers/smt/smt_solver.h>
#include <solvers/smt/tuple/smt_tuple_node.h>
#include <solvers/smt/tuple/smt_tuple_sym.h>
#include <unordered_map>

Include dependency graph for solve.cpp:

Functions
static std::string	pick_default_solver ()
static std::string	resolve_user_solver_choice (const optionst &options)
void	check_solver_availability (const optionst &options)
	Abort early if the user explicitly selected an SMT solver that was not built into this ESBMC binary.
static solver_creator &	pick_solver (std::string &solver_name, const optionst &options)
smt_convt *	create_solver (std::string solver_name, const namespacet &ns, const optionst &options)

Variables
solver_creator	create_new_smtlib_solver
solver_creator	create_new_z3_solver
solver_creator	create_new_minisat_solver
solver_creator	create_new_boolector_solver
solver_creator	create_new_cvc_solver
solver_creator	create_new_cvc5_solver
solver_creator	create_new_mathsat_solver
solver_creator	create_new_yices_solver
solver_creator	create_new_bitwuzla_solver
solver_creator	create_new_bitwuzllob_solver
solver_creator	create_new_neurosym_solver
static const std::unordered_map< std::string, solver_creator * >	esbmc_solvers
static const std::string	all_solvers []

Function Documentation

check_solver_availability()

void check_solver_availability

(

const optionst &

options

)

Abort early if the user explicitly selected an SMT solver that was not built into this ESBMC binary.

Safe to call before parsing the program; returns silently when no explicit selection was made (the default picker will choose from whatever is built in at solver-creation time).

create_solver()

smt_convt * create_solver	(	std::string	solver_name,
		const namespacet &	ns,
		const optionst &	options )

pick_default_solver()

std::string pick_default_solver ( )

static

pick_solver()

solver_creator & pick_solver ( std::string & solver_name, const optionst & options )

static

resolve_user_solver_choice()

std::string resolve_user_solver_choice ( const optionst & options )

static

Variable Documentation

all_solvers

const std::string all_solvers[]

static

Initial value:

= {
  "smtlib",
  "bitwuzllob",
  "neurosym",
  "bitwuzla",
  "boolector",
  "z3",
  "minisat",
  "cvc4",
  "cvc5",
  "mathsat",
  "yices"}

create_new_bitwuzla_solver

solver_creator create_new_bitwuzla_solver

create_new_bitwuzllob_solver

solver_creator create_new_bitwuzllob_solver

create_new_boolector_solver

solver_creator create_new_boolector_solver

create_new_cvc5_solver

solver_creator create_new_cvc5_solver

create_new_cvc_solver

solver_creator create_new_cvc_solver

create_new_mathsat_solver

solver_creator create_new_mathsat_solver

create_new_minisat_solver

solver_creator create_new_minisat_solver

create_new_neurosym_solver

solver_creator create_new_neurosym_solver

create_new_smtlib_solver

solver_creator create_new_smtlib_solver

create_new_yices_solver

solver_creator create_new_yices_solver

create_new_z3_solver

solver_creator create_new_z3_solver

esbmc_solvers

const std::unordered_map<std::string, solver_creator *> esbmc_solvers

static