cprover
linearize.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Loop Acceleration
4
5
Author: Matt Lewis
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_LINEARIZE_H
13
#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_LINEARIZE_H
14
15
#include <vector>
16
17
#include <
goto-symex/goto_symex.h
>
18
#include <
goto-symex/symex_target_equation.h
>
19
20
#include "Eigen/Eigen"
21
22
/*
23
* The idea here is that a linear_recurrencet describes a linear recurrence in
24
* the following way:
25
*
26
* vars' = matrix * vars;
27
*
28
* i.e. the next value of the vars vector is calculated by applying the matrix
29
* to the current vars vector.
30
*/
31
struct
linear_recurrencet
32
{
33
Eigen::MatrixXd
matrix
;
34
std::vector<exprt>
vars
;
35
};
36
37
bool
linearize
(
38
symex_target_equationt
&equation,
39
linear_recurrencet
&recurrence);
40
41
#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_LINEARIZE_H
symex_target_equation.h
Generate Equation using Symbolic Execution.
linear_recurrencet::matrix
Eigen::MatrixXd matrix
Definition:
linearize.h:33
symex_target_equationt
Definition:
symex_target_equation.h:31
linear_recurrencet
Definition:
linearize.h:31
linear_recurrencet::vars
std::vector< exprt > vars
Definition:
linearize.h:34
goto_symex.h
Symbolic Execution.
linearize
bool linearize(symex_target_equationt &equation, linear_recurrencet &recurrence)
Definition:
linearize.cpp:16
goto-instrument
accelerate
linearize.h
Generated by
1.8.12