diff --git a/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs b/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs
new file mode 100644
index 0000000..560fe85
--- /dev/null
+++ b/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs
@@ -0,0 +1,272 @@
+namespace Z3.Linq.Tests;
+
+using System.Globalization;
+using System.Runtime.ExceptionServices;
+using System.Threading;
+
+///
+/// Pins that translating a C# constant into a Z3 term does not depend on the ambient culture.
+///
+///
+///
+/// Z3's parser accepts only . as a decimal separator and only ASCII - as a sign,
+/// so a number handed to it has to be rendered invariantly. Until #52 was fixed,
+/// ExpressionVisitor rendered real constants with the current culture. Measured over the
+/// 606 specific cultures installed on the development machine, 301 of them produced a literal
+/// Z3 rejected with Z3Exception: parser error - about half, and every widely used
+/// European language among them. None produced a wrong value, which is the one merciful thing
+/// about it: the defect always announced itself.
+///
+///
+/// Every test here runs its solve on a dedicated thread. CurrentCulture is per-thread,
+/// these tests run in parallel at method level, and the runner hands out pooled threads - so
+/// setting it on the test's own thread could leak into whatever runs next on that thread. A
+/// thread created for the purpose cannot leak anywhere.
+///
+///
+/// Each culture test starts by asserting that the culture really does render its probe value
+/// differently from the invariant culture. Under globalization-invariant mode every culture
+/// falls back to invariant data, and without that check these tests would pass while
+/// exercising nothing.
+///
+///
+/// The solve, the model and the read back all happen on the foreign-culture thread, so these
+/// cover the whole round trip rather than the write side alone.
+///
+///
+[TestClass]
+public class CultureInvarianceTests
+{
+ ///
+ /// How long to wait for a solve running on a dedicated thread. Generous by design - it
+ /// exists to turn a hang into a failure, not to police how long a solve should take.
+ ///
+ private static readonly TimeSpan SolveTimeout = TimeSpan.FromSeconds(30);
+
+ [TestMethod]
+ [DataRow("de-DE", DisplayName = "German - comma separator")]
+ [DataRow("fr-FR", DisplayName = "French - comma separator")]
+ [DataRow("ru-RU", DisplayName = "Russian - comma separator")]
+ [DataRow("tr-TR", DisplayName = "Turkish - comma separator")]
+ [DataRow("fa-IR", DisplayName = "Persian - U+066B decimal separator")]
+ public void Solve_DoubleConstantUnderANonInvariantCulture_RoundTripsTheValue(string culture)
+ {
+ // Arrange: the case in #52's title. fa-IR is here because its separator is not a comma
+ // either - the defect was never specific to one character.
+ CultureInfo cultureInfo = RequireANonInvariantRendering(culture, 1.5);
+
+ // Act
+ double? value = SolveOn(cultureInfo, () =>
+ {
+ using var context = new Z3Context();
+ return context.NewTheorem>()
+ .Where(t => t.X1 == 1.5)
+ .Solve()?.X1;
+ });
+
+ // Assert
+ value.ShouldBe(1.5);
+ }
+
+ ///
+ /// A negative real constant survives a culture whose negative sign is not ASCII.
+ ///
+ ///
+ /// These cultures render -1.5 with U+2212 MINUS SIGN rather than ASCII -. A fix that
+ /// only swapped the decimal separator would still hand Z3 a sign it cannot parse, so this is
+ /// the case that rules out the obvious wrong fix.
+ ///
+ [TestMethod]
+ [DataRow("sv-SE", DisplayName = "Swedish")]
+ [DataRow("fi-FI", DisplayName = "Finnish")]
+ public void Solve_NegativeDoubleConstantUnderACultureWithANonAsciiSign_RoundTripsTheValue(
+ string culture)
+ {
+ // Arrange
+ CultureInfo cultureInfo = RequireANonInvariantRendering(culture, -1.5);
+ cultureInfo.NumberFormat.NegativeSign.ShouldNotBe("-");
+
+ // Act
+ double? value = SolveOn(cultureInfo, () =>
+ {
+ using var context = new Z3Context();
+ return context.NewTheorem>()
+ .Where(t => t.X1 == -1.5)
+ .Solve()?.X1;
+ });
+
+ // Assert
+ value.ShouldBe(-1.5);
+ }
+
+ [TestMethod]
+ [DataRow("de-DE", DisplayName = "German")]
+ [DataRow("sv-SE", DisplayName = "Swedish")]
+ public void Solve_DecimalConstantUnderANonInvariantCulture_RoundTripsTheValue(string culture)
+ {
+ // Arrange: decimal shares the real sort with double and the same arm of the constant
+ // switch, but it is a separate CLR formatter, so it gets its own case.
+ CultureInfo cultureInfo = RequireANonInvariantRendering(culture, 1.5m);
+
+ // Act
+ decimal? value = SolveOn(cultureInfo, () =>
+ {
+ using var context = new Z3Context();
+ return context.NewTheorem>()
+ .Where(t => t.X1 == 1.5m)
+ .Solve()?.X1;
+ });
+
+ // Assert
+ value.ShouldBe(1.5m);
+ }
+
+ ///
+ /// A float constant gets past translation under a foreign culture and fails at the
+ /// read back instead - which is #54, not #52.
+ ///
+ ///
+ /// float takes the same arm of the constant switch as double and
+ /// decimal, so without this the fix would have a third of its call site untested. It
+ /// cannot be a round-trip test, because a float symbol cannot round-trip at all: the model
+ /// value is parsed into a double and reflection then refuses to write it to a float
+ /// property. Under the defect this threw Z3Exception during translation, so reaching
+ /// is itself the evidence that translation now succeeds.
+ ///
+ [TestMethod]
+ public void Solve_FloatConstantUnderANonInvariantCulture_FailsInMarshallingNotTranslation()
+ {
+ // Arrange
+ const string Culture = "de-DE";
+ CultureInfo cultureInfo = RequireANonInvariantRendering(Culture, 1.5f);
+
+ // Act & Assert
+ Should.Throw(() => SolveOn(cultureInfo, () =>
+ {
+ using var context = new Z3Context();
+ return context.NewTheorem>()
+ .Where(t => t.X1 == 1.5f)
+ .Solve()?.X1;
+ }));
+ }
+
+ ///
+ /// A string constant is unaffected by the culture.
+ ///
+ ///
+ /// The line that fixes #52 sits two above a MkString(val.ToString()) that looks
+ /// identical. That one is safe - String.ToString() returns the instance - and this
+ /// test is here so the asymmetry is a recorded fact rather than an oversight waiting to be
+ /// tidied up. tr-TR because its casing rules are the usual way a string path turns out to
+ /// be culture-sensitive after all.
+ ///
+ [TestMethod]
+ public void Solve_StringConstantUnderANonInvariantCulture_RoundTripsTheValue()
+ {
+ // Arrange
+ const string Culture = "tr-TR";
+ CultureInfo cultureInfo = CultureInfo.GetCultureInfo(Culture);
+ cultureInfo.TextInfo.ToLower("I").ShouldNotBe("i");
+
+ // Act
+ string? value = SolveOn(cultureInfo, () =>
+ {
+ using var context = new Z3Context();
+ return context.NewTheorem>()
+ .Where(t => t.X1 == "III")
+ .Solve()?.X1;
+ });
+
+ // Assert
+ value.ShouldBe("III");
+ }
+
+ [TestMethod]
+ public void Solve_DoubleConstantUnderTheInvariantCulture_RoundTripsTheValue()
+ {
+ // Arrange: the control. It uses the same dedicated-thread mechanism as the tests above,
+ // so they differ from it by culture and nothing else. This one passed on both sides of
+ // the fix; if it ever fails, the problem is the harness rather than the culture.
+
+ // Act
+ double? value = SolveOn(CultureInfo.InvariantCulture, () =>
+ {
+ using var context = new Z3Context();
+ return context.NewTheorem>()
+ .Where(t => t.X1 == 1.5)
+ .Solve()?.X1;
+ });
+
+ // Assert
+ value.ShouldBe(1.5);
+ }
+
+ ///
+ /// Asserts that renders differently from
+ /// the invariant culture, so a test using it can detect the defect it exists for.
+ ///
+ /// The resolved culture, so the caller resolves it once.
+ private static CultureInfo RequireANonInvariantRendering(string culture, IFormattable probe)
+ {
+ CultureInfo cultureInfo = CultureInfo.GetCultureInfo(culture);
+
+ cultureInfo.NumberFormat.NumberDecimalSeparator.ShouldNotBe(
+ CultureInfo.InvariantCulture.NumberFormat.NumberDecimalSeparator,
+ $"{culture} formats numbers exactly as the invariant culture does on this machine, "
+ + "so this test cannot detect the defect it exists for - most likely the runtime is "
+ + "in globalization-invariant mode, where every culture falls back to invariant "
+ + "data");
+
+ probe.ToString(null, cultureInfo)
+ .ShouldNotBe(probe.ToString(null, CultureInfo.InvariantCulture));
+
+ return cultureInfo;
+ }
+
+ ///
+ /// Runs on a thread pinned to , and returns
+ /// what it returned or rethrows what it threw.
+ ///
+ ///
+ /// The exception is captured and rethrown rather than left to escape: one escaping a bare
+ /// thread is unhandled, so it takes down the test host and the run reports "zero tests ran"
+ /// rather than one failure.
+ ///
+ private static T SolveOn(CultureInfo culture, Func body)
+ {
+ T result = default!;
+ ExceptionDispatchInfo? failure = null;
+
+ var thread = new Thread(() =>
+ {
+ CultureInfo.CurrentCulture = culture;
+
+ try
+ {
+ result = body();
+ }
+ catch (Exception ex)
+ {
+ failure = ExceptionDispatchInfo.Capture(ex);
+ }
+ })
+ {
+ // Foreground is the default, and a foreground thread that outlives the wait below
+ // holds the whole test host open - measured: a process whose Main has returned does
+ // not exit at all while one is still running. That turns the timeout from a clean
+ // failure into a stalled run, which is the opposite of what it is here for.
+ IsBackground = true,
+ };
+
+ thread.Start();
+
+ // Bounded, so that a solver that never returns fails the test rather than hanging the
+ // whole run with no indication of which test stopped. The work itself takes single-digit
+ // milliseconds, so the limit is enormous slack rather than a tuned value.
+ string name = culture.Name.Length == 0 ? "invariant" : culture.Name;
+ thread.Join(SolveTimeout).ShouldBeTrue($"the solve on the {name} thread did not finish");
+
+ failure?.Throw();
+ return result;
+ }
+}
diff --git a/solutions/Z3.Linq.Tests/RewriterTests.cs b/solutions/Z3.Linq.Tests/RewriterTests.cs
index f5bbf02..da28e82 100644
--- a/solutions/Z3.Linq.Tests/RewriterTests.cs
+++ b/solutions/Z3.Linq.Tests/RewriterTests.cs
@@ -117,7 +117,7 @@ public void Solve_PredicateRewriterThatReturnsItsInput_ThrowsTheProgressGuard()
{
// Arrange: the visitor re-visits whatever the rewriter returns, so a rewriter returning
// its own input would recurse forever. That is detected by reference equality and
- // rejected (ExpressionVisitor.cs:191) - a guard worth keeping, since the alternative is
+ // rejected (ExpressionVisitor.cs:192) - a guard worth keeping, since the alternative is
// a hung build rather than a failed one.
using var context = new Z3Context();
var theorem = context.NewTheorem>()
@@ -131,7 +131,7 @@ public void Solve_PredicateRewriterThatReturnsItsInput_ThrowsTheProgressGuard()
public void Solve_PredicateRewriterTypeNotImplementingTheInterface_ThrowsInvalidOperationException()
{
// Arrange: as with the global rewriter, the attribute cannot enforce this at compile
- // time (ExpressionVisitor.cs:179).
+ // time (ExpressionVisitor.cs:180).
using var context = new Z3Context();
var theorem = context.NewTheorem>()
.Where(t => WrongRewriterType(t.X1, t.X2));
diff --git a/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs b/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs
index 600a2cb..aa9418f 100644
--- a/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs
+++ b/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs
@@ -1,8 +1,5 @@
namespace Z3.Linq.Tests;
-using System.Globalization;
-using System.Threading;
-
///
/// Round-trips a value of each scalar symbol type through :
/// C# constant -> Z3 term -> model -> CLR property.
@@ -23,12 +20,6 @@ namespace Z3.Linq.Tests;
[TestClass]
public class SymbolTypeMarshallingTests
{
- ///
- /// How long to wait for a solve running on a dedicated thread. Generous by design - it
- /// exists to turn a hang into a failure, not to police how long a solve should take.
- ///
- private static readonly TimeSpan SolveTimeout = TimeSpan.FromSeconds(30);
-
[TestMethod]
[DataRow(0, DisplayName = "Zero")]
[DataRow(42, DisplayName = "Positive")]
@@ -173,7 +164,7 @@ public void Solve_DoubleSymbolWithInequality_SatisfiesTheConstraint()
///
/// 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:131). A second defect waits behind
+ /// 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.
///
@@ -265,101 +256,6 @@ public void Solve_MixedTypeSymbols_MarshalsEveryPropertyIndependently()
result.X2.ShouldBe("five");
}
- ///
- /// KNOWN DEFECT (#52): a real-valued constant is written to Z3 using the current culture.
- ///
- ///
- ///
- /// ExpressionVisitor.cs:304 calls MkReal(val.ToString()) with no format provider, so under a
- /// comma-decimal culture the literal 1.5 is handed to Z3 as "1,5" and its parser rejects it.
- /// Every other numeric conversion in the visitor passes InvariantCulture, and so does every
- /// read back on the marshalling side, which is what makes this one look like an oversight
- /// rather than a decision.
- ///
- ///
- /// The work runs on a dedicated thread rather than by setting the culture on the test's own
- /// thread. CurrentCulture is per-thread, these tests run in parallel at method level, and
- /// the runner hands out pooled threads - so mutating it here could leak into whatever runs
- /// next on the same thread. A thread created for the purpose cannot leak anywhere.
- ///
- /// This test pins current behaviour and must be updated when the defect is fixed.
- ///
- [TestMethod]
- public void Solve_DoubleSymbolUnderCommaDecimalCulture_ThrowsZ3ParserError()
- {
- // Arrange
- Exception? captured = null;
-
- var thread = new Thread(() =>
- {
- CultureInfo.CurrentCulture = CultureInfo.GetCultureInfo("de-DE");
-
- try
- {
- using var context = new Z3Context();
- _ = context.NewTheorem>()
- .Where(t => t.X1 == 1.5)
- .Solve();
- }
- catch (Exception ex)
- {
- captured = ex;
- }
- });
-
- // Act
- thread.Start();
-
- // Bounded, so that a solver that never returns fails this test rather than hanging the
- // whole run with no indication of which test stopped. The work itself takes single-digit
- // milliseconds, so the limit is enormous slack rather than a tuned value.
- thread.Join(SolveTimeout).ShouldBeTrue("the solve on the de-DE thread did not finish");
-
- // Assert
- captured.ShouldBeOfType();
- }
-
- [TestMethod]
- public void Solve_DoubleSymbolUnderInvariantCulture_RoundTripsTheValue()
- {
- // Arrange: the counterpart to the pin above, on the same dedicated-thread mechanism, so
- // that the two differ only by culture. This is what the defect above should look like
- // once it is fixed.
- double? value = null;
- Exception? captured = null;
-
- var thread = new Thread(() =>
- {
- CultureInfo.CurrentCulture = CultureInfo.InvariantCulture;
-
- try
- {
- using var context = new Z3Context();
- var result = context.NewTheorem>()
- .Where(t => t.X1 == 1.5)
- .Solve();
-
- value = result?.X1;
- }
- catch (Exception ex)
- {
- // Captured rather than left to escape: an exception on a bare thread is
- // unhandled, so it takes down the test host and the run reports "zero tests
- // ran" rather than one failed test. The pin above already does this; this
- // counterpart did not, because it was not expected to throw.
- captured = ex;
- }
- });
-
- // Act
- thread.Start();
- thread.Join(SolveTimeout).ShouldBeTrue("the solve on the invariant-culture thread did not finish");
-
- // Assert
- captured.ShouldBeNull();
- value.ShouldBe(1.5);
- }
-
///
/// An unconstrained long symbol is populated rather than throwing.
///
diff --git a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs
index 1fb7f49..2a980ed 100644
--- a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs
+++ b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs
@@ -50,7 +50,7 @@ public void Solve_CallToAnUnrecognisedMethod_ThrowsNotSupportedException()
// Arrange: only Z3Methods.Distinct, indexed property getters and methods carrying a
// predicate rewriter attribute are understood. An ordinary method that depends on a
// theorem symbol cannot be evaluated away, so it reaches the visitor and is rejected
- // (ExpressionVisitor.cs:277).
+ // (ExpressionVisitor.cs:278).
using var context = new Z3Context();
var theorem = context.NewTheorem>()
.Where(t => Increment(t.X1) == 2);
@@ -64,7 +64,7 @@ public void Solve_UnsupportedCast_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:140). Note this one is NotImplementedException rather
+ // catch-all (ExpressionVisitor.cs:141). Note this one is NotImplementedException rather
// than NotSupportedException - the throw sites are not consistent about which they use.
using var context = new Z3Context();
var theorem = context.NewTheorem>()
@@ -119,7 +119,7 @@ public void Solve_NullableProperty_ThrowsArgumentException()
///
/// 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:131 reads as a real-to-int conversion and casts to RealExpr. Same
+ /// 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.
///
diff --git a/solutions/Z3.Linq/ExpressionVisitor.cs b/solutions/Z3.Linq/ExpressionVisitor.cs
index 46509b2..bc9d6d5 100644
--- a/solutions/Z3.Linq/ExpressionVisitor.cs
+++ b/solutions/Z3.Linq/ExpressionVisitor.cs
@@ -1,6 +1,7 @@
namespace Z3.Linq;
using System.Collections;
+using System.Globalization;
using System.Linq.Expressions;
using System.Reflection;
@@ -301,7 +302,9 @@ private static Expr VisitConstantValue(Context context, object val)
case TypeCode.Single:
case TypeCode.Double:
case TypeCode.Decimal:
- return context.MkReal(val.ToString());
+ // Invariant, not current: Z3's parser accepts only '.' as the decimal separator,
+ // and about half of all cultures render 1.5 as something else. See #52.
+ return context.MkReal(((IFormattable)val).ToString(null, CultureInfo.InvariantCulture));
case TypeCode.DateTime:
return context.MkInt(((DateTime)val).ToFileTimeUtc());
case TypeCode.String: