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

Implementation of the joint-width UCQ compiler's homomorphism DP (data-graph regime). More...

#include "UCQJointCompiler.h"
#include <algorithm>
#include <cstdint>
#include <functional>
#include <map>
#include <memory>
#include <set>
#include <tuple>
#include <unordered_map>
#include <vector>
#include "postgres.h"
#include "miscadmin.h"
Include dependency graph for UCQJointCompiler.cpp:

Go to the source code of this file.

Functions

static UCQJointCompiler::Result compileImpl (const JointEncoding &enc, const UCQ &ucq, unsigned max_treewidth, std::size_t max_states, const TreeDecomposition *shared_td, const std::unordered_map< unsigned long, bag_t > *shared_elim, const std::map< unsigned, unsigned long > *head_pin)
 Data-graph (TID/BID) compile, with optional decomposition reuse and an optional in-DP head pin.

Detailed Description

Implementation of the joint-width UCQ compiler's homomorphism DP (data-graph regime).

See UCQJointCompiler.h for the construction's design and the structural argument (determinism and decomposability by construction). This translation unit implements the ยง3.5 fast path: every fact gated by an independent Bernoulli event, a single bottom-up sweep over a min-fill tree decomposition of the joint (here, Gaifman) graph of the facts, the Boolean UCQ read off the root table. The correlated regime (in-bag gate valuations, MULVAR blocks) is not handled by this fast path.

The homomorphism-type state

For each disjunct, the state holds the set of partial-homomorphism codes realised by the present facts of the processed subtree. A code assigns each query variable one of: UNASSIGNED (its image is not yet decided – it will be pinned higher in the tree), a position in the current bag (its image is an in-bag element), or DONE (its image is an already-forgotten element, and every atom incident to it has been witnessed). Alongside, a bitmask records which atoms are witnessed by a present fact under this assignment. Because witnessing under a fixed assignment is deterministic, the set of achievable codes is a function of the world; states therefore partition worlds and the emitted ORs are deterministic. When a disjunct's witnessed mask becomes full the whole state collapses to the absorbing sat marker – the main state-pruning lever, the UCQ analogue of the reachability compiler's final collapse.

Definition in file UCQJointCompiler.cpp.

Function Documentation

◆ compileImpl()

UCQJointCompiler::Result compileImpl ( const JointEncoding & enc,
const UCQ & ucq,
unsigned max_treewidth,
std::size_t max_states,
const TreeDecomposition * shared_td,
const std::unordered_map< unsigned long, bag_t > * shared_elim,
const std::map< unsigned, unsigned long > * head_pin )
static

Data-graph (TID/BID) compile, with optional decomposition reuse and an optional in-DP head pin.

With shared_td == nullptr and head_pin == nullptr this is the Boolean data-graph compiler verbatim (the path the test suite exercises), which is how compile() always calls it. The shared-decomposition / per-answer head-pin parameters remain for a head-pinned per-answer sweep (no current caller; the live per-answer path is compileAnswersOneDP).

Definition at line 1845 of file UCQJointCompiler.cpp.

Here is the call graph for this function:
Here is the caller graph for this function: