 |
ProvSQL SQL API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
|
ProvSQL SQL API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
Compute the probability of a provenance token. More...
Topics | |
| Circuit initialization | |
| Register a tool, or replace the RECORD with the same logical name. | |
Functions | |
| TEXT | view_circuit (UUID token, REGCLASS token2desc, INT dbg=0) |
| Return a DOT or TEXT visualization of the provenance circuit. | |
| TEXT | compile_to_ddnnf_dot (UUID token, TEXT compiler='') |
| Return a DOT visualisation of the d-DNNF compiled from the provenance circuit. | |
| TEXT | compile_to_ddnnf (UUID token, TEXT compiler='') |
| Return the compiled d-DNNF of a provenance circuit in the c2d / d4 ".nnf" TEXT interchange format. | |
| jsonb | ddnnf_stats (UUID token, TEXT compiler='') |
| Structural statistics of the d-DNNF a compiler produces for a provenance circuit. | |
| TEXT | tseytin_cnf (UUID token, BOOLEAN weighted=TRUE, BOOLEAN mapping=TRUE) |
| Return the DIMACS CNF (Tseytin transformation) of the provenance circuit. | |
| jsonb | tseytin_cnf_mapping_json (UUID token) |
| Map each DIMACS variable of tseytin_cnf back to its provenance input. | |
| TABLE | tseytin_cnf_mapping (UUID token) |
| TEXT | tree_decomposition_dot (UUID token) |
| Return a DOT visualisation of the tree decomposition of the provenance circuit. | |
| BOOLEAN | tool_available (TEXT name) |
| Report whether an external tool is on the backend's resolved PATH. | |
| CREATE TABLE IF NOT EXISTS | tool_overrides (name TEXT PRIMARY KEY, removed BOOLEAN NOT NULL DEFAULT false, kind TEXT, executable TEXT, operations TEXT[], input_formats TEXT[], output_format TEXT, parser TEXT, preference INT, enabled BOOLEAN, dependencies TEXT[], argtpl TEXT, argtpl_circuit TEXT, endpoint TEXT) |
| Persistent overrides overlaid on the compiled-in tool seed. | |
| TABLE | tool_registry_list () |
Set-returning listing backing the provsql.tools view. | |
| VOID | register_tool (TEXT name, TEXT executable=NULL, TEXT kind='cli', TEXT[] operations=NULL, TEXT[] input_formats=NULL, TEXT output_format=NULL, TEXT parser=NULL, TEXT argtpl=NULL, TEXT argtpl_circuit=NULL, INT preference=0, BOOLEAN enabled=true, TEXT endpoint=NULL) |
| Register a tool, or replace the RECORD with the same logical name. | |
| VOID | unregister_tool (TEXT name) |
| Unregister a tool; errors on an unknown tool name. | |
| VOID | set_tool_enabled (TEXT name, BOOLEAN enabled) |
| Enable/disable a tool; errors on an unknown tool name. | |
| VOID | set_tool_preference (TEXT name, INT preference) |
| Set a tool's preference; errors on an unknown tool name. | |
| TEXT | to_provxml (UUID token, REGCLASS token2desc=NULL) |
| Return an XML representation of the provenance circuit. | |
| UUID | provenance () |
| Return the provenance token of the current query result tuple. | |
| TEXT | where_provenance (UUID token) |
| Compute where-provenance for a result tuple. | |
Variables | |
| CREATE OR REPLACE VIEW tools AS SELECT | name |
| Read-only view of the registered tools. | |
| CREATE OR REPLACE VIEW tools AS SELECT | kind |
| CREATE OR REPLACE VIEW tools AS SELECT | executable |
| CREATE OR REPLACE VIEW tools AS SELECT | operations |
| CREATE OR REPLACE VIEW tools AS SELECT | input_formats |
| CREATE OR REPLACE VIEW tools AS SELECT | output_format |
| CREATE OR REPLACE VIEW tools AS SELECT | parser |
| CREATE OR REPLACE VIEW tools AS SELECT | preference |
| CREATE OR REPLACE VIEW tools AS SELECT | enabled |
| CREATE OR REPLACE VIEW tools AS SELECT | argtpl |
| CREATE OR REPLACE VIEW tools AS SELECT | argtpl_circuit |
| CREATE OR REPLACE VIEW tools AS SELECT | endpoint |
Compute the probability of a provenance token.
Functions for visualizing and exporting provenance circuits in various formats.
Compiles the provenance circuit to d-DNNF and evaluates the probability. The compilation method can be selected explicitly.
| token | provenance token to evaluate |
| method | knowledge compilation method (NULL for default) |
| arguments | additional arguments for the method |
Cheap certified probability interval of a DNF-shaped circuit.
Returns [lower,upper] with lower <= probability_evaluate(token) <= upper, computed without compiling the circuit (the Olteanu-Huang d-tree leaf bound). Errors when token is not a monotone DNF over input leaves.
Compute the expected value of a probabilistic scalar
Computes E[input | prov] for either an AGG_TOKEN (discrete SUM/MIN/MAX aggregation over Boolean-input gate_agg circuits, with prov as the Boolean conditioning event) or a random_variable (continuous distribution, traversed by the analytical / MC evaluator from Expectation.cpp).
Implementation: thin wrapper over moment(input, 1, prov, method,
arguments). Both branches converge on the same machinery; the AGG_TOKEN side computes E[X] as the \(k=1\) instance of the \(n^k\)-tuple enumeration in agg_raw_moment, the random_variable side calls compute_expectation through rv_moment.
| input | aggregate expression or random variable to compute E[·] of |
| prov | provenance condition (defaults to gate_one(), i.e., unconditional) |
| method | knowledge compilation method (AGG_TOKEN path only) |
| arguments | additional arguments for the method (AGG_TOKEN path only) |
Internal: shared C entry point for variance / moment / central_moment.
The expected() SQL function reaches the Expectation evaluator through provenance_evaluate_compiled(..., 'expectation', ...). The variance / raw-moment / central-moment SQL functions need an extra k INTEGER argument that does not fit that dispatcher's signature, so they go through this dedicated entry point. Returns E[X^k] when central is FALSE, or E[(X - E[X])^k] when TRUE.
Compute the raw moment E[X^k | prov] of an AGG_TOKEN aggregate
Sister of expected() for the AGG_TOKEN side of the polymorphic moment / variance / central_moment dispatch. Supports the same aggregation functions as expected: SUM (which COUNT normalises to at the gate level via Aggregation.cpp:322), MIN, and MAX.
Strategy:
prov when conditioning), and evaluate the probability via probability_evaluate.v with v^k in the rank-based enumeration that expected already uses; MAX is handled by sign-flipping per the existing trick (negate vs. rerank), with the outer multiplier becoming \((-1)^k\) instead of just \(-1\).Cost: SUM is \(O(n^k)\) probability evaluations – tractable for small k or small n; for larger sizes, prefer reaching for the sampler. MIN / MAX stay linear in n.
Compute the variance Var[X | prov] of a probabilistic scalar
Polymorphic dispatcher that mirrors expected: random_variable inputs go through the analytical / MC evaluator (rv_moment(UUID, 2, true)); AGG_TOKEN inputs go through the agg_raw_moment helper, computing \(\mathrm{Var}[X|A] = E[X^2|A] - E[X|A]^2\). Conditioning on prov is supported for AGG_TOKEN (matching expected) but not yet for random_variable.
Compute the raw moment E[X^k | prov] of a probabilistic scalar
k must be a non-negative INTEGER. k = 0 returns 1; k = 1 is equivalent to expected(input). Polymorphic dispatcher: routes random_variable through rv_moment (analytical / MC) and AGG_TOKEN through agg_raw_moment (SUM via tuple enumeration, MIN / MAX via rank enumeration).
Internal: rv-side support computation
Lifts provsql.compute_support out of RangeCheck.cpp – the same interval-arithmetic propagation runRangeCheck uses to decide gate_cmps. Returns [-Infinity, +Infinity] when the tightest bound is the conservative all-real interval (e.g. for a normal RV, or any sub-circuit that mixes a normal in).
Compute the support interval [lo, hi] of a probabilistic (or deterministic) scalar
Polymorphic dispatcher mirroring expected / variance / moment / central_moment, with two extra "free" branches:
smallint / INTEGER / bigint / NUMERIC / real / double precision): degenerate point support \([c, c]\). Lets callers ask for the support of a literal without round-tripping through as_random.random_variable / bare UUID (any provenance gate token; the random_variable branch reinterprets the value via the binary-coercible random_variable -> UUID cast): routes to rv_support, which propagates distribution supports (uniform exact, exponential gate_arith via interval arithmetic. gate_value gives the same \([c, c]\) point support as the NUMERIC branch; any non-scalar gate (Boolean gates, aggregates, ...) safely falls back to the conservative all-real interval without raising. Conditioning on prov is not yet supported.AGG_TOKEN: closed-form per aggregation function:SUM : \([\sum_i \min(0,v_i), \sum_i \max(0,v_i)]\) (every row is independently in or out of the included set; the extreme SUMs are reached by including only positive or only negative-valued rows).MIN : \([\min_i v_i, \max_i v_i]\) in the non-empty subsets, plus +Infinity if the empty subset has positive probability under prov.MAX : symmetric – -Infinity if empty has positive probability under prov, otherwise min_i v_i; hi is always max_i v_i.Other aggregation functions raise.
Returns the composite RECORD (lo, hi) via the function's OUT parameters, with -Infinity / +Infinity marking unbounded ends.
Compute the central moment E[(X - E[X|prov])^k | prov]
k = 0 returns 1; k = 1 returns 0; k = 2 is equivalent to variance(input, prov, ...). Polymorphic dispatcher: routes random_variable through rv_moment, and AGG_TOKEN through the binomial expansion \(E[(X-\mu)^k|A] = \sum_{i=0}^{k} \binom{k}{i} (-\mu)^{k-i} E[X^i|A]\) with \(\mu = E[X|A]\), where each \(E[X^i|A]\) comes from agg_raw_moment.
Compute the Shapley value of an input variable
Measures the contribution of a specific input variable to the truth of a provenance expression, using game-theoretic Shapley values.
| token | provenance token to evaluate |
| variable | UUID of the input variable |
| method | knowledge compilation method |
| arguments | additional arguments for the method |
| banzhaf | if true, compute the Banzhaf value instead |
Compute Shapley values for all input variables at once
Compute the Banzhaf power index of an input variable
Compute Banzhaf power indices for all input variables at once
Exact reachability probability over bounded-treewidth data (columnar form)
Computes the probability that target is reachable from source in the probabilistic graph given by the parallel edge arrays (two-terminal network reliability). Unlike probability_evaluate(), which compiles the provenance circuit built along the relational query plan, this compiles the query along a tree decomposition of the data graph (in the spirit of the provenance refinement of Courcelle's theorem), producing a d-DNNF whose size is linear in the number of edges for data of bounded treewidth. Exact, and linear-time, on cyclic data as well – where the recursive-query fixpoint cannot terminate structurally.
Edges are independent events. Two array positions may share a token only if they are mutual reverses (the natural encoding of an undirected edge in a directed edge relation); they are then treated as a single bidirectional edge. This is an internal/testing surface: the user-facing route is a plain WITH RECURSIVE reachability query under the 'absorptive' (or 'BOOLEAN') provenance class, which the query rewriter compiles through eval_reachability() / reachability_materialize().
| sources | source vertex of each edge (dense INTEGER IDs) |
| destinations | destination vertex of each edge |
| tokens | provenance token of each edge tuple |
| probabilities | probability of each edge tuple |
| source | the vertex reachability starts from |
| target | the vertex whose reachability is evaluated |
| directed | if false, each edge can be traversed both ways |
Reachability probability plus compilation statistics (columnar form)
Same compilation as reachability_evaluate(), returning the probability together with the structural statistics that substantiate the bounded-treewidth guarantee: the treewidth of the min-fill decomposition of the data graph, its number of bags, the maximum number of dynamic-programming states at any decomposition node, and the size of the emitted d-DNNF (linear in the number of edges for fixed data treewidth).
| sources | source vertex of each edge (dense INTEGER IDs) | |
| destinations | destination vertex of each edge | |
| tokens | provenance token of each edge tuple | |
| probabilities | probability of each edge tuple | |
| source | the vertex reachability starts from | |
| target | the vertex whose reachability is evaluated | |
| directed | if false, each edge can be traversed both ways | |
| [out] | Probability and Shapley values | the reachability probability |
| [out] | data_treewidth | treewidth of the min-fill decomposition of the data graph |
| [out] | nb_bags | number of bags in the decomposition |
| [out] | max_states | maximum number of dynamic-programming states at any decomposition node |
| [out] | nb_gates | number of gates in the emitted d-DNNF |
| [out] | nb_variables | number of variables in the emitted d-DNNF |
Boolean UCQ probability plus compilation statistics (columnar form, internal)
Same compilation as ucq_joint_compile_stats(query jsonb, ...), returning the probability together with the three width columns that substantiate thesis Prop. 4.2.11 empirically – the adversarial family has small data and circuit widths but large joint width – and the structural statistics.
| disjunct_nvars | number of query variables of each disjunct | |
| atom_disjunct | disjunct index of each atom (parallel to atom_rel) | |
| atom_rel | relation id of each atom | |
| atom_vars | query-variable indices of all atom columns, concatenated | |
| atom_arity | number of columns of each atom (slices atom_vars) | |
| fact_rel | relation id of each fact | |
| fact_elems | element ids of all fact columns, concatenated | |
| fact_arity | number of columns of each fact (slices fact_elems) | |
| fact_tokens | provenance token of each fact | |
| fact_probs | probability of each fact | |
| [out] | Probability and Shapley values | the exact UCQ probability |
| [out] | joint_treewidth | width of the min-fill decomposition found |
| [out] | data_treewidth_lb | degeneracy lower bound of the data-only graph |
| [out] | circuit_treewidth_lb | degeneracy lower bound of the slice-only graph |
| [out] | n_bags | number of bags in the decomposition |
| [out] | max_states | peak number of DP states at any node |
| [out] | dd_size | number of gates in the emitted d-D |
| [out] | n_enumerating | maximum number of essential (enumerating) query variables over the disjuncts – the e of the \(2^{O(k^e)}\) bound, with variables functionally determined by others (via FDs mined from the data) removed |
Boolean UCQ probability plus statistics from a JSON specification
JSON-spec wrapper over the columnar ucq_joint_compile_stats() (see ucq_joint_evaluate(query jsonb, ...) for the JSON format).
Correlated Boolean UCQ probability plus compilation statistics (columnar form, internal)
Same compilation as ucq_joint_evaluate_tracked(); the three width columns substantiate thesis Prop. 4.2.11 on real correlated data (the data-only and circuit-only degeneracy bounds can be small while the joint width is large).
Correlated Boolean UCQ probability plus statistics from a JSON spec
Compile a correlated UCQ and materialise its certified d-D, returning the root provenance token (columnar form, internal)
The architecturally-primary route: the compiler builds the deterministic, decomposable circuit and materialises it as ordinary plus / times / monus provenance gates (carrying the d-DNNF certificate); the answer is then obtained through the standard entry points on the returned token – probability_evaluate(token), shapley(token, ...), expectation – so the joint-width path shares the one evaluation pipeline. The token is the exact Boolean provenance of the UCQ (no 'absorptive' marker).
Compile a correlated UCQ and materialise its certified d-D from a JSON spec, returning the root provenance token
JSON-spec wrapper over ucq_joint_materialize_tracked(). Evaluate the answer with the standard surface, e.g. probability_evaluate(ucq_joint_materialize_tracked(query, ...)).
Compile a UCQ over named relations into a materialised certified d-D, gathering the facts from the store – the descriptor-driven engine
The query-surface bridge for the joint-width compiler: instead of hand-built columnar arrays, a JSON descriptor names the relations and how their columns map to query variables, and this function gathers the facts itself (the provenance rewriting is disabled around the gather), builds the value-based element dictionary shared across the relations (so equal join values get the same dense id), compiles and materialises the certified d-D, and returns its provenance token. The answer is then any standard evaluation on that token – probability_evaluate(ucq_joint_provenance(...)), shapley(...), expectation. This is also the engine the planner-time query recogniser drives once it builds the descriptor from a query's abstract syntax.
Descriptor shape:
* { "disjuncts": [ { "n_vars": k,
* "atoms": [ {"rel": <relidx>, "vars": [..]}, ... ] }, ... ],
* "relations": [ "schema.r", "schema.s", ... ], -- relidx -> relation
* "elem_cols": [ ["x"], ["x","y"], ... ] } -- per relation: the
* element columns, in
* the atom's var order
* | descriptor | the UCQ + the relations and their element columns |
| fallback | token returned if the joint-width compiler declines |
Materialise the safe-UCQ Möbius circuit and return its root token. Columnar (TID) interface; see ucq_mobius_provenance for the gather.
Compile the Möbius circuit and return the lattice statistics plus the probability (the demonstrability surface). cancelled_hard is the single number that makes the mechanism legible: for q9 the 1 cancelled element is #P-hard, so the query is easy only because its hard part cancels.
Pass a token through iff it is a gate_mobius, else return NULL.
The Möbius-precedence dispatch (see make_provenance_expression) wraps the Möbius call in this and then COALESCE\ s it before the joint-width call: a Möbius success always roots a gate_mobius (the compiler wraps even a thin selector around the lineage), so it short-circuits and the joint-width compiler never runs; a Möbius decline returns the literal lineage (never a gate_mobius), so this yields NULL and COALESCE falls through to joint-width. The lineage token is a plain plus/times/input, so the test is unambiguous.
Möbius-route provenance from a descriptor (the planner-substituted entry point, and the manual one). Same descriptor and TID gather as ucq_joint_provenance; on any decline (unsafe shape, cap, not TID) returns fallback, so a recognised query never fails.
Möbius lattice statistics + probability from a descriptor: the demonstrability SRF. Gathers the same TID facts as ucq_mobius_provenance, then runs the columnar ucq_mobius_compile_stats.
Internal gather for the per-answer joint route: parse descriptor into the columnar UCQ arrays and gather every fact (relation index, dense element ids, provenance token) with the value dictionary.
Used only by the planner-substituted ucq_joint_provenance_answer (the C single-DP entry point), which calls it ONCE per query and then computes all answers in one sweep. No head pinning: the single DP discovers the answers. val_by_id maps a dense element id back to its TEXT value (so an answer's head ids can be matched to the GROUP BY head TEXT).
Per-answer joint-width provenance via the TOP-DOWN single DP (planner-substituted, C).
The transparent per-answer rewrite substitutes one call per output group. On the FIRST call of a query the function gathers the facts once (ucq_joint_gather), runs the single DP, and materialises EVERY answer's certified d-D into the store, caching head_vals -> token in fn_extra; each subsequent group call is an O(1) lookup – so the whole GROUP BY costs one gather + one decomposition + one sweep, not k of each. On any decline (joint width too large) the fallback token (the normal per-answer provenance) is returned, so the query never fails. The answer's marginal / Shapley / expectation is then the standard evaluation on the returned token – one pipeline for the whole system.
Per-answer safe-UCQ Möbius provenance (planner-substituted): one head-pinned Möbius circuit per output group. On the first call the facts are gathered once (ucq_joint_gather) and cached; each group pins head_vars to head_vals and compiles, caching head -> token. On any decline returns fallback. STABLE: it caches per fn-call context, so it is not re-evaluated within one scan.
Compile and materialise the reachability provenance of every vertex (columnar form, internal)
All-targets variant of reachability_evaluate(): compiles, along a tree decomposition of the data graph, one certified provenance circuit per vertex reachable from some source in the all-edges-present world, materialises the (shared, linear-size) circuits in the provenance store – plus / times gates carrying the d-DNNF certificate, negated edges as monus(one, edge) – and returns one (vertex, token) row per such vertex. Sources form a possibly probabilistic source set: each source arc is gated by the source tuple's token, the nil UUID marking a certain (always present) source. This is the engine behind the rewriter's recursive-reachability route; the returned tokens are ordinary provenance tokens usable with the whole evaluation surface, wrapped in the 'absorptive' assumption marker (the compiled circuit is the exact Boolean lineage but only the absorptive quotient of the infinite recursive semiring provenance: probability and absorptive semiring evaluations – e.g. nonnegative min-plus – are exact, counting and why-provenance refuse).
| sources | source vertex of each edge (dense INTEGER IDs) | |
| destinations | destination vertex of each edge | |
| tokens | provenance token of each edge tuple | |
| probabilities | probability of each edge tuple | |
| block_keys | per-edge BID key variable (nil UUID = independent tuple; alternatives sharing a key are mutually exclusive, e.g. from repair_key) | |
| block_indices | per-edge outcome index within its block | |
| source_vertices | the source vertices | |
| source_tokens | per-source provenance token (nil UUID = certain) | |
| source_probabilities | per-source probability | |
| directed | if false, each edge can be traversed both ways | |
| [out] | vertex | a vertex reachable from some source |
| [out] | token | the materialised reachability provenance token of vertex |
Bounded-hop variant of reachability_materialize() (internal)
Compiles, along a tree decomposition of the data graph, one certified provenance circuit per (vertex, walk length) pair achievable within hop_bound edges – the rows a hop-counting recursive CTE derives, row (v,h) meaning "some *walk* of exactly @c h edges connects a
present source to @c v" – and returns them as (vertex, hops, token) with hop_seed added to the lengths (the CTE base arm's hop constant). Also pre-creates, per vertex, the certified gate that a hop-discarding query's deduplication will address, wired to the compilation's native within-bound root, so the natural "within k
hops" probability evaluates through the linear certified route.
| sources | source vertex of each edge (dense INTEGER IDs) | |
| destinations | destination vertex of each edge | |
| tokens | provenance token of each edge tuple | |
| probabilities | probability of each edge tuple | |
| block_keys | per-edge BID key variable (nil UUID = independent) | |
| block_indices | per-edge outcome index within its block | |
| source_vertices | the source vertices | |
| source_tokens | per-source provenance token (nil UUID = certain) | |
| source_probabilities | per-source probability | |
| directed | if false, each edge can be traversed both ways | |
| hop_bound | maximum walk length | |
| hop_seed | hop value of the base arm (added to reported lengths) | |
| [out] | vertex | a reachable vertex |
| [out] | hops | the walk length at which vertex is reached |
| [out] | token | the materialised provenance token of the |
Per-group "some member reachable" compilation (columnar form, internal)
For each distinct group in the parallel group_ids / member_vertices arrays, compiles the certified circuit of "some
member vertex is reachable from a present source" along the data decomposition – the disjunction over the group's correlated per-vertex reachability events, deterministic by construction through the set-reachability state bit – materialises it, and returns one (group_id, token) row per group. Engine behind the rewriter's cross-vertex aggregation planting.
| sources | source vertex of each edge (dense INTEGER IDs) | |
| destinations | destination vertex of each edge | |
| tokens | provenance token of each edge tuple | |
| probabilities | probability of each edge tuple | |
| block_keys | per-edge BID key variable (nil UUID = independent) | |
| block_indices | per-edge outcome index within its block | |
| source_vertices | the source vertices | |
| source_tokens | per-source provenance token (nil UUID = certain) | |
| source_probabilities | per-source probability | |
| directed | if false, each edge can be traversed both ways | |
| group_ids | group identifier of each member row | |
| member_vertices | member vertex of each member row | |
| [out] | group_id | a group whose every member is reachable |
| [out] | token | the materialised all-members-reachable provenance token of group_id |
Compile and materialise the "every member vertex reachable" (k-terminal / coverage) circuit (columnar form, internal)
Arguments as reachability_materialize_any() with a single member set: compiles the certified circuit of "every member vertex is
reachable from a present source" – the conjunction over the members' correlated per-vertex events, deterministic by construction through the pending rescuer-set congruence – materialises it, and returns its token, wrapped in the 'absorptive' assumption marker. Probability evaluation gives the k-terminal reliability; nonnegative min-plus the cost of the cheapest covering subgraph (directed Steiner cost), shared edges paid once. A member vertex absent from the graph is unreachable: the circuit is then constant false.
| sources | source vertex of each edge (dense INTEGER IDs) |
| destinations | destination vertex of each edge |
| tokens | provenance token of each edge tuple |
| probabilities | probability of each edge tuple |
| block_keys | per-edge BID key variable (nil UUID = independent) |
| block_indices | per-edge outcome index within its block |
| source_vertices | the source vertices |
| source_tokens | per-source provenance token (nil UUID = certain) |
| source_probabilities | per-source probability |
| directed | if false, each edge can be traversed both ways |
| member_vertices | the member vertices (dense IDs) |
Plant certified any-member-reachable gates for a grouped reachability aggregation (internal)
Called (at plan time, over SPI) by the recursive-CTE lowering when the outer query aggregates a reachability working table by a column of a joined, untracked member relation: GROUP BY collapses each group's per-vertex reach tokens with provenance_plus, whose disjuncts are correlated (they share edges) and would otherwise leave the certified route. For each multi-member group this pre-creates, at the canonical address of the group's token multiset, a certified single-child plus over the group's native any-member-reachable circuit (reachability_materialize_any), so the natural aggregation stays on the linear evaluation route. Best-effort: any failure leaves the generic path untouched (notice under verbosity 10).
| work_name | the lowered CTE's working table |
| node_attribute | its vertex column |
| member_rel | the joined member relation (must be untracked) |
| member_attribute | the member relation's join column |
| group_attribute | the member relation's grouping column |
| edge_rel | the tracked edge relation (as for eval_reachability) |
| source_attribute | name of the source-vertex column |
| destination_attribute | name of the destination-vertex column |
| source_value | the base arm's constant, as TEXT |
| directed | if false, each edge can be traversed both ways |
| edge_quals | optional deterministic filter over edge columns |
| source_rel | source relation of a multi-source base arm |
| source_rel_attribute | the source relation's vertex column |
| edge_sql | deparsed edge subquery (join-defined edges) |
| member_quals | optional deterministic filter over the member relation's columns (table-qualified as t.column), restricting which members participate in each group |
Plant the certified all-members-reachable gate for a reachability self-join conjunction (internal)
Called (at plan time, over SPI) by the recursive-CTE lowering when the outer query self-joins a reachability working table with one constant node binding per reference – "are these k vertices all
reachable" – whose row provenance provenance_times() computes as the product of correlated per-vertex reach tokens (they share edges). This pre-creates, at the times-canonical address of that token multiset, a certified single-child times over the native all-members-reachable circuit (reachability_materialize_cover), so the natural conjunction stays on the linear certified route – with the joint-worlds semantics: probability evaluation gives the k-terminal reliability, and nonnegative min-plus the cost of the cheapest covering subgraph (directed Steiner cost), shared edges paid once where the raw product would pay them once per factor. Best-effort: any failure leaves the generic path untouched (notice under verbosity 10).
| work_name | the lowered CTE's working table |
| node_attribute | its vertex column |
| edge_rel | the tracked edge relation (as for eval_reachability) |
| source_attribute | name of the source-vertex column |
| destination_attribute | name of the destination-vertex column |
| source_value | the base arm's constant, as TEXT |
| directed | if false, each edge can be traversed both ways |
| node_values | the constant node bindings, as TEXT (multiset: one per self-join reference) |
| edge_quals | optional deterministic filter over edge columns |
| source_rel | source relation of a multi-source base arm |
| source_rel_attribute | the source relation's vertex column |
| edge_sql | deparsed edge subquery (join-defined edges) |
Input leaves of a conjunction-shaped provenance token (internal)
Descends a token's circuit through the conjunctive gate types (times, and the pass-through project / eq where-provenance wrappers) down to input leaves. Returns the distinct leaves, or NULL when the circuit contains any other gate type (a disjunctive or aggregate shape, which is not a conjunction of independent tuples). Used by the reachability gathering to accept join-defined edges: a derived edge whose token is a pure conjunction of base tuples.
| token | the provenance token |
Gather the edges of a tracked relation in the columnar form expected by reachability_evaluate (internal)
Materializes the edge relation with its provenance tokens and probabilities, maps arbitrary vertex values (compared as TEXT) onto dense INTEGER IDs, and checks that every edge tuple carries a base input token (independent tuples): reachability compilation along the data is only correct when the edges are independent events, so views or query results with derived provenance are rejected.
| rel | the provenance-tracked edge relation |
| source_attribute | name of the source-vertex column |
| destination_attribute | name of the destination-vertex column |
| extra_vertices | vertex values (as TEXT) that must be part of the dense ID space even when they touch no edge – the source set in particular; their IDs come back in extra_ids (aligned with the input) |
| edge_quals | optional deterministic filter over the edge relation's columns (SQL TEXT, deparsed by the rewriter from the recursive arm's WHERE clause), restricting which edges participate |
| rel_sql | deparsed edge subquery to gather from instead of rel (join-defined edges); the tokens are then conjunctions of base tuples, validated for shape and disjoint supports |
The vertices output maps the dense IDs back to the original vertex values (as TEXT, 1-indexed), for callers that need to label per-vertex results.
| [out] | sources | source vertex (dense ID) of each gathered edge |
| [out] | destinations | destination vertex (dense ID) of each edge |
| [out] | tokens | provenance token of each edge tuple |
| [out] | probabilities | probability of each edge tuple |
| [out] | block_keys | per-edge BID key variable (nil UUID = independent) |
| [out] | block_indices | per-edge outcome index within its block |
| [out] | extra_ids | dense IDs assigned to the extra_vertices |
| [out] | vertices | dense-ID-to-original-value map (TEXT, 1-indexed) |
Gather a source relation's vertices, tokens and probabilities (internal)
For a provenance-tracked source relation, every tuple must carry a base input token (a probabilistic source set); for an untracked relation the sources are certain and the tokens come back as the nil UUID. Vertex values are returned as TEXT, for the shared dense-ID mapping of gather_reachability_edges().
| rel | the source relation | |
| source_attribute | name of the vertex column | |
| [out] | source_values | vertex value of each source tuple (as TEXT) |
| [out] | source_tokens | per-source base input token (nil UUID = certain) |
| [out] | source_probabilities | per-source probability |
Fixpoint driver for the recursive reachability shape: decomposition-aligned compilation with fallback to eval_recursive
Called (at plan time, over SPI) by the recursive-CTE lowering when the provenance class is 'absorptive' or 'BOOLEAN' (provsql.provenance) and the CTE matches the linear reachability shape over a tracked base edge relation. Attempts the decomposition-aligned route – gather the edges, compile every reachable vertex's certified provenance circuit along a tree decomposition of the data graph, materialise them, and fill the working table with one tokenised row per reachable vertex. On any failure (data treewidth above the cap, per-node state bound, edges that are not independent base tuples...), falls back to the generic eval_recursive() fixpoint, preserving its behaviour exactly.
| edge_rel | the provenance-tracked edge relation |
| source_attribute | name of the source-vertex column |
| destination_attribute | name of the destination-vertex column |
| source_value | the base arm's constant, as TEXT |
| directed | if false, each edge can be traversed both ways |
| work_name | name of the working temp table (the CTE name) |
| colnames | comma-separated user column names (for the fallback) |
| coldef | column definitions of the working table |
| coltype | type of the CTE's single column |
| body_sql | deparsed CTE body (for the fallback) |
| edge_quals | optional deterministic filter over edge columns (deparsed from the recursive arm's WHERE clause) |
| source_rel | source relation of a multi-source base arm (SELECT col FROM sources), NULL for the constant form; tracked sources form a probabilistic source set, untracked ones are certain |
| source_rel_attribute | the source relation's vertex column |
| edge_sql | deparsed edge subquery when the recursive arm joins a derived (join-defined) edge relation instead of a base one; NULL for the REGCLASS form |
| hop_bound | maximum number of recursive steps for the hop-counting CTE shape (NULL for plain reachability) |
| hop_seed | the base arm's hop constant (hop-counting shape) |
| hops_position | 1-based position of the hop column among the CTE's two columns (hop-counting shape) |
Functions for visualizing and exporting provenance circuits in various formats.
| TEXT update_provenance::compile_to_ddnnf | ( | UUID | token, |
| TEXT | compiler = '' ) |
Return the compiled d-DNNF of a provenance circuit in the c2d / d4 ".nnf" TEXT interchange format.
Companion to compile_to_ddnnf_dot (DOT, for viewing): this is the machine-readable form, suitable for feeding to an external d-DNNF reasoner / verifier or saving next to tseytin_cnf (same variable numbering). Accepts the same compiler / meta-route names.
| token | root provenance token |
| compiler | compiler or in-process meta-route to use; empty (the default) picks the highest-preference available compiler |
| TEXT update_provenance::compile_to_ddnnf_dot | ( | UUID | token, |
| TEXT | compiler = '' ) |
Return a DOT visualisation of the d-DNNF compiled from the provenance circuit.
Runs the requested external knowledge compiler and renders the resulting d-DNNF as a GraphViz digraph.
| token | root provenance token |
| compiler | external compiler or in-process meta-route to invoke; empty (the default) picks the highest-preference available compiler |
| jsonb update_provenance::ddnnf_stats | ( | UUID | token, |
| TEXT | compiler = '' ) |
Structural statistics of the d-DNNF a compiler produces for a provenance circuit.
Compiles the circuit with the given compiler / meta-route (same names as compile_to_ddnnf_dot: d4, d4v2, c2d, minic2d, dsharp, panini-*, tree-decomposition, interpret-as-dd, default) and returns a jsonb object: nodes, edges, and / or / not / inputs counts, smooth, depth (longest path), treewidth (null when not computable), and compile_ms. Lets clients compare what each compiler produces on the same circuit.
| token | root provenance token |
| compiler | compiler or in-process meta-route to use; empty (the default) picks the highest-preference available compiler |
| UUID update_provenance::provenance | ( | ) |
Return the provenance token of the current query result tuple.
| REVOKE ALL ON FUNCTION register_tool | ( | TEXT | name, |
| TEXT | executable = NULL, | ||
| TEXT | kind = 'cli', | ||
| TEXT[] | operations = NULL, | ||
| TEXT[] | input_formats = NULL, | ||
| TEXT | output_format = NULL, | ||
| TEXT | parser = NULL, | ||
| TEXT | argtpl = NULL, | ||
| TEXT | argtpl_circuit = NULL, | ||
| INT | preference = 0, | ||
| BOOLEAN | enabled = true, | ||
| TEXT | endpoint = NULL ) |
Register a tool, or replace the RECORD with the same logical name.
The mutators guard at the C level too, but revoke from PUBLIC so the superuser requirement is visible in the catalog.
| name | logical id (e.g. 'd4-jm62300'); also the value provsql.fallback_compiler / the wmc tool selector use |
| executable | executable to resolve on PATH (defaults to name) |
| kind | 'cli' (spawn executable) or 'kcmcp' (talk to the KCMCP server at endpoint) |
| operations | capabilities (KCMCP names): 'compile' / 'wmc' (and ProvSQL-local 'render') |
| input_formats | accepted inputs (KCMCP names): 'dimacs-cnf', 'circuit-bcs12' (listing 'circuit-bcs12' enables the native-circuit fast path) |
| output_format | result encoding (KCMCP names): 'ddnnf-nnf', 'decimal', 'rational', ... (local 'panini-dd' / 'ascii' where KCMCP has no code) |
| parser | CLI-only decode tag: 'nnf' (the tolerant d4 / c2d NNF reader), 'panini-dd', 'wmc-line', 'weightmc', 'ascii' |
| argtpl | command template; placeholders {in} / {out} (and {binary} / {tmpdir} / {pivotAC}). When it omits {binary}, the executable is prepended. |
| argtpl_circuit | command used when the 'circuit-bcs12' input is selected (a BC-S1.2 circuit rather than a CNF); only a tool accepting that input needs it |
| preference | ordering within an operation (higher first) |
| enabled | whether the dispatchers may select it |
| endpoint | for a 'kcmcp' RECORD, the server address: 'unix:/path' or 'host:port' |
Superuser-only: a CLI RECORD runs an arbitrary command as the PostgreSQL OS user, and a kcmcp RECORD names a socket the server connects to.
| REVOKE ALL ON FUNCTION set_tool_enabled | ( | TEXT | name, |
| BOOLEAN | enabled ) |
Enable/disable a tool; errors on an unknown tool name.
Superuser-only.
| REVOKE ALL ON FUNCTION set_tool_preference | ( | TEXT | name, |
| INT | preference ) |
Set a tool's preference; errors on an unknown tool name.
Superuser-only.
| TEXT update_provenance::to_provxml | ( | UUID | token, |
| REGCLASS | token2desc = NULL ) |
Return an XML representation of the provenance circuit.
| token | root provenance token |
| token2desc | optional mapping table for gate descriptions |
| BOOLEAN update_provenance::tool_available | ( | TEXT | name | ) |
Report whether an external tool is on the backend's resolved PATH.
Uses the same find_external_tool() helper that the compilers (d4 / c2d / minic2d / dsharp / panini), model counters (ganak / sharpsat-td / dpmc via htb+dmc / weightmc), and visualisation wrappers (graph-easy, dot) themselves consult, so the result reflects exactly what a subsequent probability_evaluate or view_circuit call would see, including the provsql.tool_search_path GUC prepended to $PATH.
Names with a slash are treated as paths and tested directly via access(X_OK); bare names are resolved through /bin/sh's command -v under the backend's PATH.
| name | bare executable (e.g. 'd4') or an absolute path |
| CREATE TABLE IF NOT EXISTS update_provenance::tool_overrides | ( | name TEXT PRIMARY | KEY, |
| removed BOOLEAN NOT NULL DEFAULT | false, | ||
| kind | TEXT, | ||
| executable | TEXT, | ||
| operations | TEXT[], | ||
| input_formats | TEXT[], | ||
| output_format | TEXT, | ||
| parser | TEXT, | ||
| preference | INT, | ||
| enabled | BOOLEAN, | ||
| dependencies | TEXT[], | ||
| argtpl | TEXT, | ||
| argtpl_circuit | TEXT, | ||
| endpoint | TEXT ) |
Persistent overrides overlaid on the compiled-in tool seed.
Each row is the complete desired RECORD for a tool (added or modified) keyed by logical name, or a tombstone (removed = true) hiding a seeded default. The effective registry is the compiled seed with tombstoned names removed and the remaining rows upserted over it. Written only by the superuser-only register_tool / unregister_tool / set_tool_* functions; read back into each backend's in-memory registry on demand. Marked as a configuration table so pg_dump carries an operator's registrations.
| CREATE OR REPLACE VIEW tools AS SELECT available FROM tool_registry_list | ( | ) |
Set-returning listing backing the provsql.tools view.
operations / input_formats / output_format use the KCMCP shared-registry names (see the KCMCP server protocol), so a CLI RECORD and a future kcmcp-server RECORD are comparable; parser is the CLI-only tag for how to decode the tool's raw output. argtpl is the command template ({in}/{out}/... placeholders). available is true iff executable (when set) and every dependency currently resolve on the backend's PATH.
| TEXT update_provenance::tree_decomposition_dot | ( | UUID | token | ) |
Return a DOT visualisation of the tree decomposition of the provenance circuit.
Computes the min-fill decomposition used by the in-process knowledge compiler. The first line of the output is a comment of the form "// treewidth=<n>".
| token | root provenance token |
| TEXT update_provenance::tseytin_cnf | ( | UUID | token, |
| BOOLEAN | weighted = TRUE, | ||
| BOOLEAN | mapping = TRUE ) |
Return the DIMACS CNF (Tseytin transformation) of the provenance circuit.
Returns the same encoding the extension writes to a temp file before invoking d4 / c2d / minic2d / dsharp. With weighted true (the default), per-input probability weights are appended as w lines.
| token | root provenance token |
| weighted | include probability weights when true |
| mapping | prepend "c input <var> <UUID> <prob>" comment lines documenting which provenance input each variable stands for |
| TABLE update_provenance::tseytin_cnf_mapping | ( | UUID | token | ) |
| jsonb update_provenance::tseytin_cnf_mapping_json | ( | UUID | token | ) |
Map each DIMACS variable of tseytin_cnf back to its provenance input.
Returns one row per input gate: the variable index (matching tseytin_cnf and compile_to_ddnnf's NNF), the original-circuit UUID of that input, and its probability. Lets a satisfying assignment or weighted model count obtained from an external tool be read against the provenance circuit.
| token | root provenance token |
| REVOKE ALL ON FUNCTION unregister_tool | ( | TEXT | name | ) |
| TEXT update_provenance::view_circuit | ( | UUID | token, |
| REGCLASS | token2desc, | ||
| INT | dbg = 0 ) |
Return a DOT or TEXT visualization of the provenance circuit.
| token | root provenance token |
| token2desc | mapping table for gate descriptions |
| dbg | debug level (0 = normal) |
| TEXT update_provenance::where_provenance | ( | UUID | token | ) |
Compute where-provenance for a result tuple.
Returns a TEXT representation showing which input columns contributed to each output column.
| CREATE OR REPLACE VIEW tools AS SELECT argtpl |
| CREATE OR REPLACE VIEW tools AS SELECT argtpl_circuit |
| CREATE OR REPLACE VIEW tools AS SELECT enabled |
| CREATE OR REPLACE VIEW tools AS SELECT endpoint |
| CREATE OR REPLACE VIEW tools AS SELECT executable |
| CREATE OR REPLACE VIEW tools AS SELECT input_formats |
| CREATE OR REPLACE VIEW tools AS SELECT kind |
| CREATE OR REPLACE VIEW tools AS SELECT name |
Read-only view of the registered tools.
| CREATE OR REPLACE VIEW tools AS SELECT operations |
| CREATE OR REPLACE VIEW tools AS SELECT output_format |
| CREATE OR REPLACE VIEW tools AS SELECT parser |
| CREATE OR REPLACE VIEW tools AS SELECT preference |