cprover
|
#include <polynomial_accelerator.h>
Classes | |
struct | polynomial_array_assignment |
Public Member Functions | |
polynomial_acceleratort (message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions) | |
polynomial_acceleratort (message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter) | |
bool | accelerate (patht &loop, path_acceleratort &accelerator) |
bool | fit_polynomial (goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial) |
Protected Types | |
typedef std::pair< exprt, exprt > | expr_pairt |
typedef std::vector< expr_pairt > | expr_pairst |
typedef struct polynomial_acceleratort::polynomial_array_assignment | polynomial_array_assignmentt |
typedef std::vector< polynomial_array_assignmentt > | polynomial_array_assignmentst |
Protected Attributes | |
message_handlert & | message_handler |
symbol_tablet & | symbol_table |
const namespacet | ns |
const goto_functionst & | goto_functions |
acceleration_utilst | utils |
exprt | loop_counter |
expr_sett | nonrecursive |
Definition at line 31 of file polynomial_accelerator.h.
|
protected |
Definition at line 121 of file polynomial_accelerator.h.
|
protected |
Definition at line 120 of file polynomial_accelerator.h.
|
protected |
Definition at line 131 of file polynomial_accelerator.h.
|
protected |
|
inline |
Definition at line 34 of file polynomial_accelerator.h.
References loop_counter.
|
inline |
Definition at line 47 of file polynomial_accelerator.h.
bool polynomial_acceleratort::accelerate | ( | patht & | loop, |
path_acceleratort & | accelerator | ||
) |
Definition at line 45 of file polynomial_accelerator.cpp.
References goto_programt::add_instruction(), scratch_programt::assign(), ASSUME, acceleration_utilst::check_inductive(), check_inductive(), path_acceleratort::clear(), cone_of_influence(), path_acceleratort::dirty_vars, acceleration_utilst::do_assumptions(), acceleration_utilst::do_nonrecursive(), acceleration_utilst::ensure_no_overflows(), expr2c(), acceleration_utilst::find_modified(), fit_polynomial_sliced(), scratch_programt::fix_types(), acceleration_utilst::fresh_symbol(), from_integer(), irept::id(), goto_programt::instructions, irept::is_nil(), loop_counter, message_handler, nonrecursive, ns, goto_programt::output_instruction(), path_acceleratort::pure_accelerator, replace_expr(), exprt::source_location(), stash_polynomials(), symbolt::symbol_expr(), symbol_table, exprt::type(), unsigned_poly_type(), and utils.
Referenced by enumerating_loop_accelerationt::accelerate().
|
protected |
|
protected |
Definition at line 497 of file polynomial_accelerator.cpp.
References goto_programt::add_instruction(), scratch_programt::append(), scratch_programt::assign(), ASSUME, from_integer(), irept::id(), irept::is_nil(), join_types(), loop_counter, overflow_instrumentert::overflow_expr(), size_type(), to_bitvector_type(), and exprt::type().
Referenced by fit_polynomial_sliced().
|
protected |
Definition at line 652 of file polynomial_accelerator.cpp.
References goto_programt::add_instruction(), scratch_programt::append(), ASSERT, ASSIGN, ASSUME, scratch_programt::check_sat(), from_integer(), loop_counter, message_handler, ns, goto_programt::output(), stash_polynomials(), symbol_table, and exprt::type().
Referenced by accelerate().
|
protected |
Definition at line 611 of file polynomial_accelerator.cpp.
References acceleration_utilst::gather_rvalues(), code_assignt::lhs(), code_assignt::rhs(), to_code_assign(), and utils.
Referenced by accelerate(), and fit_polynomial().
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
Definition at line 448 of file polynomial_accelerator.cpp.
References goto_programt::add_instruction(), scratch_programt::append(), ASSERT, binary2integer(), scratch_programt::check_sat(), scratch_programt::eval(), monomialt::termt::exp, expr2c(), from_integer(), message_handler, polynomialt::monomials, ns, symbol_table, to_constant_expr(), exprt::type(), and monomialt::termt::var.
bool polynomial_acceleratort::fit_polynomial | ( | goto_programt::instructionst & | loop_body, |
exprt & | target, | ||
polynomialt & | polynomial | ||
) |
Definition at line 435 of file polynomial_accelerator.cpp.
References cone_of_influence(), and fit_polynomial_sliced().
Referenced by disjunctive_polynomial_accelerationt::accelerate().
|
protected |
Definition at line 277 of file polynomial_accelerator.cpp.
References goto_programt::add_instruction(), ASSERT, assert_for_values(), scratch_programt::check_sat(), expr2c(), acceleration_utilst::extract_polynomial(), acceleration_utilst::fresh_symbol(), is_bitvector(), loop_counter, message_handler, ns, goto_programt::output(), symbolt::symbol_expr(), symbol_table, to_bitvector_type(), exprt::type(), and utils.
Referenced by accelerate(), and fit_polynomial().
|
protected |
Definition at line 784 of file polynomial_accelerator.cpp.
References expr2c(), irept::id(), code_assignt::lhs(), ns, replace_expr(), code_assignt::rhs(), simplify(), and to_code_assign().
|
protected |
Definition at line 730 of file polynomial_accelerator.cpp.
References acceleration_utilst::find_modified(), stash_variables(), and utils.
Referenced by accelerate(), and check_inductive().
|
protected |
Definition at line 748 of file polynomial_accelerator.cpp.
References scratch_programt::assign(), find_symbols(), acceleration_utilst::fresh_symbol(), symbol_exprt::get_identifier(), symbol_table_baset::lookup(), loop_counter, symbolt::symbol_expr(), symbol_table, to_symbol_expr(), symbolt::type, and utils.
Referenced by stash_polynomials().
|
protected |
Definition at line 156 of file polynomial_accelerator.h.
|
protected |
Definition at line 159 of file polynomial_accelerator.h.
Referenced by accelerate(), assert_for_values(), check_inductive(), fit_polynomial_sliced(), polynomial_acceleratort(), and stash_variables().
|
protected |
Definition at line 69 of file polynomial_accelerator.h.
Referenced by accelerate(), check_inductive(), fit_const(), and fit_polynomial_sliced().
|
protected |
Definition at line 161 of file polynomial_accelerator.h.
Referenced by accelerate().
|
protected |
Definition at line 155 of file polynomial_accelerator.h.
Referenced by accelerate(), check_inductive(), fit_const(), fit_polynomial_sliced(), and precondition().
|
protected |
Definition at line 154 of file polynomial_accelerator.h.
Referenced by accelerate(), check_inductive(), fit_const(), fit_polynomial_sliced(), and stash_variables().
|
protected |
Definition at line 157 of file polynomial_accelerator.h.
Referenced by accelerate(), cone_of_influence(), fit_polynomial_sliced(), stash_polynomials(), and stash_variables().