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>
Collaboration diagram for linear_functiont:Public Member Functions | |
| linear_functiont (const exprt &f) | |
Put an expression f composed of additions and subtractions into its cannonical representation. More... | |
| void | add (const linear_functiont &other) |
Make this function the sum of the current function with other. More... | |
| exprt | to_expr (bool negated=false) const |
| std::string | format () |
| Format the linear function as a string, can be used for debugging. More... | |
Static Public Member Functions | |
| static exprt | solve (linear_functiont f, const exprt &var, const exprt &val) |
Return an expression y such that f(var <- y) = val. More... | |
Private Attributes | |
| mp_integer | constant_coefficient |
| std::unordered_map< exprt, mp_integer, irep_hash > | coefficients |
| typet | type |
Detailed Description
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.
Constructor & Destructor Documentation
◆ linear_functiont()
|
explicit |
Put an expression f composed of additions and subtractions into its cannonical representation.
Definition at line 60 of file string_constraint_instantiation.cpp.
Member Function Documentation
◆ add()
| void linear_functiont::add | ( | const linear_functiont & | other | ) |
Make this function the sum of the current function with other.
Definition at line 101 of file string_constraint_instantiation.cpp.
◆ format()
| std::string linear_functiont::format | ( | ) |
Format the linear function as a string, can be used for debugging.
Definition at line 166 of file string_constraint_instantiation.cpp.
◆ solve()
|
static |
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.
Definition at line 146 of file string_constraint_instantiation.cpp.
◆ 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
Definition at line 109 of file string_constraint_instantiation.cpp.
Member Data Documentation
◆ coefficients
|
private |
Definition at line 76 of file string_constraint_instantiation.h.
◆ constant_coefficient
|
private |
Definition at line 75 of file string_constraint_instantiation.h.
◆ type
|
private |
Definition at line 77 of file string_constraint_instantiation.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_instantiation.h
- /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_instantiation.cpp
