ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
Loading...
Searching...
No Matches
MinMaxCmpEvaluator.cpp
Go to the documentation of this file.
1/**
2 * @file MinMaxCmpEvaluator.cpp
3 * @brief Implementation of the MIN / MAX closed-form pre-pass.
4 * See @c MinMaxCmpEvaluator.h for the closed forms and the
5 * soundness contract.
6 */
8
9#include <vector>
10
11#include "Aggregation.h" // AggregationOperator + ComparisonOperator
12#include "CmpEvaluatorCommon.h" // matchAggCmp, computeRefCounts, contributorProb
13
14namespace provsql {
15
16namespace {
17
18/* ∏_{i : pred(m_i)} (1 - p_i) : the probability that every child whose
19 * value satisfies @p pred is absent. An empty product is 1.0. */
20template <typename Pred>
21static double qprod(const std::vector<double> &p,
22 const std::vector<long> &m,
23 Pred pred)
24{
25 double q = 1.0;
26 for (std::size_t i = 0; i < p.size(); ++i)
27 if (pred(m[i])) q *= (1.0 - p[i]);
28 return q;
29}
30
31/* Pr(MIN/MAX = C) under HAVING semantics (empty group excluded).
32 * MAX = C : no child > C present, at least one child = C present.
33 * MIN = C : no child < C present, at least one child = C present. */
34static double probEqual(AggregationOperator agg,
35 const std::vector<double> &p,
36 const std::vector<long> &m, int C)
37{
38 if (agg == AggregationOperator::MAX) {
39 double no_above = qprod(p, m, [&](long v) { return v > C; });
40 double some_equal = 1.0 - qprod(p, m, [&](long v) { return v == C; });
41 return no_above * some_equal;
42 } else { // MIN
43 double no_below = qprod(p, m, [&](long v) { return v < C; });
44 double some_equal = 1.0 - qprod(p, m, [&](long v) { return v == C; });
45 return no_below * some_equal;
46 }
47}
48
49/* Closed-form Pr(agg(a) op C) over the independent contributor marginals
50 * @p p with deterministic per-row values @p m. Empty group excluded for
51 * every operator (mirrors count_enum / CountCmpEvaluator). */
52static double cdfForOperator(AggregationOperator agg,
54 const std::vector<double> &p,
55 const std::vector<long> &m,
56 long C)
57{
58 auto atLeastOne = [&](auto pred) { return 1.0 - qprod(p, m, pred); };
59
60 if (agg == AggregationOperator::MAX) {
61 switch (op) {
63 return atLeastOne([&](long v) { return v >= C; });
65 return atLeastOne([&](long v) { return v > C; });
67 return qprod(p, m, [&](long v) { return v > C; })
68 * atLeastOne([&](long v) { return v <= C; });
70 return qprod(p, m, [&](long v) { return v >= C; })
71 * atLeastOne([&](long v) { return v < C; });
73 return probEqual(agg, p, m, C);
75 return (1.0 - qprod(p, m, [](long) { return true; }))
76 - probEqual(agg, p, m, C);
77 }
78 } else { // MIN
79 switch (op) {
81 return atLeastOne([&](long v) { return v <= C; });
83 return atLeastOne([&](long v) { return v < C; });
85 return qprod(p, m, [&](long v) { return v < C; })
86 * atLeastOne([&](long v) { return v >= C; });
88 return qprod(p, m, [&](long v) { return v <= C; })
89 * atLeastOne([&](long v) { return v > C; });
91 return probEqual(agg, p, m, C);
93 return (1.0 - qprod(p, m, [](long) { return true; }))
94 - probEqual(agg, p, m, C);
95 }
96 }
97 return 0.0;
98}
99
100} // namespace
101
103{
104 unsigned resolved = 0;
105 const auto nb = gc.getNbGates();
106
107 /* Snapshot the cmp-gate ids so in-place rewrites don't affect the
108 * iteration : same pattern as runCountCmpEvaluator. */
109 std::vector<gate_t> cmps;
110 for (std::size_t i = 0; i < nb; ++i) {
111 auto g = static_cast<gate_t>(i);
112 if (gc.getGateType(g) == gate_cmp)
113 cmps.push_back(g);
114 }
115 if (cmps.empty()) return 0;
116
117 /* Reference counts computed once; resolveCmpToBernoulli only clears
118 * the cmp's own wires, leaving every other gate's ref count intact. */
119 auto ref = computeRefCounts(gc);
120
121 for (gate_t cmp : cmps) {
122 if (gc.getGateType(cmp) != gate_cmp) continue; /* defensive */
123
124 AggCmpMatch match;
125 if (!matchAggCmp(gc, cmp, match))
126 continue;
127
128 if (match.agg_kind != AggregationOperator::MIN &&
130 continue;
131
132 /* Independence certification, identical to runCountCmpEvaluator :
133 * the aggregate is consumed by this cmp alone, each semimod by the
134 * aggregate alone, and every randomness-bearing gate inside K_i has
135 * reference count 1 (so the contributors are pairwise leaf-disjoint,
136 * private to the cmp, and individually read-once). See
137 * CountCmpEvaluator.h for the full argument. */
138 if (ref[static_cast<std::size_t>(match.agg)] != 1) continue;
139 bool sound = true;
140 std::vector<double> p;
141 p.reserve(match.ks.size());
142 for (std::size_t i = 0; i < match.ks.size(); ++i) {
143 if (ref[static_cast<std::size_t>(match.semimods[i])] != 1) { sound = false; break; }
144 double pi = contributorProb(gc, match.ks[i], ref, sound);
145 if (!sound) break;
146 p.push_back(pi);
147 }
148 if (!sound) continue;
149
150 double pr = cdfForOperator(match.agg_kind, match.op, p, match.ms, match.C);
151
152 /* Defensive clamp against floating-point roundoff. */
153 if (pr < 0.0) pr = 0.0;
154 if (pr > 1.0) pr = 1.0;
155
156 gc.resolveCmpToBernoulli(cmp, pr);
157 ++resolved;
158 }
159
160 return resolved;
161}
162
163} // namespace provsql
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
@ 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
gate_t
Strongly-typed gate identifier.
Definition Circuit.h:49
Shared machinery for the closed-form HAVING gate_cmp probability evaluators (Poisson-binomial COUNT,...
Closed-form probability resolution for HAVING MIN(a) op C and MAX(a) op C gate_cmps.
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 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::vector< unsigned > computeRefCounts(const GenericCircuit &gc)
Reference count of every gate as a wire-target across the whole circuit.
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)).
unsigned runMinMaxCmpEvaluator(GenericCircuit &gc)
Run the MIN / MAX closed-form pre-pass over gc.
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).
Result of matching a gate_cmp against the canonical HAVING aggregate-comparison shape.
gate_t agg
the gate_agg operand of the cmp
long C
the constant threshold, on the same integer grid as ms
std::vector< gate_t > ks
the K side of each semimod (contributor root)
std::vector< gate_t > semimods
the per-child gate_semimod parents
std::vector< long > ms
the M side of each semimod (per-row value), scaled to a common integer grid (numeric / decimal-float ...
AggregationOperator agg_kind
effective aggregate (SUM-of-1s remapped to COUNT)
ComparisonOperator op
comparator, flipped if the agg sits on the right