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, provsql_route route)
	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,
		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: