cprover
acceleration_utilst Class Reference

#include <acceleration_utils.h>

Collaboration diagram for acceleration_utilst:
[legend]

Classes

struct  polynomial_array_assignmentt
 

Public Types

typedef std::pair< exprt, exprtexpr_pairt
 
typedef std::vector< expr_pairtexpr_pairst
 
typedef std::vector< polynomial_array_assignmenttpolynomial_array_assignmentst
 

Public Member Functions

 acceleration_utilst (symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter)
 
 acceleration_utilst (symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
 
void extract_polynomial (scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
 
bool check_inductive (std::map< exprt, polynomialt > polynomials, patht &path)
 
void stash_variables (scratch_programt &program, expr_sett modified, substitutiont &substitution)
 
void stash_polynomials (scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)
 
exprt precondition (patht &path)
 
void abstract_arrays (exprt &expr, expr_mapt &abstractions)
 
void push_nondet (exprt &expr)
 
bool do_assumptions (std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
 
bool do_arrays (goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, scratch_programt &program)
 
expr_pairst gather_array_assignments (goto_programt::instructionst &loop_body, expr_sett &arrays_written)
 
bool array_assignments2polys (expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
 
bool expr2poly (exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
 
bool do_nonrecursive (goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
 
bool assign_array (const exprt &lhs, const exprt &rhs, const exprt &loop_counter, scratch_programt &program)
 
void gather_array_accesses (const exprt &expr, expr_sett &arrays)
 
void gather_rvalues (const exprt &expr, expr_sett &rvalues)
 
void ensure_no_overflows (scratch_programt &program)
 
void find_modified (const patht &path, expr_sett &modified)
 
void find_modified (const goto_programt &program, expr_sett &modified)
 
void find_modified (const goto_programt::instructionst &instructions, expr_sett &modified)
 
void find_modified (const natural_loops_mutablet::natural_loopt &loop, expr_sett &modified)
 
void find_modified (goto_programt::const_targett t, expr_sett &modified)
 
symbolt fresh_symbol (std::string base, typet type)
 

Public Attributes

symbol_tabletsymbol_table
 
namespacet ns
 
const goto_functionstgoto_functions
 
exprtloop_counter
 
nil_exprt nil
 

Static Public Attributes

static int num_symbols
 

Detailed Description

Definition at line 33 of file acceleration_utils.h.

Member Typedef Documentation

◆ expr_pairst

Definition at line 78 of file acceleration_utils.h.

◆ expr_pairt

Definition at line 77 of file acceleration_utils.h.

◆ polynomial_array_assignmentst

Constructor & Destructor Documentation

◆ acceleration_utilst() [1/2]

acceleration_utilst::acceleration_utilst ( symbol_tablet _symbol_table,
const goto_functionst _goto_functions,
exprt _loop_counter 
)
inline

Definition at line 36 of file acceleration_utils.h.

◆ acceleration_utilst() [2/2]

acceleration_utilst::acceleration_utilst ( symbol_tablet _symbol_table,
const goto_functionst _goto_functions 
)
inline

Definition at line 46 of file acceleration_utils.h.

Member Function Documentation

◆ abstract_arrays()

void acceleration_utilst::abstract_arrays ( exprt expr,
expr_mapt abstractions 
)

◆ array_assignments2polys()

◆ assign_array()

◆ check_inductive()

◆ do_arrays()

◆ do_assumptions()

◆ do_nonrecursive()

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 
)

◆ ensure_no_overflows()

◆ expr2poly()

bool acceleration_utilst::expr2poly ( exprt expr,
std::map< exprt, polynomialt > &  polynomials,
polynomialt poly 
)

Definition at line 859 of file acceleration_utils.cpp.

References expr2c(), polynomialt::from_expr(), ns, and replace_expr().

Referenced by array_assignments2polys().

◆ extract_polynomial()

◆ find_modified() [1/5]

◆ find_modified() [2/5]

void acceleration_utilst::find_modified ( const goto_programt program,
expr_sett modified 
)

Definition at line 69 of file acceleration_utils.cpp.

References find_modified(), and forall_goto_program_instructions.

◆ find_modified() [3/5]

void acceleration_utilst::find_modified ( const goto_programt::instructionst instructions,
expr_sett modified 
)

Definition at line 77 of file acceleration_utils.cpp.

References find_modified().

◆ find_modified() [4/5]

void acceleration_utilst::find_modified ( const natural_loops_mutablet::natural_loopt loop,
expr_sett modified 
)

Definition at line 96 of file acceleration_utils.cpp.

References find_modified().

◆ find_modified() [5/5]

void acceleration_utilst::find_modified ( goto_programt::const_targett  t,
expr_sett modified 
)

Definition at line 104 of file acceleration_utils.cpp.

References code_assignt::lhs(), and to_code_assign().

◆ fresh_symbol()

◆ gather_array_accesses()

void acceleration_utilst::gather_array_accesses ( const exprt expr,
expr_sett arrays 
)

Definition at line 1227 of file acceleration_utils.cpp.

References forall_operands, irept::id(), and exprt::op0().

Referenced by do_nonrecursive().

◆ gather_array_assignments()

acceleration_utilst::expr_pairst acceleration_utilst::gather_array_assignments ( goto_programt::instructionst loop_body,
expr_sett arrays_written 
)

◆ gather_rvalues()

void acceleration_utilst::gather_rvalues ( const exprt expr,
expr_sett rvalues 
)

Definition at line 49 of file acceleration_utils.cpp.

References forall_operands, and irept::id().

Referenced by polynomial_acceleratort::cone_of_influence().

◆ precondition()

exprt acceleration_utilst::precondition ( patht path)

◆ push_nondet()

void acceleration_utilst::push_nondet ( exprt expr)

◆ stash_polynomials()

void acceleration_utilst::stash_polynomials ( scratch_programt program,
std::map< exprt, polynomialt > &  polynomials,
std::map< exprt, exprt > &  stashed,
patht path 
)

◆ stash_variables()

Member Data Documentation

◆ goto_functions

const goto_functionst& acceleration_utilst::goto_functions

Definition at line 145 of file acceleration_utils.h.

◆ loop_counter

exprt& acceleration_utilst::loop_counter

◆ nil

nil_exprt acceleration_utilst::nil

Definition at line 147 of file acceleration_utils.h.

◆ ns

◆ num_symbols

int acceleration_utilst::num_symbols
static

Definition at line 149 of file acceleration_utils.h.

Referenced by fresh_symbol().

◆ symbol_table

symbol_tablet& acceleration_utilst::symbol_table

The documentation for this class was generated from the following files: