Report satisfiability separately from the solution

[HowardvanRooijen]

Fixes #57.
Fixes #58.

Answers #28, the original report.

The defect

Solve() reports an unsatisfiable theorem by returning default(T) (Theorem.cs:85-87). For a
reference environment that is null and reads correctly. For a value type it is a fully populated
instance with every symbol zero - which is also the answer to plenty of satisfiable theorems:

using var ctx = new Z3Context();

(from t in ctx.NewTheorem<(int a, int b)>()
 where t.a == t.b && t.a > 4 && t.b < 2      // no solution
 select t).Solve();                          // (0, 0)

(from t in ctx.NewTheorem<(int a, int b)>()
 where t.a == 0 && t.b == 0                  // exactly one solution
 select t).Solve();                          // (0, 0)

Measured, not inferred: those two calls return values that compare equal. And the caller cannot even
ask, because result is null on a non-nullable value type is error CS0037: Cannot convert null to '(int a, int b)' because it is a non-nullable value type.

It is not tuple-specific. A struct and a record struct environment both come back as populated
all-zero instances from an unsatisfiable theorem, so a fix that special-cased ValueTuple would
have looked complete and not been.

The workaround the original report offered does not work. #28 noted that declaring the
environment as (int a, int b)? returns null when unsatisfiable, and suggested it as the way
round. Measured: it returns null for the unsatisfiable case, and throws
ArgumentException: Property set method not found. for a satisfiable one. Nullable<T> exposes
HasValue and Value, both get-only, so the moment there is a solution to write the marshalling
layer fails - and the unsatisfiable case never reaches that code, which is why it looked like it
worked. Before this PR there was no way to distinguish, not even the documented one. Pinned as a
test.

The change

Additive. Solve() behaves exactly as before, so the README samples, the Demo and every existing
test still compile.

Added	For
bool TrySolve(out T) on Theorem<T> and ISolveable<T>	every environment type, including the deferred form an orderby query returns
bool TryOptimize<TResult>(Optimization, Expression<Func<T, TResult>>, out T)	the optimiser's own path, which has its own solve
T? SolveOrNull<T>() where T : struct	lifts a value-type environment to Nullable<T>, so result is null compiles and means what it says
T? OptimizeOrNull<T, TResult>(...) where T : struct	the same, for optimisation

SolveOrNull and OptimizeOrNull are extension methods rather than members because the struct
constraint that makes T? mean Nullable<T> cannot be applied to a member of Theorem<T>, whose
T is unconstrained. SolveOrNull hangs off ISolveable<T>, so it reaches the deferred orderby
form too.

Solve<T> and Optimize<T, TResult> are now thin wrappers over the two Try forms, so there is
one solve path rather than two copies of it.

#58, in the same change

Optimize was declared to return a non-nullable T while returning default! when the status was
not SATISFIABLE. It now returns T?, matching Solve(). That is warning-level for consumers, not
an error - but under this repository's TreatWarningsAsErrors it turned ten unchecked
dereferences across six tests in OptimizationTests.cs into compiler errors, each of them a real
unguarded read of a value the library could return null for. Those tests now assert satisfiability
before reading, as they should always have. That is the clearest evidence the signature was wrong:
the compiler found the callers the moment it was allowed to.

Measured, not counted by eye: deleting the ten guards the fix added and rebuilding produces ten
CS8602s, one per guard.

One part of #58's diagnosis does not survive checking. It says OrderBy/OrderByDescending
inherit the defect "since both wrap Optimize". They do wrap it, but they hand back
ISolveable<T>, whose Solve() has been declared T? since the interface was introduced in
217dc16 - and still is on main. The query-syntax route was always well-typed; only the direct
Optimize call was not. OrderBy_OnAnUnsatisfiableTheorem_ReturnsNull says so in a comment, so
the distinction is pinned rather than lost.

Both issues are fixed together because #57 says they are best designed together, and because any
shape that answers #57 has to cover Optimize and OrderBy anyway - they share GetSolution and
the same default! return.

What is deliberately not changed

