cprover
|
#include <bv_refinement.h>
Public Member Functions | |
approximationt (std::size_t _id_nr) | |
approximationt () | |
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 51 of file bv_refinement.h.
|
inlineexplicit |
Definition at line 54 of file bv_refinement.h.
|
inline |
Definition at line 70 of file bv_refinement.h.
References add_over_assumption(), add_under_assumption(), and as_string().
Referenced by bv_refinementt::add_approximation().
void bv_refinementt::approximationt::add_over_assumption | ( | literalt | l | ) |
Definition at line 24 of file refine_arithmetic.cpp.
References literalt::is_constant(), and over_assumptions.
Referenced by approximationt().
void bv_refinementt::approximationt::add_under_assumption | ( | literalt | l | ) |
Definition at line 31 of file refine_arithmetic.cpp.
References literalt::is_constant(), and under_assumptions.
Referenced by approximationt(), bv_refinementt::check_UNSAT(), and bv_refinementt::initialize().
std::string bv_refinementt::approximationt::as_string | ( | ) | const |
Definition at line 526 of file refine_arithmetic.cpp.
References expr, from_expr(), irept::id(), id2string(), and id_nr.
Referenced by approximationt(), bv_refinementt::check_SAT(), and bv_refinementt::check_UNSAT().
exprt bv_refinementt::approximationt::expr |
Definition at line 58 of file bv_refinement.h.
Referenced by bv_refinementt::add_approximation(), as_string(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), and bv_refinementt::get_values().
std::size_t bv_refinementt::approximationt::id_nr |
Definition at line 79 of file bv_refinement.h.
Referenced by as_string().
std::size_t bv_refinementt::approximationt::no_operands |
Definition at line 59 of file bv_refinement.h.
Referenced by bv_refinementt::add_approximation().
bvt bv_refinementt::approximationt::op0_bv |
Definition at line 61 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 62 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 61 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 62 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 61 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 62 of file bv_refinement.h.
Referenced by bv_refinementt::get_values().
bvt bv_refinementt::approximationt::over_assumptions |
Definition at line 65 of file bv_refinement.h.
Referenced by add_over_assumption(), and bv_refinementt::check_SAT().
unsigned bv_refinementt::approximationt::over_state |
Definition at line 68 of file bv_refinement.h.
Referenced by bv_refinementt::check_SAT(), and bv_refinementt::initialize().
bvt bv_refinementt::approximationt::result_bv |
Definition at line 61 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 62 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 64 of file bv_refinement.h.
Referenced by add_under_assumption(), bv_refinementt::check_UNSAT(), bv_refinementt::initialize(), and bv_refinementt::is_in_conflict().
unsigned bv_refinementt::approximationt::under_state |
Definition at line 68 of file bv_refinement.h.
Referenced by bv_refinementt::check_UNSAT(), and bv_refinementt::initialize().