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 "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)
	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 )

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.

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.

Parameters

child

UUID of the materialised root to wrap.

Returns

UUID of the gate_assumed wrapper.

Definition at line 260 of file CertifiedDDMaterialize.cpp.

Here is the call graph for this function:

Here is the caller graph for this function: