MinMaxCmpEvaluator.h File Reference

Closed-form probability resolution for HAVING MIN(a) op C and MAX(a) op C gate_cmps. More...

#include "GenericCircuit.h"

Include dependency graph for MinMaxCmpEvaluator.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces
namespace	provsql

Functions
unsigned	provsql::runMinMaxCmpEvaluator (GenericCircuit &gc)
	Run the MIN / MAX closed-form pre-pass over gc.

Detailed Description

Closed-form probability resolution for HAVING MIN(a) op C and MAX(a) op C gate_cmps.

For comparators that reduce to gate_cmp(gate_agg(MIN|MAX, semimod_i(K_i, m_i)*), gate_value(C)) where the contributors are mutually independent Bernoulli trials (each K_i a private read-once sub-circuit, the same soundness contract as CountCmpEvaluator), the comparator's probability has a trivial closed form – products of (1 - p_i) over the children partitioned on m_i vs C, with no DP and no DNF.

SQL HAVING semantics exclude the empty group (a group with no present row never appears in the answer), exactly as CountCmpEvaluator and count_enum do. Writing m_i for the per-row value of the aggregated column, G for "good" children and B for "bad" children, and qprod(S) = ∏_{i∈S}(1 - p_i), the twelve cases are:

MAX ≥ C : G={m_i≥C} 1 − qprod(G) MAX > C : G={m_i>C} 1 − qprod(G) MAX ≤ C : B={m_i>C}, G={m_i≤C} qprod(B)·(1 − qprod(G)) MAX < C : B={m_i≥C}, G={m_i<C} qprod(B)·(1 − qprod(G)) MAX = C : B={m_i>C}, E={m_i=C} qprod(B)·(1 − qprod(E)) MAX ≠ C : (1 − qprod(all)) − Pr(MAX = C) MIN ≤ C : G={m_i≤C} 1 − qprod(G) MIN < C : G={m_i<C} 1 − qprod(G) MIN ≥ C : B={m_i<C}, G={m_i≥C} qprod(B)·(1 − qprod(G)) MIN > C : B={m_i≤C}, G={m_i>C} qprod(B)·(1 − qprod(G)) MIN = C : B={m_i<C}, E={m_i=C} qprod(B)·(1 − qprod(E)) MIN ≠ C : (1 − qprod(all)) − Pr(MIN = C)

(The two "good" and "bad" sets are disjoint and independent, so the two factors multiply; the (1 − qprod(G)) factor enforces group non-emptiness.)

After replacement the cmp is a Bernoulli gate_input carrying the numeric probability, semantically meaningful only on the probability path. Like runCountCmpEvaluator and runAnalyticEvaluator, the pass runs inside probability_evaluate.cpp, gated on provsql.cmp_probability_evaluation, not at load time.

Definition in file MinMaxCmpEvaluator.h.