This class is used to store intervals in the form of lower <= upper. More...

#include <interval_template.h>

Public Member Functions
virtual	~interval_templatet ()=default
	interval_templatet ()=default
	interval_templatet (const type2tc &)
	interval_templatet (const T &x)
	interval_templatet (const T &l, const T &u)
T	get_lower () const
T	get_upper () const
T	adjust (const T &v) const
virtual void	set (bool is_upper, const T &b)
virtual T	get (bool is_upper) const
void	set_upper (const T &b)
void	set_lower (const T &b)
void	dump () const
virtual bool	is_le_than (const T &a, const T &b) const
virtual bool	empty () const
	Checks whether there are values that satisfy the the interval.
bool	is_bottom () const
virtual bool	is_top () const
bool	singleton () const
	There is only one value that satisfies.
virtual void	make_le_than (const T &v)
virtual bool	contains (const T &e) const
void	make_sound_le (interval_templatet< T > &v)
virtual void	make_ge_than (const T &v)
void	join (const interval_templatet< T > &i)
	Union or disjunction.
void	meet (const interval_templatet< T > &i)
	Intersection or conjunction.
void	intersect_with (const interval_templatet &i)
bool	is_subseteq (const interval_templatet &other) const
virtual void	approx_union_with (const interval_templatet &i)
interval_templatet< T >	interval_bitand (const interval_templatet< T > &, const interval_templatet< T > &) const
interval_templatet< T >	interval_bitor (const interval_templatet< T > &, const interval_templatet< T > &) const
interval_templatet< T >	interval_bitxor (const interval_templatet< T > &, const interval_templatet< T > &) const
interval_templatet< T >	interval_logical_right_shift (const interval_templatet< T > &, const interval_templatet< T > &) const
interval_templatet< T >	interval_left_shift (const interval_templatet< T > &, const interval_templatet< T > &) const
interval_templatet< T >	interval_arithmetic_right_shift (const interval_templatet< T > &, const interval_templatet< T > &) const
bool	has_changed (const interval_templatet< T > &i)
	This is just to check if a value has changed.
void	make_lower_interval ()
	Generates an interval of the form (-infinity, 0].
signed_max_or signed_max_right_shift interval_templatet< BigInt >	interval_arithmetic_right_shift (const interval_templatet< BigInt > &lhs, const interval_templatet< BigInt > &rhs) const

Static Public Member Functions
static interval_templatet< T >	ternary_if (const interval_templatet< T > &cond, const interval_templatet< T > &true_value, const interval_templatet< T > &false_value)
static bool	is_representable (const type2tc &)
	Whether an interval can be built for a value of type t; when it cannot, expressions over such values evaluate to top.
static interval_templatet< T >	cast (const interval_templatet< T > &, const type2tc &)
static interval_templatet< T >	logical_right_shift (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
static interval_templatet< T >	left_shift (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
static interval_templatet< T >	arithmetic_right_shift (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
static interval_templatet< T >	bitnot (const interval_templatet< T > &w)
static interval_templatet< T >	equality (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
static interval_templatet< T >	invert_bool (const interval_templatet< T > &i)
static interval_templatet< T >	not_equal (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
static interval_templatet< T >	less_than (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
static interval_templatet< T >	less_than_equal (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
static interval_templatet< T >	greater_than_equal (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
static interval_templatet< T >	greater_than (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
static void	contract_interval_le (interval_templatet< T > &a, interval_templatet< T > &b)
	Computer the contraction of "a" and "b" under a <= b.

Public Attributes
std::optional< T >	lower
	Bound value.
std::optional< T >	upper
type2tc	type
	Type to be used for shift operations.

Friends
interval_templatet< T >	operator+ (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
interval_templatet< T >	operator- (const interval_templatet< T > &lhs)
interval_templatet< T >	operator- (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
interval_templatet< T >	operator* (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
interval_templatet< T >	operator/ (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
interval_templatet< T >	operator% (const interval_templatet< T > &, const interval_templatet< T > &)
interval_templatet< T >	operator& (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
interval_templatet< T >	operator\| (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)
interval_templatet< T >	operator^ (const interval_templatet< T > &lhs, const interval_templatet< T > &rhs)

Detailed Description

template<class T>
class interval_templatet< T >

This class is used to store intervals in the form of lower <= upper.

It also has support for infinite. For this the variables _set are used.

Template Parameters

T	template type for the numeric value (e.g. int, float, bigint)

Constructor & Destructor Documentation

◆ ~interval_templatet()

template<class T>

virtual interval_templatet< T >::~interval_templatet ( )

virtualdefault

◆ interval_templatet() [1/4]

template<class T>

interval_templatet< T >::interval_templatet ( )

default

◆ interval_templatet() [2/4]

template<class T>

interval_templatet< T >::interval_templatet ( const type2tc & )

inlineexplicit

◆ interval_templatet() [3/4]

template<class T>

interval_templatet< T >::interval_templatet ( const T & x )

inlineexplicit

◆ interval_templatet() [4/4]

template<class T>

interval_templatet< T >::interval_templatet	(	const T &	l,
		const T &	u )

inline

Member Function Documentation

◆ adjust()

template<class T>

T interval_templatet< T >::adjust ( const T & v ) const

inline

◆ approx_union_with()

template<class T>

virtual void interval_templatet< T >::approx_union_with ( const interval_templatet< T > & i )

inlinevirtual

◆ arithmetic_right_shift()

template<class T>

interval_templatet< T > interval_templatet< T >::arithmetic_right_shift	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

inlinestatic

◆ bitnot()

template<class T>

interval_templatet< T > interval_templatet< T >::bitnot ( const interval_templatet< T > & w )

inlinestatic

◆ cast()

template<class T>

interval_templatet< T > interval_templatet< T >::cast	(	const interval_templatet< T > &	,
		const type2tc &	)

inlinestatic

◆ contains()

template<class T>

virtual bool interval_templatet< T >::contains ( const T & e ) const

inlinevirtual

Reimplemented in wrapped_interval.

◆ contract_interval_le()

template<class T>

void interval_templatet< T >::contract_interval_le	(	interval_templatet< T > &	a,
		interval_templatet< T > &	b )

inlinestatic

Computer the contraction of "a" and "b" under a <= b.

Parameters

a
b

Forward Evaluation y = (a - b) ===> [y] = ([a] - [b]) intersect [-infinity, 0]
Backwards Step, for each variable: a. [a] = [a] intersect [b] + [y] b. [b] = [b] intersect [a] - [y]
Find a fixpoint.

◆ dump()

template<class T>

void interval_templatet< T >::dump ( ) const

inline

◆ empty()

template<class T>

virtual bool interval_templatet< T >::empty ( ) const

inlinevirtual

Checks whether there are values that satisfy the the interval.

Reimplemented in wrapped_interval.

◆ equality()

template<class T>

interval_templatet< T > interval_templatet< T >::equality	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

inlinestatic

◆ get()

template<class T>

virtual T interval_templatet< T >::get ( bool is_upper ) const

inlinevirtual

Reimplemented in wrapped_interval.

◆ get_lower()

template<class T>

T interval_templatet< T >::get_lower ( ) const

inline

◆ get_upper()

template<class T>

T interval_templatet< T >::get_upper ( ) const

inline

◆ greater_than()

template<class T>

interval_templatet< T > interval_templatet< T >::greater_than	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

inlinestatic

◆ greater_than_equal()

template<class T>

interval_templatet< T > interval_templatet< T >::greater_than_equal	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

inlinestatic

◆ has_changed()

template<class T>

bool interval_templatet< T >::has_changed ( const interval_templatet< T > & i )

inline

This is just to check if a value has changed.

This is not the same as an interval comparation!

◆ intersect_with()

template<class T>

void interval_templatet< T >::intersect_with ( const interval_templatet< T > & i )

inline

◆ interval_arithmetic_right_shift() [1/2]

signed_max_or signed_max_right_shift interval_templatet< BigInt > interval_templatet< BigInt >::interval_arithmetic_right_shift	(	const interval_templatet< BigInt > &	lhs,
		const interval_templatet< BigInt > &	rhs ) const

◆ interval_arithmetic_right_shift() [2/2]

template<class T>

interval_templatet< T > interval_templatet< T >::interval_arithmetic_right_shift	(	const interval_templatet< T > &	,
		const interval_templatet< T > &	) const

inline

◆ interval_bitand()

template<class T>

interval_templatet< T > interval_templatet< T >::interval_bitand	(	const interval_templatet< T > &	,
		const interval_templatet< T > &	) const

inline

◆ interval_bitor()

template<class T>

interval_templatet< T > interval_templatet< T >::interval_bitor	(	const interval_templatet< T > &	,
		const interval_templatet< T > &	) const

inline

◆ interval_bitxor()

template<class T>

interval_templatet< T > interval_templatet< T >::interval_bitxor	(	const interval_templatet< T > &	,
		const interval_templatet< T > &	) const

inline

◆ interval_left_shift()

template<class T>

interval_templatet< T > interval_templatet< T >::interval_left_shift	(	const interval_templatet< T > &	,
		const interval_templatet< T > &	) const

inline

◆ interval_logical_right_shift()

template<class T>

interval_templatet< T > interval_templatet< T >::interval_logical_right_shift	(	const interval_templatet< T > &	,
		const interval_templatet< T > &	) const

inline

◆ invert_bool()

template<class T>

interval_templatet< T > interval_templatet< T >::invert_bool ( const interval_templatet< T > & i )

inlinestatic

◆ is_bottom()

template<class T>

bool interval_templatet< T >::is_bottom ( ) const

inline

◆ is_le_than()

template<class T>

virtual bool interval_templatet< T >::is_le_than	(	const T &	a,
		const T &	b ) const

inlinevirtual

◆ is_representable()

template<class T>

bool interval_templatet< T >::is_representable ( const type2tc & )

inlinestatic

Whether an interval can be built for a value of type t; when it cannot, expressions over such values evaluate to top.

◆ is_subseteq()

template<class T>

bool interval_templatet< T >::is_subseteq ( const interval_templatet< T > & other ) const

inline

◆ is_top()

template<class T>

virtual bool interval_templatet< T >::is_top ( ) const

inlinevirtual

Reimplemented in wrapped_interval.

◆ join()

template<class T>

void interval_templatet< T >::join ( const interval_templatet< T > & i )

inline

Union or disjunction.

◆ left_shift()

template<class T>

interval_templatet< T > interval_templatet< T >::left_shift	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

inlinestatic

◆ less_than()

template<class T>

interval_templatet< T > interval_templatet< T >::less_than	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

inlinestatic

◆ less_than_equal()

template<class T>

interval_templatet< T > interval_templatet< T >::less_than_equal	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

inlinestatic

◆ logical_right_shift()

template<class T>

interval_templatet< T > interval_templatet< T >::logical_right_shift	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

inlinestatic

◆ make_ge_than()

template<class T>

virtual void interval_templatet< T >::make_ge_than ( const T & v )

inlinevirtual

Reimplemented in wrapped_interval.

◆ make_le_than()

template<class T>

virtual void interval_templatet< T >::make_le_than ( const T & v )

inlinevirtual

Reimplemented in wrapped_interval.

◆ make_lower_interval()

template<class T>

void interval_templatet< T >::make_lower_interval ( )

inline

Generates an interval of the form (-infinity, 0].

◆ make_sound_le()

template<class T>

void interval_templatet< T >::make_sound_le ( interval_templatet< T > & v )

inline

◆ meet()

template<class T>

void interval_templatet< T >::meet ( const interval_templatet< T > & i )

inline

Intersection or conjunction.

◆ not_equal()

template<class T>

interval_templatet< T > interval_templatet< T >::not_equal	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

inlinestatic

◆ set()

template<class T>

virtual void interval_templatet< T >::set	(	bool	is_upper,
		const T &	b )

inlinevirtual

Reimplemented in wrapped_interval.

◆ set_lower()

template<class T>

void interval_templatet< T >::set_lower ( const T & b )

inline

◆ set_upper()

template<class T>

void interval_templatet< T >::set_upper ( const T & b )

inline

◆ singleton()

template<class T>

bool interval_templatet< T >::singleton ( ) const

inline

There is only one value that satisfies.

◆ ternary_if()

template<class T>

interval_templatet< T > interval_templatet< T >::ternary_if	(	const interval_templatet< T > &	cond,
		const interval_templatet< T > &	true_value,
		const interval_templatet< T > &	false_value )

inlinestatic

◆ operator%

template<class T>

interval_templatet< T > operator%	(	const interval_templatet< T > &	,
		const interval_templatet< T > &	)

friend

◆ operator&

template<class T>

interval_templatet< T > operator&	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

friend

◆ operator*

template<class T>

interval_templatet< T > operator*	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

friend

◆ operator+

template<class T>

interval_templatet< T > operator+	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

friend

◆ operator- [1/2]

template<class T>

interval_templatet< T > operator- ( const interval_templatet< T > & lhs )

friend

◆ operator- [2/2]

template<class T>

interval_templatet< T > operator-	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

friend

◆ operator/

template<class T>

interval_templatet< T > operator/	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

friend

◆ operator^

template<class T>

interval_templatet< T > operator^	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

friend

◆ operator|

template<class T>

interval_templatet< T > operator\|	(	const interval_templatet< T > &	lhs,
		const interval_templatet< T > &	rhs )

friend

Member Data Documentation

◆ lower

template<class T>

std::optional<T> interval_templatet< T >::lower

Bound value.

◆ type

template<class T>

type2tc interval_templatet< T >::type

Type to be used for shift operations.

◆ upper

template<class T>

std::optional<T> interval_templatet< T >::upper

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

src/goto-programs/abstract-interpretation/interval_template.h

Public Member Functions

Static Public Member Functions

Public Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ ~interval_templatet()

◆ interval_templatet() [1/4]

◆ interval_templatet() [2/4]

◆ interval_templatet() [3/4]

◆ interval_templatet() [4/4]

Member Function Documentation

◆ adjust()

◆ approx_union_with()

◆ arithmetic_right_shift()

◆ bitnot()

◆ cast()

◆ contains()

◆ contract_interval_le()

◆ dump()

◆ empty()

◆ equality()

◆ get()

◆ get_lower()

◆ get_upper()

◆ greater_than()

◆ greater_than_equal()

◆ has_changed()

◆ intersect_with()

◆ interval_arithmetic_right_shift() [1/2]

◆ interval_arithmetic_right_shift() [2/2]

◆ interval_bitand()

◆ interval_bitor()

◆ interval_bitxor()

◆ interval_left_shift()

◆ interval_logical_right_shift()

◆ invert_bool()

◆ is_bottom()

◆ is_le_than()

◆ is_representable()

◆ is_subseteq()

◆ is_top()

◆ join()

◆ left_shift()

◆ less_than()

◆ less_than_equal()

◆ logical_right_shift()

◆ make_ge_than()

◆ make_le_than()

◆ make_lower_interval()

◆ make_sound_le()

◆ meet()

◆ not_equal()

◆ set()

◆ set_lower()

◆ set_upper()

◆ singleton()

◆ ternary_if()

Friends And Related Symbol Documentation

◆ operator%

◆ operator&

◆ operator*

◆ operator+

◆ operator- [1/2]

◆ operator- [2/2]

◆ operator/

◆ operator^

◆ operator|

Member Data Documentation

◆ lower

◆ type

◆ upper