Internal canonicalization kernel for SMTStabilizer. More...

#include <kernel.h>

Public Member Functions
	Kernel ()=delete

	Kernel (node::NodeManager &nm, const bool &context_propagation=true, const bool &symmetry_breaking_perturbation=true)
	Build kernel state from the current node manager assertions.

void	apply (node::NodeManager &nm)
	Run the full stabilization pass and mutate node manager state.

Private Member Functions
bool	is_commutative (const size_t &i, const bool &from_cache=true)
	Check whether node kind at index `i` is treated as commutative.

void	context_propagate (const std::vector< size_t > &processing, const std::vector< size_t > &symbols)
	Run propagation to a fixed point over a selected subgraph.

void	specific_propagate ()
	Apply local perturbation to break remaining hash collisions.

void	rebuild_graph ()
	Keep only currently ambiguous graph regions for next iteration.

void	sort_propagate (std::unordered_map< std::string, node::Sort > &sort_key_map, std::vector< std::vector< parser::Parser::DTTypeDecl > > &datatype_blocks)
	Incorporate sort/datatype structure into propagation and naming.

void	propagate (const std::vector< size_t > &processing)
	One directional propagation pass on the selected nodes.

Private Attributes
std::vector< std::vector< size_t > >	d_graph

std::vector< std::vector< std::pair< size_t, size_t > > >	d_reversed_graph

std::vector< size_t >	d_hash_table

std::vector< size_t >	d_context_hash

std::vector< node::Node >	d_nodes

std::vector< size_t >	d_processing

std::vector< size_t >	d_symbols

std::vector< size_t >	d_unique_symbols

std::vector< uint8_t >	d_visited

std::vector< uint8_t >	d_is_commutative

std::vector< uint8_t >	d_is_symbol

size_t	d_symbol_num

bool	d_context_propagation = true

bool	d_symmetry_breaking_perturbation = true

Detailed Description

Internal canonicalization kernel for SMTStabilizer.

The kernel owns graph-oriented views over the assertion DAG and applies multi-stage hash propagation to derive a deterministic symbol/function ordering. It is intentionally documented for maintainers even though most stage methods are private.

Definition at line 39 of file kernel.h.

Constructor & Destructor Documentation

◆ Kernel() [1/2]

stabilizer::kernel::Kernel::Kernel ( )

delete

◆ Kernel() [2/2]

stabilizer::kernel::Kernel::Kernel	(	node::NodeManager &	nm,
		const bool &	context_propagation = `true`,
		const bool &	symmetry_breaking_perturbation = `true`
	)

Build kernel state from the current node manager assertions.

Construct graph caches and reverse-topological node storage.

Parameters

nm	Node manager that provides the DAG roots and symbol tables.
context_propagation	Enable fixed-point context propagation.
symmetry_breaking_perturbation	Enable iterative subgraph-based tie breaking for colliding symbols.

Algorithm outline:

Traverse assertion roots and collect reachable DAG nodes.
Build forward and reverse adjacency with operator-position metadata.
Classify symbol-like nodes and initialize base hash seeds.

Definition at line 48 of file kernel.cpp.

References d_graph, d_hash_table, d_is_commutative, d_is_symbol, d_nodes, d_processing, d_reversed_graph, d_symbol_num, d_symbols, d_visited, stabilizer::util::hash_combine(), stabilizer::util::hash_node(), is_commutative(), stabilizer::parser::NT_AND, stabilizer::parser::NT_EXISTS, stabilizer::parser::NT_FORALL, stabilizer::parser::NT_FP_ADD, and stabilizer::parser::NT_FP_MUL.

Member Function Documentation

◆ apply()

void stabilizer::kernel::Kernel::apply ( node::NodeManager & nm )

Run the full stabilization pass and mutate node manager state.

Execute the full kernel pipeline on node manager state.

Side effects include:

Renaming symbols and UF/function declarations to canonical names.
Reordering assertions and selected declaration blocks.
Updating datatype and sort naming maps when applicable.

Parameters

nm	Node manager to be rewritten in place.

High-level flow:

