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. ///