cprover
cbmc_solverst Class Reference

#include <cbmc_solvers.h>

Inheritance diagram for cbmc_solverst:
[legend]
Collaboration diagram for cbmc_solverst:
[legend]

Classes

class  solvert
 

Public Member Functions

 cbmc_solverst (const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler)
 
virtual std::unique_ptr< solvertget_solver ()
 
virtual ~cbmc_solverst ()
 
void set_ui (language_uit::uit _ui)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Protected Member Functions

solvertget_default ()
 Get the default decision procedure. More...
 
solvertget_dimacs ()
 
solvertget_bv_refinement ()
 
solvertget_smt1 (smt1_dect::solvert solver)
 
solvertget_smt2 (smt2_dect::solvert solver)
 
smt1_dect::solvert get_smt1_solver_type () const
 Uses the options to pick an SMT 1.2 solver. More...
 
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
 
language_uit::uit ui
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 33 of file cbmc_solvers.h.

Constructor & Destructor Documentation

§ cbmc_solverst()

cbmc_solverst::cbmc_solverst ( const optionst _options,
const symbol_tablet _symbol_table,
message_handlert _message_handler 
)
inline

Definition at line 36 of file cbmc_solvers.h.

§ ~cbmc_solverst()

virtual cbmc_solverst::~cbmc_solverst ( )
inlinevirtual

Definition at line 124 of file cbmc_solvers.h.

Member Function Documentation

§ get_bv_refinement()

§ get_default()

§ get_dimacs()

§ get_smt1()

§ get_smt1_solver_type()

smt1_dect::solvert cbmc_solverst::get_smt1_solver_type ( ) const
protected

Uses the options to pick an SMT 1.2 solver.

Returns
An smt1_dect::solvert giving the solver to use.

Definition at line 35 of file cbmc_solvers.cpp.

References optionst::get_bool_option(), and options.

Referenced by get_solver().

§ get_smt2()

§ get_smt2_solver_type()

smt2_dect::solvert cbmc_solverst::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 63 of file cbmc_solvers.cpp.

References smt2_convt::BOOLECTOR, smt2_convt::CVC3, smt2_convt::CVC4, smt2_convt::GENERIC, optionst::get_bool_option(), smt2_convt::MATHSAT, smt2_convt::OPENSMT, options, smt2_convt::YICES, and smt2_convt::Z3.

Referenced by get_solver().

§ get_solver()

virtual std::unique_ptr<solvert> cbmc_solverst::get_solver ( )
inlinevirtual

§ no_beautification()

void cbmc_solverst::no_beautification ( )
protected

§ no_incremental_check()

void cbmc_solverst::no_incremental_check ( )
protected

§ set_ui()

void cbmc_solverst::set_ui ( language_uit::uit  _ui)
inline

Definition at line 128 of file cbmc_solvers.h.

References ui.

Referenced by cbmc_parse_optionst::doit().

Member Data Documentation

§ ns

namespacet cbmc_solverst::ns
protected

Definition at line 133 of file cbmc_solvers.h.

Referenced by get_bv_refinement(), get_default(), get_dimacs(), get_smt1(), and get_smt2().

§ options

§ symbol_table

const symbol_tablet& cbmc_solverst::symbol_table
protected

Definition at line 132 of file cbmc_solvers.h.

§ ui

language_uit::uit cbmc_solverst::ui
protected

Definition at line 136 of file cbmc_solvers.h.

Referenced by get_bv_refinement(), and set_ui().


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