From 1a7f5ec60a2c1261be9b403bfb0c885ee7a5cdc2 Mon Sep 17 00:00:00 2001 From: Howard van Rooijen Date: Tue, 1 Sep 2026 21:17:03 +0100 Subject: [PATCH] Choose numeric conversions by sort, not by target type A double symbol could not be compared against a float variable. C# widens the float, and the visitor read the Convert node's target type as telling it what the operand was: every conversion to double was integer-to-real, so a real operand was cast to IntExpr and failed. The same assumption meant two symbols of different real types could not be related at all, and long, float and decimal had no arm whatever - a long symbol could not be compared to an int one. A numeric conversion is one of three things in Z3, decided by the sorts: nothing when both types map to the same sort, integer-to-real, or real-to-integer. The visitor now asks TryGetSymbolSort - the one mapping the symbols are declared with, internal from here - for the target sort and decides from that and the operand. The arm #63 added for short and enums was this rule for one row and is subsumed; its tests still fail when the rule is wrong. The pin that recorded (long)t.X1 as unsupported is repointed at (byte), which the mapping genuinely has no row for, so the catch-all stays covered. Co-Authored-By: Claude Fable 5.1 --- .../Z3.Linq.Tests/NumericConversionTests.cs | 245 ++++++++++++++++++ .../UnsupportedExpressionTests.cs | 20 +- solutions/Z3.Linq/ExpressionVisitor.cs | 42 ++- solutions/Z3.Linq/Theorem.cs | 9 +- 4 files changed, 295 insertions(+), 21 deletions(-) create mode 100644 solutions/Z3.Linq.Tests/NumericConversionTests.cs 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 {