@@ -640,7 +640,11 @@ module Make<
640640 Guard guard , GuardValue v , SsaPhiDefinition phi , Expr input
641641 ) {
642642 exists ( GuardValue dv , SsaExplicitWrite inp |
643- guardControlsPhiBranch ( guard , v , phi , inp ) and
643+ // The `forall` below implies that there's only one `inp` guarded by
644+ // `guard == v`, but checking this upfront using `unique` as opposed to
645+ // merely stating `guardControlsPhiBranch(guard, v, phi, inp)` improves
646+ // performance of the `forall` check.
647+ inp = unique( SsaDefinition inp0 | guardControlsPhiBranch ( guard , v , phi , inp0 ) ) and
644648 inp .getValue ( ) = input and
645649 dv = v .getDualValue ( ) and
646650 forall ( SsaDefinition other | phi .hasInputFromBlock ( other , _) and other != inp |
@@ -741,7 +745,7 @@ module Make<
741745 possibleValue ( v , false , e , k ) and
742746 not possibleValue ( v , true , e , k ) and
743747 // there's only one expression with the value `k`
744- 1 = strictcount ( Expr e0 | possibleValue ( v , _, e0 , k ) ) and
748+ e = unique ( Expr e0 | possibleValue ( v , _, e0 , k ) ) and
745749 // and `v` has at least two possible values
746750 2 <= strictcount ( GuardValue k0 | possibleValue ( v , _, _, k0 ) )
747751 }
0 commit comments