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>
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  */
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
Generate Equation using Symbolic Execution.
Eigen::MatrixXd matrix
Definition: linearize.h:33
std::vector< exprt > vars
Definition: linearize.h:34
Symbolic Execution.
bool linearize(symex_target_equationt &equation, linear_recurrencet &recurrence)
Definition: linearize.cpp:16