CBMC
Loading...
Searching...
No Matches
polynomial.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: Matt Lewis
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_H
13#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_H
14
15#include <vector>
16#include <map>
17
18#include <util/expr.h>
19
21{
22public:
23 struct termt
24 {
26 unsigned int exp; // This means exponent, not expression.
27 };
28
29 // Invariant: this vector is sorted lexicographically w.r.t. the variable.
30 std::vector<termt> terms;
31 int coeff;
32
33 int compare(monomialt &other);
34
35 int degree();
36 bool contains(const exprt &var);
37};
38
39typedef std::map<exprt, exprt> substitutiont;
40
42{
43public:
44 // Invariant: this vector is sorted according to the monomial ordering induced
45 // by monomialt::compare()
46 std::vector<monomialt> monomials;
47
48 exprt to_expr();
49 void from_expr(const exprt &expr);
50
52
53 void add(polynomialt &other);
54 void add(monomialt &monomial);
55
56 void mult(int scalar);
57 void mult(polynomialt &other);
58
59 int max_degree(const exprt &var);
60 int coeff(const exprt &expr);
61};
62
63typedef std::vector<polynomialt> polynomialst;
64
65#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
std::vector< termt > terms
Definition polynomial.h:30
int compare(monomialt &other)
bool contains(const exprt &var)
void substitute(substitutiont &substitution)
void from_expr(const exprt &expr)
std::vector< monomialt > monomials
Definition polynomial.h:46
void mult(int scalar)
exprt to_expr()
int coeff(const exprt &expr)
void add(polynomialt &other)
int max_degree(const exprt &var)
std::vector< polynomialt > polynomialst
Definition polynomial.h:63
std::map< exprt, exprt > substitutiont
Definition polynomial.h:39
unsigned int exp
Definition polynomial.h:26