CmpEvaluatorCommon.h File Reference

Shared machinery for the closed-form HAVING gate_cmp probability evaluators (Poisson-binomial COUNT, MIN / MAX…). More...

#include <vector>
#include "Aggregation.h"
#include "GenericCircuit.h"

Include dependency graph for CmpEvaluatorCommon.h:

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

Go to the source code of this file.

Classes
struct	provsql::AggCmpMatch
	Result of matching a gate_cmp against the canonical HAVING aggregate-comparison shape. More...

Namespaces
namespace	provsql

Functions
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)).
std::vector< unsigned >	provsql::computeRefCounts (const GenericCircuit &gc)
	Reference count of every gate as a wire-target across the whole circuit.
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).

Detailed Description

Shared machinery for the closed-form HAVING gate_cmp probability evaluators (Poisson-binomial COUNT, MIN / MAX…).

Every closed-form HAVING evaluator that runs as a probability-side pre-pass (see probability_evaluate.cpp) shares three concerns:

• matching the canonical shape gate_cmp(gate_agg(α, semimod_i(K_i, m_i)*), gate_value(C)) in either operand order (matchAggCmp) ;
• certifying that the gate_agg children are mutually independent Bernoulli contributors with leaves private to the cmp's subtree, via the reference-count walk (computeRefCounts) ;
• computing each contributor's read-once marginal probability (contributorProb).

These were first written for CountCmpEvaluator; they are factored here so the MIN / MAX (and future SUM) evaluators reuse the exact same soundness contract rather than re-deriving it. See CountCmpEvaluator.h for the soundness argument in full.

Definition in file CmpEvaluatorCommon.h.