CBMC
Classes | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
solver_factoryt Class Referencefinal

#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. More...
 
virtual std::unique_ptr< solvert > get_solver ()
 Returns a solvert object. More...
 
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 More...
 
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. More...
 
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). More...
 
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 26 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 377 of file solver_factory.cpp.

◆ get_default()

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

Definition at line 327 of file solver_factory.cpp.

◆ get_dimacs()

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

Definition at line 347 of file solver_factory.cpp.

◆ get_external_sat()

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

Definition at line 362 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 451 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 496 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 126 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 101 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 406 of file solver_factory.cpp.

◆ no_beautification()

void solver_factoryt::no_beautification ( )
protected

Definition at line 559 of file solver_factory.cpp.

◆ no_incremental_check()

void solver_factoryt::no_incremental_check ( )
protected

Definition at line 568 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 91 of file solver_factory.cpp.

Member Data Documentation

◆ message_handler

message_handlert& solver_factoryt::message_handler
protected

Definition at line 69 of file solver_factory.h.

◆ ns

const namespacet& solver_factoryt::ns
protected

Definition at line 68 of file solver_factory.h.

◆ options

const optionst& solver_factoryt::options
protected

Definition at line 67 of file solver_factory.h.

◆ output_xml_in_refinement

const bool solver_factoryt::output_xml_in_refinement
protected

Definition at line 70 of file solver_factory.h.

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