cprover
Loading...
Searching...
No Matches
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, exprtexpr_pairt
 
typedef std::vector< expr_pairtexpr_pairst
 
typedef struct polynomial_acceleratort::polynomial_array_assignment polynomial_array_assignmentt
 
typedef std::vector< polynomial_array_assignmenttpolynomial_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_handlertmessage_handler
 
symbol_table_basetsymbol_table
 
const namespacet ns
 
const goto_functionstgoto_functions
 
guard_managertguard_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

◆ polynomial_array_assignmentt

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: