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 "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 "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.
static Datum	probability_evaluate_internal (pg_uuid_t token, const string &method, const string &args, bool *isnull)
	Core implementation of probability evaluation for a circuit token.
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

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 755 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 674 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 734 of file probability_evaluate.cpp.

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 627 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 2425 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 2379 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

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

Definition at line 1898 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 650 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 1859 of file probability_evaluate.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Classes

Namespaces

Functions

Variables

Detailed Description

Function Documentation

◆ buildInversionFreeDDNNF()

◆ collect_inversion_free_keys()

◆ inversion_free_rank()

◆ mobius_probability_of()

◆ probability_bounds()

◆ probability_evaluate()

◆ probability_evaluate_internal()

◆ provsql_sigint_handler()

◆ run_stopping_rule()