transition_system.h File Reference

#include <irep2/irep2.h>
#include <util/irep/location.h>
#include <util/symtab/namespace.h>
#include <iosfwd>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <utility>
#include <vector>

Include dependency graph for transition_system.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	transition_systemt
	Transition system here represents a sequential circuit. More...
struct	transition_systemt::propertyt
struct	transition_systemt::statet
class	ts_step_renamert
	Instantiates expressions at one step, sharing the rewrite across calls so subterms common to several expressions are copied once. More...

Functions
void	collect_symbols (const expr2tc &e, std::unordered_set< expr2tc, irep2_hash > &out, std::unordered_set< const expr2t * > &seen)
	Collect every symbol2t in e into out, treating seen as a shared visited set so a DAG node reached by many parents is walked once.

Function Documentation

collect_symbols()

void collect_symbols	(	const expr2tc &	e,
		std::unordered_set< expr2tc, irep2_hash > &	out,
		std::unordered_set< const expr2t * > &	seen )

Collect every symbol2t in e into out, treating seen as a shared visited set so a DAG node reached by many parents is walked once.

Unlike irep2_utils' get_symbols this keeps __ESBMC_ symbols: the memory-model bookkeeping they name is a real dependency of the formula.