CspMap Class Reference

This class is for mapping the variables with their names and intervals. More...

#include <goto_contractor.h>

Public Member Functions
	CspMap ()=default
size_t	add_var (const std::string &name, const expr2tc &symbol)
void	update_lb_interval (double lb, const std::string &name)
void	update_ub_interval (double ub, const std::string &name)
int	find (const std::string &name)
size_t	size () const
ibex::IntervalVector	create_interval_vector ()
void	update_intervals (ibex::IntervalVector vector)
bool	is_empty_set () const
void	dump ()

Public Attributes
std::map< std::string, vart >	var_map

Static Public Attributes
static constexpr int	MAX_VAR = 20
static constexpr int	NOT_FOUND = -1
static constexpr int	IGNORE = -2

Detailed Description

This class is for mapping the variables with their names and intervals.

It includes functionalities such as search for a variable by name and add a new variable. Also update a variable interval by changing the upper/lower limit.

Constructor & Destructor Documentation

CspMap()

CspMap::CspMap ( )

default

Member Function Documentation

add_var()

size_t CspMap::add_var ( const std::string & name, const expr2tc & symbol )

inline

create_interval_vector()

ibex::IntervalVector CspMap::create_interval_vector ( )

inline

dump()

void CspMap::dump ( )

inline

find()

int CspMap::find ( const std::string & name )

inline

is_empty_set()

bool CspMap::is_empty_set ( ) const

inline

size()

size_t CspMap::size ( ) const

inline

update_intervals()

void CspMap::update_intervals ( ibex::IntervalVector vector )

inline

update_lb_interval()

void CspMap::update_lb_interval ( double lb, const std::string & name )

inline

update_ub_interval()

void CspMap::update_ub_interval ( double ub, const std::string & name )

inline

Member Data Documentation

IGNORE

int CspMap::IGNORE = -2

staticconstexpr

MAX_VAR

int CspMap::MAX_VAR = 20

staticconstexpr

NOT_FOUND

int CspMap::NOT_FOUND = -1

staticconstexpr

var_map

std::map<std::string, vart> CspMap::var_map

---

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

• src/goto-programs/goto_contractor.h