Choose numeric conversions by sort, not by target type

solutions/Z3.Linq.Tests/NumericConversionTests.cs

@@ -0,0 +1,245 @@
+namespace Z3.Linq.Tests;
+
+/// <summary>
+/// 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.
+/// </summary>
+/// <remarks>
+/// <para>
+/// Every mixed-type comparison or arithmetic expression carries a <c>Convert</c> node the caller
+/// never wrote - <c>t.X1 == f</c> against a <c>double</c> symbol and a <c>float</c> variable is
+/// <c>t.X1 == (double)f</c> 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.
+/// </para>
+/// <para>
+/// Until #76 the visitor chose from the target type alone - int-to-real for every conversion to
+/// <c>double</c>, real-to-int for every conversion to <c>int</c> - and had no case at all for
+/// <c>long</c>, <c>float</c> or <c>decimal</c>. So a <c>float</c> variable could not be compared
+/// against a <c>double</c> symbol, two symbols of different real types could not be related, and
+/// a <c>long</c> symbol could not be compared to an <c>int</c> one. #63 fixed the <c>int</c>
+/// arm the same way earlier in this stack; this finishes the job across the switch.
+/// </para>
+/// <para>
+/// The real-to-integer direction is covered by
+/// <c>SymbolTypeMarshallingTests.Solve_DoubleSymbolCastToInt_ConvertsRatherThanPassingThrough</c>,
+/// which needs a constraint the truncation can be observed through and lives beside the
+/// marshalling tests it shares that trick with.
+/// </para>
+/// </remarks>
+[TestClass]
+public class NumericConversionTests
+{
+    /// <summary>
+    /// The case in #76: a <c>double</c> symbol compared against a <c>float</c> variable.
+    /// </summary>
+    /// <remarks>
+    /// A <c>float</c> literal in the same position is folded to a <c>double</c> 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 <c>double</c> arm cast it to
+    /// <c>IntExpr</c> on the assumption that anything converted to a double must have been an
+    /// integer.
+    /// </remarks>
+    [TestMethod]
+    public void Solve_DoubleSymbolComparedToAFloatVariable_RoundTripsTheValue()
+    {
+        // Arrange
+        using var context = new Z3Context();
+        float value = 1.5f;
+
+        // Act
+        var result = context.NewTheorem<Symbols<double, int>>()
+            .Where(t => t.X1 == value)
+            .Where(t => t.X2 == 1)
+            .Solve();
+
+        // Assert
+        result.ShouldNotBeNull();
+        result.X1.ShouldBe(1.5);
+    }
+
+    /// <summary>
+    /// Two symbols of different real types can be related to each other.
+    /// </summary>
+    /// <remarks>
+    /// Stronger than the issue's repro, and the one that matters in practice: nothing about
+    /// <c>Symbols&lt;double, float&gt;</c> suggests its two members cannot appear in the same
+    /// constraint, yet every comparison between them widened the <c>float</c> and failed.
+    /// </remarks>
+    [TestMethod]
+    public void Solve_DoubleSymbolComparedToAFloatSymbol_RelatesTheTwo()
+    {
+        // Arrange
+        using var context = new Z3Context();
+
+        // Act
+        var result = context.NewTheorem<Symbols<double, float>>()
+            .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<Symbols<double, float>>()
+            .Where(t => t.X1 == t.X2 * 2)
+            .Where(t => t.X2 == 1.5f)
+            .Solve();
+
+        // Assert
+        result.ShouldNotBeNull();
+        result.X1.ShouldBe(3.0);
+    }
+
+    /// <summary>
+    /// The widening the old <c>double</c> arm was written for still works.
+    /// </summary>
+    /// <remarks>
+    /// An <c>int</c> operand converted to <c>double</c> 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.
+    /// </remarks>
+    [TestMethod]
+    public void Solve_DoubleSymbolComparedToAnIntSymbol_RelatesTheTwo()
+    {
+        // Arrange
+        using var context = new Z3Context();
+
+        // Act
+        var result = context.NewTheorem<Symbols<double, int>>()
+            .Where(t => t.X1 == t.X2)
+            .Where(t => t.X2 == 7)
+            .Solve();
+
+        // Assert
+        result.ShouldNotBeNull();
+        result.X1.ShouldBe(7.0);
+        result.X2.ShouldBe(7);
+    }
+
+    /// <summary>
+    /// A <c>decimal</c> symbol can be compared to an <c>int</c> one.
+    /// </summary>
+    /// <remarks>
+    /// There was no arm for a conversion to <c>decimal</c> at all, so this fell through to the
+    /// catch-all as <see cref="NotImplementedException"/>. It is the same integer-to-real
+    /// conversion as the <c>double</c> case, because <c>decimal</c> and <c>double</c> map to the
+    /// same sort - which is exactly what choosing by sort rather than by type buys.
+    /// </remarks>
+    [TestMethod]
+    public void Solve_DecimalSymbolComparedToAnIntSymbol_RelatesTheTwo()
+    {
+        // Arrange
+        using var context = new Z3Context();
+
+        // Act
+        var result = context.NewTheorem<Symbols<decimal, int>>()
+            .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<Symbols<float, int>>()
+            .Where(t => t.X1 == t.X2)
+            .Where(t => t.X2 == 3)
+            .Solve();
+
+        // Assert
+        result.ShouldNotBeNull();
+        result.X1.ShouldBe(3f);
+    }
+
+    /// <summary>
+    /// A <c>long</c> symbol can be compared to an <c>int</c> one.
+    /// </summary>
+    /// <remarks>
+    /// Pinned in <c>UnsupportedExpressionTests</c> as unsupported until #76, with the note that
+    /// widening an <c>int</c> to <c>long</c> 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.
+    /// </remarks>
+    [TestMethod]
+    public void Solve_LongSymbolComparedToAnIntSymbol_RelatesTheTwo()
+    {
+        // Arrange
+        using var context = new Z3Context();
+
+        // Act
+        var result = context.NewTheorem<Symbols<long, int>>()
+            .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<Symbols<double, int>>()
+            .Where(t => t.X1 == (double)value)
+            .Where(t => t.X2 == 1)
+            .Solve();
+
+        // Assert
+        result.ShouldNotBeNull();
+        result.X1.ShouldBe(1.25);
+    }
+
+    /// <summary>
+    /// A narrowing cast between real types is a no-op too.
+    /// </summary>
+    /// <remarks>
+    /// <c>(float)</c> of a <c>double</c> 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.
+    /// </remarks>
+    [TestMethod]
+    public void Solve_FloatSymbolComparedToANarrowedDoubleVariable_RoundTripsTheValue()
+    {
+        // Arrange
+        using var context = new Z3Context();
+        double value = 2.5;
+
+        // Act
+        var result = context.NewTheorem<Symbols<float, int>>()
+            .Where(t => t.X1 == (float)value)
+            .Where(t => t.X2 == 1)
+            .Solve();
+
+        // Assert
+        result.ShouldNotBeNull();
+        result.X1.ShouldBe(2.5f);
+    }
+}

solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs

@@ -59,16 +59,24 @@ public void Solve_CallToAnUnrecognisedMethod_ThrowsNotSupportedException()
         Should.Throw<NotSupportedException>(() => theorem.Solve());
     }
 
+    /// <summary>
+    /// A cast to a type the sort mapping does not know falls through to the catch-all.
+    /// </summary>
+    /// <remarks>
+    /// This pinned <c>(long)t.X1</c> until #76, when the Convert case chose by target type and
+    /// had no arm for <c>long</c>. 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 - <c>byte</c> here. Note this one is NotImplementedException
+    /// rather than NotSupportedException - the throw sites are not consistent about which they
+    /// use.
+    /// </remarks>
     [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<Symbols<int, int>>()
-            .Where(t => (long)t.X1 == 1L);
+            .Where(t => (byte)t.X1 == 1);
 
         // Act & Assert
         Should.Throw<NotImplementedException>(() => theorem.Solve());

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

solutions/Z3.Linq/Theorem.cs

@@ -229,13 +229,20 @@ private void AssertConstraints<T>(Context context, Z3Object approach, Environmen
     /// if the type is not one the library maps.
     /// </summary>
     /// <remarks>
+    /// <para>
     /// 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 <c>Int</c> 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 <c>int</c> 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.
+    /// </para>
+    /// <para>
+    /// <see cref="ExpressionVisitor"/> 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.
+    /// </para>
     /// </remarks>
-    private static Sort? TryGetSymbolSort(Context context, TypeCode typeCode)
+    internal static Sort? TryGetSymbolSort(Context context, TypeCode typeCode)
     {
         return typeCode switch
         {