CBMC
Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
disjunctive_polynomial_accelerationt Class Reference

#include <disjunctive_polynomial_acceleration.h>

+ Collaboration diagram for disjunctive_polynomial_accelerationt:

Public Member Functions

 disjunctive_polynomial_accelerationt (message_handlert &message_handler, symbol_table_baset &_symbol_table, goto_functionst &_goto_functions, goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, goto_programt::targett _loop_header, guard_managert &guard_manager)
 
bool accelerate (path_acceleratort &accelerator)
 
bool fit_polynomial (exprt &target, polynomialt &polynomial, patht &path)
 
bool find_path (patht &path)
 

Protected Types

typedef std::map< goto_programt::targett, exprt, goto_programt::target_less_than > distinguish_mapt
 
typedef std::map< exprt, bool > distinguish_valuest
 

Protected Member Functions

void assert_for_values (scratch_programt &program, std::map< exprt, exprt > &values, std::set< std::pair< expr_listt, exprt > > &coefficients, int num_unwindings, goto_programt &loop_body, exprt &target)
 
void cone_of_influence (const exprt &target, expr_sett &cone)
 
void find_distinguishing_points ()
 
void build_path (scratch_programt &scratch_program, patht &path)
 
void build_fixed ()
 
void record_path (scratch_programt &scratch_program)
 
bool depends_on_array (const exprt &e, exprt &array)
 

Protected Attributes

message_handlert & message_handler
 
symbol_table_baset & symbol_table
 
namespacet ns
 
goto_functionst & goto_functions
 
goto_programt & goto_program
 
guard_managert & guard_manager
 
natural_loops_mutablet::natural_loopt & loop
 
goto_programt::targett loop_header
 
acceleration_utilst utils
 
exprt loop_counter
 
distinguish_mapt distinguishing_points
 
std::list< symbol_exprt > distinguishers
 
expr_sett modified
 
goto_programt fixed
 
std::list< distinguish_valuest > accelerated_paths
 

Detailed Description

Definition at line 28 of file disjunctive_polynomial_acceleration.h.

Member Typedef Documentation

◆ distinguish_mapt

typedef std:: map<goto_programt::targett, exprt, goto_programt::target_less_than> disjunctive_polynomial_accelerationt::distinguish_mapt
protected

Definition at line 95 of file disjunctive_polynomial_acceleration.h.

◆ distinguish_valuest

typedef std::map<exprt, bool> disjunctive_polynomial_accelerationt::distinguish_valuest
protected

Definition at line 96 of file disjunctive_polynomial_acceleration.h.

Constructor & Destructor Documentation

◆ disjunctive_polynomial_accelerationt()

disjunctive_polynomial_accelerationt::disjunctive_polynomial_accelerationt ( message_handlert &  message_handler,
symbol_table_baset &  _symbol_table,
goto_functionst &  _goto_functions,
goto_programt &  _goto_program,
natural_loops_mutablet::natural_loopt &  _loop,
goto_programt::targett  _loop_header,
guard_managert &  guard_manager 
)
inline

Definition at line 31 of file disjunctive_polynomial_acceleration.h.

Member Function Documentation

◆ accelerate()

bool disjunctive_polynomial_accelerationt::accelerate ( path_acceleratort &  accelerator)

Definition at line 37 of file disjunctive_polynomial_acceleration.cpp.

◆ assert_for_values()

void disjunctive_polynomial_accelerationt::assert_for_values ( scratch_programt &  program,
std::map< exprt, exprt > &  values,
std::set< std::pair< expr_listt, exprt > > &  coefficients,
int  num_unwindings,
goto_programt &  loop_body,
exprt &  target 
)
protected

Definition at line 634 of file disjunctive_polynomial_acceleration.cpp.

◆ build_fixed()

void disjunctive_polynomial_accelerationt::build_fixed ( )
protected

Definition at line 840 of file disjunctive_polynomial_acceleration.cpp.

◆ build_path()

void disjunctive_polynomial_accelerationt::build_path ( scratch_programt &  scratch_program,
patht &  path 
)
protected

