Compiles s-t reachability over a probabilistic edge relation into a d-D, along a tree decomposition of the data graph. More...

#include "ReachabilityCompiler.h"

Classes
struct	EdgeRow
	One row of the edge relation. More...
struct	Stats
	Structural statistics of a compilation, for diagnostics and tests. More...
struct	Result
	A compiled reachability query: the d-D and its statistics. More...
struct	VertexRoot
	One vertex's reachability circuit in an all-targets compilation. More...
struct	AllResult
	An all-targets compilation: one shared d-D, one root per reachable vertex. More...
struct	VertexHopRoot
	One (vertex, walk length) circuit of a bounded-hop compilation. More...
struct	AllHopsResult
	A bounded-hop all-targets compilation. More...
struct	AnyReachAllResult
	A multi-set any-reach compilation: one shared circuit, one root per target set. More...
struct	SourceArc
	One source of a multi-source compilation. More...

Static Public Member Functions
static Result	compile (const std::vector< EdgeRow > &rows, unsigned long source, unsigned long target, bool directed, std::size_t max_states=DEFAULT_MAX_STATES)
	Compile s-t reachability over `rows` into a d-D.
static AllResult	compileAll (const std::vector< EdgeRow > &rows, unsigned long source, bool directed, std::size_t max_states=DEFAULT_MAX_STATES)
	Compile the reachability circuits of every vertex in one pass.
static AllResult	compileAll (const std::vector< EdgeRow > &rows, const std::vector< SourceArc > &sources, bool directed, std::size_t max_states=DEFAULT_MAX_STATES)
	Multi-source variant of `compileAll()`.
static AllHopsResult	compileAllHops (const std::vector< EdgeRow > &rows, unsigned long source, bool directed, unsigned hop_bound, std::size_t max_states=DEFAULT_MAX_STATES)
	Bounded-hop variant of `compileAll()`: per-(vertex, exact walk length) circuits for every length up to `hop_bound`.
static AllHopsResult	compileAllHops (const std::vector< EdgeRow > &rows, const std::vector< SourceArc > &sources, bool directed, unsigned hop_bound, std::size_t max_states=DEFAULT_MAX_STATES)
	Multi-source bounded-hop compilation.
static Result	compileAnyReach (const std::vector< EdgeRow > &rows, const std::vector< SourceArc > &sources, const std::vector< unsigned long > &set, bool directed, std::size_t max_states=DEFAULT_MAX_STATES)
	Compile "some vertex of @p set is reachable" into one certified circuit.
static AnyReachAllResult	compileAnyReachAll (const std::vector< EdgeRow > &rows, const std::vector< SourceArc > &sources, const std::vector< std::vector< unsigned long > > &sets, bool directed, std::size_t max_states=DEFAULT_MAX_STATES)
	Multi-set variant of `compileAnyReach()`: one shared circuit, one root per target set.
static Result	compileCoverReach (const std::vector< EdgeRow > &rows, const std::vector< SourceArc > &sources, const std::vector< unsigned long > &set, bool directed, std::size_t max_states=DEFAULT_MAX_STATES)
	Compile "every vertex of @p set is reachable" (k-terminal / coverage reachability) into one certified circuit.
static AnyReachAllResult	compileCoverReachAll (const std::vector< EdgeRow > &rows, const std::vector< SourceArc > &sources, const std::vector< std::vector< unsigned long > > &sets, bool directed, std::size_t max_states=DEFAULT_MAX_STATES)
	Multi-set variant of `compileCoverReach()`: one shared (content-deduplicated) circuit, one root per set, as `compileAnyReachAll()`.

Static Public Attributes
static constexpr std::size_t	DEFAULT_MAX_STATES = 100000
	Default bound on the number of DP states at a single decomposition node.
static constexpr unsigned	MAX_HOP_BOUND = 62
	Maximum supported hop bound for `compileAllHops()`.

Detailed Description

Compiles s-t reachability over a probabilistic edge relation into a d-D, along a tree decomposition of the data graph.

Definition at line 74 of file ReachabilityCompiler.h.

Member Function Documentation

◆ compile()

ReachabilityCompiler::Result ReachabilityCompiler::compile	(	const std::vector< EdgeRow > &	rows,
		unsigned long	source,
		unsigned long	target,
		bool	directed,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Compile s-t reachability over rows into a d-D.

Parameters

rows	Edge tuples (vertex IDs, provenance token, probability).
source	Source vertex `s`.
target	Target vertex `t`.
directed	If `false`, every edge contributes both arcs (undirected connectivity).
max_states	Bound on the DP state count per node.

Returns: The compiled d-D and statistics.

Exceptions

TreeDecompositionException	if the data treewidth exceeds `TreeDecomposition::MAX_TREEWIDTH`.
ReachabilityCompilerException	on unsupported input shapes or when `max_states` is exceeded.

Definition at line 1851 of file ReachabilityCompiler.cpp.

Here is the call graph for this function:

◆ compileAll() [1/2]

ReachabilityCompiler::AllResult ReachabilityCompiler::compileAll	(	const std::vector< EdgeRow > &	rows,
		const std::vector< SourceArc > &	sources,
		bool	directed,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Multi-source variant of compileAll().

Reachability is from a virtual super-source whose arcs to the sources are gated by the source tuples' tokens (or always present for certain sources); a vertex's circuit therefore computes "some present source reaches it". Everything else is as in compileAll(); the super-source itself is not reported in the roots.

Parameters

rows	Edge tuples.
sources	Source arcs (at least one).
directed	If `false`, every edge contributes both arcs.
max_states	Bound on the DP state count per node.

Returns: The shared d-D, per-vertex roots, statistics.

Definition at line 1768 of file ReachabilityCompiler.cpp.

◆ compileAll() [2/2]

ReachabilityCompiler::AllResult ReachabilityCompiler::compileAll	(	const std::vector< EdgeRow > &	rows,
		unsigned long	source,
		bool	directed,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Compile the reachability circuits of every vertex in one pass.

Two sweeps over the tree decomposition – bottom-up per-subtree state tables, then a top-down "rest of the graph" pass – yield, for each vertex read at its elimination bag, the deterministic OR over compatible (below, above) state pairs whose closure connects the source to it. Total circuit size stays linear in the number of edges for fixed data treewidth: gates are shared across the per-vertex roots. This matches the semantics of the recursive-query relation reach: one root per vertex reachable in the all-edges-present world (vertices certainly unreachable are omitted).

Parameters

rows	Edge tuples (vertex IDs, provenance token, probability).
source	Source vertex `s`.
directed	If `false`, every edge contributes both arcs.
max_states	Bound on the DP state count per node.

Returns: The shared d-D, per-vertex roots, statistics.

Exceptions

TreeDecompositionException / ReachabilityCompilerException as for compile().

Definition at line 1758 of file ReachabilityCompiler.cpp.

Here is the caller graph for this function:

◆ compileAllHops() [1/2]

ReachabilityCompiler::AllHopsResult ReachabilityCompiler::compileAllHops	(	const std::vector< EdgeRow > &	rows,
		const std::vector< SourceArc > &	sources,
		bool	directed,
		unsigned	hop_bound,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Multi-source bounded-hop compilation.

The virtual super-source's arcs contribute walk length zero, so the reported lengths count edges of the underlying graph only.

Parameters

rows	Edge tuples.
sources	Source arcs (at least one).
directed	If `false`, every edge contributes both arcs.
hop_bound	Maximum walk length (at most `MAX_HOP_BOUND`).
max_states	Bound on the DP state count per node.

Returns: As the single-source overload.

Definition at line 1789 of file ReachabilityCompiler.cpp.

◆ compileAllHops() [2/2]

ReachabilityCompiler::AllHopsResult ReachabilityCompiler::compileAllHops	(	const std::vector< EdgeRow > &	rows,
		unsigned long	source,
		bool	directed,
		unsigned	hop_bound,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Bounded-hop variant of compileAll(): per-(vertex, exact walk length) circuits for every length up to hop_bound.

Same DP, richer state: the relation entries are sets of achievable walk lengths (bitmasks capped at hop_bound) instead of single reachability bits, composed in the capped min-plus-set semiring (Kleene closure with diagonal star). States still partition the worlds of the introduced edge variables, so determinism and decomposability hold by the same argument; the price is the larger state space, guarded by max_states as before.

Parameters

rows	Edge tuples.
source	Source vertex.
directed	If `false`, every edge contributes both arcs.
hop_bound	Maximum walk length (at most `MAX_HOP_BOUND`).
max_states	Bound on the DP state count per node.

Returns: The shared d-D, per-(vertex, length) and per-vertex within-bound roots, statistics.

Definition at line 1778 of file ReachabilityCompiler.cpp.

Here is the caller graph for this function:

◆ compileAnyReach()

ReachabilityCompiler::Result ReachabilityCompiler::compileAnyReach	(	const std::vector< EdgeRow > &	rows,
		const std::vector< SourceArc > &	sources,
		const std::vector< unsigned long > &	set,
		bool	directed,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Compile "some vertex of @p set is reachable" into one certified circuit.

Same DP, with the state extended by one bit per domain position – "this position reaches some @p set vertex within the processed part" – folded under closure and projection, so the single acceptance bit (at the source's position, over the root's table) is read in one bottom-up sweep. This is the deterministic circuit for the OR of the per-vertex reachability roots over set – which, as an OR of correlated events (shared edges), could not otherwise be marked: it serves cross-vertex aggregations ("is some vertex of this region reachable") the per-vertex roots cannot.

Parameters

rows	Edge tuples.
sources	Source arcs (at least one).
set	The target vertex set (need not intersect the graph; an absent vertex contributes nothing).
directed	If `false`, every edge contributes both arcs.
max_states	Bound on the DP state count per node.

Returns: The circuit, its root computing the disjunction, and statistics.

Definition at line 1800 of file ReachabilityCompiler.cpp.

◆ compileAnyReachAll()

ReachabilityCompiler::AnyReachAllResult ReachabilityCompiler::compileAnyReachAll	(	const std::vector< EdgeRow > &	rows,
		const std::vector< SourceArc > &	sources,
		const std::vector< std::vector< unsigned long > > &	sets,
		bool	directed,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Multi-set variant of compileAnyReach(): one shared circuit, one root per target set.

The shared prelude – variable grouping, tree decomposition of the data graph, bag assignments, literal gates – is built once; one bottom-up sweep then runs per set, with content-deduplicated gate emission, so the parts of the circuit a set's seeds do not touch are literally shared across sets (the per-set sweeps re-derive the same gates). This is the engine behind cross-vertex aggregation planting, where one query yields many groups over the same graph.

Parameters

rows	Edge tuples.
sources	Source arcs (at least one).
sets	The target vertex sets (at least one; an absent vertex contributes nothing).
directed	If `false`, every edge contributes both arcs.
max_states	Bound on the DP state count per node.

Returns: The shared circuit, one root per set (in input order), and statistics.

Definition at line 1815 of file ReachabilityCompiler.cpp.

Here is the caller graph for this function:

◆ compileCoverReach()

ReachabilityCompiler::Result ReachabilityCompiler::compileCoverReach	(	const std::vector< EdgeRow > &	rows,
		const std::vector< SourceArc > &	sources,
		const std::vector< unsigned long > &	set,
		bool	directed,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Compile "every vertex of @p set is reachable" (k-terminal / coverage reachability) into one certified circuit.

Same DP, with the state extended by the pending rescuer-set antichain: a forgotten target vertex not yet reached by the source pends on the boundary positions that reach it (its rescuers), the sets staying closed under the relation, shrinking losslessly at forgets, discharged when the source reaches them and absorbed by the empty (reject) set; acceptance, after a final collapse onto the source domain, is the empty antichain. Worlds map to one state each, so the circuit is a certified d-D like the rest of the family: probability evaluation gives k-terminal reliability, and absorptive-semiring evaluation is exact too – nonnegative min-plus gives the cost of the cheapest covering subgraph (directed Steiner cost).

Parameters

rows	Edge tuples.
sources	Source arcs (at least one).
set	The target vertex set; a vertex absent from the graph is unreachable, so the result is constant false.
directed	If `false`, every edge contributes both arcs.
max_states	Bound on the DP state count per node.

Returns: The circuit, its root computing the conjunction, and statistics.

Definition at line 1825 of file ReachabilityCompiler.cpp.

◆ compileCoverReachAll()

ReachabilityCompiler::AnyReachAllResult ReachabilityCompiler::compileCoverReachAll	(	const std::vector< EdgeRow > &	rows,
		const std::vector< SourceArc > &	sources,
		const std::vector< std::vector< unsigned long > > &	sets,
		bool	directed,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Multi-set variant of compileCoverReach(): one shared (content-deduplicated) circuit, one root per set, as compileAnyReachAll().

Definition at line 1840 of file ReachabilityCompiler.cpp.

Here is the caller graph for this function:

Member Data Documentation

◆ DEFAULT_MAX_STATES

std::size_t ReachabilityCompiler::DEFAULT_MAX_STATES = 100000

staticconstexpr

Default bound on the number of DP states at a single decomposition node.

The state space at a node is the set of reachable transitively-closed relations over at most MAX_TREEWIDTH+3 elements; it is bounded for fixed treewidth but can still be large near the treewidth cap, so a guard keeps compilation from exhausting memory on adversarial data.

Definition at line 179 of file ReachabilityCompiler.h.

◆ MAX_HOP_BOUND

unsigned ReachabilityCompiler::MAX_HOP_BOUND = 62

staticconstexpr

Maximum supported hop bound for compileAllHops().

Length sets are bitmasks over walk lengths 0..bound in a 64-bit word; the driver falls back to the generic fixpoint above this.

Definition at line 187 of file ReachabilityCompiler.h.

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

/home/senellar/git/software/provsql/src/ReachabilityCompiler.h
/home/senellar/git/software/provsql/src/ReachabilityCompiler.cpp

Classes

Static Public Member Functions

Static Public Attributes

Detailed Description

Member Function Documentation

◆ compile()

◆ compileAll() [1/2]

◆ compileAll() [2/2]

◆ compileAllHops() [1/2]

◆ compileAllHops() [2/2]

◆ compileAnyReach()

◆ compileAnyReachAll()

◆ compileCoverReach()

◆ compileCoverReachAll()

Member Data Documentation

◆ DEFAULT_MAX_STATES

◆ MAX_HOP_BOUND