12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_H 72 std::map<exprt, exprt> &values,
73 std::set<std::pair<expr_listt, exprt> > &coefficients,
108 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_H goto_programt::targett loop_header
void build_path(scratch_programt &scratch_program, patht &path)
Goto Programs with Functions.
void record_path(scratch_programt &scratch_program)
bool depends_on_array(const exprt &e, exprt &array)
std::set< goto_programt::targett > natural_loopt
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)
std::list< symbol_exprt > distinguishers
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)
bool accelerate(path_acceleratort &accelerator)
std::unordered_set< exprt, irep_hash > expr_sett
instructionst::iterator targett
goto_functionst & goto_functions
symbol_tablet & symbol_table
std::list< path_nodet > patht
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
message_handlert & message_handler
void find_modified(const patht &path, expr_sett &modified)
A collection of goto functions.
std::map< exprt, bool > distinguish_valuest
std::map< goto_programt::targett, exprt > distinguish_mapt
A generic container class for the GOTO intermediate representation of one function.
acceleration_utilst utils
Base class for all expressions.
natural_loops_mutablet::natural_loopt & loop
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
distinguish_mapt distinguishing_points
bool find_path(patht &path)
std::list< distinguish_valuest > accelerated_paths
void cone_of_influence(const exprt &target, expr_sett &cone)
Compute natural loops in a goto_function.
goto_programt & goto_program
void find_distinguishing_points()