cprover
|
Public Member Functions | |
approximationt (std::size_t _id_nr) | |
std::string | as_string () const |
void | add_over_assumption (literalt l) |
void | add_under_assumption (literalt l) |
Public Attributes | |
exprt | expr |
std::size_t | no_operands |
bvt | op0_bv |
bvt | op1_bv |
bvt | op2_bv |
bvt | result_bv |
mp_integer | op0_value |
mp_integer | op1_value |
mp_integer | op2_value |
mp_integer | result_value |
bvt | under_assumptions |
bvt | over_assumptions |
unsigned | under_state |
unsigned | over_state |
std::size_t | id_nr |
Definition at line 65 of file bv_refinement.h.
|
inlineexplicit |
Definition at line 68 of file bv_refinement.h.
void bv_refinementt::approximationt::add_over_assumption | ( | literalt | l | ) |
Definition at line 25 of file refine_arithmetic.cpp.
References literalt::is_constant(), and over_assumptions.
void bv_refinementt::approximationt::add_under_assumption | ( | literalt | l | ) |
Definition at line 32 of file refine_arithmetic.cpp.
References literalt::is_constant().
Referenced by bv_refinementt::check_UNSAT(), and bv_refinementt::initialize().
std::string bv_refinementt::approximationt::as_string | ( | ) | const |
Definition at line 529 of file refine_arithmetic.cpp.
References from_expr(), id2string(), and to_string().
Referenced by bv_refinementt::check_SAT(), and bv_refinementt::check_UNSAT().
exprt bv_refinementt::approximationt::expr |
Definition at line 76 of file bv_refinement.h.
Referenced by bv_refinementt::add_approximation(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), and bv_refinementt::get_values().
std::size_t bv_refinementt::approximationt::id_nr |
Definition at line 93 of file bv_refinement.h.
std::size_t bv_refinementt::approximationt::no_operands |
Definition at line 77 of file bv_refinement.h.
Referenced by bv_refinementt::add_approximation().
bvt bv_refinementt::approximationt::op0_bv |
Definition at line 79 of file bv_refinement.h.
Referenced by bv_refinementt::add_approximation(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), bv_refinementt::convert_mult(), bv_refinementt::get_values(), and bv_refinementt::initialize().
mp_integer bv_refinementt::approximationt::op0_value |
Definition at line 80 of file bv_refinement.h.
Referenced by bv_refinementt::check_SAT(), and bv_refinementt::get_values().
bvt bv_refinementt::approximationt::op1_bv |
Definition at line 79 of file bv_refinement.h.
Referenced by bv_refinementt::add_approximation(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), bv_refinementt::convert_mult(), bv_refinementt::get_values(), and bv_refinementt::initialize().
mp_integer bv_refinementt::approximationt::op1_value |
Definition at line 80 of file bv_refinement.h.
Referenced by bv_refinementt::check_SAT(), and bv_refinementt::get_values().
bvt bv_refinementt::approximationt::op2_bv |
Definition at line 79 of file bv_refinement.h.
Referenced by bv_refinementt::add_approximation(), and bv_refinementt::get_values().
mp_integer bv_refinementt::approximationt::op2_value |
Definition at line 80 of file bv_refinement.h.
Referenced by bv_refinementt::get_values().
bvt bv_refinementt::approximationt::over_assumptions |
Definition at line 83 of file bv_refinement.h.
Referenced by add_over_assumption(), and bv_refinementt::check_SAT().
unsigned bv_refinementt::approximationt::over_state |
Definition at line 86 of file bv_refinement.h.
Referenced by bv_refinementt::check_SAT(), and bv_refinementt::initialize().
bvt bv_refinementt::approximationt::result_bv |
Definition at line 79 of file bv_refinement.h.
Referenced by bv_refinementt::add_approximation(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), bv_refinementt::convert_mult(), and bv_refinementt::get_values().
mp_integer bv_refinementt::approximationt::result_value |
Definition at line 80 of file bv_refinement.h.
Referenced by bv_refinementt::check_SAT(), and bv_refinementt::get_values().
bvt bv_refinementt::approximationt::under_assumptions |
Definition at line 82 of file bv_refinement.h.
Referenced by bv_refinementt::check_UNSAT(), bv_refinementt::conflicts_with(), and bv_refinementt::initialize().
unsigned bv_refinementt::approximationt::under_state |
Definition at line 86 of file bv_refinement.h.
Referenced by bv_refinementt::check_UNSAT(), and bv_refinementt::initialize().