cprover
|
#include <disjunctive_polynomial_acceleration.h>
Public Member Functions | |
disjunctive_polynomial_accelerationt (message_handlert &message_handler, symbol_tablet &_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 > | 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) |
Definition at line 30 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 95 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 96 of file disjunctive_polynomial_acceleration.h.
|
inline |
Definition at line 33 of file disjunctive_polynomial_acceleration.h.
bool disjunctive_polynomial_accelerationt::accelerate | ( | path_acceleratort & | accelerator | ) |
Definition at line 33 of file disjunctive_polynomial_acceleration.cpp.
|
protected |
Definition at line 632 of file disjunctive_polynomial_acceleration.cpp.
|
protected |
Definition at line 838 of file disjunctive_polynomial_acceleration.cpp.
|
protected |
Definition at line 760 of file disjunctive_polynomial_acceleration.cpp.
|
protected |
Definition at line 729 of file disjunctive_polynomial_acceleration.cpp.
|
protected |
Definition at line 999 of file disjunctive_polynomial_acceleration.cpp.
|
protected |
Definition at line 737 of file disjunctive_polynomial_acceleration.cpp.
Definition at line 323 of file disjunctive_polynomial_acceleration.cpp.
bool disjunctive_polynomial_accelerationt::fit_polynomial | ( | exprt & | target, |
polynomialt & | polynomial, | ||
patht & | path | ||
) |
Definition at line 384 of file disjunctive_polynomial_acceleration.cpp.
|
protected |
Definition at line 984 of file disjunctive_polynomial_acceleration.cpp.
|
protected |
Definition at line 104 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 101 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 100 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 103 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 89 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 90 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 91 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 92 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 99 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 93 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 67 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 102 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 88 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 87 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 98 of file disjunctive_polynomial_acceleration.h.