IR fundamentals. More...

Classes
struct	base_info
	Tracks information for a base point. More...

class	cell_selector_factory
	Creates cell selectors. More...

class	certification
	Certifies automorphisms. More...

struct	controller
	Controls movement in IR tree. More...

class	deviation_map
	Store deviations for a BFS level. More...

class	graph_decomposer
	Decomposes graphs and manages decomposition information. More...

class	limited_save
	Reduced IR save state. More...

class	refinement
	Color refinement and related algorithms. More...

class	shared_leaves
	Collection of leaves. More...

class	shared_tree
	IR tree structure. More...

class	stored_leaf
	IR leaf. More...

class	trace
	The trace invariant. More...

class	tree_node
	A node of an IR tree. More...

Typedefs
typedef int	type_selector_hook(const coloring *, const int)

typedef std::pair< ir::tree_node *, int >	missing_node

typedef bool	type_split_color_hook(const int, const int, const int)

typedef bool	type_worklist_color_hook(const int, const int)

Enumerations
enum	ir_mode { IR_MODE_RECORD_TRACE , IR_MODE_COMPARE_TRACE_REVERSIBLE , IR_MODE_COMPARE_TRACE_IRREVERSIBLE }
	Mode of trace for IR search. More...

Detailed Description

IR fundamentals.

Contains fundamental algorithms and data structures to implement individualization-refinement algorithms. This includes graphs, colorings, color refinement, cell selectors as well as higher level control mechanisms.

Typedef Documentation

◆ missing_node

typedef std::pair<ir::tree_node*, int> dejavu::ir::missing_node

Definition at line 1972 of file ir.h.

◆ type_selector_hook

typedef int dejavu::ir::type_selector_hook(const coloring *, const int)

int type_selector_hook(coloring* c, const int s_base_pos);

Definition at line 38 of file ir.h.

◆ type_split_color_hook

typedef bool dejavu::ir::type_split_color_hook(const int, const int, const int)

Definition at line 130 of file refinement.h.

◆ type_worklist_color_hook

typedef bool dejavu::ir::type_worklist_color_hook(const int, const int)

Definition at line 134 of file refinement.h.

Enumeration Type Documentation

◆ ir_mode

enum dejavu::ir::ir_mode

Mode of trace for IR search.

The ir_mode determines in which mode the trace is used: whether a new trace is recorded, or whether the current computation is compared to a stored trace.

Enumerator
IR_MODE_RECORD_TRACE
IR_MODE_COMPARE_TRACE_REVERSIBLE
IR_MODE_COMPARE_TRACE_IRREVERSIBLE

Definition at line 31 of file ir.h.

Classes

Typedefs

Enumerations