solve.h File Reference

#include <string>
#include <util/config/config.h>
#include <util/symtab/namespace.h>
#include <util/message/message.h>

Include dependency graph for solve.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs
typedef smt_solver_baset *	solver_creator(const optionst &options, const namespacet &ns, tuple_iface **tuple_api, array_iface **array_api, fp_convt **fp_api)

Functions
smt_convt *	create_solver (std::string solver_name, const namespacet &ns, 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.

Typedef Documentation

solver_creator

typedef smt_solver_baset * solver_creator(const optionst &options, const namespacet &ns, tuple_iface **tuple_api, array_iface **array_api, fp_convt **fp_api)

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 )