From 3615d7b5e4b4ef7204b10a698a5d96cebd532742 Mon Sep 17 00:00:00 2001 From: Howard van Rooijen Date: Tue, 1 Sep 2026 21:59:28 +0100 Subject: [PATCH] Let a solve be bounded, and say when Z3 could not decide Z3Context built its native context from a fixed configuration and offered nothing to add to it: no timeout, no resource limit, no CancellationToken. A theorem Z3 cannot decide - nonlinear integer arithmetic is undecidable in general - ran until the process was killed. And because nothing could bound a solve, Status.UNKNOWN was unreachable and was reported as unsatisfiable. Z3Context gains Timeout and ResourceLimit, applied as parameters on each solver and optimizer so they can change between solves. Every entry point takes an optional CancellationToken, wired to Context.Interrupt; the token is also inspected before the check, because an interrupt that arrives before Z3 starts is lost - measured on the raw API. An UNKNOWN is now an exception. A cancelled token throws OperationCanceledException; anything else - a limit reached, or Z3 giving up - throws TheoremUndecidedException with Z3's reason. The reason strings cannot distinguish the two (the optimizer says "canceled" for both), so the token decides. TrySolve returning false now means only that the theorem was proved to have no solution, which closes the wrinkle #57 raised and #86 had to leave open. Co-Authored-By: Claude Fable 5.1 --- README.md | 39 +++ solutions/Z3.Linq.Tests/SolveLimitTests.cs | 303 ++++++++++++++++++ solutions/Z3.Linq.Tests/TheoremSolveTests.cs | 9 +- solutions/Z3.Linq/ISolveable{T}.cs | 23 +- solutions/Z3.Linq/SolveableExtensions.cs | 15 +- solutions/Z3.Linq/Theorem.cs | 102 +++++- .../Z3.Linq/TheoremUndecidedException.cs | 40 +++ solutions/Z3.Linq/Theorem{T}.cs | 81 +++-- solutions/Z3.Linq/Z3Context.cs | 94 ++++++ 9 files changed, 658 insertions(+), 48 deletions(-) create mode 100644 solutions/Z3.Linq.Tests/SolveLimitTests.cs create mode 100644 solutions/Z3.Linq/TheoremUndecidedException.cs diff --git a/README.md b/README.md index 988789d..dc56aac 100644 --- a/README.md +++ b/README.md @@ -196,6 +196,45 @@ var solveable = from t in ctx.NewTheorem<(int a, int b)>() if (solveable.TrySolve(out var cheapest)) { /* ... */ } ``` +### When Z3 cannot decide + +Some theorems cannot be decided. Nonlinear integer arithmetic is undecidable in general, and a +theorem such as *three integers whose cubes sum to 42* leaves Z3 searching until the process is +killed - the constraints look no more exotic than the ones above. Bound the solve with a +`Timeout`, or with a `ResourceLimit`, which counts Z3's own units of work and so is reached at the +same point on every machine: + +```csharp +using (var ctx = new Z3Context { Timeout = TimeSpan.FromSeconds(5) }) +{ + var theorem = from t in ctx.NewTheorem>() + where (t.X1 * t.X1 * t.X1) + (t.X2 * t.X2 * t.X2) + (t.X3 * t.X3 * t.X3) == 42 + select t; + + try + { + var result = theorem.Solve(); + } + catch (TheoremUndecidedException e) + { + Console.WriteLine($"Z3 stopped: {e.Reason}"); // Z3 stopped: timeout + } +} +``` + +Every solve and optimisation also takes a `CancellationToken`, which interrupts Z3 and throws +`OperationCanceledException` as usual: + +```csharp +using var cancellation = new CancellationTokenSource(TimeSpan.FromSeconds(5)); + +var result = theorem.Solve(cancellation.Token); +``` + +A theorem Z3 decides within the limit is unaffected, and `TrySolve` returning `false` still means +exactly one thing: the theorem was proved to have no solution. A solve that stops without deciding +throws, so it can never be mistaken for one. + ## Getting Started You can install the [Z3.Linq NuGet Package](https://www.nuget.org/packages/Z3.Linq/). diff --git a/solutions/Z3.Linq.Tests/SolveLimitTests.cs b/solutions/Z3.Linq.Tests/SolveLimitTests.cs new file mode 100644 index 0000000..0d8f961 --- /dev/null +++ b/solutions/Z3.Linq.Tests/SolveLimitTests.cs @@ -0,0 +1,303 @@ +namespace Z3.Linq.Tests; + +/// +/// Bounding a solve: , and +/// the every solve and optimisation accepts. +/// +/// +/// +/// Nonlinear integer arithmetic is undecidable in general, and the theorem these tests use - +/// three integers whose cubes sum to 42 - is the one #85 measured as still searching after two +/// minutes. Before #85 nothing in the API could stop it. Every test that runs it carries a +/// , so a regression fails the test rather than hanging the suite. +/// +/// +/// How Z3 stops is reported by exception, never by : a cancelled token is +/// , and everything else - a limit reached, or Z3 giving +/// up - is . That settles the wrinkle #57 deferred: the +/// from TrySolve means "proved to have no solution" and nothing +/// else. Z3 describes why it stopped as a string, and the strings differ between the solver and +/// the optimizer for the same limit, so no test asserts on them beyond their presence. +/// +/// +/// The limits are small - half a second, a modest resource budget - because the point is that +/// they are reached, not how long that takes. Nothing here asserts on elapsed time. +/// +/// +[TestClass] +public class SolveLimitTests +{ + private const int HangGuardMilliseconds = 60_000; + + [TestMethod] + [Timeout(HangGuardMilliseconds)] + public void Solve_UndecidableTheoremWithATimeout_ThrowsTheoremUndecidedException() + { + // Arrange + using var context = new Z3Context { Timeout = TimeSpan.FromMilliseconds(500) }; + var theorem = SumOfThreeCubes(context); + + // Act + TheoremUndecidedException exception = Should.Throw(() => theorem.Solve()); + + // Assert + exception.Reason.ShouldNotBeNullOrEmpty(); + exception.Message.ShouldContain(exception.Reason); + } + + /// + /// A solve that stopped without deciding throws rather than returning . + /// + /// + /// The wrinkle #57 raised and #85 deferred: TrySolve used to return + /// for Status.UNKNOWN as well as for unsatisfiable, which was + /// defensible only while nothing could produce an unknown. Now something can, and + /// has to mean what it says. + /// + [TestMethod] + [Timeout(HangGuardMilliseconds)] + public void TrySolve_UndecidableTheoremWithATimeout_ThrowsRatherThanReturningFalse() + { + // Arrange + using var context = new Z3Context { Timeout = TimeSpan.FromMilliseconds(500) }; + var theorem = SumOfThreeCubes(context); + + // Act & Assert + Should.Throw(() => theorem.TrySolve(out _)); + } + + /// + /// A resource limit stops the same theorem, deterministically. + /// + /// + /// Z3's rlimit counts work rather than time, so the same theorem does the same amount + /// of it on every machine. Measured, this budget is exhausted in tens of milliseconds. + /// + [TestMethod] + [Timeout(HangGuardMilliseconds)] + public void Solve_UndecidableTheoremWithAResourceLimit_ThrowsTheoremUndecidedException() + { + // Arrange + using var context = new Z3Context { ResourceLimit = 200_000 }; + var theorem = SumOfThreeCubes(context); + + // Act & Assert + Should.Throw(() => theorem.Solve()); + } + + [TestMethod] + public void Solve_SatisfiableTheoremWithATimeout_StillSolves() + { + // Arrange: a limit changes nothing for a theorem Z3 decides within it. + using var context = new Z3Context { Timeout = TimeSpan.FromMilliseconds(500) }; + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == 3) + .Where(t => t.X2 == t.X1 + 1) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(3); + result.X2.ShouldBe(4); + } + + [TestMethod] + public void TrySolve_UnsatisfiableTheoremWithATimeout_StillReturnsFalse() + { + // Arrange: false still means proved unsatisfiable, limit or no limit. + using var context = new Z3Context { Timeout = TimeSpan.FromMilliseconds(500) }; + var theorem = context.NewTheorem>() + .Where(t => t.X1 == 3) + .Where(t => t.X1 == 4); + + // Act + bool satisfiable = theorem.TrySolve(out _); + + // Assert + satisfiable.ShouldBeFalse(); + } + + /// + /// The context stays usable after a solve is cut short. + /// + /// + /// The limit is applied to each solve, not baked into the native context, so an undecided + /// solve leaves nothing behind - the next theorem on the same context solves normally. + /// + [TestMethod] + [Timeout(HangGuardMilliseconds)] + public void Solve_AfterAnUndecidedSolveOnTheSameContext_StillSolves() + { + // Arrange + using var context = new Z3Context { Timeout = TimeSpan.FromMilliseconds(500) }; + Should.Throw(() => SumOfThreeCubes(context).Solve()); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == 7) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(7); + } + + /// + /// An already-cancelled token throws before any work is done. + /// + /// + /// Measured on the raw API: an interrupt issued before the check starts is lost, so a token + /// that is cancelled on the way in has to be inspected rather than relied on to fire. The + /// theorem here is trivially satisfiable and would solve in milliseconds; it must not. + /// + [TestMethod] + public void Solve_WithAnAlreadyCancelledToken_ThrowsOperationCanceledException() + { + // Arrange + using var context = new Z3Context(); + using var cancellation = new CancellationTokenSource(); + cancellation.Cancel(); + var theorem = context.NewTheorem>().Where(t => t.X1 == 3); + + // Act + OperationCanceledException exception = + Should.Throw(() => theorem.Solve(cancellation.Token)); + + // Assert + exception.CancellationToken.ShouldBe(cancellation.Token); + } + + [TestMethod] + [Timeout(HangGuardMilliseconds)] + public void Solve_CancelledDuringTheSolve_ThrowsOperationCanceledException() + { + // Arrange: no limit on the context, so only the token can end this. + using var context = new Z3Context(); + using var cancellation = new CancellationTokenSource(TimeSpan.FromMilliseconds(300)); + var theorem = SumOfThreeCubes(context); + + // Act + OperationCanceledException exception = + Should.Throw(() => theorem.Solve(cancellation.Token)); + + // Assert + exception.CancellationToken.ShouldBe(cancellation.Token); + } + + [TestMethod] + [Timeout(HangGuardMilliseconds)] + public void Optimize_UndecidableTheoremWithATimeout_ThrowsTheoremUndecidedException() + { + // Arrange: the optimizer has its own check, and reports the limit with a different + // string from the solver - which is why the library decides by what it asked for. + using var context = new Z3Context { Timeout = TimeSpan.FromMilliseconds(500) }; + var theorem = SumOfThreeCubes(context); + + // Act + TheoremUndecidedException exception = + Should.Throw(() => theorem.Optimize(Optimization.Minimize, t => t.X1)); + + // Assert + exception.Reason.ShouldNotBeNullOrEmpty(); + } + + [TestMethod] + [Timeout(HangGuardMilliseconds)] + public void Optimize_CancelledDuringTheSolve_ThrowsOperationCanceledException() + { + // Arrange + using var context = new Z3Context(); + using var cancellation = new CancellationTokenSource(TimeSpan.FromMilliseconds(300)); + var theorem = SumOfThreeCubes(context); + + // Act + OperationCanceledException exception = Should.Throw( + () => theorem.TryOptimize(Optimization.Minimize, t => t.X1, out _, cancellation.Token)); + + // Assert + exception.CancellationToken.ShouldBe(cancellation.Token); + } + + /// + /// The deferred form an orderby query returns takes the token when it is finally + /// solved. + /// + [TestMethod] + [Timeout(HangGuardMilliseconds)] + public void OrderBy_CancelledDuringTheDeferredSolve_ThrowsOperationCanceledException() + { + // Arrange + using var context = new Z3Context(); + using var cancellation = new CancellationTokenSource(TimeSpan.FromMilliseconds(300)); + ISolveable> deferred = SumOfThreeCubes(context).OrderBy(t => t.X1); + + // Act + OperationCanceledException exception = + Should.Throw(() => deferred.TrySolve(out _, cancellation.Token)); + + // Assert + exception.CancellationToken.ShouldBe(cancellation.Token); + } + + /// + /// The Nullable-lifting extension passes the token through. + /// + [TestMethod] + [Timeout(HangGuardMilliseconds)] + public void SolveOrNull_CancelledDuringTheSolve_ThrowsOperationCanceledException() + { + // Arrange + using var context = new Z3Context(); + using var cancellation = new CancellationTokenSource(TimeSpan.FromMilliseconds(300)); + var theorem = context.NewTheorem<(int a, int b, int c)>() + .Where(t => (t.a * t.a * t.a) + (t.b * t.b * t.b) + (t.c * t.c * t.c) == 42); + + // Act & Assert + Should.Throw(() => theorem.SolveOrNull(cancellation.Token)); + } + + [TestMethod] + [DataRow(0L, DisplayName = "Zero")] + [DataRow(-1L, DisplayName = "Negative")] + public void Timeout_SetToANonPositiveValue_ThrowsArgumentOutOfRangeException(long ticks) + { + // Arrange + using var context = new Z3Context(); + + // Act & Assert + Should.Throw(() => context.Timeout = TimeSpan.FromTicks(ticks)); + } + + [TestMethod] + public void ResourceLimit_SetToZero_ThrowsArgumentOutOfRangeException() + { + // Arrange + using var context = new Z3Context(); + + // Act & Assert + Should.Throw(() => context.ResourceLimit = 0); + } + + [TestMethod] + public void Timeout_SetToNull_ClearsTheLimit() + { + // Arrange + using var context = new Z3Context { Timeout = TimeSpan.FromSeconds(1) }; + + // Act + context.Timeout = null; + + // Assert + context.Timeout.ShouldBeNull(); + } + + private static Theorem> SumOfThreeCubes(Z3Context context) + { + // x^3 + y^3 + z^3 == 42 over the integers. A solution exists - it was found in 2019 and + // has eighteen digits - but Z3 has no way to reach it, and no way to prove there is none. + return context.NewTheorem>() + .Where(t => (t.X1 * t.X1 * t.X1) + (t.X2 * t.X2 * t.X2) + (t.X3 * t.X3 * t.X3) == 42); + } +} diff --git a/solutions/Z3.Linq.Tests/TheoremSolveTests.cs b/solutions/Z3.Linq.Tests/TheoremSolveTests.cs index 67c2b8c..267043c 100644 --- a/solutions/Z3.Linq.Tests/TheoremSolveTests.cs +++ b/solutions/Z3.Linq.Tests/TheoremSolveTests.cs @@ -13,10 +13,11 @@ namespace Z3.Linq.Tests; /// packages daily on this repository. /// /// -/// Unsatisfiable cases are deliberately kept trivial. Solve returns default for -/// both Status.UNSATISFIABLE and Status.UNKNOWN (Theorem.cs:85-87), so a theorem -/// that was merely slow would pass an "is unsatisfiable" assertion. Keeping these obviously -/// contradictory removes that risk. +/// Unsatisfiable cases are deliberately kept trivial. Since #85 a solve that stops without +/// deciding throws TheoremUndecidedException rather than reporting the theorem +/// unsatisfiable, so a merely slow theorem can no longer pass an "is unsatisfiable" assertion by +/// accident - but only once a limit is set, and none is set here. Keeping these obviously +/// contradictory keeps them fast as well as right. /// /// /// A symbol the returned model does not interpret takes an arbitrary value supplied by Z3's diff --git a/solutions/Z3.Linq/ISolveable{T}.cs b/solutions/Z3.Linq/ISolveable{T}.cs index 7153795..b7ef184 100644 --- a/solutions/Z3.Linq/ISolveable{T}.cs +++ b/solutions/Z3.Linq/ISolveable{T}.cs @@ -1,6 +1,8 @@ namespace Z3.Linq { + using System; using System.Diagnostics.CodeAnalysis; + using System.Threading; /// /// Enables optimization constraints as expressed by OrderBy to be deferred, just like @@ -12,24 +14,39 @@ public interface ISolveable /// /// Solves the theorem. /// + /// A token that interrupts the solve. /// /// Environment type instance with properties set to theorem-satisfying values, or /// default(T) if the theorem cannot be satisfied. /// + /// + /// Z3 stopped without deciding: a limit on the was reached, or it + /// gave up. See #85. + /// + /// was cancelled. /// /// For a value-type environment default(T) is a populated all-zero instance and /// cannot be told apart from a solution in which every symbol is zero. Use - /// , or SolveOrNull, where that matters. See #57. + /// , or SolveOrNull, where that + /// matters. See #57. /// - T? Solve(); + T? Solve(CancellationToken cancellationToken = default); /// /// Solves the theorem, reporting satisfiability separately from the solution. /// /// The solution, when the theorem could be satisfied. + /// A token that interrupts the solve. /// /// if the theorem was satisfiable; otherwise . + /// A solve that stopped without deciding throws rather than returning + /// . /// - bool TrySolve([MaybeNullWhen(false)] out T result); + /// + /// Z3 stopped without deciding: a limit on the was reached, or it + /// gave up. See #85. + /// + /// was cancelled. + bool TrySolve([MaybeNullWhen(false)] out T result, CancellationToken cancellationToken = default); } } diff --git a/solutions/Z3.Linq/SolveableExtensions.cs b/solutions/Z3.Linq/SolveableExtensions.cs index 021f2f4..9e5915d 100644 --- a/solutions/Z3.Linq/SolveableExtensions.cs +++ b/solutions/Z3.Linq/SolveableExtensions.cs @@ -27,14 +27,17 @@ public static class SolveableExtensions /// /// Value-type environment over which the theorem is defined. /// The theorem, or a deferred optimisation over one. + /// A token that interrupts the solve. /// The solution, or if the theorem cannot be satisfied. /// is null. - public static TEnvironment? SolveOrNull(this ISolveable solveable) + /// Z3 stopped without deciding. See #85. + /// was cancelled. + public static TEnvironment? SolveOrNull(this ISolveable solveable, CancellationToken cancellationToken = default) where TEnvironment : struct { ArgumentNullException.ThrowIfNull(solveable); - return solveable.TrySolve(out TEnvironment solution) ? solution : null; + return solveable.TrySolve(out TEnvironment solution, cancellationToken) ? solution : null; } /// @@ -46,16 +49,20 @@ public static class SolveableExtensions /// The theorem to optimize over. /// The optimization goal, i.e. whether to minimize or maximize the solution. /// Expression representing the value to minimize or maximize. + /// A token that interrupts the optimisation. /// The optimal solution, or if the theorem cannot be satisfied. /// is null. + /// Z3 stopped without deciding. See #85. + /// was cancelled. public static TEnvironment? OptimizeOrNull( this Theorem theorem, Optimization direction, - Expression> lambda) + Expression> lambda, + CancellationToken cancellationToken = default) where TEnvironment : struct { ArgumentNullException.ThrowIfNull(theorem); - return theorem.TryOptimize(direction, lambda, out TEnvironment solution) ? solution : null; + return theorem.TryOptimize(direction, lambda, out TEnvironment solution, cancellationToken) ? solution : null; } } diff --git a/solutions/Z3.Linq/Theorem.cs b/solutions/Z3.Linq/Theorem.cs index 14b647d..a02f019 100644 --- a/solutions/Z3.Linq/Theorem.cs +++ b/solutions/Z3.Linq/Theorem.cs @@ -96,14 +96,15 @@ public override string ToString() /// /// Theorem environment type. /// Result of solving the theorem; default(T) if the theorem cannot be satisfied. + /// A token that interrupts the solve. /// /// For a value-type environment default(T) is a real, populated instance - all zeroes - /// and so cannot be told apart from a solution in which every symbol happens to be zero. Use - /// where that matters. See #57. + /// where that matters. See #57. /// - protected T? Solve() + protected T? Solve(CancellationToken cancellationToken) { - return this.TrySolve(out T? result) ? result : default; + return this.TrySolve(out T? result, cancellationToken) ? result : default; } /// @@ -111,8 +112,11 @@ public override string ToString() /// /// Theorem environment type. /// The solution, when the theorem could be satisfied. + /// A token that interrupts the solve. /// if the theorem was satisfiable; otherwise . - protected bool TrySolve([MaybeNullWhen(false)] out T result) + /// Z3 stopped without deciding - a limit on the was reached, or it gave up. + /// was cancelled. + protected bool TrySolve([MaybeNullWhen(false)] out T result, CancellationToken cancellationToken) { using Context ctx = this.context.CreateContext(); var environment = GetEnvironment(ctx, typeof(T)); @@ -122,7 +126,7 @@ protected bool TrySolve([MaybeNullWhen(false)] out T result) AssertConstraints(ctx, solver, environment); - Status status = solver.Check(); + Status status = this.Check(ctx, solver, cancellationToken); if (status != Status.SATISFIABLE) { @@ -142,14 +146,16 @@ protected bool TrySolve([MaybeNullWhen(false)] out T result) /// The optimization goal, i.e. whether to minimize or maximize the solution. /// Expression representing the value to minimize or maximize. /// Result of solving the theorem; default(T) if the theorem cannot be satisfied. + /// A token that interrupts the optimisation. /// - /// Carries the same ambiguity as for a value-type environment. Use - /// + /// Carries the same ambiguity as for a value-type + /// environment. Use + /// /// where that matters. See #57. /// - protected T? Optimize(Optimization direction, Expression> lambda) + protected T? Optimize(Optimization direction, Expression> lambda, CancellationToken cancellationToken) { - return this.TryOptimize(direction, lambda, out T? result) ? result : default; + return this.TryOptimize(direction, lambda, out T? result, cancellationToken) ? result : default; } /// @@ -160,11 +166,15 @@ protected bool TrySolve([MaybeNullWhen(false)] out T result) /// The optimization goal, i.e. whether to minimize or maximize the solution. /// Expression representing the value to minimize or maximize. /// The optimal solution, when the theorem could be satisfied. + /// A token that interrupts the optimisation. /// if the theorem was satisfiable; otherwise . + /// Z3 stopped without deciding - a limit on the was reached, or it gave up. + /// was cancelled. protected bool TryOptimize( Optimization direction, Expression> lambda, - [MaybeNullWhen(false)] out T result) + [MaybeNullWhen(false)] out T result, + CancellationToken cancellationToken) { using Context ctx = this.context.CreateContext(); var environment = GetEnvironment(ctx, typeof(T)); @@ -187,7 +197,7 @@ protected bool TryOptimize( throw new ArgumentOutOfRangeException(nameof(direction), direction, null); } - Status status = optimizer.Check(); + Status status = this.Check(ctx, optimizer, cancellationToken); if (status != Status.SATISFIABLE) { @@ -199,6 +209,76 @@ protected bool TryOptimize( return true; } + /// + /// Runs the check on a solver or optimizer under the limits set on the + /// and the caller's token, and turns an undecided outcome into an exception. + /// + /// The native context the check runs in. + /// The or to check. + /// A token that interrupts the check. + /// or - never . + /// + /// + /// A cancelled token interrupts Z3 through . An interrupt that + /// arrives before the check has started is lost - measured, not assumed - so the token is + /// also inspected before the check, which leaves only the moment between that inspection and + /// Z3 starting work. + /// + /// + /// Z3 says why it stopped as a string, and the strings are not consistent: the solver says + /// timeout or interrupted, the optimizer says canceled for either, and an + /// exhausted resource limit is canceled on both. So cancellation is recognised from the + /// token rather than the string, and every other is a + /// carrying the string. Before #85 an + /// was reported as unsatisfiable, which was defensible only + /// because nothing could cause one. + /// + /// + private Status Check(Context ctx, Z3Object approach, CancellationToken cancellationToken) + { + cancellationToken.ThrowIfCancellationRequested(); + + Params? limits = this.context.CreateLimits(ctx); + + switch (approach) + { + case Solver solver when limits is not null: + solver.Parameters = limits; + break; + case Optimize optimizer when limits is not null: + optimizer.Parameters = limits; + break; + } + + Status status; + + using (cancellationToken.Register(ctx.Interrupt)) + { + cancellationToken.ThrowIfCancellationRequested(); + + status = approach switch + { + Solver solver => solver.Check(), + Optimize optimizer => optimizer.Check(), + _ => throw new ArgumentException("Expected a Solver or an Optimize.", nameof(approach)), + }; + } + + if (status == Status.UNKNOWN) + { + cancellationToken.ThrowIfCancellationRequested(); + + throw new TheoremUndecidedException(approach switch + { + Solver solver => solver.ReasonUnknown, + Optimize optimizer => optimizer.ReasonUnknown, + _ => "unknown", + }); + } + + return status; + } + /// /// Asserts the theorem constraints on the Z3 context. /// diff --git a/solutions/Z3.Linq/TheoremUndecidedException.cs b/solutions/Z3.Linq/TheoremUndecidedException.cs new file mode 100644 index 0000000..e610d4f --- /dev/null +++ b/solutions/Z3.Linq/TheoremUndecidedException.cs @@ -0,0 +1,40 @@ +namespace Z3.Linq; + +using System; + +/// +/// Z3 stopped without deciding whether the theorem is satisfiable. +/// +/// +/// +/// Thrown when a solve or optimisation ends with Z3 reporting unknown: the +/// or was reached, or Z3 +/// gave up on a problem it cannot decide. The theorem has been proved neither satisfiable nor +/// unsatisfiable, which is why this is an exception rather than a from +/// TrySolve - means the theorem has no solution, and this means +/// nobody knows. See #57 and #85. +/// +/// +/// A solve cut short by a throws +/// instead, as everywhere else in .NET. +/// +/// +public class TheoremUndecidedException : Exception +{ + /// + /// Creates the exception. + /// + /// Z3's own account of why it stopped. + public TheoremUndecidedException(string reason) + : base($"Z3 could not decide whether the theorem is satisfiable ({reason}). A timeout or resource limit set on the Z3Context was reached, or Z3 gave up; the theorem has been proved neither satisfiable nor unsatisfiable.") + { + this.Reason = reason; + } + + /// + /// Gets Z3's own account of why it stopped - timeout, canceled and + /// interrupted are the usual ones, and which of them a given limit produces differs + /// between the solver and the optimiser. + /// + public string Reason { get; } +} diff --git a/solutions/Z3.Linq/Theorem{T}.cs b/solutions/Z3.Linq/Theorem{T}.cs index ede28c9..fdd203f 100644 --- a/solutions/Z3.Linq/Theorem{T}.cs +++ b/solutions/Z3.Linq/Theorem{T}.cs @@ -48,18 +48,26 @@ internal Theorem(Z3Context context, IEnumerable constraints, o /// /// Solves the theorem. /// + /// A token that interrupts the solve. /// /// Environment type instance with properties set to theorem-satisfying values, or /// default(T) if the theorem cannot be satisfied. /// + /// + /// Z3 stopped without deciding: the or + /// was reached, or Z3 gave up. Without a limit, a theorem + /// Z3 cannot decide runs until the process is killed. See #85. + /// + /// was cancelled. /// /// /// Where is a value type - a value tuple, a struct, a record struct - /// default(T) is a populated instance with every symbol zero, which is also a perfectly /// good solution to some theorems. The two cannot be told apart here, and the result cannot - /// even be compared against . Use , or - /// , when - /// the difference matters. See #57. + /// even be compared against . Use + /// , or + /// , + /// when the difference matters. See #57. /// /// /// A symbol that no constraint mentions is free: the theorem is still satisfiable, and Z3 @@ -74,26 +82,33 @@ internal Theorem(Z3Context context, IEnumerable constraints, o /// working in local time needs on the way out. /// /// - public T? Solve() + public T? Solve(CancellationToken cancellationToken = default) { - return base.Solve(); + return base.Solve(cancellationToken); } /// /// Solves the theorem, reporting satisfiability separately from the solution. /// /// The solution, when the theorem could be satisfied. + /// A token that interrupts the solve. /// /// if the theorem was satisfiable; otherwise . /// + /// + /// Z3 stopped without deciding: the or + /// was reached, or Z3 gave up. See #85. + /// + /// was cancelled. /// /// The only form that answers "is there a solution?" for every environment type. What is /// written into when this returns is exactly - /// what would have returned. + /// what would have returned. means the theorem was + /// proved to have no solution - a solve that stopped without deciding throws instead. /// - public bool TrySolve([MaybeNullWhen(false)] out T result) + public bool TrySolve([MaybeNullWhen(false)] out T result, CancellationToken cancellationToken = default) { - return base.TrySolve(out result); + return base.TrySolve(out result, cancellationToken); } /// @@ -102,19 +117,25 @@ public bool TrySolve([MaybeNullWhen(false)] out T result) /// Type of the value being optimized. /// The optimization goal, i.e. whether to minimize or maximize the solution. /// Expression representing the value to minimize or maximize. + /// A token that interrupts the optimisation. /// /// Environment type instance with properties set to theorem-satisfying values, or /// default(T) if the theorem cannot be satisfied. /// + /// + /// Z3 stopped without deciding: the or + /// was reached, or Z3 gave up. See #85. + /// + /// was cancelled. /// /// Carries the same ambiguity as , and answers it the same way - through - /// . As - /// with , a symbol that no constraint mentions is free and takes an + /// . + /// As with , a symbol that no constraint mentions is free and takes an /// arbitrary value; the objective determines only what it is written in terms of. /// - public T? Optimize(Optimization direction, Expression> lambda) + public T? Optimize(Optimization direction, Expression> lambda, CancellationToken cancellationToken = default) { - return base.Optimize(direction, lambda); + return base.Optimize(direction, lambda, cancellationToken); } /// @@ -124,15 +145,22 @@ public bool TrySolve([MaybeNullWhen(false)] out T result) /// The optimization goal, i.e. whether to minimize or maximize the solution. /// Expression representing the value to minimize or maximize. /// The optimal solution, when the theorem could be satisfied. + /// A token that interrupts the optimisation. /// /// if the theorem was satisfiable; otherwise . /// + /// + /// Z3 stopped without deciding: the or + /// was reached, or Z3 gave up. See #85. + /// + /// was cancelled. public bool TryOptimize( Optimization direction, Expression> lambda, - [MaybeNullWhen(false)] out T result) + [MaybeNullWhen(false)] out T result, + CancellationToken cancellationToken = default) { - return base.TryOptimize(direction, lambda, out result); + return base.TryOptimize(direction, lambda, out result, cancellationToken); } /// @@ -152,11 +180,11 @@ public Theorem Where(Expression> constraint) /// Expression representing the value to minimize. /// /// A deferred minimization. Nothing reaches Z3 until or - /// is called on the result. + /// is called on the result. /// public ISolveable OrderBy(Expression> lambda) - => new DeferredSolvable(() => - TryOptimize(Optimization.Minimize, lambda, out T? solution) ? (true, solution) : (false, default)); + => new DeferredSolvable(cancellationToken => + TryOptimize(Optimization.Minimize, lambda, out T? solution, cancellationToken) ? (true, solution) : (false, default)); /// /// OrderByDescending query operator, used to optimize a solution using query expression syntax. @@ -165,11 +193,11 @@ public ISolveable OrderBy(Expression> lambda) /// Expression representing the value to maximize. /// /// A deferred maximization. Nothing reaches Z3 until or - /// is called on the result. + /// is called on the result. /// public ISolveable OrderByDescending(Expression> lambda) - => new DeferredSolvable(() => - TryOptimize(Optimization.Maximize, lambda, out T? solution) ? (true, solution) : (false, default)); + => new DeferredSolvable(cancellationToken => + TryOptimize(Optimization.Maximize, lambda, out T? solution, cancellationToken) ? (true, solution) : (false, default)); /// /// An optimisation that has not run yet. @@ -177,22 +205,23 @@ public ISolveable OrderByDescending(Expression> lam /// /// The deferred call carries satisfiability alongside the solution rather than returning the /// solution alone, because for a value-type environment the solution on its own cannot say - /// whether there was one. See #57. + /// whether there was one. See #57. The token is the caller's, supplied when the deferred + /// solve is finally asked for, so it reaches the optimizer like any other. See #85. /// private sealed class DeferredSolvable : ISolveable { - private readonly Func<(bool Satisfiable, T? Solution)> optimize; + private readonly Func optimize; - public DeferredSolvable(Func<(bool Satisfiable, T? Solution)> optimize) + public DeferredSolvable(Func optimize) { this.optimize = optimize; } - public T? Solve() => this.optimize().Solution; + public T? Solve(CancellationToken cancellationToken = default) => this.optimize(cancellationToken).Solution; - public bool TrySolve([MaybeNullWhen(false)] out T result) + public bool TrySolve([MaybeNullWhen(false)] out T result, CancellationToken cancellationToken = default) { - (bool satisfiable, T? solution) = this.optimize(); + (bool satisfiable, T? solution) = this.optimize(cancellationToken); result = solution!; return satisfiable; } diff --git a/solutions/Z3.Linq/Z3Context.cs b/solutions/Z3.Linq/Z3Context.cs index 13f1c21..d87bc36 100644 --- a/solutions/Z3.Linq/Z3Context.cs +++ b/solutions/Z3.Linq/Z3Context.cs @@ -33,6 +33,69 @@ public Z3Context() /// public TextWriter? Log { get; set; } + /// + /// Gets or sets how long a single solve or optimisation may run before Z3 gives up, or + /// for no limit. + /// + /// + /// + /// Some theorems cannot be decided - nonlinear integer arithmetic is undecidable in general - + /// and without a limit Z3 searches until the process is killed. When the limit is reached the + /// solve throws : the theorem has been proved neither + /// satisfiable nor unsatisfiable. A theorem Z3 can decide within the limit is unaffected. + /// See #85. + /// + /// + /// Wall-clock time, so the same theorem may or may not hit the limit on a different machine. + /// is the deterministic alternative. + /// + /// + /// + /// The value is not positive, or exceeds what Z3 can represent in milliseconds. + /// + public TimeSpan? Timeout + { + get => this.timeout; + set + { + if (value is { } t && (t <= TimeSpan.Zero || t.TotalMilliseconds > uint.MaxValue)) + { + throw new ArgumentOutOfRangeException(nameof(value), value, "The timeout must be positive and no more than uint.MaxValue milliseconds."); + } + + this.timeout = value; + } + } + + /// + /// Gets or sets how much work Z3 may do on a single solve or optimisation before giving up, + /// in Z3's own resource units, or for no limit. + /// + /// + /// The deterministic sibling of : the same theorem does the same amount + /// of work everywhere, so a limit that is reached on one machine is reached on all of them. + /// The unit is Z3's rlimit, which has no fixed relationship to time. When the limit is + /// reached the solve throws . See #85. + /// + /// The value is zero. + public uint? ResourceLimit + { + get => this.resourceLimit; + set + { + if (value is 0) + { + throw new ArgumentOutOfRangeException(nameof(value), value, "The resource limit must be positive."); + } + + this.resourceLimit = value; + } + } + + private TimeSpan? timeout; + + private uint? resourceLimit; + /// /// Closes the native resources held by the Z3 theorem prover. /// @@ -96,6 +159,37 @@ internal Context CreateContext() return new Context(config); } + /// + /// The solver parameters carrying and , or + /// when neither is set. + /// + /// The native context the parameters are created in. + /// + /// Applied per solver rather than through the context configuration, so that a limit is a + /// property of the that can be changed between solves. + /// + internal Params? CreateLimits(Context context) + { + if (this.timeout is null && this.resourceLimit is null) + { + return null; + } + + Params limits = context.MkParams(); + + if (this.timeout is { } t) + { + limits.Add("timeout", (uint)t.TotalMilliseconds); + } + + if (this.resourceLimit is { } r) + { + limits.Add("rlimit", r); + } + + return limits; + } + /// /// Helpers to write diagnostic log output to the registered logger, if any. ///