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: