Controls movement in IR tree. More...

#include <ir.h>

Collaboration diagram for dejavu::ir::controller:

Public Member Functions
	controller (refinement ref, coloring col)

int	get_number_of_splits ()

void	mode_write_base ()

void	mode_compare_base ()

bool	there_is_difference_to_base ()

void	singleton_automorphism_base (groups::automorphism_workspace *automorphism)

void	color_diff_automorphism_base (groups::automorphism_workspace *automorphism)

bool	there_is_difference_to_base_including_singles (int domain_size)

std::pair< int, int >	diff_pair (const controller &state)

void	reset_diff ()

void	singleton_automorphism (controller &state, groups::automorphism_workspace &automorphism)

dej_nodiscard int	get_diff_diverge () const

bool	update_diff_vertices_last_individualization (const controller &other_state)

void	link_compare (controller *state)

void	link (controller *state)

int	diff_num ()

void	compare_to_this ()

void	reserve ()

void	use_reversible (const bool reversible)

void	use_trace_early_out (bool trace_early_out)

void	use_increase_deviation (bool deviation_inc_active)

void	set_increase_deviation (int deviation_inc=48)

void	use_split_limit (bool use_split_limit, int limit=0)

void	reset_trace_equal ()

void	save_reduced_state (limited_save &state)

void	load_reduced_state (limited_save &state)

void	load_reduced_state_without_coloring (limited_save &state)

dej_nodiscard coloring *	get_coloring () const

dej_nodiscard int	get_base_pos () const

void	write_to_trace (const int d) const

void	write_strong_invariant (const sgraph *g) const

void	write_strong_invariant_quarter (const sgraph *g) const

void	move_to_child (sgraph *g, int v)

void	move_to_child_no_trace (sgraph *g, int v)

void	refine (sgraph *g)

void	move_to_parent ()

void	walk (sgraph *g, ir::limited_save &start_from, std::vector< int > &vertices)

bool	certify (sgraph *g, groups::automorphism_workspace &automorphism)

Public Attributes
coloring *	c = nullptr

trace *	T = nullptr

std::vector< int >	singletons

std::vector< int > *	compare_singletons = nullptr

std::vector< int >	base_vertex

std::vector< base_info >	base

std::vector< int > *	compare_base_vertex = nullptr

std::vector< base_info > *	compare_base = nullptr

coloring	leaf_color

markset	touched_color

worklist	touched_color_list

worklist	prev_color_list

int	s_base_pos = 0

Detailed Description

Controls movement in IR tree.

Keeps a state of an IR node. Enables the movement to a child of the node, or to the parent of the node. The controller manages data structures and functions, which facilitate the trace T as well as the reversal of color refinement.

Has different modes (managed by mode) depending on whether color refinement should be reversible or not.

Definition at line 130 of file ir.h.

Constructor & Destructor Documentation

◆ controller()

dejavu::ir::controller::controller	(	refinement *	ref,
		coloring *	col
	)

inline

Initialize this controller using a refinement and a graph coloring for the initial state.

Parameters

ref	The refinement workspace to use.
col	The initial coloring.

Definition at line 384 of file ir.h.

Member Function Documentation

◆ certify()

bool dejavu::ir::controller::certify	(	sgraph *	g,
		groups::automorphism_workspace &	automorphism
	)

inline

Certifies whether the provided automorphism is indeed an automorphism of the graph g. Runs in time roughly in the support of automorphism.

Uses internal workspace to perform this operation efficiently.

Parameters

g	The graph.
automorphism	The automorphism.

Returns: Whether automorphism is an automorphism of g.

Definition at line 1123 of file ir.h.

◆ color_diff_automorphism_base()

void dejavu::ir::controller::color_diff_automorphism_base ( groups::automorphism_workspace * automorphism )

inline

Definition at line 491 of file ir.h.

◆ compare_to_this()

void dejavu::ir::controller::compare_to_this ( )

inline

Compare all following computations to this IR node. The mode must be set to IR_MODE_RECORD_TRACE (using mode_write_base) to call this function. Changes mode to IR_MODE_COMPARE_TRACE_REVERSIBLE (i.e., such as calling mode_compare_base).

Definition at line 778 of file ir.h.

◆ diff_num()

int dejavu::ir::controller::diff_num ( )

inline

Definition at line 769 of file ir.h.

