ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
Loading...
Searching...
No Matches
ReachabilityCompiler.cpp File Reference

Implementation of the decomposition-aligned reachability compiler. More...

#include "ReachabilityCompiler.h"
#include <algorithm>
#include <array>
#include <bitset>
#include <cstdint>
#include <functional>
#include <map>
#include <unordered_map>
#include <unordered_set>
#include <vector>
#include "postgres.h"
#include "miscadmin.h"
Include dependency graph for ReachabilityCompiler.cpp:

Go to the source code of this file.

Detailed Description

Implementation of the decomposition-aligned reachability compiler.

See ReachabilityCompiler.h for the construction's design and the structural argument (determinism and decomposability by construction).

The shared implementation makes two sweeps over a min-fill tree decomposition of the data graph, both with explicit stacks (decompositions of path-like data are themselves path-like, so recursion depth would be linear in the data):

  • bottom-up: for every node, the table mapping each reachable below state – the state over the node's domain induced by the edges introduced in its subtree – to the gate computing "the subtree edges induce exactly this state";
  • top-down: symmetrically, the above state tables over the edges introduced outside the subtree, derived from the parent's above table joined with the sibling subtrees' below tables (prefix/suffix joins keep this linear in the node arity) and the parent's local edges.

The domain of every node is its bag plus the source vertex (equivalently, the DP runs on the decomposition with the source added to every bag, still a valid decomposition of width at most tw+1). Each vertex is then read at its elimination bag: below and above states partition the worlds by their disjoint edge sets, so the acceptance test over the combination of the two states is a deterministic OR over decomposable AND pairs – one linear-size certified d-D whose gates are shared across all the per-vertex roots.

The DP scaffold is generic over the state algebra (the Ops template parameter below). Four instantiations:

  • BoolOps – plain reachability: the state is the transitively closed reachability relation over the domain (a bitset), composed by Warshall closure. This is the default behaviour.
  • HopOps – bounded-hop reachability: each relation entry is the set of achievable walk lengths up to the hop bound (a bitmask), composed in the capped min-plus-set semiring by the algebraic-path (Floyd-Warshall-Kleene) algorithm with diagonal star.
  • SetReachOps – any-of-S reachability: the relation plus one bit per position, "reaches an S-vertex within the processed part".
  • CoverOps – all-of-S (k-terminal) reachability: the relation plus the pending rescuer-set antichain (see its doc comment).

In every case worlds map to exactly one state, so states partition worlds and every emitted OR remains deterministic; each edge variable is still introduced at one node, so ANDs remain decomposable.

Definition in file ReachabilityCompiler.cpp.