CBMC
Public Member Functions | Private Member Functions | Static Private Member Functions | Private Attributes | List of all members
value_set_evaluator Class Reference
+ Collaboration diagram for value_set_evaluator:

Public Member Functions

 value_set_evaluator (const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
 
abstract_object_pointert operator() () const
 

Private Member Functions

abstract_object_pointert transform () const
 
abstract_object_sett evaluate_each_combination (const std::vector< value_ranget > &value_ranges) const
 Evaluate expression for every combination of values in value_ranges. More...
 
void evaluate_combination (abstract_object_sett &results, const std::vector< value_ranget > &value_ranges, std::vector< abstract_object_pointert > &combination) const
 
exprt rewrite_expression (const std::vector< abstract_object_pointert > &ops) const
 
std::vector< value_ranget > operands_as_ranges () const
 

Static Private Member Functions

static bool is_constant_value (const abstract_object_pointert &v)
 
static abstract_object_pointert evaluate_conditional (const std::vector< value_ranget > &ops)
 

Private Attributes

const exprt & expression
 
const std::vector< abstract_object_pointert > & operands
 
const abstract_environmentt & environment
 
const namespacet & ns
 

Detailed Description

Definition at line 550 of file abstract_value_object.cpp.

Constructor & Destructor Documentation

◆ value_set_evaluator()

value_set_evaluator::value_set_evaluator ( const exprt &  e,
const std::vector< abstract_object_pointert > &  ops,
const abstract_environmentt &  env,
const namespacet &  n 
)
inline

Definition at line 553 of file abstract_value_object.cpp.

Member Function Documentation

◆ evaluate_combination()

void value_set_evaluator::evaluate_combination ( abstract_object_sett &  results,
const std::vector< value_ranget > &  value_ranges,
std::vector< abstract_object_pointert > &  combination 
) const
inlineprivate

Definition at line 593 of file abstract_value_object.cpp.

◆ evaluate_conditional()

static abstract_object_pointert value_set_evaluator::evaluate_conditional ( const std::vector< value_ranget > &  ops)
inlinestaticprivate

Definition at line 655 of file abstract_value_object.cpp.

◆ evaluate_each_combination()

abstract_object_sett value_set_evaluator::evaluate_each_combination ( const std::vector< value_ranget > &  value_ranges) const
inlineprivate

Evaluate expression for every combination of values in value_ranges.

<{1,2},{1},{1,2,3}> -> eval(1,1,1), eval(1,1,2), eval(1,1,3), eval(2,1,1), eval(2,1,2), eval(2,1,3).

Definition at line 585 of file abstract_value_object.cpp.

◆ is_constant_value()

static bool value_set_evaluator::is_constant_value ( const abstract_object_pointert &  v)
inlinestaticprivate

Definition at line 633 of file abstract_value_object.cpp.

◆ operands_as_ranges()

std::vector<value_ranget> value_set_evaluator::operands_as_ranges ( ) const
inlineprivate

Definition at line 639 of file abstract_value_object.cpp.

◆ operator()()

abstract_object_pointert value_set_evaluator::operator() ( void  ) const
inline

Definition at line 563 of file abstract_value_object.cpp.

◆ rewrite_expression()

exprt value_set_evaluator::rewrite_expression ( const std::vector< abstract_object_pointert > &  ops) const
inlineprivate

Definition at line 617 of file abstract_value_object.cpp.

◆ transform()

abstract_object_pointert value_set_evaluator::transform ( ) const
inlineprivate

Definition at line 569 of file abstract_value_object.cpp.

Member Data Documentation

◆ environment

const abstract_environmentt& value_set_evaluator::environment
private

Definition at line 682 of file abstract_value_object.cpp.

◆ expression

const exprt& value_set_evaluator::expression
private

Definition at line 680 of file abstract_value_object.cpp.

◆ ns

const namespacet& value_set_evaluator::ns
private

Definition at line 683 of file abstract_value_object.cpp.

◆ operands

const std::vector<abstract_object_pointert>& value_set_evaluator::operands
private

Definition at line 681 of file abstract_value_object.cpp.

The documentation for this class was generated from the following file: