Collaboration diagram for bv_refinementt::approximationt: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 |
| std::vector< exprt > | under_assumptions |
| std::vector< exprt > | over_assumptions |
| unsigned | under_state |
| unsigned | over_state |
| std::size_t | id_nr |
Detailed Description
Definition at line 62 of file bv_refinement.h.
Constructor & Destructor Documentation
◆ approximationt()
|
inlineexplicit |
Definition at line 65 of file bv_refinement.h.
Member Function Documentation
◆ add_over_assumption()
Definition at line 25 of file refine_arithmetic.cpp.
◆ add_under_assumption()
Definition at line 32 of file refine_arithmetic.cpp.
◆ as_string()
| std::string bv_refinementt::approximationt::as_string | ( | ) | const |
Definition at line 526 of file refine_arithmetic.cpp.
Member Data Documentation
◆ expr
| exprt bv_refinementt::approximationt::expr |
Definition at line 73 of file bv_refinement.h.
◆ id_nr
| std::size_t bv_refinementt::approximationt::id_nr |
Definition at line 90 of file bv_refinement.h.
◆ no_operands
| std::size_t bv_refinementt::approximationt::no_operands |
Definition at line 74 of file bv_refinement.h.
◆ op0_bv
| bvt bv_refinementt::approximationt::op0_bv |
Definition at line 76 of file bv_refinement.h.
◆ op0_value
| mp_integer bv_refinementt::approximationt::op0_value |
Definition at line 77 of file bv_refinement.h.
◆ op1_bv
| bvt bv_refinementt::approximationt::op1_bv |
Definition at line 76 of file bv_refinement.h.
◆ op1_value
| mp_integer bv_refinementt::approximationt::op1_value |
Definition at line 77 of file bv_refinement.h.
◆ op2_bv
| bvt bv_refinementt::approximationt::op2_bv |
Definition at line 76 of file bv_refinement.h.
◆ op2_value
| mp_integer bv_refinementt::approximationt::op2_value |
Definition at line 77 of file bv_refinement.h.
◆ over_assumptions
| std::vector<exprt> bv_refinementt::approximationt::over_assumptions |
Definition at line 80 of file bv_refinement.h.
◆ over_state
| unsigned bv_refinementt::approximationt::over_state |
Definition at line 83 of file bv_refinement.h.
◆ result_bv
| bvt bv_refinementt::approximationt::result_bv |
Definition at line 76 of file bv_refinement.h.
◆ result_value
| mp_integer bv_refinementt::approximationt::result_value |
Definition at line 77 of file bv_refinement.h.
◆ under_assumptions
| std::vector<exprt> bv_refinementt::approximationt::under_assumptions |
Definition at line 79 of file bv_refinement.h.
◆ under_state
| unsigned bv_refinementt::approximationt::under_state |
Definition at line 83 of file bv_refinement.h.
The documentation for this struct was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/refinement/bv_refinement.h
- /home/runner/work/cbmc/cbmc/src/solvers/refinement/refine_arithmetic.cpp
