Implementation of a zone with DBM. More...

#include <zone.hh>

Inheritance diagram for Zone:

Public Types
using	Tuple = std::tuple< std::vector< Bounds >, Bounds >

Public Member Functions
std::size_t	getNumOfVar () const noexcept

void	cutVars (std::shared_ptr< Zone > &out, std::size_t from, std::size_t to)

std::tuple< std::vector< Bounds >, Bounds >	toTuple () const

void	tighten (ClockVariables x, ClockVariables y, Bounds c)
	add the constraint x - y \le (c,s)

void	close1 (ClockVariables x)

void	reset (ClockVariables x)

void	elapse ()

void	canonize ()

bool	isSatisfiable ()

void	abstractize ()

void	makeUnsat ()
	make the zone unsatisfiable

std::vector< Constraint >	makeGuard ()
	make the strongest guard including the zone

bool	operator== (Zone z) const

void	intersectionAssign (Zone z)

Static Public Member Functions
static Zone	zero (int size)

static Zone	universal (int size)

Public Attributes
Eigen::Matrix< Bounds, Eigen::Dynamic, Eigen::Dynamic >	value

Bounds	M

Detailed Description

Implementation of a zone with DBM.

Note: internally, the variable 0 is used for the constant while externally, the actual clock variable is 0 origin, i.e., the variable 0 for the user is the variable 1 internally. So, we need increment or decrement to fill the gap.

Member Function Documentation

std::size_t Zone::getNumOfVar ( ) const

inlinenoexcept

Returns the number of the variables represented by this zone

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