CaseCmpExpander.h File Reference

Expansion of a comparison one of whose operands is a guarded selection (gate_case) into the comparisons of its arms. More...

#include "GenericCircuit.h"

Include dependency graph for CaseCmpExpander.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::runCaseCmpExpander (GenericCircuit &gc)
	Expand every gate_cmp with a gate_case operand in gc.

Detailed Description

Expansion of a comparison one of whose operands is a guarded selection (gate_case) into the comparisons of its arms.

A gate_case is the value of the first arm whose guard holds, and nothing in the semiring combines the value gates of its arms: a gate_cmp over one is what the Boolean translation meets and refuses ("This semiring does not support value gates"). The comparison it stands for is nonetheless an ordinary Boolean combination, since exactly one arm is selected in each world:

CASE(g₁,v₁, …, g_k,v_k, d) ⋈ O
  =  ⊕ᵢ (⊗ⱼ<ᵢ ¬gⱼ) ⊗ gᵢ ⊗ (vᵢ ⋈ O)  ⊕  (⊗ⱼ ¬gⱼ) ⊗ (d ⋈ O)

where ¬g is "𝟙 ⊖ g". The terms are mutually exclusive by the prefix of negated guards, so the ⊕ is a disjoint union in every semiring that reads these gates as Boolean events. Each arm comparison is then an ordinary one – an aggregate against the other operand, which the closed-form pre-passes and the possible-world enumeration resolve as they always have – and a comparison between two constants is decided here.

The pass runs first in resolveComparators so the comparisons it creates are seen by every later pre-pass. A comparison of two guarded selections takes one round per side; nested ones, one round per level.

Definition in file CaseCmpExpander.h.