CertifiedDDMaterialize.h File Reference

Content-addressed materialisation of a certified d-D into the mmap provenance store. More...

#include "postgres.h"
#include "utils/uuid.h"
#include "provsql_utils.h"
#include "dDNNF.h"
#include <unordered_map>
#include <vector>

Include dependency graph for CertifiedDDMaterialize.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
pg_uuid_t	provsqlUuidV5 (const std::string &name)
	RFC 4122 version-5 UUID in the ProvSQL namespace.
std::unordered_map< gate_t, pg_uuid_t, hash_gate_t >	materializeCertifiedDD (const dDNNF &dd, const std::vector< gate_t > &roots, provsql_route route=PROVSQL_ROUTE_NONE)
	Materialise (the reachable part of) a certified d-D into the mmap store.
pg_uuid_t	wrapAssumedAbsorptive (const pg_uuid_t &child)
	Wrap a materialised root in the 'absorptive' assumption marker and return the wrapper's UUID.

Detailed Description

Content-addressed materialisation of a certified d-D into the mmap provenance store.

A decomposition-aligned compiler (the reachability compiler, the joint-width UCQ compiler) builds a circuit that is deterministic and decomposable by construction – a certified d-D. Rather than reading the probability off that circuit in C++, the certified d-D can be materialised as ordinary provenance gates (plus / times / monus, carrying the DNNF_CERT_INFO mark), so that the answer – probability, Shapley, expectation, any provenance-store evaluation – is obtained through the single standard entry point probability_evaluate() (etc.) on the materialised token. This keeps one evaluation path for the whole system and exploits the certificate (linear-time independentEvaluation / interpretAsDD).

Gate UUIDs are content-addressed with the standard v5 recipes, so identical sub-circuits dedup in the store and re-materialising the same circuit is a no-op.

Definition in file CertifiedDDMaterialize.h.

Function Documentation

materializeCertifiedDD()

std::unordered_map< gate_t, pg_uuid_t, hash_gate_t > materializeCertifiedDD	(	const dDNNF &	dd,
		const std::vector< gate_t > &	roots,
		provsql_route	route = PROVSQL_ROUTE_NONE )

Materialise (the reachable part of) a certified d-D into the mmap store.

Bottom-up over the gates reachable from roots: input gates keep their existing tokens (the leaf provenance, not touched), NOT x is stored as monus(one, x), AND as times, OR as plus. Gates carrying the d-D certificate get it persisted.

Parameters

dd	The certified circuit.
roots	Gates whose closure to materialise.
route	Producing route, stamped in info2 of each materialised root (its info1 being the d-D certificate); read back by the probability dispatcher to name the evaluation method. PROVSQL_ROUTE_NONE leaves the roots untagged. A route that wraps its roots (see wrapAssumedAbsorptive) tags the wrapper instead and passes PROVSQL_ROUTE_NONE here.

Returns

Map from dd gates to their store UUIDs.

Definition at line 115 of file CertifiedDDMaterialize.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

provsqlUuidV5()

pg_uuid_t provsqlUuidV5

(

const std::string &

name

)

RFC 4122 version-5 UUID in the ProvSQL namespace.

Same value as the SQL uuid_generate_v5(uuid_ns_provsql(), name), so gates content-address identically to those the query rewriter mints.

Parameters

name	Name within the namespace.

Returns

The version-5 UUID.

Definition at line 96 of file CertifiedDDMaterialize.cpp.

Here is the caller graph for this function:

wrapAssumedAbsorptive()

pg_uuid_t wrapAssumedAbsorptive

(

const pg_uuid_t &

child

)

Wrap a materialised root in the 'absorptive' assumption marker and return the wrapper's UUID.

Used by the reachability route, whose compiled circuit is the absorptive quotient of a genuinely infinite recursive provenance. The joint-width UCQ compiler does NOT use this: its d-D is the exact Boolean provenance of the (non-recursive) UCQ, sound for every absorptive-or-not probability evaluation.

The wrapper carries PROVSQL_ROUTE_REACHABILITY in info1: the assumption kind alone does not identify the route (the truncated-fixpoint path in sql/provsql.common.sql also mints 'absorptive' wrappers), and the probability dispatcher reads the tag back to report reachability rather than the generic independent.

Parameters

child

UUID of the materialised root to wrap.

Returns

UUID of the gate_assumed wrapper.

Definition at line 279 of file CertifiedDDMaterialize.cpp.

Here is the call graph for this function:

Here is the caller graph for this function: