cprover
polynomial_acceleratort Class Reference

#include <polynomial_accelerator.h>

Inheritance diagram for polynomial_acceleratort:
[legend]
Collaboration diagram for polynomial_acceleratort:
[legend]

Classes

struct  polynomial_array_assignment
 

Public Member Functions

 polynomial_acceleratort (const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
 
 polynomial_acceleratort (const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter)
 
virtual 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_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, 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, 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)
 
void ensure_no_overflows (goto_programt &program)
 

Protected Attributes

symbol_tabletsymbol_table
 
const namespacet ns
 
const goto_functionstgoto_functions
 
acceleration_utilst utils
 
exprt loop_counter
 
expr_sett nonrecursive
 

Detailed Description

Definition at line 32 of file polynomial_accelerator.h.

Member Typedef Documentation

◆ expr_pairst

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

Definition at line 116 of file polynomial_accelerator.h.

◆ expr_pairt

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

Definition at line 115 of file polynomial_accelerator.h.

◆ polynomial_array_assignmentst

◆ polynomial_array_assignmentt

Constructor & Destructor Documentation

◆ polynomial_acceleratort() [1/2]

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

Definition at line 35 of file polynomial_accelerator.h.

References loop_counter.

◆ polynomial_acceleratort() [2/2]

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

Definition at line 46 of file polynomial_accelerator.h.

Member Function Documentation

◆ accelerate()

◆ 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

◆ check_inductive()

◆ cone_of_influence()

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

◆ do_arrays()

bool polynomial_acceleratort::do_arrays ( goto_programt::instructionst loop_body,
std::map< exprt, polynomialt > &  polynomials,
exprt loop_counter,
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()

◆ fit_polynomial()

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

◆ fit_polynomial_sliced()

◆ 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

◆ 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

◆ stash_variables()

Member Data Documentation

◆ goto_functions

const goto_functionst& polynomial_acceleratort::goto_functions
protected

Definition at line 151 of file polynomial_accelerator.h.

◆ loop_counter

exprt polynomial_acceleratort::loop_counter
protected

◆ nonrecursive

expr_sett polynomial_acceleratort::nonrecursive
protected

Definition at line 156 of file polynomial_accelerator.h.

Referenced by accelerate().

◆ ns

const namespacet polynomial_acceleratort::ns
protected

◆ symbol_table

symbol_tablet& polynomial_acceleratort::symbol_table
protected

◆ utils

acceleration_utilst polynomial_acceleratort::utils
protected

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