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 (language_uit::uit _ui) |
Protected Member Functions | |
solvert * | get_default () |
Get the default decision procedure. More... | |
solvert * | get_dimacs () |
solvert * | get_bv_refinement () |
solvert * | get_smt1 (smt1_dect::solvert solver) |
solvert * | get_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 optionst & | options |
const symbol_tablet & | symbol_table |
namespacet | ns |
language_uit::uit | ui |
Additional Inherited Members |
Definition at line 33 of file cbmc_solvers.h.
|
inline |
Definition at line 36 of file cbmc_solvers.h.
|
inlinevirtual |
Definition at line 124 of file cbmc_solvers.h.
|
protected |
Definition at line 132 of file cbmc_solvers.cpp.
References bv_refinementt::do_arithmetic_refinement, bv_refinementt::do_array_refinement, optionst::get_bool_option(), messaget::get_message_handler(), optionst::get_option(), optionst::get_unsigned_int_option(), bv_refinementt::max_node_refinement, no_beautification(), ns, options, messaget::set_message_handler(), bv_refinementt::set_ui(), and ui.
Referenced by get_solver().
|
protected |
Get the default decision procedure.
Definition at line 90 of file cbmc_solvers.cpp.
References optionst::get_bool_option(), messaget::get_message_handler(), optionst::get_option(), ns, options, cbmc_solverst::solvert::prop(), messaget::set_message_handler(), cbmc_solverst::solvert::set_prop(), cbmc_solverst::solvert::set_prop_conv(), boolbvt::U_ALL, boolbvt::U_NONE, and boolbvt::unbounded_array.
Referenced by get_solver().
|
protected |
Definition at line 119 of file cbmc_solvers.cpp.
References messaget::get_message_handler(), optionst::get_option(), no_beautification(), no_incremental_check(), ns, options, and messaget::set_message_handler().
Referenced by get_solver().
|
protected |
Definition at line 163 of file cbmc_solvers.cpp.
References CBMC_VERSION, messaget::eom(), messaget::error(), messaget::get_message_handler(), optionst::get_option(), no_beautification(), no_incremental_check(), ns, options, messaget::set_message_handler(), and widen().
Referenced by get_solver().
|
protected |
Uses the options to pick an SMT 1.2 solver.
Definition at line 35 of file cbmc_solvers.cpp.
References optionst::get_bool_option(), and options.
Referenced by get_solver().
|
protected |
Definition at line 232 of file cbmc_solvers.cpp.
References CBMC_VERSION, messaget::eom(), messaget::error(), smt2_convt::GENERIC, optionst::get_bool_option(), messaget::get_message_handler(), optionst::get_option(), no_beautification(), ns, options, messaget::set_message_handler(), smt2_convt::use_FPA_theory, and widen().
Referenced by get_solver().
|
protected |
Uses the options to pick an SMT 2.0 solver.
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().
|
inlinevirtual |
Definition at line 106 of file cbmc_solvers.h.
References optionst::get_bool_option(), get_bv_refinement(), get_default(), get_dimacs(), get_smt1(), get_smt1_solver_type(), get_smt2(), get_smt2_solver_type(), and options.
Referenced by cbmc_parse_optionst::doit().
|
protected |
Definition at line 309 of file cbmc_solvers.cpp.
References messaget::eom(), messaget::error(), optionst::get_bool_option(), and options.
Referenced by get_bv_refinement(), get_dimacs(), get_smt1(), and get_smt2().
|
protected |
Definition at line 318 of file cbmc_solvers.cpp.
References messaget::eom(), messaget::error(), optionst::get_bool_option(), optionst::get_option(), and options.
Referenced by get_dimacs(), and get_smt1().
|
inline |
Definition at line 128 of file cbmc_solvers.h.
References ui.
Referenced by cbmc_parse_optionst::doit().
|
protected |
Definition at line 133 of file cbmc_solvers.h.
Referenced by get_bv_refinement(), get_default(), get_dimacs(), get_smt1(), and get_smt2().
|
protected |
Definition at line 131 of file cbmc_solvers.h.
Referenced by get_bv_refinement(), get_default(), get_dimacs(), get_smt1(), get_smt1_solver_type(), get_smt2(), get_smt2_solver_type(), get_solver(), no_beautification(), and no_incremental_check().
|
protected |
Definition at line 132 of file cbmc_solvers.h.
|
protected |
Definition at line 136 of file cbmc_solvers.h.
Referenced by get_bv_refinement(), and set_ui().