cprover
|
#include <disjunctive_polynomial_acceleration.h>
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, 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 33 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.
|
inline |
Definition at line 36 of file disjunctive_polynomial_acceleration.h.
References accelerate(), assert_for_values(), build_fixed(), build_path(), cone_of_influence(), depends_on_array(), find_distinguishing_points(), acceleration_utilst::find_modified(), find_path(), fit_polynomial(), loop, loop_counter, modified, record_path(), and utils.
|
virtual |
Implements loop_accelerationt.
Definition at line 50 of file disjunctive_polynomial_acceleration.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), scratch_programt::assign(), ASSUME, path_acceleratort::changed_vars, acceleration_utilst::check_inductive(), path_acceleratort::clear(), exprt::copy_to_operands(), 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_program_templatet< codeT, guardT >::instructions, irept::is_nil(), loop, loop_counter, 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(), and disjunctive_polynomial_accelerationt().
|
protected |
Definition at line 652 of file disjunctive_polynomial_acceleration.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), scratch_programt::append(), scratch_programt::assign(), ASSUME, from_integer(), irept::is_nil(), join_types(), loop_counter, irept::swap(), and exprt::type().
Referenced by disjunctive_polynomial_accelerationt(), and fit_polynomial().
|
protected |
Definition at line 862 of file disjunctive_polynomial_acceleration.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSUME, goto_program_templatet< codeT, guardT >::copy_from(), distinguishers, distinguishing_points, fixed, Forall_goto_program_instructions, acceleration_utilst::fresh_symbol(), goto_program, goto_program_templatet< codeT, guardT >::insert_after(), goto_program_templatet< codeT, guardT >::insert_before(), goto_program_templatet< codeT, guardT >::instructions, loop, loop_header, remove_skip(), SKIP, symbolt::symbol_expr(), symbol_table, goto_program_templatet< codeT, guardT >::update(), and utils.
Referenced by disjunctive_polynomial_accelerationt().
|
protected |
Definition at line 783 of file disjunctive_polynomial_acceleration.cpp.
References distinguishing_points, scratch_programt::eval(), goto_program_templatet< codeT, guardT >::get_successors(), goto_program, exprt::is_true(), loop, and loop_header.
Referenced by disjunctive_polynomial_accelerationt(), find_path(), and fit_polynomial().
|
protected |
Definition at line 750 of file disjunctive_polynomial_acceleration.cpp.
References cone_of_influencet::cone_of_influence(), fixed, and symbol_table.
Referenced by depends_on_array(), disjunctive_polynomial_accelerationt(), and fit_polynomial().
|
protected |
Definition at line 1024 of file disjunctive_polynomial_acceleration.cpp.
References cone_of_influence().
Referenced by accelerate(), and disjunctive_polynomial_accelerationt().
|
protected |
Definition at line 758 of file disjunctive_polynomial_acceleration.cpp.
References distinguishers, distinguishing_points, acceleration_utilst::fresh_symbol(), goto_program_templatet< codeT, guardT >::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 343 of file disjunctive_polynomial_acceleration.cpp.
References accelerated_paths, goto_program_templatet< codeT, guardT >::add_instruction(), scratch_programt::append(), ASSERT, scratch_programt::assume(), build_path(), scratch_programt::check_sat(), fixed, record_path(), irept::swap(), and symbol_table.
Referenced by accelerate(), and disjunctive_polynomial_accelerationt().
bool disjunctive_polynomial_accelerationt::fit_polynomial | ( | exprt & | target, |
polynomialt & | polynomial, | ||
patht & | path | ||
) |
Definition at line 404 of file disjunctive_polynomial_acceleration.cpp.
References accelerated_paths, goto_program_templatet< codeT, guardT >::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, ns, record_path(), signed_poly_type(), irept::swap(), symbolt::symbol_expr(), symbol_table, and utils.
Referenced by accelerate(), and disjunctive_polynomial_accelerationt().
|
protected |
Definition at line 1009 of file disjunctive_polynomial_acceleration.cpp.
References accelerated_paths, distinguishers, scratch_programt::eval(), and exprt::is_true().
Referenced by disjunctive_polynomial_accelerationt(), find_path(), and fit_polynomial().
|
protected |
Definition at line 100 of file disjunctive_polynomial_acceleration.h.
Referenced by find_path(), fit_polynomial(), and record_path().
|
protected |
Definition at line 97 of file disjunctive_polynomial_acceleration.h.
Referenced by build_fixed(), find_distinguishing_points(), fit_polynomial(), and record_path().
|
protected |
Definition at line 96 of file disjunctive_polynomial_acceleration.h.
Referenced by build_fixed(), build_path(), and find_distinguishing_points().
|
protected |
Definition at line 99 of file disjunctive_polynomial_acceleration.h.
Referenced by build_fixed(), cone_of_influence(), find_path(), and fit_polynomial().
|
protected |
Definition at line 86 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate().
|
protected |
Definition at line 87 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), build_fixed(), build_path(), and find_distinguishing_points().
|
protected |
Definition at line 88 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), build_fixed(), build_path(), disjunctive_polynomial_accelerationt(), and find_distinguishing_points().
|
protected |
Definition at line 95 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), assert_for_values(), disjunctive_polynomial_accelerationt(), and fit_polynomial().
|
protected |
Definition at line 89 of file disjunctive_polynomial_acceleration.h.
Referenced by build_fixed(), and build_path().
|
protected |
Definition at line 98 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), and disjunctive_polynomial_accelerationt().
|
protected |
Definition at line 85 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), and fit_polynomial().
|
protected |
Definition at line 84 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), build_fixed(), cone_of_influence(), find_path(), and fit_polynomial().
|
protected |
Definition at line 94 of file disjunctive_polynomial_acceleration.h.
Referenced by accelerate(), build_fixed(), disjunctive_polynomial_accelerationt(), find_distinguishing_points(), and fit_polynomial().