cprover
Loading...
Searching...
No Matches
linear_functiont Class Reference

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.
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.

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.

Private Attributes

mp_integer constant_coefficient
std::unordered_map< exprt, mp_integer, irep_hashcoefficients
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()

linear_functiont::linear_functiont ( const exprt & f)
explicit

Put an expression f composed of additions and subtractions into its cannonical representation.

Member Function Documentation

◆ add()

void linear_functiont::add ( const linear_functiont & other)

Make this function the sum of the current function with other.

◆ 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()

exprt linear_functiont::solve ( linear_functiont f,
const exprt & var,
const exprt & val )
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.

◆ to_expr()

exprt linear_functiont::to_expr ( bool negated = false) const
Parameters
negatedoptional Boolean asking to negate the function
Returns
an expression corresponding to the linear function

Member Data Documentation

◆ coefficients

std::unordered_map<exprt, mp_integer, irep_hash> linear_functiont::coefficients
private

Definition at line 76 of file string_constraint_instantiation.h.

◆ constant_coefficient

mp_integer linear_functiont::constant_coefficient
private

Definition at line 75 of file string_constraint_instantiation.h.

◆ type

typet linear_functiont::type
private

Definition at line 77 of file string_constraint_instantiation.h.


The documentation for this class was generated from the following files: