From 4acc6662848b056e8b24665107de30a77e5cec62 Mon Sep 17 00:00:00 2001 From: Howard van Rooijen Date: Tue, 1 Sep 2026 21:29:10 +0100 Subject: [PATCH] Size collections from the instance passed to NewTheorem A collection symbol takes its length from the collection already on the solution instance, and read it with no null check: an environment that declared a collection without initialising it threw a bare NullReferenceException naming nothing. A value tuple could never hold a collection at all - the instance is built with Activator.CreateInstance, and a tuple has nowhere to put an initialiser. The instance passed to NewTheorem(T) is now the template for the solution. It was a parameter named dummy that the method discarded; its collections now give the solution's collections their length, ahead of any initialiser on the type, and it is carried through Where and into the optimiser. Nothing else about it is read. A collection with no length from either source is rejected by name, with the reason. That is what lets a tuple carry a collection, and an anonymous type too - the guard #75 added for anonymous collections is gone, since the template is exactly the initialised instance it was missing. Co-Authored-By: Claude Fable 5.1 --- .../Z3.Linq.Tests/CollectionSymbolTests.cs | 284 ++++++++++++++++-- .../Z3.Linq.Tests/EnvironmentTypeTests.cs | 39 +-- .../Z3.Linq.Tests/TheoremCompositionTests.cs | 7 +- solutions/Z3.Linq/Theorem.cs | 96 ++++-- solutions/Z3.Linq/Theorem{T}.cs | 20 +- solutions/Z3.Linq/Z3Context.cs | 32 +- 6 files changed, 385 insertions(+), 93 deletions(-) diff --git a/solutions/Z3.Linq.Tests/CollectionSymbolTests.cs b/solutions/Z3.Linq.Tests/CollectionSymbolTests.cs index 178b15c..0a9b750 100644 --- a/solutions/Z3.Linq.Tests/CollectionSymbolTests.cs +++ b/solutions/Z3.Linq.Tests/CollectionSymbolTests.cs @@ -8,9 +8,10 @@ namespace Z3.Linq.Tests; /// /// A collection symbol is declared as a Z3 array from Int to the element type's sort - /// the same sort a scalar of that type gets, from the one mapping the two share. Elements are -/// always read back with an integer index, and the number read is the Count of the -/// collection already on the instance - so an environment must pre-size its collections, and a -/// solution never changes their length. +/// always read back with an integer index, and the number read is the Count of a +/// collection that already exists - so an environment must pre-size its collections, on the +/// type or on the instance passed to NewTheorem, and a solution never changes their +/// length. /// /// /// Every element type a scalar supports now round-trips through a collection too. Until #64 @@ -29,8 +30,11 @@ namespace Z3.Linq.Tests; /// /// /// A collection symbol can be a property or a public field, and since #53 the two behave -/// identically. A collection the environment leaves null throws either way, which is #78 - and -/// unavoidable for a ValueTuple, whose elements are fields it has no way to pre-size. +/// identically. Its length comes from an instance: the one passed to NewTheorem, which +/// is the template for the solution, or failing that the type's own initialiser. A collection +/// with neither is rejected by name (#78). The template is what lets a value tuple or an +/// anonymous type carry a collection at all - neither has anywhere to put an initialiser, so it +/// is the only place a length can come from. /// /// [TestClass] @@ -840,61 +844,259 @@ public void Solve_LongArrayInAPublicField_RoundTripsEveryElement() } /// - /// KNOWN DEFECT (#78): a collection that is null on a freshly constructed environment throws - /// . + /// A collection with no length anywhere is rejected by name. /// /// - /// The count is read straight off the value the member holds, with no null check, so an - /// environment that declares a collection without initialising it fails with nothing naming - /// the member at fault. This predates #53 - the property form below has always behaved this - /// way - so fixing #53 gave fields the same behaviour rather than introducing it. - /// These tests pin current behaviour and must be updated when the defect is fixed. + /// The diagnostic half of #78. The count used to be read straight off the value the member + /// held, with no null check, so an environment that declared a collection without + /// initialising it failed with a bare and nothing naming + /// the member at fault. It now says which collection, and what to do about it. This predates + /// #53 - the property form below has always behaved this way - so fixing #53 gave fields the + /// same behaviour rather than introducing it. /// [TestMethod] - public void Solve_NullCollectionInAPublicField_ThrowsNullReferenceException() + public void Solve_NullCollectionInAPublicField_ThrowsNotSupportedExceptionNamingIt() { // Arrange using var context = new Z3Context(); var theorem = context.NewTheorem(); - // Act & Assert - Should.Throw(() => theorem.Solve()); + // Act + NotSupportedException exception = Should.Throw(() => theorem.Solve()); + + // Assert + exception.Message.ShouldStartWith("Collection symbol Values has no length"); + exception.Message.ShouldContain("pre-sized"); + } + + [TestMethod] + public void Solve_NullCollectionInAPublicProperty_ThrowsNotSupportedExceptionNamingIt() + { + // Arrange + using var context = new Z3Context(); + var theorem = context.NewTheorem(); + + // Act + NotSupportedException exception = Should.Throw(() => theorem.Solve()); + + // Assert + exception.Message.ShouldStartWith("Collection symbol Values has no length"); } /// - /// KNOWN DEFECT (#78). The property form, which behaved this way before #53 was fixed too. + /// With several collections, the message names the one without a length. /// + /// + /// The point of naming the member: #78 observed that in an environment with several + /// collections nothing said which one was at fault. The template sizes A and leaves + /// B null, and the message has to say B. + /// [TestMethod] - public void Solve_NullCollectionInAPublicProperty_ThrowsNullReferenceException() + public void Solve_TwoCollectionsWithOneUnsized_NamesTheUnsizedOne() { // Arrange using var context = new Z3Context(); - var theorem = context.NewTheorem(); + var theorem = context.NewTheorem(new TwoNullCollectionsEnvironment { A = new int[1] }) + .Where(t => t.A![0] == 1); - // Act & Assert - Should.Throw(() => theorem.Solve()); + // Act + NotSupportedException exception = Should.Throw(() => theorem.Solve()); + + // Assert + exception.Message.ShouldStartWith("Collection symbol B has no length"); } /// - /// KNOWN DEFECT (#78): a collection in a tuple environment can never work. + /// A collection in a value tuple environment is sized by the template passed to + /// NewTheorem. /// /// - /// A ValueTuple exposes its elements as public fields, so a tuple environment takes the - /// branch #53 fixed. It still cannot hold a collection: the length comes from the instance, - /// the instance is created with Activator.CreateInstance, and a tuple has nowhere to - /// put an initialiser - so the element is always null. #78 is structural for tuples rather - /// than a matter of remembering to initialise something. - /// This test pins current behaviour and must be updated when the defect is fixed. + /// + /// The structural half of #78. A ValueTuple exposes its elements as public fields, so + /// a tuple environment takes the branch #53 fixed - but the solution instance is created + /// with Activator.CreateInstance, and a tuple has nowhere to put an initialiser, so + /// the element was always null and nothing the caller wrote could change that. + /// + /// + /// The instance passed to NewTheorem is now the template for the solution: a + /// collection symbol takes its length from the corresponding collection on the template. + /// That parameter existed already, was named dummy, and was discarded. + /// /// [TestMethod] - public void Solve_CollectionInAValueTupleEnvironment_ThrowsNullReferenceException() + public void Solve_CollectionInAValueTupleEnvironment_IsSizedByTheTemplate() { // Arrange using var context = new Z3Context(); + + // Act + var result = context.NewTheorem((Values: new int[2], Other: 0)) + .Where(t => t.Values[0] == 3) + .Where(t => t.Values[1] == 4) + .Where(t => t.Other == 1) + .Solve(); + + // Assert + result.Values.ShouldBe([3, 4]); + result.Other.ShouldBe(1); + } + + [TestMethod] + public void Solve_CollectionInAValueTupleEnvironmentWithoutATemplate_ThrowsNotSupportedException() + { + // Arrange: the type-only overload has no instance to read a length from, and a tuple + // cannot supply one itself. The tuple's fields are Item1 and Item2 at runtime, whatever + // the source called them. + using var context = new Z3Context(); var theorem = context.NewTheorem<(int[] Values, int Other)>().Where(t => t.Other == 1); - // Act & Assert - Should.Throw(() => theorem.Solve()); + // Act + NotSupportedException exception = Should.Throw(() => theorem.Solve()); + + // Assert + exception.Message.ShouldStartWith("Collection symbol Item1 has no length"); + } + + [TestMethod] + public void Solve_NullCollectionProperty_IsSizedByTheTemplate() + { + // Arrange: a class that declares the collection but never initialises it, sized by the + // instance passed in rather than by an initialiser on the type. + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem(new NullPropertyCollectionEnvironment { Values = new int[3] }) + .Where(t => t.Values![2] == 9) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.Values.ShouldNotBeNull(); + result.Values.Length.ShouldBe(3); + result.Values[2].ShouldBe(9); + } + + [TestMethod] + public void Solve_NullGenericCollection_IsSizedByTheTemplate() + { + // Arrange: the generic-collection branch reads the same length and rebuilds through the + // constructor, so a List is sized the same way. + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem(new NullListCollectionEnvironment { Values = [0, 0] }) + .Where(t => t.Values![1] == 7) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.Values.ShouldNotBeNull(); + result.Values.Count.ShouldBe(2); + result.Values[1].ShouldBe(7); + } + + /// + /// The template is followed into nested objects. + /// + /// + /// The recursion that marshals a nested environment carries the corresponding member of the + /// template alongside it, so a collection two levels down is sized by the collection two + /// levels down on the instance passed in. + /// + [TestMethod] + public void Solve_NullCollectionInANestedObject_IsSizedByTheTemplate() + { + // Arrange + using var context = new Z3Context(); + var template = new NestedNullCollectionEnvironment { Inner = new NullCollectionHolder { Values = new int[2] } }; + + // Act + var result = context.NewTheorem(template) + .Where(t => t.Inner.Values![0] == 3) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.Inner.Values.ShouldNotBeNull(); + result.Inner.Values.Length.ShouldBe(2); + result.Inner.Values[0].ShouldBe(3); + } + + /// + /// A template beats the type's own initialiser. + /// + /// + /// IntArrayEnvironment initialises its collection to three elements; the instance + /// passed in has five. The caller who passes an instance has said what they want more + /// directly than the type has, so the template wins. Without a template the initialiser + /// applies, as every test using the type-only overload shows. + /// + [TestMethod] + public void Solve_TemplateCollection_TakesPrecedenceOverTheInitialiser() + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem(new IntArrayEnvironment { Values = new int[5] }) + .Where(t => t.Values[4] == 1) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.Values.Length.ShouldBe(5); + result.Values[4].ShouldBe(1); + } + + /// + /// Only the template's lengths are used; its element values do not reach the solution, and + /// the template itself is not written to. + /// + [TestMethod] + public void Solve_TemplateElementValues_DoNotReachTheSolution() + { + // Arrange + using var context = new Z3Context(); + var template = new NullPropertyCollectionEnvironment { Values = [99, 99] }; + + // Act + var result = context.NewTheorem(template) + .Where(t => t.Values![0] == 1) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.Values.ShouldNotBeNull(); + result.Values[0].ShouldBe(1); + result.Values.ShouldNotBeSameAs(template.Values); + template.Values.ShouldBe([99, 99]); + } + + /// + /// The template survives Where and OrderBy. + /// + /// + /// Each Where builds a new theorem, and OrderBy defers to a separate solve + /// through the optimiser, so the template has to be carried through both. Every templated + /// test here goes through Where; this is the only one that reads a collection back + /// through the optimiser, so a version that forgot the template on that path would pass + /// every other test in this file. + /// + [TestMethod] + public void OrderByDescending_OnATemplatedTheorem_KeepsTheTemplate() + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem((Values: new int[2], Other: 0)) + .Where(t => t.Values[0] > 0) + .Where(t => t.Values[0] < 10) + .OrderByDescending(t => t.Values[0]) + .Solve(); + + // Assert + result.Values[0].ShouldBe(9); } /// @@ -1103,4 +1305,26 @@ private sealed class NullPropertyCollectionEnvironment { public int[]? Values { get; set; } } + + private sealed class NullListCollectionEnvironment + { + public List? Values { get; set; } + } + + private sealed class TwoNullCollectionsEnvironment + { + public int[]? A { get; set; } + + public int[]? B { get; set; } + } + + private sealed class NullCollectionHolder + { + public int[]? Values { get; set; } + } + + private sealed class NestedNullCollectionEnvironment + { + public NullCollectionHolder Inner { get; set; } = new(); + } } diff --git a/solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs b/solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs index 2dc6fbe..ca1ac65 100644 --- a/solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs +++ b/solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs @@ -16,10 +16,11 @@ namespace Z3.Linq.Tests; /// named one does, nested objects included. Until then the anonymous path carried a marshaller /// of its own that handled bool and int only, and evaluated a property's handle /// before checking its type - so a nested object, whose handle is null, reached Z3 and came back -/// as a bare NullReferenceException. The one shape still refused is a collection: the -/// instance passed to NewTheorem is discarded, so nothing can pre-size it, and it is -/// rejected by name. A value tuple looks like an anonymous type in source but is an ordinary -/// framework type, so it takes the second path. +/// as a bare NullReferenceException. A collection takes its length from the instance +/// passed to NewTheorem, which #78 made the template for the solution - an anonymous +/// instance is created uninitialised, so that is the only place its length can come from. A +/// value tuple looks like an anonymous type in source but is an ordinary framework type, so it +/// takes the second path. /// /// /// Note that Symbols<T1, T2, T3, T4> does not exist - the family provides arities @@ -256,31 +257,33 @@ public void Solve_AnonymousTypeWithANestedAnonymousType_PopulatesIt() } /// - /// A collection in an anonymous environment is rejected by name. + /// A collection in an anonymous environment is sized by the instance passed to + /// NewTheorem. /// /// - /// The one shape the shared marshaller cannot serve here. It reads the element count from - /// the collection already on the instance, and an anonymous instance is created uninitialised - /// - the one passed to NewTheorem is discarded - so there is nothing to read. Without - /// the guard this would be #78's on the count; with it, - /// the message says which member and why. Pinned because dropping the guard passes every - /// other test in this file. + /// Refused by name between #75 and #78: an anonymous instance is created uninitialised, so + /// the marshaller had no collection to read a length from, and the instance passed to + /// NewTheorem - which had one - was discarded. #78 made that instance the template + /// for the solution, and with it an anonymous environment can hold a collection like any + /// other. /// [TestMethod] - public void Solve_AnonymousTypeWithACollectionProperty_ThrowsNotSupportedException() + public void Solve_AnonymousTypeWithACollectionProperty_SizesItFromTheTemplate() { // Arrange using var context = new Z3Context(); - var theorem = context.NewTheorem(new { v = new int[2], n = default(int) }) - .Where(t => t.v[0] == 3) - .Where(t => t.n == 1); // Act - NotSupportedException exception = Should.Throw(() => theorem.Solve()); + var result = context.NewTheorem(new { v = new int[2], n = default(int) }) + .Where(t => t.v[0] == 3) + .Where(t => t.v[1] == 5) + .Where(t => t.n == 1) + .Solve(); // Assert - exception.Message.ShouldContain("v"); - exception.Message.ShouldContain("pre-sized"); + result.ShouldNotBeNull(); + result.v.ShouldBe([3, 5]); + result.n.ShouldBe(1); } [TestMethod] diff --git a/solutions/Z3.Linq.Tests/TheoremCompositionTests.cs b/solutions/Z3.Linq.Tests/TheoremCompositionTests.cs index 99cc59f..82f637a 100644 --- a/solutions/Z3.Linq.Tests/TheoremCompositionTests.cs +++ b/solutions/Z3.Linq.Tests/TheoremCompositionTests.cs @@ -165,10 +165,11 @@ public void Dispose_CalledOnContext_LeavesTheContextUsable() } [TestMethod] - public void NewTheorem_WithDummyInstance_InfersTheEnvironmentType() + public void NewTheorem_WithATemplateInstance_InfersTheEnvironmentType() { - // Arrange: the dummy overload exists so anonymous types can be used inline - // (Z3Context.cs:69). The instance itself is never read. + // Arrange: the instance overload exists so anonymous types can be used inline. Since #78 + // the instance is also the template for the solution, but only the lengths of its + // collections are read; with none, as here, it does nothing but supply the type. using var context = new Z3Context(); // Act diff --git a/solutions/Z3.Linq/Theorem.cs b/solutions/Z3.Linq/Theorem.cs index 3c784a7..f8b8d3f 100644 --- a/solutions/Z3.Linq/Theorem.cs +++ b/solutions/Z3.Linq/Theorem.cs @@ -22,6 +22,11 @@ public class Theorem /// private readonly IEnumerable constraints; + /// + /// The instance passed to NewTheorem, if any, whose collections give theirs a length. + /// + private readonly object? template; + /// /// Z3 context under which the theorem is solved. /// @@ -32,7 +37,7 @@ public class Theorem /// /// Z3 context. protected Theorem(Z3Context context) - : this(context, new List()) + : this(context, new List(), null) { } @@ -42,9 +47,24 @@ protected Theorem(Z3Context context) /// Z3 context. /// Constraints to apply to the created theorem. protected Theorem(Z3Context context, IEnumerable constraints) + : this(context, constraints, null) + { + } + + /// + /// Creates a new pre-constrained theorem for the given Z3 context, with a template instance. + /// + /// Z3 context. + /// Constraints to apply to the created theorem. + /// + /// An instance of the environment type whose collections supply a length to the solution's, + /// or . See #78. + /// + protected Theorem(Z3Context context, IEnumerable constraints, object? template) { this.context = context; this.constraints = constraints; + this.template = template; } /// @@ -52,6 +72,11 @@ protected Theorem(Z3Context context, IEnumerable constraints) /// protected IEnumerable Constraints => constraints; + /// + /// Gets the template instance the theorem was created from, if any. + /// + protected object? Template => template; + /// /// Gets the Z3 context under which the theorem is solved. /// @@ -105,7 +130,7 @@ protected bool TrySolve([MaybeNullWhen(false)] out T result) return false; } - result = GetSolution(ctx, solver.Model, environment); + result = GetSolution(ctx, solver.Model, environment, this.template); return true; } @@ -170,7 +195,7 @@ protected bool TryOptimize( return false; } - result = GetSolution(ctx, optimizer.Model, environment); + result = GetSolution(ctx, optimizer.Model, environment, this.template); return true; } @@ -388,7 +413,7 @@ private Environment GetEnvironment(Context context, MemberInfo parameter, string return toReturn; } - private static object ConvertZ3Expression(object destinationObject, Context context, Model model, Environment subEnv, MemberInfo parameter) + private static object ConvertZ3Expression(object destinationObject, Context context, Model model, Environment subEnv, MemberInfo parameter, object? templateValue) { // Normalize types when facing Z3. Theorem variable type mappings allow for strong // typing within the theorem, while underlying variable representations are Z3- @@ -426,17 +451,19 @@ private static object ConvertZ3Expression(object destinationObject, Context cont var results = new ArrayList(); - //todo: deal with length in a more robust way - - int existingLength = parameter switch + // A solution never changes the length of a collection, so the length has to come + // from somewhere: the collection on the template passed to NewTheorem, or failing + // that the one already on the instance - its initialiser. A value tuple has nowhere + // to put an initialiser and an anonymous instance is created uninitialised, so for + // those the template is the only source. With neither, say so by name rather than + // fail on the null. See #53 and #78. + if ((templateValue ?? GetMemberValue(parameter, destinationObject)) is not ICollection existing) { - // Both branches read the value the member holds on the instance. The field - // branch used to cast the FieldInfo itself, which no environment could - // satisfy - see #53. - PropertyInfo property => ((ICollection)property.GetValue(destinationObject, null)!).Count, - FieldInfo field => ((ICollection)field.GetValue(destinationObject)!).Count, - _ => 0 - }; + throw new NotSupportedException( + $"Collection symbol {parameter.Name} has no length. A collection must be pre-sized: initialise it on the environment type, or pass an instance with it initialised to NewTheorem."); + } + + int existingLength = existing.Count; for (int i = 0; i < existingLength; i++) { @@ -496,7 +523,7 @@ private static object ConvertZ3Expression(object destinationObject, Context cont } else { - value = GetSolution(parameterType, context, model, subEnv); + value = GetSolution(parameterType, context, model, subEnv, templateValue); } } else @@ -599,6 +626,20 @@ private static object ConvertZ3Expression(object destinationObject, Context cont /// Z3 model to evaluate theorem parameters under. /// Environment with bindings of theorem variables to Z3 handles. /// Instance of the environment type with theorem-satisfying values. + /// + /// Reads off , or returns + /// if there is no instance to read it from. + /// + private static object? GetMemberValue(MemberInfo member, object? instance) + { + return instance is null ? null : member switch + { + PropertyInfo property => property.GetValue(instance), + FieldInfo field => field.GetValue(instance), + _ => null, + }; + } + /// /// Whether is one the library treats as a collection symbol: an /// array, or a generic type implementing . @@ -608,10 +649,10 @@ private static bool IsCollection(Type type) return type.IsArray || (type.IsGenericType && typeof(IEnumerable).IsAssignableFrom(type.GetGenericTypeDefinition())); } - private static T GetSolution(Context context, Model model, Environment environment) + private static T GetSolution(Context context, Model model, Environment environment, object? template) { Type t = typeof(T); - return (T) GetSolution(t, context, model, environment); + return (T) GetSolution(t, context, model, environment, template); } /// @@ -621,8 +662,9 @@ private static T GetSolution(Context context, Model model, Environment enviro /// Z3 context. /// Z3 model to evaluate theorem parameters under. /// Environment with bindings of theorem variables to Z3 handles. + /// An instance of whose collections give the solution's their length, or null. /// Instance of the environment type with theorem-satisfying values. - private static object GetSolution(Type t, Context context, Model model, Environment environment) + private static object GetSolution(Type t, Context context, Model model, Environment environment, object? template) { // Determine whether T is a compiler-generated type, indicating an anonymous type. // This check might not be reliable enough but works for now. @@ -658,17 +700,9 @@ private static object GetSolution(Type t, Context context, Model model, Environm // before checking the type - so a nested object, whose handle is null, reached Z3 // and surfaced as a NullReferenceException. See #75. // - // A collection is the one thing the shared path cannot do for an anonymous type: - // the element count is read from the collection already on the instance, and the - // instance here is uninitialised - the one passed to NewTheorem is discarded - so - // there is nothing to read it from. Reject it by name rather than let that read - // fail on a null. - if (IsCollection(parameter.PropertyType)) - { - throw new NotSupportedException("Unsupported parameter type for " + parameter.Name + ": a collection in an anonymous environment cannot be pre-sized."); - } - - field.SetValue(result, ConvertZ3Expression(result, context, model, subEnv, parameter)); + // The instance here is uninitialised, so a collection on it has no length of its own; + // the one on the template - the instance passed to NewTheorem - supplies it. See #78. + field.SetValue(result, ConvertZ3Expression(result, context, model, subEnv, parameter, GetMemberValue(parameter, template))); } return result; @@ -694,7 +728,7 @@ private static object GetSolution(Type t, Context context, Model model, Environm var subEnv = environment.Properties[prop]; - value = ConvertZ3Expression(result, context, model, subEnv, prop); + value = ConvertZ3Expression(result, context, model, subEnv, prop, GetMemberValue(prop, template)); prop.SetValue(result, value, null); } @@ -713,7 +747,7 @@ private static object GetSolution(Type t, Context context, Model model, Environm var subEnv = environment.Properties[prop]; - value = ConvertZ3Expression(result, context, model, subEnv, prop); + value = ConvertZ3Expression(result, context, model, subEnv, prop, GetMemberValue(prop, template)); prop.SetValue(result, value); } diff --git a/solutions/Z3.Linq/Theorem{T}.cs b/solutions/Z3.Linq/Theorem{T}.cs index 8dfafe7..ede28c9 100644 --- a/solutions/Z3.Linq/Theorem{T}.cs +++ b/solutions/Z3.Linq/Theorem{T}.cs @@ -21,13 +21,27 @@ internal Theorem(Z3Context context) { } + /// + /// Creates a new theorem for the given Z3 context, from a template instance. + /// + /// Z3 context. + /// + /// An instance of whose collections supply a length to the + /// solution's. See #78. + /// + internal Theorem(Z3Context context, T template) + : base(context, new List(), template) + { + } + /// /// Creates a new pre-constrained theorem for the given Z3 context. /// /// Z3 context. /// Constraints to apply to the created theorem. - internal Theorem(Z3Context context, IEnumerable constraints) - : base(context, constraints) + /// The template instance of the theorem being extended, or null. + internal Theorem(Z3Context context, IEnumerable constraints, object? template) + : base(context, constraints, template) { } @@ -128,7 +142,7 @@ public bool TryOptimize( /// Theorem with the new constraint applied. public Theorem Where(Expression> constraint) { - return new Theorem(base.Context, base.Constraints.Concat(new List { constraint })); + return new Theorem(base.Context, base.Constraints.Concat(new List { constraint }), base.Template); } /// diff --git a/solutions/Z3.Linq/Z3Context.cs b/solutions/Z3.Linq/Z3Context.cs index ca5f6c7..13f1c21 100644 --- a/solutions/Z3.Linq/Z3Context.cs +++ b/solutions/Z3.Linq/Z3Context.cs @@ -52,23 +52,39 @@ public Theorem NewTheorem() } /// - /// Creates a new theorem based on a skeleton object used to infer the environment - /// type with the variables constrained by the theorem. - /// - /// This overload is useful if one wants to use an anonymous type "on the fly" to - /// create a new theorem based on the type's properties as variables. + /// Creates a new theorem from a template instance, which supplies the environment type and + /// the length of any collection symbols in it. /// + /// + /// + /// The type is inferred from the instance, which is what lets an anonymous type be used as + /// an environment "on the fly". The instance is also the template for the solution: a + /// collection symbol takes its length from the corresponding collection on the template, + /// because a solution never changes a collection's length and has to get it from somewhere. + /// That is what lets a value tuple or an anonymous type - neither of which has anywhere to + /// put an initialiser - hold a collection at all. Where the type has an initialiser of its + /// own the template still wins. See #78. + /// + /// + /// Nothing else about the template is read. Its values do not constrain the theorem and do + /// not reach the solution, and it is never written to. + /// + /// /// /// /// ctx.NewTheorem(new { x = default(int), y = default(int) }).Where(t => t.x > t.y) + /// ctx.NewTheorem((Values: new int[3], Total: 0)).Where(t => t.Values[0] + t.Values[1] + t.Values[2] == t.Total) /// /// /// Theorem environment type (typically inferred). - /// Dummy parameter, typically an anonymous type instance. + /// + /// An instance of the environment type. Its collections give the solution's their length; + /// nothing else about it is used. + /// /// New theorem object based on the given environment. - public Theorem NewTheorem(T dummy) + public Theorem NewTheorem(T template) { - return new Theorem(this); + return new Theorem(this, template); } ///