diff --git a/solutions/Z3.Linq.Tests/NumericConversionTests.cs b/solutions/Z3.Linq.Tests/NumericConversionTests.cs new file mode 100644 index 0000000..57fc48c --- /dev/null +++ b/solutions/Z3.Linq.Tests/NumericConversionTests.cs @@ -0,0 +1,245 @@ +namespace Z3.Linq.Tests; + +/// +/// Numeric conversions inside a constraint: the ones the C# compiler inserts when two operands +/// have different types, and the ones a caller writes as a cast. +/// +/// +/// +/// Every mixed-type comparison or arithmetic expression carries a Convert node the caller +/// never wrote - t.X1 == f against a double symbol and a float variable is +/// t.X1 == (double)f to the expression tree. In Z3 such a conversion is one of exactly +/// three things: a no-op when both types map to the same sort, integer-to-real, or +/// real-to-integer. Which one depends on the sorts, and the visitor asks the same mapping the +/// symbols are declared with. +/// +/// +/// Until #76 the visitor chose from the target type alone - int-to-real for every conversion to +/// double, real-to-int for every conversion to int - and had no case at all for +/// long, float or decimal. So a float variable could not be compared +/// against a double symbol, two symbols of different real types could not be related, and +/// a long symbol could not be compared to an int one. #63 fixed the int +/// arm the same way earlier in this stack; this finishes the job across the switch. +/// +/// +/// The real-to-integer direction is covered by +/// SymbolTypeMarshallingTests.Solve_DoubleSymbolCastToInt_ConvertsRatherThanPassingThrough, +/// which needs a constraint the truncation can be observed through and lives beside the +/// marshalling tests it shares that trick with. +/// +/// +[TestClass] +public class NumericConversionTests +{ + /// + /// The case in #76: a double symbol compared against a float variable. + /// + /// + /// A float literal in the same position is folded to a double constant before + /// the visitor sees it, which is why this needs a variable to reproduce - and why it went + /// unnoticed. The operand translates to a real, and the old double arm cast it to + /// IntExpr on the assumption that anything converted to a double must have been an + /// integer. + /// + [TestMethod] + public void Solve_DoubleSymbolComparedToAFloatVariable_RoundTripsTheValue() + { + // Arrange + using var context = new Z3Context(); + float value = 1.5f; + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == value) + .Where(t => t.X2 == 1) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(1.5); + } + + /// + /// Two symbols of different real types can be related to each other. + /// + /// + /// Stronger than the issue's repro, and the one that matters in practice: nothing about + /// Symbols<double, float> suggests its two members cannot appear in the same + /// constraint, yet every comparison between them widened the float and failed. + /// + [TestMethod] + public void Solve_DoubleSymbolComparedToAFloatSymbol_RelatesTheTwo() + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == t.X2) + .Where(t => t.X2 == 1.5f) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(1.5); + result.X2.ShouldBe(1.5f); + } + + [TestMethod] + public void Solve_DoubleSymbolInArithmeticWithAFloatSymbol_RelatesTheTwo() + { + // Arrange: the conversion sits under a multiplication rather than directly under the + // comparison, so the visitor meets it with an arithmetic parent. + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == t.X2 * 2) + .Where(t => t.X2 == 1.5f) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(3.0); + } + + /// + /// The widening the old double arm was written for still works. + /// + /// + /// An int operand converted to double is the one integer-to-real case the + /// visitor always handled. It is here so the fix cannot be a regression in disguise: a + /// version that returned every operand unchanged would pass the float tests above and fail + /// this one with a sort mismatch. + /// + [TestMethod] + public void Solve_DoubleSymbolComparedToAnIntSymbol_RelatesTheTwo() + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == t.X2) + .Where(t => t.X2 == 7) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(7.0); + result.X2.ShouldBe(7); + } + + /// + /// A decimal symbol can be compared to an int one. + /// + /// + /// There was no arm for a conversion to decimal at all, so this fell through to the + /// catch-all as . It is the same integer-to-real + /// conversion as the double case, because decimal and double map to the + /// same sort - which is exactly what choosing by sort rather than by type buys. + /// + [TestMethod] + public void Solve_DecimalSymbolComparedToAnIntSymbol_RelatesTheTwo() + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == t.X2) + .Where(t => t.X2 == 7) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(7m); + } + + [TestMethod] + public void Solve_FloatSymbolComparedToAnIntSymbol_RelatesTheTwo() + { + // Arrange: the third real type, and the third that had no arm. + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == t.X2) + .Where(t => t.X2 == 3) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(3f); + } + + /// + /// A long symbol can be compared to an int one. + /// + /// + /// Pinned in UnsupportedExpressionTests as unsupported until #76, with the note that + /// widening an int to long is unremarkable C#. Both types map to the integer + /// sort, so the conversion is a no-op in Z3 and the operand passes through unchanged. + /// + [TestMethod] + public void Solve_LongSymbolComparedToAnIntSymbol_RelatesTheTwo() + { + // Arrange + using var context = new Z3Context(); + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == t.X2) + .Where(t => t.X2 == 5) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(5L); + } + + [TestMethod] + public void Solve_DoubleSymbolComparedToAWidenedDecimalVariable_RoundTripsTheValue() + { + // Arrange: an explicit cast the caller wrote, between two real types. The operand is + // already real-sorted, so nothing is converted. + using var context = new Z3Context(); + decimal value = 1.25m; + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == (double)value) + .Where(t => t.X2 == 1) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(1.25); + } + + /// + /// A narrowing cast between real types is a no-op too. + /// + /// + /// (float) of a double narrows in C# and does nothing in Z3, where both are + /// the same unbounded real. Worth pinning because a reader might expect a rounding step; + /// there is none, and the value the constraint names is what comes back. + /// + [TestMethod] + public void Solve_FloatSymbolComparedToANarrowedDoubleVariable_RoundTripsTheValue() + { + // Arrange + using var context = new Z3Context(); + double value = 2.5; + + // Act + var result = context.NewTheorem>() + .Where(t => t.X1 == (float)value) + .Where(t => t.X2 == 1) + .Solve(); + + // Assert + result.ShouldNotBeNull(); + result.X1.ShouldBe(2.5f); + } +} diff --git a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs index 8051e7f..2f07cd8 100644 --- a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs +++ b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs @@ -59,16 +59,24 @@ public void Solve_CallToAnUnrecognisedMethod_ThrowsNotSupportedException() Should.Throw(() => theorem.Solve()); } + /// + /// A cast to a type the sort mapping does not know falls through to the catch-all. + /// + /// + /// This pinned (long)t.X1 until #76, when the Convert case chose by target type and + /// had no arm for long. Conversions are now decided by the sorts involved, using the + /// same mapping the symbols are declared with, so what is unsupported is a target type that + /// mapping has no row for - byte here. Note this one is NotImplementedException + /// rather than NotSupportedException - the throw sites are not consistent about which they + /// use. + /// [TestMethod] - public void Solve_UnsupportedCast_ThrowsNotImplementedException() + public void Solve_CastToAnUnmappedType_ThrowsNotImplementedException() { - // Arrange: the Convert case handles conversions to double, int and char only. Widening - // an int symbol to long is unremarkable C# but has no case, so it falls through to the - // catch-all (ExpressionVisitor.cs:141). Note this one is NotImplementedException rather - // than NotSupportedException - the throw sites are not consistent about which they use. + // Arrange using var context = new Z3Context(); var theorem = context.NewTheorem>() - .Where(t => (long)t.X1 == 1L); + .Where(t => (byte)t.X1 == 1); // Act & Assert Should.Throw(() => theorem.Solve()); diff --git a/solutions/Z3.Linq/ExpressionVisitor.cs b/solutions/Z3.Linq/ExpressionVisitor.cs index 2d60cbc..b8a899d 100644 --- a/solutions/Z3.Linq/ExpressionVisitor.cs +++ b/solutions/Z3.Linq/ExpressionVisitor.cs @@ -117,23 +117,37 @@ private static Expr VisitConvert(Context context, Environment environment, Unary var inner = Visit(context, environment, expression.Operand, param); - switch (Type.GetTypeCode(expression.Type)) + // A numeric conversion the compiler inserted, or the caller wrote, means one of three + // things in Z3, and which one depends on the sorts involved rather than on the CLR + // types: nothing at all when both types map to the same sort (short to int, int to + // long, float to double, a cast that only narrows); integer-to-real when the operand is + // an integer and the target a real (int to double, int to decimal); real-to-integer the + // other way round. The target sort comes from the same mapping the symbols are declared + // with, so a conversion can never disagree with a symbol about what a type is. + // + // This used to be a switch on the target type alone, which assumed the operand sort from + // it - int-to-real for every conversion to double, real-to-int for every conversion to + // int - and had no arm at all for long, float or decimal. See #63 and #76. + Sort? targetSort = expression.Type == typeof(char) + ? context.IntSort + : Theorem.TryGetSymbolSort(context, Type.GetTypeCode(expression.Type)); + + if (targetSort is not null) { - 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. + if (inner.Sort.Equals(targetSort)) + { return inner; - case TypeCode.Int32: + } + + if (inner.IsInt && targetSort is RealSort) + { + return context.MkInt2Real((IntExpr)inner); + } + + if (inner.IsReal && targetSort is IntSort) + { return context.MkReal2Int((RealExpr)inner); - case TypeCode.Char: - if (inner.IsInt) - { - return inner;// context.MkInt(1);// ((IntExpr)inner).int); - } - break; + } } throw new NotImplementedException($"Cast '{expression.Operand} ({expression.Operand.Type})' to {expression.Type}"); diff --git a/solutions/Z3.Linq/Theorem.cs b/solutions/Z3.Linq/Theorem.cs index 5f1752c..3c784a7 100644 --- a/solutions/Z3.Linq/Theorem.cs +++ b/solutions/Z3.Linq/Theorem.cs @@ -229,13 +229,20 @@ private void AssertConstraints(Context context, Z3Object approach, Environmen /// if the type is not one the library maps. /// /// + /// /// This is the only mapping from CLR type to sort. A scalar symbol is a constant of this sort, /// and a collection symbol is a Z3 array from Int to it, so the two cannot disagree - /// there is nothing else to consult. Collections used to carry a mapping of their own, and /// only its int row agreed with this one; every other element type declared a domain or /// range that contradicted how its elements were constrained and read back. See #64. + /// + /// + /// asks the same question when a constraint converts between + /// CLR types: whether the conversion is a no-op, an integer-to-real, or a real-to-integer + /// depends only on the sorts the two types map to here. See #76. + /// /// - private static Sort? TryGetSymbolSort(Context context, TypeCode typeCode) + internal static Sort? TryGetSymbolSort(Context context, TypeCode typeCode) { return typeCode switch {