cprover
|
#include <polynomial_accelerator.h>
Classes | |
struct | polynomial_array_assignment |
Public Member Functions | |
polynomial_acceleratort (const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions) | |
polynomial_acceleratort (const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter) | |
virtual 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 | |
symbol_tablet & | symbol_table |
const namespacet | ns |
const goto_functionst & | goto_functions |
acceleration_utilst | utils |
exprt | loop_counter |
expr_sett | nonrecursive |
Definition at line 32 of file polynomial_accelerator.h.
|
protected |
Definition at line 116 of file polynomial_accelerator.h.
|
protected |
Definition at line 115 of file polynomial_accelerator.h.
|
protected |
Definition at line 126 of file polynomial_accelerator.h.
|
protected |
|
inline |
Definition at line 35 of file polynomial_accelerator.h.
References loop_counter.
|
inline |
Definition at line 46 of file polynomial_accelerator.h.
References accelerate(), assert_for_values(), check_inductive(), cone_of_influence(), do_assumptions(), extract_polynomial(), fit_const(), fit_polynomial(), fit_polynomial_sliced(), precondition(), stash_polynomials(), and stash_variables().
|
virtual |
Implements path_accelerationt.
Definition at line 47 of file polynomial_accelerator.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), scratch_programt::assign(), ASSUME, check_inductive(), path_acceleratort::clear(), cone_of_influence(), exprt::copy_to_operands(), 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_program_templatet< codeT, guardT >::instructions, irept::is_nil(), loop_counter, nonrecursive, ns, goto_programt::output_instruction(), path_acceleratort::pure_accelerator, replace_expr(), stash_polynomials(), symbolt::symbol_expr(), symbol_table, exprt::type(), unsigned_poly_type(), and utils.
Referenced by enumerating_loop_accelerationt::accelerate(), and polynomial_acceleratort().
|
protected |
|
protected |
Definition at line 502 of file polynomial_accelerator.cpp.
References goto_program_templatet< codeT, guardT >::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(), and polynomial_acceleratort().
|
protected |
Definition at line 657 of file polynomial_accelerator.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), scratch_programt::append(), ASSERT, ASSIGN, ASSUME, scratch_programt::check_sat(), from_integer(), loop_counter, ns, goto_program_templatet< codeT, guardT >::output(), stash_polynomials(), symbol_table, and exprt::type().
Referenced by accelerate(), and polynomial_acceleratort().
|
protected |
Definition at line 616 of file polynomial_accelerator.cpp.
References acceleration_utilst::gather_rvalues(), code_assignt::lhs(), code_assignt::rhs(), to_code_assign(), and utils.
Referenced by accelerate(), fit_polynomial(), and polynomial_acceleratort().
|
protected |
|
protected |
Referenced by polynomial_acceleratort().
|
protected |
|
protected |
|
protected |
Referenced by polynomial_acceleratort().
|
protected |
Definition at line 455 of file polynomial_accelerator.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), scratch_programt::append(), ASSERT, binary2integer(), scratch_programt::check_sat(), scratch_programt::eval(), monomialt::termt::exp, expr2c(), from_integer(), polynomialt::monomials, ns, symbol_table, to_constant_expr(), exprt::type(), and monomialt::termt::var.
Referenced by polynomial_acceleratort().
bool polynomial_acceleratort::fit_polynomial | ( | goto_programt::instructionst & | loop_body, |
exprt & | target, | ||
polynomialt & | polynomial | ||
) |
Definition at line 442 of file polynomial_accelerator.cpp.
References cone_of_influence(), and fit_polynomial_sliced().
Referenced by disjunctive_polynomial_accelerationt::accelerate(), and polynomial_acceleratort().
|
protected |
Definition at line 282 of file polynomial_accelerator.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), configt::ansi_c, ASSERT, assert_for_values(), scratch_programt::check_sat(), config, expr2c(), acceleration_utilst::extract_polynomial(), acceleration_utilst::fresh_symbol(), irept::id(), is_bitvector(), loop_counter, ns, goto_program_templatet< codeT, guardT >::output(), configt::ansi_ct::pointer_width, symbolt::symbol_expr(), symbol_table, to_bitvector_type(), exprt::type(), and utils.
Referenced by accelerate(), fit_polynomial(), and polynomial_acceleratort().
|
protected |
Definition at line 789 of file polynomial_accelerator.cpp.
References expr2c(), irept::id(), code_assignt::lhs(), ns, replace_expr(), code_assignt::rhs(), simplify(), and to_code_assign().
Referenced by polynomial_acceleratort().
|
protected |
Definition at line 735 of file polynomial_accelerator.cpp.
References acceleration_utilst::find_modified(), stash_variables(), and utils.
Referenced by accelerate(), check_inductive(), and polynomial_acceleratort().
|
protected |
Definition at line 753 of file polynomial_accelerator.cpp.
References scratch_programt::assign(), find_symbols(), acceleration_utilst::fresh_symbol(), symbol_exprt::get_identifier(), symbol_tablet::lookup(), loop_counter, symbolt::symbol_expr(), symbol_table, to_symbol_expr(), symbolt::type, and utils.
Referenced by polynomial_acceleratort(), and stash_polynomials().
|
protected |
Definition at line 151 of file polynomial_accelerator.h.
|
protected |
Definition at line 154 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 156 of file polynomial_accelerator.h.
Referenced by accelerate().
|
protected |
Definition at line 150 of file polynomial_accelerator.h.
Referenced by accelerate(), check_inductive(), fit_const(), fit_polynomial_sliced(), and precondition().
|
protected |
Definition at line 149 of file polynomial_accelerator.h.
Referenced by accelerate(), check_inductive(), fit_const(), fit_polynomial_sliced(), and stash_variables().
|
protected |
Definition at line 152 of file polynomial_accelerator.h.
Referenced by accelerate(), cone_of_influence(), fit_polynomial_sliced(), stash_polynomials(), and stash_variables().