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) | |
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, 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 34 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 96 of file disjunctive_polynomial_acceleration.h.
|
protected |
Definition at line 97 of file disjunctive_polynomial_acceleration.h.
|
inline |
Definition at line 37 of file disjunctive_polynomial_acceleration.h.
References build_fixed(), find_distinguishing_points(), acceleration_utilst::find_modified(), loop, loop_counter, modified, and utils.
|
virtual |
Implements loop_accelerationt.
Definition at line 49 of file disjunctive_polynomial_acceleration.cpp.
References goto_programt::add_instruction(), scratch_programt::assign(), ASSUME, path_acceleratort::changed_vars, acceleration_utilst::check_inductive(), path_acceleratort::clear(), depends_on_array(), path_acceleratort::dirty_vars, acceleration_utilst::do_arrays(), acceleration_utilst::do_assumptions(), acceleration_utilst::ensure_no_overflows(), expr2c(), acceleration_utilst::find_modified(), find_path(), fit_polynomial(), polynomial_acceleratort::fit_polynomial(), scratch_programt::fix_types(), acceleration_utilst::fresh_symbol(), from_integer(), goto_functions, goto_program, irept::id(), goto_programt::instructions, irept::is_nil(), loop, loop_counter, message_handler, modified, ns, goto_programt::output_instruction(), path_acceleratort::path, path_acceleratort::pure_accelerator, replace_expr(), simplify(), acceleration_utilst::stash_polynomials(), symbolt::symbol_expr(), symbol_table, exprt::type(), unsigned_poly_type(), and utils.
Referenced by acceleratet::accelerate_loop().
|
protected |
Definition at line 645 of file disjunctive_polynomial_acceleration.cpp.
References goto_programt::add_instruction(), scratch_programt::append(), scratch_programt::assign(), ASSUME, from_integer(), irept::is_nil(), join_types(), loop_counter, PRECONDITION, irept::swap(), and exprt::type().
Referenced by fit_polynomial().
|
protected |
Definition at line 855 of file disjunctive_polynomial_acceleration.cpp.
References goto_programt::add_instruction(), ASSUME, goto_programt::copy_from(), distinguishers, distinguishing_points, fixed, Forall_goto_program_instructions, acceleration_utilst::fresh_symbol(), goto_program, goto_programt::insert_after(), goto_programt::insert_before(), goto_programt::instructions, loop, loop_header, message_handler, PRECONDITION, remove_skip(), SKIP, symbolt::symbol_expr(), symbol_table, goto_programt::update(), and utils.
Referenced by disjunctive_polynomial_accelerationt().
|
protected |
Definition at line 776 of file disjunctive_polynomial_acceleration.cpp.
References distinguishing_points, scratch_programt::eval(), goto_programt::get_successors(), goto_program, INVARIANT, exprt::is_true(), loop, loop_header, and PRECONDITION.
Referenced by find_path(), and fit_polynomial().
|
protected |
Definition at line 743 of file disjunctive_polynomial_acceleration.cpp.
References cone_of_influencet::cone_of_influence(), fixed, and symbol_table.
Referenced by depends_on_array(), and fit_polynomial().
|
protected |
Definition at line 1017 of file disjunctive_polynomial_acceleration.cpp.
References cone_of_influence().
Referenced by accelerate().
|
protected |
Definition at line 751 of file disjunctive_polynomial_acceleration.cpp.
References distinguishers, distinguishing_points, acceleration_utilst::fresh_symbol(), goto_programt::get_successors(), goto_program, loop, symbolt::symbol_expr(), and utils.
Referenced by disjunctive_polynomial_accelerationt().
bool disjunctive_polynomial_accelerationt::find_path | ( | patht & | path | ) |
Definition at line 336 of file disjunctive_polynomial_acceleration.cpp.
References accelerated_paths, goto_programt::add_instruction(), scratch_programt::append(), ASSERT, scratch_programt::assume(), build_path(), scratch_programt::check_sat(), fixed, message_handler, record_path(), irept::swap(), and symbol_table.
Referenced by accelerate().
bool disjunctive_polynomial_accelerationt::fit_polynomial | ( | exprt & | target, |
polynomialt & | polynomial, | ||
patht & | path | ||
) |
Definition at line 397 of file disjunctive_polynomial_acceleration.cpp.
References accelerated_paths, goto_programt::add_instruction(), ASSERT, assert_for_values(), scratch_programt::assume(), build_path(), scratch_programt::check_sat(), cone_of_influence(), DECL, distinguishers, acceleration_utilst::ensure_no_overflows(), expr2c(), acceleration_utilst::extract_polynomial(), fixed, acceleration_utilst::fresh_symbol(), from_integer(), loop_counter, message_handler, ns, record_path(), signed_poly_type(), irept::swap(), symbolt::symbol_expr(), symbol_table, and utils.
Referenced by accelerate().
|
protected |
Definition at line 1002 of file disjunctive_polynomial_acceleration.cpp.
References accelerated_paths, distinguishers, scratch_programt::eval(), and exprt::is_true().
Referenced by find_path(), and fit_polynomial().
|
protected |
Definition at line 105 of file disjunctive_polynomial_acceleration.h.
Referenced by find_path(), fit_polynomial(), and record_path().
|
protected |
Definition at line 102 of file disjunctive_polynomial_acceleration.h.
Referenced by build_fixed(), find_distinguishing_points(), fit_polynomial(), and record_path().
|
protected |
Definition at line 101 of file disjunctive_polynomial_acceleration.h.
Referenced by build_fixed(), build_path(), and find_distinguishing_points().
|
protected |
Definition at line 104 of file disjunctive_polynomial_acceleration.h.
Referenced by build_fixed(), cone_of_influence(), find_path(), and fit_polynomial().
|
protected |
Definition at line 91 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate().
|
protected |
Definition at line 92 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), build_fixed(), build_path(), and find_distinguishing_points().
|
protected |
Definition at line 93 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), build_fixed(), build_path(), disjunctive_polynomial_accelerationt(), and find_distinguishing_points().
|
protected |
Definition at line 100 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), assert_for_values(), disjunctive_polynomial_accelerationt(), and fit_polynomial().
|
protected |
Definition at line 94 of file disjunctive_polynomial_acceleration.h.
Referenced by build_fixed(), and build_path().
|
protected |
Definition at line 69 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), build_fixed(), find_path(), and fit_polynomial().
|
protected |
Definition at line 103 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), and disjunctive_polynomial_accelerationt().
|
protected |
Definition at line 90 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), and fit_polynomial().
|
protected |
Definition at line 89 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), build_fixed(), cone_of_influence(), find_path(), and fit_polynomial().
|
protected |
Definition at line 99 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), build_fixed(), disjunctive_polynomial_accelerationt(), find_distinguishing_points(), and fit_polynomial().