Definition at line 762 of file disjunctive_polynomial_acceleration.cpp.

◆ cone_of_influence()

void disjunctive_polynomial_accelerationt::cone_of_influence ( const exprt &  target,
expr_sett &  cone 
)
protected

Definition at line 731 of file disjunctive_polynomial_acceleration.cpp.

◆ depends_on_array()

bool disjunctive_polynomial_accelerationt::depends_on_array ( const exprt &  e,
exprt &  array 
)
protected

Definition at line 1001 of file disjunctive_polynomial_acceleration.cpp.

◆ find_distinguishing_points()

void disjunctive_polynomial_accelerationt::find_distinguishing_points ( )
protected

Definition at line 739 of file disjunctive_polynomial_acceleration.cpp.

◆ find_path()

bool disjunctive_polynomial_accelerationt::find_path ( patht &  path)

Definition at line 325 of file disjunctive_polynomial_acceleration.cpp.

◆ fit_polynomial()

bool disjunctive_polynomial_accelerationt::fit_polynomial ( exprt &  target,
polynomialt &  polynomial,
patht &  path 
)

Definition at line 386 of file disjunctive_polynomial_acceleration.cpp.

◆ record_path()

void disjunctive_polynomial_accelerationt::record_path ( scratch_programt &  scratch_program)
protected

Definition at line 986 of file disjunctive_polynomial_acceleration.cpp.

Member Data Documentation

◆ accelerated_paths

std::list<distinguish_valuest> disjunctive_polynomial_accelerationt::accelerated_paths
protected

Definition at line 104 of file disjunctive_polynomial_acceleration.h.

◆ distinguishers

std::list<symbol_exprt> disjunctive_polynomial_accelerationt::distinguishers
protected

Definition at line 101 of file disjunctive_polynomial_acceleration.h.

◆ distinguishing_points

distinguish_mapt disjunctive_polynomial_accelerationt::distinguishing_points
protected

Definition at line 100 of file disjunctive_polynomial_acceleration.h.

◆ fixed

goto_programt disjunctive_polynomial_accelerationt::fixed
protected

Definition at line 103 of file disjunctive_polynomial_acceleration.h.

◆ goto_functions

goto_functionst& disjunctive_polynomial_accelerationt::goto_functions
protected

Definition at line 87 of file disjunctive_polynomial_acceleration.h.

◆ goto_program

goto_programt& disjunctive_polynomial_accelerationt::goto_program
protected

Definition at line 88 of file disjunctive_polynomial_acceleration.h.

◆ guard_manager

guard_managert& disjunctive_polynomial_accelerationt::guard_manager
protected

Definition at line 89 of file disjunctive_polynomial_acceleration.h.

◆ loop

natural_loops_mutablet::natural_loopt& disjunctive_polynomial_accelerationt::loop
protected

Definition at line 90 of file disjunctive_polynomial_acceleration.h.

◆ loop_counter

exprt disjunctive_polynomial_accelerationt::loop_counter
protected

Definition at line 99 of file disjunctive_polynomial_acceleration.h.

◆ loop_header

goto_programt::targett disjunctive_polynomial_accelerationt::loop_header
protected

Definition at line 91 of file disjunctive_polynomial_acceleration.h.

◆ message_handler

message_handlert& disjunctive_polynomial_accelerationt::message_handler
protected

Definition at line 65 of file disjunctive_polynomial_acceleration.h.

◆ modified

expr_sett disjunctive_polynomial_accelerationt::modified
protected

Definition at line 102 of file disjunctive_polynomial_acceleration.h.

◆ ns

namespacet disjunctive_polynomial_accelerationt::ns
protected

Definition at line 86 of file disjunctive_polynomial_acceleration.h.

◆ symbol_table

symbol_table_baset& disjunctive_polynomial_accelerationt::symbol_table
protected

Definition at line 85 of file disjunctive_polynomial_acceleration.h.

◆ utils

acceleration_utilst disjunctive_polynomial_accelerationt::utils
protected

Definition at line 98 of file disjunctive_polynomial_acceleration.h.

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