cprover
value_set_abstract_object.cpp File Reference

Value Set Abstract Object. More...

+ Include dependency graph for value_set_abstract_object.cpp:

Go to the source code of this file.

Classes

class  value_set_index_ranget
 

Functions

index_range_ptrt make_value_set_index_range (const abstract_object_sett &vals)
 
exprt rewrite_expression (const exprt &expr, const std::vector< abstract_object_pointert > &ops)
 
std::vector< abstract_object_settunwrap_operands (const std::vector< abstract_object_pointert > &operands)
 
abstract_object_sett unwrap_and_extract_values (const abstract_object_sett &values)
 
abstract_object_pointert maybe_extract_single_value (const abstract_object_pointert &maybe_singleton)
 Helper for converting singleton value sets into its only value. More...
 
abstract_object_pointert maybe_unwrap_context (const abstract_object_pointert &maybe_wrapped)
 Helper for converting context objects into its abstract-value children maybe_wrapped: either an abstract value (or a set of those) or one wrapped in a context. More...
 
template<typename Con , typename F >
void apply_comb (const std::vector< Con > &super_con, std::vector< typename Con::value_type > &sub_con, F f)
 Recursively construct a combination sub_con from super_con and once constructed call f. More...
 
template<typename Con , typename F >
void for_each_comb (const std::vector< Con > &super_con, F f)
 Call the function f on every combination of elements in super_con. More...
 

Detailed Description

Value Set Abstract Object.

Definition in file value_set_abstract_object.cpp.

Function Documentation

◆ apply_comb()

template<typename Con , typename F >
void apply_comb ( const std::vector< Con > &  super_con,
std::vector< typename Con::value_type > &  sub_con,
f 
)

Recursively construct a combination sub_con from super_con and once constructed call f.

Parameters
super_convector of some containers storing the values
sub_conthe one combination being currently constructed
fcallable with side-effects

Definition at line 82 of file value_set_abstract_object.cpp.

◆ for_each_comb()

template<typename Con , typename F >
void for_each_comb ( const std::vector< Con > &  super_con,
f 
)

Call the function f on every combination of elements in super_con.

Hence the arity of f is super_con.size(). <{1,2},{1},{1,2,3}> -> f(1,1,1), f(1,1,2), f(1,1,3), f(2,1,1), f(2,1,2), f(2,1,3).

Parameters
super_convector of some containers storing the values
fcallable with side-effects

Definition at line 107 of file value_set_abstract_object.cpp.

◆ make_value_set_index_range()

index_range_ptrt make_value_set_index_range ( const abstract_object_sett vals)

Definition at line 48 of file value_set_abstract_object.cpp.

◆ maybe_extract_single_value()

abstract_object_pointert maybe_extract_single_value ( const abstract_object_pointert maybe_singleton)

Helper for converting singleton value sets into its only value.

maybe_singleton: either a set of abstract values or a single value

Returns
an abstract value without context

Definition at line 362 of file value_set_abstract_object.cpp.

◆ maybe_unwrap_context()

abstract_object_pointert maybe_unwrap_context ( const abstract_object_pointert maybe_wrapped)

Helper for converting context objects into its abstract-value children maybe_wrapped: either an abstract value (or a set of those) or one wrapped in a context.

Returns
an abstract value without context (though it might be as set)

Definition at line 379 of file value_set_abstract_object.cpp.

◆ rewrite_expression()

exprt rewrite_expression ( const exprt expr,
const std::vector< abstract_object_pointert > &  ops 
)

Definition at line 321 of file value_set_abstract_object.cpp.

◆ unwrap_and_extract_values()

abstract_object_sett unwrap_and_extract_values ( const abstract_object_sett values)

Definition at line 349 of file value_set_abstract_object.cpp.

◆ unwrap_operands()

std::vector< abstract_object_sett > unwrap_operands ( const std::vector< abstract_object_pointert > &  operands)

Definition at line 333 of file value_set_abstract_object.cpp.