Classes
struct	AggCmpMatch
	Result of matching a `gate_cmp` against the canonical HAVING aggregate-comparison shape. More...
struct	DTreeInterval
	A certified probability interval `lower` <= Pr <= upper. More...
struct	ConditionalScalarSamples
	Outcome of a conditional Monte Carlo sampling pass. More...
struct	EvalContext
	Per-evaluation circuit state threaded to a method's evaluate(). More...
struct	Tolerance
class	ProbabilityMethod
	Strategy interface: one concrete subclass per probability method. More...
class	MethodCatalog
	Registry of `ProbabilityMethod` objects. More...
struct	DistributionSpec
	Parsed distribution spec (kind + up to two parameters). More...
struct	TruncatedSingleRv
	Detection result for a closed-form, optionally-truncated single-RV shape. More...
struct	DiracShape
	Point mass at a finite scalar value (a `gate_value` root, or an `as_random(c)` leaf surfaced as a `gate_value`). More...
struct	CategoricalShape
	Categorical distribution over a finite outcome set. More...
struct	BernoulliMixtureShape
	Bernoulli mixture (`gate_mixture` with the [p_token, x_token, y_token] shape). More...
class	ScopedTempDir
	RAII guard around a freshly mkdtemp'd /tmp directory. More...
struct	ToolRecord
	One registered external tool. More...
class	ToolRegistry
	The process-local registry singleton. More...

Typedefs
using	ClosedFormShape
	One of the closed-form shapes the analytical-curves payload can render: bare RV (continuous PDF/CDF), Dirac (point mass), categorical (multiple point masses), or Bernoulli mixture of any two of the above.

Enumerations
enum class	ToleranceKind { Exact , Relative , Additive }
	The contract the user grants – the "path". More...
enum class	Feature { DnfShape , TreewidthProxy }
	A circuit feature a method's cost/applicability estimate depends on, but that is not free to acquire. More...
enum class	DistKind { Normal , Uniform , Exponential , Erlang }
	Continuous distribution kinds supported by `gate_rv`. More...

Functions
unsigned	runAggMarginalEvaluator (GenericCircuit &gc)
	Run the safe-join aggregate marginal-vector pre-pass over `gc`.
double	pdfAt (const DistributionSpec &d, double c)
	Closed-form probability density \(f(c)\) for a basic distribution.
double	cdfAt (const DistributionSpec &d, double c)
	Closed-form CDF \(F_X(c) = P(X \le c)\) for a basic continuous distribution.
unsigned	runAnalyticEvaluator (GenericCircuit &gc)
	Run the closed-form CDF resolution pass over `gc`.
bool	matchAggCmp (GenericCircuit &gc, gate_t cmp, AggCmpMatch &out)
	Try to match `cmp` against `gate_cmp`(gate_agg(α, semimod_i(K_i, m_i)*), gate_value(C)).
std::vector< unsigned >	computeRefCounts (const GenericCircuit &gc)
	Reference count of every gate as a wire-target across the whole circuit.
double	contributorProb (const GenericCircuit &gc, gate_t g, const std::vector< unsigned > &ref, bool &ok)
	Read-once marginal probability of a count/aggregate contributor (the K side of a semimod).
unsigned	runCountCmpEvaluator (GenericCircuit &gc)
	Run the Poisson-binomial pre-pass over `gc`.
DTreeInterval	dtreeBounds (const BooleanCircuit &c, Clauses clauses, double max_width, unsigned long budget, unsigned long *steps_out)
DTreeInterval	dtreeBoundsCircuit (const BooleanCircuit &c, gate_t root, double max_width, unsigned long budget=0, unsigned long *steps_out=nullptr)
	Certified probability interval of an arbitrary Boolean circuit, refined to a target width (the d-tree generalised off monotone DNF).
DTreeInterval	dtreeBounds (const BooleanCircuit &c, std::vector< std::set< gate_t > > clauses, double max_width, unsigned long budget=0, unsigned long *steps_out=nullptr)
	Certified probability interval of a monotone DNF, refined to a target width (Olteanu-Huang-Koch d-tree).
double	evaluateBooleanProbability (const GenericCircuit &gc, gate_t boolRoot)
	Probability that the Boolean subcircuit rooted at `boolRoot` evaluates to `true` under the tuple-independent probabilistic-database model.
double	compute_expectation (const GenericCircuit &gc, gate_t root, std::optional< gate_t > event_root=std::nullopt)
	Compute \(E[X]\) (or \(E[X \mid A]\) if `event_root` is set) over the scalar sub-circuit rooted at `root`.
double	compute_raw_moment (const GenericCircuit &gc, gate_t root, unsigned k, std::optional< gate_t > event_root=std::nullopt)
	Compute the raw moment \(E[X^k]\) (or \(E[X^k \mid A]\) if `event_root` is set) for `k` >= 0.
double	compute_central_moment (const GenericCircuit &gc, gate_t root, unsigned k, std::optional< gate_t > event_root=std::nullopt)
	Compute the central moment \(E[(X - E[X])^k]\) (or \(E[(X - E[X \mid A])^k \mid A]\) if `event_root` is set).
gate_t	lift_conditioning (GenericCircuit &gc, gate_t root, std::optional< gate_t > &event_opt)
	Lift conditioning out of a scalar arithmetic expression.
unsigned	runConstantFold (GenericCircuit &gc)
	Constant-fold pass over every `gate_arith` in `gc`.
unsigned	runHybridSimplifier (GenericCircuit &gc)
	Run the peephole simplifier over `gc`.
unsigned	runHybridDecomposer (GenericCircuit &gc, unsigned samples)
	Marginalise unresolved continuous-island `gate_cmp` gates into Bernoulli `gate_input` leaves.
std::string	kcmcp_compile (const std::string &endpoint, uint8_t input_format, const std::string &problem)
	Compile `problem` on a KCMCP server and return its d-DNNF NNF text.
unsigned	runMinMaxCmpEvaluator (GenericCircuit &gc)
	Run the MIN / MAX closed-form pre-pass over `gc`.
double	monteCarloRV (const GenericCircuit &gc, gate_t root, unsigned samples)
	Run Monte Carlo on a circuit that may contain `gate_rv` leaves.
double	monteCarloRVStopping (const GenericCircuit &gc, gate_t root, double eps, double delta, unsigned long max_samples, unsigned long &samples_used, bool &reached_target)
	Whole-circuit (eps,delta)-relative probability via the Dagum-Karp-Luby-Ross stopping rule.
std::vector< double >	monteCarloJointDistribution (const GenericCircuit &gc, const std::vector< gate_t > &cmps, unsigned samples)
	Estimate the joint distribution of `cmps` via Monte Carlo.
std::vector< double >	monteCarloScalarSamples (const GenericCircuit &gc, gate_t root, unsigned samples)
	Sample a scalar sub-circuit `samples` times and return the draws.
ConditionalScalarSamples	monteCarloConditionalScalarSamples (const GenericCircuit &gc, gate_t root, gate_t event_root, unsigned samples)
	Rejection-sample `root` conditioned on `event_root`.
std::optional< std::vector< double > >	try_truncated_closed_form_sample (const GenericCircuit &gc, gate_t root, gate_t event_root, unsigned n)
	Try to draw `n` exact samples from the conditional distribution of `root` given `event_root` via closed-form truncation, bypassing MC rejection.
bool	circuitHasRV (const GenericCircuit &gc, gate_t root)
	Walk the circuit reachable from `root` looking for any `gate_rv`.
bool	circuitHasUnresolvedSampleableAgg (const GenericCircuit &gc, gate_t root)
	Whether a surviving `gate_agg` exists and every one is sample-faithful (`SUM` / `AVG` / `MIN` / `MAX` / `COUNT` – every aggregate the sampler reproduces exactly).
static double	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	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	toleranceAdmits (ToleranceKind request, ToleranceKind method)
	Admissibility of a method's guarantee under a requested tolerance.
double	parseDoubleStrict (const std::string &s)
	Strictly parse `s` as a `double`.
std::optional< DistributionSpec >	parse_distribution_spec (const std::string &s)
	Parse the on-disk text encoding of a `gate_rv` distribution.
double	analytical_mean (const DistributionSpec &d)
	Closed-form expectation E[X] for a basic distribution.
double	analytical_variance (const DistributionSpec &d)
	Closed-form variance Var(X) for a basic distribution.
double	analytical_raw_moment (const DistributionSpec &d, unsigned k)
	Closed-form raw moment \(E[X^k]\) for a basic distribution.
unsigned	runRangeCheck (GenericCircuit &gc)
	Run the support-based pruning pass over `gc`.
unsigned	runHavingAlwaysTrueRewriter (GenericCircuit &gc)
	Probability-side pre-pass: rewrite HAVING-style `gate_cmp` gates that are provably TRUE on the agg's value-interval into an OR over the agg's per-row K-gates.
std::pair< double, double >	compute_support (const GenericCircuit &gc, gate_t root, std::optional< gate_t > event_root=std::nullopt)
	Compute the [lo, hi] support interval of a scalar sub-circuit rooted at `root`.
std::optional< std::pair< double, double > >	collectRvConstraints (const GenericCircuit &gc, gate_t event_root, gate_t target_rv)
	Walk `event_root` collecting rv op c constraints on `target_rv`.
static bool	extract_finite_double (const GenericCircuit &gc, gate_t x, double &out)
	Parse a `gate_value's` `extra` as a finite `float8`.
static bool	extract_mulinput_value (const GenericCircuit &gc, gate_t mul, double &out)
	Same parsing applied to a mulinput's outcome label (categorical).
std::optional< TruncatedSingleRv >	matchTruncatedSingleRv (const GenericCircuit &gc, gate_t root, std::optional< gate_t > event_root)
	Detect a closed-form, optionally-truncated single-RV shape.
bool	eventIsProvablyInfeasible (const GenericCircuit &gc, gate_t root, std::optional< gate_t > event_root)
	True iff the conditioning event is provably infeasible for a bare `gate_rv` root.
static std::optional< double >	shape_mass (const ClosedFormShape &s, double lo, double hi)
	Unconditional probability mass of a shape over the interval [lo, hi].
static std::optional< ClosedFormShape >	truncateShape (const ClosedFormShape &s, double lo, double hi)
	Conditional shape after truncating the underlying variable to [lo, hi].
std::optional< ClosedFormShape >	matchClosedFormDistribution (const GenericCircuit &gc, gate_t root, std::optional< gate_t > event_root)
	Detect any of the closed-form shapes supported by `rv_analytical_curves`.
std::optional< std::vector< std::tuple< double, double, double > > >	analyticalHistogram (const ClosedFormShape &shape, int bins)
	Exact histogram (bin_lo, bin_hi, probability mass) of a closed-form `shape`, in `bins` equal-width bins over its natural range.
unsigned	runSumCmpEvaluator (GenericCircuit &gc)
	Run the weighted-sum DP pre-pass over `gc`.
std::string	expandCommandTemplate (const std::string &tpl, const std::string &binary, const std::string &in, const std::string &out, const std::vector< std::pair< std::string, std::string > > &extra={})
	Expand a command template into a runnable shell command line.
ToolRegistry &	tool_registry ()
	Shorthand for `ToolRegistry::instance()`.

Variables
static const size_t	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	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	kCostIndependent = 5e-5
static const double	kCostInversionFree = 5e-5
static const double	kCostPossibleWorlds = 3e-6
static const double	kCostSieve = 1e-5
static const double	kCostTreeDecomp = 7e-4
static const double	kCostCompilation = 2e-3
static const double	kCostCompilationFloor = 40.0
static const double	kCostDnfShapeFeature = 2e-6
static const double	kCostTwProxyFeature = 3e-4
static const double	kCostMonteCarlo = 1e-5
static const double	kCostStoppingRule = 1e-3
static const double	kCostKarpLuby = 3e-6
static const double	kCostDTreeExact = 3e-4
static const double	kCostDTreeApprox = 4e-4
static const double	kCostDTreeMsPerStepDnf = 1.4e-3
static const double	kCostDTreeMsPerStepGeneral = 5e-4

Typedef Documentation

◆ ClosedFormShape

using provsql::ClosedFormShape

Initial value:

std::variant<TruncatedSingleRv,
                                    DiracShape,
                                    CategoricalShape,
                                    BernoulliMixtureShape>

One of the closed-form shapes the analytical-curves payload can render: bare RV (continuous PDF/CDF), Dirac (point mass), categorical (multiple point masses), or Bernoulli mixture of any two of the above.

Definition at line 201 of file RangeCheck.h.

Enumeration Type Documentation

◆ DistKind

enum class provsql::DistKind

strong

Continuous distribution kinds supported by gate_rv.

Enumerator
Normal	Normal (Gaussian): p1=μ, p2=σ
Uniform	Uniform on [a,b]: p1=a, p2=b.
Exponential	Exponential: p1=λ, p2 unused.
Erlang	Erlang: p1=k (positive integer), p2=λ. Sum of k i.i.d. `Exp`(λ); support [0, +∞). The parameter `k` is stored in `p1` as a double but must be integer-valued ≥ 1 for any consumer that uses the finite-sum CDF / sampler.

Definition at line 28 of file RandomVariable.h.

◆ Feature

enum class provsql::Feature

strong

A circuit feature a method's cost/applicability estimate depends on, but that is not free to acquire.

Acquiring a feature has a cost (modelled by EvalContext::featureCost), and the chooser acquires one lazily only when no already-known method is cheaper than acquiring it – so a circuit the cheap methods resolve (read-once via independent, certified via inversion-free) never pays for analysis that could not change the decision. Free/O(1) features (#inputs, an inversion-free certificate) are not modelled here – they are read eagerly.

DnfShape is a linear dnfShape walk. TreewidthProxy is a cheap (O(V+E)) degeneracy lower bound on the circuit's treewidth that gates tree-decomposition's cost – it rules the method out when the bound already exceeds the build's limit, while the bounded-treewidth build can still fail implicitly when the bound is inconclusive.

Enumerator
DnfShape
TreewidthProxy

Definition at line 76 of file ProbabilityMethod.h.

◆ ToleranceKind

enum class provsql::ToleranceKind

strong

The contract the user grants – the "path".

Exact is tolerance (0,0); Relative promises (1±epsilon) with confidence 1-delta; Additive promises |p̂-p| <= epsilon with the same confidence. Admissible method sets nest Exact ⊂ Relative ⊂ Additive.

The tolerance is recorded but does not by itself drive method selection: named methods dispatch by name and the empty method set runs the exact ladder.

Enumerator
Exact
Relative
Additive

Definition at line 51 of file ProbabilityMethod.h.

Function Documentation

◆ analytical_mean()

double provsql::analytical_mean ( const DistributionSpec & d )

Closed-form expectation E[X] for a basic distribution.

Normal(μ, σ): μ
Uniform(a, b): (a + b) / 2
Exponential(λ): 1 / λ
Erlang(k, λ): k / λ

Definition at line 95 of file RandomVariable.cpp.

Here is the caller graph for this function:

◆ analytical_raw_moment()

double provsql::analytical_raw_moment	(	const DistributionSpec &	d,
		unsigned	k )

Closed-form raw moment \(E[X^k]\) for a basic distribution.

Normal(μ, σ): \(\sum_{j=0,2,\ldots}^{k} \binom{k}{j} \mu^{k-j} \sigma^j (j-1)!!\) (odd- \(j\) terms vanish since central moments of \(N(0, \sigma)\) are zero for odd \(j\)).
Uniform(a, b): \((b^{k+1} - a^{k+1}) / ((k+1)(b-a))\).
Exponential(λ): \(k! / \lambda^k\).
Erlang(s, λ): \(\Gamma(s+k) / (\Gamma(s) \lambda^k) = s(s+1)\cdots(s+k-1) / \lambda^k\) for integer shape \(s\).

Returns 1 for \(k = 0\) and analytical_mean for \(k = 1\).

Definition at line 165 of file RandomVariable.cpp.

Here is the call graph for this function:

◆ analytical_variance()

double provsql::analytical_variance ( const DistributionSpec & d )

Closed-form variance Var(X) for a basic distribution.

Normal(μ, σ): σ²
Uniform(a, b): (b − a)² / 12
Exponential(λ): 1 / λ²
Erlang(k, λ): k / λ²

Definition at line 106 of file RandomVariable.cpp.

◆ analyticalHistogram()

std::optional< std::vector< std::tuple< double, double, double > > > provsql::analyticalHistogram	(	const ClosedFormShape &	shape,
		int	bins )

Exact histogram (bin_lo, bin_hi, probability mass) of a closed-form shape, in bins equal-width bins over its natural range.

Defined in RvAnalyticalCurves.cpp (where the shape CDF / range helpers live). Lets rv_histogram answer for a closed-form distribution without sampling – e.g. a truncated Gaussian under provsql.rv_mc_samples = 0. Returns std::nullopt when the range is degenerate or the CDF is unavailable, so the caller can fall back to Monte Carlo.

Definition at line 291 of file RvAnalyticalCurves.cpp.

Here is the caller graph for this function:

◆ cdfAt()

double provsql::cdfAt	(	const DistributionSpec &	d,
		double	c )

Closed-form CDF \(F_X(c) = P(X \le c)\) for a basic continuous distribution.

Returns the cumulative distribution at c for the distribution d. Used internally by AnalyticEvaluator's gate_cmp resolution and by the HybridEvaluator decomposer's monotone-shared-scalar fast path to compute interval probabilities analytically (no MC noise) when the shared scalar is a bare gate_rv. Returns NaN when d carries a parameter shape the CDF doesn't cover (e.g. non-integer Erlang shape, which would require the regularised lower incomplete gamma function).

Normal(μ, σ): \(\Phi((c - \mu) / \sigma)\) via std::erf.
Uniform(a, b): piecewise linear; 0 for c<=a, 1 for c>=b, (c - a) / (b - a) otherwise.
Exponential(λ): 1 - exp(-λc) for c>0; 0 for c<=0.
Erlang(k, λ) (integer k≥1): finite-sum form \(1 - e^{-\lambda c} \sum_{n=0}^{k-1} (\lambda c)^n / n!\) for c>0.

Definition at line 70 of file AnalyticEvaluator.cpp.

Here is the caller graph for this function:

◆ circuitHasRV()

bool provsql::circuitHasRV	(	const GenericCircuit &	gc,
		gate_t	root )

Walk the circuit reachable from root looking for any gate_rv.

Used by probability_evaluate to dispatch between the existing BooleanCircuit path and the RV-aware sampler in this file.

Definition at line 702 of file MonteCarloSampler.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ circuitHasUnresolvedSampleableAgg()

bool provsql::circuitHasUnresolvedSampleableAgg	(	const GenericCircuit &	gc,
		gate_t	root )

Whether a surviving gate_agg exists and every one is sample-faithful (SUM / AVG / MIN / MAX / COUNT – every aggregate the sampler reproduces exactly).

A gate_agg the exact closed-form / marginal-vector pre-passes did not fold into a Bernoulli gate_input marks a HAVING aggregate comparator whose exact resolution needs provsql_having's threshold-lineage expansion – which does not terminate in practice for a large-magnitude / large-support aggregate (the dense kMaxSumRange and sparse kMaxSumSupport caps exceeded). For an (eps,delta) request probability_evaluate uses this to route the circuit straight to the world-sampler (the gate_agg arm of evalScalar) – a sound FPRAS for the apx-safe corner of the HAVING trichotomy – instead of attempting the non-terminating Boolean expansion.

The sampler's gate_agg arm pushes each kept contributor's value into the matching Aggregator, reproducing SQL semantics exactly: the value gate is the row's contribution (the summed term for SUM; the 0/1 indicator for COUNT, 0 for a NULL row so count(x) does not count NULLs; the compared value for AVG / MIN / MAX), so NULL rows are handled and an empty group finalises to the value the exact evaluator uses (0 for SUM / COUNT, NaN -> comparison false for the others), and gate_arith over them is covered too. In practice only SUM / AVG / MIN / MAX ever reach here: COUNT's value-support is small (0/1 per row) so it is always resolved exactly and never bails – but it is sample-faithful as well, so it is not excluded.

Definition at line 724 of file MonteCarloSampler.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ collectRvConstraints()

std::optional< std::pair< double, double > > provsql::collectRvConstraints	(	const GenericCircuit &	gc,
		gate_t	event_root,
		gate_t	target_rv )

Walk event_root collecting rv op c constraints on target_rv.

Descends through AND-conjunct factors (gate_times, gate_one, Boolean leaves whose footprint doesn't include target_rv – these are independent of the RV and contribute no truncation) collecting every gate_cmp interpretable as target_rv op c for a constant c, and intersects them into a running interval seeded with the unconditional support of target_rv.

Returns the resulting interval as (lo, hi), or std::nullopt if the walk found a structure that defeats the recognisers (a gate_plus / gate_monus disjunction over the chain, a cmp shape other than rv op const, ...). Callers treat std::nullopt as "fall back to the unconditional case" – sound for support and MC fallback for moments.

Constraints on RVs other than target_rv are ignored; they affect P(A) but not the truncation of the target's distribution.

Definition at line 1327 of file RangeCheck.cpp.

Here is the caller graph for this function:

◆ compute_central_moment()

double provsql::compute_central_moment	(	const GenericCircuit &	gc,
		gate_t	root,
		unsigned	k,
		std::optional< gate_t >	event_root = std::nullopt )

Compute the central moment \(E[(X - E[X])^k]\) (or \(E[(X - E[X \mid A])^k \mid A]\) if event_root is set).

k = 0 returns 1; k = 1 returns 0; k = 2 returns the variance. Higher orders are obtained by binomial expansion in terms of the raw moments returned by compute_raw_moment, which inherits the analytical / MC dispatch described above.

Definition at line 942 of file Expectation.cpp.

Here is the caller graph for this function:

◆ compute_expectation()

double provsql::compute_expectation	(	const GenericCircuit &	gc,
		gate_t	root,
		std::optional< gate_t >	event_root = std::nullopt )

Compute \(E[X]\) (or \(E[X \mid A]\) if event_root is set) over the scalar sub-circuit rooted at root.

The conditional path requires that event_root be a gate_t in the same GenericCircuit as root – typically the circuit was loaded via getJointCircuit so a shared gate_rv between root and event has one gate_t, which is what couples the MC sampler. When event_root is std::nullopt the unconditional path (existing analytical decomposition with MC fallback) is taken unchanged.

Exceptions

CircuitException on malformed circuits, unknown distribution kinds, when provsql.rv_mc_samples is 0 and a sub-expression cannot be decomposed analytically, or when the conditional MC pass accepts too few samples (suggesting P(A) is very small or zero).

Definition at line 924 of file Expectation.cpp.

Here is the caller graph for this function:

◆ compute_raw_moment()

double provsql::compute_raw_moment	(	const GenericCircuit &	gc,
		gate_t	root,
		unsigned	k,
		std::optional< gate_t >	event_root = std::nullopt )

Compute the raw moment \(E[X^k]\) (or \(E[X^k \mid A]\) if event_root is set) for k >= 0.

k = 0 returns 1; k = 1 delegates to compute_expectation.

Definition at line 933 of file Expectation.cpp.

Here is the caller graph for this function:

◆ compute_support()

std::pair< double, double > provsql::compute_support	(	const GenericCircuit &	gc,
		gate_t	root,
		std::optional< gate_t >	event_root = std::nullopt )

Compute the [lo, hi] support interval of a scalar sub-circuit rooted at root.

Same interval-arithmetic propagation runRangeCheck uses internally, exposed for the SQL support() function:

gate_value: point [c, c].
gate_rv: distribution support (uniform exact, exponential on [0, +∞), normal on (-∞, +∞)).
gate_arith: propagated through +, −, ×, /, unary −.

Anything else collapses to the conservative all-real interval (-∞, +∞). Never throws on unrecognised gates – callers receive the wide interval instead, which is the right semantic for "we cannot prove a tighter bound".

When event_root is set, the returned interval is the intersection of the unconditional support with the per-RV constraints implied by the AND-conjunct chain rooted at the event (rv op c cmps over root collected via the same walker runRangeCheck uses for joint feasibility). Constraints we cannot interpret are silently skipped: the result is then a conservative superset of the true conditional support, never a subset.

Definition at line 1294 of file RangeCheck.cpp.

Here is the caller graph for this function:

◆ computeRefCounts()

std::vector< unsigned > provsql::computeRefCounts ( const GenericCircuit & gc )

Reference count of every gate as a wire-target across the whole circuit.

One pass over all wire lists; O(total wires).

Definition at line 115 of file CmpEvaluatorCommon.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ contributorProb()

double provsql::contributorProb	(	const GenericCircuit &	gc,
		gate_t	g,
		const std::vector< unsigned > &	ref,
		bool &	ok )

Read-once marginal probability of a count/aggregate contributor (the K side of a semimod).

Exact precisely when the contributor's sub-circuit is a private read-once tree: every randomness-bearing gate it visits must have reference count 1. That single condition gives pairwise-disjoint leaf sets across contributors, no reuse outside the cmp, and read-once-ness within a contributor. Supports input / times / plus / monus and the one / zero constants; clears ok on any other gate type or on a reference-count violation. See CountCmpEvaluator.h for the full argument.

Definition at line 129 of file CmpEvaluatorCommon.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ dtreeBounds() [1/2]

DTreeInterval provsql::dtreeBounds	(	const BooleanCircuit &	c,
		Clauses	clauses,
		double	max_width,
		unsigned long	budget,
		unsigned long *	steps_out )

Definition at line 272 of file DTree.cpp.

◆ dtreeBounds() [2/2]

DTreeInterval provsql::dtreeBounds	(	const BooleanCircuit &	c,
		std::vector< std::set< gate_t > >	clauses,
		double	max_width,
		unsigned long	budget = 0,
		unsigned long *	steps_out = nullptr )

Certified probability interval of a monotone DNF, refined to a target width (Olteanu-Huang-Koch d-tree).

Refines BooleanCircuit::dnfBounds by independent-or decomposition and Shannon expansion until upper-lower <= max_width, propagating the width budget so the returned interval honours it: through Shannon the same budget passes to both cofactors (the mixture width is at most the larger branch's), through an independent-or of k components each gets max_width/k (the OR width is at most the sum of the component widths). max_width == 0 forces exact compilation (lower == upper).

Parameters

c	Circuit owning the input marginals (`getProb`).
clauses	The DNF as per-clause input-leaf supports (consumed).
max_width	Absolute target for `upper-lower` (0 = exact).
budget	Subproblem (recursion-step) ceiling; 0 = unbounded. On overrun a `CircuitException` is thrown so the caller's cost-based chooser escalates to another method.
steps_out	If non-null, receives the number of recursion steps taken (for cost calibration).

Returns: A sound interval with lower <= Pr[clauses] <= upper.

◆ dtreeBoundsCircuit()

DTreeInterval provsql::dtreeBoundsCircuit	(	const BooleanCircuit &	c,
		gate_t	root,
		double	max_width,
		unsigned long	budget = 0,
		unsigned long *	steps_out = nullptr )

Certified probability interval of an arbitrary Boolean circuit, refined to a target width (the d-tree generalised off monotone DNF).

Same anytime engine as dtreeBounds, but recursing on the circuit DAG (AND / OR / NOT / IN) instead of a flat monotone-DNF clause set, so it applies to negation (EXCEPT / monus, encoded A AND NOT B), nested AND / OR (e.g. a CNF-shaped circuit), and arbitrary sharing.

The cheap leaf bound generalises dnfBounds soundly to any gate: an independent-component split (children with disjoint free-variable footprints compose exactly), then a Bonferroni lower / min upper for AND, a max lower / union upper for OR, and a flip [1-U,1-L] for NOT. It is refined by independent-component decomposition and Shannon expansion on the most frequent shared free variable until upper-lower <= max_width (0 = exact). Every step keeps lower <= Pr <= upper (Shannon is an exact mixture; independence is over disjoint input cones, never overclaimed).

Throws CircuitException on a multivalued (MULIN / MULVAR) or UNDETERMINED gate in the cone of root, so the caller falls back to another method on BID circuits.

Parameters

c	Circuit (gate types, wiring, input marginals).
root	Root gate whose probability interval is computed.
max_width	Absolute target for `upper-lower` (0 = exact).
budget	Subproblem (recursion-step) ceiling; 0 = unbounded. On overrun a `CircuitException` is thrown so the caller's cost-based chooser escalates to another method.
steps_out	If non-null, receives the number of recursion steps taken (for cost calibration).

Returns: A sound interval with lower <= Pr[root] <= upper.

Definition at line 651 of file DTree.cpp.

◆ evaluateBooleanProbability()

double provsql::evaluateBooleanProbability	(	const GenericCircuit &	gc,
		gate_t	boolRoot )

Probability that the Boolean subcircuit rooted at boolRoot evaluates to true under the tuple-independent probabilistic-database model.

Tries BooleanCircuit::independentEvaluation first; if that throws (e.g. the subcircuit is not disconnected for that method), falls back to Monte Carlo with provsql.rv_mc_samples samples. Used by the mixture moment evaluators for compound Boolean Bernoulli wires.

Definition at line 36 of file Expectation.cpp.

Here is the call graph for this function:

◆ eventIsProvablyInfeasible()

bool provsql::eventIsProvablyInfeasible	(	const GenericCircuit &	gc,
		gate_t	root,
		std::optional< gate_t >	event_root )

True iff the conditioning event is provably infeasible for a bare gate_rv root.

Distinguishes "event proved infeasible" (event resolves to gate_zero, or collectRvConstraints intersects to an empty interval) from "shape unsupported by @c matchTruncatedSingleRv" (return std::nullopt that just means "fall back to MC").

Used by the conditional-moment dispatcher to raise an explicit infeasibility error before falling through to MC rejection – MC would still detect the same condition by accepting 0 of N samples, but the closed-form predicate spots it without ten thousand wasted draws and emits a tighter message.

Returns false for non-gate_rv roots and for roots whose event/support pair is not provably infeasible by this cheap pass (the caller can still proceed to MC).

Definition at line 1445 of file RangeCheck.cpp.

Here is the call graph for this function:

◆ expandCommandTemplate()

std::string provsql::expandCommandTemplate	(	const std::string &	tpl,
		const std::string &	binary,
		const std::string &	in,
		const std::string &	out,
		const std::vector< std::pair< std::string, std::string > > &	extra = {} )

inline

Expand a command template into a runnable shell command line.

Replaces {binary} / {in} / {out} and any extra placeholders (e.g. {tmpdir}, {pivotAC}) in tpl. When tpl contains no {binary} placeholder, a non-empty binary is prepended (the common "<binary> <args>" shape); a template that places the binaries itself (the dpmc pipeline) is returned as-is.

Header-only and dependency-free on purpose, so the standalone tdkc build can expand a template without linking the registry.

Definition at line 57 of file ToolRegistry.h.

Here is the caller graph for this function:

◆ extract_finite_double()

bool provsql::extract_finite_double	(	const GenericCircuit &	gc,
		gate_t	x,
		double &	out )

static

Parse a gate_value's extra as a finite float8.

Sibling of extract_constant_double in having_semantics.cpp but with a const GenericCircuit ref (used in the closed-form shape detector path). Bails on NaN / ±Infinity so a downstream stem renderer never sees a non-finite x coordinate.

Definition at line 1366 of file RangeCheck.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ extract_mulinput_value()

bool provsql::extract_mulinput_value	(	const GenericCircuit &	gc,
		gate_t	mul,
		double &	out )

static

Same parsing applied to a mulinput's outcome label (categorical).

Definition at line 1384 of file RangeCheck.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ kcmcp_compile()

std::string provsql::kcmcp_compile	(	const std::string &	endpoint,
		uint8_t	input_format,
		const std::string &	problem )

Compile problem on a KCMCP server and return its d-DNNF NNF text.

Connects to endpoint ("unix:/path" or "host:port"), performs the HELLO handshake, issues one compile REQUEST for problem in the given input_format (0 = dimacs-cnf, 1 = circuit-bcs12) wanting ddnnf-nnf output, and returns the RESULT's NNF text verbatim (parsed by BooleanCircuit::parseDDNNF, exactly as the CLI temp-file path is). A fresh connection per call.

Honours PostgreSQL query-cancel / statement_timeout while waiting: a pending cancel closes the socket (so the server abandons the job) and is then raised, mirroring the cancel discipline in external_tool.cpp. Throws std::runtime_error on any connect / protocol / server-ERROR failure so the caller can fall back to the CLI path.

Definition at line 252 of file kcmcp_client.cpp.

Here is the caller graph for this function:

◆ lift_conditioning()

gate_t provsql::lift_conditioning	(	GenericCircuit &	gc,
		gate_t	root,
		std::optional< gate_t > &	event_opt )

Lift conditioning out of a scalar arithmetic expression.

Normalise conditioning in a scalar sub-circuit before evaluation.

Implements "f(X|A, Y|B, …) = f(X, Y, …) | (A ∧ B ∧ …)": walks the scalar tree rooted at root, replaces every nested gate_conditioned by a transparent passthrough to its target (so the tree becomes the plain arithmetic over the unconditioned distributions), collects the evidence children, and conjoins them – together with any pre-existing event_opt – into a single conditioning event. The conjunction is built as an in-memory gate_times over the evidence gates, all of which already live in the (joint) circuit, so a base gate_rv shared between a value and its evidence keeps a single draw under the MC sampler. A conditioned ROOT is peeled to its bare target (returned), so a stored "X | C" reaching any low-level RV entry point keeps the closed-form scalar path; the (possibly new) root is returned. Leaves event_opt untouched and returns root unchanged when the expression carries no conditioning.

Peels a conditioned ROOT to its bare target and rewrites every buried gate_conditioned into a transparent passthrough, folding all collected evidence (and any pre-existing event_opt) into a single conditioning event left in event_opt. Returns the (possibly new) root so a stored "X | C" reaching a low-level RV entry point evaluates as the bare scalar conditioned on the folded event – keeping the closed-form path available. No-op (returns root, leaves event_opt untouched) when there is no conditioning.

Definition at line 978 of file Expectation.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ makeDDAuto()

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.

A thin entry point over MethodCatalog::chooseAndBuildDD that builds the EvalContext from the Boolean view alone (the d-D portfolio needs no generic-circuit state); the callers that have a method/compiler request route the empty / "default" / "auto" case here and keep BooleanCircuit::makeDD for the named routes (tree-decomposition / interpret-as-dd / compilation, plus makeDD's own internal interpret -> tree-decomposition -> compiler fallback chain).

Definition at line 1619 of file probability_evaluate.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ matchAggCmp()

bool provsql::matchAggCmp	(	GenericCircuit &	gc,
		gate_t	cmp,
		AggCmpMatch &	out )

Try to match cmp against gate_cmp(gate_agg(α, semimod_i(K_i, m_i)*), gate_value(C)).

Accepts both operand orders (agg left or right), flipping op in the latter case. Mirrors pw_from_cmp_gate's build_from and the SUM-of-1s → COUNT remap. Returns false (leaving out untouched) on any shape mismatch; cheap to call.

Parameters

[in]	gc	Circuit to inspect.
[in]	cmp	Candidate `gate_cmp`.
[out]	out	Filled on success.

Returns: true iff the shape matched.

Definition at line 17 of file CmpEvaluatorCommon.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ matchClosedFormDistribution()

std::optional< ClosedFormShape > provsql::matchClosedFormDistribution	(	const GenericCircuit &	gc,
		gate_t	root,
		std::optional< gate_t >	event_root )

Detect any of the closed-form shapes supported by rv_analytical_curves.

Generalisation of matchTruncatedSingleRv that adds Bernoulli mixtures, categoricals, and Dirac (scalar gate_value) roots. Conditioning (event_root) is honoured for bare RV roots only; Dirac / categorical / mixture roots bail when the event isn't gate_one (the post-load-simplification "always true" default).

Returns std::nullopt when none of the supported shapes match; callers fall back to histogram-only rendering.

Definition at line 1580 of file RangeCheck.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ matchTruncatedSingleRv()

std::optional< TruncatedSingleRv > provsql::matchTruncatedSingleRv	(	const GenericCircuit &	gc,
		gate_t	root,
		std::optional< gate_t >	event_root )

Detect a closed-form, optionally-truncated single-RV shape.

Common shape-detection helper shared by every closed-form single-RV consumer:

try_truncated_closed_form (truncated moments, Expectation.cpp);
try_truncated_closed_form_sample (rejection-free sampling, MonteCarloSampler.cpp);
rv_analytical_curves (PDF / CDF overlay, RvAnalyticalCurves.cpp).

Returns std::nullopt when the shape is not tractable:

root is not a bare gate_rv;
the gate's extra does not parse as a DistributionSpec;
event_root resolves to gate_zero (event already decided infeasible by runRangeCheck);
collectRvConstraints fails (incomplete walk);
the resulting interval is empty or degenerate (lo >= hi).

When event_root is omitted or resolves to gate_one, the returned TruncatedSingleRv carries the RV's natural support and truncated = false; callers that don't distinguish the conditional and unconditional cases (e.g. the analytical-curves x-range chooser) can read uniformly off the result.

Definition at line 1402 of file RangeCheck.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ monteCarloConditionalScalarSamples()

ConditionalScalarSamples provsql::monteCarloConditionalScalarSamples	(	const GenericCircuit &	gc,
		gate_t	root,
		gate_t	event_root,
		unsigned	samples )

Rejection-sample root conditioned on event_root.

For each of samples iterations, the shared Sampler resets its per-iteration cache, then:

evaluates event_root as a Boolean (populating bool_cache_ and scalar_cache_ for every gate_rv / gate_input touched);
if the indicator is true, evaluates root as a scalar using the SAME caches, so any shared gate_t leaf produces one draw that the indicator and the value both observe;
otherwise rejects the iteration.

This coupling is the entire point of routing the conditional path through one joint circuit: a gate_rv reachable from both root and event_root has the same gate_t and therefore shares its per-iteration draw between the indicator (which decides acceptance) and the value (which we record). The accepted draws are samples from the conditional distribution \(X \mid A\) where X = root and A = event_root.

Parameters

gc	Circuit (typically from `getJointCircuit`).
root	Scalar gate whose value we sample.
event_root	Boolean gate that the iteration must satisfy.
samples	Number of iterations to attempt.

Definition at line 526 of file MonteCarloSampler.cpp.

Here is the caller graph for this function:

◆ monteCarloJointDistribution()

std::vector< double > provsql::monteCarloJointDistribution	(	const GenericCircuit &	gc,
		const std::vector< gate_t > &	cmps,
		unsigned	samples )

Estimate the joint distribution of cmps via Monte Carlo.

For each of samples worlds, samples the underlying continuous island once (shared gate_rv leaves use the same per-iteration draw, per monteCarloRV's evalScalar) and evaluates each comparator in cmps; the k = cmps.size() resulting bits form a single word w with bit i = result of cmps[i]. The returned vector has size 2^k; entry w is the empirical probability that the joint outcome w occurred.

Used by the multi-cmp half of the hybrid evaluator's island decomposer to inline a categorical distribution over the k cmps that share an island; cmps must all sit over a continuous island whose scalar evaluation reuses common gate_rv leaves so the cmp draws are correctly correlated.

k is capped at 30 (the result vector size is 2^30) to keep memory bounded; the decomposer enforces a much tighter cap (k_max in HybridEvaluator.cpp) so this is purely a safety limit. Throws CircuitException above the cap.

Parameters

gc	The circuit.
cmps	The comparators jointly evaluated.
samples	Number of independent worlds.

Returns: Vector of joint probabilities, indexed by the bit word w (bit i = cmps[i] outcome).

Definition at line 469 of file MonteCarloSampler.cpp.

◆ monteCarloRV()

double provsql::monteCarloRV	(	const GenericCircuit &	gc,
		gate_t	root,
		unsigned	samples )

Run Monte Carlo on a circuit that may contain gate_rv leaves.

Parameters

gc	The circuit (loaded from the mmap store via `CircuitFromMMap`).
root	Gate to evaluate as a Boolean expression.
samples	Number of independent worlds to sample.

Returns: Estimated probability that root is true.

Exceptions

CircuitException on malformed circuits (unknown gate kind in a Boolean position, malformed extra, unknown comparison operator, etc.).

Definition at line 407 of file MonteCarloSampler.cpp.

Here is the caller graph for this function:

◆ monteCarloRVStopping()

double provsql::monteCarloRVStopping	(	const GenericCircuit &	gc,
		gate_t	root,
		double	eps,
		double	delta,
		unsigned long	max_samples,
		unsigned long &	samples_used,
		bool &	reached_target )

Whole-circuit (eps,delta)-relative probability via the Dagum-Karp-Luby-Ross stopping rule.

The general-Bernoulli case of BooleanCircuit::karpLubyStopping, driven by the RV-aware Sampler's evalBool rather than by DNF coverage trials, so it applies to ANY circuit the sampler can evaluate (plain Boolean, continuous gate_rv, and HAVING gate_cmp / gate_agg) – the universal relative estimator. Draws whole-circuit worlds until the success count reaches the threshold Y1 = 1 + (1+eps)*4*(e-2)*ln(2/delta)/eps^2, then returns Y1/N: a relative (eps,delta) approximation of Pr[root]. The sample count N adapts to the true Pr[root] (expected Y1/Pr[root]), so the cost is polynomial precisely when Pr[root] is at least 1/poly.

Sampling stops early at max_samples worlds; reached_target is then false and the return is the plain unbiased success/N mean over the spent budget (the relative target was not met – the caller reports the weaker, additive guarantee actually achieved).

Parameters

gc	The circuit.
root	Gate to evaluate as a Boolean event.
eps	Target relative error (in (0,1]).
delta	Target failure probability (in (0,1)).
max_samples	Hard cap on the number of worlds drawn.
samples_used	Output: worlds actually drawn.
reached_target	Output: whether the threshold was reached before the cap (i.e. the relative guarantee holds).

Returns: The probability estimate.

Definition at line 425 of file MonteCarloSampler.cpp.

Here is the caller graph for this function:

◆ monteCarloScalarSamples()

std::vector< double > provsql::monteCarloScalarSamples	(	const GenericCircuit &	gc,
		gate_t	root,
		unsigned	samples )

Sample a scalar sub-circuit samples times and return the draws.

root must yield a scalar (gate_value, gate_rv, or gate_arith over scalar children); otherwise a CircuitException is thrown. Each iteration uses a fresh per-iteration memo cache so that repeated occurrences of the same gate_rv UUID inside an arithmetic expression share their draw within an iteration but not across iterations.

The RNG is seeded from provsql.monte_carlo_seed exactly like monteCarloRV; pinning the GUC makes the returned vector reproducible.

Used as the universal MC fallback by the analytical evaluators (Expectation, HybridEvaluator) when structural shortcuts cannot decide a sub-expression. Returning the raw draws (rather than a single statistic) lets callers compute any combination of moments from a single sampling pass.

Definition at line 507 of file MonteCarloSampler.cpp.

Here is the caller graph for this function:

◆ parse_distribution_spec()

std::optional< DistributionSpec > provsql::parse_distribution_spec ( const std::string & s )

Parse the on-disk text encoding of a gate_rv distribution.

Accepts "normal:μ,σ", "uniform:a,b", "exponential:λ", and "erlang:k,λ", with parameters parseable as double. Whitespace around the kind name and parameters is tolerated.

Parameters

s	The byte string read from `MMappedCircuit::getExtra`.

Returns: The parsed spec, or std::nullopt on malformed input.

Definition at line 59 of file RandomVariable.cpp.

Here is the caller graph for this function:

◆ parseDoubleStrict()

double provsql::parseDoubleStrict ( const std::string & s )

Strictly parse s as a double.

Used by every consumer that has to interpret the extra byte string of a gate_value: the sampler when sampling a constant leaf, the interval-arith pass when bounding a constant leaf, and any future scalar-evaluation pass. Lives here (rather than next to one specific consumer) so the parsing convention is shared.

Exceptions

CircuitException on empty input, non-numeric input, or trailing characters past the parsed double.

Definition at line 17 of file RandomVariable.cpp.

Here is the caller graph for this function:

◆ pdfAt()

double provsql::pdfAt	(	const DistributionSpec &	d,
		double	c )

Closed-form probability density \(f(c)\) for a basic distribution.

Used by rv_analytical_curves to ship a sampled curve to clients (Studio's Distribution profile overlay). Returns 0 outside the natural support and NaN for parameter shapes the analytical form doesn't cover (e.g. non-integer Erlang shape).

Normal(μ, σ): \(\frac{1}{\sigma\sqrt{2\pi}} \exp(-(c-\mu)^2 / (2\sigma^2))\).
Uniform(a, b): 1/(b-a) for a<=c<=b, 0 otherwise.
Exponential(λ): λ·exp(-λc) for c>=0, 0 otherwise.
Erlang(k, λ) (integer k>=1): \(\frac{\lambda^k c^{k-1} e^{-\lambda c}}{(k-1)!}\) for c>=0, 0 otherwise.

Definition at line 21 of file AnalyticEvaluator.cpp.

◆ pow2_clamped()

double provsql::pow2_clamped ( size_t k )

static

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

Definition at line 881 of file probability_evaluate.cpp.

◆ runAggMarginalEvaluator()

unsigned provsql::runAggMarginalEvaluator ( GenericCircuit & gc )

Run the safe-join aggregate marginal-vector pre-pass over gc.

For every gate_cmp matching the hierarchical-join shape (see file docstring) over COUNT / SUM / MIN / MAX, computes the comparator's exact probability through the recursive hierarchical engine and replaces the cmp by a Bernoulli gate_input via GenericCircuit::resolveCmpToBernoulli. Leaves every other cmp untouched. COUNT / SUM use the count/weighted-sum distribution (block mixture + additive convolution); MIN / MAX reduce to a handful of "all of a value-thresholded subset absent" probabilities over the same hierarchical recursion.

Parameters

gc	Circuit to mutate in place.

Returns: Number of comparators resolved by this pass.

Definition at line 1093 of file AggMarginalEvaluator.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ runAnalyticEvaluator()

unsigned provsql::runAnalyticEvaluator ( GenericCircuit & gc )

Run the closed-form CDF resolution pass over gc.

For every gate_cmp in the circuit whose two sides match one of the supported shapes (see the header docstring), computes the comparator's probability analytically and replaces the cmp by a Bernoulli gate_input via GenericCircuit::resolveCmpToBernoulli.

Parameters

gc	Circuit to mutate in place.

Returns: Number of comparators resolved by this pass.

Definition at line 300 of file AnalyticEvaluator.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ runConstantFold()

unsigned provsql::runConstantFold ( GenericCircuit & gc )

Constant-fold pass over every gate_arith in gc.

Walks the circuit bottom-up and replaces any gate_arith whose children all evaluate to scalar constants with the equivalent gate_value (e.g. arith(NEG, value:2) becomes value:-2, arith(PLUS, value:1, value:2) becomes value:3).

Strictly a subset of runHybridSimplifier (only try_eval_constant fires; no family closures, identity drops, or mixture lifts), and therefore safe to run at load time alongside runRangeCheck and foldSemiringIdentities: the resulting gate_value gates carry no random identity, so no consumer's shared-RV coupling is broken by the rewrite. The family closures stay behind the separate hybrid_evaluation GUC because they replace a multi-leaf subtree with a fresh gate_rv UUID and would decouple shared base RVs that other parts of the circuit reference.

Lifts the -c::random_variable parser quirk (which builds an arith(NEG, value:c) gate rather than value:-c) into a clean gate_value before downstream consumers like collectRvConstraints / asRvVsConstCmp inspect the circuit.

Returns: Number of gates rewritten.

Definition at line 1285 of file HybridEvaluator.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ runCountCmpEvaluator()

unsigned provsql::runCountCmpEvaluator ( GenericCircuit & gc )

Run the Poisson-binomial pre-pass over gc.

For every gate_cmp whose shape matches the first-slice scope (see file docstring), computes the comparator's probability by Poisson-binomial CDF and replaces the cmp by a Bernoulli gate_input via GenericCircuit::resolveCmpToBernoulli.

Parameters

gc	Circuit to mutate in place.

Returns: Number of comparators resolved by this pass.

Definition at line 206 of file CountCmpEvaluator.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ runHavingAlwaysTrueRewriter()

unsigned provsql::runHavingAlwaysTrueRewriter ( GenericCircuit & gc )

Probability-side pre-pass: rewrite HAVING-style gate_cmp gates that are provably TRUE on the agg's value-interval into an OR over the agg's per-row K-gates.

Probability-side pre-pass that rewrites gate_cmp gates provably true on the agg's value-interval to a gate_plus over the agg's per-row K-gates.

Companion to runCountCmpEvaluator's Poisson-binomial pre-pass: where that one resolves COUNT op C to a closed-form Bernoulli, this one catches the always-true sub-case (e.g. COUNT <= K with K >= N inputs, or any aggregator whose value-interval entirely satisfies the predicate) and replaces the cmp with gate_plus over the agg's K-gates – the "group is non-empty" indicator.

Why a separate pass: runRangeCheck deliberately blocks TRUE decisions because gate_one is universally unsound for HAVING (it would credit the empty world). The safe TRUE rewrite "OR of K-gates" requires absorptive gate_plus semantics (probability, Boolean, formula, why, which, max-min, max-max), so the pass is restricted to the probability-evaluate path where absorption is guaranteed by the downstream BoolExpr translation.

Fires regardless of provsql.cmp_probability_evaluation: when the Poisson-binomial path is disabled (developer A/B testing), this lighter shortcut still catches the always-true case and spares the d-DNNF compiler the 2^N-clause DNF that provsql_having's enumerate_valid_worlds would otherwise emit.

Same matching contract as decideAggVsConstCmp for the agg side: cmp wires must be {gate_agg, scalar-const-encoded-as-semimod}, the agg's children must all be gate_semimod, and the agg kind must be one of COUNT / SUM / MIN / MAX (the only kinds with an interval). Mismatches leave the cmp untouched.

Parameters

gc	Circuit to mutate in place.

Returns: Number of comparators rewritten to gate_plus.

Catches the always-true HAVING case (e.g. COUNT <= K with K >= N) that runRangeCheck deliberately leaves alone (the universally-sound gate_one rewrite would credit the empty world). Sound only in absorptive semirings; restricted to the probability-evaluate path.

Returns: Number of comparators rewritten. See the implementation doc comment in RangeCheck.cpp for the full contract.

Definition at line 1115 of file RangeCheck.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ runHybridDecomposer()

unsigned provsql::runHybridDecomposer	(	GenericCircuit &	gc,
		unsigned	samples )

Marginalise unresolved continuous-island gate_cmp gates into Bernoulli gate_input leaves.

Runs after RangeCheck, the simplifier (runHybridSimplifier), and AnalyticEvaluator have done what they can. Picks up the residual comparators whose two sides are an entirely continuous island (subtree of gate_value, gate_rv, gate_arith with no Boolean structure underneath) but whose specific shape is not one the analytic CDF resolver handles – e.g. Normal + Uniform > 0, heterogeneous-rate sums of exponentials, or other compositions the simplifier could not fold to a bare distribution leaf.

Each qualifying comparator is marginalised by drawing samples worlds and applying the comparator scalar-by-scalar; the empirical probability replaces the gate_cmp via resolveCmpToBernoulli. The circuit downstream becomes purely Boolean, so the existing independent / tree-decomposition / compilation methods become available on circuits that would otherwise have to fall through to whole-circuit MC.

Singleton groups are marginalised into a single gate_input via GenericCircuit::resolveCmpToBernoulli.

Multi-cmp shared-island groups (k comparators sharing one or more base gate_rv leaves, detected via pairwise footprint overlap with union-find) are resolved by inlining a 2^k joint distribution table:

One anonymous gate_input acts as the block key.
One gate_mulinput per joint outcome with positive probability, all sharing the key, carries the joint mass (mutually-exclusive block).
Each comparator is rewritten as gate_plus over the mulinputs whose joint outcome word has the comparator's bit set. The downstream OR over the rewritten comparators thereby observes the dependent joint distribution: mulinputs across comparators dedup at OR sites in BooleanCircuit::independentEvaluationInternal (or are Bayesian-tree-rewritten by rewriteMultivaluedGates before tree-decomposition / monte-carlo / external compilers). Groups with k > JOINT_TABLE_K_MAX (currently 8, i.e. 256 outcomes) fall through to whole-circuit MC to keep the materialisation bounded.

Parameters

gc	Circuit to mutate in place.
samples	Number of MC iterations used per marginalisation. Callers typically pass `provsql_rv_mc_samples`.

Returns: Number of comparators resolved by this pass.

Definition at line 1807 of file HybridEvaluator.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ runHybridSimplifier()

unsigned provsql::runHybridSimplifier ( GenericCircuit & gc )

Run the peephole simplifier over gc.

Visits every gate in post-order and applies the closure rules described in the header comment until a fixed point is reached.

Parameters

gc	Circuit to mutate in place.

Returns: Number of gate rewrites performed by this pass.

Definition at line 1307 of file HybridEvaluator.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ runMinMaxCmpEvaluator()

unsigned provsql::runMinMaxCmpEvaluator ( GenericCircuit & gc )

Run the MIN / MAX closed-form pre-pass over gc.

For every gate_cmp whose shape matches a MIN(a)/MAX(a) op C HAVING predicate over independent private contributors, computes the comparator's probability in closed form and replaces the cmp by a Bernoulli gate_input via GenericCircuit::resolveCmpToBernoulli.

Parameters

gc	Circuit to mutate in place.

Returns: Number of comparators resolved by this pass.

Definition at line 102 of file MinMaxCmpEvaluator.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ runRangeCheck()

unsigned provsql::runRangeCheck ( GenericCircuit & gc )

Run the support-based pruning pass over gc.

For every gate_cmp in the circuit, computes the interval of (lhs - rhs) via interval arithmetic over gate_value, gate_rv, and gate_arith leaves; when the interval is provably above, below, or disjoint from zero, replaces the gate_cmp by a Bernoulli gate_input carrying the decided probability (0 or 1).

Comparators whose interval is inconclusive (overlaps zero) are left intact for downstream passes.

Iterates every gate (rather than walking from a specific root) so that a single sweep at getGenericCircuit time benefits every downstream consumer regardless of which sub-circuit they later traverse.

Parameters

gc	Circuit to mutate in place.

Returns: Number of comparators resolved by this pass.

Definition at line 871 of file RangeCheck.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ runSumCmpEvaluator()

unsigned provsql::runSumCmpEvaluator ( GenericCircuit & gc )

Run the weighted-sum DP pre-pass over gc.

For every gate_cmp whose shape matches a SUM(a) op C HAVING predicate over independent private contributors and whose reachable-sum range is within kMaxSumRange, computes the comparator's probability by the subset-sum DP and replaces the cmp by a Bernoulli gate_input via GenericCircuit::resolveCmpToBernoulli.

Parameters

gc	Circuit to mutate in place.

Returns: Number of comparators resolved by this pass.

Definition at line 43 of file SumCmpEvaluator.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ shape_mass()

std::optional< double > provsql::shape_mass	(	const ClosedFormShape &	s,
		double	lo,
		double	hi )

static

Unconditional probability mass of a shape over the interval [lo, hi].

TruncatedSingleRv arms supplied here must carry truncated == false (the unconditional shape); the helper uses the natural support to compute the CDF endpoints, so calling with an already-truncated input would double-truncate.

Recursive: a Bernoulli mixture's mass is the Bernoulli-weighted combination of its arms' masses. Categorical mass is the sum of outcome masses falling in the interval. Dirac mass is 1 iff the Dirac value sits in the interval, else 0. Returns std::nullopt when a leaf's spec defeats the closed-form CDF (e.g. non-integer Erlang shape – cdfAt returns NaN there).

Definition at line 1483 of file RangeCheck.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ toleranceAdmits()

bool provsql::toleranceAdmits	(	ToleranceKind	request,
		ToleranceKind	method )

static

Admissibility of a method's guarantee under a requested tolerance.

The paths nest Exact ⊂ Relative ⊂ Additive: a method is admissible iff its guarantee is at least as tight as the request (an exact method serves any path – "exact when cheaper"; a relative method serves relative & additive; an additive method serves only additive). This both widens the relative/additive portfolios to the approximate members AND keeps the exact path (which calls chooseAndRun with an Exact tolerance) from ever selecting an approximate method.

Definition at line 1648 of file probability_evaluate.cpp.

Here is the caller graph for this function:

◆ tool_registry()

ToolRegistry & provsql::tool_registry ( )

inline

Shorthand for ToolRegistry::instance().

Definition at line 224 of file ToolRegistry.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ truncateShape()

std::optional< ClosedFormShape > provsql::truncateShape	(	const ClosedFormShape &	s,
		double	lo,
		double	hi )

static

Conditional shape after truncating the underlying variable to [lo, hi].

Bare-RV arm: intersects its natural / current truncation with [lo, hi] and marks the result truncated so downstream shape_pdf renormalises by the truncated CDF. Dirac: keep iff value ∈ interval, otherwise nullopt (infeasible). Categorical: keep outcomes in interval, renormalise masses. Bernoulli mixture: recursively truncate each arm and reweight the Bernoulli by the ratio of arm masses (the standard \( \pi' = \pi Z_L / (\pi Z_L + (1-\pi) Z_R) \) update); a fully-eliminated arm degenerates to the surviving one. Returns nullopt when the truncated shape has zero mass (caller can raise infeasibility).

Definition at line 1529 of file RangeCheck.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ try_truncated_closed_form_sample()

std::optional< std::vector< double > > provsql::try_truncated_closed_form_sample	(	const GenericCircuit &	gc,
		gate_t	root,
		gate_t	event_root,
		unsigned	n )

Try to draw n exact samples from the conditional distribution of root given event_root via closed-form truncation, bypassing MC rejection.

Fires only when root is a bare gate_rv whose family admits a closed-form truncation (Uniform / Exponential / Normal) and collectRvConstraints can extract a sound interval from event_root. Other shapes (arith composites, mixtures, Erlang, un-extractable events) return std::nullopt so the caller can fall back to monteCarloConditionalScalarSamples.

Sampling kernels:

Uniform(a, b): collectRvConstraints already intersects with [a, b], so the draw is a plain U(lo, hi) on the intersected interval. 100% acceptance.
Exponential(λ), one-sided X > c: memorylessness yields c + Exp(λ). Two-sided lo < X < hi: inverse-CDF via std::log1p / std::expm1 for numerical accuracy near the support boundary.
Normal(μ, σ): inverse-CDF transform. Forward CDF uses std::erf (matching AnalyticEvaluator::cdfAt); inverse uses the Beasley-Springer-Moro rational approximation (~1e-7 accuracy, ample for sampling).

Empty / degenerate truncations (lo >= hi after intersection) also return std::nullopt so the caller's MC fallback can emit its usual "accepted 0" diagnostic.

The RNG is seeded from provsql.monte_carlo_seed identically to monteCarloScalarSamples, so a pinned seed gives reproducible output on either path.

Definition at line 620 of file MonteCarloSampler.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

◆ kCostCompilation

const double provsql::kCostCompilation = 2e-3

static

Definition at line 843 of file probability_evaluate.cpp.

◆ kCostCompilationFloor

const double provsql::kCostCompilationFloor = 40.0

static

Definition at line 844 of file probability_evaluate.cpp.

◆ kCostDnfShapeFeature

const double provsql::kCostDnfShapeFeature = 2e-6

static

Definition at line 845 of file probability_evaluate.cpp.

◆ kCostDTreeApprox

const double provsql::kCostDTreeApprox = 4e-4

static

Definition at line 866 of file probability_evaluate.cpp.

◆ kCostDTreeExact

const double provsql::kCostDTreeExact = 3e-4

static

Definition at line 865 of file probability_evaluate.cpp.

◆ kCostDTreeMsPerStepDnf

const double provsql::kCostDTreeMsPerStepDnf = 1.4e-3

static

Definition at line 876 of file probability_evaluate.cpp.

◆ kCostDTreeMsPerStepGeneral

const double provsql::kCostDTreeMsPerStepGeneral = 5e-4

static

Definition at line 877 of file probability_evaluate.cpp.

◆ kCostIndependent

const double provsql::kCostIndependent = 5e-5

static

Definition at line 829 of file probability_evaluate.cpp.

◆ kCostInversionFree

const double provsql::kCostInversionFree = 5e-5

static

Definition at line 830 of file probability_evaluate.cpp.

◆ kCostKarpLuby

const double provsql::kCostKarpLuby = 3e-6

static

Definition at line 864 of file probability_evaluate.cpp.

◆ kCostMonteCarlo

const double provsql::kCostMonteCarlo = 1e-5

static

Definition at line 862 of file probability_evaluate.cpp.

◆ kCostPossibleWorlds

const double provsql::kCostPossibleWorlds = 3e-6

static

Definition at line 831 of file probability_evaluate.cpp.

◆ kCostSieve

const double provsql::kCostSieve = 1e-5

static

Definition at line 832 of file probability_evaluate.cpp.

◆ kCostStoppingRule

const double provsql::kCostStoppingRule = 1e-3

static

Definition at line 863 of file probability_evaluate.cpp.

◆ kCostTreeDecomp

const double provsql::kCostTreeDecomp = 7e-4

static

Definition at line 837 of file probability_evaluate.cpp.

◆ kCostTwProxyFeature

const double provsql::kCostTwProxyFeature = 3e-4

static

Definition at line 846 of file probability_evaluate.cpp.

◆ kPossibleWorldsSanityMax

const size_t provsql::kPossibleWorldsSanityMax = 30

static

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

The by-name call ignores it (up to possibleWorlds' own 64 limit). The actual small-N-vs-compile crossover is a cost comparison, not this bound.

Definition at line 805 of file probability_evaluate.cpp.

◆ kSieveSanityMaxClauses

const size_t provsql::kSieveSanityMaxClauses = 24

static

Largest clause count for which the auto-chosen sieve (2^m inclusion-exclusion) is admitted (matches BooleanCircuit::sieve's internal cap).

The by-name call is unaffected.

Definition at line 810 of file probability_evaluate.cpp.

Classes

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

◆ ClosedFormShape

Enumeration Type Documentation

◆ DistKind

◆ Feature

◆ ToleranceKind

Function Documentation

◆ analytical_mean()

◆ analytical_raw_moment()

◆ analytical_variance()

◆ analyticalHistogram()

◆ cdfAt()

◆ circuitHasRV()

◆ circuitHasUnresolvedSampleableAgg()

◆ collectRvConstraints()

◆ compute_central_moment()

◆ compute_expectation()

◆ compute_raw_moment()

◆ compute_support()

◆ computeRefCounts()

◆ contributorProb()

◆ dtreeBounds() [1/2]

◆ dtreeBounds() [2/2]

◆ dtreeBoundsCircuit()

◆ evaluateBooleanProbability()

◆ eventIsProvablyInfeasible()

◆ expandCommandTemplate()

◆ extract_finite_double()

◆ extract_mulinput_value()

◆ kcmcp_compile()

◆ lift_conditioning()

◆ makeDDAuto()

◆ matchAggCmp()

◆ matchClosedFormDistribution()

◆ matchTruncatedSingleRv()

◆ monteCarloConditionalScalarSamples()

◆ monteCarloJointDistribution()

◆ monteCarloRV()

◆ monteCarloRVStopping()

◆ monteCarloScalarSamples()

◆ parse_distribution_spec()

◆ parseDoubleStrict()

◆ pdfAt()

◆ pow2_clamped()

◆ runAggMarginalEvaluator()

◆ runAnalyticEvaluator()

◆ runConstantFold()

◆ runCountCmpEvaluator()

◆ runHavingAlwaysTrueRewriter()

◆ runHybridDecomposer()

◆ runHybridSimplifier()

◆ runMinMaxCmpEvaluator()

◆ runRangeCheck()

◆ runSumCmpEvaluator()

◆ shape_mass()

◆ toleranceAdmits()

◆ tool_registry()

◆ truncateShape()

◆ try_truncated_closed_form_sample()

Variable Documentation

◆ kCostCompilation

◆ kCostCompilationFloor

◆ kCostDnfShapeFeature

◆ kCostDTreeApprox

◆ kCostDTreeExact

◆ kCostDTreeMsPerStepDnf

◆ kCostDTreeMsPerStepGeneral

◆ kCostIndependent

◆ kCostInversionFree

◆ kCostKarpLuby

◆ kCostMonteCarlo

◆ kCostPossibleWorlds

◆ kCostSieve

◆ kCostStoppingRule

◆ kCostTreeDecomp