solver_factoryt Class Reference

#include <solver_factory.h>

Collaboration diagram for solver_factoryt:

Classes
class	solvert

Public Member Functions
	solver_factoryt (const optionst &_options, const namespacet &_ns, message_handlert &_message_handler, bool _output_xml_in_refinement)
	Note: The solver returned will hold a reference to the namespace ns.
virtual std::unique_ptr< solvert >	get_solver ()
	Returns a solvert object.
virtual	~solver_factoryt ()=default

Protected Member Functions
std::unique_ptr< solvert >	get_default ()
std::unique_ptr< solvert >	get_dimacs ()
std::unique_ptr< solvert >	get_external_sat ()
std::unique_ptr< solvert >	get_bv_refinement ()
std::unique_ptr< solvert >	get_string_refinement ()
	the string refinement adds to the bit vector refinement specifications for functions from the Java string library
std::unique_ptr< solvert >	get_incremental_smt2 (std::string solver_command)
std::unique_ptr< solvert >	get_smt2 (smt2_dect::solvert solver)
smt2_dect::solvert	get_smt2_solver_type () const
	Uses the options to pick an SMT 2.0 solver.
void	set_decision_procedure_time_limit (solver_resource_limitst &decision_procedure)
	Sets the timeout of decision_procedure if the solver-time-limit option has a positive value (in seconds).
void	no_beautification ()
void	no_incremental_check ()

Protected Attributes
const optionst &	options
const namespacet &	ns
message_handlert &	message_handler
const bool	output_xml_in_refinement

Detailed Description

Definition at line 27 of file solver_factory.h.

Constructor & Destructor Documentation

solver_factoryt()

solver_factoryt::solver_factoryt	(	const optionst &	_options,
		const namespacet &	_ns,
		message_handlert &	_message_handler,
		bool	_output_xml_in_refinement
	)

Note: The solver returned will hold a reference to the namespace ns.

Definition at line 36 of file solver_factory.cpp.

~solver_factoryt()

virtual solver_factoryt::~solver_factoryt ( )

virtualdefault

Member Function Documentation

get_bv_refinement()

std::unique_ptr< solver_factoryt::solvert > solver_factoryt::get_bv_refinement ( )

protected

Definition at line 419 of file solver_factory.cpp.

get_default()

std::unique_ptr< solver_factoryt::solvert > solver_factoryt::get_default ( )

protected

Definition at line 358 of file solver_factory.cpp.

get_dimacs()

std::unique_ptr< solver_factoryt::solvert > solver_factoryt::get_dimacs ( )

protected

Definition at line 378 of file solver_factory.cpp.

get_external_sat()

std::unique_ptr< solver_factoryt::solvert > solver_factoryt::get_external_sat ( )

protected

Definition at line 404 of file solver_factory.cpp.

get_incremental_smt2()

std::unique_ptr< solver_factoryt::solvert > solver_factoryt::get_incremental_smt2 ( std::string  solver_command )

protected

Definition at line 471 of file solver_factory.cpp.

get_smt2()

std::unique_ptr< solver_factoryt::solvert > solver_factoryt::get_smt2 ( smt2_dect::solvert  solver )

protected

Definition at line 516 of file solver_factory.cpp.

get_smt2_solver_type()

smt2_dect::solvert solver_factoryt::get_smt2_solver_type ( ) const

protected

Uses the options to pick an SMT 2.0 solver.

Returns

An smt2_dect::solvert giving the solver to use.

Definition at line 136 of file solver_factory.cpp.

get_solver()

std::unique_ptr< solver_factoryt::solvert > solver_factoryt::get_solver ( )

virtual

Returns a solvert object.

Definition at line 111 of file solver_factory.cpp.

get_string_refinement()

std::unique_ptr< solver_factoryt::solvert > solver_factoryt::get_string_refinement ( )

protected

the string refinement adds to the bit vector refinement specifications for functions from the Java string library

Returns

a solver for cbmc

Definition at line 448 of file solver_factory.cpp.

no_beautification()

void solver_factoryt::no_beautification ( )

protected

Definition at line 580 of file solver_factory.cpp.

no_incremental_check()

void solver_factoryt::no_incremental_check ( )

protected

Definition at line 589 of file solver_factory.cpp.

set_decision_procedure_time_limit()

void solver_factoryt::set_decision_procedure_time_limit ( solver_resource_limitst &  decision_procedure )

protected

Sets the timeout of decision_procedure if the solver-time-limit option has a positive value (in seconds).

Note

Most solvers silently ignore the time limit at the moment.

Definition at line 101 of file solver_factory.cpp.

Member Data Documentation

message_handler

message_handlert& solver_factoryt::message_handler

protected

Definition at line 74 of file solver_factory.h.

ns

const namespacet& solver_factoryt::ns

protected

Definition at line 73 of file solver_factory.h.

options

const optionst& solver_factoryt::options

protected

Definition at line 72 of file solver_factory.h.

output_xml_in_refinement

const bool solver_factoryt::output_xml_in_refinement

protected

Definition at line 75 of file solver_factory.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/cbmc/cbmc/src/goto-checker/solver_factory.h
• /home/runner/work/cbmc/cbmc/src/goto-checker/solver_factory.cpp