cprover
|
#include <cbmc_solvers.h>
Classes | |
class | solvert |
Public Member Functions | |
cbmc_solverst (const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler) | |
virtual std::unique_ptr< solvert > | get_solver () |
virtual | ~cbmc_solverst () |
void | set_ui (ui_message_handlert::uit _ui) |
Protected Member Functions | |
std::unique_ptr< solvert > | get_default () |
std::unique_ptr< solvert > | get_dimacs () |
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_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 optionst & | options |
const symbol_tablet & | symbol_table |
namespacet | ns |
ui_message_handlert::uit | ui |
Additional Inherited Members |
Definition at line 32 of file cbmc_solvers.h.
|
inline |
Definition at line 35 of file cbmc_solvers.h.
|
inlinevirtual |
Definition at line 119 of file cbmc_solvers.h.
|
protected |
Definition at line 101 of file cbmc_solvers.cpp.
References optionst::get_bool_option(), messaget::get_message_handler(), optionst::get_unsigned_int_option(), bv_refinementt::configt::max_node_refinement, no_beautification(), bv_refinementt::infot::ns, ns, options, bv_refinementt::infot::prop, bv_refinementt::configt::refine_arithmetic, bv_refinementt::configt::refine_arrays, messaget::set_message_handler(), bv_refinementt::configt::ui, and ui.
Referenced by get_solver().
|
protected |
Definition at line 58 of file cbmc_solvers.cpp.
References optionst::get_bool_option(), messaget::get_message_handler(), optionst::get_option(), ns, options, solver(), boolbvt::U_ALL, and boolbvt::U_NONE.
Referenced by get_solver().
|
protected |
Definition at line 87 of file cbmc_solvers.cpp.
References messaget::get_message_handler(), optionst::get_option(), no_beautification(), no_incremental_check(), ns, and options.
Referenced by get_solver().
|
protected |
Definition at line 159 of file cbmc_solvers.cpp.
References messaget::eom(), messaget::error(), smt2_convt::GENERIC, optionst::get_bool_option(), messaget::get_message_handler(), optionst::get_option(), no_beautification(), ns, options, solver(), and widen().
Referenced by get_solver().
|
protected |
Uses the options to pick an SMT 2.0 solver.
Definition at line 34 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, options, smt2_convt::YICES, and smt2_convt::Z3.
Referenced by get_solver().
|
inlinevirtual |
Definition at line 106 of file cbmc_solvers.h.
References optionst::get_bool_option(), get_bv_refinement(), get_default(), get_dimacs(), get_smt2(), get_smt2_solver_type(), get_string_refinement(), and options.
|
protected |
the string refinement adds to the bit vector refinement specifications for functions from the Java string library
Definition at line 137 of file cbmc_solvers.cpp.
References DEFAULT_MAX_NB_REFINEMENT, optionst::get_bool_option(), messaget::get_message_handler(), optionst::get_signed_int_option(), optionst::get_unsigned_int_option(), bv_refinementt::configt::max_node_refinement, string_refinementt::configt::max_string_length, bv_refinementt::infot::ns, ns, options, bv_refinementt::infot::prop, bv_refinementt::configt::refine_arithmetic, bv_refinementt::configt::refine_arrays, string_refinementt::configt::refinement_bound, string_refinementt::configt::trace, bv_refinementt::configt::ui, and ui.
Referenced by get_solver().
|
protected |
Definition at line 237 of file cbmc_solvers.cpp.
References messaget::eom(), messaget::error(), optionst::get_bool_option(), and options.
Referenced by get_bv_refinement(), get_dimacs(), and get_smt2().
|
protected |
Definition at line 246 of file cbmc_solvers.cpp.
References messaget::eom(), messaget::error(), optionst::get_bool_option(), optionst::get_option(), and options.
Referenced by get_dimacs().
|
inline |
Definition at line 123 of file cbmc_solvers.h.
References ui.
Referenced by bmct::do_language_agnostic_bmc().
|
protected |
Definition at line 128 of file cbmc_solvers.h.
Referenced by get_bv_refinement(), get_default(), get_dimacs(), get_smt2(), and get_string_refinement().
|
protected |
Definition at line 126 of file cbmc_solvers.h.
Referenced by get_bv_refinement(), get_default(), get_dimacs(), get_smt2(), get_smt2_solver_type(), get_solver(), get_string_refinement(), no_beautification(), and no_incremental_check().
|
protected |
Definition at line 127 of file cbmc_solvers.h.
|
protected |
Definition at line 131 of file cbmc_solvers.h.
Referenced by get_bv_refinement(), get_string_refinement(), and set_ui().