Seed hashes for function definitions and run global context propagation.
Optionally refine with sort/datatype-aware propagation.
Resolve collisions via specific propagation and graph rebuild rounds.
Canonicalize symbol/function names and reorder declarations/assertions.

Definition at line 575 of file kernel.cpp.

References context_propagate(), d_context_hash, d_hash_table, d_nodes, d_processing, d_symbol_num, d_symbols, d_symmetry_breaking_perturbation, d_unique_symbols, stabilizer::util::hash_combine(), stabilizer::parser::NT_DT_TESTER, rebuild_graph(), stabilizer::parser::SK_DEC, sort_propagate(), and specific_propagate().

Referenced by stabilizer::api::SMTStabilizer::run_pipeline().

◆ context_propagate()

void stabilizer::kernel::Kernel::context_propagate	(	const std::vector< size_t > &	processing,
		const std::vector< size_t > &	symbols
	)

private

Run propagation to a fixed point over a selected subgraph.

Repeat propagation until symbol hash cardinality converges.

Parameters

processing	Node indices participating in propagation.
symbols	Symbol indices monitored for convergence.

The stage tracks unique symbol hashes after each round and stops when the number of unique values no longer increases.

Definition at line 205 of file kernel.cpp.

References propagate().

Referenced by apply(), sort_propagate(), and specific_propagate().

◆ is_commutative()

bool stabilizer::kernel::Kernel::is_commutative	(	const size_t &	i,
		const bool &	from_cache = `true`
	)

private

Check whether node kind at index i is treated as commutative.

Parameters

i	Node index in the internal node vector.
from_cache	Use cached commutativity when true.

Definition at line 110 of file kernel.cpp.

Referenced by Kernel(), propagate(), and sort_propagate().

◆ propagate()

void stabilizer::kernel::Kernel::propagate ( const std::vector< size_t > & processing )

private

One directional propagation pass on the selected nodes.

Parameters

processing Node indices to process in the current round.

Definition at line 157 of file kernel.cpp.

References d_context_propagation, d_graph, d_hash_table, d_reversed_graph, stabilizer::util::hash_children(), stabilizer::util::hash_communative_children(), stabilizer::util::hash_parents(), and is_commutative().

Referenced by context_propagate().

◆ rebuild_graph()

void stabilizer::kernel::Kernel::rebuild_graph ( )

private

Keep only currently ambiguous graph regions for next iteration.

Rebuild active processing graph to unresolved nodes only.

Nodes with unique hash values are pruned from subsequent iterations; the remaining ambiguous nodes keep only edges to other ambiguous nodes.

Definition at line 306 of file kernel.cpp.

References d_graph, d_hash_table, d_is_symbol, d_processing, d_reversed_graph, d_symbols, d_unique_symbols, and d_visited.

Referenced by apply().

◆ sort_propagate()

void stabilizer::kernel::Kernel::sort_propagate	(	std::unordered_map< std::string, node::Sort > &	sort_key_map,
		std::vector< std::vector< parser::Parser::DTTypeDecl > > &	datatype_blocks
	)

private

Incorporate sort/datatype structure into propagation and naming.

Propagate sort/datatype constraints into hash refinement.

Parameters

sort_key_map	Mutable sort name map from node manager/parser.
datatype_blocks	Mutable datatype declaration blocks.

This stage temporarily augments the graph with sort vertices, stabilizes their ordering, renames sort/datatype symbols, and then restores core graph structures while keeping updated hash information.

Definition at line 360 of file kernel.cpp.

References context_propagate(), d_graph, d_hash_table, d_is_commutative, d_nodes, d_reversed_graph, d_symbols, stabilizer::util::hash_combine(), and is_commutative().

Referenced by apply().

◆ specific_propagate()

void stabilizer::kernel::Kernel::specific_propagate ( )

private

Apply local perturbation to break remaining hash collisions.

Resolve collisions within connected regions by targeted perturbation.

Algorithm outline:

Explore one unvisited symbol region at a time.
Compute region fingerprint and inject region-level tie-break data.
If duplicate symbol hashes remain, perturb one selected symbol and rerun context propagation on the region.

Definition at line 229 of file kernel.cpp.