Status.UNKNOWN is still reported as "no solution". #57 raises this as a third wrinkle, and it
stays open, for a measured reason: Z3Context builds its context from a fixed { "MODEL", "true" }
and exposes no timeout or rlimit, so a caller cannot ask Z3 to give up. I tried to produce an
UNKNOWN through the public API with a nonlinear integer problem - the sum of three cubes - and it
had not returned after 120 seconds; the process had to be killed. Z3 searched rather than
abandoning. A three-state result would model a state that cannot currently be observed, so
TrySolve returns a bool, and the missing timeout is raised as #85, which gates a proper
answer to the wrinkle.

Solve() keeps its ambiguity rather than being made unambiguous by a breaking change. That was
a deliberate choice of the additive shape; the ambiguity is now documented on Solve itself, in
ISolveable<T>, in a README section, and pinned by a characterisation test that shows the two
theorems returning the same value.

Note for reviewers

ISolveable<T> gains a member. That is source-breaking for anyone who implemented the interface
themselves - unlikely, since it exists to let OrderBy defer, and both implementations are in this
repository - but it is a real break and next-version is already 2.0.

Tests

187 -> 202, in a new UnsatisfiabilityTests.cs, plus the two #58 pins in OptimizationTests.cs
rewritten now that the signature tells the truth.

Every negative is paired with a positive over the same value, because the whole difficulty is
that the two look identical. A test that only checked the unsatisfiable case would pass against an
implementation that always answered "no solution".

Test	What it covers
Solve_UnsatisfiableValueTupleTheorem_ReturnsWhatASatisfiableAllZeroTheoremReturns	the ambiguity itself, as a characterisation - two different theorems, one result
TrySolve_UnsatisfiableValueTupleTheorem_ReturnsFalse / TrySolve_SatisfiableAllZeroValueTupleTheorem_ReturnsTrue	the pair. Both values are (0, 0); only the bool differs
TrySolve_SatisfiableTheorem_ReturnsTheSolutionSolveWouldHaveReturned	the two forms must disagree only about how they report absence
TrySolve_UnsatisfiableReferenceTypeTheorem_ReturnsFalse	keeps both paths answering the same way
TrySolve_UnsatisfiableStructTheorems_ReturnFalse	a struct and a record struct - the problem is the value type, not the tuple
SolveOrNull_UnsatisfiableValueTupleTheorem_ReturnsNull / ..._SatisfiableAllZeroValueTupleTheorem_ReturnsTheAllZeroSolution	the same pair through the Nullable<T> form
TryOptimize_UnsatisfiableTheorem_ReturnsFalse / TryOptimize_SatisfiableTheoremWhoseOptimumIsZero_ReturnsTrue	the same trap on the optimiser's path, where the optimum genuinely is zero
OptimizeOrNull_UnsatisfiableTheorem_ReturnsNull / OptimizeOrNull_SatisfiableTheorem_ReturnsTheOptimum	the optimisation half of the Nullable<T> form
TrySolve_OnADeferredOrderBy_ReportsSatisfiabilityEitherWay	the deferred solvable's own implementation of the interface
SolveOrNull_OnADeferredOrderByDescending_ReturnsTheOptimum	the extension reaching the deferred form
Solve_NullableValueTupleEnvironment_ThrowsWhenTheTheoremIsSatisfiable	the #28 workaround, pinned as the non-answer it is

Mutation results

Mutation	Failures	Which
TrySolve reports satisfiable whatever the status	4	every unsatisfiable case, across value tuple, struct, record struct and reference environments
TrySolve infers satisfiability from the solution instead of the status	2	both all-zero satisfiable cases - and nothing else. This is the mutation those pairs exist for: it passes every other test in the suite
TryOptimize infers satisfiability the same way	2	the optimiser case and the deferred orderby case, confirming the two solve paths are covered independently
The deferred solvable always reports satisfiable	1	the deferred test alone
SolveOrNull / OptimizeOrNull ignore the status they were given	2	both null cases
Revert #58 - Optimize declared non-nullable again	build fails, error CS8603	the signature is load-bearing at compile time, not just documentation

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 202/202 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 77.5% -> 78.2% line (670 of 856), 70.3% -> 70.9% branch (460 of 648).
  SolveableExtensions and DeferredSolvable are both at 100%

Documentation

A When there is no solution section in the README, after the examples: what Solve() returns,
why that is ambiguous for a value type, and the three forms that are not. The remarks on Solve,
Optimize and ISolveable<T> say the same thing at the call site.

New issue

