 |
ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
|
ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
Möbius-inversion exact route for safe UCQs (the last missing exact route of the Dalvi-Suciu dichotomy). More...
#include "postgres.h"#include "fmgr.h"#include "funcapi.h"#include "miscadmin.h"#include "access/htup_details.h"#include "access/xact.h"#include "catalog/pg_type.h"#include "executor/spi.h"#include "utils/array.h"#include "utils/builtins.h"#include "utils/resowner.h"#include "utils/uuid.h"#include "compatibility.h"#include "provsql_utils.h"#include "provsql_mmap.h"#include "c_cpp_compatibility.h"#include "CertifiedDDMaterialize.h"#include "mobius_evaluate.h"#include "provsql_utils_cpp.h"#include <algorithm>#include <cmath>#include <cstdint>#include <functional>#include <map>#include <set>#include <stdexcept>#include <string>#include <unordered_map>#include <unordered_set>#include <vector>
Go to the source code of this file.
Functions | |
| Datum | get_gate_type (PG_FUNCTION_ARGS) |
| PostgreSQL-callable wrapper for get_gate_type(). | |
| Datum | ucq_mobius_materialize_tracked (PG_FUNCTION_ARGS) |
| Materialise the safe-UCQ Möbius circuit and return its root token. | |
| Datum | ucq_mobius_compile_stats (PG_FUNCTION_ARGS) |
| Compile the Möbius circuit and return the lattice statistics plus the probability (the demonstrability surface). | |
| Datum | ucq_mobius_provenance_answer (PG_FUNCTION_ARGS) |
| Per-answer Möbius provenance (the planner-substituted entry point for a non-Boolean UCQ with free head variables). | |
Variables | |
| int | provsql_mobius_max_gates |
Data-cost cap of the Möbius route: it declines (falling through to joint-width / the ladder) once its compile has built more than this many gates, bounding the \(O(|D|^k)\) blow-up of a high-level safe query on large data; provsql.mobius_max_gates GUC. | |
Möbius-inversion exact route for safe UCQs (the last missing exact route of the Dalvi-Suciu dichotomy).
Some unions of conjunctive queries are safe (PTIME data complexity) only because the #P-hard terms of their inclusion-exclusion expansion carry a zero Möbius value on the CNF lattice and cancel. The canonical witness is QW / q9 (Dalvi-Suciu 2012; Monet & Olteanu 2018). No other ProvSQL route handles it in PTIME: the safe-query rewriter is per-CQ and hierarchical, the query is not inversion-free (that is the point), and on adversarial data the joint treewidth is unbounded.
This file packages the extensional lattice-walking algorithm (Dalvi, Schnaitter & Suciu, "Computing query probability with incidence algebras", PODS 2010) the way the joint-width route already is: a compile-at-execution step producing a certified circuit over the gathered data, and a linear evaluation – the only genuinely new evaluation primitive being a signed linear combination at gate_mobius nodes (see provsql_utils.h and the gate_mobius handling in probability_evaluate.cpp).
The probability of a UCQ Q given in CNF as \(\bigwedge_i d_i\) is, by inclusion-exclusion on the \(\lnot d_i\),
\[ P(Q) = \sum_{\emptyset\neq s\subseteq[M]} (-1)^{|s|+1} P\Big(\bigvee_{i\in s} d_i\Big), \]
and grouping the \(\bigvee_{i\in s} d_i\) up to logical equivalence collapses the hard term (its coefficient sums to zero – the whole game). Each surviving \(\bigvee_{i\in s} d_i\) is a safe disjunctive sentence, compiled recursively by the standard IndepStep / MobiusStep lifted-inference recursion (component split, disjoint-symbol product, separator independent-project, inner Möbius step) into certified-independent Boolean islands, combined at the root gate_mobius by the signed coefficients.
Restrictions: reduced-form UCQs (no relation repeated within a disjunct, no repeated variable inside an atom, no constants), tuple-independent (TID) inputs. Anything outside that declines (a C++ exception caught at the SQL boundary), so the query falls back to the normal provenance and never fails.
Definition in file mobius_evaluate.cpp.
|
extern |
PostgreSQL-callable wrapper for get_gate_type().
On cache miss this fetches BOTH the gate type and its children from the worker, in one critical section, then caches them together. If we cached only the type (with an empty children list), a subsequent get_children() call for the same token would consult the cache, find the entry, and return 0 children : never querying the worker for the real children. provsql.provenance_evaluate hits exactly that pattern (it calls get_gate_type first, then unnest(get_children(...))) and silently folds plus/times gates over an empty set.
Definition at line 141 of file provsql_mmap.c.
| Datum ucq_mobius_compile_stats | ( | PG_FUNCTION_ARGS | ) |
Compile the Möbius circuit and return the lattice statistics plus the probability (the demonstrability surface).
Same columnar arguments as ucq_mobius_materialize_tracked.
Definition at line 1118 of file mobius_evaluate.cpp.
| Datum ucq_mobius_materialize_tracked | ( | PG_FUNCTION_ARGS | ) |
Materialise the safe-UCQ Möbius circuit and return its root token.
Columnar arguments (mirrors ucq_joint_materialize_tracked, TID inputs): 0..4 disjunct_nvars, atom_disjunct, atom_rel, atom_vars, atom_arity 5..8 fact_rel, fact_elems, fact_arity, fact_tokens 9 lineage (uuid, optional): the literal Boolean provenance of the query, carried on the root gate_mobius so the token still answers Shapley / semiring / PROV on the normal lineage (the Möbius combination is a probability-only shortcut layered over it).
The root is a gate_mobius carrying the certified-independent Boolean islands (the signed combination) and the lineage child; probability_evaluate answers the #P-hard UCQ in PTIME through the fast Möbius route, and every other evaluator passes through to the lineage. Declines raise an error so the SQL wrapper falls back.
Definition at line 1089 of file mobius_evaluate.cpp.
| Datum ucq_mobius_provenance_answer | ( | PG_FUNCTION_ARGS | ) |
Per-answer Möbius provenance (the planner-substituted entry point for a non-Boolean UCQ with free head variables).
Arguments: (descriptor jsonb, head_vars int[], head_vals text[], fallback uuid). Called once per output group; on the first call the facts are gathered once and the value dictionary cached, then each group pins its head variables (the canonical head indices head_vars, in every disjunct) to their values (head_vals, matched through the gather's text dictionary) and compiles the head-pinned Möbius circuit, caching head-key -> token. On any decline (unsafe shape, head value absent, ...) returns fallback.
Definition at line 1164 of file mobius_evaluate.cpp.
|
extern |