cprover
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_rangetoperands_as_ranges () const
 

Static Private Member Functions

static bool is_constant_value (const abstract_object_pointert &v)
 
static abstract_object_sett unwrap_and_extract_values (const abstract_object_sett &values)
 
static abstract_object_pointert maybe_extract_single_value (const abstract_object_pointert &maybe_singleton)
 
static abstract_object_pointert resolve_values (const abstract_object_sett &new_values)
 
static abstract_object_pointert make_interval (const abstract_object_sett &values)
 
static abstract_object_pointert make_value_set (const abstract_object_sett &values)
 
static abstract_object_pointert evaluate_conditional (const std::vector< value_ranget > &ops)
 

Private Attributes

const exprtexpression
 
const std::vector< abstract_object_pointert > & operands
 
const abstract_environmenttenvironment
 
const namespacetns
 

Detailed Description

Definition at line 492 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 495 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 535 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 527 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 575 of file abstract_value_object.cpp.

◆ make_interval()

static abstract_object_pointert value_set_evaluator::make_interval ( const abstract_object_sett values)
inlinestaticprivate

Definition at line 640 of file abstract_value_object.cpp.

◆ make_value_set()

static abstract_object_pointert value_set_evaluator::make_value_set ( const abstract_object_sett values)
inlinestaticprivate

Definition at line 646 of file abstract_value_object.cpp.

◆ maybe_extract_single_value()

static abstract_object_pointert value_set_evaluator::maybe_extract_single_value ( const abstract_object_pointert maybe_singleton)
inlinestaticprivate

Definition at line 610 of file abstract_value_object.cpp.

◆ operands_as_ranges()

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

Definition at line 581 of file abstract_value_object.cpp.

◆ operator()()

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

Definition at line 505 of file abstract_value_object.cpp.

◆ resolve_values()

static abstract_object_pointert value_set_evaluator::resolve_values ( const abstract_object_sett new_values)
inlinestaticprivate

Definition at line 627 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 559 of file abstract_value_object.cpp.

◆ transform()

abstract_object_pointert value_set_evaluator::transform ( ) const
inlineprivate

Definition at line 511 of file abstract_value_object.cpp.

◆ unwrap_and_extract_values()

static abstract_object_sett value_set_evaluator::unwrap_and_extract_values ( const abstract_object_sett values)
inlinestaticprivate

Definition at line 597 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: