SQL function provsql.probability_evaluate() – probabilistic circuit evaluation. More...

#include "postgres.h"
#include "fmgr.h"
#include "catalog/pg_type.h"
#include "miscadmin.h"
#include "storage/latch.h"
#include "utils/uuid.h"
#include "executor/spi.h"
#include "funcapi.h"
#include "access/htup_details.h"
#include "provsql_shmem.h"
#include "provsql_utils.h"
#include "utils/guc.h"
#include "c_cpp_compatibility.h"
#include <set>
#include <stack>
#include <map>
#include <unordered_map>
#include <limits>
#include <chrono>
#include <vector>
#include <algorithm>
#include <cmath>
#include <csignal>
#include <string>
#include <sstream>
#include <cctype>
#include "BooleanCircuit.h"
#include "CircuitFromMMap.h"
#include "GenericCircuit.h"
#include "AnalyticEvaluator.h"
#include "CountCmpEvaluator.h"
#include "MinMaxCmpEvaluator.h"
#include "SumCmpEvaluator.h"
#include "AggMarginalEvaluator.h"
#include "HybridEvaluator.h"
#include "RangeCheck.h"
#include "MonteCarloSampler.h"
#include "dDNNFTreeDecompositionBuilder.h"
#include "TreeDecomposition.h"
#include "StructuredDNNF.h"
#include "DTree.h"
#include "ProbabilityMethod.h"
#include "ComparatorResolution.h"
#include "having_semantics.hpp"
#include "provsql_mmap.h"
#include "safe_query_cert.h"
#include "provsql_utils_cpp.h"
#include "tool_registry_sync.h"
#include "semiring/BoolExpr.h"
#include "semiring/Semiring.h"
#include "mobius_evaluate.h"

Include dependency graph for probability_evaluate.cpp:

Go to the source code of this file.

Classes
struct	provsql::EvalContext
	Per-evaluation circuit state threaded to a method's evaluate(). More...

Namespaces
namespace	provsql

Functions
double	mobius_probability_of (pg_uuid_t token)
	External entry point for the Möbius-route probability sweep (declared in mobius_evaluate.h, used by the stats SRF in mobius_evaluate.cpp).
static void	provsql_sigint_handler (int)
	SIGINT handler that sets the global interrupted flag.
static bool	collect_inversion_free_keys (const GenericCircuit &gc, gate_t gc_root, const std::unordered_map< gate_t, gate_t > &gc_to_bc, const BooleanCircuit &c, gate_t bc_root, std::map< gate_t, StructuredDNNFBuilder::InputKey > &out)
	Collect the inversion-free per-input order keys for the structured builder.
static std::map< gate_t, int >	inversion_free_rank (const std::map< gate_t, StructuredDNNFBuilder::InputKey > &keys)
	Flatten the per-input order keys into a total rank for the structured builder's order-only constructor.
dDNNF	buildInversionFreeDDNNF (pg_uuid_t token)
	Compile a query certified inversion-free to its structured d-DNNF.
static void	run_stopping_rule (GenericCircuit &gc, gate_t gc_root, const MethodArgs &a, double &result, std::string &actual_method)
	Whole-circuit (eps,delta)-relative estimate via the stopping rule (shared by the explicit 'stopping-rule' method and the 'relative' path's estimator).
static double	provsql::pow2_clamped (size_t k)
	2^k with the exponent clamped to keep the cost finite (a clamped exponent still sorts the method dead last – it is then a guaranteed fall-through).
dDNNF	provsql::makeDDAuto (BooleanCircuit &c, gate_t g)
	Cost-select a d-DNNF construction route for gate `g` of Boolean circuit `c` and build it – the default makeDD route.
static bool	provsql::toleranceAdmits (ToleranceKind request, ToleranceKind method)
	Admissibility of a method's guarantee under a requested tolerance.
double	provsql::booleanSubcircuitProbability (GenericCircuit &gc, gate_t root, const std::string &method="", const std::string &args="", bool inv_free_cert=false, const Tolerance &tol=Tolerance{}, bool mc_fallback=true, std::string *actual_method_out=nullptr)
	Probability of the Boolean function rooted at `root` in `gc` – THE single entry point over the method portfolio.
static void	record_last_eval_method (const std::string &actual_method)
	Record the method just used in the `provsql.last_eval_method` GUC (comma-separated, deduplicated across calls in the session) so callers can inspect which evaluation strategy the default auto-selection settled on.
static unsigned	maxAggContributions (const GenericCircuit &gc, gate_t root)
	The most contributions an aggregation gate below `root` has, 0 when neither a comparison nor an aggregation is there.
static Datum	probability_evaluate_internal (pg_uuid_t token, const string &method, const string &args, bool *isnull)
Datum	probability_evaluate (PG_FUNCTION_ARGS)
	PostgreSQL-callable wrapper for probability_evaluate().
Datum	probability_bounds (PG_FUNCTION_ARGS)
	PostgreSQL-callable wrapper for the d-tree leaf bound: `probability_bounds(token uuid, OUT lower float8, OUT upper float8)`.

Variables
static const size_t	provsql::kPossibleWorldsSanityMax = 30
	Sanity bound on the reachable-input count for the auto-chosen 2^N possible-worlds enumeration: above it the method drops out of the portfolio so it is never attempted (its 2^N cost already deprioritises it, but this guards against a catastrophic last-resort attempt if every cheaper method failed).
static const size_t	provsql::kSieveSanityMaxClauses = 24
	Largest clause count for which the auto-chosen sieve (2^m inclusion-exclusion) is admitted (matches BooleanCircuit::sieve's internal cap).
static const double	provsql::kCostIndependent = 5e-5
static const double	provsql::kCostInversionFree = 5e-5
static const double	provsql::kCostPossibleWorlds = 3e-6
static const double	provsql::kCostSieve = 1e-5
static const double	provsql::kCostTreeDecomp = 7e-4
static const double	provsql::kCostCompilation = 2e-3
static const double	provsql::kCostCompilationFloor = 40.0
static const double	provsql::kCostDnfShapeFeature = 2e-6
static const double	provsql::kCostTwProxyFeature = 3e-4
static const double	provsql::kCostMonteCarlo = 1e-5
static const double	provsql::kCostStoppingRule = 1e-3
static const double	provsql::kCostKarpLuby = 3e-6
static const double	provsql::kCostDTreeExact = 3e-4
static const double	provsql::kCostDTreeApprox = 4e-4
static const double	provsql::kCostDTreeMsPerStepDnf = 1.4e-3
static const double	provsql::kCostDTreeMsPerStepGeneral = 5e-4
static const char *const	kPossibleWorldsAgg = "possible-worlds-aggregates"
	Core implementation of probability evaluation for a circuit token.
static const unsigned	kPossibleWorldsAggMaxInputs = 20
	Most inputs it enumerates the 2^n worlds of.

Detailed Description

SQL function provsql.probability_evaluate() – probabilistic circuit evaluation.

Implements provsql.probability_evaluate(), which computes the probability that a provenance circuit evaluates to true under the tuple-independent probabilistic-database model.

The method argument selects the computation algorithm:

"possible-worlds": exact enumeration of all 2^n worlds.
"monte-carlo": approximate via random sampling (fast, inexact).
"weightmc": approximate using the weightmc model counter.
"tree-decomposition": exact via tree-decomposition-based d-DNNF.
"independent": exact evaluation for disconnected circuits.
"inversion-free": exact via the structured-d-DNNF builder over the query-derived order; errors unless the root carries an inversion-free certificate. The default method also tries it (after "independent") when a certificate is present.
Any external compiler name ("d4", "c2d", "minic2d", "dsharp").

A SIGINT signal sets a process-local flag that causes the evaluation to abort and return NULL (used when the user cancels a long-running probability computation).

Definition in file probability_evaluate.cpp.

Function Documentation

◆ buildInversionFreeDDNNF()

dDNNF buildInversionFreeDDNNF ( pg_uuid_t token )

Compile a query certified inversion-free to its structured d-DNNF.

Builds the same structured d-DNNF the 'inversion-free' probability method uses (over the query-derived Prop. 4.5 order carried on the circuit's annotation markers), for the knowledge-compilation surface (DOT / NNF / stats). Throws CircuitException if token's root carries no inversion-free certificate. Defined in probability_evaluate.cpp.

Definition at line 757 of file probability_evaluate.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ collect_inversion_free_keys()

bool collect_inversion_free_keys	(	const GenericCircuit &	gc,
		gate_t	gc_root,
		const std::unordered_map< gate_t, gate_t > &	gc_to_bc,
		const BooleanCircuit &	c,
		gate_t	bc_root,
		std::map< gate_t, StructuredDNNFBuilder::InputKey > &	out )

static

Collect the inversion-free per-input order keys for the structured builder.

Walks the GenericCircuit gc for K-prefixed annotation gates whose child is a gate_input (the per-input order markers attached by the planner on the certified path), parses each key, and maps the wrapped input to its BooleanCircuit variable via gc_to_bc. Returns true only if every BooleanCircuit input reachable from bc_root carries a key (the structured builder needs a total order over all variables); a missing marker means the certified markers are absent / incomplete and the caller must not use the structured path.

Definition at line 676 of file probability_evaluate.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ inversion_free_rank()

std::map< gate_t, int > inversion_free_rank ( const std::map< gate_t, StructuredDNNFBuilder::InputKey > & keys )

static

Flatten the per-input order keys into a total rank for the structured builder's order-only constructor.

Sorts the certified inputs into a Prop. 4.5-consistent order – root-class value first (one independent block per value), then secondary-class value (one tile per value within a block), then the shared self-join guard before the payloads of its tile, then by factor – and assigns consecutive ranks. Ties (two inputs with identical keys) keep a deterministic order via the input gate id, so distinct variables always get distinct ranks. Unlike the keyed (factored-sweep) constructor this makes no single-secondary-axis / one-payload-per-tile assumption, so it certifies every hierarchical inversion-free lineage, including the self-join-free case.

Definition at line 736 of file probability_evaluate.cpp.

Here is the caller graph for this function:

◆ maxAggContributions()

unsigned maxAggContributions	(	const GenericCircuit &	gc,
		gate_t	root )

static

The most contributions an aggregation gate below root has, 0 when neither a comparison nor an aggregation is there.

The worst case of the Boolean view is the enumeration of the subsets of those contributions, so this is what the enumeration of the worlds of the inputs competes with.

Definition at line 2151 of file probability_evaluate.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ mobius_probability_of()

double mobius_probability_of ( pg_uuid_t token )

External entry point for the Möbius-route probability sweep (declared in mobius_evaluate.h, used by the stats SRF in mobius_evaluate.cpp).

Probability of a Möbius-route token (a gate_mobius-rooted circuit, or any Boolean island beneath one).

Definition at line 629 of file probability_evaluate.cpp.

Here is the caller graph for this function:

◆ probability_bounds()

Datum probability_bounds ( PG_FUNCTION_ARGS )

PostgreSQL-callable wrapper for the d-tree leaf bound: probability_bounds(token uuid, OUT lower float8, OUT upper float8).

Returns a cheap certified interval [lower,upper] with lower ≤ Pr ≤ upper for the probability of the DNF-shaped circuit rooted at token, via BooleanCircuit::dnfBounds (Olteanu-Huang-Koch Fig. 3). Errors when the circuit is not a monotone DNF over input leaves (the leaf-bound heuristic is DNF-specific); the future d-tree engine will recurse on non-DNF roots.

Definition at line 2565 of file probability_evaluate.cpp.

Here is the call graph for this function:

◆ probability_evaluate()

Datum probability_evaluate ( PG_FUNCTION_ARGS )

PostgreSQL-callable wrapper for probability_evaluate().

Definition at line 2509 of file probability_evaluate.cpp.

Here is the call graph for this function:

◆ probability_evaluate_internal()

Datum probability_evaluate_internal	(	pg_uuid_t	token,
		const string &	method,
		const string &	args,
		bool *	isnull )

static

Definition at line 2173 of file probability_evaluate.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ provsql_sigint_handler()

void provsql_sigint_handler ( int )

static

SIGINT handler that sets the global interrupted flag.

The signal number argument is required by the signal() API but is not used.

In addition to the provsql_interrupted flag polled by the long Monte-Carlo / possible-worlds evaluation loops, we drive PG's standard cancel pipeline (InterruptPending / QueryCancelPending

SetLatch) the same way PG's own StatementCancelHandler does. That makes a SIGINT delivered to the backend (e.g. via pg_cancel_backend) outside of a system() wait turn into a proper 57014 cancel at the next CHECK_FOR_INTERRUPTS instead of being silently absorbed. (The matching case where an external compiler is running is handled in run_external_tool, which runs the tool in its own process group and SIGKILLs that group on a pending cancel, then lets CHECK_FOR_INTERRUPTS raise it.)

Definition at line 652 of file probability_evaluate.cpp.

Here is the caller graph for this function:

◆ record_last_eval_method()

void record_last_eval_method ( const std::string & actual_method )

static

Record the method just used in the provsql.last_eval_method GUC (comma-separated, deduplicated across calls in the session) so callers can inspect which evaluation strategy the default auto-selection settled on.

Shared by the main dispatch and the early-returning gate_mobius route.

Definition at line 2117 of file probability_evaluate.cpp.

Here is the caller graph for this function:

◆ run_stopping_rule()

void run_stopping_rule	(	GenericCircuit &	gc,
		gate_t	gc_root,
		const MethodArgs &	a,
		double &	result,
		std::string &	actual_method )

static

Whole-circuit (eps,delta)-relative estimate via the stopping rule (shared by the explicit 'stopping-rule' method and the 'relative' path's estimator).

Complexity O(S / (p * eps^2) * ln(1/delta)): the Dagum rule draws ~Y1/p whole-circuit worlds, each an O(S) evalBool. The 1/p factor makes the cost NOT a priori computable from static features – a precise cost needs a p-lower-bound feature – which is why this estimator stays a path fallback rather than a cost-ranked portfolio member for now.

Definition at line 2085 of file probability_evaluate.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

◆ kPossibleWorldsAgg

const char* const kPossibleWorldsAgg = "possible-worlds-aggregates"

static

Core implementation of probability evaluation for a circuit token.

Parameters

token	UUID of the root provenance gate.
method	Evaluation method name (e.g. "independent", "monte-carlo").
args	Additional arguments for the chosen method.
isnull	Out-param set to `true` when the result is SQL NULL (a conditioned token whose evidence has probability zero); may be `NULL` when the caller does not need null-propagation.

Returns: Float8 Datum containing the computed probability (undefined when isnull is set to true). Name of the exact route that enumerates the worlds of the inputs on the circuit as it is, comparisons and aggregates evaluated per world.

Definition at line 2143 of file probability_evaluate.cpp.

◆ kPossibleWorldsAggMaxInputs

const unsigned kPossibleWorldsAggMaxInputs = 20

static

Most inputs it enumerates the 2^n worlds of.

Definition at line 2145 of file probability_evaluate.cpp.

Classes

Namespaces

Functions

Variables

Detailed Description

Function Documentation

◆ buildInversionFreeDDNNF()

◆ collect_inversion_free_keys()

◆ inversion_free_rank()

◆ maxAggContributions()

◆ mobius_probability_of()

◆ probability_bounds()

◆ probability_evaluate()

◆ probability_evaluate_internal()

◆ provsql_sigint_handler()

◆ record_last_eval_method()

◆ run_stopping_rule()

Variable Documentation

◆ kPossibleWorldsAgg

◆ kPossibleWorldsAggMaxInputs