cprover
Loading...
Searching...
No Matches
acceleration_utilst Class Reference

#include <acceleration_utils.h>

+ Collaboration diagram for acceleration_utilst:

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_table_baset &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions, exprt &_loop_counter)
 
 acceleration_utilst (symbol_table_baset &_symbol_table, message_handlert &message_handler, 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, guard_managert &guard_manager)
 
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, guard_managert &guard_manager)
 
bool do_arrays (goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, 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, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
 
bool assign_array (const index_exprt &lhs, const exprt &rhs, 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_table_basetsymbol_table
 
namespacet ns
 
const goto_functionstgoto_functions
 
exprtloop_counter
 
nil_exprt nil
 

Protected Attributes

message_handlertmessage_handler
 

Detailed Description

Definition at line 34 of file acceleration_utils.h.

Member Typedef Documentation

◆ expr_pairst

Definition at line 93 of file acceleration_utils.h.

◆ expr_pairt

Definition at line 92 of file acceleration_utils.h.

◆ polynomial_array_assignmentst

Constructor & Destructor Documentation

◆ acceleration_utilst() [1/2]

acceleration_utilst::acceleration_utilst ( symbol_table_baset & _symbol_table,
message_handlert & message_handler,
const goto_functionst & _goto_functions,
exprt & _loop_counter )
inline

Definition at line 40 of file acceleration_utils.h.

◆ acceleration_utilst() [2/2]

acceleration_utilst::acceleration_utilst ( symbol_table_baset & _symbol_table,
message_handlert & message_handler,
const goto_functionst & _goto_functions )
inline

Definition at line 53 of file acceleration_utils.h.

Member Function Documentation

◆ abstract_arrays()

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

Definition at line 275 of file acceleration_utils.cpp.

◆ array_assignments2polys()

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 764 of file acceleration_utils.cpp.

◆ assign_array()

bool acceleration_utilst::assign_array ( const index_exprt & lhs,
const exprt & rhs,
scratch_programt & program )

Definition at line 990 of file acceleration_utils.cpp.

◆ check_inductive()

bool acceleration_utilst::check_inductive ( std::map< exprt, polynomialt > polynomials,
patht & path,
guard_managert & guard_manager )

Definition at line 98 of file acceleration_utils.cpp.

◆ do_arrays()

bool acceleration_utilst::do_arrays ( goto_programt::instructionst & loop_body,
std::map< exprt, polynomialt > & polynomials,
substitutiont & substitution,
scratch_programt & program )

Definition at line 529 of file acceleration_utils.cpp.

◆ do_assumptions()

bool acceleration_utilst::do_assumptions ( std::map< exprt, polynomialt > polynomials,
patht & body,
exprt & guard,
guard_managert & guard_manager )

Definition at line 329 of file acceleration_utils.cpp.

◆ do_nonrecursive()

bool acceleration_utilst::do_nonrecursive ( goto_programt::instructionst & loop_body,
std::map< exprt, polynomialt > & polynomials,
substitutiont & substitution,
expr_sett & nonrecursive,
scratch_programt & program )

Definition at line 853 of file acceleration_utils.cpp.

◆ ensure_no_overflows()

void acceleration_utilst::ensure_no_overflows ( scratch_programt & program)

Definition at line 452 of file acceleration_utils.cpp.

◆ expr2poly()

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

Definition at line 823 of file acceleration_utils.cpp.

◆ extract_polynomial()

void acceleration_utilst::extract_polynomial ( scratch_programt & program,
std::set< std::pair< expr_listt, exprt > > & coefficients,
polynomialt & polynomial )

Definition at line 1197 of file acceleration_utils.cpp.

◆ find_modified() [1/5]

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

Definition at line 55 of file acceleration_utils.cpp.

◆ find_modified() [2/5]

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

Definition at line 63 of file acceleration_utils.cpp.

◆ find_modified() [3/5]

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

Definition at line 82 of file acceleration_utils.cpp.

◆ find_modified() [4/5]

void acceleration_utilst::find_modified ( const patht & path,
expr_sett & modified )

Definition at line 74 of file acceleration_utils.cpp.

◆ find_modified() [5/5]

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

Definition at line 90 of file acceleration_utils.cpp.

◆ fresh_symbol()

symbolt acceleration_utilst::fresh_symbol ( std::string base,
typet type )

Definition at line 1246 of file acceleration_utils.cpp.

◆ gather_array_accesses()

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

Definition at line 1178 of file acceleration_utils.cpp.

◆ gather_array_assignments()

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

Definition at line 486 of file acceleration_utils.cpp.

◆ gather_rvalues()

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

Definition at line 35 of file acceleration_utils.cpp.

◆ precondition()

exprt acceleration_utilst::precondition ( patht & path)

Definition at line 223 of file acceleration_utils.cpp.

◆ push_nondet()

void acceleration_utilst::push_nondet ( exprt & expr)

Definition at line 304 of file acceleration_utils.cpp.

◆ stash_polynomials()

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

Definition at line 175 of file acceleration_utils.cpp.

◆ stash_variables()

void acceleration_utilst::stash_variables ( scratch_programt & program,
expr_sett modified,
substitutiont & substitution )

Definition at line 194 of file acceleration_utils.cpp.

Member Data Documentation

◆ goto_functions

const goto_functionst& acceleration_utilst::goto_functions

Definition at line 157 of file acceleration_utils.h.

◆ loop_counter

exprt& acceleration_utilst::loop_counter

Definition at line 158 of file acceleration_utils.h.

◆ message_handler

message_handlert& acceleration_utilst::message_handler
protected

Definition at line 37 of file acceleration_utils.h.

◆ nil

nil_exprt acceleration_utilst::nil

Definition at line 159 of file acceleration_utils.h.

◆ ns

namespacet acceleration_utilst::ns

Definition at line 156 of file acceleration_utils.h.

◆ symbol_table

symbol_table_baset& acceleration_utilst::symbol_table

Definition at line 155 of file acceleration_utils.h.


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