Loading...

Searching...

No Matches

Public Member Functions | Static Public Member Functions | Private Attributes | List of all members

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:

[フレーム]

[legend]

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

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

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.

Definition at line 146 of file string_constraint_instantiation.cpp.