Translate ternaries, and stop crashing on bitwise and real modulo

[HowardvanRooijen]

Improves the expression-tree translation layer (ExpressionVisitor) — the part of the library
that turns a constraint lambda into Z3 terms. Behavioural, perf, and cleanup; no public-API
change (the instance-visitor refactor and internal narrowing are a separate PR).

What was wrong, measured

Three rough edges, all confirmed by probe before the change:

Constraint	Before
(t.X1 > 0 ? t.X2 : 0) == 5 — a ternary	NotSupportedException: Conditional — no case at all
(t.X1 & 6) == 4 — integer bitwise & (also |, ^)	InvalidCastException: IntExpr → BoolExpr, from inside Z3
t.X1 % 2.5 == 0.5 — real modulo	InvalidCastException: RealExpr → IntExpr

The bitwise and modulo crashes share one cause: the operator dispatch keyed on the expression
node and cast the operands to an assumed sort. But C# spells two different operations the same
way — &/|/^ are Boolean logic on bool and bitwise arithmetic on integers, and % is
integer remainder with no real counterpart. The node can't tell them apart, so the wrong operand
got a cast that succeeded for one meaning and threw an opaque Z3 cast error for the other. This is
the same lesson the Convert case learned in #63/#76 — decide from the operand's translated
sort, not the node — that the rest of the dispatch never got.

The change

Ternary → if-then-else. ExpressionType.Conditional now translates to MkITE, so
t.X1 > 0 ? a : b works, including nested inside arithmetic and over real-sorted branches.

Sort-aware & | ^. The operator is chosen from the operands: Boolean operands give the
logical operator exactly as before; anything else is a bitwise operation, which Z3's integer sort
has no counterpart for, so it is refused with

The '&' operator is supported only on Boolean operands. A bitwise operation on integer symbols
is not supported, because it would need a bit-vector representation the library does not expose.

Sort-aware %. Integer operands give the remainder as before; a real modulo is refused with a
message saying Z3 has no remainder on reals, rather than crashing in the cast.

Genuine integer bitwise and shift support needs bit-vector symbols — a separate feature. This PR
turns two opaque crashes into clear, honest diagnostics; it does not pretend to add the feature.

Perf. The Distinct translation looked up three MethodInfos by reflection on every visit
— typeof(Z3Methods).GetMethod("Distinct") and, worse, typeof(Enumerable).GetMethods().First(…)
twice, materialising all of Enumerable. They are now cached in static readonly fields.

Cleanup. Removed the commented-out VisitParameter and a dead else { //Debugger.Break(); };
fixed MkString(val.ToString()) to (string)val where the value is already a string; corrected
an "unsuported" message.

Tests

280 → 290. A new ExpressionTranslationTests for the operators this touches, and two pins in
UnsupportedExpressionTests updated because their subject changed.

Test	What it covers
Solve_TernaryWhoseTestHolds_TakesTheTrueBranch / ..TestFails_TakesTheFalseBranch	both arms of the conditional
Solve_TernaryOverRealBranches_Translates	real-sorted branches
Solve_TernaryNestedInArithmetic_Translates	the conditional as a sub-term, not just the whole constraint
Solve_BitwiseOperatorOnIntegerSymbols_ThrowsNotSupportedNamingIt (&, |, ^)	the refusal names the operator and bit-vector
Solve_ModuloOnRealSymbols_ThrowsNotSupportedNamingIt	the refusal names modulo
Solve_BooleanBitwiseOperators_StillTranslate	the load-bearing regression guard — Boolean &/|/^ unchanged
Solve_ModuloOnIntegerSymbols_StillTranslates	integer remainder unchanged
Solve_ConditionalExpression_ThrowsNotSupportedException (removed)	ternary is now supported and covered positively above
Solve_SupportedExpressionsAlongsideRejectedOnes_StillRejects (updated)	its rejected example was a ternary; now an integer bitwise op

The Distinct MethodInfo caching is behaviour-preserving and stays covered by the existing
DistinctSelectorTheoremTests / DistinctInlineArrayTheoremTests.

Mutation results

Mutation	Failures	Which
Remove the Conditional case	4	every ternary test
&/|/^ cast to BoolExpr blindly (the old code)	4	the three bitwise rows and the alongside-rejected pin — back to InvalidCastException
% casts to IntExpr blindly (the old code)	1	the real-modulo test

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release — clean, TreatWarningsAsErrors and
  documentation generation on
• 290/290 locally
• ./build.ps1 -Configuration Release — 46 tasks, 0 errors, 0 warnings
• Coverage 88.9% -> 89.2% line (839 of 940); branch 78.6% -> 76.0% (543 of 714), the dip being the
  new refusal branches that fire only in the negative tests plus the ternary MkITE paths — the
  operators' own branches are covered in both directions

Follow-ups (not in this PR)

• Instance visitor + internal narrowing — ExpressionVisitor threads
  (Context, Environment, ParameterExpression) through every method and is public only "for
  historical reasons." Turning it into an internal instance class with those as fields is the
  mechanical modernisation the .NET 10 / major-version work unblocks; kept separate so a large
  no-behaviour diff doesn't bury these fixes. Next PR on the stack.
• Bit-vector symbols — what would make integer bitwise and shifts actually work, rather than
  be diagnosed. A feature in its own right.

Release note

Releases remain on hold under #60 until Microsoft.Z3 5.x reaches nuget.org, so this reaches main
but not consumers. Nothing about the hold changes.

[github-actions]

Test Results

  1 files  ±0    1 suites  ±0   9s ⏱️ ±0s
279 tests +9  279 ✅ +9  0 💤 ±0  0 ❌ ±0 
290 runs  +9  290 ✅ +9  0 💤 ±0  0 ❌ ±0 

Results for commit 03bc794. ± Comparison against base commit c9035f4.