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

linear_functiont::linear_functiont ( const exprt &  f )

explicit

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

Definition at line 58 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 99 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 164 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 144 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 107 of file string_constraint_instantiation.cpp.

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:

• /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/strings/string_constraint_instantiation.h
• /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/strings/string_constraint_instantiation.cpp