Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given by constant_coefficient
2 and coefficients:
x -> 2, y -> -1.
More...
#include <string_constraint_instantiation.h>
|
| linear_functiont (const exprt &f) |
| Put an expression f composed of additions and subtractions into its cannonical representation.
|
|
void | add (const linear_functiont &other) |
| Make this function the sum of the current function with other .
|
|
exprt | to_expr (bool negated=false) const |
|
std::string | format () |
| Format the linear function as a string, can be used for debugging.
|
|
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given by constant_coefficient
2 and coefficients:
x -> 2, y -> -1.
Definition at line 51 of file string_constraint_instantiation.h.
◆ linear_functiont()
linear_functiont::linear_functiont |
( |
const exprt & | f | ) |
|
|
explicit |
Put an expression f
composed of additions and subtractions into its cannonical representation.
◆ add()
Make this function the sum of the current function with other
.
◆ format()
std::string linear_functiont::format |
( |
| ) |
|
◆ solve()
Return an expression y
such that f(var <- y) = val
.
The coefficient of var
in the linear function must be 1 or -1. For instance, if f
corresponds to the expression q + x
, solve(q,v,f)
returns the expression v - x
.
◆ to_expr()
exprt linear_functiont::to_expr |
( |
bool | negated = false | ) |
const |
- Parameters
-
negated | optional Boolean asking to negate the function |
- Returns
- an expression corresponding to the linear function
◆ coefficients
◆ constant_coefficient
◆ type
typet linear_functiont::type |
|
private |
The documentation for this class was generated from the following files: