ComparatorResolution.h File Reference

The single comparator-resolution pipeline and the single Boolean-subcircuit probability entry point, shared by the probability path and the scalar-moment evaluator. More...

#include "GenericCircuit.h"

Include dependency graph for ComparatorResolution.h:

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

Go to the source code of this file.

Namespaces
namespace	provsql

Functions
void	provsql::resolveComparators (GenericCircuit &gc, gate_t root, bool simplify, bool decompose)
	Run the comparator-resolution pipeline on gc, rewriting every gate_cmp (RV comparison, HAVING aggregate comparison) into Boolean structure so the downstream getBooleanCircuit / BoolExpr translation never meets a raw comparator.

Detailed Description

The single comparator-resolution pipeline and the single Boolean-subcircuit probability entry point, shared by the probability path and the scalar-moment evaluator.

Historically the probability path (probability_evaluate) and the moment evaluator (Expectation.cpp) each had their own, divergent notion of "resolve the RV comparators, then compute the probability of a Boolean function". This header collapses both into one place.

Definition in file ComparatorResolution.h.