diff --git a/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs b/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs index e058428..69dd071 100644 --- a/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs +++ b/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs @@ -11,11 +11,11 @@ namespace Z3.Linq.Tests; /// which solution was chosen. /// /// -/// One of the types listed as supported still does not work, and is pinned as a characterisation -/// test rather than skipped - short (#63). It fails in the marshalling layer, which no example in -/// the repository exercises, which is why it went unnoticed. float was a second until #54 was -/// fixed, and DateTime a third until #56 - that one returned a value rather than throwing, so it -/// took a test asserting the value to find it at all. +/// Every type listed as supported now works. Three did not when this file was written: short +/// (#63), float (#54) and DateTime (#56). All three failed in the marshalling layer, which no +/// example in the repository exercises, which is why they went unnoticed. DateTime is the one +/// worth remembering - it returned a value rather than throwing, so only a test asserting the +/// value could find it at all. /// /// [TestClass] @@ -160,25 +160,192 @@ public void Solve_DoubleSymbolWithInequality_SatisfiesTheConstraint() } /// - /// KNOWN DEFECT (#63): no theorem over a short symbol can be solved. + /// A short symbol round-trips the value it was constrained to. /// /// - /// A short symbol is created with MkIntConst, but C# widens short to int for the comparison - /// and ExpressionVisitor.VisitUnary reads that Convert node as a real-to-int conversion, - /// casting the IntExpr to RealExpr (ExpressionVisitor.cs:132). A second defect waits behind - /// it: TypeCode.Int16 marshals to an int, which a short property rejects. - /// This test pins current behaviour and must be updated when the defect is fixed. + /// The case in #63, which had to be fixed twice over. C# widens short to int + /// for the comparison, and the visitor read that Convert node as a real-to-int + /// conversion and cast the IntExpr to RealExpr; behind that, + /// TypeCode.Int16 shared the Int32 arm of the marshalling switch and handed + /// reflection an int, which a short member rejects. Neither defect was + /// reachable while the other stood. + /// + [TestMethod] + [DataRow((short)0, DisplayName = "Zero")] + [DataRow((short)42, DisplayName = "Positive")] + [DataRow((short)-42, DisplayName = "Negative")] + [DataRow(short.MaxValue, DisplayName = "Int16.MaxValue")] + [DataRow(short.MinValue, DisplayName = "Int16.MinValue")] + public void Solve_ShortSymbol_RoundTripsTheValue(short value) + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == value) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(value); + } + + /// + /// A short symbol whose model value no short can hold fails loudly. + /// + /// + /// + /// The symbol is an unbounded MkIntConst - nothing tells Z3 the value has to fit in + /// 16 bits - so a constraint written against the widened int can be satisfied by a + /// number the member cannot hold. The read is a checked cast, which throws; an unchecked one + /// would wrap 40000 to -25536 and hand back a wrong answer that looks like a right one. + /// + /// + /// C# blocks the direct spelling of this - t.X1 == 40000 against a short is + /// error CS0652 - so it takes an int variable to reach. Pinned because the + /// choice between wrapping and throwing is the whole point of the arm, and a later + /// simplification to a plain cast would pass every other test in this file. See #63, and + /// #87 for bounding the symbol so Z3 cannot pick the value in the first place. + /// /// [TestMethod] - public void Solve_ShortSymbol_ThrowsInvalidCastException() + public void Solve_ShortSymbolConstrainedOutsideShortRange_ThrowsOverflowException() { // Arrange using var context = new Z3Context(); - var theorem = context.NewTheorem>() - .Where(t => t.X1 == 7); + int beyondShortRange = 40000; + var theorem = context.NewTheorem>() + .Where(t => t.X1 == beyondShortRange); // Act & Assert - Should.Throw(() => theorem.Solve()); + Should.Throw(() => theorem.Solve()); + } + + /// + /// short symbols work in arithmetic, not only in a bare equality. + /// + /// + /// The fix guards a Convert node, and C# emits one wherever a short is used in + /// arithmetic - so a fix that covered only the comparison form would leave this failing. + /// + [TestMethod] + public void Solve_ShortSymbolsInArithmetic_RoundTripTheValues() + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 + t.X2 == 10) + .Where(t => t.X1 == 4) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe((short)4); + result.X2.ShouldBe((short)6); + } + + /// + /// A short symbol can be compared against an int one. + /// + /// + /// Both sides widen to int, so this is the case where the guard has to leave one + /// operand alone and still produce a well-sorted comparison. + /// + [TestMethod] + public void Solve_ShortSymbolComparedToAnIntSymbol_RoundTripsBoth() + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == t.X2) + .Where(t => t.X2 == 9) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe((short)9); + result.X2.ShouldBe(9); + } + + /// + /// An enum symbol round-trips the member it was constrained to. + /// + /// + /// + /// An enum's TypeCode is that of its underlying type, so is + /// Int32 and takes the same path a short does - which is why the same guard + /// fixes both, as #63 records. + /// + /// + /// Unlike short, an enum needs nothing on the marshalling side: the model value is an + /// int, and reflection converts an int to an enum member on its own. #63 + /// predicted a second defect here and there is not one - measured, not assumed. + /// + /// + [TestMethod] + [DataRow(DayOfWeek.Sunday, DisplayName = "Underlying value zero")] + [DataRow(DayOfWeek.Monday, DisplayName = "Positive")] + [DataRow(DayOfWeek.Saturday, DisplayName = "Largest member")] + public void Solve_EnumSymbol_RoundTripsTheValue(DayOfWeek value) + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem() + .Where(t => t.Day == value) + .Where(t => t.Other == 1) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.Day.ShouldBe(value); + result.Other.ShouldBe(1); + } + + /// + /// An explicit (int) cast of a real-sorted symbol still converts. + /// + /// + /// + /// The other side of the guard #63 added. That guard makes the Int32 arm of the + /// conversion switch conditional on the operand's Z3 sort: an integer passes through, a real + /// goes to MkReal2Int. Only the first half is exercised by the short and enum + /// tests above, so without this one a guard widened to return the operand unconditionally + /// would pass the whole suite and silently stop converting reals. + /// + /// + /// Worth knowing that this path had no test before #63 either. It was reachable only from a + /// widening the visitor misread, so every execution of it threw - it was covered without + /// ever having worked. + /// + /// + [TestMethod] + public void Solve_DoubleSymbolCastToInt_ConvertsRatherThanPassingThrough() + { + // Arrange + using var context = new Z3Context(); + + // Act: the second constraint is what makes the truncation observable. Z3.s real-to-int + // is a floor, so together these ask for a real in (3.5, 4). Pass the operand through + // unconverted and they read as X1 == 3 and X1 > 3.5, which has no solution at all - so + // this fails by returning null rather than by returning a wrong number. + var result = context.NewTheorem>() + .Where(t => (int)t.X1 == 3) + .Where(t => t.X1 > 3.5) + .Where(t => t.X2 == 1) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBeGreaterThan(3.5); + result.X1.ShouldBeLessThan(4d); + result.X2.ShouldBe(1); } /// @@ -508,18 +675,17 @@ public void Solve_MixedTypeSymbols_MarshalsEveryPropertyIndependently() /// /// /// - /// The tests above pin what each type does with a value; these seven pin what each does with + /// The tests above pin what each type does with a value; these eight pin what each does with /// no value at all. Every type takes a different arm of the marshalling switch, so each can /// regress on its own, and all but bool threw before #51. The value a free symbol /// comes back with is supplied by model completion and is deliberately not asserted. /// /// - /// short is absent on purpose: an unconstrained one evaluates cleanly and then fails - /// at the reflection write, which is #63 rather than anything to do with completion. Its pin - /// above is unchanged. float failed the same way until #54 was fixed, and now has a - /// case here like every other working type. DateTime never threw here, but read back - /// in local time until #56, so its case asserts the kind rather than only that a result - /// appeared. + /// Two of the eight could not be written when this family was: float and short + /// both evaluated cleanly under completion and then failed at the reflection write, which + /// was #54 and #63 rather than anything to do with completion. DateTime never threw + /// here, but read back in local time until #56, so its case asserts the kind rather than + /// only that a result appeared. /// /// [TestMethod] @@ -662,4 +828,36 @@ public void Solve_UnconstrainedDateTimeSymbol_ReturnsAResult() // path, so it can be asserted where the value cannot. result.X1.Kind.ShouldBe(DateTimeKind.Utc); } + + /// + /// An unconstrained short symbol is populated rather than throwing. + /// + /// + /// short could not be in this family until #63: it evaluated cleanly under completion + /// and then failed at the reflection write, so its absence here said nothing about + /// completion. It takes the Int16 arm of the marshalling switch, which no other test + /// in this family reaches. + /// + [TestMethod] + public void Solve_UnconstrainedShortSymbol_ReturnsAResult() + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X2 == 0) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X2.ShouldBe(0); + } + + private sealed class EnumEnvironment + { + public DayOfWeek Day { get; set; } + + public int Other { get; set; } + } } diff --git a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs index 2a980ed..8051e7f 100644 --- a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs +++ b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs @@ -114,26 +114,36 @@ public void Solve_NullableProperty_ThrowsArgumentException() } /// - /// KNOWN DEFECT (#63): an enum symbol fails the same way a short does. + /// An enum whose underlying type is not one the environment builder maps is rejected by + /// name, before anything is translated. /// /// - /// An enum's TypeCode is that of its underlying type, so the symbol is created as an - /// integer - and then C# emits a Convert to int for the comparison, which - /// ExpressionVisitor.cs:132 reads as a real-to-int conversion and casts to RealExpr. Same - /// root cause as short, so the same fix covers both. - /// This test pins current behaviour and must be updated when the defect is fixed. + /// + /// An enum is only ever as supported as its underlying type. #63 fixed the int-backed + /// case - and friends - which is now round-tripped in + /// SymbolTypeMarshallingTests. A byte-backed enum is TypeCode.Byte, + /// which the sort mapping has never handled, so it stops at the same guard that rejects a + /// bare byte or uint. + /// + /// + /// This is the outcome #63 asked for where a type genuinely is not supported: a + /// naming the member, rather than an + /// from inside the visitor. Pinned so the distinction + /// between the two enum cases does not quietly collapse. + /// /// [TestMethod] - public void Solve_EnumProperty_ThrowsInvalidCastException() + public void Solve_EnumPropertyWithAnUnsupportedUnderlyingType_ThrowsNotSupportedException() { // Arrange using var context = new Z3Context(); - var theorem = context.NewTheorem() - .Where(t => t.Day == DayOfWeek.Monday) + var theorem = context.NewTheorem() + .Where(t => t.Size == ByteBackedEnum.Large) .Where(t => t.Other == 1); // Act & Assert - Should.Throw(() => theorem.Solve()); + Should.Throw(() => theorem.Solve()) + .Message.ShouldContain("Size"); } [TestMethod] @@ -188,9 +198,15 @@ private sealed class NullableEnvironment public int Other { get; set; } } - private sealed class EnumEnvironment + private enum ByteBackedEnum : byte { - public DayOfWeek Day { get; set; } + Small = 1, + Large = 2, + } + + private sealed class ByteEnumEnvironment + { + public ByteBackedEnum Size { get; set; } public int Other { get; set; } } diff --git a/solutions/Z3.Linq/ExpressionVisitor.cs b/solutions/Z3.Linq/ExpressionVisitor.cs index 0824642..2d60cbc 100644 --- a/solutions/Z3.Linq/ExpressionVisitor.cs +++ b/solutions/Z3.Linq/ExpressionVisitor.cs @@ -117,17 +117,15 @@ private static Expr VisitConvert(Context context, Environment environment, Unary var inner = Visit(context, environment, expression.Operand, param); - switch (Type.GetTypeCode(expression.Operand.Type)) - { - case TypeCode.Int16: - case TypeCode.Int32: - break; - } - switch (Type.GetTypeCode(expression.Type)) { case TypeCode.Double: return context.MkInt2Real((IntExpr)inner); + case TypeCode.Int32 when inner.IsInt: + // A widening onto a value Z3 already holds at integer sort is a no-op: short to + // int, or an enum to its underlying int. Only a real operand needs converting, + // and reading the target type alone cannot tell the two apart. See #63. + return inner; case TypeCode.Int32: return context.MkReal2Int((RealExpr)inner); case TypeCode.Char: diff --git a/solutions/Z3.Linq/Theorem.cs b/solutions/Z3.Linq/Theorem.cs index b7f7377..6959c71 100644 --- a/solutions/Z3.Linq/Theorem.cs +++ b/solutions/Z3.Linq/Theorem.cs @@ -560,6 +560,13 @@ private static object ConvertZ3Expression(object destinationObject, Context cont value = val.String; break; case TypeCode.Int16: + // Int16 cannot share the Int32 arm: the model value is an int, and reflection + // refuses to write an int to a short member. The cast is checked because the + // symbol is an unbounded MkIntConst, so Z3 may return a value no short can + // hold - an unchecked cast would wrap it into a plausible wrong answer. + // See #63. + value = checked((short)((IntNum)val).Int); + break; case TypeCode.Int32: value = ((IntNum)val).Int; break;