AnalyticEvaluator.h File Reference

Closed-form CDF resolution for trivial gate_cmp shapes. More...

#include "GenericCircuit.h"
#include "RandomVariable.h"

Include dependency graph for AnalyticEvaluator.h:

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

Go to the source code of this file.

Namespaces
namespace	provsql

Functions
double	provsql::cdfAt (const DistributionSpec &d, double c)
	Closed-form CDF \(F_X(c) = P(X \le c)\) for a basic continuous distribution.
double	provsql::pdfAt (const DistributionSpec &d, double c)
	Closed-form probability density \(f(c)\) for a basic distribution.
unsigned	provsql::runAnalyticEvaluator (GenericCircuit &gc)
	Run the closed-form CDF resolution pass over gc.

Detailed Description

Closed-form CDF resolution for trivial gate_cmp shapes.

For comparators that reduce to either:

• X cmp c with X a bare gate_rv leaf and c a bare gate_value constant, or
• X cmp Y with X and Y two distinct independent normal gate_rv leaves,

the comparator's probability has a closed form via the distribution's CDF. Implementations live inline in the .cpp (normal: std::erf; uniform: arithmetic; exponential: std::expm1) so the pass has no external math dependency. The difference of two independent normals is itself normal, with the obvious mean and variance. Replacing the gate_cmp by a Bernoulli gate_input carrying the analytical probability lets the surrounding circuit be evaluated exactly by every downstream probability method – no MC noise.

Unlike RangeCheck, this pass is probability-specific: fractional probabilities are meaningful only on the probability path. It therefore runs in probability_evaluate.cpp, not inside getGenericCircuit (which is shared with semiring evaluation, view_circuit, PROV export, etc.).

Compositions involving gate_arith (e.g. aX + bY > c for independent normals) are out of scope here; folding them into a single distribution requires the family-closure simplifier planned for the hybrid evaluator.

Definition in file AnalyticEvaluator.h.