bv_refinementt::approximationt Struct Reference

#include <bv_refinement.h>

Collaboration diagram for bv_refinementt::approximationt:

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

Definition at line 70 of file bv_refinement.h.

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.

add_under_assumption()

void bv_refinementt::approximationt::add_under_assumption

(

literalt

l

)

Definition at line 31 of file refine_arithmetic.cpp.

References literalt::is_constant().

Referenced by bv_refinementt::check_UNSAT(), and bv_refinementt::initialize().

as_string()

std::string bv_refinementt::approximationt::as_string

(

)

const

Definition at line 526 of file refine_arithmetic.cpp.

References from_expr(), and id2string().

Referenced by bv_refinementt::check_SAT(), and bv_refinementt::check_UNSAT().

Member Data Documentation

expr

exprt bv_refinementt::approximationt::expr

Definition at line 58 of file bv_refinement.h.

Referenced by bv_refinementt::add_approximation(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), and bv_refinementt::get_values().

id_nr

std::size_t bv_refinementt::approximationt::id_nr

Definition at line 79 of file bv_refinement.h.

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

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

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

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

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

Definition at line 61 of file bv_refinement.h.

Referenced by bv_refinementt::add_approximation(), and bv_refinementt::get_values().

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

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

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

Definition at line 64 of file bv_refinement.h.

Referenced by bv_refinementt::check_UNSAT(), bv_refinementt::initialize(), and bv_refinementt::is_in_conflict().

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:

• solvers/refinement/bv_refinement.h
• solvers/refinement/refine_arithmetic.cpp