#85 - no way to bound a solve. Z3Context's configuration is fixed, no timeout or rlimit
can be set, and there is no CancellationToken, so an undecidable theorem runs until the process is
killed. Found while testing whether Status.UNKNOWN is reachable; it also explains why it is not.

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   4s ⏱️ -1s
195 tests +15  195 ✅ +15  0 💤 ±0  0 ❌ ±0 
202 runs  +15  202 ✅ +15  0 💤 ±0  0 ❌ ±0 

Results for commit 3b8d54a. ± Comparison against base commit 59b8a9f.

♻️ This comment has been updated with latest results.

[Copilot]

Pull request overview

This PR adds new API surface to report satisfiability separately from the solution value, addressing the ambiguity where Solve()/Optimize() return default(T) for unsatisfiable theorems (indistinguishable from valid all-zero solutions for value-type environments).

Changes:

• Introduces TrySolve(out T) and TryOptimize(..., out T) to return a bool satisfiable flag alongside the solution.
• Adds SolveOrNull() / OptimizeOrNull(...) extension methods to lift value-type environments to Nullable<T> for idiomatic null checks.
• Updates docs and expands test coverage (including characterization tests and deferred orderby paths).

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
solutions/Z3.Linq/Theorem{T}.cs	Adds TrySolve/TryOptimize, updates Optimize nullability, and updates deferred orderby to carry satisfiability.
solutions/Z3.Linq/Theorem.cs	Refactors core solve/optimize paths to implement TrySolve/TryOptimize and have Solve/Optimize wrap them.
solutions/Z3.Linq/SolveableExtensions.cs	Adds SolveOrNull / OptimizeOrNull for value-type environments via Nullable<T>.
solutions/Z3.Linq/ISolveable{T}.cs	Extends the interface with TrySolve(out T) and documents ambiguity of Solve().
solutions/Z3.Linq.Tests/UnsatisfiabilityTests.cs	Adds a comprehensive test suite pinning ambiguity + validating the new APIs across tuples/structs/reference types and deferred orderby.
solutions/Z3.Linq.Tests/OptimizationTests.cs	Updates tests for Optimize now returning T? and adds satisfiability assertions before dereference.
README.md	Documents “When there is no solution” and points users to the new APIs.

Suppressed comments (1)

solutions/Z3.Linq/Theorem{T}.cs:151

• The XML doc <returns> for OrderByDescending is inaccurate: it returns an ISolveable<T> (deferred optimization), not an environment instance. Updating this avoids misleading API documentation.

    /// OrderBy query operator, used to optimize a solution using query expression syntax.
    /// </summary>
    /// <typeparam name="TResult">Type of the value being maximized.</typeparam>
    /// <param name="lambda">Expression representing the value to maximize.</param>
    /// <returns>Environment type instance with properties set to theorem-satisfying values.</returns>
    public ISolveable<T> OrderByDescending<TResult>(Expression<Func<T, TResult>> lambda)
        => new DeferredSolvable(() =>

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[HowardvanRooijen]

Correct on both, and on the suppressed one for OrderByDescending too - fixed in d63ad00.

Both operators return an ISolveable<T>, so the <returns> was describing what Solve on that
value eventually produces rather than what the operator hands back. They now say it is a deferred
minimization/maximization and that nothing reaches Z3 until Solve or TrySolve is called on the
result, which is the part a consumer actually needs to know. While in the same blocks I also fixed
OrderByDescending's summary, which called it "OrderBy query operator".

Worth being precise about why the build missed it: no project here sets GenerateDocumentationFile,
so doc comments are never parsed - but that would not have caught this one either. The XML is well
formed and every cref resolves; the sentence was simply about the wrong thing, and no compiler
setting detects that.

It did prompt me to check the part a setting can catch. With GenerateDocumentationFile turned on
temporarily, the whole solution compiles with no CS1570 and no CS1574 - so nothing is malformed and
every cref in the new API resolves, including TrySolve(out T) and
SolveableExtensions.SolveOrNull{TEnvironment}(ISolveable{TEnvironment}). I confirmed that check
actually reports something before trusting it, by breaking one cref deliberately and watching
CS1574 fire; my first two attempts at that control silently changed nothing, and a clean result
from a check that cannot fail would have been worthless. The project change is reverted - it belongs
to #82.