#include <polynomial_accelerator.h>

Collaboration diagram for polynomial_acceleratort:

Classes
struct	polynomial_array_assignment

Public Member Functions
	polynomial_acceleratort (message_handlert &message_handler, const symbol_table_baset &_symbol_table, const goto_functionst &_goto_functions, guard_managert &guard_manager)
	polynomial_acceleratort (message_handlert &message_handler, const symbol_table_baset &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter, guard_managert &guard_manager)
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 Member Functions
bool	fit_polynomial_sliced (goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
void	assert_for_values (scratch_programt &program, std::map< exprt, int > &values, std::set< std::pair< expr_listt, exprt > > &coefficients, int num_unwindings, goto_programt::instructionst &loop_body, exprt &target, overflow_instrumentert &overflow)
void	extract_polynomial (scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
void	cone_of_influence (goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
bool	fit_const (goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
bool	check_inductive (std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
void	stash_polynomials (scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
exprt	precondition (patht &path)
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, 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)
void	ensure_no_overflows (goto_programt &program)

Protected Attributes
message_handlert &	message_handler
symbol_table_baset &	symbol_table
const namespacet	ns
const goto_functionst &	goto_functions
guard_managert &	guard_manager
acceleration_utilst	utils
exprt	loop_counter
expr_sett	nonrecursive

Detailed Description

Definition at line 28 of file polynomial_accelerator.h.

Member Typedef Documentation

◆ expr_pairst

typedef std::vector<expr_pairt> polynomial_acceleratort::expr_pairst

protected

Definition at line 118 of file polynomial_accelerator.h.

◆ expr_pairt

typedef std::pair<exprt, exprt> polynomial_acceleratort::expr_pairt

protected

Definition at line 117 of file polynomial_accelerator.h.

◆ polynomial_array_assignmentst

typedef std::vector<polynomial_array_assignmentt> polynomial_acceleratort::polynomial_array_assignmentst

protected

Definition at line 128 of file polynomial_accelerator.h.

◆ polynomial_array_assignmentt

typedef struct polynomial_acceleratort::polynomial_array_assignment polynomial_acceleratort::polynomial_array_assignmentt

protected

Constructor & Destructor Documentation

◆ polynomial_acceleratort() [1/2]

polynomial_acceleratort::polynomial_acceleratort	(	message_handlert &	message_handler,
		const symbol_table_baset &	_symbol_table,
		const goto_functionst &	_goto_functions,
		guard_managert &	guard_manager )

inline

Definition at line 31 of file polynomial_accelerator.h.

◆ polynomial_acceleratort() [2/2]

polynomial_acceleratort::polynomial_acceleratort	(	message_handlert &	message_handler,
		const symbol_table_baset &	_symbol_table,
		const goto_functionst &	_goto_functions,
		exprt &	_loop_counter,
		guard_managert &	guard_manager )

inline

Definition at line 46 of file polynomial_accelerator.h.

Member Function Documentation

◆ accelerate()

bool polynomial_acceleratort::accelerate	(	patht &	loop,
		path_acceleratort &	accelerator )

Definition at line 35 of file polynomial_accelerator.cpp.

◆ array_assignments2polys()

bool polynomial_acceleratort::array_assignments2polys	(	expr_pairst &	array_assignments,
		std::map< exprt, polynomialt > &	polynomials,
		polynomial_array_assignmentst &	array_polynomials,
		polynomialst &	nondet_indices )

protected

◆ assert_for_values()

void polynomial_acceleratort::assert_for_values	(	scratch_programt &	program,
		std::map< exprt, int > &	values,
		std::set< std::pair< expr_listt, exprt > > &	coefficients,
		int	num_unwindings,
		goto_programt::instructionst &	loop_body,
		exprt &	target,
		overflow_instrumentert &	overflow )

protected

Definition at line 490 of file polynomial_accelerator.cpp.

◆ check_inductive()

bool polynomial_acceleratort::check_inductive	(	std::map< exprt, polynomialt >	polynomials,
		goto_programt::instructionst &	body )

protected

Definition at line 646 of file polynomial_accelerator.cpp.

◆ cone_of_influence()

void polynomial_acceleratort::cone_of_influence	(	goto_programt::instructionst &	orig_body,
		exprt &	target,
		goto_programt::instructionst &	body,
		expr_sett &	influence )

protected

Definition at line 604 of file polynomial_accelerator.cpp.

◆ do_arrays()

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

protected

◆ do_assumptions()

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

protected

◆ ensure_no_overflows()

void polynomial_acceleratort::ensure_no_overflows ( goto_programt & program )

protected

◆ expr2poly()

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

protected

◆ extract_polynomial()

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

protected

◆ fit_const()

bool polynomial_acceleratort::fit_const	(	goto_programt::instructionst &	loop_body,
		exprt &	target,
		polynomialt &	polynomial )

protected

Definition at line 437 of file polynomial_accelerator.cpp.

◆ fit_polynomial()

bool polynomial_acceleratort::fit_polynomial	(	goto_programt::instructionst &	loop_body,
		exprt &	target,
		polynomialt &	polynomial )

Definition at line 424 of file polynomial_accelerator.cpp.

◆ fit_polynomial_sliced()

bool polynomial_acceleratort::fit_polynomial_sliced	(	goto_programt::instructionst &	sliced_body,
		exprt &	target,
		expr_sett &	influence,
		polynomialt &	polynomial )

protected

Definition at line 268 of file polynomial_accelerator.cpp.

◆ gather_array_assignments()

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

protected

◆ precondition()

exprt polynomial_acceleratort::precondition ( patht & path )

protected

Definition at line 749 of file polynomial_accelerator.cpp.

◆ stash_polynomials()

void polynomial_acceleratort::stash_polynomials	(	scratch_programt &	program,
		std::map< exprt, polynomialt > &	polynomials,
		std::map< exprt, exprt > &	stashed,
		goto_programt::instructionst &	body )

protected

Definition at line 723 of file polynomial_accelerator.cpp.

Member Data Documentation

◆ goto_functions

const goto_functionst& polynomial_acceleratort::goto_functions

protected

Definition at line 152 of file polynomial_accelerator.h.

◆ guard_manager

guard_managert& polynomial_acceleratort::guard_manager

protected

Definition at line 153 of file polynomial_accelerator.h.

◆ loop_counter

exprt polynomial_acceleratort::loop_counter

protected

Definition at line 156 of file polynomial_accelerator.h.

◆ message_handler

message_handlert& polynomial_acceleratort::message_handler

protected

Definition at line 70 of file polynomial_accelerator.h.

◆ nonrecursive

expr_sett polynomial_acceleratort::nonrecursive

protected

Definition at line 158 of file polynomial_accelerator.h.

◆ ns

const namespacet polynomial_acceleratort::ns

protected

Definition at line 151 of file polynomial_accelerator.h.

◆ symbol_table

symbol_table_baset& polynomial_acceleratort::symbol_table

protected

Definition at line 150 of file polynomial_accelerator.h.

◆ utils

acceleration_utilst polynomial_acceleratort::utils

protected

Definition at line 154 of file polynomial_accelerator.h.

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

goto-instrument/accelerate/polynomial_accelerator.h
goto-instrument/accelerate/polynomial_accelerator.cpp

Classes

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ expr_pairst

◆ expr_pairt

◆ polynomial_array_assignmentst

◆ polynomial_array_assignmentt

Constructor & Destructor Documentation

◆ polynomial_acceleratort() [1/2]

◆ polynomial_acceleratort() [2/2]

Member Function Documentation

◆ accelerate()

◆ array_assignments2polys()

◆ assert_for_values()

◆ check_inductive()

◆ cone_of_influence()

◆ do_arrays()

◆ do_assumptions()

◆ ensure_no_overflows()

◆ expr2poly()

◆ extract_polynomial()

◆ fit_const()

◆ fit_polynomial()

◆ fit_polynomial_sliced()

◆ gather_array_assignments()

◆ precondition()

◆ stash_polynomials()

Member Data Documentation

◆ goto_functions

◆ guard_manager

◆ loop_counter

◆ message_handler

◆ nonrecursive

◆ ns

◆ symbol_table

◆ utils