cprover
cbmc_solverst Class Reference

#include <cbmc_solvers.h>

+ Collaboration diagram for cbmc_solverst:

Classes

class  solvert
 

Public Member Functions

 cbmc_solverst (const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler, bool _output_xml_in_refinement)
 
virtual std::unique_ptr< solvertget_solver ()
 
virtual ~cbmc_solverst ()
 

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 cbmc_solvers.h.

Constructor & Destructor Documentation

◆ cbmc_solverst()

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

Definition at line 31 of file cbmc_solvers.h.

◆ ~cbmc_solverst()

virtual cbmc_solverst::~cbmc_solverst ( )
inlinevirtual

Definition at line 116 of file cbmc_solvers.h.

Member Function Documentation

◆ get_bv_refinement()

std::unique_ptr< cbmc_solverst::solvert > cbmc_solverst::get_bv_refinement ( )
protected

Definition at line 105 of file cbmc_solvers.cpp.

◆ get_default()

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

Definition at line 62 of file cbmc_solvers.cpp.

◆ get_dimacs()

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

Definition at line 91 of file cbmc_solvers.cpp.

◆ get_smt2()

std::unique_ptr< cbmc_solverst::solvert > cbmc_solverst::get_smt2 ( smt2_dect::solvert  solver)
protected

Definition at line 160 of file cbmc_solvers.cpp.

◆ 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 35 of file cbmc_solvers.cpp.

◆ get_solver()

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

Definition at line 103 of file cbmc_solvers.h.

◆ get_string_refinement()

std::unique_ptr< cbmc_solverst::solvert > cbmc_solverst::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 141 of file cbmc_solvers.cpp.

◆ no_beautification()

void cbmc_solverst::no_beautification ( )
protected

Definition at line 237 of file cbmc_solvers.cpp.

◆ no_incremental_check()

void cbmc_solverst::no_incremental_check ( )
protected

Definition at line 246 of file cbmc_solvers.cpp.

Member Data Documentation

◆ message_handler

message_handlert& cbmc_solverst::message_handler
protected

Definition at line 124 of file cbmc_solvers.h.

◆ ns

namespacet cbmc_solverst::ns
protected

Definition at line 123 of file cbmc_solvers.h.

◆ options

const optionst& cbmc_solverst::options
protected

Definition at line 121 of file cbmc_solvers.h.

◆ output_xml_in_refinement

const bool cbmc_solverst::output_xml_in_refinement
protected

Definition at line 125 of file cbmc_solvers.h.

◆ symbol_table

const symbol_tablet& cbmc_solverst::symbol_table
protected

Definition at line 122 of file cbmc_solvers.h.


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