cprover
bv_refinementt::approximationt Struct Reference

#include <bv_refinement.h>

Collaboration diagram for bv_refinementt::approximationt:
[legend]

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
 

Detailed Description

Definition at line 51 of file bv_refinement.h.

Constructor & Destructor Documentation

§ approximationt() [1/2]

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

Definition at line 54 of file bv_refinement.h.

§ approximationt() [2/2]

bv_refinementt::approximationt::approximationt ( )
inline

Member Function Documentation

§ add_over_assumption()

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().

§ add_under_assumption()

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

§ as_string()

std::string bv_refinementt::approximationt::as_string ( ) const

Member Data Documentation

§ expr

§ id_nr

std::size_t bv_refinementt::approximationt::id_nr

Definition at line 79 of file bv_refinement.h.

Referenced by as_string().

§ no_operands

std::size_t bv_refinementt::approximationt::no_operands

Definition at line 59 of file bv_refinement.h.

Referenced by bv_refinementt::add_approximation().

§ op0_bv

§ op0_value

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().

§ op1_bv

§ op1_value

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().

§ op2_bv

bvt bv_refinementt::approximationt::op2_bv

§ op2_value

mp_integer bv_refinementt::approximationt::op2_value

Definition at line 62 of file bv_refinement.h.

Referenced by bv_refinementt::get_values().

§ over_assumptions

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().

§ over_state

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().

§ result_bv

§ result_value

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().

§ under_assumptions

bvt bv_refinementt::approximationt::under_assumptions

§ under_state

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().


The documentation for this struct was generated from the following files: