![]() |
ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
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"
Go to the source code of this file.
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):
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.