References context_propagate(), d_graph, d_hash_table, d_is_symbol, d_processing, d_reversed_graph, d_symbols, d_visited, stabilizer::util::hash_combine(), and stabilizer::util::hash_communative_children().

Referenced by apply().

Member Data Documentation

◆ d_context_hash

std::vector<size_t> stabilizer::kernel::Kernel::d_context_hash

private

Definition at line 68 of file kernel.h.

Referenced by apply().

◆ d_context_propagation

bool stabilizer::kernel::Kernel::d_context_propagation = true

private

Definition at line 84 of file kernel.h.

Referenced by propagate().

◆ d_graph

std::vector<std::vector<size_t> > stabilizer::kernel::Kernel::d_graph

private

Definition at line 65 of file kernel.h.

Referenced by Kernel(), propagate(), rebuild_graph(), sort_propagate(), and specific_propagate().

◆ d_hash_table

std::vector<size_t> stabilizer::kernel::Kernel::d_hash_table

private

Definition at line 67 of file kernel.h.

Referenced by apply(), Kernel(), propagate(), rebuild_graph(), sort_propagate(), and specific_propagate().

◆ d_is_commutative

std::vector<uint8_t> stabilizer::kernel::Kernel::d_is_commutative

private

Definition at line 77 of file kernel.h.

Referenced by is_commutative(), Kernel(), and sort_propagate().

◆ d_is_symbol

std::vector<uint8_t> stabilizer::kernel::Kernel::d_is_symbol

private

Definition at line 78 of file kernel.h.

Referenced by Kernel(), rebuild_graph(), and specific_propagate().

◆ d_nodes

std::vector<node::Node> stabilizer::kernel::Kernel::d_nodes

private

Definition at line 69 of file kernel.h.

Referenced by apply(), is_commutative(), Kernel(), and sort_propagate().

◆ d_processing

std::vector<size_t> stabilizer::kernel::Kernel::d_processing

private

Definition at line 70 of file kernel.h.

Referenced by apply(), Kernel(), rebuild_graph(), and specific_propagate().

◆ d_reversed_graph

std::vector<std::vector<std::pair<size_t, size_t> > > stabilizer::kernel::Kernel::d_reversed_graph

private

Definition at line 66 of file kernel.h.

Referenced by Kernel(), propagate(), rebuild_graph(), sort_propagate(), and specific_propagate().

◆ d_symbol_num

size_t stabilizer::kernel::Kernel::d_symbol_num

private

Definition at line 82 of file kernel.h.

Referenced by apply(), and Kernel().

◆ d_symbols

std::vector<size_t> stabilizer::kernel::Kernel::d_symbols

private

Definition at line 72 of file kernel.h.

Referenced by apply(), Kernel(), rebuild_graph(), sort_propagate(), and specific_propagate().

◆ d_symmetry_breaking_perturbation

bool stabilizer::kernel::Kernel::d_symmetry_breaking_perturbation = true

private

Definition at line 85 of file kernel.h.

Referenced by apply().

◆ d_unique_symbols

std::vector<size_t> stabilizer::kernel::Kernel::d_unique_symbols

private

Definition at line 73 of file kernel.h.

Referenced by apply(), and rebuild_graph().

◆ d_visited

std::vector<uint8_t> stabilizer::kernel::Kernel::d_visited

private

Definition at line 76 of file kernel.h.

Referenced by Kernel(), rebuild_graph(), and specific_propagate().

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

src/kernel/kernel.h
src/kernel/kernel.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Kernel() [1/2]

◆ Kernel() [2/2]

Member Function Documentation

◆ apply()

◆ context_propagate()

◆ is_commutative()

◆ propagate()

◆ rebuild_graph()

◆ sort_propagate()

◆ specific_propagate()

Member Data Documentation

◆ d_context_hash

◆ d_context_propagation

◆ d_graph

◆ d_hash_table

◆ d_is_commutative

◆ d_is_symbol

◆ d_nodes

◆ d_processing

◆ d_reversed_graph

◆ d_symbol_num

◆ d_symbols

◆ d_symmetry_breaking_perturbation

◆ d_unique_symbols

◆ d_visited