◆ diff_pair()

std::pair< int, int > dejavu::ir::controller::diff_pair ( const controller & state )

inline

Need to use difference-checking before. Returns a differing pair of vertices of the same non-singleton color.

Parameters

state the other state (for which we've checked differences before)

Returns

Definition at line 539 of file ir.h.

◆ get_base_pos()

dej_nodiscard int dejavu::ir::controller::get_base_pos ( ) const

inline

Definition at line 929 of file ir.h.

◆ get_coloring()

dej_nodiscard coloring * dejavu::ir::controller::get_coloring ( ) const

inline

Definition at line 925 of file ir.h.

◆ get_diff_diverge()

dej_nodiscard int dejavu::ir::controller::get_diff_diverge ( ) const

inline

Need to use difference-checking before. Returns whether the difference is diverging, i.e., there is no point in further difference checking since branches are non-isomorphic.

Returns: whether states are diverging

Definition at line 597 of file ir.h.

◆ get_number_of_splits()

int dejavu::ir::controller::get_number_of_splits ( )

inline

Definition at line 415 of file ir.h.

◆ link()

void dejavu::ir::controller::link ( controller * state )

inline

Copy the state of another controller. Does not copy the trace, but instead links the trace of this controller to the comparison state of the other (such that both states compare to the same single trace).

Parameters

state the other state which is copied

Definition at line 740 of file ir.h.

◆ link_compare()

void dejavu::ir::controller::link_compare ( controller * state )

inline

Copy the state of another controller. Does not copy the trace, but instead links the trace of this controller to the comparison state of the other (such that both states compare to the same single trace).

Parameters

state the other state which is copied

Definition at line 703 of file ir.h.

◆ load_reduced_state()

void dejavu::ir::controller::load_reduced_state ( limited_save & state )

inline

Load a partial state into this controller.

Parameters

state A reference to the limited_save from which the state will be loaded.

Definition at line 893 of file ir.h.

◆ load_reduced_state_without_coloring()

void dejavu::ir::controller::load_reduced_state_without_coloring ( limited_save & state )

inline

Definition at line 910 of file ir.h.

◆ mode_compare_base()

void dejavu::ir::controller::mode_compare_base ( )

inline

We compare to a pre-existing trace, recorded earlier using mode_write_base. Must use compare_to_this or provide a comparison trace in another manner before being able to use this mode in the intended manner.

Definition at line 442 of file ir.h.

◆ mode_write_base()

void dejavu::ir::controller::mode_write_base ( )

inline

Sets internal trace into recording mode. We write a trace which we might want to compare to later.

Always reversible (see also use_reversible).

Definition at line 424 of file ir.h.

◆ move_to_child()

void dejavu::ir::controller::move_to_child	(	sgraph *	g,
		int	v
	)

inline

Move IR node kept in this controller to a child, specified by a vertex to be individualized.

Parameters

R	a refinement workspace
g	the graph
v	the vertex to be individualized

Definition at line 989 of file ir.h.

◆ move_to_child_no_trace()

void dejavu::ir::controller::move_to_child_no_trace	(	sgraph *	g,
		int	v
	)

inline

Move IR node kept in this controller to a child, specified by a vertex to be individualized.

Parameters

R	a refinement workspace
g	the graph
v	the vertex to be individualized

Definition at line 1040 of file ir.h.

◆ move_to_parent()

void dejavu::ir::controller::move_to_parent ( )

inline

Move IR node kept in this controller back to its parent.

Definition at line 1057 of file ir.h.

◆ refine()

void dejavu::ir::controller::refine ( sgraph * g )

inline

Perform color refinement on the internal coloring based on the given graph.

Parameters

g	The graph.

Definition at line 1050 of file ir.h.

◆ reserve()

void dejavu::ir::controller::reserve ( )

inline

Definition at line 800 of file ir.h.

◆ reset_diff()

void dejavu::ir::controller::reset_diff ( )

inline

Resets all difference-checking information.

Definition at line 566 of file ir.h.

◆ reset_trace_equal()

void dejavu::ir::controller::reset_trace_equal ( )

inline

Resets whether the trace is deemed equal to its comparison trace.

Definition at line 873 of file ir.h.

◆ save_reduced_state()

void dejavu::ir::controller::save_reduced_state ( limited_save & state )

inline

Save a partial state of this controller.

Parameters

state A reference to the limited_save in which the state will be stored.

Definition at line 883 of file ir.h.

◆ set_increase_deviation()

void dejavu::ir::controller::set_increase_deviation ( int deviation_inc = 48 )

inline

Whether to record additional deviation information once a deviation from the comparison trace is found. Only applicable when use_trace_early_out is set. Essentially delays the termination of color refinement to record more information into the trace invariant.

Parameters

deviation_inc how many deviations to add before terminating (default = 48)

Definition at line 854 of file ir.h.

◆ singleton_automorphism()

void dejavu::ir::controller::singleton_automorphism	(	controller &	state,
		groups::automorphism_workspace &	automorphism
	)

inline

Need to use difference-checking before. Makes a singleton automorphism with the singleton difference between this state and the given state.

Parameters

state	the other state
automorphism	workspace to write the automorphism to

Definition at line 584 of file ir.h.

◆ singleton_automorphism_base()

void dejavu::ir::controller::singleton_automorphism_base ( groups::automorphism_workspace * automorphism )

inline

Make an automorphism with the current singletons and the singletons of the base, i.e., useful when there_is_difference_to_base returns false.

Parameters

automorphism workspace to write the automorphism to

Definition at line 478 of file ir.h.

◆ there_is_difference_to_base()

bool dejavu::ir::controller::there_is_difference_to_base ( )

inline

Checks whether the current coloring matches the coloring on the base (AKA in saucy terms, whether this ordered partition and the one on the base are matched).

Returns: whether the colorings match

Definition at line 452 of file ir.h.

◆ there_is_difference_to_base_including_singles()

bool dejavu::ir::controller::there_is_difference_to_base_including_singles ( int domain_size )

inline

Checks whether the current coloring matches the coloring on the base, including singletons (AKA, whether the colorings are equal). Useful for debugging.

Returns: whether the colorings are equal

Definition at line 513 of file ir.h.

◆ update_diff_vertices_last_individualization()

bool dejavu::ir::controller::update_diff_vertices_last_individualization ( const controller & other_state )

inline

Difference-checking. Records differences between this state and the given other_state. Before using this, this state and other_state should start from the same node of the IR tree, and the difference should be reset at that point. Then, after each individualization this update function should be called. The function keeps track of all colors that are non-matching.

Parameters

other_state the other state

Returns: whether there is a difference

Definition at line 611 of file ir.h.

◆ use_increase_deviation()

void dejavu::ir::controller::use_increase_deviation ( bool deviation_inc_active )

inline

Whether to record additional deviation information once a deviation from the comparison trace is found. Only applicable when use_trace_early_out is set. Essentially delays the termination of color refinement to record more information into the trace invariant.

Parameters

deviation_inc_active Whether increased deviation is recorded or not.

Definition at line 843 of file ir.h.

◆ use_reversible()

void dejavu::ir::controller::use_reversible ( const bool reversible )

inline

Enables or disables whether following move_to_child calls will be reversible using move_to_parent, or not. Using non-reversible calls to move_to_child is faster.

When recording a trace using mode_write_base, computations are always reversible and calling this function will have no effect.

Parameters

reversible

Definition at line 816 of file ir.h.

◆ use_split_limit()

void dejavu::ir::controller::use_split_limit	(	bool	use_split_limit,
		int	limit = `0`
	)

inline

Whether to record additional deviation information once a deviation from the comparison trace is found. Only applicable when use_trace_early_out is set. Essentially delays the termination of color refinement to record more information into the trace invariant.

Parameters

deviation_inc_active Whether increased deviation is recorded or not.

Definition at line 865 of file ir.h.

◆ use_trace_early_out()

void dejavu::ir::controller::use_trace_early_out ( bool trace_early_out )

inline

Whether to terminate color refinement whenever a deviation to its comparison trace is found.

Parameters

trace_early_out Flag that determines whether the early out is used.

Definition at line 831 of file ir.h.

◆ walk()

void dejavu::ir::controller::walk	(	sgraph *	g,
		ir::limited_save &	start_from,
		std::vector< int > &	vertices
	)

inline

Perform the given walk from the given IR node.

Parameters

g	The graph.
start_from	A limited_save describing the IR node from which the walk should be performed.
vertices	A vector of vertices that describes the walk, i.e., these vertices will be individualized in the given order.

Definition at line 1104 of file ir.h.

◆ write_strong_invariant()

void dejavu::ir::controller::write_strong_invariant ( const sgraph * g ) const

inline

Writes a stronger invariant using the internal coloring and graph to the trace.

Parameters

g	The graph.

Definition at line 948 of file ir.h.

◆ write_strong_invariant_quarter()

void dejavu::ir::controller::write_strong_invariant_quarter ( const sgraph * g ) const

inline

Writes a stronger invariant using the internal coloring and graph to the trace, but less strong than the one written by write_strong_invariant.

Parameters

g	The graph.

Definition at line 968 of file ir.h.

◆ write_to_trace()

void dejavu::ir::controller::write_to_trace ( const int d ) const

inline

Write additional information into the internal trace. Care must be taken that the written data is isomorphism-invariant.

Parameters

d	Data to be written to the trace.

Definition at line 939 of file ir.h.

Member Data Documentation

◆ base

std::vector<base_info> dejavu::ir::controller::base

current base (i.e., root-to-node path)

Definition at line 139 of file ir.h.

◆ base_vertex

std::vector<int> dejavu::ir::controller::base_vertex

singletons of the comparison trace

Definition at line 138 of file ir.h.

◆ c

coloring* dejavu::ir::controller::c = nullptr

coloring to be moved around in the tree

Definition at line 132 of file ir.h.

◆ compare_base

std::vector<base_info>* dejavu::ir::controller::compare_base = nullptr

comparison base

Definition at line 142 of file ir.h.

◆ compare_base_vertex

std::vector<int>* dejavu::ir::controller::compare_base_vertex = nullptr

additional info for the current base

Definition at line 141 of file ir.h.

◆ compare_singletons

std::vector<int>* dejavu::ir::controller::compare_singletons = nullptr

singletons of the current trace

Definition at line 136 of file ir.h.

◆ leaf_color

coloring dejavu::ir::controller::leaf_color

additional info of the comparison base

Definition at line 144 of file ir.h.

◆ prev_color_list

worklist dejavu::ir::controller::prev_color_list

...and its vertices were previously of color prev_color_list[i]

Definition at line 148 of file ir.h.

◆ s_base_pos

int dejavu::ir::controller::s_base_pos = 0

how large the base of the current IR node is

Definition at line 151 of file ir.h.

◆ singletons

std::vector<int> dejavu::ir::controller::singletons

Definition at line 135 of file ir.h.

◆ T

trace* dejavu::ir::controller::T = nullptr

trace of current root-to-node path

Definition at line 133 of file ir.h.

◆ touched_color

markset dejavu::ir::controller::touched_color

comparison leaf coloring were changes in this color already tracked?

Definition at line 146 of file ir.h.

◆ touched_color_list

worklist dejavu::ir::controller::touched_color_list

color touched_color_list[i] was changed...

Definition at line 147 of file ir.h.

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

ir.h

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ controller()

Member Function Documentation

◆ certify()

◆ color_diff_automorphism_base()

◆ compare_to_this()

◆ diff_num()

◆ diff_pair()

◆ get_base_pos()

◆ get_coloring()

◆ get_diff_diverge()

◆ get_number_of_splits()

◆ link()

◆ link_compare()

◆ load_reduced_state()

◆ load_reduced_state_without_coloring()

◆ mode_compare_base()

◆ mode_write_base()

◆ move_to_child()

◆ move_to_child_no_trace()

◆ move_to_parent()

◆ refine()

◆ reserve()

◆ reset_diff()

◆ reset_trace_equal()

◆ save_reduced_state()

◆ set_increase_deviation()

◆ singleton_automorphism()

◆ singleton_automorphism_base()

◆ there_is_difference_to_base()

◆ there_is_difference_to_base_including_singles()

◆ update_diff_vertices_last_individualization()

◆ use_increase_deviation()

◆ use_reversible()

◆ use_split_limit()

◆ use_trace_early_out()

◆ walk()

◆ write_strong_invariant()

◆ write_strong_invariant_quarter()

◆ write_to_trace()

Member Data Documentation

◆ base

◆ base_vertex

◆ c

◆ compare_base

◆ compare_base_vertex

◆ compare_singletons

◆ leaf_color

◆ prev_color_list

◆ s_base_pos

◆ singletons

◆ T

◆ touched_color

◆ touched_color_list