CBMC
Loading...
Searching...
No Matches
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:
[フレーム]
[legend]

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

◆  get_default()

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

Definition at line 355 of file solver_factory.cpp.

◆  get_dimacs()

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

Definition at line 375 of file solver_factory.cpp.

◆  get_external_sat()

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

Definition at line 401 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 468 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 513 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 137 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 112 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 445 of file solver_factory.cpp.

◆  no_beautification()

void solver_factoryt::no_beautification ( )
protected

Definition at line 577 of file solver_factory.cpp.

◆  no_incremental_check()

void solver_factoryt::no_incremental_check ( )
protected

Definition at line 586 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 102 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:

AltStyle によって変換されたページ (->オリジナル) /