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);
}
///