cprover
|
Public Attributes | |
ui_message_handlert::uit | ui =ui_message_handlert::uit::PLAIN |
unsigned | max_node_refinement =5 |
Max number of times we refine a formula node. More... | |
bool | refine_arrays =true |
Enable array refinement. More... | |
bool | refine_arithmetic =true |
Enable arithmetic refinement. More... | |
Definition at line 24 of file bv_refinement.h.
unsigned bv_refinementt::configt::max_node_refinement =5 |
Max number of times we refine a formula node.
Definition at line 28 of file bv_refinement.h.
Referenced by bv_refinementt::check_SAT(), cbmc_solverst::get_bv_refinement(), and cbmc_solverst::get_string_refinement().
bool bv_refinementt::configt::refine_arithmetic =true |
Enable arithmetic refinement.
Definition at line 32 of file bv_refinement.h.
Referenced by bv_refinementt::convert_div(), bv_refinementt::convert_floatbv_op(), bv_refinementt::convert_mod(), bv_refinementt::convert_mult(), cbmc_solverst::get_bv_refinement(), and cbmc_solverst::get_string_refinement().
bool bv_refinementt::configt::refine_arrays =true |
Enable array refinement.
Definition at line 30 of file bv_refinement.h.
Referenced by bv_refinementt::arrays_overapproximated(), cbmc_solverst::get_bv_refinement(), cbmc_solverst::get_string_refinement(), and bv_refinementt::post_process_arrays().
ui_message_handlert::uit bv_refinementt::configt::ui =ui_message_handlert::uit::PLAIN |
Definition at line 26 of file bv_refinement.h.
Referenced by bv_refinementt::dec_solve(), cbmc_solverst::get_bv_refinement(), and cbmc_solverst::get_string_refinement().