Let a solve be bounded, and say when Z3 could not decide

[HowardvanRooijen]

Fixes #85.

Settles the third wrinkle of #57.

The defect

Z3Context built its native context from a fixed configuration and offered no way to add to it.
No timeout, no resource limit, no CancellationToken - and Check() ran synchronously on the
calling thread. A theorem Z3 cannot decide therefore ran until the process was killed:

using var ctx = new Z3Context();

ctx.NewTheorem<Symbols<int, int, int>>()
   .Where(t => (t.X1 * t.X1 * t.X1) + (t.X2 * t.X2 * t.X2) + (t.X3 * t.X3 * t.X3) == 42)
   .Solve();
// still running after 120 seconds when #85 was raised; killed

And because nothing could bound a solve, Status.UNKNOWN was unreachable, so Theorem.cs
reported it as unsatisfiable - the wrinkle #57 raised and #86 had to leave open.

Measured first, on the raw Microsoft.Z3 API

Before any library change, against the theorem above:

Mechanism	Result	Time
solver parameter timeout = 500	UNKNOWN, reason timeout	592 ms
solver parameter rlimit = 200000	UNKNOWN, reason canceled	58 ms
context configuration timeout = 500	UNKNOWN, reason timeout	532 ms
Context.Interrupt() from another thread after 300 ms	UNKNOWN, reason interrupted	320 ms
optimizer parameter timeout = 500	UNKNOWN, reason canceled	512 ms
optimizer interrupted after 300 ms	UNKNOWN, reason canceled	311 ms
an easy theorem with the timeout set	SATISFIABLE / UNSATISFIABLE as before	9 ms
Interrupt() issued before Check()	SATISFIABLE - the interrupt is lost	6 ms

Two of those rows shaped the design. The reason strings are not consistent - the optimizer says
canceled for a timeout and an interrupt alike, and an exhausted rlimit is canceled on both

• so the library cannot tell cancellation from a limit by reading them. And an interrupt that
  arrives before the check starts does nothing, so an already-cancelled token has to be inspected
  rather than relied on to fire.

The change

Z3Context.Timeout and Z3Context.ResourceLimit, both nullable, both validated in the
setter, applied as parameters on each solver and optimizer rather than baked into the native
context - so they are properties of the Z3Context that can change between solves, and an
undecided solve leaves nothing behind. ResourceLimit is Z3's rlimit: deterministic, reached
at the same point on every machine, in units with no fixed relationship to time.

A CancellationToken on every entry point - Solve, TrySolve, Optimize, TryOptimize,
ISolveable<T>, the deferred orderby form, SolveOrNull and OptimizeOrNull - as an optional
parameter, CancellationToken cancellationToken = default. A cancelled token calls
Context.Interrupt(); the token is also inspected before the check, because of the lost-interrupt
row above. What remains is the moment between that inspection and Z3 starting work, which the
remarks say plainly.

How UNKNOWN is reported, the question #85 deferred to. Put to the maintainer with the
measurements above and chosen over a three-state result:

• a cancelled token throws OperationCanceledException, carrying the token, as everywhere in .NET;
• every other UNKNOWN - a timeout, an exhausted resource limit, or Z3 giving up on its own -
  throws a new TheoremUndecidedException, carrying Z3's reason string;
• TrySolve returning false now means one thing: the theorem was proved to have no solution.

Cancellation is recognised from the token rather than the string, because the strings cannot be
trusted to say which it was.

Public surface

Optional parameters on existing methods: source-compatible for every caller, binary-breaking for
the changed signatures. ISolveable<T> changes shape for the second time in this stack, which
2.0 allows and #86 already did. Z3Context gains two properties; the library gains one exception
type.

The README gets a When Z3 cannot decide section after When there is no solution, with the
theorem above as its example.

Tests

254 → 270, in a new SolveLimitTests.cs. Every test that runs the undecidable theorem carries a
[Timeout], so a regression fails the test rather than hanging the suite - and the whole suite
still finishes in under a second and a half, because the parallel runner overlaps the waits.

Test	What it covers
Solve_UndecidableTheoremWithATimeout_ThrowsTheoremUndecidedException	the issue's theorem, stopped by a timeout; the reason is carried and appears in the message
TrySolve_UndecidableTheoremWithATimeout_ThrowsRatherThanReturningFalse	#57's wrinkle, closed
Solve_UndecidableTheoremWithAResourceLimit_ThrowsTheoremUndecidedException	rlimit, with no timeout set - so it passing proves the limit reaches the solver
Solve_SatisfiableTheoremWithATimeout_StillSolves / TrySolve_UnsatisfiableTheoremWithATimeout_StillReturnsFalse	a limit changes nothing for a theorem Z3 decides within it
Solve_AfterAnUndecidedSolveOnTheSameContext_StillSolves	the limit is per solve; the context stays usable
Solve_WithAnAlreadyCancelledToken_ThrowsOperationCanceledException	the lost-interrupt row; a trivially satisfiable theorem must not solve
Solve_CancelledDuringTheSolve_ThrowsOperationCanceledException	the interrupt, with no limit on the context so only the token can end it; the exception carries the token
Optimize_..WithATimeout.. / Optimize_CancelledDuringTheSolve..	the optimizer's own check, which reports both with a different string
OrderBy_CancelledDuringTheDeferredSolve..	the token reaches the deferred form when it is finally solved
SolveOrNull_CancelledDuringTheSolve..	the extension passes it through
Timeout_SetToANonPositiveValue.. / ResourceLimit_SetToZero.. / Timeout_SetToNull_ClearsTheLimit	the setters

No test asserts on the reason string beyond its presence, for the reason in the table above, and
none asserts on elapsed time.

Mutation results

Chosen so that no mutation can hang the run: the limits themselves are proved by construction
(each limit test sets only the limit it is about), and the mutations target how an UNKNOWN is
reported.

Mutation	Failures	Which
UNKNOWN reported as unsatisfiable again - the pre-#85 code	9	every test that expects an exception, plus the one that solves again afterwards - an interrupted solve came back as "no solution" too
No inspection of the token before the check	1	the already-cancelled-token test alone: the trivially satisfiable theorem solved, because the interrupt fired before the check and was lost
An UNKNOWN is always TheoremUndecidedException; the token never consulted	4	the four cancelled-during tests, which get a TheoremUndecidedException instead of OperationCanceledException

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors and
  documentation generation on; every new cref resolves
• 270/270 locally, 1.4 s
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 88.3% -> 88.7% line (770 of 868), 77.9% -> 78.8% branch (517 of 656)

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 ⏱️ +4s
259 tests +16  259 ✅ +16  0 💤 ±0  0 ❌ ±0 
270 runs  +16  270 ✅ +16  0 💤 ±0  0 ❌ ±0 

Results for commit 3615d7b. ± Comparison against base commit 1a458e4.