cprover
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
51 void substitute(substitutiont &substitution);
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
Base class for all expressions.
Definition: expr.h:54
int coeff
Definition: polynomial.h:31
std::vector< termt > terms
Definition: polynomial.h:30
int degree()
Definition: polynomial.cpp:456
int compare(monomialt &other)
Definition: polynomial.cpp:341
bool contains(const exprt &var)
Definition: polynomial.cpp:470
void substitute(substitutiont &substitution)
Definition: polynomial.cpp:160
void from_expr(const exprt &expr)
Definition: polynomial.cpp:100
std::vector< monomialt > monomials
Definition: polynomial.h:46
void mult(int scalar)
Definition: polynomial.cpp:252
exprt to_expr()
Definition: polynomial.cpp:22
int coeff(const exprt &expr)
Definition: polynomial.cpp:426
void add(polynomialt &other)
Definition: polynomial.cpp:178
int max_degree(const exprt &var)
Definition: polynomial.cpp:408
std::vector< polynomialt > polynomialst
Definition: polynomial.h:63
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
unsigned int exp
Definition: polynomial.h:26