cprover
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< solvertget_solver ()
 
virtual ~solver_factoryt ()
 

Protected Member Functions

std::unique_ptr< solvertget_default ()
 
std::unique_ptr< solvertget_dimacs ()
 
std::unique_ptr< solvertget_bv_refinement ()
 
std::unique_ptr< solvertget_string_refinement ()
 the string refinement adds to the bit vector refinement specifications for functions from the Java string library More...
 
std::unique_ptr< solvertget_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 optionstoptions
 
const symbol_tabletsymbol_table
 
namespacet ns
 
message_handlertmessage_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: