CertifiedDDMaterialize.cpp File Reference

Implementation of certified-d-D materialisation into the store. More...

#include "postgres.h"
#include "miscadmin.h"
#include "utils/uuid.h"
#include "provsql_utils.h"
#include "provsql_mmap.h"
#include "CertifiedDDMaterialize.h"
#include "BooleanCircuit.h"
#include "provsql_utils_cpp.h"
#include <algorithm>
#include <cstdint>
#include <string>
#include <unordered_set>
#include <vector>

Include dependency graph for CertifiedDDMaterialize.cpp:

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

Implementation of certified-d-D materialisation into the store.

See CertifiedDDMaterialize.h. Extracted from the reachability compiler's SQL glue so the joint-width UCQ compiler shares the same content-addressed materialisation (and so probability / Shapley / expectation all go through the standard probability_evaluate path on the materialised token).

Definition in file CertifiedDDMaterialize.cpp.

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: