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 symbol_tablet &_symbol_table, message_handlert &_message_handler, bool _output_xml_in_refinement)
virtual std::unique_ptr< solvert >	get_solver ()
virtual	~solver_factoryt ()

Protected Member Functions
std::unique_ptr< solvert >	get_default ()
std::unique_ptr< solvert >	get_dimacs ()
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 More...
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. More...
void	no_beautification ()
void	no_incremental_check ()

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

Detailed Description

Definition at line 28 of file solver_factory.h.

Constructor & Destructor Documentation

solver_factoryt()

solver_factoryt::solver_factoryt ( const optionst &  _options, const symbol_tablet &  _symbol_table, message_handlert &  _message_handler, bool  _output_xml_in_refinement  )

inline

Definition at line 31 of file solver_factory.h.

~solver_factoryt()

virtual solver_factoryt::~solver_factoryt ( )

inlinevirtual

Definition at line 115 of file solver_factory.h.

Member Function Documentation

get_bv_refinement()

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

protected

Definition at line 104 of file solver_factory.cpp.

get_default()

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

protected

Definition at line 60 of file solver_factory.cpp.

get_dimacs()

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

protected

Definition at line 90 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 159 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 33 of file solver_factory.cpp.

get_solver()

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

inlinevirtual

Definition at line 102 of file solver_factory.h.

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 139 of file solver_factory.cpp.

no_beautification()

void solver_factoryt::no_beautification ( )

protected

Definition at line 235 of file solver_factory.cpp.

no_incremental_check()

void solver_factoryt::no_incremental_check ( )

protected

Definition at line 244 of file solver_factory.cpp.

Member Data Documentation

message_handler

message_handlert& solver_factoryt::message_handler

protected

Definition at line 123 of file solver_factory.h.

ns

namespacet solver_factoryt::ns

protected

Definition at line 122 of file solver_factory.h.

options

const optionst& solver_factoryt::options

protected

Definition at line 120 of file solver_factory.h.

output_xml_in_refinement

const bool solver_factoryt::output_xml_in_refinement

protected

Definition at line 124 of file solver_factory.h.

symbol_table

const symbol_tablet& solver_factoryt::symbol_table

protected

Definition at line 121 of file solver_factory.h.

---

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

• goto-checker/solver_factory.h
• goto-checker/solver_factory.cpp