cprover
disjunctive_polynomial_accelerationt Class Reference

#include <disjunctive_polynomial_acceleration.h>

Inheritance diagram for disjunctive_polynomial_accelerationt:
[legend]
Collaboration diagram for disjunctive_polynomial_accelerationt:
[legend]

Public Member Functions

 disjunctive_polynomial_accelerationt (symbol_tablet &_symbol_table, goto_functionst &_goto_functions, goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, goto_programt::targett _loop_header)
 
virtual 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, exprtdistinguish_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

symbol_tabletsymbol_table
 
namespacet ns
 
goto_functionstgoto_functions
 
goto_programtgoto_program
 
natural_loops_mutablet::natural_looptloop
 
goto_programt::targett loop_header
 
acceleration_utilst utils
 
exprt loop_counter
 
distinguish_mapt distinguishing_points
 
std::list< exprtdistinguishers
 
expr_sett modified
 
goto_programt fixed
 
std::list< distinguish_valuestaccelerated_paths
 

Detailed Description

Definition at line 33 of file disjunctive_polynomial_acceleration.h.

Member Typedef Documentation

§ distinguish_mapt

§ distinguish_valuest

Constructor & Destructor Documentation

§ disjunctive_polynomial_accelerationt()

disjunctive_polynomial_accelerationt::disjunctive_polynomial_accelerationt ( symbol_tablet _symbol_table,
goto_functionst _goto_functions,
goto_programt _goto_program,
natural_loops_mutablet::natural_loopt _loop,
goto_programt::targett  _loop_header 
)
inline

Member Function Documentation

§ accelerate()

§ 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

§ build_fixed()

§ build_path()

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

§ cone_of_influence()

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

§ depends_on_array()

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

§ find_distinguishing_points()

§ find_path()

§ fit_polynomial()

§ record_path()

void disjunctive_polynomial_accelerationt::record_path ( scratch_programt scratch_program)
protected

Member Data Documentation

§ accelerated_paths

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

Definition at line 100 of file disjunctive_polynomial_acceleration.h.

Referenced by find_path(), fit_polynomial(), and record_path().

§ distinguishers

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

§ distinguishing_points

distinguish_mapt disjunctive_polynomial_accelerationt::distinguishing_points
protected

§ fixed

goto_programt disjunctive_polynomial_accelerationt::fixed
protected

§ goto_functions

goto_functionst& disjunctive_polynomial_accelerationt::goto_functions
protected

Definition at line 86 of file disjunctive_polynomial_acceleration.h.

Referenced by accelerate().

§ goto_program

goto_programt& disjunctive_polynomial_accelerationt::goto_program
protected

§ loop

§ loop_counter

exprt disjunctive_polynomial_accelerationt::loop_counter
protected

§ loop_header

goto_programt::targett disjunctive_polynomial_accelerationt::loop_header
protected

Definition at line 89 of file disjunctive_polynomial_acceleration.h.

Referenced by build_fixed(), and build_path().

§ modified

expr_sett disjunctive_polynomial_accelerationt::modified
protected

§ ns

namespacet disjunctive_polynomial_accelerationt::ns
protected

Definition at line 85 of file disjunctive_polynomial_acceleration.h.

Referenced by accelerate(), and fit_polynomial().

§ symbol_table

symbol_tablet& disjunctive_polynomial_accelerationt::symbol_table
protected

§ utils

acceleration_utilst disjunctive_polynomial_accelerationt::utils
protected

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