CountCmpEvaluator.h

Go to the documentation of this file.

/**
 * @file CountCmpEvaluator.h
 * @brief Closed-form Poisson-binomial CDF resolution for HAVING
 *        @c COUNT(*) @c op @c C @c gate_cmps.
 *
 * For comparators that reduce to
 * @c gate_cmp(gate_agg(COUNT, semimod children), gate_value(C)) where
 * each semimod child's K side is a distinct single @c gate_input
 * leaf (the first-slice scope: flat-table HAVING COUNT queries), the
 * comparator's probability is @c Pr(B op C) with @c B Poisson-binomial
 * over the children's stored marginal probabilities.  A partial DP
 * computed on the smaller side of @c C (either the lower tail
 * @c [0, C-1] on the original Bernoullis, or the upper tail computed
 * via the complementary @c [0, N-C] on the inverted Bernoullis
 * @c Y_i @c = @c 1-X_i) gives the answer in @c O(N x min(C, N-C))
 * time per cmp, without ever materialising the @c binom(N, C) DNF
 * that @c provsql_having's @c enumerate_valid_worlds path would
 * otherwise emit.
 *
 * Soundness condition (checked per cmp gate) :
 *  - shape matches `gate_cmp(gate_agg(COUNT, semimod_i(K_i, 1)*), gate_value(C))`
 *    in either order ;
 *  - every K_i is a single @c gate_input leaf (no @c gate_times,
 *    no @c gate_mulinput, no nested arithmetic) ;
 *  - the K_i leaves are pairwise distinct (no shared input across
 *    children) ;
 *  - none of the K_i leaves is reachable from the rest of the
 *    surrounding circuit, i.e. each input appears exactly once and
 *    only inside this cmp's subtree.
 *
 * The first two conditions are cheap to check locally.  The third
 * (no outside reachability) is checked once per pass via a
 * reference-count walk over the whole circuit.
 *
 * After replacement the cmp is a Bernoulli @c gate_input carrying
 * the numeric probability, semantically meaningful only on the
 * probability path.  Like @c runAnalyticEvaluator, the pass runs
 * inside @c probability_evaluate.cpp, not at load time.
 *
 * Empty-group semantics mirror @c count_enum and SQL : for a grouped
 * aggregate, worlds with zero present children are excluded (an empty
 * group is no row), so the "all-absent" mass @c dp[N][0] is not
 * included.  For a scalar aggregate (@c PROVSQL_AGG_SCALAR_FLAG: no
 * GROUP BY, or a window frame that may exclude its current row, as for
 * ranks) the empty world is real, and its mass is added when
 * @c 0 @c op @c C holds.
 */
#ifndef PROVSQL_COUNT_CMP_EVALUATOR_H
#define PROVSQL_COUNT_CMP_EVALUATOR_H
 
#include "GenericCircuit.h"
 
namespace provsql {
 
/**
 * @brief Run the Poisson-binomial pre-pass over @p gc.
 *
 * For every @c 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
 * @c gate_input via @c GenericCircuit::resolveCmpToBernoulli.  Two
 * cmps on the same COUNT whose only parent is one @c times gate
 * (@c count @c > @c m @c AND @c count @c <= @c m @c + @c k) are
 * resolved together, as the probability that the count lies in the
 * intersection of their intervals: the first becomes that Bernoulli,
 * the second @c gate_one.
 *
 * @param gc  Circuit to mutate in place.
 * @return    Number of comparators resolved by this pass.
 */
unsigned runCountCmpEvaluator(GenericCircuit &gc);
 
}  // namespace provsql
 
#endif  // PROVSQL_COUNT_CMP_EVALUATOR_H