cprover
|
#include <acceleration_utils.h>
Classes | |
struct | polynomial_array_assignmentt |
Public Types | |
typedef std::pair< exprt, exprt > | expr_pairt |
typedef std::vector< expr_pairt > | expr_pairst |
typedef std::vector< polynomial_array_assignmentt > | polynomial_array_assignmentst |
Public Attributes | |
symbol_tablet & | symbol_table |
namespacet | ns |
const goto_functionst & | goto_functions |
exprt & | loop_counter |
nil_exprt | nil |
Static Public Attributes | |
static int | num_symbols |
Protected Attributes | |
message_handlert & | message_handler |
Definition at line 36 of file acceleration_utils.h.
typedef std::vector<expr_pairt> acceleration_utilst::expr_pairst |
Definition at line 90 of file acceleration_utils.h.
typedef std::pair<exprt, exprt> acceleration_utilst::expr_pairt |
Definition at line 89 of file acceleration_utils.h.
typedef std::vector<polynomial_array_assignmentt> acceleration_utilst::polynomial_array_assignmentst |
Definition at line 100 of file acceleration_utils.h.
|
inline |
Definition at line 42 of file acceleration_utils.h.
|
inline |
Definition at line 55 of file acceleration_utils.h.
Definition at line 302 of file acceleration_utils.cpp.
References Forall_operands, fresh_symbol(), irept::id(), symbolt::symbol_expr(), and exprt::type().
bool acceleration_utilst::array_assignments2polys | ( | expr_pairst & | array_assignments, |
std::map< exprt, polynomialt > & | polynomials, | ||
polynomial_array_assignmentst & | array_polynomials, | ||
polynomialst & | nondet_indices | ||
) |
Definition at line 792 of file acceleration_utils.cpp.
References acceleration_utilst::polynomial_array_assignmentt::array, index_exprt::array(), expr2c(), expr2poly(), acceleration_utilst::polynomial_array_assignmentt::index, index_exprt::index(), ns, polynomialt::to_expr(), to_index_expr(), and acceleration_utilst::polynomial_array_assignmentt::value.
Referenced by do_arrays().
bool acceleration_utilst::assign_array | ( | const exprt & | lhs, |
const exprt & | rhs, | ||
const exprt & | loop_counter, | ||
scratch_programt & | program | ||
) |
Definition at line 1020 of file acceleration_utils.cpp.
References scratch_programt::assign(), scratch_programt::assume(), polynomialt::coeff(), expr2c(), fresh_symbol(), polynomialt::from_expr(), from_integer(), irept::id(), loop_counter, polynomialt::max_degree(), ns, exprt::op0(), exprt::op1(), replace_expr(), simplify_expr(), exprt::source_location(), symbolt::symbol_expr(), exprt::type(), unsigned_poly_type(), and quantifier_exprt::where().
Referenced by do_nonrecursive().
bool acceleration_utilst::check_inductive | ( | std::map< exprt, polynomialt > | polynomials, |
patht & | path | ||
) |
Definition at line 114 of file acceleration_utils.cpp.
References goto_programt::add_instruction(), scratch_programt::append_path(), ASSERT, ASSIGN, ASSUME, scratch_programt::check_sat(), ensure_no_overflows(), from_integer(), loop_counter, message_handler, ns, goto_programt::output(), stash_polynomials(), symbol_table, and exprt::type().
Referenced by disjunctive_polynomial_accelerationt::accelerate(), and polynomial_acceleratort::accelerate().
bool acceleration_utilst::do_arrays | ( | goto_programt::instructionst & | loop_body, |
std::map< exprt, polynomialt > & | polynomials, | ||
exprt & | loop_counter, | ||
substitutiont & | substitution, | ||
scratch_programt & | program | ||
) |
Definition at line 556 of file acceleration_utils.cpp.
References polynomialt::add(), array_assignments2polys(), scratch_programt::assign(), scratch_programt::assume(), polynomialt::coeff(), conjunction(), exprt::copy_to_operands(), expr2c(), fresh_symbol(), polynomialt::from_expr(), from_integer(), gather_array_assignments(), loop_counter, polynomialt::max_degree(), polynomialt::mult(), ns, replace_expr(), signed_poly_type(), polynomialt::substitute(), symbolt::symbol_expr(), polynomialt::to_expr(), exprt::type(), and unsigned_poly_type().
Referenced by disjunctive_polynomial_accelerationt::accelerate().
bool acceleration_utilst::do_assumptions | ( | std::map< exprt, polynomialt > | polynomials, |
patht & | body, | ||
exprt & | guard | ||
) |
Definition at line 357 of file acceleration_utils.cpp.
References goto_programt::add_instruction(), ASSERT, scratch_programt::assign(), scratch_programt::assume(), scratch_programt::check_sat(), ensure_no_overflows(), from_integer(), loop_counter, message_handler, ns, goto_programt::output(), precondition(), simplify(), stash_polynomials(), symbol_table, and exprt::type().
Referenced by disjunctive_polynomial_accelerationt::accelerate(), and polynomial_acceleratort::accelerate().
bool acceleration_utilst::do_nonrecursive | ( | goto_programt::instructionst & | loop_body, |
std::map< exprt, polynomialt > & | polynomials, | ||
exprt & | loop_counter, | ||
substitutiont & | substitution, | ||
expr_sett & | nonrecursive, | ||
scratch_programt & | program | ||
) |
Definition at line 881 of file acceleration_utils.cpp.
References scratch_programt::assign(), assign_array(), expr2c(), from_integer(), gather_array_accesses(), irept::id(), loop_counter, ns, exprt::op0(), exprt::op1(), replace_expr(), polynomialt::substitute(), polynomialt::to_expr(), and exprt::type().
Referenced by polynomial_acceleratort::accelerate().
void acceleration_utilst::ensure_no_overflows | ( | scratch_programt & | program | ) |
Definition at line 479 of file acceleration_utils.cpp.
References goto_programt::add_instruction(), overflow_instrumentert::add_overflow_checks(), ASSUME, fresh_symbol(), optionst::set_option(), symbolt::symbol_expr(), and symbol_table.
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), check_inductive(), do_assumptions(), and disjunctive_polynomial_accelerationt::fit_polynomial().
bool acceleration_utilst::expr2poly | ( | exprt & | expr, |
std::map< exprt, polynomialt > & | polynomials, | ||
polynomialt & | poly | ||
) |
Definition at line 851 of file acceleration_utils.cpp.
References expr2c(), polynomialt::from_expr(), ns, and replace_expr().
Referenced by array_assignments2polys().
void acceleration_utilst::extract_polynomial | ( | scratch_programt & | program, |
std::set< std::pair< expr_listt, exprt > > & | coefficients, | ||
polynomialt & | polynomial | ||
) |
Definition at line 1225 of file acceleration_utils.cpp.
References binary2integer(), dstringt::c_str(), monomialt::coeff, scratch_programt::eval(), monomialt::termt::exp, constant_exprt::get_value(), polynomialt::monomials, monomialt::terms, to_constant_expr(), and monomialt::termt::var.
Referenced by disjunctive_polynomial_accelerationt::fit_polynomial(), and polynomial_acceleratort::fit_polynomial_sliced().
Definition at line 86 of file acceleration_utils.cpp.
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), disjunctive_polynomial_accelerationt::disjunctive_polynomial_accelerationt(), find_modified(), stash_polynomials(), and polynomial_acceleratort::stash_polynomials().
void acceleration_utilst::find_modified | ( | const goto_programt & | program, |
expr_sett & | modified | ||
) |
Definition at line 67 of file acceleration_utils.cpp.
References find_modified(), and forall_goto_program_instructions.
void acceleration_utilst::find_modified | ( | const goto_programt::instructionst & | instructions, |
expr_sett & | modified | ||
) |
Definition at line 75 of file acceleration_utils.cpp.
References find_modified().
void acceleration_utilst::find_modified | ( | const natural_loops_mutablet::natural_loopt & | loop, |
expr_sett & | modified | ||
) |
Definition at line 94 of file acceleration_utils.cpp.
References find_modified().
void acceleration_utilst::find_modified | ( | goto_programt::const_targett | t, |
expr_sett & | modified | ||
) |
Definition at line 102 of file acceleration_utils.cpp.
References code_assignt::lhs(), and to_code_assign().
Definition at line 1278 of file acceleration_utils.cpp.
References symbol_table_baset::add(), symbolt::base_name, symbolt::module, symbolt::name, num_symbols, symbolt::pretty_name, symbol_table, to_string(), and symbolt::type.
Referenced by abstract_arrays(), disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), assign_array(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), do_arrays(), ensure_no_overflows(), sat_path_enumeratort::find_distinguishing_points(), disjunctive_polynomial_accelerationt::find_distinguishing_points(), disjunctive_polynomial_accelerationt::fit_polynomial(), polynomial_acceleratort::fit_polynomial_sliced(), acceleratet::make_overflow_loc(), acceleratet::set_dirty_vars(), stash_variables(), and polynomial_acceleratort::stash_variables().
Definition at line 1209 of file acceleration_utils.cpp.
References forall_operands, irept::id(), and exprt::op0().
Referenced by do_nonrecursive().
acceleration_utilst::expr_pairst acceleration_utilst::gather_array_assignments | ( | goto_programt::instructionst & | loop_body, |
expr_sett & | arrays_written | ||
) |
Definition at line 513 of file acceleration_utils.cpp.
References index_exprt::array(), irept::id(), code_assignt::lhs(), replace_expr(), code_assignt::rhs(), to_code_assign(), and to_index_expr().
Referenced by do_arrays().
Definition at line 47 of file acceleration_utils.cpp.
References forall_operands, and irept::id().
Referenced by polynomial_acceleratort::cone_of_influence().
Definition at line 249 of file acceleration_utils.cpp.
References expr2c(), irept::id(), code_assignt::lhs(), ns, replace_expr(), code_assignt::rhs(), simplify(), and to_code_assign().
Referenced by do_assumptions().
void acceleration_utilst::push_nondet | ( | exprt & | expr | ) |
Definition at line 331 of file acceleration_utils.cpp.
References Forall_operands, irept::id(), exprt::op0(), exprt::op1(), exprt::source_location(), and exprt::type().
void acceleration_utilst::stash_polynomials | ( | scratch_programt & | program, |
std::map< exprt, polynomialt > & | polynomials, | ||
std::map< exprt, exprt > & | stashed, | ||
patht & | path | ||
) |
Definition at line 194 of file acceleration_utils.cpp.
References find_modified(), and stash_variables().
Referenced by disjunctive_polynomial_accelerationt::accelerate(), check_inductive(), and do_assumptions().
void acceleration_utilst::stash_variables | ( | scratch_programt & | program, |
expr_sett | modified, | ||
substitutiont & | substitution | ||
) |
Definition at line 213 of file acceleration_utils.cpp.
References scratch_programt::assign(), find_symbols(), fresh_symbol(), symbol_exprt::get_identifier(), symbol_table_baset::lookup(), loop_counter, symbolt::symbol_expr(), symbol_table, to_symbol_expr(), and symbolt::type.
Referenced by stash_polynomials().
const goto_functionst& acceleration_utilst::goto_functions |
Definition at line 157 of file acceleration_utils.h.
exprt& acceleration_utilst::loop_counter |
Definition at line 158 of file acceleration_utils.h.
Referenced by assign_array(), check_inductive(), do_arrays(), do_assumptions(), do_nonrecursive(), and stash_variables().
|
protected |
Definition at line 39 of file acceleration_utils.h.
Referenced by check_inductive(), and do_assumptions().
nil_exprt acceleration_utilst::nil |
Definition at line 159 of file acceleration_utils.h.
namespacet acceleration_utilst::ns |
Definition at line 156 of file acceleration_utils.h.
Referenced by array_assignments2polys(), assign_array(), check_inductive(), do_arrays(), do_assumptions(), do_nonrecursive(), expr2poly(), and precondition().
|
static |
Definition at line 161 of file acceleration_utils.h.
Referenced by fresh_symbol().
symbol_tablet& acceleration_utilst::symbol_table |
Definition at line 155 of file acceleration_utils.h.
Referenced by check_inductive(), do_assumptions(), ensure_no_overflows(), fresh_symbol(), and stash_variables().