C++: Fix forex recursion in sign analysis

[MathiasVP]

It's well-known that recursion through forall/forex may perform poorly. Apparently we do recursion through forex in the sign analysis library (which is part of the new range analysis library for C++). This results in some unfortunate tuple counts because the "range" part of the forall/forex gets joined with itself:

Tuple counts for _RangeAnalysisImpl::SignAnalysis::zeroBound/3#c119dcdb_RangeAnalysisImpl::SignAnalysis::zeroBound/3#__#antijoin_rhs/3@i4#L3#76559w2g after 1m28s:
  256000    ~900%         {4} r1 = JOIN `RangeAnalysisImpl::SignAnalysis::zeroBoundOk/3#a6688e7a#prev_delta` WITH num#Sign::TZero#65a6fcab CARTESIAN PRODUCT OUTPUT Lhs.0, Lhs.1 'arg1', Lhs.2 'arg2', Rhs.0
  251000    ~1835%        {3}    | JOIN WITH `RangeAnalysisImpl::SignAnalysis::zeroBound/3#c119dcdb` ON FIRST 3 OUTPUT Lhs.1 'arg1', Lhs.2 'arg2', Lhs.3 'arg0'
  692772000 ~2073%        {4}    | JOIN WITH `RangeAnalysisImpl::SignAnalysis::zeroBound/3#c119dcdb_120#join_rhs` ON FIRST 2 OUTPUT Rhs.2, Lhs.0 'arg1', Lhs.1 'arg2', Lhs.2 'arg0'
                          {4}    | AND NOT `RangeAnalysisImpl::SignAnalysis::zeroBoundOk/3#a6688e7a#prev`(FIRST 3)
  64314500  ~1238106%     {3}    | SCAN OUTPUT In.3 'arg0', In.1 'arg1', In.2 'arg2'

Luckily, there's a standard way to work around this problem by rewriting the forall/forex to recursion over integers. This PR does just that. This results in much better RA.

Copilot encountered an error and was unable to review this pull request. You can try again, by re-requesting a review.

[MathiasVP]

DCA looks good. Zero result changes (as expected), and now the problematic project no longer times out 🎉

[aschackmull]

Let's leave in the original line as a comment:

Suggested change

	posBoundGuardedSsaSignOk(v, pos)
	// optimised version of
	// `forex(SemExpr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos))`
	posBoundGuardedSsaSignOk(v, pos)

[aschackmull]

Same for the others.

[MathiasVP]

Fixed in 4ffe70d

[aschackmull]

It's a shame that it's necessary, but LGTM.