test: add xUnit test project with smoke coverage of the theorem API

[jsboige]

Summary

Adds the first xUnit test project to the repository (solutions/Z3.Linq.Tests), wired into Z3.Linq.sln.

Ten facts pin the theorem API as it exists on main today:

• integer and boolean symbols over anonymous-type environments
• chained Where clauses (conjunction)
• multi-symbol tuple theorems with full read-back
• Z3Methods.Distinct
• Optimize in both directions (objective on a symbol and on a tuple expression)
• contradictory constraints → Solve() returns null (pins the unsat contract)
• the NewTheorem<T>(T dummy) overload

Verified locally: 10 passed, 0 failed (dotnet test, net8.0).

Why this first

This is the opening move of the plan discussed on #29 and #43: send things one concern at a time, tests first. A green floor on current main gives the modernisation stack (#44–#110) a regression net to land on — anything that changes the behaviours pinned here shows up as a red test instead of a silent semantic drift.

What is deliberately NOT here

The downstream fork (MyIntelligenceAgency/Z3.Linq, 45 commits ahead, 0 behind) carries 14 more suites, but they exercise APIs main does not have yet (collection handling, positional-record environments, conditional Ite, bit-vector widths, pseudo-boolean ExactlyOne/WeightedAtLeast, solver configuration, UNSAT-core explanations, witness evaluation, rational-exact arithmetic). They would not compile — or would fail by construction — against this base, so each will arrive with its feature PR, one concern at a time. Two notes for the stack specifically:

• the DateTime round-trip suite is red on main today by construction — it is the reproducing evidence for Encode a DateTime as ticks rather than a file time #95 (file-time encoding vs ticks), happy to send it targeted at that branch if useful;
• once the stack lands, the fork's suites double as an independent validation pass of the refactors (that experiment is running on our side and results will be posted on Convert the demos to single-file Spectre.Console apps #110).

Targeting

Opened against main; if a staging branch suits the stack better, retarget or say the word — drift adaptation on our side is agent-driven, matching the workflow you described on #43.

Related: #29 · #43 · #95 · #110

🤖 Generated with Claude Code

[jsboige]

Re-confirmed xUnit harness on tests/port-xunit-harness at commit 314d817 (heads origin/tests/port-xunit-harness and endjin/main fetch verified clean). Local run with .NET 8 runtime installed (latest 8.0.31 plus the just-installed 8.0.13 in ~/.dotnet):

• Restore: OK (Z3.Linq.Tests.csproj net8.0)
• Build: 0 errors, 1 warning (xUnit2002 Do not use Assert.NotNull() on value type on tuple-deconstruction in BasicTheoremTests.cs:56)
• Test: 10 passed, 0 failed, 0 skipped, 286 ms — all smoke facts (integer/boolean symbols over anonymous-type environments, chained Where, tuple multi-symbol, Z3Methods.Distinct, Optimize in both directions, contradictory constraints returning null, NewTheorem(T) overload)

Recommended follow-ups before merge:

1. Trim the warning: replace Assert.NotNull(result) on (int x, int y) tuple by Assert.True(result.x > 0) or drop the check — the analyzer is right that tuples can't be null.
2. MyIntelligenceAgency/Z3.Linq clone behind count: 45 commits on top of endjin/main (the G1-bis #16070 fork work). Feature suites (collections, environments, meal planner, theorem contexts) still live in solutions/Z3.Linq.Tests/-adjacent csproj additions — recommend splitting into one-concern PRs (per the upstream style guide Pinned PRs fix(theorem): partial-eval constraint body before visiting (cross-submission capture) #43-style) once a single suite goes red on endjin/main.
3. CI gating: tests/port-xunit-harness will need a workflow addition on endjin/.github/workflows/build.yml. Locally reproducible (286 ms) — should add <1 min to job duration.

Happy to iterate on (1) if useful — would let this PR ship today as the first CI-checked test in the repository. Branch is at MyIntelligenceAgency/Z3.Linq tests/port-xunit-harness if Howard wants to pull rather than review-via-PR.

cc @idg10 (PR author) @jsboige (downstream-fork shepherd).

[HowardvanRooijen]

I'm still waiting on the internal work to get the latest Z3 package up on nuget. There's been some progress, but it's still a WIP.