Repository navigation
Port the fork onto the endjin pile tip (net10, MTP, Z3 5.1.0) - #44
Merged
Merged
Conversation
Replaces the Endjin.RecommendedPractices.Build bootstrap in build.ps1 with the ZeroFailed equivalent, moving all build configuration out into .zf/config.ps1 as per the ZeroFailed convention. - build.ps1 is now a thin bootstrap (ZeroFailed 1.0.6, InvokeBuild 5.14.22) that dots into .zf/config.ps1. The existing parameter surface is unchanged. - .zf/config.ps1 declares the ZeroFailed.Build.DotNet extension and carries the build configuration previously inline in build.ps1. SkipTest remains true as the solution still has no test project. - The old $ExcludeFilesFromCodeCoverage placeholder becomes ZeroFailed's Include/ExcludeAssembliesInCodeCoverage properties. - .gitignore excludes the .zf/extensions/ download cache. - The CI publish source env var is renamed BUILDVAR_NuGetPublishSource -> ZF_NUGET_PUBLISH_SOURCE. BUILDVAR_ is an Endjin.RecommendedPractices.Build convention that ZeroFailed does not read, so without this the publish stage would silently fall back to the local feed default. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Both were a single patch release behind the latest stable on the PowerShell Gallery. Verified locally: the build bootstraps on ZeroFailed 1.0.7 and completes with 35 tasks, 0 errors, 0 warnings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The scaffolded wording ('use latest version from main will be downloaded')
reads as two half-sentences spliced together. Same meaning, in one sentence.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
- Converts the solution to the .slnx format via 'dotnet sln migrate', and adds a Solution Items folder for the shared props files. - Adds solutions/Directory.Packages.props enabling Central Package Management; version attributes are removed from the PackageReference items. - Adds solutions/Directory.Build.props hoisting everything the three projects duplicated: TargetFramework (now net10.0), ImplicitUsings, Nullable, PlatformTarget (x64, required by Microsoft.Z3's native binaries), TreatWarningsAsErrors, and the shared package metadata. Also enables SourceLink and deterministic CI builds. - Points $SolutionToBuild at the .slnx and bumps CI netSdkVersion to 10.x. MiaPlaza.ExpressionUtils is deliberately held at 1.2.0: 1.3.x removes the general PartialEval(Expression, IExpressionEvaluator) overload in favour of a LambdaExpression-constrained generic, which ExpressionVisitor.cs relies on. Microsoft.Z3 4.12.2 is already the newest published to nuget.org. Verified: builds clean on net10.0 with TreatWarningsAsErrors (0 warnings), the demo app solves all examples correctly, and the full ZeroFailed build packages both libraries as lib/net10.0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
auto_release.yml installed the .NET 6 SDK solely to give 'dotnet tool install' something to run under; the GitVersion step never compiles the solution. .NET 6 is long out of support, and build.yml is now on 10.x, so the two workflows were pinned to different SDKs for no reason. GitVersion.Tool 5.8.0 is unaffected by the change: it ships "rollForward": "LatestMajor" in its runtimeconfig.json, so it binds to whatever the newest installed runtime is rather than requiring .NET 5/6. Verified on a machine with no .NET 5 or 6 runtime installed (only 8.0.30, 9.0.19, 10.0.8, 10.0.11): a fresh 'dotnet tool install GitVersion.Tool --version 5.8.0' under SDK 10.0.400 succeeds, COREHOST_TRACE confirms it selects Microsoft.NETCore.App 10.0.11, and it returns MajorMinorPatch 2.0.2 - the variable this workflow consumes for the release tag. The GitVersion version itself is deliberately unchanged. Moving to GitVersion 6 is breaking here: it rejects next-version "2.0" and needs "2.0.0", and GitVersion.yml is generated by the pr-autoflow codeops mechanism, so that fix belongs in endjin-codeops rather than this repo. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Z3.Linq uses Description but Z3.Linq.Examples uses PackageDescription, so naming only the former misdirects the next person adding a packable project. Verified that PackageDescription does populate the nuspec <description>. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The headline still described the library as .NET 8.0 bindings, and the Polyglot Notebook referenced bin/Debug/net8.0 paths that the build no longer produces - so anyone following the README's 'run it locally' route hit missing assemblies. The History entries naming .NET 4.5, 6.0 and 8.0 are left alone; they record what those contributors did at the time. A 2026 entry is added for this work. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ange 1.3.x removes PartialEvaluator.PartialEval's Expression-taking overloads, leaving only PartialEval<TExpression>(TExpression, IExpressionEvaluator) constrained to LambdaExpression. ExpressionVisitor fed it the output of ParameterSubstituter.SubstituteParameter, which is the selector's body and so not a lambda, giving CS0311 on upgrade. The body is now wrapped in a lambda for the call and unwrapped afterwards, which is the supported equivalent of the removed overload. The theorem's own parameter stays free in the wrapper; the evaluator folds only closed subtrees and leaves parameter-dependent ones alone, so the result is unchanged. This affects Z3Methods.Distinct(collection.Select(...).ToArray()). Nothing in the repository exercises that branch - the Sudoku theorems build their Distinct arguments as a NewArrayExpression, which takes the other path - so it was verified with a purpose-built probe covering satisfiable, unsatisfiable, constant-folded and two-symbol selectors. All four produce byte-identical results before and after the upgrade: multipliers-sat: X1=11, X2=12 duplicate-unsat: <unsat> folded-sat: X1=7, X2=0 two-symbols-sat: X1=4, X2=9 The demo app's output is also unchanged, and the full ZeroFailed build passes (35 tasks, 0 errors, 0 warnings under TreatWarningsAsErrors). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Microsoft.Z3 4.12.2 contains native binaries for win-x64 and osx-x64 only. On Linux the managed assembly therefore loads and then fails at the first solve, either with DllNotFoundException or - where the machine happens to have an unrelated system libz3, as the GitHub Actions runner image does - with EntryPointNotFoundException against a solver we never pinned. That is why the build goes red as soon as a stage actually executes a theorem. 5.1.0 ships linux-x64, linux-arm64, osx-x64, osx-arm64, win-x64 and win-arm64. Verified by running the solution on Ubuntu 24.04 (glibc 2.39, matching ubuntu-latest) as well as Windows, and by diffing the full demo output between 4.12.2 and 5.1.0: the Sudoku, oil purchase and warehouse results are identical, and Missionaries & Cannibals still reaches the same optimum under both Optimize() and orderby. Only the unoptimised Solve() picks a different valid model, which is expected where the constraints admit many. The Z3 project stopped publishing to nuget.org after 4.12.2 and now ships the package as a GitHub release asset, so it is fetched into a local folder feed before restore. The download is pinned by SHA-256 and only moved into the feed once it matches, so an interrupted or substituted download cannot become a package that restore consumes. PlatformTarget is dropped now that arm64 binaries exist - pinning x64 would shut those machines out. NOTE: this is not yet safe to publish. The packed Z3.Linq declares a dependency on Microsoft.Z3 5.1.0, which does not exist on nuget.org, so a consumer restoring Z3.Linq from nuget.org fails with NU1102. The published package's dependency has to be settled before this is released. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The packed Z3.Linq declares a dependency on Microsoft.Z3 5.1.0, which is not published to nuget.org, so a consumer restoring from nuget.org with a clean cache fails with NU1102. NuGet gives a package no way to tell consumers where its dependencies live, so no feed we control can fix that - only an upstream publish can. $SkipPublish keeps a tagged build from shipping an unrestorable package in the meantime. Verified: FullBuildAndPublish reports "Publish skipped" and still completes the package stage. See endjin#60 for what lifts the hold, and Z3Prover/z3#10711 upstream. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The README told everyone to target x64, which stops being true with this change: 5.1.0 carries native binaries for x64 and arm64 on all three platforms, so AnyCPU resolves the right one. The note is there because the advice does not apply to anything on nuget.org yet. Published versions depend on Microsoft.Z3 4.12.2, which has no Linux or arm64 binaries, so on those platforms they restore and then throw DllNotFoundException on the first solve - a failure worth naming, since it looks like a bug in this library rather than a missing native. Releases are paused until upstream publishes (endjin#60). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Adds the repository's first test project, following the endjin .NET testing framework guidelines: MSTest 4.0 on Microsoft.Testing.Platform via the MSTest SDK, with Shouldly for assertions. - global.json selects the MTP runner and pins MSTest.Sdk 4.3.3, which is how .NET 10 enables MTP mode (the older TestingPlatformDotnetTestSupport property is obsolete). - AssemblyInfo.cs carries [assembly: Parallelize(Workers = 0, Scope = ExecutionScope.MethodLevel)], required by MSTest 4.0 to avoid MSTEST0001. - TestingExtensionsProfile=Default brings in the code coverage and TRX report extensions. - Shouldly is added to Directory.Packages.props. No PackageVersion is added for Microsoft.Testing.Extensions.CodeCoverage: the MSTest SDK injects its own under CPM and a second one trips NU1506. - NSubstitute is deliberately omitted; there is nothing to substitute in these tests, and the guidelines say to mock only what is used. - .zf/config.ps1 stops skipping the Test and TestReport stages, so the ZeroFailed build now runs tests and produces coverage. The coverage assembly filters added earlier (+Z3.Linq*;-Z3.Linq*.Tests*) apply as-is. - .gitignore excludes the TRX and Cobertura output the run leaves behind. The 16 tests cover Z3Methods.Distinct in both of its visitor branches: the Select(...).ToArray() form that reaches PartialEvaluator.PartialEval, and the inline NewArrayExpression form that does not, including cases asserting the two forms agree. Two of them exist specifically to pin the partial-evaluation step. The arithmetic-only cases turned out to pass with partial evaluation removed, because Z3 folds constant arithmetic itself, so they do not actually guard the change. The host-method cases do: the selector calls an ordinary C# method that the visitor cannot translate, so it only reaches Z3 as a constant if the substituted body is partially evaluated first. Verified by mutation - removing the PartialEval call fails exactly those two tests with "NotSupportedException: Unknown method call: Int32 Get(Int32)", and passes the other 14. Full ZeroFailed build: 45 tasks, 0 errors, 0 warnings, 16/16 tests passing, 31.5% line coverage on Z3.Linq. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The MSTest SDK adds this package implicitly and defaults it to 18.9.0, which left the coverage extension a release behind the dotnet-coverage collector that the ZeroFailed test task runs (18.10.0). The reference is injected from a .targets file imported after the project body, so a per-project PackageReference Update would be a no-op; setting MicrosoftTestingExtensionsCodeCoverageVersion in Directory.Build.props is the supported override. No PackageVersion is added in Directory.Packages.props - under CPM the SDK derives its own from this property, and a second one trips NU1506. With this, 'dotnet list package --outdated' reports no updates for any of the four projects. Full ZeroFailed build: 45 tasks, 0 errors, 16/16 tests passing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
First phase of broadening Z3.Linq's test coverage beyond the Distinct paths. 23 new tests take the suite from 16 to 39 and line coverage from 31.5% to 38.8%. - GlobalUsings.cs centralises the common imports. Note the Z3Environment alias: a global 'using Z3.Linq' makes the bare name Environment bind to Z3.Linq.Environment rather than System.Environment, which is a surprising shadowing failure the alias makes explicit. - TheoremSolveTests covers satisfiable and unsatisfiable outcomes, repeated solves, and integer round-tripping including Int32 boundaries. - TheoremCompositionTests covers Where immutability and accumulation, Theorem.ToString, the Z3Context.Log seam, Dispose being a harmless no-op, the NewTheorem(dummy) overload, and Symbols.ToString formatting. Assertions follow a determinism rule stated in the test doc comments: exact values are asserted only where the constraints admit exactly one model, otherwise the test asserts a model-independent invariant. Z3 does not promise which satisfying model it returns and Dependabot bumps NuGet packages daily. Unsatisfiable cases are kept trivially contradictory, because Solve returns default for both UNSATISFIABLE and UNKNOWN, so a merely slow theorem would otherwise pass an "is unsatisfiable" assertion. Writing these found a previously unknown defect: any symbol not referenced by a constraint makes Solve throw InvalidCastException, because model.Eval defaults to completion:false and an unreferenced constant evaluates to itself. Raised as endjin#51 and pinned by two characterisation tests rather than fixed, per the agreed approach of documenting defects for a later PR. Verified by mutation: making Where drop its new constraint fails 20+ tests across the suite, including these. Issues raised for the defects found by this review: endjin#51 unconstrained symbols, endjin#52 culture-sensitive MkReal, endjin#53 collection-typed fields, endjin#54 float round-trip, endjin#55 decimal arrays, endjin#56 DateTime timezone, endjin#57 value-type unsat ambiguity, endjin#58 Optimize nullability. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…lias
The comment claimed the bare name Environment is CS0104-ambiguous between
System.Environment and Z3.Linq.Environment. It is not: these tests live in
namespace Z3.Linq.Tests, so the enclosing Z3.Linq namespace is searched before
any using directive and the name binds to Z3.Linq.Environment. Verified - a bare
Environment.NewLine gives CS0117 ('Environment' does not contain a definition
for 'NewLine'), not CS0104.
The Z3Environment alias the wrong explanation justified was never used, so it
goes with it rather than being kept alive by a corrected comment.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…hapes Phase B of the test plan, covering the layer that turns a Z3 model back into a CLR object. 39 tests -> 87; line coverage 38.8% -> 62.9%, branch 52.1%. Writing these found that four of the types the library presents as supported do not work at all, none of which any example exercises: - short throws InvalidCastException before it reaches the solver, and would throw ArgumentException on the way back even if that were fixed (endjin#63, new) - every collection element type except int fails translation with a Z3 sort error - long, bool, double, decimal and string (endjin#64, new) - float solves and then fails to marshal (endjin#54) - a real constant is written to Z3 using the current culture, so a comma-decimal culture produces a parser error (endjin#52) Each is pinned by a characterisation test naming the issue, per the standing decision to document rather than fix defects in this work. endjin#55 turned out to be unreachable and has been annotated: decimal arrays die at translation long before the element-evaluation bug it describes can be observed. The culture test runs its work on a dedicated thread rather than setting CurrentCulture on the test's own. These run in parallel at method level on pooled threads, so mutating culture in place could leak into whatever ran next. DateTime is asserted in a form that holds in any time zone: the instant round trips correctly, but the value returns as Kind=Local, so comparing it to the UTC value supplied fails by exactly the local offset (endjin#56). Mutation-checked: reading Int64 model values through .Int fails 3 tests, and reading every array element from index 0 fails 3 tests. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
An unbounded Join means a solver that never returns hangs the entire run with no indication of which test stopped. A bounded one fails that test and lets the rest finish. The limit is 30 seconds against work that takes single-digit milliseconds, so it is slack rather than a tuned value. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phase C of the test plan. 87 tests -> 102; line coverage 62.9% -> 69.9%, branch 52.1% -> 54.7%. The whole optimisation surface was previously untested despite being the feature the README leads with. Covers both directions, the orderby operators and their equivalence to the Optimize calls they delegate to, deferred execution, objectives over several symbols, reuse of a theorem across calls, and the oil purchase linear program from the README - whose optimum is a single vertex, 2200 and 3100 barrels for $90,500, so the cost is safe to assert exactly. Pins endjin#58: an unsatisfiable Optimize returns default! through a non-nullable T. Solve returns T? and makes the caller check; Optimize promises a value and then hands back a null the compiler has been told cannot exist, so the caller dereferences it somewhere else entirely. Deferred execution is asserted through the Z3Context.Log seam rather than by timing or by relying on a theorem that throws: an eager OrderBy would have written its asserted constraints to the log before Solve was called. Mutation-checked, including the mutation that matters most here - never attaching the objective to the optimiser, so Optimize degenerates into Solve, fails 5 tests. Swapping Minimize and Maximize fails 9; mapping OrderBy to Maximize fails 2. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two test names used -ise while the rest of the file, and the Optimization enum they describe, use -ize. Someone grepping for Minimize would have missed them. Identifiers now follow the API; comment prose stays as it is. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phase D of the test plan. 102 tests -> 120; line coverage 69.9% -> 76.2%, branch 54.7% -> 68.7%. Branch coverage moves most here because throw sites are branches, and none of them had ever been executed. UnsupportedExpressionTests pins the boundary of the translator: Distinct called outside a query, ternaries, unrecognised method calls, unsupported casts, char, uint and nullable properties, and two levels of object collections. These matter as much as the supported cases - a change that quietly stops rejecting something does not fail loudly, it produces a theorem meaning something other than what was written. RewriterTests covers both extension points, which were public API and entirely unverified. The tests assert what a rewrite did rather than that one ran: a global rewriter appends a constraint no query mentions, and another discards a contradiction so an unsatisfiable theorem becomes satisfiable. A predicate rewriter turns a call the visitor would reject into Z3Methods.Distinct, checked both for being accepted and for meaning something - the unsatisfiable case would still pass if the rewrite were built and then dropped. Assertions are on exception type, not message. Several messages are misspelled or malformed; pinning them would turn a typo fix into a test failure. Also found that enums fail exactly as short does, same Convert defect, same fix - recorded on endjin#63. Mutation-checked: discarding the global rewriter's return value fails the 2 effect-based tests, and removing its interface check fails 1. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phase E of the test plan, and the last of it. 120 tests -> 133. These are the only tests that exercise the library at realistic size - 81 symbols, 27 Distinct constraints and a global rewriter in one theorem - so they are where a translation regression that only appears at scale would surface. Sudoku puzzle B is published and uniquely solvable, so its grid is asserted cell by cell. Puzzle A has 21 givens and almost certainly several solutions, so it is asserted by invariant: the givens survive and every row, column and box is a permutation of 1-9. Missionaries and Cannibals is checked against the rules of the puzzle at every step, not just its length, so an optimiser that reached the optimum by violating the safety rule would still fail. Measured before classifying, per the plan. Two of its numbers were wrong: the optimal crossing is 12 states rather than 11, and the smallest feasible maxLength is 13 rather than 12 - the goal requires Length < maxLength, so a bound equal to the optimum is one short. Both boundaries are now pinned. No test is tagged Slow because none needs to be. After dropping one pathological case the whole suite runs in 946ms and the slowest test is 443ms, so the category and the AdditionalTestArgs filter are both skipped as the plan directed. That dropped case was a Sudoku with no givens. It solved correctly but took 25 seconds - fifty times the next slowest test - because an unconstrained grid gives Z3 nothing to propagate from. It proved only that the constraints are satisfiable alone, which the two real puzzles already establish while also checking an answer, and tagging it slow would have left a test that never runs. Coverage is 75.8% line and 69.3% branch. The line percentage is a shade below Phase D's 76.2% only because Z3.Linq.Examples now falls inside the coverage filter: covered lines went from 555 to 627 against a denominator that grew by 99. Mutation-checked: making Distinct assert nothing fails 11 tests, and reading every collection element from index 0 fails 6. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two gaps found in review, both real. The puzzle A test constrained 21 givens and asserted 8 of them, under a comment claiming the givens survive the solve. A regression that dropped or mistranslated some but not all of the constraints would have passed. All 21 are now asserted - that failure mode is the whole reason for testing at this size. AssertIsValidCrossing checked how many people moved per step but not which way they went. The sample alternates by parity - from an even step the boat leaves the near bank, from an odd step it returns - so a plan that crossed twice in the same direction without the boat coming back would have satisfied a magnitude-only check. The direction is now asserted per step. Verified the new check has teeth: inverting its parity fails 3 tests. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A Z3 model is partial: it assigns values only to the constants the solver actually needed. Marshalling a solution evaluated every symbol without asking for model completion, so a symbol the model did not interpret evaluated to the term itself - an IntExpr rather than an IntNum - and the cast failed. The condition is not "no constraint mentions it" but "the model does not interpret it": a tautology the solver discards as it is asserted leaves its symbol uninterpreted just the same. All four evaluation sites now route through one EvaluateWithCompletion helper, so the invariant is stated and enforced in one place rather than repeated four times - which is how the omission came to exist at all. The helper is appended at the end of the class so that no line moves and the ~23 Theorem.cs:NNN citations in the test comments stay accurate. Fixes endjin#51. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The signature is deliberate rather than an oversight, but nothing said so. It now records that Environment.Expr is nullable, that the anonymous-type branch passes it unguarded, that the resulting NullReferenceException is reachable and pre-existing, and that endjin#75 tracks a better fix than a defensive guard would be. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Thirty-two tests carried a constraint - usually .Where(t => t.X2 == 0) - whose only purpose was to keep the second symbol referenced, because an unreferenced one made Solve throw. With endjin#51 fixed they are noise, and they were actively misleading: a reader could not tell which constraints were part of a test's subject and which were there to work around a defect. Removing them turns those tests into regression coverage for the fix. Reverting the completion flag now fails 51 tests rather than 12. Constraints whose value a test actually asserts are kept - the point stands only where the symbol was genuinely incidental. Also captures the exception on the invariant-culture thread. That solve ran on a bare Thread with no try/catch, so an exception there was unhandled and killed the test host: the run reported "zero tests ran" instead of one failure, which made the mutation check above impossible to read. Its sibling pin already did this. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ExpressionVisitor handed real constants to Z3 with the current culture, so a comma-decimal culture produced "1,5" and Z3's parser rejected it. Measured over the 606 specific cultures installed on this machine, 301 of them - about half - could not solve a theorem containing a real literal. The two culture tests move out of SymbolTypeMarshallingTests into a file of their own, joined by coverage for the negative-sign and non-comma-separator cases that a naive fix would miss. Fixes endjin#52. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The solve threads were foreground, so one that outlived its bounded Join would hold the test host open indefinitely - measured: a process whose Main has returned does not exit at all while a foreground thread is still running. That turned the timeout from a clean failure into a stalled run. SolveOn now takes the resolved CultureInfo rather than a name, so the control test names the invariant culture instead of passing an empty string, and the timeout message has something to say for it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Working out how many elements to marshal cast the FieldInfo itself rather than the collection it points at, so every environment with a collection in a public field threw InvalidCastException. Scalar fields were unaffected; the property branch beside it was already correct. Fixing it makes the element-materialisation loop reachable through a field for the first time, so the tests walk that whole path rather than stopping at the one case in the issue. Fixes endjin#53. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
TypeCode.Single parsed the model value with double.Parse, so a solved float symbol was boxed as a double and reflection refused to write it to a float member. Translation, solving and the model were all correct; only the last step lost the answer. Parsing straight to float rounds once rather than parsing to double and narrowing. The array element arm carried the same defect and is corrected with it, though no test can reach it while endjin#64 stands. Fixes endjin#54. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The decimal arm of the array element loop evaluated subEnv.Expr - the whole array constant - instead of numValExpr, the element the loop had just selected with MkSelect. Every other arm of that loop uses numValExpr. Casting an ArrayExpr to RatNum can never succeed, so the arm always threw InvalidCastException rather than giving every element the same value, which is what the issue predicted as the alternative. endjin#64 recorded this code as unreachable. That holds only for a constraint naming a decimal constant, which fails during translation. With the elements left free the theorem solves and the loop runs, which is how the three new tests observe the fix. Fixes endjin#55. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
".NET Interactive" is now "Polyglot Notebooks", and Microsoft deprecated both in early 2026 and archived dotnet/interactive (read-only since April 2026). No community-maintained fork has been established - only discussed. Renames the reference, adds a sourced deprecation note, and leads the Examples section with the single-file demos as the maintained, tooling-free way to run the examples. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PipoHZJsgydrV3JC3fQN6Q
Microsoft deprecated and archived Polyglot Notebooks / .NET Interactive, so the examples/z3-problems.dib notebook and every reference to it are removed: the Examples section now points only to the maintained single-file demos, the "For Polyglot Notebooks" getting-started subsection is dropped, and the stale notebook link in the project history is removed. The examples/ folder held only the notebook, so it is gone too. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PipoHZJsgydrV3JC3fQN6Q
A collection symbol is modelled as a single Z3 array constant, read with Select. That is the right model for a constraint that indexes with a symbol, but not for the classic binding model, where each element is a constant of its own and a constraint can name it. CollectionHandling.Constants gives each element its own constant, created lazily on first index access, so a collection nothing reads costs nothing. The mode lives on Z3Context, propagates to every theorem it creates and is re-propagated by Where, so a fluent chain does not silently fall back to the array model. A symbolic index in Constants mode is refused by name rather than cast to a null ArrayExpr. The read-back follows the same split: element constants are read from the collection's sub-environments, an index the constraints never named comes back as the element type's default, and the solution keeps the length of the template or instance collection, extended past the highest materialised index. Tests: the 4x4 Sudoku CSP and the three element-type cases run in both modes, plus a guard that a bare context still defaults to Array. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
A collection whose element type is itself a collection - int[][], List<int[]> - was modelled as one array per property of the element type (Length, Rank, SyncRoot, and so on), because the element type code is Object and the object-collection branch caught it. Nothing about a nested grid was representable, so a theorem over int[][] could not be stated. An array of arrays is now an array whose range is the sort the element type's own array would get, computed recursively, so a Select on the outer array yields a row. The read-back descends the same way: the selected row term becomes the row's environment, which needs no marker on the environment and works at any depth of nesting. Tests: a 4x4 Sudoku over int[][] in both collection modes, with and without a hint constraining an interior cell. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
VisitMember unpacks a captured constant by walking the member hierarchy, but it read every level off the root constant instead of off the previous level. That works for the common single-field closure and fails on the second level with "field ... is not a field on the target object". Two ordinary shapes reach it. A lambda that captures a method parameter and a loop variable: Roslyn gives the loop body its own display class nested in the method's, so the outer value sits two fields deep. And a property read off a captured instance, limit.Value: a field then a property. Each level is now read off the value the previous level produced, which is what the hierarchy of member accesses already meant. Tests: the per-iteration floor built from a method parameter, and a captured instance property constraining a solution and making one unsatisfiable. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
The binary + translates to a pairwise addition, so summing an arbitrary number of theorem-collection elements needed per-element unrolling - the shape an aggregation such as sum of price[i] * quantity[i] over a collection cannot write. Sum joins Distinct on the variadic path the visitor already had: both take a params array, both accept a literal NewArrayExpression or a Select(...).ToArray() over a runtime collection, and they differ only in the term built from the materialised arguments. Add is variadic, so the sum is one node rather than a fold. Tests: a sum over a collection in both collection modes, its upper bound asserted by a satisfiable case and its strict complement by an unsatisfiable one, and the indicator encoding with a conditional sum counting the true flags. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…ndjin ExactlyOne, AtMostOne et AtLeastOne sont traduits en contraintes pseudo-Booleennes natives (MkPBGe sur les indicateurs et leurs negations) plutot qu'en une expansion Ite + Add : Z3 garde sa propagation de cardinalite et le terme ne croit pas quadratiquement avec la taille du groupe. L'extraction des arguments variadiques est factorisee (MaterializeVariadicArguments), partagee avec Distinct et Sum, et accepte desormais toute source IEnumerable : la version heritee exigeait ICollection et echouait sur Enumerable.Range, donc sur tout groupe dont la taille est une valeur de runtime -- precisement la capacite que ces methodes existent pour offrir. Suite : 350/350.
…le endjin WeightedAtLeast, WeightedAtMost et WeightedExactly se traduisent en MkPBGe / MkPBLe / MkPBEq natifs. Les poids et la borne decrivent le groupe, ils ne participent pas a la contrainte : ils sont donc evalues cote hote (EvaluateToHostValue, avec le meme contournement LambdaExpression que pour les arguments variadiques) au lieu d'etre traduits en termes. Un desaccord de longueur entre poids et indicateurs leve une erreur explicite plutot que d'apparier silencieusement le plus court des deux. Suite : 359/359.
…la pile endjin Le domaine est une valeur hote, le predicat est substitue element par element puis replie, et les termes obtenus sont combines en MkAnd (universel) ou MkOr (existentiel). Le domaine vide tombe de cette lecture plutot que d'un cas particulier : une conjonction vide tient, une disjonction vide non. Ce sont des quantificateurs a domaine fini, pas des quantificateurs SMT sur un tri non borne -- la distinction est observable sur le domaine vide, et les tests la fixent. Suite : 365/365.
Le chemin de lecture des symboles Single et Double passait par RatNum.ToDecimalString(32|64) puis float.Parse / double.Parse. Deux defauts mesurables en decoulaient : - une valeur dont l'expansion decimale ne termine pas (1/3) sortait marquee d'un « ? » que seul le bras Decimal retirait, donc la lecture levait FormatException apres une resolution reussie ; - aucun nombre fixe de decimales ne peut exprimer toutes les valeurs d'un type binaire : a 32 places, float.Epsilon se lit « 0.000...0? », soit zero. La lecture passe desormais par le numerateur et le denominateur reduits par Z3, chacun ramene a 64 bits avec son exposant conserve a part, ce qui garde les deux casts dans la plage du double quelle que soit la magnitude (1/2^1074, le rationnel de double.Epsilon, ne tient pas dans un double ; son quotient si). Les trois tests de SymbolTypeMarshallingTests qui epinglaient le FormatException sont reecrits pour affirmer la valeur, comme leur propre remarque le demandait. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…endjin Un litteral reel atteint Z3 par MkReal(value.ToString()), exact pour un decimal qui termine et lossy pour tout le reste : 1.0/3.0 s'ecrit en seize chiffres tronques, donc x == 1.0/3.0 conjoint a 3*x == 1 est insatisfaisable alors que la contrainte est evidemment soluble. Rational porte une fraction num/den reduite dans l'arbre d'expression et l'emission la traduit en rationnel exact, si bien que x == Rational.Of(1, 3) conjoint a 3*x == 1 tient. Les six operateurs de comparaison existent dans les deux ordres pour qu'un rationnel puisse figurer de chaque cote d'une contrainte sur un membre reel. Cote visiteur, deux ajouts : - VisitConstantValue reconnait un Rational et l'emet par MkReal de sa fraction ; - a defaut de branche dediee, un appel qui ne mentionne aucun parametre du theoreme n'est pas un terme : il produit la valeur qu'il produit, et seule cette valeur appartient a la traduction. Sans cela Rational.Of(1, 3) - une fabrique statique, le seul moyen d'ecrire une fraction exacte dans un lambda - serait refuse comme appel de methode inconnu. Le repli vient apres les methodes magiques et les indexeurs, qui sont des appels que le DSL traduit et que ce repli evaluerait sur l'hote. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…nstraints Solve collapses every non-satisfiable outcome to default(T): "the constraints contradict each other" and "Z3 ran out of budget" arrive as the same value, and nothing says which constraints conflict. Explain reports Z3's own status and, on a conflict, the unsatisfiable core - the hard Where constraints its refutation used, by position and source text. Each constraint is asserted under a fresh tracking literal, so the solver is pinned to the general-purpose Context.MkSolver() rather than taking what the context is configured to build: core extraction rides on hypothesis tracking, and a backend without it returns an empty or partial core, which is a wrong answer rather than a slow one. The scalar type bounds the solve path adds are asserted here too, untracked, so the two surfaces cannot disagree about a theorem whose only conflict is a value outside its CLR type's range. Solve is untouched, including the TheoremUndecidedException it throws; the shared constraint resolution moved into GetConstraintsToAssert so a registered global rewriter cannot make the two paths read different systems, and the check itself split into Check (throws on UNKNOWN) and CheckStatus (returns it). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
… may sacrifice A Where constraint is required to hold: violating it makes the theorem unsatisfiable, so "satisfy this if you can, but prefer that one" could not be written at all. SoftWhere adds a constraint the optimizer may leave unsatisfied at a cost, with a strictly positive weight and a MaxSAT group; Z3 then minimises the total weight it leaves unsatisfied, which is what makes a weight a statement of priority. A theorem carrying at least one soft constraint is checked through MkOptimize rather than a plain solver, since an implicit objective has nowhere to live on a solver. TrySolve now selects the object once and reads the model off it, and AssertConstraints asserts the soft set into the optimizer only - the solve path is the only caller that can reach it with any. The soft set travels through the Where chain next to the hard one: the two lists are independent, and dropping one there would silently turn a trade-off into a requirement. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…ic sequence The solve path hard-coded Context.MkSolver(), so a solver specialised to the constraint fragment could not be chosen even when the fragment was known, and the strategy a caller wanted could not be expressed at all. SolverKind selects the combined, the simple or a logic-specialised solver; a non-empty Tactics sequence composes Z3 tactics left to right and takes precedence over the kind, since a tactic sequence already ends in a decision procedure. Asking for SolverKind.Logic without naming the logic fails rather than silently building the general-purpose solver Z3 falls back to. The two paths that need something other than a solver are untouched: the optimizer a soft constraint requires, and the diagnostic path, which needs the hypothesis tracking a combined solver provides. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…rameters Two configuration surfaces the solve path lacked. [BitVecWidth] turns an integral member into a bit-vector constant of the declared width, so its arithmetic wraps modulo 2^n and its comparisons are the unsigned bit-vector ones. That is what makes an overflow predicate such as a + b < a satisfiable at all: over unbounded integers it is simply false. A literal beside a bit-vector is read as a width-matched bit pattern, since a constant does not carry a sort of its own, and the read-back goes through the unsigned value - a BitVecNum is not an IntNum, so the integer cast would throw. SetParameter sets a Z3 solver parameter (random_seed, phase_selection, ...), applied per check alongside the timeout and resource limits. It is typed because Z3 types its parameters: random_seed takes an unsigned integer and fails when handed a symbol, so the caller states the type instead of the library guessing one from the text. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Two defects the ported suites expose, both in the translation and the read-back. A static member had no root expression to read from, so a theorem written against DateTime.MaxValue failed with "Unknown parameter encountered: MaxValue". A static member is folded the same way a captured instance is, from a null starting value. An element read that narrows to a small type used a bare checked cast, so a value the type cannot hold surfaced as "arithmetic overflow" with no idea which symbol it came from. The narrowing now names the symbol, as the DateTime element read already did - which is the only place it can happen, a scalar being bounded to its own range. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
The bit-vector suite pins the capability the [BitVecWidth] attribute exists for: a predicate that is satisfiable over 4-bit bit-vectors and unsatisfiable over mathematical integers. `a + b < a` with `b >= 1` wraps below `a` in one theory and has no witness in the other, and the same test asserts both halves, so neither outcome can pass by accident. The remaining cases cover wrap-to-zero on addition and multiplication, a literal coerced to the declared width, unsigned ordering (`A > 15` has no 4-bit witness), and read-back honouring the width. The list suite is a source fix as much as a test port: a `List<T>` indexer compiles to a `get_Item` call, not to an ArrayIndex node, so it never reached the Constants-mode per-element path and fell through to `MkSelect`, which assumes an ArrayExpr that mode never builds. `VisitCall` now resolves the element the same way the ArrayIndex path does - bound environment, then element environment at the constant index - and returns early only when that element has an expression of its own, so a nested collection still falls through to Select for the next level. Both modes are pinned for int and bool, plus an unreferenced index coming back as the element type's default. Suite 412 -> 424, green before the commit. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Two capabilities the pile did not have, each with its suite. Witness. `Solve` built a model, populated the result object and dropped the model, so a value that is not itself a member of the environment - the derived `t => t.X + t.Y`, or a relational fact like `t.X < t.Y` - could not be read back at all. `Solve(inspect)` now hands the caller a `ModelWitness<T>` while the native context is still alive; `Eval` folds the body, translates it against the same environment and reads it through the same scalar path a member goes through, so the witness and the solution agree by construction. The callback is not invoked on UNSAT, where there is no model to witness, and it is exercised over an optimizer model as well as a solver one - the soft-constraint case reads the MaxSAT-chosen value, not a solver's. Reconstruction. `GetSolution` knew two shapes: an anonymous type, rebuilt through its backing fields, and a named type, built with `Activator.CreateInstance` and property setters. A positional record is neither - no public parameterless constructor, and init-only members - so it threw `MissingMethodException`. A third branch matches each constructor parameter to an environment member by name, reads it from the model and invokes the primary constructor; the longest fully-readable constructor wins, so a copy or convenience overload never displaces it. Value types keep the existing branch, which they need. The template supplies collection lengths, as it does for a named environment. The one pile test that asserted the record limitation (`Solve_PositionalRecordEnvironment_ ThrowsMissingMethodException`) is flipped rather than deleted: its subject is real, only its expectation was a description of the missing branch. Suite 424 -> 432, green before the commit. Crefs naming `Solve` are disambiguated, since a second overload makes them ambiguous under TreatWarningsAsErrors. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
The notebooks reach this library through `#r "../Z3.Linq/.deploy/..."`, so the four assemblies they load are committed here and refreshed whenever a fix has to reach them - the same convention as the DateTime and Int16 refreshes before this one. Produced with `dotnet publish solutions/Z3.Linq/Z3.Linq.csproj -c Release`. All four change, not just the library: the port moves to net10 on the pile, which brings Microsoft.Z3 5.1.0 and its native libz3, and the MiaPlaza ExpressionUtils version the pile pins. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…t repro over from the fork The port dropped three artefacts the fork's main still carries: the Sudoku grid example (SudokuGrid + SudokuGridTheorem, range/distinct constraints over g.Cells[i][j]), the pseudo-Boolean MkPBGe-vs-MkIte benchmark harness, and the CrossSubmissionCaptureRepro notebook that pinned the polyglot capture bug fixed by the fork's partial-eval pass. pb-bench.csproj is adapted: it pinned net8.0 on the fork, which cannot reference the net10.0 library it measures - the target framework now comes from Directory.Build.props like every other project, and the project is registered in the .slnx. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
… translating A constraint reading an element of a captured collection - kcalArr[i], or a captured lookup table - used to fail with 'Unsupported constant System.Int32[]': the element access arrives as an ArrayIndex (or a get_Item call) over a ConstantExpression holding the whole array, and the visitor translates scalars, so the array itself reached VisitConstantValue. The fork's whole-constraint partial evaluation covered this; the port had dropped that pre-pass, and a G5 meal-planner notebook regressed on it. Two moves restore the coverage without breaking the pile's marker design: - Theorem.TranslateConstraint folds the constraint body again, except when the body mentions a Z3Methods marker - those calls throw at runtime by design (they are translated, never run), which is what broke UnweightedPbTests.EmptyGroup_IsDecided on the first attempt. - The visitor folds a closed element read itself (TryFoldClosedRead): a node that mentions no parameter and no marker denotes a constant, so it is evaluated and translated as one; anything else, or an evaluation that fails, falls through to the previous paths. Pinned by CapturedCollectionTests (array and list element, element times a symbol, element inside a soft constraint, both collection modes). Suite: 437/437. Measured on the real artifact: notebook 06 of the G5 series went from '28 cells, 1 error' to '28 cells, 0 errors' on this build. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Author
|
Conflit avec Pourquoi le conflit existaitLes deux lignées ne partagent que la base endjin Subsomption mesurée avant de trancher
Politique de résolution (39 fichiers en conflit)
Le diff du merge contre la pointe de branche se réduit à 3 fichiers, +334/−5 — les deux docs et le commentaire. Validation post-mergeBuild : Delta connu assuméLa section README « Planning a Single Meal » (exemple PB one-hot de |
Code Coverage Summary Report - Linux (No TFM)Summary
CoverageZ3.Linq - 90.6%
Z3.Linq.Examples - 48.9%
|
Test Results 1 files ± 0 1 suites ±0 11s ⏱️ +7s Results for commit c8ef411. ± Comparison against base commit 8a2562d. This pull request removes 29 and adds 351 tests. Note that renamed tests count towards both. |
jsboige
added a commit
to jsboige/CoursIA
that referenced
this pull request
Oct 25, 2026
Le merge MyIntelligenceAgency/Z3.Linq#44 (68a6356f) porte exactement l'arbre deja valide de c8ef411 (diff vide). Suite fraiche: 437/437 tests, 0 echec. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
myia-ai-01
pushed a commit
to jsboige/CoursIA
that referenced
this pull request
Oct 27, 2026
…22570) * chore(submodule,#16609): bump Z3.Linq sur le port de la pile endjin (PR fork #44) Grain: LIGHT/infra -- lane myia-po-2025:CoursIA -- prev: DEEP/lean #22083 Gitlink 8a2562db -> 1ae1d3c : le fork porte desormais l'integralite de ses features sur la pointe de la pile endjin (feature/spectre-demos @ b425802, net10/MTP/Z3 5.1.0) -- 19 commits, build 0 warning, suite 437/437, serie G5 re-executee (17/18 verts, 06 et 07 compris ; 10 barre par le sous-module Automata non initialise localement). Voir MyIntelligenceAgency/Z3.Linq#44 pour le detail (porte, retire par la pile, non porte). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * chore(submodule,#16609): pointer Z3.Linq sur le main issu du merge #44 Le merge MyIntelligenceAgency/Z3.Linq#44 (68a6356f) porte exactement l'arbre deja valide de c8ef411 (diff vide). Suite fraiche: 437/437 tests, 0 echec. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * chore(submodule,#16609): rebump Z3.Linq sur 0f00539d8b -- .deploy net8.0 (voie 2 de la review #22570) Le fork MyIntelligenceAgency/Z3.Linq#45 (multi-ciblage net8.0;net10.0, build net8.0 deposeee dans .deploy/) est merge en 0f00539d8b. Marqueur mesure dans la DLL : .NETCoreApp,Version=v8.0 -- compatibilite .NET 8/9 des postes etudiants restauree, mesure au meme instrument que la review. Le merge de ce bump reste apres les seances TP du 26/10 (calendrier de la review). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fork ported onto the endjin pile tip (feature/spectre-demos @ b425802)
Grain: DEEP/refactor — lane myia-po-2025:CoursIA — prev: DEEP/lean #22083
What this is
The fork's entire feature set, rebased and adapted onto the tip of the endjin
pile (
feature/spectre-demos@b425802), following the endjin direction theupstream PRs (endjin#110, with #43 and endjin#111 rebased on it) have converged on:
net10.0, MSTest + Microsoft.Testing.Platform, Shouldly, enforced XML docs,
Microsoft.Z35.1.0 from the local folder feed,.slnx, central packagemanagement,
demos/replacing the Polyglot notebooks.Method: final state per feature — one commit + green build + green suite at
each step (see the individual commits; 19 on top of the pile tip).
What is carried
Every fork feature was ported and re-validated test-by-test: bit-vector width
declarations and solver parameters, witness evaluation and constructor-based
reconstruction, the DateTime / Int16 / ternary round-trip suites, the
bit-vector theory and list-collection suites, rational constants,
.deployconvention, plus the two fixes below.
fda0d34): the Sudoku example(
SudokuGrid+SudokuGridTheorem), thepb-benchMkPBGe-vs-MkIte harness(csproj re-targeted to inherit net10.0 from
Directory.Build.props— thefork's copy pinned net8.0, which cannot reference the net10.0 library), and
the
CrossSubmissionCaptureRepronotebook.1ae1d3c): a constraint reading an element ofa captured collection (
kcalArr[i]) regressed on the port — the fork'swhole-constraint partial evaluation covered it, the port had dropped that
pre-pass. Restored, guarded so a body mentioning a
Z3Methodsmarker (whoseruntime bodies throw by design) is never evaluated; the visitor also folds
closed element reads itself (
TryFoldClosedRead). Pinned byCapturedCollectionTests.What the pile deliberately removed (not carried back)
The Polyglot
.dibfiles and theZ3.Linq.Demoproject — replaced by thepile's
demos/.Deliberately not carried
DIVERGENCE_STATUS.mdandOVERLAP_G1.md— coordination artefacts of theporting effort itself, not library code; they stay in the working history if
needed.
Validation
dotnet buildon the full solution: 0 warnings, 0 errors (XML docs andTreatWarningsAsErrorson).captured-collection tests and the previously-breaking
UnweightedPbTests.EmptyGroup_IsDecided..deployDLLs): 17/18 green, 0 errors — including notebook 06 (the
captured-array regression case: 28/28 cells) and notebook 07 (10/10 cells
once the pinned Wayback corpus completed to 110/110 batches). Notebook 10
is blocked on the
Automatasubmodule not being initialised locally — alocal environment barrier, not a library defect.
🤖 Generated with Claude Code