CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions | Public Attributes | List of all members
bv_refinementt::approximationt Struct Referencefinal
+ 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()

bv_refinementt::approximationt::approximationt ( std::size_t  _id_nr)
inlineexplicit

Definition at line 65 of file bv_refinement.h.

Member Function Documentation

◆ add_over_assumption()

void bv_refinementt::approximationt::add_over_assumption ( literalt  l)

Definition at line 25 of file refine_arithmetic.cpp.

◆ add_under_assumption()

void bv_refinementt::approximationt::add_under_assumption ( literalt  l)

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: