CBMC
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
polynomial_acceleratort Class Reference

#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: