ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
Loading...
Searching...
No Matches
RangeCheck.cpp
Go to the documentation of this file.
1/**
2 * @file RangeCheck.cpp
3 * @brief Implementation of the support-based bound check pass.
4 * See @c RangeCheck.h for the full docstring.
5 */
6#include "RangeCheck.h"
7
8#include <algorithm>
9#include <cmath>
10#include <limits>
11#include <stack>
12#include <unordered_map>
13#include <unordered_set>
14#include <vector>
15
16#include "Aggregation.h" // ComparisonOperator + cmpOpFromOid
17#include "AnalyticEvaluator.h" // cdfAt for shape_mass under truncation
18#include "CircuitFromMMap.h" // getGenericCircuit
19#include "Expectation.h" // lift_conditioning
20#include "RandomVariable.h" // parse_distribution_spec, DistKind
21#include "provsql_utils_cpp.h" // uuid2string
22
23#include <type_traits> // std::is_same_v in truncateShape
24#include <variant>
25extern "C" {
26#include "postgres.h"
27#include "fmgr.h"
28#include "funcapi.h" // get_call_result_type, BlessTupleDesc
29#include "access/htup_details.h" // heap_form_tuple (PG 10 declares it here;
30 // funcapi.h pulls it in transitively from
31 // PG 11 onwards, but not on 10)
32#include "utils/uuid.h"
33#include "provsql_utils.h" // gate_type, provsql_arith_op
34#include "provsql_error.h"
35
36PG_FUNCTION_INFO_V1(rv_support);
37}
38
39namespace provsql {
40
41namespace {
42
43/**
44 * @brief Closed interval @c [lo, hi] on the extended real line.
45 *
46 * @c -INFINITY / @c +INFINITY are used for unbounded ends (e.g. the
47 * support of a normal RV is @c {-INF, +INF}). Empty intervals are
48 * not generated by any constructor below; comparators against an
49 * empty interval would be vacuous and we consider them undecidable.
50 */
51struct Interval {
52 double lo;
53 double hi;
54
55 static Interval point(double v) { return {v, v}; }
56 static Interval all() { return {-std::numeric_limits<double>::infinity(),
57 +std::numeric_limits<double>::infinity()}; }
58 bool isAll() const {
59 return std::isinf(lo) && lo < 0 && std::isinf(hi) && hi > 0;
60 }
61};
62
63Interval add(Interval a, Interval b) { return {a.lo + b.lo, a.hi + b.hi}; }
64Interval sub(Interval a, Interval b) { return {a.lo - b.hi, a.hi - b.lo}; }
65Interval neg(Interval a) { return {-a.hi, -a.lo}; }
66
67/* Interval product: take the min/max of the four corner products.
68 * Handles signed bounds correctly (no special case for negative). */
69Interval mul(Interval a, Interval b)
70{
71 double p1 = a.lo * b.lo, p2 = a.lo * b.hi;
72 double p3 = a.hi * b.lo, p4 = a.hi * b.hi;
73 return {std::min({p1, p2, p3, p4}), std::max({p1, p2, p3, p4})};
74}
75
76/* Interval division: if the divisor straddles zero, the result is
77 * unbounded in both directions; otherwise compute via @c mul(a, 1/b).
78 * The conservative all-real fallback is correct (any real value is
79 * possible) but throws away precision &ndash; division by an interval
80 * crossing zero is rare in our tests. */
81Interval divInt(Interval a, Interval b)
82{
83 if (b.lo <= 0.0 && b.hi >= 0.0)
84 return Interval::all();
85 Interval inv = {1.0 / b.hi, 1.0 / b.lo};
86 return mul(a, inv);
87}
88
89/**
90 * @brief Recursively compute the interval of @p g's value across
91 * worlds. Memoised in @p cache.
92 *
93 * Recognised gate types:
94 * - @c gate_value: point interval on the parsed scalar.
95 * - @c gate_rv: distribution support (uniform exact, exponential
96 * on @c [0, +∞), normal on @c (-∞, +∞)).
97 * - @c gate_arith: propagated via the interval-arith helpers above.
98 *
99 * Anything else (e.g. an aggregate gate reached via a HAVING cmp)
100 * yields the all-real interval, which downstream conservatively
101 * treats as undecidable.
102 */
103Interval intervalOf(const GenericCircuit &gc, gate_t g,
104 std::unordered_map<gate_t, Interval> &cache)
105{
106 auto it = cache.find(g);
107 if (it != cache.end()) return it->second;
108
109 Interval result = Interval::all();
110 auto type = gc.getGateType(g);
111
112 switch (type) {
113 case gate_value:
114 /* A value RangeCheck cannot read as a double (e.g. a text constant
115 * from an agg_token = text comparison) carries no numeric interval
116 * constraint: leave it unconstrained rather than aborting the whole
117 * load-time pass. Mirrors the "undecidable -> all()" default. */
118 try {
119 result = Interval::point(parseDoubleStrict(gc.getExtra(g)));
120 } catch (const CircuitException &) {
121 result = Interval::all();
122 }
123 break;
124 case gate_rv: {
125 auto spec = parse_distribution_spec(gc.getExtra(g));
126 if (!spec) break;
127 switch (spec->kind) {
128 case DistKind::Normal:
129 /* Support is all of ℝ; Interval::all() is the default. */
130 break;
132 result = {spec->p1, spec->p2};
133 break;
135 case DistKind::Erlang:
136 result = {0.0, std::numeric_limits<double>::infinity()};
137 break;
138 }
139 break;
140 }
141 case gate_arith: {
142 auto op = static_cast<provsql_arith_op>(gc.getInfos(g).first);
143 const auto &wires = gc.getWires(g);
144 if (wires.empty()) break;
145 Interval first = intervalOf(gc, wires[0], cache);
146 switch (op) {
148 result = first;
149 for (std::size_t i = 1; i < wires.size(); ++i)
150 result = add(result, intervalOf(gc, wires[i], cache));
151 break;
153 result = first;
154 for (std::size_t i = 1; i < wires.size(); ++i)
155 result = mul(result, intervalOf(gc, wires[i], cache));
156 break;
158 if (wires.size() != 2) break;
159 result = sub(first, intervalOf(gc, wires[1], cache));
160 break;
162 if (wires.size() != 2) break;
163 result = divInt(first, intervalOf(gc, wires[1], cache));
164 break;
166 if (wires.size() != 1) break;
167 result = neg(first);
168 break;
169 }
170 break;
171 }
172 case gate_semimod: {
173 /* HAVING-style constant wrapper: semimod(gate_one, value). The
174 * semiring action of gate_one (always true) on a scalar leaves
175 * the scalar unchanged in every world, so the interval of the
176 * semimod equals the interval of its value child. Other
177 * semimod shapes (non-trivial k_gate) keep the conservative
178 * all-real default here; @c support_intervalOf widens it to
179 * a sampling-time support for rv_* callers. */
180 const auto &wires = gc.getWires(g);
181 if (wires.size() == 2 && gc.getGateType(wires[0]) == gate_one)
182 result = intervalOf(gc, wires[1], cache);
183 break;
184 }
185 case gate_mixture: {
186 /* Support of a mixture is the union of its branch supports.
187 * Two shapes:
188 * - Classic 3-wire [p_token, x_token, y_token]: the Bernoulli
189 * is a Boolean leaf and contributes nothing to the scalar
190 * interval.
191 * - Categorical N-wire [key, mul_1, ..., mul_n]: each mulinput
192 * carries its outcome value in extra; the support is the
193 * [min, max] of those values. */
194 const auto &wires = gc.getWires(g);
195 if (gc.isCategoricalMixture(g)) {
196 double lo = std::numeric_limits<double>::infinity();
197 double hi = -std::numeric_limits<double>::infinity();
198 bool any = false;
199 for (std::size_t i = 1; i < wires.size(); ++i) {
200 double v;
201 try { v = parseDoubleStrict(gc.getExtra(wires[i])); }
202 catch (const CircuitException &) { any = false; break; }
203 lo = std::min(lo, v);
204 hi = std::max(hi, v);
205 any = true;
206 }
207 if (any) result = {lo, hi};
208 } else if (wires.size() == 3) {
209 Interval ix = intervalOf(gc, wires[1], cache);
210 Interval iy = intervalOf(gc, wires[2], cache);
211 result = {std::min(ix.lo, iy.lo), std::max(ix.hi, iy.hi)};
212 }
213 break;
214 }
215 default:
216 /* gate_agg is intentionally not handled here -- the empty-subset
217 * NULL semantics make a flat interval misleading, so the
218 * runRangeCheck loop dispatches agg-bearing cmps to a separate
219 * decider that knows the asymmetry between sound FALSE and
220 * unsound TRUE decisions for SUM / MIN / MAX. All other gate
221 * types fall through to the all-real default. */
222 break;
223 }
224
225 cache[g] = result;
226 return result;
227}
228
229/**
230 * @brief Decide a @c gate_cmp from the interval of @c (lhs - rhs).
231 *
232 * Returns @c NaN when the comparator cannot be decided from interval
233 * bounds alone (e.g. the difference straddles zero, or the comparator
234 * is @c = / @c <> on overlapping continuous supports &ndash; both of
235 * which need a CDF, which a downstream analytic pass can supply).
236 * Otherwise returns the certain probability @c 0.0 or @c 1.0.
237 */
238double decideCmp(const Interval &diff, ComparisonOperator op)
239{
240 switch (op) {
242 if (diff.hi < 0.0) return 1.0;
243 if (diff.lo >= 0.0) return 0.0;
244 break;
246 if (diff.hi <= 0.0) return 1.0;
247 if (diff.lo > 0.0) return 0.0;
248 break;
250 if (diff.lo > 0.0) return 1.0;
251 if (diff.hi <= 0.0) return 0.0;
252 break;
254 if (diff.lo >= 0.0) return 1.0;
255 if (diff.hi < 0.0) return 0.0;
256 break;
258 /* Disjoint supports ⇒ certainly false. Overlapping supports of
259 * continuous RVs would have probability zero in the measure-
260 * theoretic sense, but the interval pass alone cannot tell
261 * whether either side is continuous; leave that to a downstream
262 * analytic-CDF pass when one is available. */
263 if (diff.hi < 0.0 || diff.lo > 0.0) return 0.0;
264 break;
266 if (diff.hi < 0.0 || diff.lo > 0.0) return 1.0;
267 break;
268 }
269 return std::numeric_limits<double>::quiet_NaN();
270}
271
272/**
273 * @brief Decide a @c gate_cmp where one side is a @c gate_agg, the
274 * other is a scalar constant.
275 *
276 * Computes a value-interval for the aggregate from its semimod
277 * children's per-row values, then folds the comparator like the
278 * non-agg path &ndash; but accepts only FALSE decisions, never
279 * TRUE. The reason is structural to ProvSQL's HAVING semantics:
280 * the per-aggregator subset enumerators in @c subset.cpp
281 * (@c count_enum, @c sum_dp, @c enumerate_exhaustive) all skip
282 * the empty subset, matching SQL's "no group, no HAVING" rule.
283 * So a HAVING cmp's value is the OR over the @em non-empty subsets
284 * where the predicate holds.
285 *
286 * - When no non-empty subset satisfies the predicate (the bound is
287 * strictly disjoint from the threshold on the right side of the
288 * comparator), the cmp value is exactly @c 0 = @c gate_zero.
289 * FALSE decision: sound.
290 * - When every non-empty subset satisfies the predicate, the cmp
291 * value equals "the group is non-empty" &ndash; the OR over the
292 * children's k_gates &ndash; which is a non-constant Boolean
293 * expression, @em not @c gate_one. Returning TRUE here would
294 * replace the cmp with @c gate_one and over-count probability
295 * mass from the empty world (where the group does not exist),
296 * so TRUE decisions are blocked uniformly across all aggregators.
297 *
298 * Aggregators we don't bound (@c AVG, @c AND, @c OR, @c CHOOSE,
299 * @c ARRAY_AGG, @c NONE) fall through to undecidable.
300 *
301 * @return @c 0.0 if decided to FALSE, @c NaN otherwise.
302 */
303double decideAggVsConstCmp(const GenericCircuit &gc, gate_t agg_gate,
304 ComparisonOperator op, double const_val,
305 bool agg_on_lhs,
306 bool *out_always_true = nullptr)
307{
308 AggregationOperator aop = getAggregationOperator(gc.getInfos(agg_gate).first);
309
310 /* Extract per-child scalar values from the semimod children. */
311 std::vector<double> values;
312 for (gate_t child : gc.getWires(agg_gate)) {
313 if (gc.getGateType(child) != gate_semimod)
314 return std::numeric_limits<double>::quiet_NaN();
315 const auto &sw = gc.getWires(child);
316 if (sw.size() != 2)
317 return std::numeric_limits<double>::quiet_NaN();
318 gate_t value_gate = sw[1];
319 if (gc.getGateType(value_gate) != gate_value)
320 return std::numeric_limits<double>::quiet_NaN();
321 try {
322 values.push_back(parseDoubleStrict(gc.getExtra(value_gate)));
323 } catch (const CircuitException &) {
324 return std::numeric_limits<double>::quiet_NaN();
325 }
326 }
327
328 Interval val_interval = Interval::all();
329
330 switch (aop) {
332 val_interval = {0.0, static_cast<double>(values.size())};
333 break;
335 double sum_neg = 0.0, sum_pos = 0.0;
336 for (double v : values) {
337 if (v < 0.0) sum_neg += v;
338 else sum_pos += v;
339 }
340 val_interval = {std::min(0.0, sum_neg), std::max(0.0, sum_pos)};
341 break;
342 }
345 if (values.empty())
346 return std::numeric_limits<double>::quiet_NaN();
347 val_interval = {*std::min_element(values.begin(), values.end()),
348 *std::max_element(values.begin(), values.end())};
349 break;
350 default:
351 /* AVG / AND / OR / CHOOSE / ARRAY_AGG / NONE: not decidable
352 * with this pass. */
353 return std::numeric_limits<double>::quiet_NaN();
354 }
355
356 Interval lhs = agg_on_lhs ? val_interval : Interval::point(const_val);
357 Interval rhs = agg_on_lhs ? Interval::point(const_val) : val_interval;
358 Interval diff = sub(lhs, rhs);
359 double p = decideCmp(diff, op);
360
361 /* Only FALSE decisions are universally sound (see doc comment).
362 * gate_one would over-credit the empty subset, which provsql_having
363 * deliberately excludes from valid worlds; the safe TRUE rewrite
364 * is "the group is non-empty" = OR over the agg's K-gates, and is
365 * sound only in absorptive semirings. The TRUE signal is therefore
366 * reported via @p out_always_true rather than the return value;
367 * the universal load-time @c runRangeCheck caller ignores it,
368 * while the probability-side @c runHavingAlwaysTrueRewriter caller
369 * acts on it. */
370 if (p == 0.0) return 0.0;
371 if (p == 1.0 && out_always_true != nullptr) *out_always_true = true;
372 return std::numeric_limits<double>::quiet_NaN();
373}
374
375/**
376 * @brief Try to extract a scalar constant from a cmp's child.
377 *
378 * Recognises two shapes:
379 * - bare @c gate_value: parse its @c extra as a double;
380 * - HAVING-style @c gate_semimod with @c k=gate_one and
381 * @c value=gate_value: parse the value's extra.
382 *
383 * Returns @c NaN on any other shape.
384 */
385double extractScalarConst(const GenericCircuit &gc, gate_t g)
386{
387 auto t = gc.getGateType(g);
388 if (t == gate_value) {
389 try { return parseDoubleStrict(gc.getExtra(g)); }
390 catch (const CircuitException &) {
391 return std::numeric_limits<double>::quiet_NaN();
392 }
393 }
394 if (t == gate_semimod) {
395 const auto &w = gc.getWires(g);
396 if (w.size() != 2) return std::numeric_limits<double>::quiet_NaN();
397 if (gc.getGateType(w[0]) != gate_one)
398 return std::numeric_limits<double>::quiet_NaN();
399 if (gc.getGateType(w[1]) != gate_value)
400 return std::numeric_limits<double>::quiet_NaN();
401 try { return parseDoubleStrict(gc.getExtra(w[1])); }
402 catch (const CircuitException &) {
403 return std::numeric_limits<double>::quiet_NaN();
404 }
405 }
406 return std::numeric_limits<double>::quiet_NaN();
407}
408
409/**
410 * @brief Flip the sides of a comparison operator.
411 *
412 * @c (a op b) is equivalent to @c (b flip(op) a). Used to normalise
413 * a cmp so the random-variable side is always on the left.
414 */
416{
417 switch (op) {
424 }
425 return op;
426}
427
428/**
429 * @brief Interpret a @c gate_cmp as a per-RV constraint @c rv op c.
430 *
431 * Returns @c true and fills @p rv_out, @p op_out, @p const_out when
432 * exactly one side of the cmp is a @c gate_rv and the other a
433 * @c gate_value with a parseable scalar; @c false otherwise (both
434 * sides are RVs, both constants, an @c arith subtree appears, etc.).
435 *
436 * Strict-vs-non-strict inequalities are preserved as the operator;
437 * the caller decides whether to treat the boundary as inclusive
438 * (continuous distributions: measure-zero, irrelevant for
439 * feasibility verdicts).
440 */
441bool asRvVsConstCmp(const GenericCircuit &gc, gate_t cmp_gate,
442 gate_t &rv_out, ComparisonOperator &op_out,
443 double &const_out)
444{
445 bool ok = false;
446 ComparisonOperator op = cmpOpFromOid(gc.getInfos(cmp_gate).first, ok);
447 if (!ok) return false;
448 const auto &wires = gc.getWires(cmp_gate);
449 if (wires.size() != 2) return false;
450
451 /* Recognise scalar-vs-constant cmps where the scalar side is a
452 * bare gate_rv (the original use case for the per-cmp resolution
453 * pass) or a gate_mixture (so the conditioning walker can extract
454 * intervals on mixture / categorical variables – value-vs-value
455 * cmps are folded upstream by RangeCheck before they reach this
456 * walker). Dirac (gate_value) is never the scalar side of a
457 * non-trivial cmp at this point; the value-vs-value pair would have
458 * been resolved upstream. */
459 auto isScalarRv = [](gate_type t) {
460 return t == gate_rv || t == gate_mixture;
461 };
462 auto t0 = gc.getGateType(wires[0]);
463 auto t1 = gc.getGateType(wires[1]);
464 if (isScalarRv(t0) && t1 == gate_value) {
465 try { const_out = parseDoubleStrict(gc.getExtra(wires[1])); }
466 catch (const CircuitException &) { return false; }
467 rv_out = wires[0];
468 op_out = op;
469 return true;
470 }
471 if (t0 == gate_value && isScalarRv(t1)) {
472 try { const_out = parseDoubleStrict(gc.getExtra(wires[0])); }
473 catch (const CircuitException &) { return false; }
474 rv_out = wires[1];
475 op_out = flipCmpOp(op);
476 return true;
477 }
478 return false;
479}
480
481/**
482 * @brief Apply a single @c rv-op-constant constraint to a running
483 * interval for the RV.
484 *
485 * Strict vs non-strict inequalities collapse onto the same closed
486 * interval: continuous distributions assign zero mass to the
487 * boundary, so the joint-feasibility verdict is unchanged whether
488 * we use @c < or @c <=. @c <> (NE) cannot be represented as a
489 * single interval and is left to the per-cmp pass.
490 */
491Interval intersectRvConstraint(Interval current, ComparisonOperator op,
492 double c)
493{
494 switch (op) {
497 current.hi = std::min(current.hi, c);
498 break;
501 current.lo = std::max(current.lo, c);
502 break;
504 current.lo = std::max(current.lo, c);
505 current.hi = std::min(current.hi, c);
506 break;
508 /* Cannot represent the complement of a point as a single
509 * interval; leave the running interval unchanged. */
510 break;
511 }
512 return current;
513}
514
515bool intervalEmpty(Interval i) { return i.lo > i.hi; }
516
517/**
518 * @brief Walk an AND-conjunct tree collecting per-RV interval
519 * constraints from its @c gate_cmp leaves.
520 *
521 * Shared between @c isAndJointlyInfeasible (which checks for an empty
522 * intersection) and the public @c collectRvConstraints / conditional
523 * @c compute_support paths. Descends through @c gate_times,
524 * collecting every @c gate_cmp interpretable as `rv op const` and
525 * intersecting its constraint into a running interval for that RV.
526 *
527 * @p complete is set to @c true on entry and cleared if the walk
528 * encounters any structure other than the AND-friendly set
529 * (@c gate_times, @c gate_cmp, @c gate_input, @c gate_one,
530 * @c gate_zero) whose footprint *might* constrain an RV
531 * (i.e. excluding bare Bernoulli factors). Callers that need a
532 * tight bound (the closed-form moment shortcut) must check it; the
533 * support intersection caller can use the result unconditionally
534 * because dropping a disjunctive factor only loosens the interval,
535 * which is sound for a superset bound on the conditional support.
536 *
537 * Cmps that do not interpret as `rv op const` (RV vs RV, arith on
538 * either side, agg…) are silently ignored; they belong to the
539 * conditioning event but don't constrain a single RV's interval.
540 */
541void walkAndConjunctIntervals(
542 const GenericCircuit &gc, gate_t root,
543 std::unordered_map<gate_t, Interval> &rv_intervals,
544 std::unordered_map<gate_t, Interval> &support_cache,
545 bool &complete)
546{
547 std::unordered_set<gate_t> seen;
548 std::stack<gate_t> stk;
549 stk.push(root);
550 complete = true;
551
552 while (!stk.empty()) {
553 gate_t g = stk.top(); stk.pop();
554 if (!seen.insert(g).second) continue;
555
556 auto t = gc.getGateType(g);
557 if (t == gate_cmp) {
558 gate_t rv = static_cast<gate_t>(0);
560 double c = 0.0;
561 if (!asRvVsConstCmp(gc, g, rv, op, c)) {
562 /* Cmp shape we don't interpret (RV vs RV, arith involved).
563 * Conservatively mark the walk incomplete: this cmp belongs
564 * to the event AND could constrain an RV in a way we can't
565 * fold into a single interval. */
566 complete = false;
567 continue;
568 }
569 auto it = rv_intervals.find(rv);
570 Interval current = (it == rv_intervals.end())
571 ? intervalOf(gc, rv, support_cache)
572 : it->second;
573 current = intersectRvConstraint(current, op, c);
574 rv_intervals[rv] = current;
575 continue; /* never descend into a cmp's operands */
576 }
577 if (t == gate_times || t == gate_delta || g == root) {
578 /* gate_delta wraps a single child as the δ-semiring identity on
579 * Booleans, so the AND-conjunct walker is sound to descend
580 * through it -- the wrapper carries no constraint of its own.
581 * Skipping the descent would mark the walk incomplete and force
582 * the moment caller to fall back to MC even when the inner
583 * cmps are decidable closed-form. */
584 for (gate_t c : gc.getWires(g)) stk.push(c);
585 continue;
586 }
587 if (t == gate_input || t == gate_update || t == gate_one ||
588 t == gate_zero) {
589 /* Bernoulli leaf / constants: shift P(event), don't truncate
590 * any continuous RV. Skipping is sound and the walk stays
591 * complete. */
592 continue;
593 }
594 /* gate_plus (OR), gate_monus (set diff), gate_arith, gate_rv, ...:
595 * could affect an RV's conditional distribution in ways that
596 * don't reduce to an interval intersection. Mark the walk
597 * incomplete so a moment closed-form caller falls through to MC. */
598 complete = false;
599 }
600}
601
602/**
603 * @brief Walk @p root's AND-conjunct cmps and decide whether the
604 * conjunction is jointly infeasible by per-RV interval
605 * intersection.
606 *
607 * For every @c gate_cmp reachable through a chain of @c gate_times
608 * starting at @p root, that is interpretable as @c rv-op-constant,
609 * intersect the constraint with the running interval for that RV
610 * (initialised to the RV's distribution support). As soon as any
611 * RV's interval becomes empty, the AND is infeasible.
612 *
613 * Descends only through @c gate_times: @c gate_plus is OR (the
614 * disjuncts could individually be feasible even when each is a
615 * narrow constraint on the RV, so they do not contribute to the
616 * conjunction's infeasibility), @c gate_monus is set difference
617 * (likewise), and other gate types break the AND chain.
618 *
619 * Cmps that this pass cannot interpret (RV vs RV, arith on either
620 * side, agg…) are simply ignored: skipping them is sound &ndash; we
621 * just have fewer constraints, so we never falsely declare
622 * infeasibility we cannot prove.
623 */
624bool isAndJointlyInfeasible(const GenericCircuit &gc, gate_t root)
625{
626 std::unordered_map<gate_t, Interval> rv_intervals;
627 std::unordered_map<gate_t, Interval> support_cache;
628 bool complete;
629 walkAndConjunctIntervals(gc, root, rv_intervals, support_cache, complete);
630 for (const auto &kv : rv_intervals) {
631 if (intervalEmpty(kv.second)) return true;
632 }
633 return false;
634}
635
636/**
637 * @brief Memoised recursive predicate: does @p g's sub-circuit
638 * produce a continuous random variable (no point-mass /
639 * Dirac component)?
640 *
641 * Used to widen the EQ / NE = 0 / 1 shortcut at the cmp resolution
642 * site below the bare-@c gate_rv test, so multi-gate composites like
643 * <tt>Exp(0.4) + Exp(0.3) = c</tt> (heterogeneous-rate exponential
644 * sum, no closed-form Erlang fold) or
645 * <tt>mixture(p, Normal, Uniform) = c</tt> (Bernoulli mixture over
646 * two continuous arms) also resolve at load time. Without this the
647 * cmp falls through to AnalyticEvaluator (which returns NaN for
648 * EQ / NE) and then to the MC marginalisation, which in finite
649 * precision estimates @c P(X = Y) at 0 anyway -- but costs
650 * @c provsql.rv_mc_samples iterations to do so.
651 *
652 * Recursion:
653 * - @c gate_rv -> true (Normal / Uniform / Exp / Erlang all have
654 * continuous densities, no point masses).
655 * - @c gate_value -> false (Dirac at the literal).
656 * - @c gate_arith -> true iff every wire has only-continuous
657 * support. Sums, products, negations, divisions of continuous
658 * RVs stay continuous in distribution; a @c gate_value sibling
659 * poisons the result (e.g. @c X + 2 is continuous, but
660 * @c X * 0 = 0 has a Dirac at zero -- handled by the existing
661 * constant-fold pre-pass, but defensive here).
662 * - @c gate_mixture, Bernoulli 3-wire <tt>[p, X, Y]</tt> -> true
663 * iff X and Y are both continuous; the Boolean @c p only chooses
664 * an arm, so it does not affect the support type.
665 * - @c gate_mixture, categorical
666 * <tt>[key, mul_1, ..., mul_n]</tt> -> false (point masses at
667 * each mulinput's outcome value).
668 * - Any other gate type -> false (defensive: gate_plus / gate_times
669 * / gate_cmp / gate_agg are not continuous-RV containers).
670 *
671 * The cache is keyed on @c gate_t and may be shared across multiple
672 * cmp gates inside a single @c runRangeCheck invocation.
673 */
674bool hasOnlyContinuousSupport(const GenericCircuit &gc, gate_t g,
675 std::unordered_map<gate_t, bool> &cache)
676{
677 auto it = cache.find(g);
678 if (it != cache.end()) return it->second;
679 /* Memoise pessimistically before recursing so a malformed cyclic
680 * sub-circuit (shouldn't happen on well-formed input) returns
681 * @c false rather than blowing the stack. */
682 cache[g] = false;
683
684 bool result = false;
685 auto t = gc.getGateType(g);
686 switch (t) {
687 case gate_rv:
688 result = true;
689 break;
690 case gate_value:
691 result = false;
692 break;
693 case gate_arith: {
694 result = true;
695 for (gate_t w : gc.getWires(g)) {
696 if (!hasOnlyContinuousSupport(gc, w, cache)) { result = false; break; }
697 }
698 break;
699 }
700 case gate_mixture: {
701 if (gc.isCategoricalMixture(g)) { result = false; break; }
702 const auto &w = gc.getWires(g);
703 if (w.size() != 3) { result = false; break; }
704 result = hasOnlyContinuousSupport(gc, w[1], cache)
705 && hasOnlyContinuousSupport(gc, w[2], cache);
706 break;
707 }
708 default:
709 result = false;
710 break;
711 }
712
713 cache[g] = result;
714 return result;
715}
716
717/**
718 * @brief Recursive collection of the @c gate_rv and @c gate_input
719 * leaves reachable from @p g.
720 *
721 * The result is a sub-circuit's "random-source footprint": two
722 * sub-circuits are independent iff their random-source sets are
723 * disjoint. Used to gate the exact-EQ Dirac sum-product below: the
724 * factoring @c P(X = Y) = Σ_v @c P(X=v)·P(Y=v) is only valid when
725 * @c X and @c Y are independent, otherwise the per-row coupling
726 * (e.g. two mixtures sharing a Bernoulli @c p_token) breaks the
727 * factoring and the sum-product silently produces the wrong
728 * probability.
729 *
730 * Descent rules: @c gate_arith and @c gate_mixture descend into all
731 * children (Bernoulli @c p_token, categorical key, mulinputs all
732 * contribute to the random footprint). @c gate_value is a
733 * deterministic literal and contributes no random source. Other
734 * gate types (Boolean / agg / etc.) don't appear under a continuous
735 * cmp side in well-formed circuits; defensively, they contribute
736 * nothing.
737 */
738const std::unordered_set<gate_t> &
739collectRandomLeaves(const GenericCircuit &gc, gate_t g,
740 std::unordered_map<gate_t, std::unordered_set<gate_t>> &cache)
741{
742 auto it = cache.find(g);
743 if (it != cache.end()) return it->second;
744 /* Insert an empty entry first so a recursive call on a cyclic
745 * sub-circuit returns early. std::unordered_map insertion does
746 * not invalidate references to existing elements, but it MAY
747 * rehash on growth (invalidating ALL references, including the
748 * one we're about to capture). Build the result locally, then
749 * write it back in one shot at the end. */
750 cache.emplace(g, std::unordered_set<gate_t>{});
751
752 std::unordered_set<gate_t> out;
753 auto t = gc.getGateType(g);
754 if (t == gate_rv || t == gate_input) {
755 out.insert(g);
756 } else if (t == gate_arith || t == gate_mixture) {
757 for (gate_t w : gc.getWires(g)) {
758 const auto &child = collectRandomLeaves(gc, w, cache);
759 out.insert(child.begin(), child.end());
760 }
761 }
762
763 /* Overwrite the placeholder; locate by find() to avoid a fresh
764 * insertion that could rehash and invalidate other iterators in
765 * upstream frames. */
766 auto fit = cache.find(g);
767 fit->second = std::move(out);
768 return fit->second;
769}
770
771using DiracMap = std::unordered_map<double, double>;
772using DiracMapOpt = std::optional<DiracMap>;
773
774/**
775 * @brief Recursive extraction of @p g's Dirac mass map (value -> mass).
776 *
777 * Returns @c std::nullopt when the sub-circuit's discrete component
778 * is not statically extractable (e.g. an opaque @c gate_arith over
779 * mixtures, a Bernoulli mixture whose @c p_token is a compound
780 * Boolean, etc.). When the sub-circuit is purely continuous the
781 * map is well-defined but empty (no Diracs, no masses).
782 *
783 * Used by the exact EQ shortcut below: for independent @c X, @c Y
784 * with extractable mass maps @c M_X, @c M_Y:
785 * <tt>P(X = Y) = Σ_{v ∈ M_X ∩ M_Y} M_X[v] · M_Y[v]</tt>. Continuous
786 * components contribute zero by measure-zero arguments (Dirac vs
787 * continuous and continuous vs continuous), so they need not appear
788 * in the sum.
789 *
790 * Shape rules:
791 * - @c gate_value:v: a Dirac at the literal with mass @c 1.
792 * - @c gate_rv: continuous in every supported family, empty map.
793 * - categorical @c gate_mixture <tt>[key, mul_1, ..., mul_n]</tt>:
794 * sum @c getProb(mul_i) into @c map[parseDouble(extra(mul_i))].
795 * Multiple mulinputs at the same outcome (which the constructor
796 * doesn't produce but is sound to handle) merge masses.
797 * - Bernoulli @c gate_mixture <tt>[p_token, X, Y]</tt> with
798 * @c p_token a bare @c gate_input: pull @c π = @c getProb(p_token)
799 * and recurse into X, Y to get @c M_X, @c M_Y; result is
800 * <tt>π·M_X[v] + (1-π)·M_Y[v]</tt> per outcome value. Compound
801 * Boolean @c p_tokens (whose probability would have to come from
802 * a recursive @c probability_evaluate call) bail.
803 * - Anything else: @c std::nullopt.
804 */
805DiracMapOpt
806collectDiracMassMap(const GenericCircuit &gc, gate_t g,
807 std::unordered_map<gate_t, DiracMapOpt> &cache)
808{
809 auto it = cache.find(g);
810 if (it != cache.end()) return it->second;
811 /* Pessimistic cycle guard, same reasoning as @c collectRandomLeaves. */
812 cache.emplace(g, std::nullopt);
813
814 DiracMapOpt result;
815 auto t = gc.getGateType(g);
816 switch (t) {
817 case gate_value: {
818 try {
819 DiracMap m;
820 m[parseDoubleStrict(gc.getExtra(g))] = 1.0;
821 result = std::move(m);
822 } catch (const CircuitException &) {
823 /* unparseable extra: bail */
824 }
825 break;
826 }
827 case gate_rv:
828 result = DiracMap{}; /* continuous, no point masses */
829 break;
830 case gate_mixture: {
831 const auto &w = gc.getWires(g);
832 if (gc.isCategoricalMixture(g)) {
833 DiracMap m;
834 bool ok = true;
835 for (std::size_t i = 1; i < w.size(); ++i) {
836 double v;
837 try { v = parseDoubleStrict(gc.getExtra(w[i])); }
838 catch (const CircuitException &) { ok = false; break; }
839 const double p = gc.getProb(w[i]);
840 if (!std::isfinite(p) || p < 0.0 || p > 1.0) { ok = false; break; }
841 m[v] += p;
842 }
843 if (ok) result = std::move(m);
844 } else if (w.size() == 3
845 && gc.getGateType(w[0]) == gate_input) {
846 const double pi = gc.getProb(w[0]);
847 if (std::isfinite(pi) && pi >= 0.0 && pi <= 1.0) {
848 auto mx = collectDiracMassMap(gc, w[1], cache);
849 auto my = collectDiracMassMap(gc, w[2], cache);
850 if (mx && my) {
851 DiracMap m;
852 for (const auto &[v, mass] : *mx) m[v] += pi * mass;
853 for (const auto &[v, mass] : *my) m[v] += (1.0 - pi) * mass;
854 result = std::move(m);
855 }
856 }
857 }
858 break;
859 }
860 default:
861 break;
862 }
863
864 auto fit = cache.find(g);
865 fit->second = result;
866 return result;
867}
868
869} // namespace
870
872{
873 std::unordered_map<gate_t, Interval> cache;
874 /* Shared across all cmp gates in this @c runRangeCheck invocation.
875 * Keyed on gate_t and immutable across cmp iterations because
876 * resolving one cmp only changes the cmp's own gate type, not
877 * the sub-circuit underneath @c wires[0..1] of other cmps. */
878 std::unordered_map<gate_t, bool> continuous_support_cache;
879 std::unordered_map<gate_t, DiracMapOpt> dirac_cache;
880 std::unordered_map<gate_t, std::unordered_set<gate_t>> leaf_cache;
881 unsigned resolved = 0;
882
883 /* Snapshot the cmp gate ids before we start mutating: in-place
884 * resolution turns a @c gate_cmp into a @c gate_input, but
885 * @c getNbGates only grows, never shrinks, so iterating by index
886 * over the original count is safe. We re-check the type at each
887 * step to skip already-resolved slots. */
888 const auto nb = gc.getNbGates();
889 std::vector<gate_t> cmps;
890 for (std::size_t i = 0; i < nb; ++i) {
891 auto g = static_cast<gate_t>(i);
892 if (gc.getGateType(g) == gate_cmp)
893 cmps.push_back(g);
894 }
895
896 for (gate_t c : cmps) {
897 if (gc.getGateType(c) != gate_cmp) continue; /* defensive */
898
899 bool ok = false;
900 ComparisonOperator op = cmpOpFromOid(gc.getInfos(c).first, ok);
901 if (!ok) continue;
902
903 const auto &wires = gc.getWires(c);
904 if (wires.size() != 2) continue;
905
906 /* Identity shortcut: when both sides of the cmp are the same
907 * gate (same UUID), the sampler's per-iteration memoisation
908 * guarantees both reads return identical values, so the
909 * comparator collapses to a constant. Universal across gate
910 * types and semirings; runs first so neither the continuous
911 * EQ/NE shortcut nor the interval-based path needs an explicit
912 * @c lhs != rhs guard. */
913 if (wires[0] == wires[1]) {
914 double p = std::numeric_limits<double>::quiet_NaN();
915 switch (op) {
919 p = 1.0; break;
923 p = 0.0; break;
924 }
925 gc.resolveCmpToBernoulli(c, p);
926 ++resolved;
927 continue;
928 }
929
930 /* Continuous EQ / NE shortcut: P(X = c) = 0 and P(X != c) = 1
931 * exactly when at least one side has a continuous distribution
932 * (point equality has measure zero under any continuous
933 * distribution). Universal across semirings: the gate_zero /
934 * gate_one rewrite is meaningful in every semiring (not just
935 * probability), so the resolution belongs here rather than in
936 * AnalyticEvaluator.
937 *
938 * @c hasOnlyContinuousSupport widens the test beyond a bare
939 * @c gate_rv leaf: heterogeneous-rate exponential sums, products
940 * of independent continuous RVs, and Bernoulli mixtures over
941 * two continuous arms all qualify because their distribution
942 * has no point-mass component. Categorical mixtures (point
943 * masses at each outcome value) and pure-deterministic
944 * @c gate_value sub-circuits do NOT qualify and fall through to
945 * the agg / interval / AnalyticEvaluator paths.
946 *
947 * The @c wires[0] == @c wires[1] case is already handled by the
948 * identity shortcut above. */
949 if (op == ComparisonOperator::EQ ||
951 bool lhs_continuous = hasOnlyContinuousSupport(gc, wires[0],
952 continuous_support_cache);
953 bool rhs_continuous = hasOnlyContinuousSupport(gc, wires[1],
954 continuous_support_cache);
955 if (lhs_continuous || rhs_continuous) {
956 double p = (op == ComparisonOperator::EQ) ? 0.0 : 1.0;
957 gc.resolveCmpToBernoulli(c, p);
958 ++resolved;
959 continue;
960 }
961
962 /* Exact Dirac sum-product. When both sides have extractable
963 * @c (value -> mass) maps AND the two sub-circuits are
964 * independent (random-leaf footprints disjoint), the
965 * convolution at zero of @c (X - Y) has support exactly on
966 * @c Dirac(X) ∩ Dirac(Y) with mass
967 * <tt>M_X(v) · M_Y(v)</tt> per overlapping value; the
968 * continuous and continuous-vs-Dirac contributions vanish by
969 * measure zero. This generalises the bare-disjoint case to
970 * any pair of statically-known discrete distributions:
971 * <tt>P(categorical(a) = categorical(b))</tt> with overlapping
972 * outcomes, mixtures with @c as_random branches, etc.
973 *
974 * The independence test is essential: two mixtures sharing a
975 * Bernoulli @c p_token are correlated and the sum-product
976 * factoring breaks (the actual @c P(X=Y) cannot be recovered
977 * from the marginals alone). @c collectRandomLeaves'
978 * footprint-disjoint check is the gate.
979 *
980 * When both maps are empty (purely continuous on both sides)
981 * the existing branch above already fired, so the sum-product
982 * path here only runs for at-least-one-discrete shapes. */
983 auto m_l = collectDiracMassMap(gc, wires[0], dirac_cache);
984 auto m_r = collectDiracMassMap(gc, wires[1], dirac_cache);
985 if (m_l && m_r) {
986 const auto &leaves_l = collectRandomLeaves(gc, wires[0], leaf_cache);
987 const auto &leaves_r = collectRandomLeaves(gc, wires[1], leaf_cache);
988 bool independent = true;
989 for (gate_t leaf : leaves_l) {
990 if (leaves_r.count(leaf)) { independent = false; break; }
991 }
992 if (independent) {
993 double p_eq = 0.0;
994 /* Iterate over the smaller map to keep the sum at
995 * O(min(|M_l|, |M_r|)) lookups. */
996 const DiracMap *small = (m_l->size() <= m_r->size()) ? &*m_l : &*m_r;
997 const DiracMap *large = (m_l->size() <= m_r->size()) ? &*m_r : &*m_l;
998 for (const auto &[v, mass] : *small) {
999 auto fit = large->find(v);
1000 if (fit != large->end()) p_eq += mass * fit->second;
1001 }
1002 /* Clamp into @c [0, 1] defensively: floating-point summation
1003 * of masses (each in [0, 1]) might overshoot by an ULP, and
1004 * @c resolveCmpToBernoulli requires a strict probability. */
1005 if (p_eq < 0.0) p_eq = 0.0;
1006 if (p_eq > 1.0) p_eq = 1.0;
1007 double p = (op == ComparisonOperator::EQ) ? p_eq : 1.0 - p_eq;
1008 gc.resolveCmpToBernoulli(c, p);
1009 ++resolved;
1010 continue;
1011 }
1012 }
1013 }
1014
1015 /* HAVING-style cmp: agg on one side, scalar constant on the
1016 * other. Decide via the agg-aware path which is cheaper than
1017 * intervalOf + decideCmp and which knows the empty-subset NULL
1018 * semantics for SUM / MIN / MAX (see decideAggVsConstCmp). */
1019 bool lhs_is_agg = gc.getGateType(wires[0]) == gate_agg;
1020 bool rhs_is_agg = gc.getGateType(wires[1]) == gate_agg;
1021 if (lhs_is_agg != rhs_is_agg) {
1022 gate_t agg_side = lhs_is_agg ? wires[0] : wires[1];
1023 gate_t const_side = lhs_is_agg ? wires[1] : wires[0];
1024 double const_val = extractScalarConst(gc, const_side);
1025 if (!std::isnan(const_val)) {
1026 double p = decideAggVsConstCmp(gc, agg_side, op, const_val,
1027 lhs_is_agg);
1028 if (!std::isnan(p)) {
1029 gc.resolveCmpToBernoulli(c, p);
1030 ++resolved;
1031 continue;
1032 }
1033 }
1034 }
1035
1036 /* Interval-based path for non-agg cmps (RV, gate_arith, value). */
1037 Interval lhs = intervalOf(gc, wires[0], cache);
1038 Interval rhs = intervalOf(gc, wires[1], cache);
1039 /* Skip if both sides are unbounded; @c decideCmp would never
1040 * return a decision and the work is wasted. */
1041 if (lhs.isAll() && rhs.isAll()) continue;
1042
1043 Interval diff = sub(lhs, rhs);
1044 double p = decideCmp(diff, op);
1045 if (!std::isnan(p)) {
1046 gc.resolveCmpToBernoulli(c, p);
1047 ++resolved;
1048 }
1049 }
1050
1051 /* Joint-conjunction pass: walk every @c gate_times and check
1052 * whether its AND-conjunct cmps, viewed together, constrain some
1053 * shared RV to an empty interval. Catches the joint-infeasibility
1054 * case the per-cmp pass above cannot see (each cmp individually
1055 * leaves a non-empty range, but their intersection is empty).
1056 *
1057 * Snapshot the gate_times indices first: @c resolveGateToZero
1058 * mutates the type, so iterating the live vector while resolving
1059 * would skip slots. The post-snapshot type re-check guards against
1060 * a @c gate_times that the per-cmp pass somehow already collapsed
1061 * (currently not possible, but cheap insurance for future passes). */
1062 const auto nb_after = gc.getNbGates();
1063 std::vector<gate_t> times_gates;
1064 for (std::size_t i = 0; i < nb_after; ++i) {
1065 auto g = static_cast<gate_t>(i);
1066 if (gc.getGateType(g) == gate_times)
1067 times_gates.push_back(g);
1068 }
1069 for (gate_t t : times_gates) {
1070 if (gc.getGateType(t) != gate_times) continue; /* defensive */
1071 if (isAndJointlyInfeasible(gc, t)) {
1072 gc.resolveGateToZero(t);
1073 ++resolved;
1074 }
1075 }
1076
1077 return resolved;
1078}
1079
1080/**
1081 * @brief Probability-side pre-pass: rewrite HAVING-style @c gate_cmp
1082 * gates that are provably TRUE on the agg's value-interval
1083 * into an OR over the agg's per-row K-gates.
1084 *
1085 * Companion to @c runCountCmpEvaluator's Poisson-binomial pre-pass:
1086 * where that one resolves @c COUNT op C to a closed-form Bernoulli,
1087 * this one catches the always-true sub-case (e.g. @c COUNT <= K with
1088 * @c K >= N inputs, or any aggregator whose value-interval entirely
1089 * satisfies the predicate) and replaces the cmp with @c gate_plus
1090 * over the agg's K-gates -- the "group is non-empty" indicator.
1091 *
1092 * Why a separate pass: @c runRangeCheck deliberately blocks TRUE
1093 * decisions because @c gate_one is universally unsound for HAVING
1094 * (it would credit the empty world). The safe TRUE rewrite
1095 * "OR of K-gates" requires absorptive @c gate_plus semantics
1096 * (probability, Boolean, formula, why, which, max-min, max-max), so
1097 * the pass is restricted to the probability-evaluate path where
1098 * absorption is guaranteed by the downstream BoolExpr translation.
1099 *
1100 * Fires regardless of @c provsql.cmp_probability_evaluation: when
1101 * the Poisson-binomial path is disabled (developer A/B testing),
1102 * this lighter shortcut still catches the always-true case and
1103 * spares the d-DNNF compiler the 2^N-clause DNF that
1104 * @c provsql_having's @c enumerate_valid_worlds would otherwise emit.
1105 *
1106 * Same matching contract as @c decideAggVsConstCmp for the agg side:
1107 * cmp wires must be {gate_agg, scalar-const-encoded-as-semimod}, the
1108 * agg's children must all be @c gate_semimod, and the agg kind must
1109 * be one of COUNT / SUM / MIN / MAX (the only kinds with an
1110 * interval). Mismatches leave the cmp untouched.
1111 *
1112 * @param gc Circuit to mutate in place.
1113 * @return Number of comparators rewritten to gate_plus.
1114 */
1116{
1117 unsigned resolved = 0;
1118 const auto nb = gc.getNbGates();
1119
1120 std::vector<gate_t> cmps;
1121 cmps.reserve(nb / 8); /* rough guess */
1122 for (std::size_t i = 0; i < nb; ++i) {
1123 auto g = static_cast<gate_t>(i);
1124 if (gc.getGateType(g) == gate_cmp)
1125 cmps.push_back(g);
1126 }
1127
1128 for (gate_t c : cmps) {
1129 if (gc.getGateType(c) != gate_cmp) continue; /* defensive */
1130
1131 bool ok = false;
1132 ComparisonOperator op = cmpOpFromOid(gc.getInfos(c).first, ok);
1133 if (!ok) continue;
1134
1135 const auto &wires = gc.getWires(c);
1136 if (wires.size() != 2) continue;
1137
1138 bool lhs_is_agg = gc.getGateType(wires[0]) == gate_agg;
1139 bool rhs_is_agg = gc.getGateType(wires[1]) == gate_agg;
1140 if (lhs_is_agg == rhs_is_agg) continue; /* both agg or neither */
1141
1142 gate_t agg_side = lhs_is_agg ? wires[0] : wires[1];
1143 gate_t const_side = lhs_is_agg ? wires[1] : wires[0];
1144
1145 double const_val = extractScalarConst(gc, const_side);
1146 if (std::isnan(const_val)) continue;
1147
1148 bool always_true = false;
1149 double p = decideAggVsConstCmp(gc, agg_side, op, const_val,
1150 lhs_is_agg, &always_true);
1151 if (!always_true) {
1152 /* p might be 0.0 (already handled by runRangeCheck at load time
1153 * if simplify_on_load is on); skip either way. */
1154 (void)p;
1155 continue;
1156 }
1157
1158 /* Scalar aggregation (no GROUP BY): the single result row always exists, so
1159 * a tautological predicate (count >= 0, count > -K, ...) is gate_one --
1160 * probability 1, including the empty-input world. The "group is non-empty"
1161 * rewrite below is the grouped semantics (the empty group is no row), which
1162 * is exactly the empty-world over-credit the doc comment on
1163 * decideAggVsConstCmp warns against; for a scalar agg that world is real. */
1164 if ((gc.getInfos(agg_side).second & PROVSQL_AGG_SCALAR_FLAG) != 0) {
1165 gc.resolveCmpToBernoulli(c, 1.0);
1166 ++resolved;
1167 continue;
1168 }
1169
1170 /* Gather the per-row K-gates from the agg's semimod children. */
1171 std::vector<gate_t> ks;
1172 bool shape_ok = true;
1173 ks.reserve(gc.getWires(agg_side).size());
1174 for (gate_t ch : gc.getWires(agg_side)) {
1175 if (gc.getGateType(ch) != gate_semimod) { shape_ok = false; break; }
1176 const auto &sw = gc.getWires(ch);
1177 if (sw.size() != 2) { shape_ok = false; break; }
1178 ks.push_back(sw[0]); /* K side; M side is sw[1] = gate_value */
1179 }
1180 if (!shape_ok || ks.empty()) continue;
1181
1182 gc.resolveCmpToPlusOfKGates(c, ks);
1183 ++resolved;
1184 }
1185
1186 return resolved;
1187}
1188
1189namespace {
1190
1191/* Sampling-time support for aggregation gates. Unlike @c intervalOf
1192 * (shared with the @c runRangeCheck cmp dispatcher, which must stay
1193 * conservative on agg to respect SQL NULL semantics), this widens
1194 * gate_agg and non-trivial gate_semimod to the actual range of
1195 * scalar MC samples @c MonteCarloSampler::evalScalar can produce.
1196 * Used only by @c compute_support, called from rv_support /
1197 * rv_histogram / rv_moment fallbacks, so the cmp decider remains
1198 * untouched.
1199 *
1200 * Empty-group convention (see test/sql/continuous_aggregation §5):
1201 * COUNT and SUM yield 0; MIN / MAX / AVG yield NaN. NaN sits
1202 * outside any real interval, so callers binning samples drop those
1203 * worlds automatically; the moment averagers in
1204 * Expectation::mc_raw_moment also skip them.
1205 */
1206Interval aggSupportOf(const GenericCircuit &gc, gate_t root,
1207 std::unordered_map<gate_t, Interval> &cache)
1208{
1209 const auto type = gc.getGateType(root);
1210 if (type == gate_semimod) {
1211 const auto &wires = gc.getWires(root);
1212 if (wires.size() != 2) return Interval::all();
1213 Interval vi = intervalOf(gc, wires[1], cache);
1214 if (gc.getGateType(wires[0]) == gate_one) return vi;
1215 /* Boolean k child: per-iteration scalar is value · 1_{k fires},
1216 * so the support is the union of {0} and the value's range. */
1217 return Interval{std::min(0.0, vi.lo), std::max(0.0, vi.hi)};
1218 }
1219 if (type != gate_agg) return intervalOf(gc, root, cache);
1220
1221 const auto &wires = gc.getWires(root);
1223 getAggregationOperator(gc.getInfos(root).first);
1224
1225 std::vector<gate_t> sm_children;
1226 sm_children.reserve(wires.size());
1227 for (gate_t c : wires)
1228 if (gc.getGateType(c) == gate_semimod) sm_children.push_back(c);
1229
1230 auto child_value_iv = [&](gate_t sm) -> Interval {
1231 const auto &sw = gc.getWires(sm);
1232 if (sw.size() != 2) return Interval::all();
1233 return intervalOf(gc, sw[1], cache);
1234 };
1235 auto child_always_fires = [&](gate_t sm) -> bool {
1236 const auto &sw = gc.getWires(sm);
1237 return sw.size() == 2 && gc.getGateType(sw[0]) == gate_one;
1238 };
1239
1240 const auto inf = std::numeric_limits<double>::infinity();
1241 switch (op) {
1243 /* [0, n_rows]. Each semimod contributes 0 or 1 to the count. */
1244 return Interval{0.0, static_cast<double>(sm_children.size())};
1246 /* Per row, contribution is value if k fires, else 0; sum the
1247 * per-row support intervals. Always-firing rows contribute
1248 * their value interval verbatim; possibly-firing rows
1249 * contribute [min(0, v.lo), max(0, v.hi)]. */
1250 double lo = 0.0, hi = 0.0;
1251 for (gate_t sm : sm_children) {
1252 Interval vi = child_value_iv(sm);
1253 if (vi.isAll()) return Interval::all();
1254 if (child_always_fires(sm)) {
1255 lo += vi.lo;
1256 hi += vi.hi;
1257 } else {
1258 lo += std::min(0.0, vi.lo);
1259 hi += std::max(0.0, vi.hi);
1260 }
1261 }
1262 return Interval{lo, hi};
1263 }
1266 /* MIN / MAX of values where k_i fires. The actual MIN (or MAX)
1267 * is some value from one of the firing rows, so the support is
1268 * the union of the children's value intervals. Empty-group
1269 * worlds finalise to NaN, which sits outside the real
1270 * interval. */
1271 if (sm_children.empty()) return Interval::all();
1272 double lo = inf;
1273 double hi = -inf;
1274 for (gate_t sm : sm_children) {
1275 Interval vi = child_value_iv(sm);
1276 if (vi.isAll()) return Interval::all();
1277 lo = std::min(lo, vi.lo);
1278 hi = std::max(hi, vi.hi);
1279 }
1280 if (lo > hi) return Interval::all();
1281 return Interval{lo, hi};
1282 }
1283 default:
1284 /* AVG: ratio depends on the world's row count. AND / OR /
1285 * CHOOSE / ARRAY_AGG: not numeric carriers rv_* surfaces.
1286 * Keep the conservative all-real default. */
1287 return Interval::all();
1288 }
1289}
1290
1291} // namespace
1292
1293std::pair<double, double>
1295 std::optional<gate_t> event_root)
1296{
1297 std::unordered_map<gate_t, Interval> cache;
1298 Interval iv = aggSupportOf(gc, root, cache);
1299
1300 /* Conditional path: intersect with the event's AND-conjunct
1301 * constraints on @p root. Walks event_root collecting `rv op c`
1302 * cmps; non-target constraints are ignored (they affect P(event)
1303 * but not the truncation of root's distribution). Even if the
1304 * walk is "incomplete" (gate_plus / gate_monus / arith encountered)
1305 * the result is sound: we're computing a SUPERSET bound on the
1306 * conditional support, and the unconditional support is already a
1307 * superset, so the intersection of the collected constraints with
1308 * the unconditional is also a superset. */
1309 if (event_root.has_value()) {
1310 std::unordered_map<gate_t, Interval> rv_intervals;
1311 bool complete;
1312 walkAndConjunctIntervals(gc, *event_root, rv_intervals, cache, complete);
1313 auto it = rv_intervals.find(root);
1314 if (it != rv_intervals.end()) {
1315 iv.lo = std::max(iv.lo, it->second.lo);
1316 iv.hi = std::min(iv.hi, it->second.hi);
1317 /* Defensively clamp to avoid an inverted interval if a buggy
1318 * walker produced one; should not happen but cheap. */
1319 if (iv.lo > iv.hi) iv.lo = iv.hi;
1320 }
1321 }
1322
1323 return {iv.lo, iv.hi};
1324}
1325
1326std::optional<std::pair<double, double>>
1328 gate_t target_rv)
1329{
1330 std::unordered_map<gate_t, Interval> rv_intervals;
1331 std::unordered_map<gate_t, Interval> support_cache;
1332 bool complete;
1333 walkAndConjunctIntervals(gc, event_root, rv_intervals, support_cache,
1334 complete);
1335 if (!complete) return std::nullopt;
1336 /* If the walk found no cmp constraining target_rv, the conditional
1337 * support is the unconditional support (the event is independent
1338 * of target_rv along the recognised structure). Returning the
1339 * unconditional interval lets the moment closed-form path
1340 * short-circuit to the unconditional moment, matching the
1341 * mathematical truth. */
1342 auto it = rv_intervals.find(target_rv);
1343 Interval iv;
1344 if (it != rv_intervals.end()) {
1345 iv = it->second;
1346 /* Intersect with the RV's own support to be safe (event may
1347 * over-constrain past the support, e.g. `Exp(λ) < -1`). */
1348 Interval base = intervalOf(gc, target_rv, support_cache);
1349 iv.lo = std::max(iv.lo, base.lo);
1350 iv.hi = std::min(iv.hi, base.hi);
1351 if (iv.lo > iv.hi) iv.lo = iv.hi;
1352 } else {
1353 iv = intervalOf(gc, target_rv, support_cache);
1354 }
1355 return std::make_pair(iv.lo, iv.hi);
1356}
1357
1358/**
1359 * @brief Parse a @c gate_value's @c extra as a finite @c float8.
1360 *
1361 * Sibling of @c extract_constant_double in @c having_semantics.cpp but
1362 * with a const @c GenericCircuit ref (used in the closed-form shape
1363 * detector path). Bails on @c NaN / @c ±Infinity so a downstream
1364 * stem renderer never sees a non-finite x coordinate.
1365 */
1367 double &out)
1368{
1369 if (gc.getGateType(x) != gate_value) return false;
1370 const std::string &s = gc.getExtra(x);
1371 if (s.empty()) return false;
1372 try {
1373 size_t idx = 0;
1374 double v = std::stod(s, &idx);
1375 if (idx != s.size() || !std::isfinite(v)) return false;
1376 out = v;
1377 return true;
1378 } catch (...) {
1379 return false;
1380 }
1381}
1382
1383/** @brief Same parsing applied to a mulinput's outcome label (categorical). */
1385 double &out)
1386{
1387 if (gc.getGateType(mul) != gate_mulinput) return false;
1388 const std::string &s = gc.getExtra(mul);
1389 if (s.empty()) return false;
1390 try {
1391 size_t idx = 0;
1392 double v = std::stod(s, &idx);
1393 if (idx != s.size() || !std::isfinite(v)) return false;
1394 out = v;
1395 return true;
1396 } catch (...) {
1397 return false;
1398 }
1399}
1400
1401std::optional<TruncatedSingleRv>
1403 std::optional<gate_t> event_root)
1404{
1405 if (gc.getGateType(root) != gate_rv) return std::nullopt;
1406 auto spec = parse_distribution_spec(gc.getExtra(root));
1407 if (!spec) return std::nullopt;
1408
1409 /* Natural support per family. Normal is unbounded both sides;
1410 * Uniform sits exactly on its parameters; Exp / Erlang on
1411 * [0, +inf). Used both as the unconditional case and as the
1412 * intersection seed for collectRvConstraints (which already
1413 * intersects internally, but the bare-natural case still needs
1414 * a baseline). */
1415 double nat_lo = -std::numeric_limits<double>::infinity();
1416 double nat_hi = +std::numeric_limits<double>::infinity();
1417 switch (spec->kind) {
1418 case DistKind::Normal: break;
1419 case DistKind::Uniform: nat_lo = spec->p1;
1420 nat_hi = spec->p2; break;
1421 case DistKind::Exponential: nat_lo = 0.0; break;
1422 case DistKind::Erlang: nat_lo = 0.0; break;
1423 }
1424
1425 /* Unconditional path: return natural support, mark untruncated. */
1426 if (!event_root.has_value()
1427 || gc.getGateType(*event_root) == gate_one) {
1428 return TruncatedSingleRv{*spec, nat_lo, nat_hi, /*truncated=*/false};
1429 }
1430
1431 /* Infeasible event resolved upstream by RangeCheck: the cmp was
1432 * folded to gate_zero, the conditional distribution is undefined.
1433 * @c collectRvConstraints would silently fall back to the natural
1434 * support here (its walker skips gate_zero like gate_one), so we
1435 * have to detect this explicitly. */
1436 if (gc.getGateType(*event_root) == gate_zero) return std::nullopt;
1437
1438 auto iv = collectRvConstraints(gc, *event_root, root);
1439 if (!iv.has_value()) return std::nullopt;
1440 if (!(iv->first < iv->second)) return std::nullopt;
1441
1442 return TruncatedSingleRv{*spec, iv->first, iv->second, /*truncated=*/true};
1443}
1444
1446 std::optional<gate_t> event_root)
1447{
1448 if (!event_root.has_value()) return false;
1449 const auto et = gc.getGateType(*event_root);
1450 if (et == gate_one) return false;
1451 /* RangeCheck folded the event to false upstream – universal
1452 * signal, independent of root gate type (a constant scalar
1453 * value paired with an impossible cmp lands here too). */
1454 if (et == gate_zero) return true;
1455 /* Walk the event's AND-conjuncts; an empty intersection with the
1456 * RV's natural support is the second infeasibility signal that
1457 * @c matchTruncatedSingleRv collapses into @c std::nullopt. Only
1458 * applicable when the root is itself a bare gate_rv that the
1459 * walker recognises. */
1460 if (gc.getGateType(root) != gate_rv) return false;
1461 auto iv = collectRvConstraints(gc, *event_root, root);
1462 if (!iv.has_value()) return false;
1463 return !(iv->first < iv->second);
1464}
1465
1466/**
1467 * @brief Unconditional probability mass of a shape over the
1468 * interval @c [lo, hi].
1469 *
1470 * @c TruncatedSingleRv arms supplied here must carry
1471 * @c truncated == @c false (the unconditional shape); the helper
1472 * uses the natural support to compute the CDF endpoints, so calling
1473 * with an already-truncated input would double-truncate.
1474 *
1475 * Recursive: a Bernoulli mixture's mass is the Bernoulli-weighted
1476 * combination of its arms' masses. Categorical mass is the sum of
1477 * outcome masses falling in the interval. Dirac mass is 1 iff the
1478 * Dirac value sits in the interval, else 0. Returns @c std::nullopt
1479 * when a leaf's spec defeats the closed-form CDF (e.g. non-integer
1480 * Erlang shape – @c cdfAt returns NaN there).
1481 */
1482static std::optional<double>
1483shape_mass(const ClosedFormShape &s, double lo, double hi)
1484{
1485 return std::visit([&](const auto &v) -> std::optional<double> {
1486 using T = std::decay_t<decltype(v)>;
1487 if constexpr (std::is_same_v<T, TruncatedSingleRv>) {
1488 const double a = std::max(lo, v.lo);
1489 const double b = std::min(hi, v.hi);
1490 if (!(a < b)) return 0.0;
1491 const double cl = std::isfinite(a) ? cdfAt(v.spec, a) : 0.0;
1492 const double ch = std::isfinite(b) ? cdfAt(v.spec, b) : 1.0;
1493 if (std::isnan(cl) || std::isnan(ch)) return std::nullopt;
1494 return ch - cl;
1495 } else if constexpr (std::is_same_v<T, DiracShape>) {
1496 return (v.value >= lo && v.value <= hi) ? 1.0 : 0.0;
1497 } else if constexpr (std::is_same_v<T, CategoricalShape>) {
1498 double m = 0.0;
1499 for (const auto &pr : v.outcomes)
1500 if (pr.first >= lo && pr.first <= hi) m += pr.second;
1501 return m;
1502 } else if constexpr (std::is_same_v<T, BernoulliMixtureShape>) {
1503 auto L = shape_mass(*v.left, lo, hi);
1504 auto R = shape_mass(*v.right, lo, hi);
1505 if (!L || !R) return std::nullopt;
1506 return v.p * (*L) + (1.0 - v.p) * (*R);
1507 }
1508 return std::nullopt;
1509 }, s);
1510}
1511
1512/**
1513 * @brief Conditional shape after truncating the underlying variable
1514 * to @c [lo, hi].
1515 *
1516 * Bare-RV arm: intersects its natural / current truncation with
1517 * @c [lo, hi] and marks the result truncated so downstream
1518 * @c shape_pdf renormalises by the truncated CDF. Dirac: keep iff
1519 * value ∈ interval, otherwise nullopt (infeasible). Categorical:
1520 * keep outcomes in interval, renormalise masses. Bernoulli mixture:
1521 * recursively truncate each arm and reweight the Bernoulli by the
1522 * ratio of arm masses (the standard
1523 * @f$ \pi' = \pi Z_L / (\pi Z_L + (1-\pi) Z_R) @f$ update); a
1524 * fully-eliminated arm degenerates to the surviving one. Returns
1525 * @c nullopt when the truncated shape has zero mass (caller can
1526 * raise infeasibility).
1527 */
1528static std::optional<ClosedFormShape>
1529truncateShape(const ClosedFormShape &s, double lo, double hi)
1530{
1531 return std::visit([&](const auto &v) -> std::optional<ClosedFormShape> {
1532 using T = std::decay_t<decltype(v)>;
1533 if constexpr (std::is_same_v<T, TruncatedSingleRv>) {
1534 const double a = std::max(lo, v.lo);
1535 const double b = std::min(hi, v.hi);
1536 if (!(a < b)) return std::nullopt;
1537 return ClosedFormShape{TruncatedSingleRv{v.spec, a, b, /*trunc=*/true}};
1538 } else if constexpr (std::is_same_v<T, DiracShape>) {
1539 if (v.value < lo || v.value > hi) return std::nullopt;
1540 return ClosedFormShape{v};
1541 } else if constexpr (std::is_same_v<T, CategoricalShape>) {
1542 CategoricalShape out;
1543 double total = 0.0;
1544 for (const auto &pr : v.outcomes) {
1545 if (pr.first >= lo && pr.first <= hi) {
1546 out.outcomes.emplace_back(pr.first, pr.second);
1547 total += pr.second;
1548 }
1549 }
1550 if (out.outcomes.empty() || !(total > 0.0)) return std::nullopt;
1551 for (auto &pr : out.outcomes) pr.second /= total;
1552 return ClosedFormShape{std::move(out)};
1553 } else if constexpr (std::is_same_v<T, BernoulliMixtureShape>) {
1554 auto mL = shape_mass(*v.left, lo, hi);
1555 auto mR = shape_mass(*v.right, lo, hi);
1556 if (!mL || !mR) return std::nullopt;
1557 const double pL = v.p * (*mL);
1558 const double pR = (1.0 - v.p) * (*mR);
1559 const double Z = pL + pR;
1560 if (!(Z > 0.0)) return std::nullopt;
1561 auto Lt = truncateShape(*v.left, lo, hi);
1562 auto Rt = truncateShape(*v.right, lo, hi);
1563 /* Either arm eliminated by the truncation collapses to the
1564 * surviving arm (its mass was already 0 in shape_mass, so the
1565 * reweighted p_arm is 1). */
1566 if (!Lt && !Rt) return std::nullopt;
1567 if (!Lt) return Rt;
1568 if (!Rt) return Lt;
1570 m.p = pL / Z;
1571 m.left = std::make_shared<ClosedFormShape>(std::move(*Lt));
1572 m.right = std::make_shared<ClosedFormShape>(std::move(*Rt));
1573 return ClosedFormShape{std::move(m)};
1574 }
1575 return std::nullopt;
1576 }, s);
1577}
1578
1579std::optional<ClosedFormShape>
1581 std::optional<gate_t> event_root)
1582{
1583 /* Test "event is trivial true": either absent, or resolved to
1584 * gate_one by load-time simplification. */
1585 const bool event_trivial = !event_root.has_value()
1586 || gc.getGateType(*event_root) == gate_one;
1587
1588 /* Bare gate_rv root: delegate to the existing single-RV matcher
1589 * so the truncation logic (collectRvConstraints) is the single
1590 * source of truth across the closed-form-shape surface. */
1591 if (gc.getGateType(root) == gate_rv) {
1592 auto m = matchTruncatedSingleRv(gc, root, event_root);
1593 if (!m) return std::nullopt;
1594 return ClosedFormShape{*m};
1595 }
1596
1597 /* Helper: match the shape unconditionally first, then if the event
1598 * is non-trivial extract an interval via collectRvConstraints and
1599 * apply truncateShape. Used by the Dirac / categorical / mixture
1600 * branches below so all three honour conditioning through the same
1601 * pipeline. */
1602 auto with_optional_truncation =
1603 [&](std::optional<ClosedFormShape> unc)
1604 -> std::optional<ClosedFormShape> {
1605 if (!unc) return std::nullopt;
1606 if (event_trivial) return unc;
1607 auto iv = collectRvConstraints(gc, *event_root, root);
1608 if (!iv.has_value()) return std::nullopt;
1609 if (!(iv->first < iv->second)) return std::nullopt;
1610 return truncateShape(*unc, iv->first, iv->second);
1611 };
1612
1613 /* Dirac point: a gate_value with extra parseable as a finite
1614 * float8 (the underlying form of as_random(c)). Conditioning on
1615 * a constant is normally folded upstream by RangeCheck to
1616 * gate_one / gate_zero, but a probabilistic event whose footprint
1617 * doesn't constrain the constant lands here untouched (the cmp
1618 * walker returns the unconditional support); truncateShape then
1619 * keeps the Dirac iff its value falls in the recognised interval. */
1620 if (gc.getGateType(root) == gate_value) {
1621 double v;
1622 if (!extract_finite_double(gc, root, v)) return std::nullopt;
1623 return with_optional_truncation(ClosedFormShape{DiracShape{v}});
1624 }
1625
1626 /* gate_mixture: either the explicit categorical form
1627 * (isCategoricalMixture) or the classic Bernoulli triple
1628 * [p_token, x_token, y_token]. */
1629 if (gc.getGateType(root) == gate_mixture) {
1630 const auto &w = gc.getWires(root);
1631
1632 if (gc.isCategoricalMixture(root)) {
1634 cs.outcomes.reserve(w.size() - 1);
1635 for (std::size_t i = 1; i < w.size(); ++i) {
1636 double v;
1637 if (!extract_mulinput_value(gc, w[i], v)) return std::nullopt;
1638 double p = gc.getProb(w[i]);
1639 if (!std::isfinite(p) || p < 0.0 || p > 1.0) return std::nullopt;
1640 cs.outcomes.emplace_back(v, p);
1641 }
1642 if (cs.outcomes.empty()) return std::nullopt;
1643 return with_optional_truncation(ClosedFormShape{std::move(cs)});
1644 }
1645
1646 /* Classic Bernoulli mixture: 3 wires, [p_token, x_token, y_token]
1647 * with p_token a bare gate_input; compound Boolean p bails (the
1648 * generic path would need a probability-over-Boolean-circuit
1649 * pre-pass we deliberately do not run here). */
1650 if (w.size() != 3) return std::nullopt;
1651 if (gc.getGateType(w[0]) != gate_input) return std::nullopt;
1652 double p = gc.getProb(w[0]);
1653 if (!std::isfinite(p) || p < 0.0 || p > 1.0) return std::nullopt;
1654
1655 auto left = matchClosedFormDistribution(gc, w[1], std::nullopt);
1656 auto right = matchClosedFormDistribution(gc, w[2], std::nullopt);
1657 if (!left || !right) return std::nullopt;
1658
1660 m.p = p;
1661 m.left = std::make_shared<ClosedFormShape>(std::move(*left));
1662 m.right = std::make_shared<ClosedFormShape>(std::move(*right));
1663 return with_optional_truncation(ClosedFormShape{std::move(m)});
1664 }
1665
1666 return std::nullopt;
1667}
1668
1669} // namespace provsql
1670
1671extern "C" {
1672
1673/**
1674 * @brief SQL: rv_support(token uuid, prov uuid, OUT lo float8, OUT hi float8)
1675 *
1676 * Loads the persisted circuit rooted at @p token, intersects with the
1677 * AND-conjunct cmps in @p prov constraining @p token, and returns the
1678 * resulting @c [lo, hi] support interval. When @p prov resolves to
1679 * @c gate_one (the unconditional default after load-time
1680 * simplification), the conditional path is skipped and the bare
1681 * unconditional support of @p token is returned.
1682 *
1683 * @c -Infinity / @c +Infinity float8 represent unbounded ends (e.g.
1684 * the support of a normal RV is @c [-Infinity, +Infinity]).
1685 */
1686Datum rv_support(PG_FUNCTION_ARGS)
1687{
1688 try {
1689 pg_uuid_t *token = PG_GETARG_UUID_P(0);
1690 pg_uuid_t *prov = PG_GETARG_UUID_P(1);
1691
1692 gate_t root_gate, event_gate;
1693 auto gc = getJointCircuit(*token, *prov, root_gate, event_gate);
1694
1695 /* gate_one as event-side means the conditioning is the trivial
1696 * "always true" event (either the user passed gate_one() directly
1697 * or load-time simplification collapsed the event to it). Take
1698 * the unconditional path. */
1699 std::optional<gate_t> event_opt;
1700 if (gc.getGateType(event_gate) != gate_one)
1701 event_opt = event_gate;
1702
1703 /* A stored "X | C" arrives here as a conditioned root: peel it to the
1704 * bare target and fold the condition into the event, so the support is
1705 * the conditional (truncated) one rather than the unconditional. */
1706 root_gate = provsql::lift_conditioning(gc, root_gate, event_opt);
1707
1708 auto iv = provsql::compute_support(gc, root_gate, event_opt);
1709
1710 TupleDesc tupdesc;
1711 Datum values[2];
1712 bool nulls[2] = {false, false};
1713
1714 if (get_call_result_type(fcinfo, NULL, &tupdesc) != TYPEFUNC_COMPOSITE)
1715 provsql_error("rv_support: expected composite return type");
1716 tupdesc = BlessTupleDesc(tupdesc);
1717
1718 values[0] = Float8GetDatum(iv.first);
1719 values[1] = Float8GetDatum(iv.second);
1720
1721 PG_RETURN_DATUM(HeapTupleGetDatum(heap_form_tuple(tupdesc, values, nulls)));
1722 } catch (const std::exception &e) {
1723 provsql_error("rv_support: %s", e.what());
1724 } catch (...) {
1725 provsql_error("rv_support: unknown exception");
1726 }
1727 PG_RETURN_NULL();
1728}
1729
1730} // extern "C"
ComparisonOperator cmpOpFromOid(Oid op_oid, bool &ok)
Map a PostgreSQL comparison-operator OID to a ComparisonOperator.
AggregationOperator getAggregationOperator(Oid oid)
Map a PostgreSQL aggregate function OID to an AggregationOperator.
Typed aggregation value, operator, and aggregator abstractions.
AggregationOperator
SQL aggregation functions tracked by ProvSQL.
Definition Aggregation.h:51
@ MAX
MAX → input type.
Definition Aggregation.h:55
@ COUNT
COUNT(*) or COUNT(expr) → integer.
Definition Aggregation.h:52
@ SUM
SUM → integer or float.
Definition Aggregation.h:53
@ MIN
MIN → input type.
Definition Aggregation.h:54
ComparisonOperator
SQL comparison operators used in gate_cmp circuit gates.
Definition Aggregation.h:39
@ LT
Less than (<).
Definition Aggregation.h:43
@ GT
Greater than (>).
Definition Aggregation.h:45
@ LE
Less than or equal (<=).
Definition Aggregation.h:42
@ NE
Not equal (<>).
Definition Aggregation.h:41
@ GE
Greater than or equal (>=).
Definition Aggregation.h:44
Closed-form CDF resolution for trivial gate_cmp shapes.
static CircuitCache cache
Process-local singleton circuit gate cache.
GenericCircuit getJointCircuit(pg_uuid_t root_token, pg_uuid_t event_token, gate_t &root_gate, gate_t &event_gate)
Build a GenericCircuit containing the closures of two roots, with shared subgraphs unified.
Build in-memory circuits from the mmap-backed persistent store.
gate_t
Strongly-typed gate identifier.
Definition Circuit.h:49
Analytical expectation / variance / moment evaluator over RV circuits.
Continuous random-variable helpers (distribution parsing, moments).
Datum rv_support(PG_FUNCTION_ARGS)
SQL: rv_support(token uuid, prov uuid, OUT lo float8, OUT hi float8).
Support-based bound check for continuous-RV comparators.
iterator end()
Past-the-end iterator for the cache.
std::vector< gate_t > & getWires(gate_t g)
Return a mutable reference to the child-wire list of gate g.
Definition Circuit.h:140
gateType getGateType(gate_t g) const
Return the type of gate g.
Definition Circuit.h:130
std::vector< gate_t >::size_type getNbGates() const
Return the total number of gates in the circuit.
Definition Circuit.h:103
In-memory provenance circuit with semiring-generic evaluation.
void resolveGateToZero(gate_t g)
Replace an arbitrary gate (typically gate_times) by gate_zero.
void resolveCmpToPlusOfKGates(gate_t g, const std::vector< gate_t > &ks)
Replace a gate_cmp by a gate_plus over the given per-row K-gates (the OR of the agg's row-presence in...
bool isCategoricalMixture(gate_t g) const
Test whether g is a categorical-form gate_mixture (the explicit provsql.categorical output).
std::string getExtra(gate_t g) const
Return the string extra for gate g.
double getProb(gate_t g) const
Return the probability for gate g.
void resolveCmpToBernoulli(gate_t g, double p)
Replace a gate_cmp by a constant Boolean leaf (gate_one for p == 1, gate_zero for p == 0) or by a Ber...
std::pair< unsigned, unsigned > getInfos(gate_t g) const
Return the integer annotation pair for gate g.
@ Normal
Normal (Gaussian): p1=μ, p2=σ
@ Exponential
Exponential: p1=λ, p2 unused.
@ Uniform
Uniform on [a,b]: p1=a, p2=b.
@ Erlang
Erlang: p1=k (positive integer), p2=λ.
std::pair< double, double > compute_support(const GenericCircuit &gc, gate_t root, std::optional< gate_t > event_root)
Compute the [lo, hi] support interval of a scalar sub-circuit rooted at root.
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::variant< TruncatedSingleRv, DiracShape, CategoricalShape, BernoulliMixtureShape > ClosedFormShape
One of the closed-form shapes the analytical-curves payload can render: bare RV (continuous PDF/CDF),...
Definition RangeCheck.h:201
gate_t lift_conditioning(GenericCircuit &gc, gate_t root, std::optional< gate_t > &event_opt)
Lift conditioning out of a scalar arithmetic expression.
static bool extract_mulinput_value(const GenericCircuit &gc, gate_t mul, double &out)
Same parsing applied to a mulinput's outcome label (categorical).
static bool extract_finite_double(const GenericCircuit &gc, gate_t x, double &out)
Parse a gate_value's extra as a finite float8.
double parseDoubleStrict(const std::string &s)
Strictly parse s as a double.
unsigned runRangeCheck(GenericCircuit &gc)
Run the support-based pruning pass over gc.
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].
std::optional< DistributionSpec > parse_distribution_spec(const std::string &s)
Parse the on-disk text encoding of a gate_rv distribution.
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.
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.
double cdfAt(const DistributionSpec &d, double c)
Closed-form CDF for a basic continuous distribution.
unsigned runHavingAlwaysTrueRewriter(GenericCircuit &gc)
Probability-side pre-pass: rewrite HAVING-style gate_cmp gates that are provably TRUE on the agg's va...
Uniform error-reporting macros for ProvSQL.
#define provsql_error(fmt,...)
Report a fatal ProvSQL error and abort the current transaction.
Core types, constants, and utilities shared across ProvSQL.
provsql_arith_op
Arithmetic operator tags used by gate_arith.
@ PROVSQL_ARITH_DIV
binary, child0 / child1
@ PROVSQL_ARITH_PLUS
n-ary, sum of children
@ PROVSQL_ARITH_NEG
unary, -child0
@ PROVSQL_ARITH_MINUS
binary, child0 - child1
@ PROVSQL_ARITH_TIMES
n-ary, product of children
@ gate_rv
Continuous random-variable leaf (extra encodes distribution).
@ gate_mixture
Probabilistic mixture: three wires [p_token (gate_input Bernoulli), x_token, y_token]; samples x when...
@ gate_arith
n-ary arithmetic gate over scalar-valued children (info1 holds operator tag)
#define PROVSQL_AGG_SCALAR_FLAG
Scalar-aggregation flag, stored in the upper bit of a gate_agg's info2 (whose low 31 bits hold the ag...
C++ utility functions for UUID manipulation.
UUID structure.
Bernoulli mixture (gate_mixture with the [p_token, x_token, y_token] shape).
Definition RangeCheck.h:218
std::shared_ptr< ClosedFormShape > right
Definition RangeCheck.h:221
std::shared_ptr< ClosedFormShape > left
Definition RangeCheck.h:220
Categorical distribution over a finite outcome set.
Definition RangeCheck.h:189
std::vector< std::pair< double, double > > outcomes
(value, mass) pairs
Definition RangeCheck.h:190
Point mass at a finite scalar value (a gate_value root, or an as_random(c) leaf surfaced as a gate_va...
Definition RangeCheck.h:173
Detection result for a closed-form, optionally-truncated single-RV shape.
Definition RangeCheck.h:102