diff --git a/PerfectNumbers.Core.Tests/BitContradictionSolverTests.cs b/PerfectNumbers.Core.Tests/BitContradictionSolverTests.cs index cfb365f..837ce2e 100644 --- a/PerfectNumbers.Core.Tests/BitContradictionSolverTests.cs +++ b/PerfectNumbers.Core.Tests/BitContradictionSolverTests.cs @@ -1,3 +1,4 @@ +using System.Numerics; using FluentAssertions; using PerfectNumbers.Core.ByDivisor; using Xunit; @@ -22,7 +23,7 @@ public class BitContradictionSolverTests [Fact] public void TryPropagateCarry_FailsWhenParityUnreachable() { - CarryRange carry = CarryRange.Single(0); + CarryRange carry = CarryRange.Single(0); bool success = TryPropagateCarry( currentCarry: ref carry, forcedOnes: 0, @@ -34,10 +35,34 @@ public class BitContradictionSolverTests carry.Max.Should().Be(0); } + [Fact] + [Trait("Category", "Fast")] + public void ShouldPruneWithFinalPow2Shift_ReturnsTrue_WhenShiftedResidueStaysBelowModulusAndResidueIsNotOne() + { + bool shouldPrune = ShouldPruneWithFinalPow2Shift( + prefixResidue: new BigInteger(3), + modulus: new BigInteger(1000), + tailShift: 8); + + shouldPrune.Should().BeTrue(); + } + + [Fact] + [Trait("Category", "Fast")] + public void ShouldPruneWithFinalPow2Shift_ReturnsFalse_WhenResidueIsOne() + { + bool shouldPrune = ShouldPruneWithFinalPow2Shift( + prefixResidue: BigInteger.One, + modulus: new BigInteger(1000), + tailShift: 8); + + shouldPrune.Should().BeFalse(); + } + [Fact] public void TryPropagateCarry_ComputesNextCarryRange() { - CarryRange carry = new(0, 1); + CarryRange carry = new(0, 1); bool success = TryPropagateCarry( currentCarry: ref carry, forcedOnes: 1, diff --git a/PerfectNumbers.Core/ByDivisor/BitContradictionSolverWithAMultiplier.cs b/PerfectNumbers.Core/ByDivisor/BitContradictionSolverWithAMultiplier.cs index 3403595..e1bf9ee 100644 --- a/PerfectNumbers.Core/ByDivisor/BitContradictionSolverWithAMultiplier.cs +++ b/PerfectNumbers.Core/ByDivisor/BitContradictionSolverWithAMultiplier.cs @@ -1,120 +1,134 @@ -using System.Runtime.CompilerServices; +using System.Runtime.CompilerServices; using System.Numerics; using PerfectNumbers.Core; +using ILGPU; namespace PerfectNumbers.Core.ByDivisor; internal sealed class PrivateWorkSet { - private const int QPrefixReverseCacheSize = 1024; + // Active hot-path scratch buffer. + public ulong[] KnownOne1 = []; - // Per-thread scratch buffers to avoid per-run allocations in the hot path. - // Buffers grow on demand and are never shrunk. - public ulong[] KnownOne0 = []; - public ulong[] KnownOne1 = []; - public ulong[] KnownZero0 = []; - public ulong[] KnownZero1 = []; - public ulong[] QMaskWords = []; - public ulong[] AOneWin = []; - public ulong[] AZeroWin = []; - public int[] PrevOffsets = []; - public int PrevOffsetsLength; - public bool HasPrevOffsets; - public BigInteger[] InvByKMod = []; - public bool[] HasInvByKMod = []; - public bool HasLastInvMod2k; - public BigInteger LastInvMod2k = BigInteger.Zero; - public BigInteger LastPow2K = BigInteger.Zero; - public BigInteger LastPow2QMod2k = BigInteger.Zero; - public bool HasLastPow2QMod2k; - public byte[] QMod2kBytes = []; - public ulong[] QPrefixReverseKeys0 = []; - public ulong[] QPrefixReverseKeys1 = []; - public ulong[] QPrefixReverseValues0 = []; - public ulong[] QPrefixReverseValues1 = []; - public ulong[] QPrefixReverseValues2 = []; - public ulong[] QPrefixReverseValues3 = []; - public ulong[] QPrefixReverseValues4 = []; - public ulong[] QPrefixReverseValues5 = []; - public ulong[] QPrefixReverseValues6 = []; - public ulong[] QPrefixReverseValues7 = []; - public ulong[] QPrefixReverseValues8 = []; - public ulong[] QPrefixReverseValues9 = []; - public ulong[] QPrefixReverseValues10 = []; - public ulong[] QPrefixReverseValues11 = []; - public ulong[] QPrefixReverseValues12 = []; - public ulong[] QPrefixReverseValues13 = []; - public ulong[] QPrefixReverseValues14 = []; - public ulong[] QPrefixReverseValues15 = []; - public bool[] QPrefixReverseValid = []; - public ulong[] LastQPrefix = []; - public ulong[] LastQReverse = []; - public bool HasLastQPrefix1024; +#if false + private const int QPrefixReverseCacheSize = 1024; + private const int ForcedALowBits = PerfectNumberConstants.BitContradictionForcedALowBits; - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void EnsureCapacity(int wordCount, int qWordCount) - { - if (KnownOne0.Length < wordCount) - { - EnsureUlong(ref KnownOne0, wordCount); - EnsureUlong(ref KnownOne1, wordCount); - EnsureUlong(ref KnownZero0, wordCount); - EnsureUlong(ref KnownZero1, wordCount); - } + // Currently disabled buffers retained for quick restore. + public ulong[] KnownOne0 = []; + public ulong[] KnownZero0 = []; + public ulong[] KnownZero1 = []; + public ulong[] QMaskWords = []; + public ulong[] AOneWin = []; + public ulong[] AZeroWin = []; + public int[] PrevOffsets = []; + public int PrevOffsetsLength; + public bool HasPrevOffsets; + public BigInteger[] InvByKMod = []; + public bool[] HasInvByKMod = []; + public bool HasLastInvMod2k; + public BigInteger LastInvMod2k = BigInteger.Zero; + public BigInteger LastPow2K = BigInteger.Zero; + public BigInteger LastPow2QMod2k = BigInteger.Zero; + public bool HasLastPow2QMod2k; + public byte[] QMod2kBytes = []; + public ulong[] QPrefixReverseKeys0 = []; + public ulong[] QPrefixReverseKeys1 = []; + public ulong[] QPrefixReverseValues0 = []; + public ulong[] QPrefixReverseValues1 = []; + public ulong[] QPrefixReverseValues2 = []; + public ulong[] QPrefixReverseValues3 = []; + public ulong[] QPrefixReverseValues4 = []; + public ulong[] QPrefixReverseValues5 = []; + public ulong[] QPrefixReverseValues6 = []; + public ulong[] QPrefixReverseValues7 = []; + public ulong[] QPrefixReverseValues8 = []; + public ulong[] QPrefixReverseValues9 = []; + public ulong[] QPrefixReverseValues10 = []; + public ulong[] QPrefixReverseValues11 = []; + public ulong[] QPrefixReverseValues12 = []; + public ulong[] QPrefixReverseValues13 = []; + public ulong[] QPrefixReverseValues14 = []; + public ulong[] QPrefixReverseValues15 = []; + public bool[] QPrefixReverseValid = []; + public ulong[] LastQPrefix = []; + public ulong[] LastQReverse = []; + public bool HasLastQPrefix1024; +#endif - if (QMaskWords.Length < qWordCount) - { - EnsureUlong(ref QMaskWords, qWordCount); - EnsureUlong(ref AOneWin, qWordCount); - EnsureUlong(ref AZeroWin, qWordCount); - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public void EnsureCapacity(int wordCount, int qWordCount) + { + if (KnownOne1.Length < wordCount) + { + EnsureUlong(ref KnownOne1, wordCount); + } - if (InvByKMod.Length != 1024) - { - InvByKMod = new BigInteger[1024]; - HasInvByKMod = new bool[1024]; - } - if (QMod2kBytes.Length != 128) - { - QMod2kBytes = new byte[128]; - } - if (QPrefixReverseKeys0.Length != QPrefixReverseCacheSize) - { - QPrefixReverseKeys0 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseKeys1 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues0 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues1 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues2 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues3 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues4 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues5 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues6 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues7 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues8 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues9 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues10 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues11 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues12 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues13 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues14 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValues15 = new ulong[QPrefixReverseCacheSize]; - QPrefixReverseValid = new bool[QPrefixReverseCacheSize]; - } - if (LastQPrefix.Length != 16) - { - LastQPrefix = new ulong[16]; - LastQReverse = new ulong[16]; - } - } +#if false + if (KnownOne0.Length < wordCount) + { + EnsureUlong(ref KnownOne0, wordCount); + EnsureUlong(ref KnownZero0, wordCount); + EnsureUlong(ref KnownZero1, wordCount); + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void EnsureUlong(ref ulong[] arr, int needed) => Array.Resize(ref arr, needed); + if (QMaskWords.Length < qWordCount) + { + EnsureUlong(ref QMaskWords, qWordCount); + EnsureUlong(ref AOneWin, qWordCount); + EnsureUlong(ref AZeroWin, qWordCount); + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void EnsureInt(ref int[] arr, int needed) => Array.Resize(ref arr, needed); + if (InvByKMod.Length != ForcedALowBits) + { + InvByKMod = new BigInteger[ForcedALowBits]; + HasInvByKMod = new bool[ForcedALowBits]; + } + + if (QMod2kBytes.Length != (ForcedALowBits >> 3)) + { + QMod2kBytes = new byte[ForcedALowBits >> 3]; + } + + if (QPrefixReverseKeys0.Length != QPrefixReverseCacheSize) + { + QPrefixReverseKeys0 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseKeys1 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues0 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues1 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues2 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues3 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues4 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues5 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues6 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues7 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues8 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues9 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues10 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues11 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues12 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues13 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues14 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValues15 = new ulong[QPrefixReverseCacheSize]; + QPrefixReverseValid = new bool[QPrefixReverseCacheSize]; + } + + if (LastQPrefix.Length != 16) + { + LastQPrefix = new ulong[16]; + LastQReverse = new ulong[16]; + } +#endif + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void EnsureUlong(ref ulong[] arr, int needed) => Array.Resize(ref arr, needed); + +#if false + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void EnsureInt(ref int[] arr, int needed) => Array.Resize(ref arr, needed); +#endif } - - /// /// Helper utilities for the BitContradiction divisor search. These methods implement the /// interval-based carry propagation described in the BitContradictions plan document. @@ -123,4564 +137,5581 @@ internal sealed class PrivateWorkSet [DeviceDependentTemplate(typeof(ComputationDevice))] internal static class BitContradictionSolverWithAMultiplier { -private const ulong DebugTargetP = 138000001UL; -private static readonly BigInteger DebugTargetK = new(3); -private static readonly ulong DebugTargetQ = checked((ulong)((DebugTargetK * DebugTargetP) << 1)); -// private const ulong DebugTargetQ = 1209708008767UL; - -[MethodImpl(MethodImplOptions.AggressiveInlining)] -private static bool IsTargetCase(ulong p, System.Numerics.BigInteger k) => p == DebugTargetP && k == DebugTargetK; - -[MethodImpl(MethodImplOptions.AggressiveInlining)] -private static void Dbg(ulong p, System.Numerics.BigInteger k, string msg) -{ - if (IsTargetCase(p, k)) - Console.WriteLine(msg); -} - - - - private const int PingPongBlockColumns = 4096; - private const int TailCarryBatchColumns = 16384; - private const int TailCarryBatchRepeats = 1; - private const int TopDownBorrowColumns = 4096; - private const int TopDownBorrowMinUnknown = 12; - private const int PrefixRunCacheOffsets = 256; - private const int PrefixRunCacheCapacity = 256; - private const int ModLocalPrefilterMaxABits = 20; - private const int TopDownCacheCapacity = 16; - private const int HighBitCarryPrefilterColumns = 16; - private const int MiniPingPongPrefilterColumns = 60; - private const int QPrefixReverseCacheSize = 1024; - private const int QPrefixReverseCacheMask = QPrefixReverseCacheSize - 1; - - private static readonly int[] ModLocalPrefilterModuli = { 65537, 65521 }; - private static readonly ulong[] BitMask64 = CreateBitMask64(); - private static readonly byte[] ReverseByteLut = CreateReverseByteLut(); - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static long BestCaseCarryOutOneStep(long carryIn, int forced, int possible, int requiredBit /*1*/) - { - // Choose sum in [forced..possible] s.t. (carryIn + sum) % 2 == requiredBit, - // minimize carryOut = (carryIn + sum - requiredBit) / 2. - - int needSumParity = (requiredBit ^ ((int)carryIn & 1)) & 1; - - int sum = forced; - if ((sum & 1) != needSumParity) - sum++; - - if (sum > possible) - return -1; // parity infeasible in this column - - return (carryIn + sum - requiredBit) >> 1; - } - - // --- ADD near other helpers in BitContradictionSolverWithAMultiplier.cs --- - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static bool CouldStillReachTopCarryZero_UpperBound( - CarryRange carryIn, - int currentColumn, - int highColumn, - int maxPossibleOnesPerColumn) // this is "possible" = forced+remaining for *this* column; - { - // Quick conservative check: - // If even the *maximum* per-column ones cannot prevent carry from staying >=1 by the time we hit highColumn, - // we can prune. We use a crude but safe bound: - // - // carry_{t+1} >= floor(carry_t / 2) - // and carry_{t+1} <= floor((carry_t + maxPossibleOnesPerColumn) / 2) - // - // For a SAFE prune we need a LOWER bound on the best case (smallest achievable carry). - // The smallest carry you can get after one step is at least floor(carryMin / 2). - // After L steps: at least floor(carryMin / 2^L). - // - // If that lower bound is still >=1 at the top, impossible. - int stepsLeft = highColumn - currentColumn + 1; - if (stepsLeft <= 0) return true; - - long minCarry = carryIn.Min; - if (minCarry <= 0) return true; - - // floor(minCarry / 2^stepsLeft) - if (stepsLeft >= 63) return false; // 2^63 exceeds long shifts; if minCarry>0 it will go to 0, so be conservative - long minPossibleAtTop = minCarry >> stepsLeft; - return minPossibleAtTop == 0; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static ulong[] CreateBitMask64() - { - ulong[] masks = new ulong[64]; - ulong value = 1UL; - for (int i = 0; i < 64; i++) - { - masks[i] = value; - value <<= 1; - } - return masks; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static byte[] CreateReverseByteLut() - { - byte[] lut = new byte[256]; - for (int i = 0; i < lut.Length; i++) - { - int v = i; - int r = 0; - for (int b = 0; b < 8; b++) - { - r = (r << 1) | (v & 1); - v >>= 1; - } - - lut[i] = (byte)r; - } - - return lut; - } - -[MethodImpl(MethodImplOptions.AggressiveInlining)] -private static bool IntervalHasParity(long lo, long hi, int parity) // parity: 0=even,1=odd -{ - if (lo > hi) return false; - return ((lo & 1L) == parity) || (lo + 1 <= hi); -} - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static ulong ReverseBits64(ulong value) - { - return ((ulong)ReverseByteLut[(byte)value] << 56) | - ((ulong)ReverseByteLut[(byte)(value >> 8)] << 48) | - ((ulong)ReverseByteLut[(byte)(value >> 16)] << 40) | - ((ulong)ReverseByteLut[(byte)(value >> 24)] << 32) | - ((ulong)ReverseByteLut[(byte)(value >> 32)] << 24) | - ((ulong)ReverseByteLut[(byte)(value >> 40)] << 16) | - ((ulong)ReverseByteLut[(byte)(value >> 48)] << 8) | - ReverseByteLut[(byte)(value >> 56)]; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void ReverseBits1024(in ReadOnlySpan prefix, Span reversed) - { - reversed[0] = ReverseBits64(prefix[15]); - reversed[1] = ReverseBits64(prefix[14]); - reversed[2] = ReverseBits64(prefix[13]); - reversed[3] = ReverseBits64(prefix[12]); - reversed[4] = ReverseBits64(prefix[11]); - reversed[5] = ReverseBits64(prefix[10]); - reversed[6] = ReverseBits64(prefix[9]); - reversed[7] = ReverseBits64(prefix[8]); - reversed[8] = ReverseBits64(prefix[7]); - reversed[9] = ReverseBits64(prefix[6]); - reversed[10] = ReverseBits64(prefix[5]); - reversed[11] = ReverseBits64(prefix[4]); - reversed[12] = ReverseBits64(prefix[3]); - reversed[13] = ReverseBits64(prefix[2]); - reversed[14] = ReverseBits64(prefix[1]); - reversed[15] = ReverseBits64(prefix[0]); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void GetReversePrefix1024(PrivateWorkSet workSet, in ReadOnlySpan prefix, Span reversed) - { - ulong p0 = prefix[0]; - ulong p1 = prefix[1]; - ulong[] keys0 = workSet.QPrefixReverseKeys0; - ulong[] keys1 = workSet.QPrefixReverseKeys1; - ulong[] values0 = workSet.QPrefixReverseValues0; - ulong[] values1 = workSet.QPrefixReverseValues1; - ulong[] values2 = workSet.QPrefixReverseValues2; - ulong[] values3 = workSet.QPrefixReverseValues3; - ulong[] values4 = workSet.QPrefixReverseValues4; - ulong[] values5 = workSet.QPrefixReverseValues5; - ulong[] values6 = workSet.QPrefixReverseValues6; - ulong[] values7 = workSet.QPrefixReverseValues7; - ulong[] values8 = workSet.QPrefixReverseValues8; - ulong[] values9 = workSet.QPrefixReverseValues9; - ulong[] values10 = workSet.QPrefixReverseValues10; - ulong[] values11 = workSet.QPrefixReverseValues11; - ulong[] values12 = workSet.QPrefixReverseValues12; - ulong[] values13 = workSet.QPrefixReverseValues13; - ulong[] values14 = workSet.QPrefixReverseValues14; - ulong[] values15 = workSet.QPrefixReverseValues15; - bool[] valid = workSet.QPrefixReverseValid; - int slot = (int)p0 & QPrefixReverseCacheMask; - if (valid[slot] && keys0[slot] == p0 && keys1[slot] == p1) - { - reversed[0] = values0[slot]; - reversed[1] = values1[slot]; - reversed[2] = values2[slot]; - reversed[3] = values3[slot]; - reversed[4] = values4[slot]; - reversed[5] = values5[slot]; - reversed[6] = values6[slot]; - reversed[7] = values7[slot]; - reversed[8] = values8[slot]; - reversed[9] = values9[slot]; - reversed[10] = values10[slot]; - reversed[11] = values11[slot]; - reversed[12] = values12[slot]; - reversed[13] = values13[slot]; - reversed[14] = values14[slot]; - reversed[15] = values15[slot]; - return; - } - - ReverseBits1024(prefix, reversed); - keys0[slot] = p0; - keys1[slot] = p1; - values0[slot] = reversed[0]; - values1[slot] = reversed[1]; - values2[slot] = reversed[2]; - values3[slot] = reversed[3]; - values4[slot] = reversed[4]; - values5[slot] = reversed[5]; - values6[slot] = reversed[6]; - values7[slot] = reversed[7]; - values8[slot] = reversed[8]; - values9[slot] = reversed[9]; - values10[slot] = reversed[10]; - values11[slot] = reversed[11]; - values12[slot] = reversed[12]; - values13[slot] = reversed[13]; - values14[slot] = reversed[14]; - values15[slot] = reversed[15]; - valid[slot] = true; - } - - #if DETAILED_LOG - [ThreadStatic] private static long _statStableAdvanceCalls; - [ThreadStatic] private static long _statStableAdvanceCols; - [ThreadStatic] private static long _statStableAdvanceColsBatched; - [ThreadStatic] private static long _statScalarCols; + private const ulong DebugTargetP = 138000001UL; + private static readonly BigInteger DebugTargetK = new(3); + private static readonly ulong DebugTargetQ = checked((ulong)((DebugTargetK * DebugTargetP) << 1)); + // private const ulong DebugTargetQ = 1209708008767UL; - [ThreadStatic] private static long _statDeltaRequests; - [ThreadStatic] private static long _statDeltaHits; - [ThreadStatic] private static long _statDeltaBuilds; + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool IsTargetCase(ulong p, System.Numerics.BigInteger k) => p == DebugTargetP && k == DebugTargetK; - [ThreadStatic] private static long _statStableAdvanceBigShift; // how many times columnCount>=64 in TryAdvanceStableUnknown - [ThreadStatic] private static long _statBatchEntry; - [ThreadStatic] private static long _statBatchCols; - [ThreadStatic] private static long _statCleanChecks; - [ThreadStatic] private static long _statCleanFalse; - [ThreadStatic] private static int _statFirstDirtyColumn; - [ThreadStatic] private static int _statFirstDirtyWord; - [ThreadStatic] private static ulong _statFirstDirtyQ; - [ThreadStatic] private static ulong _statFirstDirtyKnown; - - public readonly struct TopDownPruneFailure(long column, long carryMin, long carryMax, long unknown) - { - public readonly long Column = column; - public readonly long CarryMin = carryMin; - public readonly long CarryMax = carryMax; - public readonly long Unknown = unknown; - } - - private readonly struct TopDownCacheValue(bool success, TopDownPruneFailure? failure) - { - public readonly bool Success = success; - public readonly TopDownPruneFailure? Failure = failure; - } - - [ThreadStatic] - private static Dictionary? _topDownCache; - - [ThreadStatic] - private static TopDownPruneFailure? _lastTopDownFailure; - internal static TopDownPruneFailure? LastTopDownFailure => _lastTopDownFailure; - - - private static void PrintStats() - { - Console.WriteLine( - $"[STATS] stableCalls={_statStableAdvanceCalls} stableCols={_statStableAdvanceColsBatched} " + - $"scalarCols={_statScalarCols} bigShift={_statStableAdvanceBigShift} " + - $"deltaReq={_statDeltaRequests} deltaHits={_statDeltaHits} deltaBuilds={_statDeltaBuilds}"); - Console.WriteLine( - $"[CLEAN] checks={_statCleanChecks} false={_statCleanFalse} " + - $"firstDirtyCol={_statFirstDirtyColumn} word={_statFirstDirtyWord} " + - $"qWord=0x{_statFirstDirtyQ:X16} knownWord=0x{_statFirstDirtyKnown:X16}"); - } -#else - [ThreadStatic] - private static Dictionary? _topDownCache; -#endif - [ThreadStatic] - private static long _dynamicModChecks; - [ThreadStatic] - private static long _dynamicModFailures; - [ThreadStatic] - private static Dictionary? _qModCache; - [ThreadStatic] - private static List? _topDownCacheOrder; - [ThreadStatic] - private static Dictionary? _prefixRunCache; - [ThreadStatic] - private static List? _prefixRunCacheOrder; - [ThreadStatic] - private static Dictionary? _pow2DiffModCache; - - [ThreadStatic] - private static PrivateWorkSet _privateWorkSet; - - private readonly struct QModCacheKey(long hash, int mod) - { - public readonly long Hash = hash; - public readonly int Mod = mod; - - public bool Equals(QModCacheKey other) => Hash == other.Hash && Mod == other.Mod; - public override bool Equals(object? obj) => obj is QModCacheKey other && Equals(other); - public override int GetHashCode() => HashCode.Combine(Hash, Mod); - } - - private readonly struct TopDownCacheKey(long hash, int length, long maxAllowedA, long pLong) - { - public readonly long Hash = hash; - public readonly int Length = length; - public readonly long MaxAllowedA = maxAllowedA; - public readonly long PLong = pLong; - - public bool Equals(TopDownCacheKey other) => Hash == other.Hash && Length == other.Length && MaxAllowedA == other.MaxAllowedA && PLong == other.PLong; - public override bool Equals(object? obj) => obj is TopDownCacheKey other && Equals(other); - public override int GetHashCode() => HashCode.Combine(Hash, Length, MaxAllowedA, PLong); - } - - private readonly struct PrefixRunCacheEntry( - int prefixCount, - int runCount, - int lastOffset, - int lastRunStart, - int lastRunLength, - int[] runStarts, - int[] runLengths) - { - public readonly int PrefixCount = prefixCount; - public readonly int RunCount = runCount; - public readonly int LastOffset = lastOffset; - public readonly int LastRunStart = lastRunStart; - public readonly int LastRunLength = lastRunLength; - public readonly int[] RunStarts = runStarts; - public readonly int[] RunLengths = runLengths; - } - -[MethodImpl(MethodImplOptions.AggressiveInlining)] -private static byte AllowedCarryInMask4FromCarryOut(byte carryOutMask4, byte onesMask4) -{ - byte m = 0; - for (int co = 0; co < 4; co++) + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void Dbg(ulong p, System.Numerics.BigInteger k, string msg) { - if (((carryOutMask4 >> co) & 1) == 0) continue; + if (IsTargetCase(p, k)) + Console.WriteLine(msg); + } +#endif +#if WITH_PRUNE_STATS + private static volatile int _pruneStatsConsoleCounter; + private static ulong _prunedWithGetAKnownStateRowAware; + private static ulong _prunedWithTryRunHighBitAndBorrowPrefiltersCombined; + private static ulong _prunedWithTargetJ; + private static ulong _prunedWithInterMinInterMax; + private static ulong _prunedWithTryProcessBottomUpBlockRowAware; + private static ulong _prunedWithTryAdvanceStableUnknown; + private static ulong _prunedWithBestCaseCarryOutOneStep; + private static ulong _prunedWithCouldStillReachTopCarryZero_UpperBound; + private static ulong _prunedWithTryFindSingleUnknownInQ_Prefix; + private static ulong _prunedWithTryPropagateCarry1; + private static ulong _prunedWithTryPropagateCarry2; + private static ulong _prunedWithTopCarry; + private static ulong _prunedWithPowmod2FinalShift; + private static ulong _prunedWithTruncatedLength1; + private static ulong _prunedWithTruncatedLength2; + private static ulong _prunedWithTryHighBitCarryRangeToColumnJ; + private static ulong _prunedWithCarryLowNonZeroFinal; + private static ulong _prunedWithEvenQAfterBuild; + private static ulong _prunedWithPowmod2FinalResidue; + private static ulong _prunedWithPowmod2Direct; + private static ulong _prunedWithPowmod2Tracked; + private static ulong _prunedWithPowmod2TrackedOptimized; + private static ulong _prunedWithPowmod2ZeroBeforeLastBlock; + private static ulong _prunedWithTryDynamicModularRangePrune; + private static ulong _prunedWithTopPrefixRangeConflict; + private static ulong _prunedWithQTimesAInterval; + private static ulong _prunedWithTopStateConflict; + private static ulong _prunedWithTopBothZeroConflict; + private static ulong _prunedWithCarryParityPrecheck; + private static ulong _prunedWithKnownBitsModResidue; + private static ulong _prunedWithCarryDropHeuristic; + private static ulong _prunedWithCarryDominance67; + private static ulong _prunedWithCarryDominance8910; + private static ulong _prunedWithCarryDominance15161718; + private static ulong _prunedWithCarryDominanceReached10AndStayedAbove5; + private static ulong _prunedWithCarryDominance1011121314; +#endif - int r = ((co << 1) + 1) & 3; // (2*carryOut+1) mod 4 - for (int o = 0; o < 4; o++) + + private const int PingPongBlockColumns = 4096; + private const int TailCarryBatchColumns = 16384; + private const int TailCarryBatchRepeats = 1; + private const int TopDownBorrowColumns = 4096; + private const int TopDownBorrowMinUnknown = 12; + private const int PrefixRunCacheOffsets = 256; + private const int PrefixRunCacheCapacity = 256; + private const int ModLocalPrefilterMaxABits = 20; + private const int TopDownCacheCapacity = 16; + private const int HighBitCarryPrefilterColumns = 16; + private const int MiniPingPongPrefilterColumns = 60; + private const int DynamicModPeriodicColumns = 1024; + private const int DynamicModPeriodicMask = DynamicModPeriodicColumns - 1; + private const int TopPrefixProbeBits = 24; + private const int ForcedALowBits = PerfectNumberConstants.BitContradictionForcedALowBits; + private const int QPrefixReverseCacheSize = 1024; + private const int QPrefixReverseCacheMask = QPrefixReverseCacheSize - 1; + + private static readonly int[] ModLocalPrefilterModuli = { 65537, 65521 }; + private static readonly int[] KnownBitsModResidueModuli = { 3, 5, 7, 11, 13, 17, 19, 23, 29, 31 }; + private const int CarryDropHeuristicBlockBits = 64; + private const int Powmod2AdaptiveTargetBlocks = 512; + private const int Powmod2AdaptiveMinRatio = 16; + private const int CarryDropHeuristicMaxBits = 1024; + private const bool EnableCarryDropHeuristic = true; + private static readonly ulong[] BitMask64 = CreateBitMask64(); + private static readonly byte[] ReverseByteLut = CreateReverseByteLut(); + +#if WITH_PRUNE_STATS + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void IncrementPruneCounter(ref ulong counter) + { + Atomic.Add(ref counter, 1UL); + _pruneStatsConsoleCounter++; + if (_pruneStatsConsoleCounter < PerfectNumberConstants.ConsoleInterval) { - if (((onesMask4 >> o) & 1) == 0) continue; + return; + } - int ci = (r - o) & 3; - // parzystość: carryIn + ones musi być nieparzyste - if (((ci + o) & 1) == 0) continue; + PrintPruneStats(); + _pruneStatsConsoleCounter = 0; + } - m |= (byte)(1 << ci); + private static void PrintPruneStats() + { + Console.WriteLine("Prune stats:"); + Console.WriteLine( + $"TryPropagateCarry1={_prunedWithTryPropagateCarry1}, " + + $"Powmod2ZeroBeforeLastBlock={_prunedWithPowmod2ZeroBeforeLastBlock}, " + + $"Powmod2Tracked={_prunedWithPowmod2Tracked}, " + + $"Powmod2TrackedOptimized={_prunedWithPowmod2TrackedOptimized}, " + + $"CarryDropHeuristic={_prunedWithCarryDropHeuristic}, " + + $"CarryDominance67={_prunedWithCarryDominance67}, " + + $"CarryDominance8910AndMore={_prunedWithCarryDominance8910}, " + + $"CarryDominance15161718={_prunedWithCarryDominance15161718}, " + + $"CarryDominanceReached10AndStayedAbove5={_prunedWithCarryDominanceReached10AndStayedAbove5}, " + + $"CarryDominance1011121314={_prunedWithCarryDominance1011121314}" + ); + } +#endif + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void ValidateHeuristicPruneAgainstPowmod2OrThrow(BigInteger q, int p, string filterName) + { + if (BigInteger.ModPow(BigIntegerNumbers.Two, p, q) == BigInteger.One) + { + throw new InvalidOperationException($"Heuristic prune '{filterName}' rejected a valid divisor for p={p}, q={q}."); } } - return m; -} - -[MethodImpl(MethodImplOptions.AggressiveInlining)] -private static byte NextCarryMask4(byte carryInMask4, byte onesMask4, int requiredResultBit) -{ - int b = requiredResultBit & 1; - byte outMask = 0; - - for (int ci = 0; ci < 4; ci++) + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static long BestCaseCarryOutOneStep(long carryIn, int forced, int possible, int requiredBit /*1*/) { - if (((carryInMask4 >> ci) & 1) == 0) continue; + // Choose sum in [forced..possible] s.t. (carryIn + sum) % 2 == requiredBit, + // minimize carryOut = (carryIn + sum - requiredBit) / 2. - for (int o = 0; o < 4; o++) + int needSumParity = (requiredBit ^ ((int)carryIn & 1)) & 1; + + int sum = forced; + if ((sum & 1) != needSumParity) + sum++; + + if (sum > possible) + return -1; // parity infeasible in this column + + return (carryIn + sum - requiredBit) >> 1; + } + + // --- ADD near other helpers in BitContradictionSolverWithAMultiplier.cs --- + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool CouldStillReachTopCarryZero_UpperBound( + CarryRange carryIn, + int currentColumn, + int highColumn, + int maxPossibleOnesPerColumn) // this is "possible" = forced+remaining for *this* column; + { + // Quick conservative check: + // If even the *maximum* per-column ones cannot prevent carry from staying >=1 by the time we hit highColumn, + // we can prune. We use a crude but safe bound: + // + // carry_{t+1} >= floor(carry_t / 2) + // and carry_{t+1} <= floor((carry_t + maxPossibleOnesPerColumn) / 2) + // + // For a SAFE prune we need a LOWER bound on the best case (smallest achievable carry). + // The smallest carry you can get after one step is at least floor(carryMin / 2). + // After L steps: at least floor(carryMin / 2^L). + // + // If that lower bound is still >=1 at the top, impossible. + int stepsLeft = highColumn - currentColumn + 1; + if (stepsLeft <= 0) return true; + + long minCarry = carryIn.Min; + if (minCarry <= 0) return true; + + // floor(minCarry / 2^stepsLeft) + if (stepsLeft >= 63) return false; // 2^63 exceeds long shifts; if minCarry>0 it will go to 0, so be conservative + long minPossibleAtTop = minCarry >> stepsLeft; + return minPossibleAtTop == 0; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static ulong[] CreateBitMask64() + { + ulong[] masks = new ulong[64]; + ulong value = 1UL; + for (int i = 0; i < 64; i++) { - if (((onesMask4 >> o) & 1) == 0) continue; + masks[i] = value; + value <<= 1; + } + return masks; + } - // warunek bitu: (carryIn + ones) ≡ b (mod 2) - if (((ci + o) & 1) != b) continue; + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static byte[] CreateReverseByteLut() + { + byte[] lut = new byte[256]; + for (int i = 0; i < lut.Length; i++) + { + int v = i; + int r = 0; + for (int b = 0; b < 8; b++) + { + r = (r << 1) | (v & 1); + v >>= 1; + } - // s = carryIn + ones - b jest parzyste; bazujemy na resztach mod 4, - // ale UWAGA: (carryIn + 4) zmienia (s/2) o +2 => trzeba domknąć o +2. - int s = (ci + o - b) & 3; // s mod 4, zawsze 0 albo 2 - int baseCo = ((s >> 1) & 3); // 0 albo 1 - outMask |= (byte)(1 << baseCo); - outMask |= (byte)(1 << (baseCo ^ 2)); // +2 (mod4) dla bezpieczeństwa + lut[i] = (byte)r; + } + + return lut; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool IntervalHasParity(long lo, long hi, int parity) // parity: 0=even,1=odd + { + if (lo > hi) return false; + return ((lo & 1L) == parity) || (lo + 1 <= hi); + } +#if false + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static ulong ReverseBits64(ulong value) + { + return ((ulong)ReverseByteLut[(byte)value] << 56) | + ((ulong)ReverseByteLut[(byte)(value >> 8)] << 48) | + ((ulong)ReverseByteLut[(byte)(value >> 16)] << 40) | + ((ulong)ReverseByteLut[(byte)(value >> 24)] << 32) | + ((ulong)ReverseByteLut[(byte)(value >> 32)] << 24) | + ((ulong)ReverseByteLut[(byte)(value >> 40)] << 16) | + ((ulong)ReverseByteLut[(byte)(value >> 48)] << 8) | + ReverseByteLut[(byte)(value >> 56)]; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void ReverseBits1024(in ReadOnlySpan prefix, Span reversed) + { + reversed[0] = ReverseBits64(prefix[15]); + reversed[1] = ReverseBits64(prefix[14]); + reversed[2] = ReverseBits64(prefix[13]); + reversed[3] = ReverseBits64(prefix[12]); + reversed[4] = ReverseBits64(prefix[11]); + reversed[5] = ReverseBits64(prefix[10]); + reversed[6] = ReverseBits64(prefix[9]); + reversed[7] = ReverseBits64(prefix[8]); + reversed[8] = ReverseBits64(prefix[7]); + reversed[9] = ReverseBits64(prefix[6]); + reversed[10] = ReverseBits64(prefix[5]); + reversed[11] = ReverseBits64(prefix[4]); + reversed[12] = ReverseBits64(prefix[3]); + reversed[13] = ReverseBits64(prefix[2]); + reversed[14] = ReverseBits64(prefix[1]); + reversed[15] = ReverseBits64(prefix[0]); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void GetReversePrefix1024(PrivateWorkSet workSet, in ReadOnlySpan prefix, Span reversed) + { + ulong p0 = prefix[0]; + ulong p1 = prefix[1]; + ulong[] keys0 = workSet.QPrefixReverseKeys0; + ulong[] keys1 = workSet.QPrefixReverseKeys1; + ulong[] values0 = workSet.QPrefixReverseValues0; + ulong[] values1 = workSet.QPrefixReverseValues1; + ulong[] values2 = workSet.QPrefixReverseValues2; + ulong[] values3 = workSet.QPrefixReverseValues3; + ulong[] values4 = workSet.QPrefixReverseValues4; + ulong[] values5 = workSet.QPrefixReverseValues5; + ulong[] values6 = workSet.QPrefixReverseValues6; + ulong[] values7 = workSet.QPrefixReverseValues7; + ulong[] values8 = workSet.QPrefixReverseValues8; + ulong[] values9 = workSet.QPrefixReverseValues9; + ulong[] values10 = workSet.QPrefixReverseValues10; + ulong[] values11 = workSet.QPrefixReverseValues11; + ulong[] values12 = workSet.QPrefixReverseValues12; + ulong[] values13 = workSet.QPrefixReverseValues13; + ulong[] values14 = workSet.QPrefixReverseValues14; + ulong[] values15 = workSet.QPrefixReverseValues15; + bool[] valid = workSet.QPrefixReverseValid; + int slot = (int)p0 & QPrefixReverseCacheMask; + if (valid[slot] && keys0[slot] == p0 && keys1[slot] == p1) + { + reversed[0] = values0[slot]; + reversed[1] = values1[slot]; + reversed[2] = values2[slot]; + reversed[3] = values3[slot]; + reversed[4] = values4[slot]; + reversed[5] = values5[slot]; + reversed[6] = values6[slot]; + reversed[7] = values7[slot]; + reversed[8] = values8[slot]; + reversed[9] = values9[slot]; + reversed[10] = values10[slot]; + reversed[11] = values11[slot]; + reversed[12] = values12[slot]; + reversed[13] = values13[slot]; + reversed[14] = values14[slot]; + reversed[15] = values15[slot]; + return; + } + + ReverseBits1024(prefix, reversed); + keys0[slot] = p0; + keys1[slot] = p1; + values0[slot] = reversed[0]; + values1[slot] = reversed[1]; + values2[slot] = reversed[2]; + values3[slot] = reversed[3]; + values4[slot] = reversed[4]; + values5[slot] = reversed[5]; + values6[slot] = reversed[6]; + values7[slot] = reversed[7]; + values8[slot] = reversed[8]; + values9[slot] = reversed[9]; + values10[slot] = reversed[10]; + values11[slot] = reversed[11]; + values12[slot] = reversed[12]; + values13[slot] = reversed[13]; + values14[slot] = reversed[14]; + values15[slot] = reversed[15]; + valid[slot] = true; + } +#endif + +#if DETAILED_LOG + [ThreadStatic] private static long _statStableAdvanceCalls; + [ThreadStatic] private static long _statStableAdvanceCols; + [ThreadStatic] private static long _statStableAdvanceColsBatched; + [ThreadStatic] private static long _statScalarCols; + + [ThreadStatic] private static long _statDeltaRequests; + [ThreadStatic] private static long _statDeltaHits; + [ThreadStatic] private static long _statDeltaBuilds; + + [ThreadStatic] private static long _statStableAdvanceBigShift; // how many times columnCount>=64 in TryAdvanceStableUnknown + [ThreadStatic] private static long _statBatchEntry; + [ThreadStatic] private static long _statBatchCols; + [ThreadStatic] private static long _statCleanChecks; + [ThreadStatic] private static long _statCleanFalse; + [ThreadStatic] private static int _statFirstDirtyColumn; + [ThreadStatic] private static int _statFirstDirtyWord; + [ThreadStatic] private static ulong _statFirstDirtyQ; + [ThreadStatic] private static ulong _statFirstDirtyKnown; + + public readonly struct TopDownPruneFailure(long column, long carryMin, long carryMax, long unknown) + { + public readonly long Column = column; + public readonly long CarryMin = carryMin; + public readonly long CarryMax = carryMax; + public readonly long Unknown = unknown; + } + + private readonly struct TopDownCacheValue(bool success, TopDownPruneFailure? failure) + { + public readonly bool Success = success; + public readonly TopDownPruneFailure? Failure = failure; + } + + [ThreadStatic] + private static Dictionary? _topDownCache; + + [ThreadStatic] + private static TopDownPruneFailure? _lastTopDownFailure; + internal static TopDownPruneFailure? LastTopDownFailure => _lastTopDownFailure; + + + private static void PrintStats() + { + Console.WriteLine( + $"[STATS] stableCalls={_statStableAdvanceCalls} stableCols={_statStableAdvanceColsBatched} " + + $"scalarCols={_statScalarCols} bigShift={_statStableAdvanceBigShift} " + + $"deltaReq={_statDeltaRequests} deltaHits={_statDeltaHits} deltaBuilds={_statDeltaBuilds}"); + Console.WriteLine( + $"[CLEAN] checks={_statCleanChecks} false={_statCleanFalse} " + + $"firstDirtyCol={_statFirstDirtyColumn} word={_statFirstDirtyWord} " + + $"qWord=0x{_statFirstDirtyQ:X16} knownWord=0x{_statFirstDirtyKnown:X16}"); + } +#else + [ThreadStatic] + private static Dictionary? _topDownCache; +#endif + [ThreadStatic] + private static long _dynamicModChecks; + [ThreadStatic] + private static long _dynamicModFailures; + [ThreadStatic] + private static Dictionary? _qModCache; + [ThreadStatic] + private static List? _topDownCacheOrder; + [ThreadStatic] + private static Dictionary? _prefixRunCache; + [ThreadStatic] + private static List? _prefixRunCacheOrder; + [ThreadStatic] + private static Dictionary? _pow2DiffModCache; + + [ThreadStatic] + private static PrivateWorkSet _privateWorkSet; + + private readonly struct QModCacheKey(long hash, int mod) + { + public readonly long Hash = hash; + public readonly int Mod = mod; + + public bool Equals(QModCacheKey other) => Hash == other.Hash && Mod == other.Mod; + public override bool Equals(object? obj) => obj is QModCacheKey other && Equals(other); + public override int GetHashCode() => HashCode.Combine(Hash, Mod); + } + + private readonly struct TopDownCacheKey(long hash, int length, long maxAllowedA, long pLong) + { + public readonly long Hash = hash; + public readonly int Length = length; + public readonly long MaxAllowedA = maxAllowedA; + public readonly long PLong = pLong; + + public bool Equals(TopDownCacheKey other) => Hash == other.Hash && Length == other.Length && MaxAllowedA == other.MaxAllowedA && PLong == other.PLong; + public override bool Equals(object? obj) => obj is TopDownCacheKey other && Equals(other); + public override int GetHashCode() => HashCode.Combine(Hash, Length, MaxAllowedA, PLong); + } + + private readonly struct PrefixRunCacheEntry( + int prefixCount, + int runCount, + int lastOffset, + int lastRunStart, + int lastRunLength, + int[] runStarts, + int[] runLengths) + { + public readonly int PrefixCount = prefixCount; + public readonly int RunCount = runCount; + public readonly int LastOffset = lastOffset; + public readonly int LastRunStart = lastRunStart; + public readonly int LastRunLength = lastRunLength; + public readonly int[] RunStarts = runStarts; + public readonly int[] RunLengths = runLengths; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static byte AllowedCarryInMask4FromCarryOut(byte carryOutMask4, byte onesMask4) + { + byte m = 0; + for (int co = 0; co < 4; co++) + { + if (((carryOutMask4 >> co) & 1) == 0) continue; + + int r = ((co << 1) + 1) & 3; // (2*carryOut+1) mod 4 + for (int o = 0; o < 4; o++) + { + if (((onesMask4 >> o) & 1) == 0) continue; + + int ci = (r - o) & 3; + // parzystość: carryIn + ones musi być nieparzyste + if (((ci + o) & 1) == 0) continue; + + m |= (byte)(1 << ci); + } + } + + return m; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static byte NextCarryMask4(byte carryInMask4, byte onesMask4, int requiredResultBit) + { + int b = requiredResultBit & 1; + byte outMask = 0; + + for (int ci = 0; ci < 4; ci++) + { + if (((carryInMask4 >> ci) & 1) == 0) continue; + + for (int o = 0; o < 4; o++) + { + if (((onesMask4 >> o) & 1) == 0) continue; + + // warunek bitu: (carryIn + ones) ≡ b (mod 2) + if (((ci + o) & 1) != b) continue; + + // s = carryIn + ones - b jest parzyste; bazujemy na resztach mod 4, + // ale UWAGA: (carryIn + 4) zmienia (s/2) o +2 => trzeba domknąć o +2. + int s = (ci + o - b) & 3; // s mod 4, zawsze 0 albo 2 + int baseCo = ((s >> 1) & 3); // 0 albo 1 + outMask |= (byte)(1 << baseCo); + outMask |= (byte)(1 << (baseCo ^ 2)); // +2 (mod4) dla bezpieczeństwa + } + } + + return outMask; + } + + private static Vector SimdPopCount(Vector value) + { + // A classic parallel popcount algorithm (SWAR) + var m1 = new Vector(0x5555555555555555); // 0101... + var m2 = new Vector(0x3333333333333333); // 0011... + var m4 = new Vector(0x0F0F0F0F0F0F0F0F); // 00001111... + var h01 = new Vector(0x0101010101010101); + + value -= (value >> 1) & m1; + value = (value & m2) + ((value >> 2) & m2); + value = (value + (value >> 4)) & m4; + return (value * h01) >> 56; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void ComputeForcedRemainingAndClean( + in ulong[] qMask, + in ulong[] oneWin, + in ulong[] zeroWin, + int wordCount, + out int forced, + out int remaining, + out bool clean) + { + // Use scalar implementation for small inputs or when SIMD is not available. + int i; + if (!Vector.IsHardwareAccelerated || wordCount < Vector.Count) + { + forced = 0; + remaining = 0; + clean = true; + for (i = 0; i < wordCount; i++) + { + ulong q = qMask[i]; + ulong one = oneWin[i]; + ulong known = one | zeroWin[i]; + + one &= q; + ulong unknownBits = q & ~known; + + forced += PopCount(one); + remaining += PopCount(unknownBits); + + if ((q & known) != 0) + { + clean = false; + } + } + return; + } + + // Vectorized implementation + var vForced = Vector.Zero; + var vRemaining = Vector.Zero; + var vContradictions = Vector.Zero; + int limit = wordCount - (wordCount % Vector.Count); + + for (i = 0; i < limit; i += Vector.Count) + { + var vq = new Vector(qMask, i); + var vOne = new Vector(oneWin, i); + var vZero = new Vector(zeroWin, i); + + var vKnown = vOne | vZero; + var vForcedBits = vOne & vq; + var vUnknownBits = vq & ~vKnown; + + vForced += SimdPopCount(vForcedBits); + vRemaining += SimdPopCount(vUnknownBits); + + vContradictions |= (vq & vKnown); + } + + forced = (int)Vector.Sum(vForced); + remaining = (int)Vector.Sum(vRemaining); + clean = (vContradictions == Vector.Zero); + + // Process the remainder + for (; i < wordCount; i++) + { + ulong q = qMask[i]; + ulong one = oneWin[i]; + ulong known = one | zeroWin[i]; + + one &= q; + ulong unknownBits = q & ~known; + + forced += PopCount(one); + remaining += PopCount(unknownBits); + + if (clean && (q & known) != 0) + { + clean = false; + } } } - return outMask; -} + private static readonly byte[] _popCount16Cache = CreatePopCount16Cache(); - private static Vector SimdPopCount(Vector value) - { - // A classic parallel popcount algorithm (SWAR) - var m1 = new Vector(0x5555555555555555); // 0101... - var m2 = new Vector(0x3333333333333333); // 0011... - var m4 = new Vector(0x0F0F0F0F0F0F0F0F); // 00001111... - var h01 = new Vector(0x0101010101010101); - - value -= (value >> 1) & m1; - value = (value & m2) + ((value >> 2) & m2); - value = (value + (value >> 4)) & m4; - return (value * h01) >> 56; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void ComputeForcedRemainingAndClean( - in ulong[] qMask, - in ulong[] oneWin, - in ulong[] zeroWin, - int wordCount, - out int forced, - out int remaining, - out bool clean) - { - // Use scalar implementation for small inputs or when SIMD is not available. - int i; - if (!Vector.IsHardwareAccelerated || wordCount < Vector.Count) - { - forced = 0; - remaining = 0; - clean = true; - for (i = 0; i < wordCount; i++) - { - ulong q = qMask[i]; - ulong one = oneWin[i]; - ulong known = one | zeroWin[i]; - - one &= q; - ulong unknownBits = q & ~known; - - forced += PopCount(one); - remaining += PopCount(unknownBits); - - if ((q & known) != 0) - { - clean = false; - } - } - return; - } - - // Vectorized implementation - var vForced = Vector.Zero; - var vRemaining = Vector.Zero; - var vContradictions = Vector.Zero; - int limit = wordCount - (wordCount % Vector.Count); - - for (i = 0; i < limit; i += Vector.Count) - { - var vq = new Vector(qMask, i); - var vOne = new Vector(oneWin, i); - var vZero = new Vector(zeroWin, i); - - var vKnown = vOne | vZero; - var vForcedBits = vOne & vq; - var vUnknownBits = vq & ~vKnown; - - vForced += SimdPopCount(vForcedBits); - vRemaining += SimdPopCount(vUnknownBits); - - vContradictions |= (vq & vKnown); - } - - forced = (int)Vector.Sum(vForced); - remaining = (int)Vector.Sum(vRemaining); - clean = (vContradictions == Vector.Zero); - - // Process the remainder - for (; i < wordCount; i++) - { - ulong q = qMask[i]; - ulong one = oneWin[i]; - ulong known = one | zeroWin[i]; - - one &= q; - ulong unknownBits = q & ~known; - - forced += PopCount(one); - remaining += PopCount(unknownBits); - - if (clean && (q & known) != 0) - { - clean = false; - } - } - } - - private static readonly byte[] _popCount16Cache = CreatePopCount16Cache(); - - private static byte[] CreatePopCount16Cache() - { - const int CacheSize = 65536; - byte[] cache = new byte[CacheSize]; - for (int i = 0; i < CacheSize; i++) - { - cache[i] = (byte)BitOperations.PopCount((uint)i); - } - - return cache; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static int PopCount(ulong value) - { - byte[] cache = _popCount16Cache; - int result = cache[(ushort)value]; - value >>= 16; - result += cache[(ushort)value]; - value >>= 16; - result += cache[(ushort)value]; - value >>= 16; - result += cache[(ushort)value]; - return result; - } - - private static long ComputeQOffsetsHash(in ReadOnlySpan qOneOffsets) - { - const long fnvOffset = unchecked(1469598103934665603); - const long fnvPrime = 1099511628211; - long hash = fnvOffset; - int qOneOffsetsLength = qOneOffsets.Length; - for (int i = 0; i < qOneOffsetsLength; i++) - { - hash ^= qOneOffsets[i]; - hash *= fnvPrime; - } - - return hash; - } - - private static int GetQModCached(ReadOnlySpan qOneOffsets, long qHash, int mod) - { - Dictionary? cache = _qModCache; - if (cache is null) - { - cache = []; - _qModCache = cache; - - } - var key = new QModCacheKey(qHash, mod); - if (cache.TryGetValue(key, out int cached)) - { - return cached; - } - - int value = ComputeQMod(qOneOffsets, mod); - cache[key] = value; - return value; - } - - private static long ComputeQOffsetsPrefixHash(in ReadOnlySpan qOneOffsets, int count) - { - const long fnvOffset = unchecked(1469598103934665603); - const long fnvPrime = 1099511628211; - long hash = fnvOffset; - for (int i = 0; i < count; i++) - { - hash ^= qOneOffsets[i]; - hash *= fnvPrime; - } - - hash ^= count; - hash *= fnvPrime; - return hash; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static bool IsCleanInQ(in ulong[] qMask, in ulong[] oneWin, in ulong[] zeroWin, int wordCount) - { - for (int i = 0; i < wordCount; i++) - { - if ((qMask[i] & (oneWin[i] | zeroWin[i])) != 0) - return false; - } - - return true; - } - -[MethodImpl(MethodImplOptions.AggressiveInlining)] -private static byte MaskFromIntervalMod4(long lo, long hi) -{ - if (lo > hi) return 0; - // Jeżeli długość >= 4, to mamy wszystkie klasy reszt. - if (hi - lo >= 3) return 0b1111; - - byte m = 0; - for (long x = lo; x <= hi; x++) - m |= (byte)(1 << (int)(x & 3)); - return m; -} - -[MethodImpl(MethodImplOptions.AggressiveInlining)] -private static long AlignUpToAllowedMod4(long value, byte mask) -{ - // przesuwa do najbliższej wartości >=value której (value mod 4) jest w masce - for (int d = 0; d < 4; d++) + private static byte[] CreatePopCount16Cache() { - long v = value + d; - if (((mask >> (int)(v & 3)) & 1) != 0) return v; - } - return long.MaxValue; // brak -} + const int CacheSize = 65536; + byte[] cache = new byte[CacheSize]; + for (int i = 0; i < CacheSize; i++) + { + cache[i] = (byte)BitOperations.PopCount((uint)i); + } -[MethodImpl(MethodImplOptions.AggressiveInlining)] -private static long AlignDownToAllowedMod4(long value, byte mask) -{ - for (int d = 0; d < 4; d++) + return cache; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static int PopCount(ulong value) { - long v = value - d; - if (((mask >> (int)(v & 3)) & 1) != 0) return v; + byte[] cache = _popCount16Cache; + int result = cache[(ushort)value]; + value >>= 16; + result += cache[(ushort)value]; + value >>= 16; + result += cache[(ushort)value]; + value >>= 16; + result += cache[(ushort)value]; + return result; } - return long.MinValue; -} - private static bool TryGetPrefixRunCache(long key, out PrefixRunCacheEntry entry) - { - var cache = _prefixRunCache; - if (cache is null) - { - cache = []; - _prefixRunCache = cache; - } + private static long ComputeQOffsetsHash(in ReadOnlySpan qOneOffsets) + { + const long fnvOffset = unchecked(1469598103934665603); + const long fnvPrime = 1099511628211; + long hash = fnvOffset; + int qOneOffsetsLength = qOneOffsets.Length; + for (int i = 0; i < qOneOffsetsLength; i++) + { + hash ^= qOneOffsets[i]; + hash *= fnvPrime; + } - return cache.TryGetValue(key, out entry); - } + return hash; + } - private static void StorePrefixRunCache(long key, in PrefixRunCacheEntry entry) - { - _prefixRunCacheOrder ??= new List(PrefixRunCacheCapacity + 1); + private static int GetQModCached(ReadOnlySpan qOneOffsets, long qHash, int mod) + { + Dictionary? cache = _qModCache; + if (cache is null) + { + cache = []; + _qModCache = cache; - if (_prefixRunCache!.ContainsKey(key)) - { - _prefixRunCache[key] = entry; - return; - } + } + var key = new QModCacheKey(qHash, mod); + if (cache.TryGetValue(key, out int cached)) + { + return cached; + } - if (_prefixRunCacheOrder.Count >= PrefixRunCacheCapacity) - { - long evict = _prefixRunCacheOrder[0]; - _prefixRunCacheOrder.RemoveAt(0); - _prefixRunCache.Remove(evict); - } + int value = ComputeQMod(qOneOffsets, mod); + cache[key] = value; + return value; + } - _prefixRunCache[key] = entry; - _prefixRunCacheOrder.Add(key); - } + private static long ComputeQOffsetsPrefixHash(in ReadOnlySpan qOneOffsets, int count) + { + const long fnvOffset = unchecked(1469598103934665603); + const long fnvPrime = 1099511628211; + long hash = fnvOffset; + for (int i = 0; i < count; i++) + { + hash ^= qOneOffsets[i]; + hash *= fnvPrime; + } - private static PrefixRunCacheEntry BuildPrefixRunCache(in ReadOnlySpan qOneOffsets, int prefixCount) - { - // TODO: Remove per-call allocations - int[] starts = new int[prefixCount]; - int[] lengths = new int[prefixCount]; - int runCount = 0; - int prev = qOneOffsets[0]; - int currentStart = prev; - int currentLength = 1; + hash ^= count; + hash *= fnvPrime; + return hash; + } - for (int i = 1; i < prefixCount; i++) - { - int offset = qOneOffsets[i]; - if (offset == prev + 1) - { - currentLength++; - } - else - { - starts[runCount] = currentStart; - lengths[runCount] = currentLength; - runCount++; - currentStart = offset; - currentLength = 1; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool IsCleanInQ(in ulong[] qMask, in ulong[] oneWin, in ulong[] zeroWin, int wordCount) + { + for (int i = 0; i < wordCount; i++) + { + if ((qMask[i] & (oneWin[i] | zeroWin[i])) != 0) + return false; + } - prev = offset; - } + return true; + } - starts[runCount] = currentStart; - lengths[runCount] = currentLength; - runCount++; + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static byte MaskFromIntervalMod4(long lo, long hi) + { + if (lo > hi) return 0; + // Jeżeli długość >= 4, to mamy wszystkie klasy reszt. + if (hi - lo >= 3) return 0b1111; - int[] cachedStarts = new int[runCount]; - int[] cachedLengths = new int[runCount]; - Array.Copy(starts, cachedStarts, runCount); - Array.Copy(lengths, cachedLengths, runCount); + byte m = 0; + for (long x = lo; x <= hi; x++) + m |= (byte)(1 << (int)(x & 3)); + return m; + } - return new PrefixRunCacheEntry( - prefixCount, - runCount, - prev, - currentStart, - currentLength, - cachedStarts, - cachedLengths); - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static long AlignUpToAllowedMod4(long value, byte mask) + { + // przesuwa do najbliższej wartości >=value której (value mod 4) jest w masce + for (int d = 0; d < 4; d++) + { + long v = value + d; + if (((mask >> (int)(v & 3)) & 1) != 0) return v; + } + return long.MaxValue; // brak + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static long AlignDownToAllowedMod4(long value, byte mask) + { + for (int d = 0; d < 4; d++) + { + long v = value - d; + if (((mask >> (int)(v & 3)) & 1) != 0) return v; + } + return long.MinValue; + } + + private static bool TryGetPrefixRunCache(long key, out PrefixRunCacheEntry entry) + { + var cache = _prefixRunCache; + if (cache is null) + { + cache = []; + _prefixRunCache = cache; + } + + return cache.TryGetValue(key, out entry); + } + + private static void StorePrefixRunCache(long key, in PrefixRunCacheEntry entry) + { + _prefixRunCacheOrder ??= new List(PrefixRunCacheCapacity + 1); + + if (_prefixRunCache!.ContainsKey(key)) + { + _prefixRunCache[key] = entry; + return; + } + + if (_prefixRunCacheOrder.Count >= PrefixRunCacheCapacity) + { + long evict = _prefixRunCacheOrder[0]; + _prefixRunCacheOrder.RemoveAt(0); + _prefixRunCache.Remove(evict); + } + + _prefixRunCache[key] = entry; + _prefixRunCacheOrder.Add(key); + } + + private static PrefixRunCacheEntry BuildPrefixRunCache(in ReadOnlySpan qOneOffsets, int prefixCount) + { + // TODO: Remove per-call allocations + int[] starts = new int[prefixCount]; + int[] lengths = new int[prefixCount]; + int runCount = 0; + int prev = qOneOffsets[0]; + int currentStart = prev; + int currentLength = 1; + + for (int i = 1; i < prefixCount; i++) + { + int offset = qOneOffsets[i]; + if (offset == prev + 1) + { + currentLength++; + } + else + { + starts[runCount] = currentStart; + lengths[runCount] = currentLength; + runCount++; + currentStart = offset; + currentLength = 1; + } + + prev = offset; + } + + starts[runCount] = currentStart; + lengths[runCount] = currentLength; + runCount++; + + int[] cachedStarts = new int[runCount]; + int[] cachedLengths = new int[runCount]; + Array.Copy(starts, cachedStarts, runCount); + Array.Copy(lengths, cachedLengths, runCount); + + return new PrefixRunCacheEntry( + prefixCount, + runCount, + prev, + currentStart, + currentLength, + cachedStarts, + cachedLengths); + } #if DETAILED_LOG - private static bool TryGetTopDownCache(in TopDownCacheKey key, out TopDownCacheValue value) + private static bool TryGetTopDownCache(in TopDownCacheKey key, out TopDownCacheValue value) #else - private static bool TryGetTopDownCache(in TopDownCacheKey key, out bool value) + private static bool TryGetTopDownCache(in TopDownCacheKey key, out bool value) #endif - { - // TODO: Remove this check after Initialize - if (_topDownCache == null) - { - value = default; - return false; - } + { + // TODO: Remove this check after Initialize + if (_topDownCache == null) + { + value = default; + return false; + } - return _topDownCache.TryGetValue(key, out value); - } + return _topDownCache.TryGetValue(key, out value); + } #if DETAILED_LOG - private static void StoreTopDownCache(in TopDownCacheKey key, in TopDownCacheValue value) + private static void StoreTopDownCache(in TopDownCacheKey key, in TopDownCacheValue value) #else - private static void StoreTopDownCache(in TopDownCacheKey key, in bool value) + private static void StoreTopDownCache(in TopDownCacheKey key, in bool value) #endif - { - // TODO: Remove this check after Initialize - _topDownCache ??= []; - _topDownCacheOrder ??= new List(TopDownCacheCapacity + 1); + { + // TODO: Remove this check after Initialize + _topDownCache ??= []; + _topDownCacheOrder ??= new List(TopDownCacheCapacity + 1); - if (_topDownCache.ContainsKey(key)) - { - _topDownCache[key] = value; - return; - } + if (_topDownCache.ContainsKey(key)) + { + _topDownCache[key] = value; + return; + } - if (_topDownCacheOrder.Count >= TopDownCacheCapacity) - { - var evict = _topDownCacheOrder[0]; - _topDownCacheOrder.RemoveAt(0); - _topDownCache.Remove(evict); - } + if (_topDownCacheOrder.Count >= TopDownCacheCapacity) + { + var evict = _topDownCacheOrder[0]; + _topDownCacheOrder.RemoveAt(0); + _topDownCache.Remove(evict); + } - _topDownCache[key] = value; - _topDownCacheOrder.Add(key); - } + _topDownCache[key] = value; + _topDownCacheOrder.Add(key); + } - internal static ColumnBounds ComputeColumnBounds( - ReadOnlySpan multiplicand, - ReadOnlySpan multiplier, - int columnIndex) - { - int forced = 0; - int possible = 0; + internal static ColumnBounds ComputeColumnBounds( + ReadOnlySpan multiplicand, + ReadOnlySpan multiplier, + int columnIndex) + { + int forced = 0; + int possible = 0; - int multiplicandLength = multiplicand.Length; - int multiplierLength = multiplier.Length; - for (int i = 0; i <= columnIndex; i++) - { - bool a = i < multiplicandLength && multiplicand[i]; - bool q = columnIndex - i < multiplierLength && multiplier[columnIndex - i]; - if (!a && !q) - { - continue; - } + int multiplicandLength = multiplicand.Length; + int multiplierLength = multiplier.Length; + for (int i = 0; i <= columnIndex; i++) + { + bool a = i < multiplicandLength && multiplicand[i]; + bool q = columnIndex - i < multiplierLength && multiplier[columnIndex - i]; + if (!a && !q) + { + continue; + } - if (a && q) - { - forced++; - } + if (a && q) + { + forced++; + } - possible++; - } + possible++; + } - return new ColumnBounds(forced, possible); - } + return new ColumnBounds(forced, possible); + } -internal static bool TryPropagateCarry( - ref CarryRange currentCarry, - int forcedOnes, - int possibleOnes, - int requiredResultBit) -{ - // sum = carryIn + ones - long minSum = currentCarry.Min + forcedOnes; - long maxSum = currentCarry.Max + possibleOnes; + internal static bool TryPropagateCarry( + ref CarryRange currentCarry, + int forcedOnes, + int possibleOnes, + int requiredResultBit) + { + // sum = carryIn + ones + long minSum = currentCarry.Min + forcedOnes; + long maxSum = currentCarry.Max + possibleOnes; - int parity = requiredResultBit & 1; + int parity = requiredResultBit & 1; - // enforce sum parity: sum ≡ requiredResultBit (mod 2) - minSum = AlignUpToParity(minSum, parity); - maxSum = AlignDownToParity(maxSum, parity); + // enforce sum parity: sum ≡ requiredResultBit (mod 2) + minSum = AlignUpToParity(minSum, parity); + maxSum = AlignDownToParity(maxSum, parity); - if (minSum > maxSum) - return false; + if (minSum > maxSum) + return false; - // carryOut = (sum - requiredBit) / 2 - long nextMin = (minSum - requiredResultBit) >> 1; - long nextMax = (maxSum - requiredResultBit) >> 1; + // carryOut = (sum - requiredBit) / 2 + long nextMin = (minSum - requiredResultBit) >> 1; + long nextMax = (maxSum - requiredResultBit) >> 1; - // ones-range is [forcedOnes..possibleOnes], not [nextMin..nextMax] - byte onesMask4 = MaskFromIntervalMod4(forcedOnes, possibleOnes); + // // ones-range is [forcedOnes..possibleOnes], not [nextMin..nextMax] + // byte onesMask4 = MaskFromIntervalMod4(forcedOnes, possibleOnes); - // IMPORTANT: NextCarryMask4 must account for requiredResultBit, otherwise it may over-prune for b=0. - byte nextMask4 = NextCarryMask4(currentCarry.Mod4Mask, onesMask4, requiredResultBit); - if (nextMask4 == 0) - return false; + // // IMPORTANT: NextCarryMask4 must account for requiredResultBit, otherwise it may over-prune for b=0. + // byte nextMask4 = NextCarryMask4(currentCarry.Mod4Mask, onesMask4, requiredResultBit); + // if (nextMask4 == 0) + // return false; - // Optional safety: intersect with the interval’s own mod4 availability - byte intervalMask4 = MaskFromIntervalMod4(nextMin, nextMax); - nextMask4 &= intervalMask4; - if (nextMask4 == 0) - return false; + // // Optional safety: intersect with the interval’s own mod4 availability + // byte intervalMask4 = MaskFromIntervalMod4(nextMin, nextMax); + // nextMask4 &= intervalMask4; + // if (nextMask4 == 0) + // return false; - currentCarry = new CarryRange(nextMin, nextMax, nextMask4); - return true; -} + currentCarry = new CarryRange(nextMin, nextMax, byte.MaxValue); + return true; + } - /// - /// Mini ping-pong (Option B): compute a conservative allowed carry range after walking - /// top-down for a given number of columns starting at . - /// - /// Semantics: - /// - We treat "carryOut at column = startColumn+1" as the starting set (seed). - /// - Each step processes one column (carryOut -> carryIn) moving downward. - /// - After columns, the resulting set corresponds to carry-in - /// at column (startColumn - steps + 1). - /// - private static bool TryHighBitCarryRangeToColumnJ( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - int pLong, - int maxAllowedA, - int startColumn, // e.g. p-1, then J1-1, ... - int steps, // number of columns to process downward - long startCarryOutMin, // seed carryOut range - long startCarryOutMax, - out long allowedMin, - out long allowedMax) - { - allowedMin = 0; - allowedMax = long.MaxValue; - - if (steps <= 0) - { - // No processing: carry-in == seed (conservative) - allowedMin = startCarryOutMin < 0 ? 0 : startCarryOutMin; - allowedMax = startCarryOutMax < 0 ? 0 : startCarryOutMax; - if (allowedMax < allowedMin) (allowedMin, allowedMax) = (0, long.MaxValue); - return true; - } - - // Clamp startColumn to legal high column range. If outside, be conservative. - int maxHigh = pLong - 1; - if (startColumn > maxHigh || startColumn < 0) - { - allowedMin = 0; - allowedMax = long.MaxValue; - return true; - } - - // Determine last processed column. - int endColumn = startColumn - (steps - 1); - if (endColumn < 0) - { - // Processing would go past column 0. We can clamp steps to reach column 0 exactly. - steps = startColumn + 1; - endColumn = 0; - if (steps <= 0) - { - allowedMin = 0; - allowedMax = 0; - return true; - } - } - - // Two fixed interval buffers on stack: each interval is [lo, hi], disjoint and sorted. - Span lo0 = stackalloc long[64]; - Span hi0 = stackalloc long[64]; - Span lo1 = stackalloc long[64]; - Span hi1 = stackalloc long[64]; - - Span outLo = lo0, outHi = hi0; - Span inLo = lo1, inHi = hi1; - - int outCount = 1; - outLo[0] = startCarryOutMin; - outHi[0] = startCarryOutMax; - - int inCount = 0; - bool flip = false; - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - static bool AddInterval(ref int count, Span loArr, Span hiArr, long lo, long hi) - { - if (hi < lo) return true; - if (lo < 0) lo = 0; - if (hi < 0) return true; - - if (count == 0) - { - loArr[0] = lo; - hiArr[0] = hi; - count = 1; - return true; - } - - long lastHi = hiArr[count - 1]; - if (lo <= lastHi + 1) - { - if (hi > lastHi) hiArr[count - 1] = hi; - return true; - } - -if ((uint)count >= (uint)loArr.Length) -{ - // Too many intervals -> disable this filter conservatively. - count = 0; // signal overflow / disabled - return true; // do NOT fail the candidate -} - - loArr[count] = lo; - hiArr[count] = hi; - count++; - return true; - } - - for (int step = 0; step < steps; step++) - { - int column = startColumn - step; - - // n = count of q-offsets t such that 0 <= column - t <= maxAllowedA - // <=> column - maxAllowedA <= t <= column - int lowerT; - long lowerTLong = (long)column - (long)maxAllowedA; - if (lowerTLong <= 0) lowerT = 0; - else if (lowerTLong >= int.MaxValue) lowerT = int.MaxValue; - else lowerT = (int)lowerTLong; - - int upperT = column <= 0 ? 0 : column; - - FindBounds(qOneOffsets, lowerT, upperT, out int left, out int right); - int n = right - left; - if (n < 0) return false; - - inCount = 0; - - for (int i = 0; i < outCount; i++) - { - long a = outLo[i]; - long b = outHi[i]; - - if (b < 0) continue; - if (a < 0) a = 0; - if (b < a) continue; - - const long TwicePlusOneOverflowLimit = (long.MaxValue - 1) >> 1; - - // If carryOut is too large for safe 2*x+1 in long, we must remain conservative. - if (a > TwicePlusOneOverflowLimit || b > TwicePlusOneOverflowLimit) - { - allowedMin = 0; - allowedMax = long.MaxValue; - return true; - } - - long rMin = (a << 1) + 1; - long rMax = (b << 1) + 1; - -// carryIn ∈ [ max(0, r-n), r ] -if (n <= 0) -{ - // n==0 => ones==0 deterministycznie, bit wyniku = 1 => carryIn musi być nieparzyste. - long lo02 = rMin; - long hi02 = rMax; - - if (!IntervalHasParity(lo02, hi02, 1)) - continue; - - if ((lo02 & 1L) == 0) lo02++; - - if (!AddInterval(ref inCount, inLo, inHi, lo02, hi02) || inCount == 0) + /// + /// Mini ping-pong (Option B): compute a conservative allowed carry range after walking + /// top-down for a given number of columns starting at . + /// + /// Semantics: + /// - We treat "carryOut at column = startColumn+1" as the starting set (seed). + /// - Each step processes one column (carryOut -> carryIn) moving downward. + /// - After columns, the resulting set corresponds to carry-in + /// at column (startColumn - steps + 1). + /// + private static bool TryHighBitCarryRangeToColumnJ( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + int pLong, + int maxAllowedA, + int startColumn, // e.g. p-1, then J1-1, ... + int steps, // number of columns to process downward + long startCarryOutMin, // seed carryOut range + long startCarryOutMax, + out long allowedMin, + out long allowedMax) { allowedMin = 0; allowedMax = long.MaxValue; + + if (steps <= 0) + { + // No processing: carry-in == seed (conservative) + allowedMin = startCarryOutMin < 0 ? 0 : startCarryOutMin; + allowedMax = startCarryOutMax < 0 ? 0 : startCarryOutMax; + if (allowedMax < allowedMin) (allowedMin, allowedMax) = (0, long.MaxValue); + return true; + } + + // Clamp startColumn to legal high column range. If outside, be conservative. + int maxHigh = pLong - 1; + if (startColumn > maxHigh || startColumn < 0) + { + allowedMin = 0; + allowedMax = long.MaxValue; + return true; + } + + // Determine last processed column. + int endColumn = startColumn - (steps - 1); + if (endColumn < 0) + { + // Processing would go past column 0. We can clamp steps to reach column 0 exactly. + steps = startColumn + 1; + endColumn = 0; + if (steps <= 0) + { + allowedMin = 0; + allowedMax = 0; + return true; + } + } + + // Two fixed interval buffers on stack: each interval is [lo, hi], disjoint and sorted. + Span lo0 = stackalloc long[64]; + Span hi0 = stackalloc long[64]; + Span lo1 = stackalloc long[64]; + Span hi1 = stackalloc long[64]; + + Span outLo = lo0, outHi = hi0; + Span inLo = lo1, inHi = hi1; + + int outCount = 1; + outLo[0] = startCarryOutMin; + outHi[0] = startCarryOutMax; + + int inCount = 0; + bool flip = false; + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + static bool AddInterval(ref int count, Span loArr, Span hiArr, long lo, long hi) + { + if (hi < lo) return true; + if (lo < 0) lo = 0; + if (hi < 0) return true; + + if (count == 0) + { + loArr[0] = lo; + hiArr[0] = hi; + count = 1; + return true; + } + + long lastHi = hiArr[count - 1]; + if (lo <= lastHi + 1) + { + if (hi > lastHi) hiArr[count - 1] = hi; + return true; + } + + if ((uint)count >= (uint)loArr.Length) + { + // Too many intervals -> disable this filter conservatively. + count = 0; // signal overflow / disabled + return true; // do NOT fail the candidate + } + + loArr[count] = lo; + hiArr[count] = hi; + count++; + return true; + } + + for (int step = 0; step < steps; step++) + { + int column = startColumn - step; + + // n = count of q-offsets t such that 0 <= column - t <= maxAllowedA + // <=> column - maxAllowedA <= t <= column + int lowerT; + long lowerTLong = (long)column - (long)maxAllowedA; + if (lowerTLong <= 0) lowerT = 0; + else if (lowerTLong >= int.MaxValue) lowerT = int.MaxValue; + else lowerT = (int)lowerTLong; + + int upperT = column <= 0 ? 0 : column; + + FindBounds(qOneOffsets, lowerT, upperT, out int left, out int right); + int n = right - left; + if (n < 0) return false; + + inCount = 0; + + for (int i = 0; i < outCount; i++) + { + long a = outLo[i]; + long b = outHi[i]; + + if (b < 0) continue; + if (a < 0) a = 0; + if (b < a) continue; + + const long TwicePlusOneOverflowLimit = (long.MaxValue - 1) >> 1; + + // If carryOut is too large for safe 2*x+1 in long, we must remain conservative. + if (a > TwicePlusOneOverflowLimit || b > TwicePlusOneOverflowLimit) + { + allowedMin = 0; + allowedMax = long.MaxValue; + return true; + } + + long rMin = (a << 1) + 1; + long rMax = (b << 1) + 1; + + // carryIn ∈ [ max(0, r-n), r ] + if (n <= 0) + { + // n==0 => ones==0 deterministycznie, bit wyniku = 1 => carryIn musi być nieparzyste. + long lo02 = rMin; + long hi02 = rMax; + + if (!IntervalHasParity(lo02, hi02, 1)) + continue; + + if ((lo02 & 1L) == 0) lo02++; + + if (!AddInterval(ref inCount, inLo, inHi, lo02, hi02) || inCount == 0) + { + allowedMin = 0; + allowedMax = long.MaxValue; + return true; + } + continue; + } + + long lo = rMin - n; + if (lo < 0) lo = 0; + + if (!AddInterval(ref inCount, inLo, inHi, lo, rMax) || inCount == 0) + { + allowedMin = 0; + allowedMax = long.MaxValue; + return true; + } + } + + if (inCount <= 0) + { + return false; + } + + // Swap buffers for next step. + outCount = inCount; + flip = !flip; + if (!flip) + { + outLo = lo0; outHi = hi0; + inLo = lo1; inHi = hi1; + } + else + { + outLo = lo1; outHi = hi1; + inLo = lo0; inHi = hi0; + } + } + + // After steps, 'out' corresponds to carry-in at the last processed column (endColumn). + allowedMin = outLo[0]; + allowedMax = outHi[outCount - 1]; +#if DETAILED_LOG + Console.WriteLine($"[TD] steps={steps} endRange=[{allowedMin},{allowedMax}] intervals={outCount}"); +#endif + return true; } - continue; -} - long lo = rMin - n; - if (lo < 0) lo = 0; - - if (!AddInterval(ref inCount, inLo, inHi, lo, rMax) || inCount == 0) - { - allowedMin = 0; - allowedMax = long.MaxValue; - return true; - } - } - - if (inCount <= 0) - { - return false; - } - - // Swap buffers for next step. - outCount = inCount; - flip = !flip; - if (!flip) - { - outLo = lo0; outHi = hi0; - inLo = lo1; inHi = hi1; - } - else - { - outLo = lo1; outHi = hi1; - inLo = lo0; inHi = hi0; - } - } - - // After steps, 'out' corresponds to carry-in at the last processed column (endColumn). - allowedMin = outLo[0]; - allowedMax = outHi[outCount - 1]; - Console.WriteLine($"[TD] steps={steps} endRange=[{allowedMin},{allowedMax}] intervals={outCount}"); - - return true; - } - - private static bool TryModularPrefilter( - ReadOnlySpan qOneOffsets, - long qHash, - ulong p, - long maxAllowedA) - { - if (maxAllowedA < 0 || maxAllowedA > ModLocalPrefilterMaxABits) - { - return true; - } - - int bitCount = (int)(maxAllowedA + 1); - if (bitCount <= 0 || bitCount >= 62) - { - return true; - } - - long maxAValue = (1L << bitCount) - 1L; - int modLocalPrefilterModuliLength = ModLocalPrefilterModuli.Length; - for (int i = 0; i < modLocalPrefilterModuliLength; i++) - { - int mod = ModLocalPrefilterModuli[i]; - int qMod = GetQModCached(qOneOffsets, qHash, mod); - int target = ModPow2Minus1(p, mod); - if (qMod == 0) - { - if (target != 0) - { - return false; - } - - continue; - } - - int inverse = ModPow(qMod, mod - 2, mod); - long x = (long)target * inverse % mod; - if (x > maxAValue) - { - return false; - } - } - - return true; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void FindBounds(ReadOnlySpan values, int lowerTarget, int upperTarget, out int lower, out int upper) - { - // Find lower bound for lowerTarget - int lo = 0; - int valuesLength = values.Length; - int hi = valuesLength; - int mid; - while (lo < hi) - { - mid = lo + ((hi - lo) >> 1); - if (values[mid] < lowerTarget) - { - lo = mid + 1; - } - else - { - hi = mid; - } - } - - lower = lo; - - // Find upper bound for upperTarget, starting from the lower bound's result. - // Since upperTarget >= lowerTarget is assumed, we can start the search for the upper bound - // from the position of the lower bound, effectively reducing the search space. - hi = valuesLength; - while (lo < hi) - { - mid = lo + ((hi - lo) >> 1); - if (values[mid] <= upperTarget) - { - lo = mid + 1; - } - else - { - hi = mid; - } - } - - upper = lo; - } - - /// - /// Extremely small, allocation-free prefilter over the last few columns (near p-1). - /// - /// It uses only the fact that the product must have no carry beyond column p-1 (i.e. carry-out from - /// column p-1 is zero) and that bits 0..p-1 of M_p are all ones. - /// - /// This is intentionally conservative (never rejects a valid divisor). In practice it can still - /// remove some q with "awkward" high-bit geometry where the required carry values near the top - /// become impossible given the availability of contributions implied by qOneOffsets and maxAllowedA. - /// - private static bool TryHighBitTopCarryPrefilter( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - long pLong, - long maxAllowedA) - { - // We process last K columns: (p-1), (p-2), ... - int columns = HighBitCarryPrefilterColumns; - long maxPossibleColumns = pLong - 1; - if (columns > maxPossibleColumns) - columns = (int)maxPossibleColumns; - - // Two fixed interval buffers on stack. - // Each interval is [lo, hi], disjoint and sorted. - // 32 is intentionally small: in practice this stays tiny (often 1-2 intervals). - Span lo0 = stackalloc long[64]; - Span hi0 = stackalloc long[64]; - Span lo1 = stackalloc long[64]; - Span hi1 = stackalloc long[64]; - - // "out" = carryOut set for current column (start at top with {0}) - Span outLo = lo0, outHi = hi0; - Span inLo = lo1, inHi = hi1; - - int outCount = 1; - outLo[0] = 0; - outHi[0] = 0; - - int inCount = 0; - bool flip = false; - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - static void AddInterval(ref int count, Span loArr, Span hiArr, long lo, long hi) - { - if (hi < lo) return; - - if (lo < 0) lo = 0; - if (hi < 0) return; - - if (count == 0) - { - loArr[0] = lo; - hiArr[0] = hi; - count = 1; - return; - } - - // Merge into last interval if overlapping/adjacent. - long lastHi = hiArr[count - 1]; - if (lo <= lastHi + 1) - { - if (hi > lastHi) - hiArr[count - 1] = hi; - return; - } - - // Append - if ((uint)count >= (uint)loArr.Length) - { - // If this ever happens, we conservatively stop filtering (do not reject). - // Returning "true" keeps correctness (prefilter is optional). - count = 0; - return; - } - - loArr[count] = lo; - hiArr[count] = hi; - count++; - } - - for (int step = 0; step < columns; step++) - { - long column = maxPossibleColumns - step; - if (column < 0) - break; - - // n = count of q-offsets t such that 0 <= column - t <= maxAllowedA - // <=> column - maxAllowedA <= t <= column - long lowerTLong = column - maxAllowedA; - - int lowerT = - lowerTLong <= 0 ? 0 : - (lowerTLong >= int.MaxValue ? int.MaxValue : (int)lowerTLong); - - int upperT = - column <= 0 ? 0 : - (column >= int.MaxValue ? int.MaxValue : (int)column); - - FindBounds(qOneOffsets, lowerT, upperT, out int left, out int right); - int n = right - left; - - if (n < 0) - { - // Console.WriteLine("n < 0 - excluding in pre-filter"); - return false; - } - - // Build carryIn set into inLo/inHi - inCount = 0; - - // For M_p, bit in columns [0..p-1] is 1: - // carryIn + ones = 1 + 2*carryOut - // carryIn = (2*carryOut + 1) - ones, with ones in [0..min(n, 2*carryOut+1)]. - // - // That yields carryIn interval: - // r = 2*carryOut + 1 - // carryIn ∈ [ r - min(n, r), r ] = [ max(0, r-n), r ]. - // - // Union over carryOut intervals is merged cheaply. - - for (int i = 0; i < outCount; i++) - { - long a = outLo[i]; - long b = outHi[i]; - - if (b < 0) continue; - if (a < 0) a = 0; - if (b < a) continue; - - const long TwicePlusOneOverflowLimit = (long.MaxValue - 1) >> 1; - // When carryOut is already too big, top-down becomes useless in long. - // We want to be conservative to avoid rejecting correct divisors => stop filtering with this filter. - if (a > TwicePlusOneOverflowLimit || b > TwicePlusOneOverflowLimit) - { - return true; - } - - // r ranges from rMin..rMax over carryOut in [a..b] - long rMin = (a << 1) + 1; - long rMax = (b << 1) + 1; - - if (n <= 0) - { - // ones=0 only -> carryIn=r (odd sequence). Conservatively interval [rMin..rMax]. - AddInterval(ref inCount, inLo, inHi, rMin, rMax); - if (inCount == 0) return true; // overflow of intervals -> stop filtering - continue; - } - - if (n == 1) - { - // ones in {0,1} -> carryIn in {r, r-1}. Conservatively [rMin-1 .. rMax]. - AddInterval(ref inCount, inLo, inHi, rMin - 1, rMax); - if (inCount == 0) return true; - continue; - } - - // n >= 2 : union becomes dense enough that interval bounds are safe conservative approximations. - if (rMax <= n) - { - // For all r<=n, lower bound is 0. - AddInterval(ref inCount, inLo, inHi, 0, rMax); - if (inCount == 0) return true; - } - else if (rMin > n) - { - // Always r>n => [r-n .. r] - AddInterval(ref inCount, inLo, inHi, rMin - n, rMax); - if (inCount == 0) return true; - } - else - { - // Crossing: part uses [0..r], later [r-n..r]. For n>=2 union is [0..rMax]. - AddInterval(ref inCount, inLo, inHi, 0, rMax); - if (inCount == 0) return true; - } - } - - if (inCount <= 0) - { - // Console.WriteLine("inCount <= 0 - excluding in pre-filter"); - return false; - } - - // Prepare for next column: carryOut := carryIn (shift down one column) - outCount = inCount; - - // Toggle which buffers are used for out vs in. - // Avoid tuple swap / temp Span to satisfy Span lifetime rules. - flip = !flip; - if (!flip) - { - outLo = lo0; outHi = hi0; - inLo = lo1; inHi = hi1; - } - else - { - outLo = lo1; outHi = hi1; - inLo = lo0; inHi = hi0; - } - } - - return true; - } - - - private static int[] GetPow2DiffLut(int mod) - { - _pow2DiffModCache ??= new Dictionary(); - if (_pow2DiffModCache.TryGetValue(mod, out int[]? lut)) - { - return lut; - } - - int[] values = new int[256]; - values[0] = mod > 1 ? 1 : 0; - for (int i = 1; i < values.Length; i++) - { - values[i] = (values[i - 1] << 1) % mod; - } - - _pow2DiffModCache[mod] = values; - return values; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void ComputeForcedRemainingAndClean_Prefix( - in ulong[] qMask, in ulong[] oneWin, in ulong[] zeroWin, - int words, ulong lastMask, - out int forced, out int remaining) - { - if (words == 0) - { - forced = 0; - remaining = 0; - return; - } - - int i = 0; - int wordsMinusOne = words - 1; - var vForced = Vector.Zero; - var vRemaining = Vector.Zero; - - if (Vector.IsHardwareAccelerated) - { - // Console.WriteLine("SIMD accelerator ComputeForcedRemainingAndClean_Prefix"); - int limit = wordsMinusOne - (wordsMinusOne % Vector.Count); - for (; i < limit; i += Vector.Count) - { - var vq = new Vector(qMask, i); - var vOne = new Vector(oneWin, i); - var vZero = new Vector(zeroWin, i); - - var vKnown = vOne | vZero; - var vForcedBits = vOne & vq; - var vUnknownBits = vq & ~vKnown; - - vForced += SimdPopCount(vForcedBits); - vRemaining += SimdPopCount(vUnknownBits); - } - } - // else - // { - // Console.WriteLine("No acceleration for ComputeForcedRemainingAndClean_Prefix"); - // } - - forced = (int)Vector.Sum(vForced); - remaining = (int)Vector.Sum(vRemaining); - - for (; i < wordsMinusOne; i++) - { - ulong unknownBits = qMask[i]; - ulong one = oneWin[i]; - ulong known = one | zeroWin[i]; - one &= unknownBits; - unknownBits &= ~known; - forced += PopCount(one); - remaining += PopCount(unknownBits); - } - - if (words > 0) - { - ulong unknownBits = qMask[words - 1] & lastMask; - ulong one = oneWin[words - 1]; - ulong known = one | zeroWin[words - 1]; - one &= unknownBits; - unknownBits &= ~known; - forced += PopCount(one); - remaining += PopCount(unknownBits); - } - } - - private static int ComputeQMod(ReadOnlySpan qOneOffsets, int mod) - { - int count = qOneOffsets.Length; - if (count == 0) - { - return 0; - } - - int[] diffLut = GetPow2DiffLut(mod); - int diffLutLength = diffLut.Length; - long sum = 0; - int prevOffset = qOneOffsets[0]; - long pow = PowMod2((ulong)prevOffset, mod); - sum += pow; - - for (int i = 1; i < count; i++) - { - int offset = qOneOffsets[i]; - int diff = offset - prevOffset; - if (diff <= 0) - { - prevOffset = offset; - continue; - } - - if (diff < diffLutLength) - { - pow = pow * diffLut[diff] % mod; - } - else - { - pow = pow * PowMod2((ulong)diff, mod) % mod; - } - - sum += pow; - if (sum >= mod) - { - sum %= mod; - } - - prevOffset = offset; - } - - return (int)(sum % mod); - } - - private static bool ExistsCongruentInRange(BigInteger minA, BigInteger maxA, int residue, int mod) - { - if (minA > maxA) - { - return false; - } - - int minMod = (int)((minA % mod + mod) % mod); - int delta = residue - minMod; - if (delta < 0) - { - delta += mod; - } - - BigInteger candidate = minA + delta; - return candidate <= maxA; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void GetQPrefixMask(int startColumn, int qBitLen, int qWordCount, out int words, out ulong lastMask) - { - // We want only offsets t <= startColumn. - // start column is inclusive for maxT - if (startColumn >= qBitLen - 1) - { - words = qWordCount; - lastMask = ulong.MaxValue; // caller can still & lastWordMask separately - return; - } - - if (startColumn < 0) - { - words = 0; - lastMask = 0; - return; - } - - qBitLen = startColumn >> 6; - words = qBitLen + 1; - - qWordCount = startColumn & 63; - lastMask = qWordCount == 63 ? ulong.MaxValue : ((1UL << (qWordCount + 1)) - 1UL); - } - - private static void ComputeARangeFromTopConstraints( - long maxAllowedA, - bool top0KnownOne, - bool top0KnownZero, - bool top1KnownOne, - long zeroTailStart, - out BigInteger minA, - out BigInteger maxA) - { - _dynamicModChecks++; - if (zeroTailStart <= maxAllowedA + 1) - { - zeroTailStart--; - } - - // zeroTailStart is effectiveTop from here. We're reusing variable to limit registry pressure. - if (zeroTailStart < 0) - { - minA = BigInteger.Zero; - maxA = BigInteger.Zero; - return; - } - - int shift = zeroTailStart + 1L > int.MaxValue ? int.MaxValue : (int)(zeroTailStart + 1L); - maxA = Pow2Provider.BigIntegerMinusOne(shift); - minA = BigInteger.Zero; - - if (zeroTailStart == maxAllowedA) - { - if (top0KnownOne) - { - shift = maxAllowedA > int.MaxValue ? int.MaxValue : (int)maxAllowedA; - } - else if (top0KnownZero && top1KnownOne && maxAllowedA - 1L >= 0) - { - // zeroTailStart is index from here. We're reusing the variable to limit registry pressure. - zeroTailStart = maxAllowedA - 1L; - shift = zeroTailStart > int.MaxValue ? int.MaxValue : (int)zeroTailStart; - } - - minA = Pow2Provider.BigInteger(shift); - } - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static bool IsCleanInQ_Prefix(ulong[] qMask, ulong[] oneWin, ulong[] zeroWin, int words, ulong lastMask) - { - for (int i = 0; i < words; i++) - { - ulong q = qMask[i]; - if (i == words - 1) q &= lastMask; - if ((q & (oneWin[i] | zeroWin[i])) != 0) return false; - } - - return true; - } - - private static bool TryDynamicModularRangePrune( - ReadOnlySpan qOneOffsets, - long qHash, - ulong p, - long maxAllowedA, - bool top0KnownOne, - bool top0KnownZero, - bool top1KnownOne, - long zeroTailStart) - { - _dynamicModChecks++; - long effectiveTop = maxAllowedA; - if (zeroTailStart <= effectiveTop + 1) - { - effectiveTop = zeroTailStart - 1; - } - - if (effectiveTop > 4096) - { - return true; - } - - ComputeARangeFromTopConstraints( - maxAllowedA, - top0KnownOne, - top0KnownZero, - top1KnownOne, - zeroTailStart, - out BigInteger minA, - out BigInteger maxA); - - int modLocalPrefilterModuliLength = ModLocalPrefilterModuli.Length; - for (int i = 0; i < modLocalPrefilterModuliLength; i++) - { - int mod = ModLocalPrefilterModuli[i]; - int qMod = GetQModCached(qOneOffsets, qHash, mod); - int target = ModPow2Minus1(p, mod); - if (qMod == 0) - { - if (target != 0) - { - return false; - } - continue; - } - - int inverse = ModPow(qMod, mod - 2, mod); - int aResidue = (int)((long)target * inverse % mod); - if (!ExistsCongruentInRange(minA, maxA, aResidue, mod)) - { - _dynamicModFailures++; - return false; - } - } - - return true; - } - - private static int ModPow2Minus1(ulong p, int mod) - { - int pow = PowMod2(p, mod); - int result = pow - 1; - return result < 0 ? result + mod : result; - } - - private static int PowMod2(ulong exp, int mod) - { - long result = 1; - long baseVal = 2; - ulong value = exp; - while (value > 0) - { - if ((value & 1) != 0) - { - result = (result * baseVal) % mod; - } - - baseVal = (baseVal * baseVal) % mod; - value >>= 1; - } - - return (int)result; - } - - private static int ModPow(int value, int exp, int mod) - { - long result = 1 % mod; - long baseVal = value % mod; - int e = exp; - while (e > 0) - { - if ((e & 1) != 0) - { - result = (result * baseVal) % mod; - } - - baseVal = (baseVal * baseVal) % mod; - e >>= 1; - } - - return (int)result; - } - - // internal static bool TryCheckDivisibilityFromDivisor(ulong q, ulong p, out bool divides, out ContradictionReason reason) - // { - // divides = false; - // if (q == 0UL) - // { - // reason = ContradictionReason.ParityUnreachable; - // return true; - // } - - // Span oneOffsets = stackalloc int[64]; - // int count = 0; - // ulong remaining = q; - // int baseIndex = 0; - // while (remaining != 0UL) - // { - // int tz = BitOperations.TrailingZeroCount(remaining); - // baseIndex += tz; - // oneOffsets[count++] = baseIndex; - // remaining >>= tz + 1; - // baseIndex++; - // } - - // return TryCheckDivisibilityFromOneOffsets(oneOffsets.Slice(0, count), p, out divides, out reason); - // } - - [ThreadStatic] - private static bool _initialized; - - public static void Initialize() - { - if (_initialized) - { - return; - } - - // _privateWorkSet = new(); - // _stableUnknownDelta8 = new(); - _initialized = true; - // Start with a small size and grow on demand. - _stableUnknownDelta8ByUnknown = new int[64][]; - _privateWorkSet = new PrivateWorkSet(); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static int ComputeForcedSumFromKnownPrefix( - ReadOnlySpan qOneOffsets, - int col, - ulong[] knownOne0) - { - int forced = 0; - - // qOneOffsets są rosnące; przerywamy gdy t>col (bo wtedy aIndex<0 => wkład 0) - for (int i = 0; i < qOneOffsets.Length; i++) - { - int t = qOneOffsets[i]; - if (t > col) break; - - int aIndex = col - t; // w prefiksie gwarantujemy 0 <= aIndex <= maxFixed - ulong word = knownOne0[aIndex >> 6]; - forced += (int)((word >> (aIndex & 63)) & 1UL); - } - - return forced; - } - - /// - /// Full column-wise propagation for a given set of q one-bit offsets (LSB=0) and exponent p. - /// Returns true if the solver could decide locally (divides or contradiction). - /// -#if DETAILED_LOG - internal static bool TryCheckDivisibilityFromOneOffsets( - ReadOnlySpan qOneOffsets, - ulong p, - BigInteger k, - bool isPowerOfTwo, - out bool divides, - out ContradictionReason reason) -#else - internal static bool TryCheckDivisibilityFromOneOffsets( - ReadOnlySpan qOneOffsets, - ulong p, - BigInteger k, - bool isPowerOfTwo, - out bool divides) -#endif - { - if (!_initialized) - { - Initialize(); - } - - PrivateWorkSet workSet = _privateWorkSet; - - divides = false; - - Dbg(p, k, $"[TGT] Enter solver. p={p} k={k} isPowerOfTwo={isPowerOfTwo}"); -#if DETAILED_LOG - _lastTopDownFailure = null; - _statStableAdvanceCalls = 0; - _statStableAdvanceCols = 0; - _statStableAdvanceColsBatched = 0; - _statScalarCols = 0; - _statDeltaRequests = 0; - _statDeltaHits = 0; - _statDeltaBuilds = 0; - _statStableAdvanceBigShift = 0; - _statCleanChecks = 0; - _statCleanFalse = 0; - _statFirstDirtyColumn = -1; -#endif - _dynamicModChecks = 0; - _dynamicModFailures = 0; - - // These conditions will never be true on EvenPerfectBitScanner execution path. - // if (p == 0 || qOneOffsets.Length == 0) - // { - // reason = ContradictionReason.ParityUnreachable; - // return true; - // } - - // While the scanner supports p >= 31, it's a tiny subset of all checked exponents. No need to support it. - // Exact small-case evaluation to short-circuit both success and failure deterministically. - // int highestBit = qOneOffsets[^1]; - // if (p <= 64 && highestBit < 63) - // { - // ulong q = 0; - // foreach (int bit in qOneOffsets) - // { - // q |= 1UL << bit; - // } - - // ulong mersenne = (1UL << (int)p) - 1UL; - // divides = q != 0 && (mersenne % q == 0); - // reason = divides ? ContradictionReason.None : ContradictionReason.ParityUnreachable; - // return true; - // } - - int qOneOffsetsLength = qOneOffsets.Length; - int qBitLen = qOneOffsets[qOneOffsetsLength - 1] + 1; - if ((ulong)qBitLen >= p) - { -#if DETAILED_LOG - reason = ContradictionReason.TruncatedLength; -#endif - return true; - } - - // q from EvenPerfectBitScanner will always have the correct 2kp+1 form. - // if (qOneOffsets[0] != 0) - // { - // reason = ContradictionReason.ParityUnreachable; - // return true; - // } - - const int ForcedALowBits = 1024; - int windowSize = qBitLen < ForcedALowBits ? ForcedALowBits : qBitLen; - windowSize = (windowSize + 63) & ~63; - int aWordCount = (windowSize + 63) >> 6; - int qWordCount = (qBitLen + 63) >> 6; - workSet.EnsureCapacity(aWordCount, qWordCount); - ulong[] knownOne0 = workSet.KnownOne0; - ulong[] knownOne1 = workSet.KnownOne1; - ulong[] knownZero0 = workSet.KnownZero0; - ulong[] knownZero1 = workSet.KnownZero1; - ulong[] qMaskWords = workSet.QMaskWords; - - Array.Clear(knownOne0, 0, aWordCount); - Array.Clear(knownOne1, 0, aWordCount); - Array.Clear(knownZero0, 0, aWordCount); - Array.Clear(knownZero1, 0, aWordCount); - Array.Clear(qMaskWords, 0, qWordCount); - - int segmentBase = 0; - int pLong = (int)p; - int maxAllowedA = pLong - qBitLen; - if (maxAllowedA < 0) - { -#if DETAILED_LOG - reason = ContradictionReason.TruncatedLength; -#endif - return true; - } - - // Force low bits of 'a' from a ≡ -q^{-1} (mod 2^1024). - // This is a necessary condition for q | (2^p - 1) when p >= 1024 (true here). - BigInteger mask = Pow2Provider.BigIntegerMinusOne(ForcedALowBits); - BigInteger qMod2k; - bool usedPow2Transform = false; - if (isPowerOfTwo && workSet.HasLastPow2QMod2k && workSet.LastPow2K != BigInteger.Zero && k == (workSet.LastPow2K << 1)) - { - qMod2k = ((workSet.LastPow2QMod2k << 1) - BigInteger.One) & mask; - usedPow2Transform = true; - } - else - { - qMod2k = BigInteger.Zero; - } - - byte[] qMod2kBytes = workSet.QMod2kBytes; - Span qPrefix = stackalloc ulong[16]; - int i, lastBit, t, index, forced, word; - ulong wordValue; - ulong[] bitMask64 = BitMask64; - if (usedPow2Transform) - { - for (i = 0; i < qOneOffsetsLength; i++) - { - t = qOneOffsets[i]; - qMaskWords[t >> 6] |= bitMask64[t & 63]; - if ((uint)t < 1024u) - { - qPrefix[t >> 6] |= bitMask64[t & 63]; - } - } - } - else - { - Array.Clear(qMod2kBytes, 0, qMod2kBytes.Length); - int currentByte = -1; - byte currentValue = 0; - for (i = 0; i < qOneOffsetsLength; i++) - { - t = qOneOffsets[i]; - if (t < ForcedALowBits) - { - // lastBit stand for lastByte here. We're reusing variable to limit registry pressure. - lastBit = t >> 3; - if (lastBit != currentByte) - { - if (currentByte >= 0) - { - qMod2kBytes[currentByte] = currentValue; - } - - currentByte = lastBit; - currentValue = 0; - } - - currentValue |= (byte)(1 << (t & 7)); - } - - qMaskWords[t >> 6] |= bitMask64[t & 63]; - if ((uint)t < 1024u) - { - qPrefix[t >> 6] |= bitMask64[t & 63]; - } - } - - if (currentByte >= 0) - { - qMod2kBytes[currentByte] = currentValue; - } - - qMod2k = new BigInteger(qMod2kBytes, isUnsigned: true, isBigEndian: false); - } - - ulong[] reversePrefix = workSet.LastQReverse; - GetReversePrefix1024(workSet, qPrefix, reversePrefix); - ulong[] lastPrefix = workSet.LastQPrefix; - for (i = 0; i < 16; i++) - { - lastPrefix[i] = qPrefix[i]; - } - - workSet.HasLastQPrefix1024 = true; - - // Compute inv = q^{-1} mod 2^1024 using Hensel/Newton iteration in Z/2^kZ. - BigInteger[] invByKMod = workSet.InvByKMod; - bool[] hasInvByKMod = workSet.HasInvByKMod; - int kMod = (int)(k & 1023); - BigInteger inv; - if (hasInvByKMod[kMod]) - { - inv = invByKMod[kMod]; - } - else if (workSet.HasLastInvMod2k) - { - inv = workSet.LastInvMod2k; - } - else - { - inv = qMod2k; - } - - inv = (inv * (BigIntegerNumbers.Two - (qMod2k * inv))) & mask; - inv = (inv * (BigIntegerNumbers.Two - (qMod2k * inv))) & mask; - inv = (inv * (BigIntegerNumbers.Two - (qMod2k * inv))) & mask; - - if (((qMod2k * inv) & mask) != BigInteger.One) - { - inv = qMod2k; - for (i = 0; i < 5; i++) - { - inv = (inv * (BigIntegerNumbers.Two - (qMod2k * inv))) & mask; - inv = (inv * (BigIntegerNumbers.Two - (qMod2k * inv))) & mask; - } - } - - BigInteger aLow = (-inv) & mask; - - if (isPowerOfTwo) - { - workSet.LastPow2QMod2k = qMod2k; - workSet.LastPow2K = k; - workSet.HasLastPow2QMod2k = true; - } - - workSet.LastInvMod2k = inv; - workSet.HasLastInvMod2k = true; - invByKMod[kMod] = inv; - hasInvByKMod[kMod] = true; - // a ≡ -aLow (mod 2^512) - // Apply constraints for bits i in [0..min(511, maxAllowedA)] into knownOne0/knownZero0. - // NOTE: now windowSize >= 512, so wordCount is enough to store these bits. - Span aLowBytes = stackalloc byte[128]; - if (!aLow.TryWriteBytes(aLowBytes, out int aLowBytesWritten, isUnsigned: true, isBigEndian: false)) - { - aLowBytesWritten = 0; - } - - int maxKnownA; - int maxFixed = maxAllowedA < (ForcedALowBits - 1) ? maxAllowedA : (ForcedALowBits - 1); - - if (maxFixed >= 0) - { - int numWordsToProcess = (maxFixed >> 6) + 1; - Array.Clear(knownOne0, 0, numWordsToProcess); - - int bytesToCopy = Math.Min(aLowBytesWritten, numWordsToProcess * 8); - if (bytesToCopy > 0) - { - System.Runtime.InteropServices.MemoryMarshal.Cast(aLowBytes.Slice(0, bytesToCopy)) - .CopyTo(new Span(knownOne0, 0, (bytesToCopy + 7) / 8)); - } - - i = 0; - if (Vector.IsHardwareAccelerated) - { - int limit = numWordsToProcess - (numWordsToProcess % Vector.Count); - for (; i < limit; i += Vector.Count) - { - var vKnownOne = new Vector(knownOne0, i); - (~vKnownOne).CopyTo(knownZero0, i); - } - } - for (; i < numWordsToProcess; i++) - { - knownZero0[i] = ~knownOne0[i]; - } - - int lastWordIndex = maxFixed >> 6; - int lastBitInWord = maxFixed & 63; - if (lastBitInWord < 63) - { - ulong finalMask = (1UL << (lastBitInWord + 1)) - 1UL; - knownOne0[lastWordIndex] &= finalMask; - knownZero0[lastWordIndex] &= finalMask; - } - } - - // We have learned bits up to maxFixed in the current segment. - maxKnownA = -1; - if (maxFixed > maxKnownA) - { - maxKnownA = maxFixed; - } - - CarryRange carryLow = CarryRange.Zero; - - // ------------------------------------------------------------ - // Cheap low-column prefilter (prefix-style): - // For the first N columns, all a-indices that contribute to the column are within - // the forced low-bit region (aLow). When every contributing bit is known (remaining==0), - // we can propagate carry deterministically and reject immediately on contradiction. - // This is significantly cheaper than entering the full row-aware window DP. - // ------------------------------------------------------------ - // maxFixed now serves as preMax. - maxFixed = 512 - 1; // 256..512 is a good trade-off; keep <= 1024 forced bits - if (maxFixed > maxKnownA) - { - maxFixed = maxKnownA; - } - - if (maxFixed > maxAllowedA) - { - maxFixed = maxAllowedA; - } - // Do NOT clamp to maxOffset: for columns above maxOffset the full set of q=1 positions - // still contributes, and aLow still fixes the corresponding a-bits. - - // Only run if we have at least a few columns to check. - if (maxFixed >= 8) - { - Span prefixMask = stackalloc ulong[16]; - // index is column here. We're reusing the variable to limit registry pressure. - for (index = 0; index <= maxFixed; index++) - { - // Required result bit for M_p in columns [0..p-1] is 1. - // Compute forced ones exactly: sum of a_{col - t} for all q_t=1 with t<=col. - forced = 0; - if (index <= 1023) - { - int shift = 1023 - index; - int wordShift = shift >> 6; - int bitShift = shift & 63; - for (word = 0; word < 16; word++) - { - int src = word + wordShift; - ulong value = 0; - if (src < 16) - { - value = reversePrefix[src] >> bitShift; - if (bitShift != 0 && src + 1 < 16) - { - value |= reversePrefix[src + 1] << (64 - bitShift); - } - } - - prefixMask[word] = value; - } - - forced = 0; - for (word = 0; word < 16; word++) - { - forced += PopCount(knownOne0[word] & prefixMask[word]); - } - } - else - { - for (i = 0; i < qOneOffsetsLength; i++) - { - t = qOneOffsets[i]; - if (t > index) - { - break; - } - - int aIndex = index - t; - // For this prefilter we only run where aIndex is guaranteed within [0..maxFixed]. - word = aIndex >> 6; - ulong m64 = bitMask64[aIndex & 63]; - if ((knownOne0[word] & m64) != 0) forced++; - } - } - - // remaining==0 here, so possible==forced. Propagate carry range deterministically. - if (!TryPropagateCarry(ref carryLow, forced, forced, 1)) - { - // reason = ContradictionReason.ParityUnreachable; - divides = false; - Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryPropagateCarry)}, reversed prefix filter"); - return true; - } - } - } - -// ----------------------------- -// Force MSB of 'a' to be 1 (last row must be active => a has exact bit-length maxAllowedA+1) -// ----------------------------- -if (maxAllowedA >= 0) -{ - int msbIndex = maxAllowedA; - - // Check existing knowledge to avoid contradiction - int msbState = GetAKnownStateRowAware(msbIndex, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); - if (msbState == 2) + private static bool TryModularPrefilter( + ReadOnlySpan qOneOffsets, + long qHash, + ulong p, + long maxAllowedA) { -#if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + if (maxAllowedA < 0 || maxAllowedA > ModLocalPrefilterMaxABits) + { + return true; + } + + int bitCount = (int)(maxAllowedA + 1); + if (bitCount <= 0 || bitCount >= 62) + { + return true; + } + + long maxAValue = (1L << bitCount) - 1L; + + int modLocalPrefilterModuliLength = ModLocalPrefilterModuli.Length; + for (int i = 0; i < modLocalPrefilterModuliLength; i++) + { + int mod = ModLocalPrefilterModuli[i]; + int qMod = GetQModCached(qOneOffsets, qHash, mod); + int target = ModPow2Minus1(p, mod); + if (qMod == 0) + { + if (target != 0) + { + return false; + } + + continue; + } + + int inverse = ModPow(qMod, mod - 2, mod); + long x = (long)target * inverse % mod; + if (x > maxAValue) + { + return false; + } + } + + return true; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void FindBounds(ReadOnlySpan values, int lowerTarget, int upperTarget, out int lower, out int upper) + { + // Find lower bound for lowerTarget + int lo = 0; + int valuesLength = values.Length; + int hi = valuesLength; + int mid; + while (lo < hi) + { + mid = lo + ((hi - lo) >> 1); + if (values[mid] < lowerTarget) + { + lo = mid + 1; + } + else + { + hi = mid; + } + } + + lower = lo; + + // Find upper bound for upperTarget, starting from the lower bound's result. + // Since upperTarget >= lowerTarget is assumed, we can start the search for the upper bound + // from the position of the lower bound, effectively reducing the search space. + hi = valuesLength; + while (lo < hi) + { + mid = lo + ((hi - lo) >> 1); + if (values[mid] <= upperTarget) + { + lo = mid + 1; + } + else + { + hi = mid; + } + } + + upper = lo; + } + + /// + /// Extremely small, allocation-free prefilter over the last few columns (near p-1). + /// + /// It uses only the fact that the product must have no carry beyond column p-1 (i.e. carry-out from + /// column p-1 is zero) and that bits 0..p-1 of M_p are all ones. + /// + /// This is intentionally conservative (never rejects a valid divisor). In practice it can still + /// remove some q with "awkward" high-bit geometry where the required carry values near the top + /// become impossible given the availability of contributions implied by qOneOffsets and maxAllowedA. + /// + private static bool TryHighBitTopCarryPrefilter( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + long pLong, + long maxAllowedA) + { + // We process last K columns: (p-1), (p-2), ... + int columns = HighBitCarryPrefilterColumns; + long maxPossibleColumns = pLong - 1; + if (columns > maxPossibleColumns) + columns = (int)maxPossibleColumns; + + // Two fixed interval buffers on stack. + // Each interval is [lo, hi], disjoint and sorted. + // 32 is intentionally small: in practice this stays tiny (often 1-2 intervals). + Span lo0 = stackalloc long[64]; + Span hi0 = stackalloc long[64]; + Span lo1 = stackalloc long[64]; + Span hi1 = stackalloc long[64]; + + // "out" = carryOut set for current column (start at top with {0}) + Span outLo = lo0, outHi = hi0; + Span inLo = lo1, inHi = hi1; + + int outCount = 1; + outLo[0] = 0; + outHi[0] = 0; + + int inCount = 0; + bool flip = false; + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + static void AddInterval(ref int count, Span loArr, Span hiArr, long lo, long hi) + { + if (hi < lo) return; + + if (lo < 0) lo = 0; + if (hi < 0) return; + + if (count == 0) + { + loArr[0] = lo; + hiArr[0] = hi; + count = 1; + return; + } + + // Merge into last interval if overlapping/adjacent. + long lastHi = hiArr[count - 1]; + if (lo <= lastHi + 1) + { + if (hi > lastHi) + hiArr[count - 1] = hi; + return; + } + + // Append + if ((uint)count >= (uint)loArr.Length) + { + // If this ever happens, we conservatively stop filtering (do not reject). + // Returning "true" keeps correctness (prefilter is optional). + count = 0; + return; + } + + loArr[count] = lo; + hiArr[count] = hi; + count++; + } + + for (int step = 0; step < columns; step++) + { + long column = maxPossibleColumns - step; + if (column < 0) + break; + + // n = count of q-offsets t such that 0 <= column - t <= maxAllowedA + // <=> column - maxAllowedA <= t <= column + long lowerTLong = column - maxAllowedA; + + int lowerT = + lowerTLong <= 0 ? 0 : + (lowerTLong >= int.MaxValue ? int.MaxValue : (int)lowerTLong); + + int upperT = + column <= 0 ? 0 : + (column >= int.MaxValue ? int.MaxValue : (int)column); + + FindBounds(qOneOffsets, lowerT, upperT, out int left, out int right); + int n = right - left; + + if (n < 0) + { + // Console.WriteLine("n < 0 - excluding in pre-filter"); + return false; + } + + // Build carryIn set into inLo/inHi + inCount = 0; + + // For M_p, bit in columns [0..p-1] is 1: + // carryIn + ones = 1 + 2*carryOut + // carryIn = (2*carryOut + 1) - ones, with ones in [0..min(n, 2*carryOut+1)]. + // + // That yields carryIn interval: + // r = 2*carryOut + 1 + // carryIn ∈ [ r - min(n, r), r ] = [ max(0, r-n), r ]. + // + // Union over carryOut intervals is merged cheaply. + + for (int i = 0; i < outCount; i++) + { + long a = outLo[i]; + long b = outHi[i]; + + if (b < 0) continue; + if (a < 0) a = 0; + if (b < a) continue; + + const long TwicePlusOneOverflowLimit = (long.MaxValue - 1) >> 1; + // When carryOut is already too big, top-down becomes useless in long. + // We want to be conservative to avoid rejecting correct divisors => stop filtering with this filter. + if (a > TwicePlusOneOverflowLimit || b > TwicePlusOneOverflowLimit) + { + return true; + } + + // r ranges from rMin..rMax over carryOut in [a..b] + long rMin = (a << 1) + 1; + long rMax = (b << 1) + 1; + + if (n <= 0) + { + // ones=0 only -> carryIn=r (odd sequence). Conservatively interval [rMin..rMax]. + AddInterval(ref inCount, inLo, inHi, rMin, rMax); + if (inCount == 0) return true; // overflow of intervals -> stop filtering + continue; + } + + if (n == 1) + { + // ones in {0,1} -> carryIn in {r, r-1}. Conservatively [rMin-1 .. rMax]. + AddInterval(ref inCount, inLo, inHi, rMin - 1, rMax); + if (inCount == 0) return true; + continue; + } + + // n >= 2 : union becomes dense enough that interval bounds are safe conservative approximations. + if (rMax <= n) + { + // For all r<=n, lower bound is 0. + AddInterval(ref inCount, inLo, inHi, 0, rMax); + if (inCount == 0) return true; + } + else if (rMin > n) + { + // Always r>n => [r-n .. r] + AddInterval(ref inCount, inLo, inHi, rMin - n, rMax); + if (inCount == 0) return true; + } + else + { + // Crossing: part uses [0..r], later [r-n..r]. For n>=2 union is [0..rMax]. + AddInterval(ref inCount, inLo, inHi, 0, rMax); + if (inCount == 0) return true; + } + } + + if (inCount <= 0) + { + // Console.WriteLine("inCount <= 0 - excluding in pre-filter"); + return false; + } + + // Prepare for next column: carryOut := carryIn (shift down one column) + outCount = inCount; + + // Toggle which buffers are used for out vs in. + // Avoid tuple swap / temp Span to satisfy Span lifetime rules. + flip = !flip; + if (!flip) + { + outLo = lo0; outHi = hi0; + inLo = lo1; inHi = hi1; + } + else + { + outLo = lo1; outHi = hi1; + inLo = lo0; inHi = hi0; + } + } + + return true; + } + + + private static int[] GetPow2DiffLut(int mod) + { + _pow2DiffModCache ??= new Dictionary(); + if (_pow2DiffModCache.TryGetValue(mod, out int[]? lut)) + { + return lut; + } + + int[] values = new int[256]; + values[0] = mod > 1 ? 1 : 0; + for (int i = 1; i < values.Length; i++) + { + values[i] = (values[i - 1] << 1) % mod; + } + + _pow2DiffModCache[mod] = values; + return values; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void ComputeForcedRemainingAndClean_Prefix( + in ulong[] qMask, in ulong[] oneWin, in ulong[] zeroWin, + int words, ulong lastMask, + out int forced, out int remaining) + { + if (words == 0) + { + forced = 0; + remaining = 0; + return; + } + + int i = 0; + int wordsMinusOne = words - 1; + var vForced = Vector.Zero; + var vRemaining = Vector.Zero; + + if (Vector.IsHardwareAccelerated) + { + // Console.WriteLine("SIMD accelerator ComputeForcedRemainingAndClean_Prefix"); + int limit = wordsMinusOne - (wordsMinusOne % Vector.Count); + for (; i < limit; i += Vector.Count) + { + var vq = new Vector(qMask, i); + var vOne = new Vector(oneWin, i); + var vZero = new Vector(zeroWin, i); + + var vKnown = vOne | vZero; + var vForcedBits = vOne & vq; + var vUnknownBits = vq & ~vKnown; + + vForced += SimdPopCount(vForcedBits); + vRemaining += SimdPopCount(vUnknownBits); + } + } + // else + // { + // Console.WriteLine("No acceleration for ComputeForcedRemainingAndClean_Prefix"); + // } + + forced = (int)Vector.Sum(vForced); + remaining = (int)Vector.Sum(vRemaining); + + for (; i < wordsMinusOne; i++) + { + ulong unknownBits = qMask[i]; + ulong one = oneWin[i]; + ulong known = one | zeroWin[i]; + one &= unknownBits; + unknownBits &= ~known; + forced += PopCount(one); + remaining += PopCount(unknownBits); + } + + if (words > 0) + { + ulong unknownBits = qMask[words - 1] & lastMask; + ulong one = oneWin[words - 1]; + ulong known = one | zeroWin[words - 1]; + one &= unknownBits; + unknownBits &= ~known; + forced += PopCount(one); + remaining += PopCount(unknownBits); + } + } + + private static int ComputeQMod(ReadOnlySpan qOneOffsets, int mod) + { + int count = qOneOffsets.Length; + if (count == 0) + { + return 0; + } + + int[] diffLut = GetPow2DiffLut(mod); + int diffLutLength = diffLut.Length; + long sum = 0; + int prevOffset = qOneOffsets[0]; + long pow = PowMod2((ulong)prevOffset, mod); + sum += pow; + + for (int i = 1; i < count; i++) + { + int offset = qOneOffsets[i]; + int diff = offset - prevOffset; + if (diff <= 0) + { + prevOffset = offset; + continue; + } + + if (diff < diffLutLength) + { + pow = pow * diffLut[diff] % mod; + } + else + { + pow = pow * PowMod2((ulong)diff, mod) % mod; + } + + sum += pow; + if (sum >= mod) + { + sum %= mod; + } + + prevOffset = offset; + } + + return (int)(sum % mod); + } + + private static bool ExistsCongruentInRange(BigInteger minA, BigInteger maxA, int residue, int mod) + { + if (minA > maxA) + { + return false; + } + + int minMod = (int)((minA % mod + mod) % mod); + int delta = residue - minMod; + if (delta < 0) + { + delta += mod; + } + + BigInteger candidate = minA + delta; + return candidate <= maxA; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static int NormalizeMod(int value, int mod) + { + int normalized = value % mod; + return normalized < 0 ? normalized + mod : normalized; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool IsResidueReachable(ulong mask, int residue) + { + return ((mask >> residue) & 1UL) != 0UL; + } + + private static bool TryPruneWithKnownBitsModResidue( + ReadOnlySpan qOneOffsets, + long qHash, + ulong p, + int mod, + long maxAllowedA, + HashSet knownOneIndices, + HashSet knownZeroIndices) + { + if (maxAllowedA < 0) + { + return true; + } + + int maxIndex = maxAllowedA > int.MaxValue ? int.MaxValue : (int)maxAllowedA; + + int bitsNeeded = 0; + int bitsSource = mod - 1; + while (bitsSource > 0) + { + bitsNeeded++; + bitsSource >>= 1; + } + + if (bitsNeeded <= 0) + { + bitsNeeded = 1; + } + + int qMod = GetQModCached(qOneOffsets, qHash, mod); + int target = ModPow2Minus1(p, mod); + if (qMod == 0) + { + return target != 0; + } + + int inverse = ModPow(qMod, mod - 2, mod); + int targetA = (int)((long)target * inverse % mod); + + int fixedResidue = 0; + foreach (int index in knownOneIndices) + { + if ((uint)index > (uint)maxIndex) + { + continue; + } + + fixedResidue += PowMod2((ulong)index, mod); + if (fixedResidue >= mod) + { + fixedResidue %= mod; + } + } + + targetA = NormalizeMod(targetA - fixedResidue, mod); + + List knownIndices = new(knownOneIndices.Count + knownZeroIndices.Count); + foreach (int index in knownOneIndices) + { + if ((uint)index <= (uint)maxIndex) + { + knownIndices.Add(index); + } + } + + foreach (int index in knownZeroIndices) + { + if ((uint)index <= (uint)maxIndex) + { + knownIndices.Add(index); + } + } + + knownIndices.Sort(); + + ulong reachableMask = 1UL; + ulong moduloMask = (1UL << mod) - 1UL; + + int previousKnown = -1; + int knownCount = knownIndices.Count; + for (int i = 0; i <= knownCount; i++) + { + int nextKnown = i == knownCount ? maxIndex + 1 : knownIndices[i]; + if (i > 0 && nextKnown == knownIndices[i - 1]) + { + continue; + } + + int runStart = previousKnown + 1; + int runEnd = nextKnown - 1; + int runLength = runEnd - runStart + 1; + if (runLength >= bitsNeeded) + { + return false; + } + + for (int bitIndex = runStart; bitIndex <= runEnd; bitIndex++) + { + int shift = PowMod2((ulong)bitIndex, mod); + ulong shiftedMask; + if (shift == 0) + { + shiftedMask = reachableMask; + } + else + { + shiftedMask = ((reachableMask << shift) | (reachableMask >> (mod - shift))) & moduloMask; + } + + reachableMask |= shiftedMask; + if (IsResidueReachable(reachableMask, targetA)) + { + return false; + } + } + + previousKnown = nextKnown; + } + + return !IsResidueReachable(reachableMask, targetA); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void GetQPrefixMask(int startColumn, int qBitLen, int qWordCount, out int words, out ulong lastMask) + { + // We want only offsets t <= startColumn. + // start column is inclusive for maxT + if (startColumn >= qBitLen - 1) + { + words = qWordCount; + lastMask = ulong.MaxValue; // caller can still & lastWordMask separately + return; + } + + if (startColumn < 0) + { + words = 0; + lastMask = 0; + return; + } + + qBitLen = startColumn >> 6; + words = qBitLen + 1; + + qWordCount = startColumn & 63; + lastMask = qWordCount == 63 ? ulong.MaxValue : ((1UL << (qWordCount + 1)) - 1UL); + } + + private static void ComputeARangeFromTopConstraints( + long maxAllowedA, + bool top0KnownOne, + bool top0KnownZero, + bool top1KnownOne, + long zeroTailStart, + out BigInteger minA, + out BigInteger maxA) + { + _dynamicModChecks++; + if (zeroTailStart <= maxAllowedA + 1) + { + zeroTailStart--; + } + + // zeroTailStart is effectiveTop from here. We're reusing variable to limit registry pressure. + if (zeroTailStart < 0) + { + minA = BigInteger.Zero; + maxA = BigInteger.Zero; + return; + } + + int shift = zeroTailStart + 1L > int.MaxValue ? int.MaxValue : (int)(zeroTailStart + 1L); + maxA = Pow2Provider.BigIntegerMinusOne(shift); + minA = BigInteger.Zero; + + if (zeroTailStart == maxAllowedA) + { + if (top0KnownOne) + { + shift = maxAllowedA > int.MaxValue ? int.MaxValue : (int)maxAllowedA; + } + else if (top0KnownZero && top1KnownOne && maxAllowedA - 1L >= 0) + { + // zeroTailStart is index from here. We're reusing the variable to limit registry pressure. + zeroTailStart = maxAllowedA - 1L; + shift = zeroTailStart > int.MaxValue ? int.MaxValue : (int)zeroTailStart; + } + + minA = Pow2Provider.BigInteger(shift); + } + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void ComputeGuaranteedTopPrefixFromInterval( + in BigInteger qExact, + int qBitLen, + int maxAllowedA, + out int knownBits, + out ulong knownValue) + { + knownBits = 1; + knownValue = 1UL; + if (maxAllowedA <= 0) + { + return; + } + + int windowBits = TopPrefixProbeBits; + int maxBits = maxAllowedA + 1; + if (windowBits > maxBits) + { + windowBits = maxBits; + } + + if (windowBits <= 1) + { + return; + } + + BigInteger scaled = BigInteger.One << (qBitLen + windowBits - 1); + BigInteger prefixHighBig = scaled / qExact; + if (prefixHighBig <= BigInteger.Zero) + { + return; + } + + // prefixHighBig fits in windowBits (<= TopPrefixProbeBits), so ulong is sufficient. + ulong prefixHigh = (ulong)prefixHighBig; + ulong prefixLow = prefixHigh - 1UL; + ulong xor = prefixHigh ^ prefixLow; + int differingBits = xor == 0UL ? 0 : 64 - BitOperations.LeadingZeroCount(xor); + int commonBits = windowBits - differingBits; + if (commonBits < 1) + { + // MSB of a is still guaranteed by construction. + return; + } + + knownBits = commonBits; + int shift = windowBits - commonBits; + knownValue = shift == 0 ? prefixHigh : (prefixHigh >> shift); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool TryGetTopPrefixBitValue( + long maxAllowedA, + int topPrefixKnownBits, + ulong topPrefixValue, + long bitIndex, + out bool bitValue) + { + bitValue = false; + long offsetFromTop = maxAllowedA - bitIndex; + if (offsetFromTop < 0 || offsetFromTop >= topPrefixKnownBits) + { + return false; + } + + int shift = topPrefixKnownBits - 1 - (int)offsetFromTop; + bitValue = ((topPrefixValue >> shift) & 1UL) != 0UL; + return true; + } + + private static bool TryDynamicPrefixConsistencyPruneLarge( + long maxAllowedA, + bool top0KnownOne, + bool top0KnownZero, + bool top1KnownOne, + long zeroTailStart, + int topPrefixKnownBits, + ulong topPrefixValue) + { + if (topPrefixKnownBits <= 0) + { + return true; + } + + if (TryGetTopPrefixBitValue(maxAllowedA, topPrefixKnownBits, topPrefixValue, maxAllowedA, out bool top0PrefixValue)) + { + if ((top0KnownOne && !top0PrefixValue) || (top0KnownZero && top0PrefixValue)) + { + return false; + } + } + + long topIndex1 = maxAllowedA - 1; + if (topIndex1 >= 0 && top1KnownOne && + TryGetTopPrefixBitValue(maxAllowedA, topPrefixKnownBits, topPrefixValue, topIndex1, out bool top1PrefixValue) && !top1PrefixValue) + { + return false; + } + + if (zeroTailStart <= maxAllowedA) + { + long prefixMinIndex = maxAllowedA - topPrefixKnownBits + 1; + long start = zeroTailStart > prefixMinIndex ? zeroTailStart : prefixMinIndex; + for (long bitIndex = start; bitIndex <= maxAllowedA; bitIndex++) + { + if (TryGetTopPrefixBitValue(maxAllowedA, topPrefixKnownBits, topPrefixValue, bitIndex, out bool bitValue) && bitValue) + { + return false; + } + } + } + + return true; + } + + private static bool IsCleanInQ_Prefix(ulong[] qMask, ulong[] oneWin, ulong[] zeroWin, int words, ulong lastMask) + { + for (int i = 0; i < words; i++) + { + ulong q = qMask[i]; + if (i == words - 1) q &= lastMask; + if ((q & (oneWin[i] | zeroWin[i])) != 0) return false; + } + + return true; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool TryPruneWithQTimesAInterval( + in BigInteger qExact, + in BigInteger minA, + in BigInteger maxA, + ulong p) + { + if (minA > BigInteger.Zero) + { + long minProductBits = (qExact * minA).GetBitLength(); + if ((ulong)minProductBits > p) + { + return true; + } + } + + BigInteger maxProduct = qExact * maxA; + long maxProductBits = maxProduct.GetBitLength(); + if ((ulong)maxProductBits < p) + { + return true; + } + + if ((ulong)maxProductBits == p) + { + BigInteger plusOne = maxProduct + BigInteger.One; + if (!plusOne.IsPowerOfTwo) + { + return true; + } + } + + return false; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool TrySetGlobalKnownBit( + int aIndex, + bool valueOne, + HashSet knownOneIndices, + HashSet knownZeroIndices, + ref BigInteger globalMinA, + ref BigInteger globalMaxA) + { + if (aIndex < 0) + { + return true; + } + + if (valueOne) + { + if (knownZeroIndices.Contains(aIndex)) + { + return false; + } + + if (knownOneIndices.Add(aIndex)) + { + globalMinA += Pow2Provider.BigInteger(aIndex); + } + } + else + { + if (knownOneIndices.Contains(aIndex)) + { + return false; + } + + if (knownZeroIndices.Add(aIndex)) + { + globalMaxA -= Pow2Provider.BigInteger(aIndex); + } + } + + return true; + } + private static bool TryDynamicModularRangePrune( + ReadOnlySpan qOneOffsets, + long qHash, + in BigInteger qExact, + ulong p, + in BigInteger globalKnownMinA, + in BigInteger globalKnownMaxA, + HashSet globalKnownOneIndices, + HashSet globalKnownZeroIndices, + long maxAllowedA, + bool top0KnownOne, + bool top0KnownZero, + bool top1KnownOne, + long zeroTailStart, + int topPrefixKnownBits, + ulong topPrefixValue) + { + _dynamicModChecks++; + long effectiveTop = maxAllowedA; + if (zeroTailStart <= effectiveTop + 1) + { + effectiveTop = zeroTailStart - 1; + } + + if (globalKnownMinA > globalKnownMaxA) + { + _dynamicModFailures++; + return false; + } + + if (effectiveTop > 4096) + { + if (!TryDynamicPrefixConsistencyPruneLarge(maxAllowedA, top0KnownOne, top0KnownZero, top1KnownOne, zeroTailStart, topPrefixKnownBits, topPrefixValue)) + { + _dynamicModFailures++; +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTopPrefixRangeConflict); #endif - Console.WriteLine($"[bit-contradiction] Pruned with {nameof(GetAKnownStateRowAware)}, msbState=2, maxAllowedA={maxAllowedA}"); + return false; + } + + if (TryPruneWithQTimesAInterval(qExact, globalKnownMinA, globalKnownMaxA, p)) + { + _dynamicModFailures++; +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithQTimesAInterval); +#endif + return false; + } + + return true; + } + + ComputeARangeFromTopConstraints( + maxAllowedA, + top0KnownOne, + top0KnownZero, + top1KnownOne, + zeroTailStart, + out BigInteger minA, + out BigInteger maxA); + + if (topPrefixKnownBits > 0) + { + int shift = (int)(maxAllowedA + 1L - topPrefixKnownBits); + BigInteger prefixBase = new(topPrefixValue); + BigInteger prefixMin = prefixBase << shift; + BigInteger prefixMax = ((prefixBase + BigInteger.One) << shift) - BigInteger.One; + if (prefixMin > minA) + { + minA = prefixMin; + } + + if (prefixMax < maxA) + { + maxA = prefixMax; + } + + if (minA > maxA) + { + _dynamicModFailures++; +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTopPrefixRangeConflict); +#endif + return false; + } + } + + if (globalKnownMinA > minA) + { + minA = globalKnownMinA; + } + + if (globalKnownMaxA < maxA) + { + maxA = globalKnownMaxA; + } + + if (minA > maxA) + { + _dynamicModFailures++; + return false; + } + + if (TryPruneWithQTimesAInterval(qExact, minA, maxA, p)) + { + _dynamicModFailures++; +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithQTimesAInterval); +#endif + return false; + } + + int knownBitsModResidueModuliLength = KnownBitsModResidueModuli.Length; + for (int i = 0; i < knownBitsModResidueModuliLength; i++) + { + int mod = KnownBitsModResidueModuli[i]; + if (TryPruneWithKnownBitsModResidue(qOneOffsets, qHash, p, mod, maxAllowedA, globalKnownOneIndices, globalKnownZeroIndices)) + { + _dynamicModFailures++; +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithKnownBitsModResidue); +#endif + return false; + } + } + + int modLocalPrefilterModuliLength = ModLocalPrefilterModuli.Length; + for (int i = 0; i < modLocalPrefilterModuliLength; i++) + { + int mod = ModLocalPrefilterModuli[i]; + int qMod = GetQModCached(qOneOffsets, qHash, mod); + int target = ModPow2Minus1(p, mod); + if (qMod == 0) + { + if (target != 0) + { + return false; + } + continue; + } + + int inverse = ModPow(qMod, mod - 2, mod); + int aResidue = (int)((long)target * inverse % mod); + if (!ExistsCongruentInRange(minA, maxA, aResidue, mod)) + { + _dynamicModFailures++; + return false; + } + } + + return true; + } + + private static int ModPow2Minus1(ulong p, int mod) + { + int pow = PowMod2(p, mod); + int result = pow - 1; + return result < 0 ? result + mod : result; + } + + private static int PowMod2(ulong exp, int mod) + { + long result = 1; + long baseVal = 2; + ulong value = exp; + while (value > 0) + { + if ((value & 1) != 0) + { + result = (result * baseVal) % mod; + } + + baseVal = (baseVal * baseVal) % mod; + value >>= 1; + } + + return (int)result; + } + + private static int ModPow(int value, int exp, int mod) + { + long result = 1 % mod; + long baseVal = value % mod; + int e = exp; + while (e > 0) + { + if ((e & 1) != 0) + { + result = (result * baseVal) % mod; + } + + baseVal = (baseVal * baseVal) % mod; + e >>= 1; + } + + return (int)result; + } + + private enum CarryDropPruneReason : byte + { + None = 0, + ZeroDrop = 1, + Dominance67ThenZeroDrop = 2, + Dominance10AndMoreDrop = 3, + Dominance15161718Drop = 4, + DominanceReached10AndStayedAbove5 = 5, + Dominance1011121314 = 6, + } + + private static bool TryCarryDropHeuristicPrune( + ReadOnlySpan qOneOffsets, + int pLong, + int maxAllowedA, + ulong[] aBitsBuffer, + out CarryDropPruneReason pruneReason) + { + pruneReason = CarryDropPruneReason.None; + if (!EnableCarryDropHeuristic || maxAllowedA <= 0 || qOneOffsets[0] != 0) + { + return false; + } + + int bitLimit = maxAllowedA + 1; + if (bitLimit > pLong) + { + bitLimit = pLong; + } + + if (bitLimit > CarryDropHeuristicMaxBits) + { + bitLimit = CarryDropHeuristicMaxBits; + } + + if (bitLimit <= 1) + { + return false; + } + + int wordCount = (bitLimit + 63) >> 6; + if ((uint)wordCount > (uint)aBitsBuffer.Length) + { + return false; + } + + Array.Clear(aBitsBuffer, 0, wordCount); + + long carry = 0; + bool hadPositiveCarry = false; + int upperOffsetExclusive = 1; + int qOneOffsetsLength = qOneOffsets.Length; + + + int totalCarry67Count = 0, + totalCarry8Count = 0, + totalCarry9Count = 0, + totalCarry10Count = 0, + totalCarry11Count = 0, + totalCarry12Count = 0, + totalCarry13Count = 0, + totalCarry14Count = 0, + totalCarry15Count = 0;//, totalCarry16Count = 0, totalCarry17Count = 0, totalCarry18Count = 0; + int totalCarryOtherPositive67Count = 0, + // totalCarryOtherPositive8910OtherCount = 0, + totalCarryOtherPositive1011121314OtherCount = 0, + totalCarryOtherPositive15161718OtherCount = 0; + bool hadZeroBefore = false; + bool reached10 = false; + bool reachedBelow5 = false; + int reached5 = 0; + int zeroCount = 0; + for (int blockStart = 0; blockStart < bitLimit; blockStart += CarryDropHeuristicBlockBits) + { + int blockEnd = blockStart + CarryDropHeuristicBlockBits; + if (blockEnd > bitLimit) + { + blockEnd = bitLimit; + } + + int blockCarry67Count = 0; + int blockCarryOtherPositive67Count = 0; + + for (int col = blockStart; col < blockEnd; col++) + { + while (upperOffsetExclusive < qOneOffsetsLength && qOneOffsets[upperOffsetExclusive] <= col) + { + upperOffsetExclusive++; + } + + long sumWithoutCurrent = carry; + for (int i = 1; i < upperOffsetExclusive; i++) + { + int aIndex = col - qOneOffsets[i]; + ulong word = aBitsBuffer[aIndex >> 6]; + sumWithoutCurrent += (long)((word >> (aIndex & 63)) & 1UL); + } + + int aBit = (1 - ((int)sumWithoutCurrent & 1)) & 1; + if (aBit != 0) + { + aBitsBuffer[col >> 6] |= 1UL << (col & 63); + } + + long carryOut = (sumWithoutCurrent + aBit) >> 1; + if (carryOut == 6 || carryOut == 7) + { + blockCarry67Count++; + } + else if (carryOut > 0) + { + blockCarryOtherPositive67Count++; + } + + // if (carryOut == 8) + // { + // totalCarry8Count++; + // } + // else if (carryOut == 9) + // { + // totalCarry9Count++; + // } + // else + if (carryOut == 10) + { + if (!reached10) + { + reached10 = true; + } + + totalCarry10Count++; + } + else if (carryOut == 11) + { + totalCarry11Count++; + } + else if (carryOut == 12) + { + totalCarry12Count++; + } + else if (carryOut == 13) + { + totalCarry13Count++; + } + else if (carryOut == 14) + { + totalCarry14Count++; + } + else if (carryOut > 0) + { + // totalCarryOtherPositive8910OtherCount++; + totalCarryOtherPositive1011121314OtherCount++; + } + + if (reached10) + { + if (carryOut == 5) + { + reached5++; + } + else if (carryOut < 5) + { + reachedBelow5 = true; + } + } + + if (carryOut >= 15) + // if (carryOut == 15) + { + totalCarry15Count++; + } + // else if (carryOut == 16) + // { + // totalCarry16Count++; + // } + // else if (carryOut == 17) + // { + // totalCarry17Count++; + // } + // else if (carryOut == 18) + // { + // totalCarry18Count++; + // } + else if (carryOut > 0) + { + totalCarryOtherPositive15161718OtherCount++; + } + + if (hadPositiveCarry && carryOut == 0 && col < maxAllowedA) + { + if (hadZeroBefore) + { + pruneReason = CarryDropPruneReason.ZeroDrop; + return true; + } + + hadZeroBefore = true; + } + + if (carryOut == 0) + { + zeroCount++; + } + + if (carryOut > 0) + { + hadPositiveCarry = true; + } + + carry = carryOut; + } + + totalCarry67Count += blockCarry67Count; + totalCarryOtherPositive67Count += blockCarryOtherPositive67Count; + } + + if (reached10 && !reachedBelow5 && reached5 <= 1 && zeroCount <= 5) + { + pruneReason = CarryDropPruneReason.DominanceReached10AndStayedAbove5; + return true; + } + + if (totalCarry12Count > totalCarry10Count && totalCarry12Count > totalCarry11Count && + totalCarry12Count > totalCarry13Count && totalCarry12Count > totalCarry14Count && + totalCarry11Count > 100 && totalCarry13Count > 100 + ) + { + pruneReason = CarryDropPruneReason.Dominance1011121314; + return true; + } + + if (totalCarry67Count > totalCarryOtherPositive67Count) + { + pruneReason = CarryDropPruneReason.Dominance67ThenZeroDrop; + return true; + } + + if (totalCarry15Count /*+ totalCarry16Count + totalCarry17Count + totalCarry18Count */> totalCarryOtherPositive15161718OtherCount + // totalCarry16Count + totalCarry17Count >= totalCarry15Count + totalCarry18Count) + // totalCarry16Count >= 100 && totalCarry17Count >= 100 + // /* totalCarry15Count >= 100 &&*/ totalCarry16Count >= 150 && totalCarry17Count >= 150 /*&& totalCarry18Count >= 100*/ + ) + { + pruneReason = CarryDropPruneReason.Dominance15161718Drop; + return true; + } + + // if (totalCarry8Count + totalCarry9Count + totalCarry10Count > totalCarryOtherPositive8910OtherCount && + // totalCarry8Count >= 150 && totalCarry9Count >= 150 && totalCarry10Count >= 150) + // { + // pruneReason = CarryDropPruneReason.Dominance10AndMoreDrop; + // return true; + // } + + return false; + } + // internal static bool TryCheckDivisibilityFromDivisor(ulong q, ulong p, out bool divides, out ContradictionReason reason) + // { + // divides = false; + // if (q == 0UL) + // { + // reason = ContradictionReason.ParityUnreachable; + // return true; + // } + + // Span oneOffsets = stackalloc int[64]; + // int count = 0; + // ulong remaining = q; + // int baseIndex = 0; + // while (remaining != 0UL) + // { + // int tz = BitOperations.TrailingZeroCount(remaining); + // baseIndex += tz; + // oneOffsets[count++] = baseIndex; + // remaining >>= tz + 1; + // baseIndex++; + // } + + // return TryCheckDivisibilityFromOneOffsets(oneOffsets.Slice(0, count), p, out divides, out reason); + // } + + [ThreadStatic] + private static bool _initialized; + + public static void Initialize() + { + if (_initialized) + { + return; + } + + // _privateWorkSet = new(); + // _stableUnknownDelta8 = new(); + _initialized = true; + // Start with a small size and grow on demand. + _stableUnknownDelta8ByUnknown = new int[64][]; + _privateWorkSet = new PrivateWorkSet(); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static int ComputeForcedSumFromKnownPrefix( + ReadOnlySpan qOneOffsets, + int col, + ulong[] knownOne0) + { + int forced = 0; + + // qOneOffsets są rosnące; przerywamy gdy t>col (bo wtedy aIndex<0 => wkład 0) + for (int i = 0; i < qOneOffsets.Length; i++) + { + int t = qOneOffsets[i]; + if (t > col) break; + + int aIndex = col - t; // w prefiksie gwarantujemy 0 <= aIndex <= maxFixed + ulong word = knownOne0[aIndex >> 6]; + forced += (int)((word >> (aIndex & 63)) & 1UL); + } + + return forced; + } + + /// + /// Full column-wise propagation for a given set of q one-bit offsets (LSB=0) and exponent p. + /// Returns true if the solver could decide locally (divides or contradiction). + /// +#if DETAILED_LOG + internal static bool TryCheckDivisibilityFromOneOffsets( + ReadOnlySpan qOneOffsets, + ulong p, + BigInteger qExact, + BigInteger k, + bool isPowerOfTwo, + out bool divides, + out ContradictionReason reason) +#else + internal static bool TryCheckDivisibilityFromOneOffsets( + ReadOnlySpan qOneOffsets, + ulong p, + BigInteger qExact, + BigInteger k, + bool isPowerOfTwo, + out bool divides) +#endif + { + if (!_initialized) + { + Initialize(); + } + + PrivateWorkSet workSet = _privateWorkSet; + divides = false; + + // Dbg(p, k, $"[TGT] Enter solver. p={p} k={k} isPowerOfTwo={isPowerOfTwo}"); +#if DETAILED_LOG + _lastTopDownFailure = null; + _statStableAdvanceCalls = 0; + _statStableAdvanceCols = 0; + _statStableAdvanceColsBatched = 0; + _statScalarCols = 0; + _statDeltaRequests = 0; + _statDeltaHits = 0; + _statDeltaBuilds = 0; + _statStableAdvanceBigShift = 0; + _statCleanChecks = 0; + _statCleanFalse = 0; + _statFirstDirtyColumn = -1; +#endif + _dynamicModChecks = 0; + _dynamicModFailures = 0; + + // These conditions will never be true on EvenPerfectBitScanner execution path. + // if (p == 0 || qOneOffsets.Length == 0) + // { + // reason = ContradictionReason.ParityUnreachable; + // return true; + // } + + // While the scanner supports p >= 31, it's a tiny subset of all checked exponents. No need to support it. + // Exact small-case evaluation to short-circuit both success and failure deterministically. + // int highestBit = qOneOffsets[^1]; + // if (p <= 64 && highestBit < 63) + // { + // ulong q = 0; + // foreach (int bit in qOneOffsets) + // { + // q |= 1UL << bit; + // } + + // ulong mersenne = (1UL << (int)p) - 1UL; + // divides = q != 0 && (mersenne % q == 0); + // reason = divides ? ContradictionReason.None : ContradictionReason.ParityUnreachable; + // return true; + // } + + int qOneOffsetsLength = qOneOffsets.Length; + int qBitLen = qOneOffsets[qOneOffsetsLength - 1] + 1; + if ((ulong)qBitLen >= p) + { +#if DETAILED_LOG + reason = ContradictionReason.TruncatedLength; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTruncatedLength1); +#endif + return true; + } + + // q from EvenPerfectBitScanner will always have the correct 2kp+1 form. + // if (qOneOffsets[0] != 0) + // { + // reason = ContradictionReason.ParityUnreachable; + // return true; + // } + + int pLong = (int)p; + int maxAllowedA = pLong - qBitLen; + int carryDropBitLimit = maxAllowedA + 1; + if (carryDropBitLimit > pLong) + { + carryDropBitLimit = pLong; + } + + if (carryDropBitLimit > CarryDropHeuristicMaxBits) + { + carryDropBitLimit = CarryDropHeuristicMaxBits; + } + + int carryDropWordCount = (carryDropBitLimit + 63) >> 6; + workSet.EnsureCapacity(carryDropWordCount, 0); + ulong[] knownOne1 = workSet.KnownOne1; + Array.Clear(knownOne1, 0, carryDropWordCount); +#if false + Array.Clear(qMaskWords, 0, qWordCount); +#endif + +#if false + int segmentBase = 0; +#endif + if (maxAllowedA < 0) + { +#if DETAILED_LOG + reason = ContradictionReason.TruncatedLength; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTruncatedLength2); +#endif + return true; + } + + if (TryCarryDropHeuristicPrune(qOneOffsets, pLong, maxAllowedA, knownOne1, out CarryDropPruneReason carryDropPruneReason)) + { + divides = false; +#if WITH_PRUNE_STATS + if (carryDropPruneReason == CarryDropPruneReason.DominanceReached10AndStayedAbove5) + { + IncrementPruneCounter(ref _prunedWithCarryDominanceReached10AndStayedAbove5); + } + else if (carryDropPruneReason == CarryDropPruneReason.Dominance1011121314) + { + IncrementPruneCounter(ref _prunedWithCarryDominance1011121314); + } + else if (carryDropPruneReason == CarryDropPruneReason.Dominance67ThenZeroDrop) + { + IncrementPruneCounter(ref _prunedWithCarryDominance67); + } + else if (carryDropPruneReason == CarryDropPruneReason.Dominance10AndMoreDrop) + { + IncrementPruneCounter(ref _prunedWithCarryDominance8910); + } + else if (carryDropPruneReason == CarryDropPruneReason.Dominance15161718Drop) + { + IncrementPruneCounter(ref _prunedWithCarryDominance15161718); + } + else if (carryDropPruneReason == CarryDropPruneReason.ZeroDrop) + { + IncrementPruneCounter(ref _prunedWithCarryDropHeuristic); + } +#endif +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif +// #if WITH_PRUNE_STATS + ValidateHeuristicPruneAgainstPowmod2OrThrow(qExact, pLong, $"CarryDropHeuristic:{carryDropPruneReason}"); +// #endif + return true; + } +#if false + // Force low bits of 'a' from a ≡ -q^{-1} (mod 2^ForcedALowBits). + // This is a necessary condition for q | (2^p - 1) when p >= ForcedALowBits. + BigInteger mask = Pow2Provider.BigIntegerMinusOne(ForcedALowBits); + BigInteger qMod2k; + bool usedPow2Transform = false; + if (isPowerOfTwo && workSet.HasLastPow2QMod2k && workSet.LastPow2K != BigInteger.Zero && k == (workSet.LastPow2K << 1)) + { + qMod2k = ((workSet.LastPow2QMod2k << 1) - BigInteger.One) & mask; + usedPow2Transform = true; + } + else + { + qMod2k = BigInteger.Zero; + } + + byte[] qMod2kBytes = workSet.QMod2kBytes; + Span qPrefix = stackalloc ulong[16]; + int i, lastBit, t, index, forced, word; +#if false + ulong wordValue; +#endif + ulong[] bitMask64 = BitMask64; + if (usedPow2Transform) + { + for (i = 0; i < qOneOffsetsLength; i++) + { + t = qOneOffsets[i]; +#if false + qMaskWords[t >> 6] |= bitMask64[t & 63]; +#endif + if ((uint)t < 1024u) + { + qPrefix[t >> 6] |= bitMask64[t & 63]; + } + } + } + else + { + Array.Clear(qMod2kBytes, 0, qMod2kBytes.Length); + int currentByte = -1; + byte currentValue = 0; + for (i = 0; i < qOneOffsetsLength; i++) + { + t = qOneOffsets[i]; + if (t < ForcedALowBits) + { + // lastBit stand for lastByte here. We're reusing variable to limit registry pressure. + lastBit = t >> 3; + if (lastBit != currentByte) + { + if (currentByte >= 0) + { + qMod2kBytes[currentByte] = currentValue; + } + + currentByte = lastBit; + currentValue = 0; + } + + currentValue |= (byte)(1 << (t & 7)); + } + +#if false + qMaskWords[t >> 6] |= bitMask64[t & 63]; +#endif + if ((uint)t < 1024u) + { + qPrefix[t >> 6] |= bitMask64[t & 63]; + } + } + + if (currentByte >= 0) + { + qMod2kBytes[currentByte] = currentValue; + } + + qMod2k = new BigInteger(qMod2kBytes, isUnsigned: true, isBigEndian: false); + } + + ulong[] reversePrefix = workSet.LastQReverse; + GetReversePrefix1024(workSet, qPrefix, reversePrefix); +#if false + ulong[] lastPrefix = workSet.LastQPrefix; + for (i = 0; i < 16; i++) + { + lastPrefix[i] = qPrefix[i]; + } + + workSet.HasLastQPrefix1024 = true; +#endif + + // Compute inv = q^{-1} mod 2^ForcedALowBits using Hensel/Newton iteration in Z/2^kZ. + BigInteger[] invByKMod = workSet.InvByKMod; + bool[] hasInvByKMod = workSet.HasInvByKMod; + int kMod = (int)(k % ForcedALowBits); + BigInteger inv; + if (hasInvByKMod[kMod]) + { + inv = invByKMod[kMod]; + } + else if (workSet.HasLastInvMod2k) + { + inv = workSet.LastInvMod2k; + } + else + { + inv = qMod2k; + } + + BigInteger qTimesInvMod2k = (qMod2k * inv) & mask; + inv = (inv * (BigIntegerNumbers.Two - qTimesInvMod2k)) & mask; + qTimesInvMod2k = (qMod2k * inv) & mask; + inv = (inv * (BigIntegerNumbers.Two - qTimesInvMod2k)) & mask; + qTimesInvMod2k = (qMod2k * inv) & mask; + inv = (inv * (BigIntegerNumbers.Two - qTimesInvMod2k)) & mask; + + qTimesInvMod2k = (qMod2k * inv) & mask; + if (qTimesInvMod2k != BigInteger.One) + { + inv = qMod2k; + for (i = 0; i < 5; i++) + { + qTimesInvMod2k = (qMod2k * inv) & mask; + inv = (inv * (BigIntegerNumbers.Two - qTimesInvMod2k)) & mask; + qTimesInvMod2k = (qMod2k * inv) & mask; + inv = (inv * (BigIntegerNumbers.Two - qTimesInvMod2k)) & mask; + } + } + + BigInteger aLow = (-inv) & mask; + + if (isPowerOfTwo) + { + workSet.LastPow2QMod2k = qMod2k; + workSet.LastPow2K = k; + workSet.HasLastPow2QMod2k = true; + } + + workSet.LastInvMod2k = inv; + workSet.HasLastInvMod2k = true; + invByKMod[kMod] = inv; + hasInvByKMod[kMod] = true; + // a ≡ -aLow (mod 2^ForcedALowBits) + // Apply constraints for bits i in [0..min(ForcedALowBits-1, maxAllowedA)]. + Span aLowBytes = stackalloc byte[ForcedALowBits >> 3]; + if (!aLow.TryWriteBytes(aLowBytes, out int aLowBytesWritten, isUnsigned: true, isBigEndian: false)) + { + aLowBytesWritten = 0; + } + + int maxKnownA; + int maxFixed = maxAllowedA < (ForcedALowBits - 1) ? maxAllowedA : (ForcedALowBits - 1); + + if (maxFixed >= 0) + { + int numWordsToProcess = (maxFixed >> 6) + 1; + Array.Clear(knownOne0, 0, numWordsToProcess); + + int bytesToCopy = Math.Min(aLowBytesWritten, numWordsToProcess * 8); + if (bytesToCopy > 0) + { + System.Runtime.InteropServices.MemoryMarshal.Cast(aLowBytes.Slice(0, bytesToCopy)) + .CopyTo(new Span(knownOne0, 0, (bytesToCopy + 7) / 8)); + } + + i = 0; + if (Vector.IsHardwareAccelerated) + { + int limit = numWordsToProcess - (numWordsToProcess % Vector.Count); + for (; i < limit; i += Vector.Count) + { + var vKnownOne = new Vector(knownOne0, i); + (~vKnownOne).CopyTo(knownZero0, i); + } + } + for (; i < numWordsToProcess; i++) + { + knownZero0[i] = ~knownOne0[i]; + } + + int lastWordIndex = maxFixed >> 6; + int lastBitInWord = maxFixed & 63; + if (lastBitInWord < 63) + { + ulong finalMask = (1UL << (lastBitInWord + 1)) - 1UL; + knownOne0[lastWordIndex] &= finalMask; + knownZero0[lastWordIndex] &= finalMask; + } + } + + // We have learned bits up to maxFixed in the current segment. + maxKnownA = -1; + if (maxFixed > maxKnownA) + { + maxKnownA = maxFixed; + } + + CarryRange carryLow = CarryRange.Zero; + + // ------------------------------------------------------------ + // Cheap low-column prefilter (prefix-style): + // For the first N columns, all a-indices that contribute to the column are within + // the forced low-bit region (aLow). When every contributing bit is known (remaining==0), + // we can propagate carry deterministically and reject immediately on contradiction. + // This is significantly cheaper than entering the full row-aware window DP. + // ------------------------------------------------------------ + // maxFixed now serves as preMax. + maxFixed = 512 - 1; // 256..512 is a good trade-off; keep <= ForcedALowBits + if (maxFixed > maxKnownA) + { + maxFixed = maxKnownA; + } + + if (maxFixed > maxAllowedA) + { + maxFixed = maxAllowedA; + } + // Do NOT clamp to maxOffset: for columns above maxOffset the full set of q=1 positions + // still contributes, and aLow still fixes the corresponding a-bits. + + // Only run if we have at least a few columns to check. + if (false && maxFixed >= 8) + { + Span prefixMask = stackalloc ulong[16]; + // index is column here. We're reusing the variable to limit registry pressure. + for (index = 0; index <= maxFixed; index++) + { + // Required result bit for M_p in columns [0..p-1] is 1. + // Compute forced ones exactly: sum of a_{col - t} for all q_t=1 with t<=col. + forced = 0; + if (index <= 1023) + { + int shift = 1023 - index; + int wordShift = shift >> 6; + int bitShift = shift & 63; + for (word = 0; word < 16; word++) + { + int src = word + wordShift; + ulong value = 0; + if (src < 16) + { + value = reversePrefix[src] >> bitShift; + if (bitShift != 0 && src + 1 < 16) + { + value |= reversePrefix[src + 1] << (64 - bitShift); + } + } + + prefixMask[word] = value; + } + + forced = 0; + for (word = 0; word < 16; word++) + { + forced += PopCount(knownOne0[word] & prefixMask[word]); + } + } + else + { + for (i = 0; i < qOneOffsetsLength; i++) + { + t = qOneOffsets[i]; + if (t > index) + { + break; + } + + int aIndex = index - t; + // For this prefilter we only run where aIndex is guaranteed within [0..maxFixed]. + word = aIndex >> 6; + ulong m64 = bitMask64[aIndex & 63]; + if ((knownOne0[word] & m64) != 0) forced++; + } + } + + // remaining==0 here, so possible==forced. Propagate carry range deterministically. + if (!TryPropagateCarry(ref carryLow, forced, forced, 1)) + { + // reason = ContradictionReason.ParityUnreachable; + divides = false; + +#if DETAILED_LOG + Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryPropagateCarry)}, reversed prefix filter"); +#endif + +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTryPropagateCarry1); + ValidateHeuristicPruneAgainstPowmod2OrThrow(qExact, pLong, "TryPropagateCarry1"); +#endif + + return true; + } + } + } + +#endif + + #if false + // Disabled intentionally: all filters/calculations except TryPropagateCarry1, CarryDropHeuristic, Powmod2Tracked. + // Original block retained below for easy restore. + // ----------------------------- + // Force MSB of 'a' to be 1 (last row must be active => a has exact bit-length maxAllowedA+1) + // ----------------------------- + #endif + + // Active filters only: CarryDropHeuristic (above), Powmod2 zero-before-last-block, Powmod2Tracked (optimized). + if (TryGetPowmod2BlockStep(qExact, pLong, out int blockBits, out BigInteger blockResidue)) + { + divides = ComputePowmod2TrackedOptimizedWithZeroBeforeLastBlock( + pLong, + qExact, + blockBits, + blockResidue, + out bool prunedWithZeroBeforeLastBlock); + +#if WITH_PRUNE_STATS + if (!divides) + { + if (prunedWithZeroBeforeLastBlock) + { + IncrementPruneCounter(ref _prunedWithPowmod2ZeroBeforeLastBlock); + } + else + { + IncrementPruneCounter(ref _prunedWithPowmod2TrackedOptimized); + } + } +#endif + } + else + { + divides = BigInteger.ModPow(BigIntegerNumbers.Two, pLong, qExact) == BigInteger.One; +#if WITH_PRUNE_STATS + if (!divides) + { + IncrementPruneCounter(ref _prunedWithPowmod2Tracked); + } +#endif + } +#if DETAILED_LOG + reason = ContradictionReason.None; + PrintStats(); +#endif return true; } - if (msbState != 1) - { - SetAKnownRowAware(msbIndex, true, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); - - // DO NOT extend maxKnownA here: row-aware caches cover only segmentBase±windowSize. - // msbIndex is typically far outside current cached segments at this point. - // It has been temporarily enabled for validation. - // if (msbIndex > maxKnownA) maxKnownA = msbIndex; - } -} - - // carryLow now serves as main bottom-up carry. - int lowColumn = maxFixed + 1; // maxFixed == preMax po clampach - if (lowColumn < 0) lowColumn = 0; - - // var qHash = ComputeQOffsetsHash(qOneOffsets); - // if (!TryModularPrefilter(qOneOffsets, qHash, p, maxAllowedA)) - // { - // // reason = ContradictionReason.ParityUnreachable; - // return true; - // } - - // Ultra-cheap high-bit feasibility check based on the forced top carry-out (no bit beyond p-1). - // This is a tiny reverse-carry DP over the last few columns (p-1, p-2, ...), using only the - // geometric availability of contributions implied by qOneOffsets and maxAllowedA. - // It can reject entire classes of q with sparse/awkward high-bit structure before the full DP runs. #if DETAILED_LOG - if (!TryRunHighBitAndBorrowPrefiltersCombined(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA, out _lastTopDownFailure)) -#else - if (!TryRunHighBitAndBorrowPrefiltersCombined(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA)) -#endif - { -#if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; -#endif - Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryRunHighBitAndBorrowPrefiltersCombined)}, maxAllowedA={maxAllowedA}"); - return true; - } + internal static bool TryCheckDivisibilityFromOneOffsets( + ReadOnlySpan qOneOffsets, + ulong p, + BigInteger k, + bool isPowerOfTwo, + out bool divides, + out ContradictionReason reason) + => TryCheckDivisibilityFromOneOffsets(qOneOffsets, p, BuildQExact(qOneOffsets), k, isPowerOfTwo, out divides, out reason); -// ----------------------------- -// Prefix carry exact (skip DP from column 0) -// ----------------------------- -// We know bits a[0..maxFixed] exactly (from aLow). For any column col <= maxFixed, -// every contributing aIndex = col - t (for q_t=1 and t<=col) lies in [0..maxFixed], -// so the column sum is fully determined and we can propagate carry without DP. - - // Row-aware masks for q and a-window (supports q > 64 bits) - // wordValue now holds lastWordMask. - wordValue = (qBitLen & 63) == 0 ? ulong.MaxValue : (bitMask64[qBitLen & 63] - 1UL); - // Initialize window for column 0: mark negative a indices as zero (t>0). - // Sliding window over a: bit t corresponds to a_{column - t}. - ulong[] aOneWin = workSet.AOneWin; - ulong[] aZeroWin = workSet.AZeroWin; - Array.Clear(aOneWin, 0, qWordCount); - Array.Clear(aZeroWin, 0, qWordCount); - - - - -int windowColumn = lowColumn; -index = lowColumn; - -if (IsTargetCase(p, k)) -{ - Console.WriteLine($"[TGT] After prefix prefilter: maxFixed={maxFixed} lowColumn={lowColumn} carryLow=[{carryLow.Min},{carryLow.Max}] windowColumn={windowColumn} segmentBase={segmentBase}"); - if (windowColumn != lowColumn) - Console.WriteLine($"[TGT][WARN] windowColumn({windowColumn}) != lowColumn({lowColumn}) right after prefix stage"); -} - -// Build window for current lowColumn: bit t corresponds to a_{lowColumn - t} -Array.Clear(aOneWin, 0, qWordCount); -Array.Clear(aZeroWin, 0, qWordCount); - -int maxOffset = qOneOffsets[qOneOffsetsLength - 1]; -for (int step = 0; step <= maxOffset; step++) -{ - int aIndex = lowColumn - step; - int state = (aIndex < 0 || aIndex > maxAllowedA) - ? 2 - : GetAKnownStateRowAware(aIndex, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); - - if (state == 1) - aOneWin[step >> 6] |= 1UL << (step & 63); - else if (state == 2) - aZeroWin[step >> 6] |= 1UL << (step & 63); -} - -// Apply lastWordMask -if (qWordCount > 0) -{ - aOneWin[qWordCount - 1] &= wordValue; // wordValue u Ciebie to lastWordMask dla q - aZeroWin[qWordCount - 1] &= wordValue; -} - - // index now serves as lowColumn. - - - - int pLongMinus1 = pLong - 1; - int highColumn = pLongMinus1; - int bottomRunStart = 0; - int bottomRunEnd = 0; - -// if (ShouldRunTopDownBorrowPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA)) -// { -// if (IsTargetCase(p, k)) -// { -// Console.WriteLine("Running top down borrow prefilter"); -// } - -// #if DETAILED_LOG -// if (!TryTopDownBorrowPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA, out _lastTopDownFailure)) -// #else -// if (!TryTopDownBorrowPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA)) -// #endif -// { -// #if DETAILED_LOG -// reason = ContradictionReason.ParityUnreachable; -// #endif -// return true; -// } -// } -// else -// { -// if (IsTargetCase(p, k)) -// { -// Console.WriteLine("Top down borrow prefilter did NOT run"); -// } -// } - - - // ----------------------------- - // Option B mini ping-pong prefilter (chunk + reseed) - // ----------------------------- - int chunk = MiniPingPongPrefilterColumns; // Currently 60 - int maxDepth = chunk; // wymusza 1 iterację - if (maxDepth > highColumn) maxDepth = highColumn; - - int currentStartColumn = pLongMinus1; // We start from the very top (column p-1) - - for (int depth = chunk; depth <= maxDepth; depth += chunk) - { - int targetJ = pLong - depth; - if (targetJ <= 0 || targetJ > highColumn) break; - -if (IsTargetCase(p, k)) - Console.WriteLine($"[TGT] PP: before BU-to-J lowColumn={lowColumn} targetJ={targetJ} carry=[{carryLow.Min},{carryLow.Max}]"); - - // 1) Bottom-up DP only up to column J (process columns lowColumn..J-1). - while (lowColumn < targetJ) - { - int remaining = targetJ - lowColumn; - int blockSize = remaining < PingPongBlockColumns ? remaining : PingPongBlockColumns; - if (IsTargetCase(p, k)) - { - Console.WriteLine($"[DBG] call BU start={index} window={windowColumn} low={lowColumn}"); - Console.WriteLine($"[PP] entry low={lowColumn} targetJ={targetJ} carry=[{carryLow.Min},{carryLow.Max}] win={windowColumn}"); - } - - if (!TryProcessBottomUpBlockRowAware( - qOneOffsets, qMaskWords, qWordCount, wordValue, maxAllowedA, - lowColumn, blockSize, - ref carryLow, ref maxKnownA, ref segmentBase, - ref knownOne0, ref knownOne1, ref knownZero0, ref knownZero1, - windowSize, aWordCount, aOneWin, aZeroWin, ref windowColumn -#if DETAILED_LOG - ,out reason -#endif - )) - { - Console.WriteLine("Pruned with targetJ"); - return true; - } - - lowColumn += blockSize; - index = lowColumn; - windowColumn = lowColumn; - } - - if (IsTargetCase(p, k)) - { - Console.WriteLine($"[TGT] PP: after BU-to-J lowColumn={lowColumn} (expect {targetJ}) carry=[{carryLow.Min},{carryLow.Max}] windowColumn={windowColumn}"); - Console.WriteLine($"[PP] after BU-to-J low={lowColumn} (expect {targetJ}) carry=[{carryLow.Min},{carryLow.Max}] win={windowColumn}"); - } - - // 2) Top-down for exactly 'chunk' columns, seeded from previous intersection. - int stepsToJ = pLong - targetJ; // inclusive: columns (p-1 .. targetJ) - if (!TryHighBitCarryRangeToColumnJ( - qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA, - startColumn: pLongMinus1, - steps: stepsToJ, - startCarryOutMin: 0, - startCarryOutMax: 0, - out long topMin, out long topMax)) - { - // Treat as prune only if the function proves impossibility; - // if it "disabled filtering" it should return true with wide range. - return true; - } - - // 3) Intersect with bottom-up carry at the SAME targetJ. - long interMin = carryLow.Min > topMin ? carryLow.Min : topMin; - long interMax = carryLow.Max < topMax ? carryLow.Max : topMax; - if (IsTargetCase(p, k)) - { - Console.WriteLine($"[PP] TD=[{topMin},{topMax}] BU=[{carryLow.Min},{carryLow.Max}] -> inter=[{interMin},{interMax}]"); - } - - if (interMin > interMax) - { - Console.WriteLine("Pruned with interMin > interMax"); - // reason = ContradictionReason.ParityUnreachable; - return true; - } - - if (IsTargetCase(p, k)) - Console.WriteLine($"[TGT] PP: top=[{topMin},{topMax}] inter=[{interMin},{interMax}] carryBefore=[{carryLow.Min},{carryLow.Max}]"); - - // 4) Reseed for the next chunk: carryOut above next block is our intersection. - // seedMin = interMin; - // seedMax = interMax; - - // Next chunk starts right above the current targetJ. - // currentStartColumn = targetJ - 1; - - // Also tighten carryLow (optional but consistent). - carryLow = new CarryRange(interMin, interMax); - - // Safety: if we fell off the bottom, stop. - if (currentStartColumn < 0) break; - } - - // ----------------------------- - // Continue full bottom-up DP for remaining columns - // ----------------------------- - index = lowColumn; - windowColumn = lowColumn; - while (index <= highColumn) - { - int remaining = highColumn - index + 1; - int blockSize = remaining < PingPongBlockColumns ? remaining : PingPongBlockColumns; - if (IsTargetCase(p, k)) - { - Console.WriteLine($"[DBG] call BU start={index} window={windowColumn} low={lowColumn}"); - } - -#if DETAILED_LOG - if (!TryProcessBottomUpBlockRowAware( - qOneOffsets, qMaskWords, qWordCount, wordValue, maxAllowedA, - index, blockSize, - ref carryLow, ref maxKnownA, ref segmentBase, - ref knownOne0, ref knownOne1, ref knownZero0, ref knownZero1, - windowSize, aWordCount, aOneWin, aZeroWin, ref windowColumn, - out reason)) -#else - if (!TryProcessBottomUpBlockRowAware( - qOneOffsets, qMaskWords, qWordCount, wordValue, maxAllowedA, - index, blockSize, - ref carryLow, ref maxKnownA, ref segmentBase, - ref knownOne0, ref knownOne1, ref knownZero0, ref knownZero1, - windowSize, aWordCount, aOneWin, aZeroWin, ref windowColumn)) -#endif - { -#if DETAILED_LOG - PrintStats(); -#endif - - Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryProcessBottomUpBlockRowAware)}, index={index}, maxAllowedA={maxAllowedA}"); - return true; - } - - index += blockSize; - } - - // long carryMin = carryLow.Min > carryHigh.Min ? carryLow.Min : carryHigh.Min; - // long carryMax = carryLow.Max < carryHigh.Max ? carryLow.Max : carryHigh.Max; - // if (carryMin > carryMax) - // { - // divides = false; - // reason = ContradictionReason.ParityUnreachable; - // return true; - // } - - // if (_debugEnabled) - // { - // Console.WriteLine($"[bit-contradiction] AMultiplier dynamic-mod checks={_dynamicModChecks} failures={_dynamicModFailures}"); - // } - - divides = carryLow.Min == 0; - if (divides) - { - ulong qLow = BuildQLow64(qOneOffsets); - if ((qLow & 1UL) == 0UL) - { - divides = false; - } - else - { - BigInteger qExact = new BigInteger(qLow); - if (BigInteger.ModPow(2, (int)p, qExact) != BigInteger.One) - { - divides = false; - Console.WriteLine($"We indicated that k={k} divides p={p}, but powmod2 proved otherwise"); - } - } - } -#if DETAILED_LOG - reason = ContradictionReason.None; - PrintStats(); -#endif - return true; - } - -#if DETAILED_LOG - internal static bool TryCheckDivisibilityFromOneOffsets( - ReadOnlySpan qOneOffsets, - ulong p, - out bool divides) => TryCheckDivisibilityFromOneOffsets(qOneOffsets, p, BigInteger.Zero, false, out divides, out _); + internal static bool TryCheckDivisibilityFromOneOffsets( + ReadOnlySpan qOneOffsets, + ulong p, + out bool divides) + => TryCheckDivisibilityFromOneOffsets(qOneOffsets, p, BuildQExact(qOneOffsets), BigInteger.Zero, false, out divides, out _); #endif #if !DETAILED_LOG - internal static bool TryCheckDivisibilityFromOneOffsets( - ReadOnlySpan qOneOffsets, - ulong p, - out bool divides) => TryCheckDivisibilityFromOneOffsets(qOneOffsets, p, BigInteger.Zero, false, out divides); + internal static bool TryCheckDivisibilityFromOneOffsets( + ReadOnlySpan qOneOffsets, + ulong p, + BigInteger k, + bool isPowerOfTwo, + out bool divides) + => TryCheckDivisibilityFromOneOffsets(qOneOffsets, p, BuildQExact(qOneOffsets), k, isPowerOfTwo, out divides); + + internal static bool TryCheckDivisibilityFromOneOffsets( + ReadOnlySpan qOneOffsets, + ulong p, + out bool divides) + => TryCheckDivisibilityFromOneOffsets(qOneOffsets, p, BuildQExact(qOneOffsets), BigInteger.Zero, false, out divides); #endif - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static ulong BuildQLow64(ReadOnlySpan qOneOffsets) - { - ulong q = 0; - for (int i = 0; i < qOneOffsets.Length; i++) - { - int bit = qOneOffsets[i]; - if ((uint)bit >= 64u) break; - q |= 1UL << bit; - } - return q; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool TryGetPowmod2BlockStep(in BigInteger modulus, int exponent, out int blockBits, out BigInteger blockResidue) + { + // blockBits = 0; + // blockResidue = BigInteger.Zero; + // if (modulus <= BigInteger.One) + // { + // return false; + // } - /// - /// Modular inverse of odd q modulo 2^64. - /// Uses Newton/Hensel lifting: x_{k+1} = x_k * (2 - q*x_k) mod 2^64. - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static ulong ModInversePow2_64(ulong qOdd) - { - // qOdd must be odd. - // Start with x ≡ 1 (mod 2). A common fast seed is x = qOdd. - // Each iteration doubles correct bits. 6 iterations are enough for 64 bits: 1->2->4->8->16->32->64. - unchecked - { - qOdd *= 2UL - qOdd * qOdd; - qOdd *= 2UL - qOdd * qOdd; - qOdd *= 2UL - qOdd * qOdd; - qOdd *= 2UL - qOdd * qOdd; - qOdd *= 2UL - qOdd * qOdd; - qOdd *= 2UL - qOdd * qOdd; - } + // long blockBitsLong = modulus.GetBitLength(); + // if (blockBitsLong <= 0 || blockBitsLong > int.MaxValue) + // { + // return false; + // } - return qOdd; - } + // blockBits = (int)blockBitsLong; + // if (exponent > blockBits * Powmod2AdaptiveMinRatio) + // { + // int adaptiveBits = (exponent + Powmod2AdaptiveTargetBlocks - 1) / Powmod2AdaptiveTargetBlocks; + // if (adaptiveBits > blockBits) + // { + // blockBits = adaptiveBits; + // } + blockBits = 262_144; + // } - [MethodImpl(MethodImplOptions.AggressiveInlining | MethodImplOptions.AggressiveOptimization)] - private static bool TryAdvanceZeroColumns(ref CarryRange carry, int columnCount) - { - const int Step = 30; - long carryMin = carry.Min; - long carryMax = carry.Max; - int add; - while (columnCount >= Step) - { - add = (1 << Step) - 1; - carryMin = (carryMin + add) >> Step; - carryMax >>= Step; - if (carryMin > carryMax) - { - return false; - } + blockResidue = Pow2Provider.BigInteger(blockBits) % modulus; + // blockResidue = BigInteger.ModPow(BigIntegerNumbers.Two, blockBits, modulus); + return true; + } - columnCount -= Step; - } - if (columnCount > 0) - { - add = (1 << columnCount) - 1; - carryMin = (carryMin + add) >> columnCount; - carryMax >>= columnCount; - if (carryMin > carryMax) - { - return false; - } - } - carry = new CarryRange(carryMin, carryMax); - return true; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool ComputePowmod2TrackedOptimizedWithZeroBeforeLastBlock( + int exponent, + in BigInteger modulus, + int blockBits, + in BigInteger blockResidue, + out bool prunedWithZeroBeforeLastBlock) + { + prunedWithZeroBeforeLastBlock = false; - // [ThreadStatic] - // private static Dictionary _stableUnknownDelta8; + int fullBlocks = exponent / blockBits; + int fullBlocksMinusOne = fullBlocks - 1; + int tailBits = exponent - (fullBlocks * blockBits); - // Indexed by "unknown" (usually qOneOffsetsLength). Elements are lazy initialized. - private static volatile int[][]? _stableUnknownDelta8ByUnknown; + BigInteger residue = BigInteger.One; + for (int i = 0; i < fullBlocks; i++) + { + residue *= blockResidue; + if (residue >= modulus) + { + residue %= modulus; + } - private static int[] GetStableUnknownDelta(int unknown) - { + if (i < fullBlocksMinusOne && residue.IsZero) + { + prunedWithZeroBeforeLastBlock = true; + return false; + } + } + + if (tailBits > 0) + { + BigInteger tailResidue = Pow2Provider.BigInteger(tailBits) % modulus; + // BigInteger tailResidue = BigInteger.ModPow(BigIntegerNumbers.Two, tailBits, modulus); + residue *= tailResidue; + if (residue >= modulus) + { + residue %= modulus; + } + } + + return residue == BigInteger.One; + } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + internal static bool ShouldPruneWithFinalPow2Shift(BigInteger prefixResidue, BigInteger modulus, int tailShift) + { + if (tailShift <= 0) + { + return false; + } + + if (prefixResidue == BigInteger.One) + { + return false; + } + + return (prefixResidue << tailShift) < modulus; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void AdvancePow2Residue( + ref BigInteger residue, + int delta, + in BigInteger modulus, + ref int cachedDelta, + ref BigInteger cachedPow2Delta) + { + if (delta <= 0) + { + return; + } + + if (cachedDelta != delta) + { + cachedPow2Delta = BigInteger.ModPow(BigIntegerNumbers.Two, delta, modulus); + cachedDelta = delta; + } + + residue = (residue * cachedPow2Delta) % modulus; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static BigInteger BuildQExact(ReadOnlySpan qOneOffsets) + { + BigInteger q = BigInteger.Zero; + for (int i = 0; i < qOneOffsets.Length; i++) + { + q |= BigInteger.One << qOneOffsets[i]; + } + + return q; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static ulong BuildQLow64(ReadOnlySpan qOneOffsets) + { + ulong q = 0; + for (int i = 0; i < qOneOffsets.Length; i++) + { + int bit = qOneOffsets[i]; + if ((uint)bit >= 64u) break; + q |= 1UL << bit; + } + return q; + } + + /// + /// Modular inverse of odd q modulo 2^64. + /// Uses Newton/Hensel lifting: x_{k+1} = x_k * (2 - q*x_k) mod 2^64. + /// + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static ulong ModInversePow2_64(ulong qOdd) + { + // qOdd must be odd. + // Start with x ≡ 1 (mod 2). A common fast seed is x = qOdd. + // Each iteration doubles correct bits. 6 iterations are enough for 64 bits: 1->2->4->8->16->32->64. + unchecked + { + qOdd *= 2UL - qOdd * qOdd; + qOdd *= 2UL - qOdd * qOdd; + qOdd *= 2UL - qOdd * qOdd; + qOdd *= 2UL - qOdd * qOdd; + qOdd *= 2UL - qOdd * qOdd; + qOdd *= 2UL - qOdd * qOdd; + } + + return qOdd; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining | MethodImplOptions.AggressiveOptimization)] + private static bool TryAdvanceZeroColumns(ref CarryRange carry, int columnCount) + { + const int Step = 30; + long carryMin = carry.Min; + long carryMax = carry.Max; + int add; + while (columnCount >= Step) + { + add = (1 << Step) - 1; + carryMin = (carryMin + add) >> Step; + carryMax >>= Step; + if (carryMin > carryMax) + { + return false; + } + + columnCount -= Step; + } + + if (columnCount > 0) + { + add = (1 << columnCount) - 1; + carryMin = (carryMin + add) >> columnCount; + carryMax >>= columnCount; + if (carryMin > carryMax) + { + return false; + } + } + + carry = new CarryRange(carryMin, carryMax); + return true; + } + + // [ThreadStatic] + // private static Dictionary _stableUnknownDelta8; + + // Indexed by "unknown" (usually qOneOffsetsLength). Elements are lazy initialized. + private static volatile int[][]? _stableUnknownDelta8ByUnknown; + + private static int[] GetStableUnknownDelta(int unknown) + { #if DETAILED_LOG - _statDeltaRequests++; + _statDeltaRequests++; #endif - // Lazily allocate the outer array. Keep it volatile to publish safely. - int[][] cache = _stableUnknownDelta8ByUnknown!; + // Lazily allocate the outer array. Keep it volatile to publish safely. + int[][] cache = _stableUnknownDelta8ByUnknown!; - // Ensure capacity for this "unknown". - int cacheLength = cache.Length, - parity; + // Ensure capacity for this "unknown". + int cacheLength = cache.Length, + parity; - if ((uint)unknown >= (uint)cacheLength) - { - // Grow to at least unknown+1, doubling for amortized O(1). parity means newLength here - we're reusing variable to limit registry pressure. - parity = cacheLength; - while (parity <= unknown) parity <<= 1; + if ((uint)unknown >= (uint)cacheLength) + { + // Grow to at least unknown+1, doubling for amortized O(1). parity means newLength here - we're reusing variable to limit registry pressure. + parity = cacheLength; + while (parity <= unknown) parity <<= 1; - var newCache = new int[parity][]; - Array.Copy(cache, newCache, cacheLength); + var newCache = new int[parity][]; + Array.Copy(cache, newCache, cacheLength); - // Publish the grown cache (racy publish is OK; contents are immutable after creation). - _stableUnknownDelta8ByUnknown = newCache; - cache = newCache; - } + // Publish the grown cache (racy publish is OK; contents are immutable after creation). + _stableUnknownDelta8ByUnknown = newCache; + cache = newCache; + } - // Fast path: already computed. - var cached = cache[unknown]; - if (cached != null) - { + // Fast path: already computed. + var cached = cache[unknown]; + if (cached != null) + { #if DETAILED_LOG - _statDeltaHits++; + _statDeltaHits++; #endif - return cached; - } + return cached; + } - // Compute. - const int PrefixLength = 1 << ColumnsAtOnce; - int[] delta = new int[PrefixLength]; + // Compute. + const int PrefixLength = 1 << ColumnsAtOnce; + int[] delta = new int[PrefixLength]; - for (int low = 0; low < PrefixLength; low++) - { - long value = low; + for (int low = 0; low < PrefixLength; low++) + { + long value = low; - // 16 iterations correspond to processing 16 columns at once. It was slower with: 32, 128, 1024 and rolled. - for (int i = 0; i < ColumnsAtOnce; i += 4) - { - parity = (int)(value & 1L); - int sMax = (((unknown ^ parity) & 1) != 0) ? unknown : (unknown - 1); - value = (value + sMax - 1) >> 1; + // 16 iterations correspond to processing 16 columns at once. It was slower with: 32, 128, 1024 and rolled. + for (int i = 0; i < ColumnsAtOnce; i += 4) + { + parity = (int)(value & 1L); + int sMax = (((unknown ^ parity) & 1) != 0) ? unknown : (unknown - 1); + value = (value + sMax - 1) >> 1; - parity = (int)(value & 1L); - sMax = (((unknown ^ parity) & 1) != 0) ? unknown : (unknown - 1); - value = (value + sMax - 1) >> 1; + parity = (int)(value & 1L); + sMax = (((unknown ^ parity) & 1) != 0) ? unknown : (unknown - 1); + value = (value + sMax - 1) >> 1; - parity = (int)(value & 1L); - sMax = (((unknown ^ parity) & 1) != 0) ? unknown : (unknown - 1); - value = (value + sMax - 1) >> 1; + parity = (int)(value & 1L); + sMax = (((unknown ^ parity) & 1) != 0) ? unknown : (unknown - 1); + value = (value + sMax - 1) >> 1; - parity = (int)(value & 1L); - sMax = (((unknown ^ parity) & 1) != 0) ? unknown : (unknown - 1); - value = (value + sMax - 1) >> 1; - } + parity = (int)(value & 1L); + sMax = (((unknown ^ parity) & 1) != 0) ? unknown : (unknown - 1); + value = (value + sMax - 1) >> 1; + } - delta[low] = (int)((value << ColumnsAtOnce) - low); - } + delta[low] = (int)((value << ColumnsAtOnce) - low); + } #if DETAILED_LOG - _statDeltaBuilds++; + _statDeltaBuilds++; #endif - // Publish into cache. If a race computes it twice, that's acceptable (same deterministic result). - cache[unknown] = delta; - return delta; - } + // Publish into cache. If a race computes it twice, that's acceptable (same deterministic result). + cache[unknown] = delta; + return delta; + } - // private static int[] GetStableUnknownDelta8(int unknown) - // { - // var stableUnknownDelta8Cache = _stableUnknownDelta8; - // if (stableUnknownDelta8Cache.TryGetValue(unknown, out int[]? cached)) - // { - // return cached!; - // } + // private static int[] GetStableUnknownDelta8(int unknown) + // { + // var stableUnknownDelta8Cache = _stableUnknownDelta8; + // if (stableUnknownDelta8Cache.TryGetValue(unknown, out int[]? cached)) + // { + // return cached!; + // } - // const int PrefixLength = 131072; - // int[] delta = new int[PrefixLength]; - // for (int low = 0; low < PrefixLength; low++) - // { - // long value = low; - // for (int i = 0; i < 8; i++) - // { - // int sMax = (((unknown ^ (int)value) & 1) != 0) ? unknown : unknown - 1; - // value = (value + sMax - 1) >> 1; - // } + // const int PrefixLength = 131072; + // int[] delta = new int[PrefixLength]; + // for (int low = 0; low < PrefixLength; low++) + // { + // long value = low; + // for (int i = 0; i < 8; i++) + // { + // int sMax = (((unknown ^ (int)value) & 1) != 0) ? unknown : unknown - 1; + // value = (value + sMax - 1) >> 1; + // } - // delta[low] = (int)((value << 8) - low); - // } + // delta[low] = (int)((value << 8) - low); + // } - // stableUnknownDelta8Cache[unknown] = delta; - // return delta; - // } + // stableUnknownDelta8Cache[unknown] = delta; + // return delta; + // } - const int ColumnsAtOnce = 20; + const int ColumnsAtOnce = 20; #if DETAILED_LOG - private static bool TryAdvanceStableUnknown(ref CarryRange carry, int unknown, int columnCount, out ContradictionReason reason) + private static bool TryAdvanceStableUnknown(ref CarryRange carry, int unknown, int columnCount, out ContradictionReason reason) #else - private static bool TryAdvanceStableUnknown(ref CarryRange carry, int unknown, int columnCount) + private static bool TryAdvanceStableUnknown(ref CarryRange carry, int unknown, int columnCount) #endif - { + { #if DETAILED_LOG - _statStableAdvanceCalls++; - _statStableAdvanceCols += columnCount; - if (columnCount >= 64) _statStableAdvanceBigShift++; + _statStableAdvanceCalls++; + _statStableAdvanceCols += columnCount; + if (columnCount >= 64) _statStableAdvanceBigShift++; #endif - if (columnCount <= 0) - { + if (columnCount <= 0) + { #if DETAILED_LOG - reason = ContradictionReason.None; - _statStableAdvanceColsBatched += columnCount; + reason = ContradictionReason.None; + _statStableAdvanceColsBatched += columnCount; #endif - return true; - } + return true; + } - if (unknown <= 0) - { - if (!TryAdvanceZeroColumns(ref carry, columnCount)) - { + if (unknown <= 0) + { + if (!TryAdvanceZeroColumns(ref carry, columnCount)) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } + return false; + } #if DETAILED_LOG - _statStableAdvanceColsBatched += columnCount; - reason = ContradictionReason.None; + _statStableAdvanceColsBatched += columnCount; + reason = ContradictionReason.None; #endif - return true; - } + return true; + } - long carryMin = columnCount >= 63 ? 0 : (carry.Min >> columnCount); - long carryMax = carry.Max; - int remaining = columnCount; - int[] delta = GetStableUnknownDelta(unknown); + long carryMin = columnCount >= 63 ? 0 : (carry.Min >> columnCount); + long carryMax = carry.Max; + int remaining = columnCount; + int[] delta = GetStableUnknownDelta(unknown); - const long CarryDecimalMask = (1L << ColumnsAtOnce) - 1L; - int carryMask; - while (remaining >= ColumnsAtOnce) - { - carryMask = (int)(carryMax & CarryDecimalMask); - carryMax = (carryMax + delta[carryMask]) >> ColumnsAtOnce; - remaining -= ColumnsAtOnce; - } + const long CarryDecimalMask = (1L << ColumnsAtOnce) - 1L; + int carryMask; + while (remaining >= ColumnsAtOnce) + { + carryMask = (int)(carryMax & CarryDecimalMask); + carryMax = (carryMax + delta[carryMask]) >> ColumnsAtOnce; + remaining -= ColumnsAtOnce; + } - while (remaining > 0) - { - // carryMask is sMax here. We're reusing variable to limit registry pressure. - carryMask = (((unknown ^ (int)carryMax) & 1) != 0) ? unknown : unknown - 1; - carryMax = (carryMax + carryMask - 1) >> 1; - remaining--; - } + while (remaining > 0) + { + // carryMask is sMax here. We're reusing variable to limit registry pressure. + carryMask = (((unknown ^ (int)carryMax) & 1) != 0) ? unknown : unknown - 1; + carryMax = (carryMax + carryMask - 1) >> 1; + remaining--; + } - if (carryMax < carryMin) - { + if (carryMax < carryMin) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } + return false; + } #if DETAILED_LOG - _statStableAdvanceColsBatched += columnCount; - reason = ContradictionReason.None; + _statStableAdvanceColsBatched += columnCount; + reason = ContradictionReason.None; #endif - carry = new CarryRange(carryMin, carryMax); - return true; - } + carry = new CarryRange(carryMin, carryMax); + return true; + } - // ----------------------------- - // Row-aware bottom-up block processing - // ----------------------------- - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void ShiftLeft1InPlace(ulong[] wordsOne, ulong[] wordsZero, int wordCount, ulong lastWordMask) - { - if (wordCount > 0) - { - ulong carryOne = 0, - carryZero = 0; + // ----------------------------- + // Row-aware bottom-up block processing + // ----------------------------- + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void ShiftLeft1InPlace(ulong[] wordsOne, ulong[] wordsZero, int wordCount, ulong lastWordMask) + { + if (wordCount > 0) + { + ulong carryOne = 0, + carryZero = 0; - for (int i = 0; i < wordCount; i++) - { - ulong w = wordsOne[i]; - wordsOne[i] = (w << 1) | carryOne; - carryOne = w >> 63; + for (int i = 0; i < wordCount; i++) + { + ulong w = wordsOne[i]; + wordsOne[i] = (w << 1) | carryOne; + carryOne = w >> 63; - w = wordsZero[i]; - wordsZero[i] = (w << 1) | carryZero; - carryZero = w >> 63; - } + w = wordsZero[i]; + wordsZero[i] = (w << 1) | carryZero; + carryZero = w >> 63; + } - wordCount--; - wordsOne[wordCount] &= lastWordMask; - wordsZero[wordCount] &= lastWordMask; - } - } + wordCount--; + wordsOne[wordCount] &= lastWordMask; + wordsZero[wordCount] &= lastWordMask; + } + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static bool AnyAndNonZero(ulong[] a, ulong[] b, int wordCount) - { - for (int i = 0; i < wordCount; i++) - { - if ((a[i] & b[i]) != 0) return true; - } - return false; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool AnyAndNonZero(ulong[] a, ulong[] b, int wordCount) + { + for (int i = 0; i < wordCount; i++) + { + if ((a[i] & b[i]) != 0) return true; + } + return false; + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static int PopCountAnd(ulong[] a, ulong[] b, int wordCount) - { - int c = 0; - for (int i = 0; i < wordCount; i++) - { - c += BitOperations.PopCount(a[i] & b[i]); - } - return c; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static int PopCountAnd(ulong[] a, ulong[] b, int wordCount) + { + int c = 0; + for (int i = 0; i < wordCount; i++) + { + c += BitOperations.PopCount(a[i] & b[i]); + } + return c; + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static int PopCountUnknownInQ(ulong[] qMask, ulong[] oneWin, ulong[] zeroWin, int wordCount) - { - int c = 0; - for (int i = 0; i < wordCount; i++) - { - ulong known = oneWin[i] | zeroWin[i]; - ulong unkQ = qMask[i] & ~known; - c += BitOperations.PopCount(unkQ); - } - return c; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static int PopCountUnknownInQ(ulong[] qMask, ulong[] oneWin, ulong[] zeroWin, int wordCount) + { + int c = 0; + for (int i = 0; i < wordCount; i++) + { + ulong known = oneWin[i] | zeroWin[i]; + ulong unkQ = qMask[i] & ~known; + c += BitOperations.PopCount(unkQ); + } + return c; + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static bool TryFindSingleUnknownInQ(ulong[] qMask, ulong[] oneWin, ulong[] zeroWin, int wordCount, out int offset) - { - // Returns true if exactly one unknown bit among positions where q has 1. - offset = -1; - int found = 0; - for (int w = 0; w < wordCount; w++) - { - ulong known = oneWin[w] | zeroWin[w]; - ulong unk = qMask[w] & ~known; - if (unk == 0) - { - continue; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool TryFindSingleUnknownInQ(ulong[] qMask, ulong[] oneWin, ulong[] zeroWin, int wordCount, out int offset) + { + // Returns true if exactly one unknown bit among positions where q has 1. + offset = -1; + int found = 0; + for (int w = 0; w < wordCount; w++) + { + ulong known = oneWin[w] | zeroWin[w]; + ulong unk = qMask[w] & ~known; + if (unk == 0) + { + continue; + } - int pc = BitOperations.PopCount(unk); - found += pc; - if (found > 1) - { - return false; - } + int pc = BitOperations.PopCount(unk); + found += pc; + if (found > 1) + { + return false; + } - int bit = BitOperations.TrailingZeroCount(unk); - offset = (w << 6) + bit; - } + int bit = BitOperations.TrailingZeroCount(unk); + offset = (w << 6) + bit; + } - return found == 1; - } + return found == 1; + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static int GetAKnownStateRowAware( - int aIndex, - int segmentBase, - int windowSize, - in ulong[] knownOne0, - in ulong[] knownZero0, - in ulong[] knownOne1, - in ulong[] knownZero1) - { - // 0 unknown, 1 one, 2 zero - if (aIndex < 0) - { - return 2; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static int GetAKnownStateRowAware( + int aIndex, + int segmentBase, + int windowSize, + in ulong[] knownOne0, + in ulong[] knownZero0, + in ulong[] knownOne1, + in ulong[] knownZero1) + { + // 0 unknown, 1 one, 2 zero + if (aIndex < 0) + { + return 2; + } - int rel, w; - ulong m; - if (aIndex >= segmentBase && aIndex < segmentBase + windowSize) - { - rel = aIndex - segmentBase; - w = rel >> 6; - m = 1UL << (rel & 63); - rel = (knownOne0[w] & m) != 0 ? 1 : - (knownZero0[w] & m) != 0 ? 2 : - 0; + int rel, w; + ulong m; + if (aIndex >= segmentBase && aIndex < segmentBase + windowSize) + { + rel = aIndex - segmentBase; + w = rel >> 6; + m = 1UL << (rel & 63); + rel = (knownOne0[w] & m) != 0 ? 1 : + (knownZero0[w] & m) != 0 ? 2 : + 0; - return rel; - } + return rel; + } - w = segmentBase - windowSize; - if (aIndex >= w && aIndex < segmentBase) - { - rel = aIndex - w; - w = rel >> 6; - m = 1UL << (rel & 63); - rel = (knownOne1[w] & m) != 0 ? 1 : - (knownZero1[w] & m) != 0 ? 2 : - 0; + w = segmentBase - windowSize; + if (aIndex >= w && aIndex < segmentBase) + { + rel = aIndex - w; + w = rel >> 6; + m = 1UL << (rel & 63); + rel = (knownOne1[w] & m) != 0 ? 1 : + (knownZero1[w] & m) != 0 ? 2 : + 0; - return rel; - } + return rel; + } - return 0; - } + return 0; + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void SetAKnownRowAware( - int aIndex, - bool valueOne, - int segmentBase, - int windowSize, - ulong[] knownOne0, - ulong[] knownZero0, - ulong[] knownOne1, - ulong[] knownZero1) - { - if (aIndex < 0) return; + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void SetAKnownRowAware( + int aIndex, + bool valueOne, + int segmentBase, + int windowSize, + ulong[] knownOne0, + ulong[] knownZero0, + ulong[] knownOne1, + ulong[] knownZero1) + { + if (aIndex < 0) return; - int rel, w; - ulong m; - if (aIndex >= segmentBase && aIndex < segmentBase + windowSize) - { - rel = aIndex - segmentBase; - w = rel >> 6; - m = 1UL << (rel & 63); - if (valueOne) - knownOne0[w] |= m; - else - knownZero0[w] |= m; - return; - } + int rel, w; + ulong m; + if (aIndex >= segmentBase && aIndex < segmentBase + windowSize) + { + rel = aIndex - segmentBase; + w = rel >> 6; + m = 1UL << (rel & 63); + if (valueOne) + knownOne0[w] |= m; + else + knownZero0[w] |= m; + return; + } - // windowSize is seg1Start here. We're reusing the variable to limit registry pressure. - windowSize = segmentBase - windowSize; - if (aIndex >= windowSize && aIndex < segmentBase) - { - rel = aIndex - windowSize; - w = rel >> 6; - m = 1UL << (rel & 63); - if (valueOne) - knownOne1[w] |= m; - else - knownZero1[w] |= m; - } - } + // windowSize is seg1Start here. We're reusing the variable to limit registry pressure. + windowSize = segmentBase - windowSize; + if (aIndex >= windowSize && aIndex < segmentBase) + { + rel = aIndex - windowSize; + w = rel >> 6; + m = 1UL << (rel & 63); + if (valueOne) + knownOne1[w] |= m; + else + knownZero1[w] |= m; + } + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static bool TryFindSingleUnknownInQ_Prefix( - in ulong[] qMask, in ulong[] oneWin, in ulong[] zeroWin, - int words, ulong lastMask, - out int offset) - { - offset = -1; - int found = 0; + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool TryFindSingleUnknownInQ_Prefix( + in ulong[] qMask, in ulong[] oneWin, in ulong[] zeroWin, + int words, ulong lastMask, + out int offset) + { + offset = -1; + int found = 0; - for (int w = 0; w < words; w++) - { - ulong q = qMask[w]; - if (w == words - 1) q &= lastMask; + for (int w = 0; w < words; w++) + { + ulong q = qMask[w]; + if (w == words - 1) q &= lastMask; - ulong unknown = oneWin[w] | zeroWin[w]; - unknown = q & ~unknown; - if (unknown == 0) continue; + ulong unknown = oneWin[w] | zeroWin[w]; + unknown = q & ~unknown; + if (unknown == 0) continue; - found += PopCount(unknown); - if (found > 1) return false; + found += PopCount(unknown); + if (found > 1) return false; - int bit = BitOperations.TrailingZeroCount(unknown); - offset = (w << 6) + bit; - } + int bit = BitOperations.TrailingZeroCount(unknown); + offset = (w << 6) + bit; + } - return found == 1; - } + return found == 1; + } #if DETAILED_LOG - private static bool TryProcessBottomUpBlockRowAware( - ReadOnlySpan qOneOffsets, - in ulong[] qMaskWords, - int qWordCount, - ulong lastWordMask, - int maxAllowedA, - int startColumn, - int columnCount, - ref CarryRange carry, - ref int maxKnownA, - ref int segmentBase, - ref ulong[] knownOne0, - ref ulong[] knownOne1, - ref ulong[] knownZero0, - ref ulong[] knownZero1, - int windowSize, - int wordCount, - ulong[] aOneWin, - ulong[] aZeroWin, - ref int windowColumn, - out ContradictionReason reason) + private static bool TryProcessBottomUpBlockRowAware( + ReadOnlySpan qOneOffsets, + in ulong[] qMaskWords, + int qWordCount, + ulong lastWordMask, + int maxAllowedA, + int startColumn, + int columnCount, + ref CarryRange carry, + ref int maxKnownA, + ref int segmentBase, + ref ulong[] knownOne0, + ref ulong[] knownOne1, + ref ulong[] knownZero0, + ref ulong[] knownZero1, + int windowSize, + int wordCount, + ulong[] aOneWin, + ulong[] aZeroWin, + ref int windowColumn, + ulong prime, + long qHash, + in BigInteger qExact, + int topIndex0, + int topIndex1, + ref bool top0KnownOne, + ref bool top1KnownOne, + ref bool top0KnownZero, + ref bool top1KnownZero, + ref int zeroTailStart, + int topPrefixKnownBits, + ulong topPrefixValue, + HashSet globalKnownOneIndices, + HashSet globalKnownZeroIndices, + ref BigInteger globalKnownMinA, + ref BigInteger globalKnownMaxA, + out ContradictionReason reason) #else - private static bool TryProcessBottomUpBlockRowAware( - ReadOnlySpan qOneOffsets, - in ulong[] qMaskWords, - int qWordCount, - ulong lastWordMask, - int maxAllowedA, - int startColumn, - int columnCount, - ref CarryRange carry, - ref int maxKnownA, - ref int segmentBase, - ref ulong[] knownOne0, - ref ulong[] knownOne1, - ref ulong[] knownZero0, - ref ulong[] knownZero1, - int windowSize, - int wordCount, - ulong[] aOneWin, - ulong[] aZeroWin, - ref int windowColumn) + private static bool TryProcessBottomUpBlockRowAware( + ReadOnlySpan qOneOffsets, + in ulong[] qMaskWords, + int qWordCount, + ulong lastWordMask, + int maxAllowedA, + int startColumn, + int columnCount, + ref CarryRange carry, + ref int maxKnownA, + ref int segmentBase, + ref ulong[] knownOne0, + ref ulong[] knownOne1, + ref ulong[] knownZero0, + ref ulong[] knownZero1, + int windowSize, + int wordCount, + ulong[] aOneWin, + ulong[] aZeroWin, + ref int windowColumn, + ulong prime, + long qHash, + in BigInteger qExact, + int topIndex0, + int topIndex1, + ref bool top0KnownOne, + ref bool top1KnownOne, + ref bool top0KnownZero, + ref bool top1KnownZero, + ref int zeroTailStart, + int topPrefixKnownBits, + ulong topPrefixValue, + HashSet globalKnownOneIndices, + HashSet globalKnownZeroIndices, + ref BigInteger globalKnownMinA, + ref BigInteger globalKnownMaxA) #endif - { - // columnCount is endColumn from here. We're reusing the variable to limit registry pressure. - columnCount += startColumn; - int stableUnknown = qOneOffsets.Length; - int maxOffset = qOneOffsets[stableUnknown - 1]; - ulong[] temp; + { + // columnCount is endColumn from here. We're reusing the variable to limit registry pressure. + columnCount += startColumn; + int stableUnknown = qOneOffsets.Length; + int maxOffset = qOneOffsets[stableUnknown - 1]; + ulong[] temp; - // Ensure window is aligned. - ArgumentOutOfRangeException.ThrowIfNotEqual(windowColumn, startColumn); + // Ensure window is aligned. + ArgumentOutOfRangeException.ThrowIfNotEqual(windowColumn, startColumn); - int maxOffsetPlusOne = maxOffset + 1, - qWordCountMinusOne = qWordCount - 1, - endColumnMinusOne = columnCount - 1; + int maxOffsetPlusOne = maxOffset + 1, + qWordCountMinusOne = qWordCount - 1, + endColumnMinusOne = columnCount - 1; - while (startColumn < columnCount) - { - int aIndex, remaining, state, step; - // Segment rollover based on current column (because we may set aIndex within [startColumn-maxOffset..startColumn]). - int bound = (startColumn / windowSize) * windowSize; + while (startColumn < columnCount) + { + int aIndex, remaining, state, step; + bool oldTop0KnownOne = top0KnownOne; + bool oldTop1KnownOne = top1KnownOne; + bool oldTop0KnownZero = top0KnownZero; + bool oldTop1KnownZero = top1KnownZero; + int oldZeroTailStart = zeroTailStart; + bool topChanged = false; + // Segment rollover based on current column (because we may set aIndex within [startColumn-maxOffset..startColumn]). + int bound = (startColumn / windowSize) * windowSize; - if (bound != segmentBase) - { - if (bound == segmentBase + windowSize) - { - temp = knownOne0; knownOne0 = knownOne1; knownOne1 = temp; - temp = knownZero0; knownZero0 = knownZero1; knownZero1 = temp; - Array.Clear(knownOne0, 0, wordCount); - Array.Clear(knownZero0, 0, wordCount); - } - else - { - // Console.WriteLine("Rebuilding window"); - Array.Clear(knownOne0, 0, wordCount); - Array.Clear(knownOne1, 0, wordCount); - Array.Clear(knownZero0, 0, wordCount); - Array.Clear(knownZero1, 0, wordCount); - // Also clear window because it may reference bits outside cache. - Array.Clear(aOneWin, 0, qWordCount); - Array.Clear(aZeroWin, 0, qWordCount); + if (bound != segmentBase) + { + if (bound == segmentBase + windowSize) + { + temp = knownOne0; knownOne0 = knownOne1; knownOne1 = temp; + temp = knownZero0; knownZero0 = knownZero1; knownZero1 = temp; + Array.Clear(knownOne0, 0, wordCount); + Array.Clear(knownZero0, 0, wordCount); + } + else + { + // Console.WriteLine("Rebuilding window"); + Array.Clear(knownOne0, 0, wordCount); + Array.Clear(knownOne1, 0, wordCount); + Array.Clear(knownZero0, 0, wordCount); + Array.Clear(knownZero1, 0, wordCount); + // Also clear window because it may reference bits outside cache. + Array.Clear(aOneWin, 0, qWordCount); + Array.Clear(aZeroWin, 0, qWordCount); - // Build window for current startColumn: bit t corresponds to a_{startColumn - t} - for (step = 0; step <= maxOffset; step++) - { - aIndex = startColumn - step; - state = aIndex < 0 || aIndex > maxAllowedA - ? 2 - : GetAKnownStateRowAware(aIndex, bound, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); + // Build window for current startColumn: bit t corresponds to a_{startColumn - t} + for (step = 0; step <= maxOffset; step++) + { + aIndex = startColumn - step; + state = aIndex < 0 || aIndex > maxAllowedA + ? 2 + : GetAKnownStateRowAware(aIndex, bound, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); - if (state == 1) - { - aOneWin[step >> 6] |= 1UL << (step & 63); - } - else if (state == 2) - { - aZeroWin[step >> 6] |= 1UL << (step & 63); - } - } + if (state == 1) + { + aOneWin[step >> 6] |= 1UL << (step & 63); + } + else if (state == 2) + { + aZeroWin[step >> 6] |= 1UL << (step & 63); + } + } - if (qWordCount > 0) - { - aOneWin[qWordCountMinusOne] &= lastWordMask; - aZeroWin[qWordCountMinusOne] &= lastWordMask; - } - } + if (qWordCount > 0) + { + aOneWin[qWordCountMinusOne] &= lastWordMask; + aZeroWin[qWordCountMinusOne] &= lastWordMask; + } + } - segmentBase = bound; - } + segmentBase = bound; + } - int qWordsEff = qWordCount; - ulong qLastEff = lastWordMask; - if (startColumn < maxOffset) - { - GetQPrefixMask(startColumn, maxOffsetPlusOne, qWordCount, out qWordsEff, out qLastEff); - } + int qWordsEff = qWordCount; + ulong qLastEff = lastWordMask; + if (startColumn < maxOffset) + { + GetQPrefixMask(startColumn, maxOffsetPlusOne, qWordCount, out qWordsEff, out qLastEff); + } - // StableUnknown batching is valid only if the window contains no known bits in the q-active positions. - if (startColumn >= maxOffset && startColumn <= maxAllowedA) - { - remaining = endColumnMinusOne; - if (remaining > maxAllowedA) - { - remaining = maxAllowedA; - } + // StableUnknown batching is valid only if the window contains no known bits in the q-active positions. + if (startColumn >= maxOffset && startColumn <= maxAllowedA) + { + remaining = endColumnMinusOne; + if (remaining > maxAllowedA) + { + remaining = maxAllowedA; + } - remaining = remaining - startColumn + 1; - if (remaining > 0) - { - // Additionally, ensure current window has no known bits (should be true if maxKnownA condition holds). - // Conservative batching: ignore row-aware window state and assume all q positions are unknown. - // This cannot create false negatives; it may only reduce pruning power. + remaining = remaining - startColumn + 1; + if (remaining > 0) + { + // Additionally, ensure current window has no known bits (should be true if maxKnownA condition holds). + // Conservative batching: ignore row-aware window state and assume all q positions are unknown. + // This cannot create false negatives; it may only reduce pruning power. #if DETAILED_LOG - _statBatchEntry++; - _statBatchCols += remaining; + _statBatchEntry++; + _statBatchCols += remaining; #endif - while (remaining >= TailCarryBatchColumns) - { + while (remaining >= TailCarryBatchColumns) + { #if DETAILED_LOG - if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns, out var propagateReason)) + if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns, out var propagateReason)) #else - if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns)) + if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns)) #endif - { + { #if DETAILED_LOG - reason = propagateReason; + reason = propagateReason; + Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryAdvanceStableUnknown)} 1, remaining={remaining}"); #endif - Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryAdvanceStableUnknown)} 1, remaining={remaining}"); - return false; - } - startColumn += TailCarryBatchColumns; - windowColumn = startColumn; - remaining -= TailCarryBatchColumns; - } +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTryAdvanceStableUnknown); +#endif - if (remaining > 0) - { + return false; + } + + startColumn += TailCarryBatchColumns; + windowColumn = startColumn; + remaining -= TailCarryBatchColumns; + } + + if (remaining > 0) + { #if DETAILED_LOG - if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining, out var propagateReason)) + if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining, out var propagateReason)) #else - if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining)) + if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining)) #endif - { + { #if DETAILED_LOG - reason = propagateReason; + reason = propagateReason; + Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryAdvanceStableUnknown)} 2, remaining={remaining}"); #endif - Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryAdvanceStableUnknown)} 2, remaining={remaining}"); - return false; - } - startColumn += remaining; - windowColumn = startColumn; - } +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTryAdvanceStableUnknown); +#endif - // Reset window to unknown (no known bits) because we skipped updating it across columns. - Array.Clear(aOneWin, 0, qWordCount); - Array.Clear(aZeroWin, 0, qWordCount); + return false; + } - continue; - } - } + startColumn += remaining; + windowColumn = startColumn; + } - // Mark out-of-range (negative) a indices as zero in this column. - // if (startColumn < maxOffset) - // { - // int firstOut = startColumn + 1; - // for (int t = firstOut; t <= maxOffset; t++) - // { - // int w = t >> 6; - // int b = t & 63; - // aZeroWin[w] |= 1UL << b; - // } - // if (qWordCount > 0) aZeroWin[qWordCount - 1] &= lastWordMask; - // } + // Reset window to unknown (no known bits) because we skipped updating it across columns. + Array.Clear(aOneWin, 0, qWordCount); + Array.Clear(aZeroWin, 0, qWordCount); - ComputeForcedRemainingAndClean_Prefix(qMaskWords, aOneWin, aZeroWin, qWordsEff, qLastEff, out int forced, out remaining); + continue; + } + } - // OPTION-A - doesn't work and skips valid q candidates - // // possible = forced + remaining (later you already do remaining += forced) - // int possible = forced + remaining; + // Mark out-of-range (negative) a indices as zero in this column. + // if (startColumn < maxOffset) + // { + // int firstOut = startColumn + 1; + // for (int t = firstOut; t <= maxOffset; t++) + // { + // int w = t >> 6; + // int b = t & 63; + // aZeroWin[w] |= 1UL << b; + // } + // if (qWordCount > 0) aZeroWin[qWordCount - 1] &= lastWordMask; + // } - // // --- ADD THIS PRUNE --- - // if (!CouldStillReachTopCarryZero_UpperBound(carry, startColumn, endColumnMinusOne, possible)) - // { - // #if DETAILED_LOG - // reason = ContradictionReason.ParityUnreachable; - // #endif - // // Console.WriteLine("[bit-contradiction] Pruned with CouldStillReachTopCarryZero_UpperBound"); - // return false; - // } - // - // remaining = possible; + ComputeForcedRemainingAndClean_Prefix(qMaskWords, aOneWin, aZeroWin, qWordsEff, qLastEff, out int forced, out remaining); - // OPTION-B - doesn't work with steps > 1. - // int possible = forced + remaining; + // OPTION-A - doesn't work and skips valid q candidates + // // possible = forced + remaining (later you already do remaining += forced) + // int possible = forced + remaining; - // // --- ADD: best-case carry check to see if we can still reach 0 before we pass endColumnMinusOne --- - // long best = carry.Min; - // if (best > 0) - // { - // // We only need a quick check; simulate a few steps or until it hits 0. - // int stepsLeft = Math.Min(1, endColumnMinusOne - startColumn + 1); - // long c = best; + // // --- ADD THIS PRUNE --- + // if (!CouldStillReachTopCarryZero_UpperBound(carry, startColumn, endColumnMinusOne, possible)) + // { + // #if DETAILED_LOG + // reason = ContradictionReason.ParityUnreachable; + // #endif + // // Console.WriteLine("[bit-contradiction] Pruned with CouldStillReachTopCarryZero_UpperBound"); + // #if WITH_PRUNE_STATS + // Atomic.Add(ref _prunedWithCouldStillReachTopCarryZero_UpperBound, 1UL); + // #endif + // return false; + // } + // + // remaining = possible; - // for (int s = 0; s < stepsLeft && c > 0; s++) - // { - // c = BestCaseCarryOutOneStep(c, forced, possible, 1); - // if (c < 0) - // { - // #if DETAILED_LOG - // reason = ContradictionReason.ParityUnreachable; - // #endif + // OPTION-B - doesn't work with steps > 1. + // int possible = forced + remaining; - // Console.WriteLine("[bit-contradiction] Pruned with BestCaseCarryOutOneStep"); - // return false; - // } - // // For subsequent columns, forced/possible will change, so this is still conservative (weak). - // // But even this single-step parity feasibility is a useful prune. - // // break; // cheap mode: only 1 step; remove break for stronger prune (but slower) - // } + // // --- ADD: best-case carry check to see if we can still reach 0 before we pass endColumnMinusOne --- + // long best = carry.Min; + // if (best > 0) + // { + // // We only need a quick check; simulate a few steps or until it hits 0. + // int stepsLeft = Math.Min(1, endColumnMinusOne - startColumn + 1); + // long c = best; - // // If even best-case can't reduce at all due to parity infeasibility, prune already handled. - // // Full multi-step would require using future columns' forced/possible, which we don't have here cheaply. - // } + // for (int s = 0; s < stepsLeft && c > 0; s++) + // { + // c = BestCaseCarryOutOneStep(c, forced, possible, 1); + // if (c < 0) + // { + // #if DETAILED_LOG + // reason = ContradictionReason.ParityUnreachable; + // #endif - // If exactly one unknown contribution among q=1 positions AND carry parity is fixed, - // we can force the corresponding a bit to satisfy the required result bit parity. - if (remaining == 1 && ((carry.Min ^ carry.Max) & 1L) == 0) - { - if (TryFindSingleUnknownInQ_Prefix(qMaskWords, aOneWin, aZeroWin, qWordsEff, qLastEff, out step)) - { - aIndex = startColumn - step; + // Console.WriteLine("[bit-contradiction] Pruned with BestCaseCarryOutOneStep"); - // Required result bit for M_p in columns [0..p-1] is 1. - const int requiredBit = 1; + // #if WITH_PRUNE_STATS + // Atomic.Add(ref _prunedWithBestCaseCarryOutOneStep, 1UL); + // #endif - // We need (carryIn + forced + x) % 2 == requiredBit, where x ∈ {0,1}. - int b = (int)(carry.Min & 1L); // fixed parity because Min/Max same parity - // We're reusing qWordsEff as w from here to limit registry pressure - qWordsEff = (requiredBit ^ b ^ (forced & 1)) & 1; - bool needOne = qWordsEff != 0; + // return false; + // } + // // For subsequent columns, forced/possible will change, so this is still conservative (weak). + // // But even this single-step parity feasibility is a useful prune. + // // break; // cheap mode: only 1 step; remove break for stronger prune (but slower) + // } - // Check contradiction with already-known value. - state = GetAKnownStateRowAware(aIndex, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); - if (needOne) - { - if (state == 2) - { + // // If even best-case can't reduce at all due to parity infeasibility, prune already handled. + // // Full multi-step would require using future columns' forced/possible, which we don't have here cheaply. + // } + + // If exactly one unknown contribution among q=1 positions AND carry parity is fixed, + // we can force the corresponding a bit to satisfy the required result bit parity. + if (remaining == 1 && ((carry.Min ^ carry.Max) & 1L) == 0) + { + if (TryFindSingleUnknownInQ_Prefix(qMaskWords, aOneWin, aZeroWin, qWordsEff, qLastEff, out step)) + { + aIndex = startColumn - step; + + // Required result bit for M_p in columns [0..p-1] is 1. + const int requiredBit = 1; + + // We need (carryIn + forced + x) % 2 == requiredBit, where x ∈ {0,1}. + int b = (int)(carry.Min & 1L); // fixed parity because Min/Max same parity + // We're reusing qWordsEff as w from here to limit registry pressure + qWordsEff = (requiredBit ^ b ^ (forced & 1)) & 1; + bool needOne = qWordsEff != 0; + + // Check contradiction with already-known value. + state = GetAKnownStateRowAware(aIndex, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); + if (needOne) + { + if (state == 2) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; + Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryFindSingleUnknownInQ_Prefix)}, needOne={needOne}, aIndex={aIndex}, state=2"); #endif - Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryFindSingleUnknownInQ_Prefix)}, needOne={needOne}, aIndex={aIndex}, state=2"); - return false; - } - SetAKnownRowAware(aIndex, true, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTryFindSingleUnknownInQ_Prefix); +#endif - // Reflect in window at offset t - qWordsEff = step >> 6; - b = step & 63; - aOneWin[qWordsEff] |= 1UL << b; - forced++; - } - else - { - if (state == 1) - { + return false; + } + + SetAKnownRowAware(aIndex, true, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); + if (!TrySetGlobalKnownBit(aIndex, true, globalKnownOneIndices, globalKnownZeroIndices, ref globalKnownMinA, ref globalKnownMaxA)) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryFindSingleUnknownInQ_Prefix)}, needOne={needOne}, aIndex={aIndex}, state=1"); - return false; - } - - SetAKnownRowAware(aIndex, false, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); - - qWordsEff = step >> 6; - b = step & 63; - aZeroWin[qWordsEff] |= 1UL << b; - } - - remaining = 0; - if (aIndex > maxKnownA) - { - maxKnownA = aIndex; - } - } - } - - // Now propagate carry using forced and possible (=forced+remaining). - remaining += forced; - - if (!TryPropagateCarry(ref carry, forced, remaining, 1)) - { + return false; + } + if (aIndex == topIndex0) + { + if (top0KnownZero) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryPropagateCarry)}"); - return false; - } + return false; + } - // --- SAFE TOP-CARRY PRUNE (uses true remaining columns to p-1) --- - // We never reach the case when colsLeftToTop is small. We eliminate candidates very quickly, - // with colsLeftToTop ~138 mln. - // int colsLeftToTop = topColumnExclusive - (startColumn + 1); // +1 bo kolumnę startColumn już właśnie przetworzyłeś - // if (carry.Min > 0 && colsLeftToTop > 0) - // { - // if (colsLeftToTop < 63) - // { - // Console.WriteLine("[bit-contradiction] Checking TOP-CARRY PRUNE"); - // if ((carry.Min >> colsLeftToTop) > 0) - // { - // #if DETAILED_LOG - // reason = ContradictionReason.ParityUnreachable; - // #endif - // Console.WriteLine("[bit-contradiction] Pruned with TOP-CARRY PRUNE"); - // return false; - // } - // } - // else - // { - // Console.WriteLine($"[bit-contradiction] TOP-CARRY PRUNE too far away from top {colsLeftToTop}"); - // } - // // colsLeftToTop >= 63 => shift dałby 0, więc nigdy nie tnij (konserwatywnie) - // } - - // Advance to next column: shift window, then insert status of a_{startColumn+1} into bit0. - // remaining is nextA from here. We're reusing variable to limit registry pressure. - remaining = startColumn + 1; - ShiftLeft1InPlace(aOneWin, aZeroWin, qWordCount, lastWordMask); - - // Insert bit0 for nextA - if (remaining > maxAllowedA) - { - // state = 2; - aZeroWin[0] |= 1UL; - } - else - { - state = GetAKnownStateRowAware(remaining, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); - if (state == 1) - { - aOneWin[0] |= 1UL; - } - else if (state == 2) - { - aZeroWin[0] |= 1UL; - } - } - - - startColumn++; - windowColumn = startColumn; + if (!top0KnownOne) + { + top0KnownOne = true; + topChanged = true; + } + } + else if (aIndex == topIndex1) + { + if (top1KnownZero) + { #if DETAILED_LOG - _statScalarCols++; + reason = ContradictionReason.ParityUnreachable; #endif - } + return false; + } + + if (!top1KnownOne) + { + top1KnownOne = true; + topChanged = true; + } + } + + // Reflect in window at offset t + qWordsEff = step >> 6; + b = step & 63; + aOneWin[qWordsEff] |= 1UL << b; + forced++; + } + else + { + if (state == 1) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; + Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryFindSingleUnknownInQ_Prefix)}, needOne={needOne}, aIndex={aIndex}, state=1"); +#endif + +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTryFindSingleUnknownInQ_Prefix); +#endif + + return false; + } + + SetAKnownRowAware(aIndex, false, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); + if (!TrySetGlobalKnownBit(aIndex, false, globalKnownOneIndices, globalKnownZeroIndices, ref globalKnownMinA, ref globalKnownMaxA)) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif + return false; + } + if (aIndex == topIndex0) + { + if (top0KnownOne) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif + return false; + } + + if (!top0KnownZero) + { + top0KnownZero = true; + topChanged = true; + } + } + else if (aIndex == topIndex1) + { + if (top1KnownOne) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif + return false; + } + + if (!top1KnownZero) + { + top1KnownZero = true; + topChanged = true; + } + } + { + UpdateZeroTailFromTop(ref zeroTailStart, topIndex0, topIndex1, top0KnownZero, top1KnownZero); + } + + qWordsEff = step >> 6; + b = step & 63; + aZeroWin[qWordsEff] |= 1UL << b; + } + + remaining = 0; + if (aIndex > maxKnownA) + { + maxKnownA = aIndex; + } + } + } + + topChanged = topChanged || + oldTop0KnownOne != top0KnownOne || + oldTop1KnownOne != top1KnownOne || + oldTop0KnownZero != top0KnownZero || + oldTop1KnownZero != top1KnownZero || + oldZeroTailStart != zeroTailStart; + + bool runDynamicModPrune = topChanged || ((startColumn & DynamicModPeriodicMask) == 0); + if (runDynamicModPrune) + { + if (!TryDynamicModularRangePrune(qOneOffsets, qHash, qExact, prime, globalKnownMinA, globalKnownMaxA, globalKnownOneIndices, globalKnownZeroIndices, maxAllowedA, top0KnownOne, top0KnownZero, top1KnownOne, zeroTailStart, topPrefixKnownBits, topPrefixValue)) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTryDynamicModularRangePrune); +#endif + return false; + } + } + + if ((top0KnownZero && top0KnownOne) || (top1KnownZero && top1KnownOne)) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTopStateConflict); +#endif + return false; + } + + if (topIndex1 < 0) + { + if (top0KnownZero) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTopBothZeroConflict); +#endif + return false; + } + } + else if (top0KnownZero && top1KnownZero) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTopBothZeroConflict); +#endif + return false; + } + + if (remaining == 0) + { + int requiredCarryParity = 1 ^ (forced & 1); + long carryMin = AlignUpToParity(carry.Min, requiredCarryParity); + long carryMax = AlignDownToParity(carry.Max, requiredCarryParity); + if (carryMin > carryMax) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithCarryParityPrecheck); +#endif + return false; + } + + carry = new CarryRange(carryMin, carryMax); + } + + long minSum = carry.Min + forced; + long maxSum = carry.Max + forced + remaining; + const int requiredParity = 1; + if (minSum == maxSum) + { + if ((minSum & 1L) != requiredParity) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithCarryParityPrecheck); +#endif + return false; + } + + carry = CarryRange.Single((minSum - requiredParity) >> 1); + } + else + { + if ((minSum & 1L) != requiredParity && remaining == 0) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithCarryParityPrecheck); +#endif + return false; + } + + if (!TryPropagateCarry(ref carry, forced, forced + remaining, requiredParity)) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; + Console.WriteLine($"[bit-contradiction] Pruned with {nameof(TryPropagateCarry)}"); +#endif + +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTryPropagateCarry2); +#endif + + return false; + } + } + + // --- SAFE TOP-CARRY PRUNE (uses true remaining columns to p-1) --- + // We never reach the case when colsLeftToTop is small. We eliminate candidates very quickly, + // with colsLeftToTop ~138 mln. + // int colsLeftToTop = topColumnExclusive - (startColumn + 1); // +1 bo kolumnę startColumn już właśnie przetworzyłeś + // if (carry.Min > 0 && colsLeftToTop > 0) + // { + // if (colsLeftToTop < 63) + // { + // Console.WriteLine("[bit-contradiction] Checking TOP-CARRY PRUNE"); + // if ((carry.Min >> colsLeftToTop) > 0) + // { + // #if DETAILED_LOG + // reason = ContradictionReason.ParityUnreachable; + // Console.WriteLine("[bit-contradiction] Pruned with TOP-CARRY PRUNE"); + // #endif + // #if WITH_PRUNE_STATS + // Atomic.Add(ref _prunedWithTopCarry, 1UL); + // #endif + // return false; + // } + // } + // else + // { + // Console.WriteLine($"[bit-contradiction] TOP-CARRY PRUNE too far away from top {colsLeftToTop}"); + // } + // // colsLeftToTop >= 63 => shift dałby 0, więc nigdy nie tnij (konserwatywnie) + // } + + // Advance to next column: shift window, then insert status of a_{startColumn+1} into bit0. + // remaining is nextA from here. We're reusing variable to limit registry pressure. + remaining = startColumn + 1; + ShiftLeft1InPlace(aOneWin, aZeroWin, qWordCount, lastWordMask); + + // Insert bit0 for nextA + if (remaining > maxAllowedA) + { + // state = 2; + aZeroWin[0] |= 1UL; + } + else + { + state = GetAKnownStateRowAware(remaining, segmentBase, windowSize, knownOne0, knownZero0, knownOne1, knownZero1); + if (state == 1) + { + aOneWin[0] |= 1UL; + } + else if (state == 2) + { + aZeroWin[0] |= 1UL; + } + } + + + startColumn++; + windowColumn = startColumn; +#if DETAILED_LOG + _statScalarCols++; +#endif + } #if DETAILED_LOG - reason = ContradictionReason.None; + reason = ContradictionReason.None; #endif - return true; - } + return true; + } - private static bool TryProcessBottomUpBlock( - ulong prime, - ReadOnlySpan qOneOffsets, - in int[] runStarts, - in int[] runLengths, - int runCount, - int maxAllowedA, - int startColumn, - int columnCount, - ref CarryRange carry, - ref int maxKnownA, - ref int segmentBase, - ref int runStartIdx, - ref int runEndIdx, - ulong[] knownOne0, - ulong[] knownOne1, - ulong[] knownZero0, - ulong[] knownZero1, - int windowSize, - int topIndex0, - int topIndex1, - ref bool top0KnownOne, - ref bool top1KnownOne, - ref bool top0KnownZero, - ref bool top1KnownZero, - ref int zeroTailStart + private static bool TryProcessBottomUpBlock( + ulong prime, + ReadOnlySpan qOneOffsets, + in int[] runStarts, + in int[] runLengths, + int runCount, + int maxAllowedA, + int startColumn, + int columnCount, + ref CarryRange carry, + ref int maxKnownA, + ref int segmentBase, + ref int runStartIdx, + ref int runEndIdx, + ulong[] knownOne0, + ulong[] knownOne1, + ulong[] knownZero0, + ulong[] knownZero1, + int windowSize, + int topIndex0, + int topIndex1, + ref bool top0KnownOne, + ref bool top1KnownOne, + ref bool top0KnownZero, + ref bool top1KnownZero, + ref int zeroTailStart, + int topPrefixKnownBits, + ulong topPrefixValue #if DETAILED_LOG - , out ContradictionReason reason + , out ContradictionReason reason #endif - ) - { - int endColumn = startColumn + columnCount; - int qOneOffsetsLength = qOneOffsets.Length; - int maxOffset = qOneOffsets[qOneOffsetsLength - 1]; - int stableUnknown = qOneOffsetsLength; - int bound, runStart, runEnd; - ulong[] temp; - // Span temp; - while (startColumn < endColumn) - { - int remaining; - if (startColumn >= maxOffset && startColumn <= maxAllowedA && maxKnownA < startColumn - maxOffset) - { - remaining = endColumn - 1; - if (remaining > maxAllowedA) - { - remaining = maxAllowedA; - } + ) + { + int endColumn = startColumn + columnCount; + int qOneOffsetsLength = qOneOffsets.Length; + int maxOffset = qOneOffsets[qOneOffsetsLength - 1]; + int stableUnknown = qOneOffsetsLength; + long qHash = ComputeQOffsetsHash(qOneOffsets); + BigInteger qExact = BuildQExact(qOneOffsets); + HashSet globalKnownOneIndices = new(); + HashSet globalKnownZeroIndices = new(); + BigInteger globalKnownMinA = BigInteger.Zero; + BigInteger globalKnownMaxA = Pow2Provider.BigIntegerMinusOne(maxAllowedA + 1); + int bound, runStart, runEnd; + ulong[] temp; + // Span temp; + while (startColumn < endColumn) + { + int remaining; + if (startColumn >= maxOffset && startColumn <= maxAllowedA && maxKnownA < startColumn - maxOffset) + { + remaining = endColumn - 1; + if (remaining > maxAllowedA) + { + remaining = maxAllowedA; + } - remaining = remaining - startColumn + 1; - if (remaining >= 16) - { - runStartIdx = 0; - runEndIdx = runCount; - while (remaining >= TailCarryBatchColumns) - { + remaining = remaining - startColumn + 1; + if (remaining >= 16) + { + runStartIdx = 0; + runEndIdx = runCount; + while (remaining >= TailCarryBatchColumns) + { #if DETAILED_LOG - if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns, out var propagateReason)) + if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns, out var propagateReason)) #else - if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns)) + if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns)) #endif - { + { #if DETAILED_LOG - reason = propagateReason; + reason = propagateReason; #endif - return false; - } + return false; + } - startColumn += TailCarryBatchColumns; - remaining -= TailCarryBatchColumns; - } + startColumn += TailCarryBatchColumns; + remaining -= TailCarryBatchColumns; + } - if (remaining > 0) - { + if (remaining > 0) + { #if DETAILED_LOG - if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining, out var propagateReason)) + if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining, out var propagateReason)) #else - if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining)) + if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining)) #endif - { + { #if DETAILED_LOG - reason = propagateReason; + reason = propagateReason; #endif - return false; - } + return false; + } - remaining = 0; - } + remaining = 0; + } - bound = (startColumn / windowSize) * windowSize; - if (bound != segmentBase) - { - if (bound == segmentBase + windowSize) - { - // rollover forward by one segment: swap and clear only the new "current" segment - temp = knownOne0; knownOne0 = knownOne1; knownOne1 = temp; - temp = knownZero0; knownZero0 = knownZero1; knownZero1 = temp; + bound = (startColumn / windowSize) * windowSize; + if (bound != segmentBase) + { + if (bound == segmentBase + windowSize) + { + // rollover forward by one segment: swap and clear only the new "current" segment + temp = knownOne0; knownOne0 = knownOne1; knownOne1 = temp; + temp = knownZero0; knownZero0 = knownZero1; knownZero1 = temp; - Array.Clear(knownOne0); - Array.Clear(knownZero0); - } - else - { - // jumped more than one segment: we genuinely lost locality; clear both - Array.Clear(knownOne0); - Array.Clear(knownOne1); - Array.Clear(knownZero0); - Array.Clear(knownZero1); - } + Array.Clear(knownOne0); + Array.Clear(knownZero0); + } + else + { + // jumped more than one segment: we genuinely lost locality; clear both + Array.Clear(knownOne0); + Array.Clear(knownOne1); + Array.Clear(knownZero0); + Array.Clear(knownZero1); + } - segmentBase = bound; - } + segmentBase = bound; + } - continue; - } - } + continue; + } + } - int forced = 0; - remaining = 0; - int chosenIndex = -1; - // bool topChanged = false; - bound = (startColumn / windowSize) * windowSize; - if (bound != segmentBase) - { - if (bound == segmentBase + windowSize) - { - temp = knownOne0; - knownOne0 = knownOne1; - knownOne1 = temp; + int forced = 0; + remaining = 0; + int chosenIndex = -1; + bool oldTop0KnownOne = top0KnownOne; + bool oldTop1KnownOne = top1KnownOne; + bool oldTop0KnownZero = top0KnownZero; + bool oldTop1KnownZero = top1KnownZero; + int oldZeroTailStart = zeroTailStart; + bool topChanged = false; + bound = (startColumn / windowSize) * windowSize; + if (bound != segmentBase) + { + if (bound == segmentBase + windowSize) + { + temp = knownOne0; + knownOne0 = knownOne1; + knownOne1 = temp; - temp = knownZero0; - knownZero0 = knownZero1; - knownZero1 = temp; + temp = knownZero0; + knownZero0 = knownZero1; + knownZero1 = temp; - // knownOne0.Clear(); - // knownZero0.Clear(); - Array.Clear(knownOne0); - Array.Clear(knownZero0); - } - else - { - // knownOne0.Clear(); - // knownOne1.Clear(); - // knownZero0.Clear(); - // knownZero1.Clear(); - Array.Clear(knownOne0); - Array.Clear(knownOne1); - Array.Clear(knownZero0); - Array.Clear(knownZero1); - } + // knownOne0.Clear(); + // knownZero0.Clear(); + Array.Clear(knownOne0); + Array.Clear(knownZero0); + } + else + { + // knownOne0.Clear(); + // knownOne1.Clear(); + // knownZero0.Clear(); + // knownZero1.Clear(); + Array.Clear(knownOne0); + Array.Clear(knownOne1); + Array.Clear(knownZero0); + Array.Clear(knownZero1); + } - segmentBase = bound; - } + segmentBase = bound; + } - bound = startColumn - maxAllowedA; - while (runEndIdx < runCount && runStarts[runEndIdx] <= startColumn) - { - runEndIdx++; - } + bound = startColumn - maxAllowedA; + while (runEndIdx < runCount && runStarts[runEndIdx] <= startColumn) + { + runEndIdx++; + } - while (runStartIdx < runEndIdx) - { - runStart = runStarts[runStartIdx]; - runEnd = runStart + runLengths[runStartIdx] - 1; - if (runEnd < bound) - { - runStartIdx++; - continue; - } + while (runStartIdx < runEndIdx) + { + runStart = runStarts[runStartIdx]; + runEnd = runStart + runLengths[runStartIdx] - 1; + if (runEnd < bound) + { + runStartIdx++; + continue; + } - break; - } + break; + } - int known0Len, runIndex; - int seg0Start = segmentBase; - for (runIndex = runStartIdx; runIndex < runEndIdx; runIndex++) - { - runStart = runStarts[runIndex]; - if (runStart > startColumn) - { - break; - } + int known0Len, runIndex; + int seg0Start = segmentBase; + for (runIndex = runStartIdx; runIndex < runEndIdx; runIndex++) + { + runStart = runStarts[runIndex]; + if (runStart > startColumn) + { + break; + } - runEnd = runStart + runLengths[runIndex] - 1; - if (runEnd > startColumn) - { - runEnd = startColumn; - } + runEnd = runStart + runLengths[runIndex] - 1; + if (runEnd > startColumn) + { + runEnd = startColumn; + } - if (runStart < bound) - { - runStart = bound; - } + if (runStart < bound) + { + runStart = bound; + } - if (runStart > runEnd) - { - continue; - } + if (runStart > runEnd) + { + continue; + } - int aStart = startColumn - runEnd; - runEnd = startColumn - runStart; - if (aStart > maxAllowedA) - { - continue; - } + int aStart = startColumn - runEnd; + runEnd = startColumn - runStart; + if (aStart > maxAllowedA) + { + continue; + } - if (runEnd > maxAllowedA) - { - runEnd = maxAllowedA; - } + if (runEnd > maxAllowedA) + { + runEnd = maxAllowedA; + } - int rangeLength = runEnd - aStart + 1; - if (rangeLength <= 0) - { - continue; - } + int rangeLength = runEnd - aStart + 1; + if (rangeLength <= 0) + { + continue; + } - int seg0End = seg0Start + windowSize - 1; - int seg1Start = seg0Start - windowSize; - int seg1End = seg0Start - 1; + int seg0End = seg0Start + windowSize - 1; + int seg1Start = seg0Start - windowSize; + int seg1End = seg0Start - 1; - int overlapStart = aStart > seg0Start ? aStart : seg0Start; - int overlap0End = runEnd < seg0End ? runEnd : seg0End; - // seg1End is now overlap1End to limit registry pressure - seg1End = runEnd < seg1End ? runEnd : seg1End; + int overlapStart = aStart > seg0Start ? aStart : seg0Start; + int overlap0End = runEnd < seg0End ? runEnd : seg0End; + // seg1End is now overlap1End to limit registry pressure + seg1End = runEnd < seg1End ? runEnd : seg1End; - known0Len = 0; - int ones; - if (overlapStart <= overlap0End) - { - runStart = overlapStart - seg0Start; - // overlap0Start is now len to limit registry pressure - overlapStart = overlap0End - overlapStart + 1; - ones = CountBitsInRange(knownOne0, runStart, overlapStart); - // overlap0End is now zeros to limit registry pressure - overlap0End = CountBitsInRange(knownZero0, runStart, overlapStart); - forced += ones; - remaining += overlapStart - ones - overlap0End; - known0Len = overlapStart; + known0Len = 0; + int ones; + if (overlapStart <= overlap0End) + { + runStart = overlapStart - seg0Start; + // overlap0Start is now len to limit registry pressure + overlapStart = overlap0End - overlapStart + 1; + ones = CountBitsInRange(knownOne0, runStart, overlapStart); + // overlap0End is now zeros to limit registry pressure + overlap0End = CountBitsInRange(knownZero0, runStart, overlapStart); + forced += ones; + remaining += overlapStart - ones - overlap0End; + known0Len = overlapStart; - if (chosenIndex == -1 && overlapStart > ones + overlap0End && TryFindFirstUnknown(knownOne0, knownZero0, runStart, overlapStart, out int idx)) - { - chosenIndex = seg0Start + idx; - } - } + if (chosenIndex == -1 && overlapStart > ones + overlap0End && TryFindFirstUnknown(knownOne0, knownZero0, runStart, overlapStart, out int idx)) + { + chosenIndex = seg0Start + idx; + } + } - // overlap0End is now knownTotal to limit registry pressure - overlap0End = 0; - overlapStart = aStart > seg1Start ? aStart : seg1Start; - if (overlapStart <= seg1End) - { - runStart = overlapStart - seg1Start; - // overlap1Start is now len to limit registry pressure - overlapStart = seg1End - overlapStart + 1; - ones = CountBitsInRange(knownOne1, runStart, overlapStart); - // seg1End is now zeros to limit registry pressure - seg1End = CountBitsInRange(knownZero1, runStart, overlapStart); - forced += ones; - remaining += overlapStart - ones - seg1End; - overlap0End = overlapStart; + // overlap0End is now knownTotal to limit registry pressure + overlap0End = 0; + overlapStart = aStart > seg1Start ? aStart : seg1Start; + if (overlapStart <= seg1End) + { + runStart = overlapStart - seg1Start; + // overlap1Start is now len to limit registry pressure + overlapStart = seg1End - overlapStart + 1; + ones = CountBitsInRange(knownOne1, runStart, overlapStart); + // seg1End is now zeros to limit registry pressure + seg1End = CountBitsInRange(knownZero1, runStart, overlapStart); + forced += ones; + remaining += overlapStart - ones - seg1End; + overlap0End = overlapStart; - if (chosenIndex == -1 && overlapStart > ones + seg1End && TryFindFirstUnknown(knownOne1, knownZero1, runStart, overlapStart, out int idx)) - { - chosenIndex = seg1Start + idx; - } - } + if (chosenIndex == -1 && overlapStart > ones + seg1End && TryFindFirstUnknown(knownOne1, knownZero1, runStart, overlapStart, out int idx)) + { + chosenIndex = seg1Start + idx; + } + } - overlap0End = known0Len + overlap0End; - if (overlap0End < rangeLength) - { - remaining += rangeLength - overlap0End; - } + overlap0End = known0Len + overlap0End; + if (overlap0End < rangeLength) + { + remaining += rangeLength - overlap0End; + } - if (zeroTailStart <= runEnd) - { - // overlap0End is now tailStart to limit registry pressure - overlap0End = aStart > zeroTailStart ? aStart : zeroTailStart; - if (overlap0End <= runEnd) - { - rangeLength = runEnd - overlap0End + 1; - if (rangeLength > 0) - { - remaining -= rangeLength; - if (remaining < 0) - { - remaining = 0; - } - } - } - } - } + if (zeroTailStart <= runEnd) + { + // overlap0End is now tailStart to limit registry pressure + overlap0End = aStart > zeroTailStart ? aStart : zeroTailStart; + if (overlap0End <= runEnd) + { + rangeLength = runEnd - overlap0End + 1; + if (rangeLength > 0) + { + remaining -= rangeLength; + if (remaining < 0) + { + remaining = 0; + } + } + } + } + } - long minSum = carry.Min; - long maxSum = carry.Max; - ulong mask; - if (remaining == 1 && ((minSum ^ maxSum) & 1) == 0) - { - // known0Len is now requiredUnknownParity to limit registry pressure - known0Len = 1 ^ ((int)minSum & 1) ^ (forced & 1); - if (known0Len != 0) - { - if (chosenIndex >= 0) - { - if (chosenIndex >= seg0Start) - { - bound = chosenIndex - seg0Start; - // runIndex is now word to limit registry pressure - runIndex = bound >> 6; - mask = 1UL << (bound & 63); - knownOne0[runIndex] |= mask; - knownZero0[runIndex] &= ~mask; - } - else - { - bound = chosenIndex - (seg0Start - windowSize); - // runIndex is now word to limit registry pressure - runIndex = bound >> 6; - mask = 1UL << (bound & 63); - knownOne1[runIndex] |= mask; - knownZero1[runIndex] &= ~mask; - } + long minSum = carry.Min; + long maxSum = carry.Max; + ulong mask; + if (remaining == 1 && ((minSum ^ maxSum) & 1) == 0) + { + // known0Len is now requiredUnknownParity to limit registry pressure + known0Len = 1 ^ ((int)minSum & 1) ^ (forced & 1); + if (known0Len != 0) + { + if (chosenIndex >= 0) + { + if (chosenIndex >= seg0Start) + { + bound = chosenIndex - seg0Start; + // runIndex is now word to limit registry pressure + runIndex = bound >> 6; + mask = 1UL << (bound & 63); + knownOne0[runIndex] |= mask; + knownZero0[runIndex] &= ~mask; + } + else + { + bound = chosenIndex - (seg0Start - windowSize); + // runIndex is now word to limit registry pressure + runIndex = bound >> 6; + mask = 1UL << (bound & 63); + knownOne1[runIndex] |= mask; + knownZero1[runIndex] &= ~mask; + } - forced++; - remaining = 0; - if (chosenIndex > maxKnownA) - { - maxKnownA = chosenIndex; - } - if (chosenIndex == topIndex0) - { - if (top0KnownZero) - { + forced++; + remaining = 0; + if (chosenIndex > maxKnownA) + { + maxKnownA = chosenIndex; + } + if (chosenIndex == topIndex0) + { + if (top0KnownZero) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } + return false; + } - top0KnownOne = true; - // topChanged = true; - } - else if (chosenIndex == topIndex1) - { - if (top1KnownZero) - { + top0KnownOne = true; + topChanged = true; + } + else if (chosenIndex == topIndex1) + { + if (top1KnownZero) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } + return false; + } - top1KnownOne = true; - // topChanged = true; - } - } - } - else - { - // if (_debugEnabled && _parityZeroLogCount < 8) - // { - // _parityZeroLogCount++; - // Console.WriteLine($"[bit-contradiction] unknown==1 parity forces zero at column={column} carry=[{minSum},{maxSum}] forced={forced} chosenIndex={chosenIndex}"); - // } + top1KnownOne = true; + topChanged = true; + } + } + } + else + { + // if (_debugEnabled && _parityZeroLogCount < 8) + // { + // _parityZeroLogCount++; + // Console.WriteLine($"[bit-contradiction] unknown==1 parity forces zero at column={column} carry=[{minSum},{maxSum}] forced={forced} chosenIndex={chosenIndex}"); + // } - // Treat the single unknown as 0 for parity. - remaining = 0; + // Treat the single unknown as 0 for parity. + remaining = 0; - if (chosenIndex == topIndex0) - { - if (top0KnownOne) - { + if (chosenIndex == topIndex0) + { + if (top0KnownOne) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } + return false; + } - top0KnownZero = true; - } - else if (chosenIndex == topIndex1) - { - if (top1KnownOne) - { + top0KnownZero = true; + } + else if (chosenIndex == topIndex1) + { + if (top1KnownOne) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } + return false; + } - top1KnownZero = true; - } + top1KnownZero = true; + } - UpdateZeroTailFromTop(ref zeroTailStart, topIndex0, topIndex1, top0KnownZero, top1KnownZero); - } - } + UpdateZeroTailFromTop(ref zeroTailStart, topIndex0, topIndex1, top0KnownZero, top1KnownZero); + } + } - // if (topChanged) - // { - // var qHash = ComputeQOffsetsHash(qOneOffsets); - // if (!TryDynamicModularRangePrune(qOneOffsets, qHash, prime, maxAllowedA, top0KnownOne, top0KnownZero, top1KnownOne, zeroTailStart)) - // { - // #if DETAILED_LOG - // reason = ContradictionReason.ParityUnreachable; - // #endif - // return false; - // } - // } + topChanged = topChanged || + oldTop0KnownOne != top0KnownOne || + oldTop1KnownOne != top1KnownOne || + oldTop0KnownZero != top0KnownZero || + oldTop1KnownZero != top1KnownZero || + oldZeroTailStart != zeroTailStart; - if ((top0KnownZero && top0KnownOne) || (top1KnownZero && top1KnownOne)) - { + bool runDynamicModPrune = topChanged || ((startColumn & DynamicModPeriodicMask) == 0); + if (runDynamicModPrune) + { + if (!TryDynamicModularRangePrune(qOneOffsets, qHash, qExact, prime, globalKnownMinA, globalKnownMaxA, globalKnownOneIndices, globalKnownZeroIndices, maxAllowedA, top0KnownOne, top0KnownZero, top1KnownOne, zeroTailStart, topPrefixKnownBits, topPrefixValue)) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTryDynamicModularRangePrune); +#endif + return false; + } + } - if (topIndex1 < 0) - { - if (top0KnownZero) - { + if ((top0KnownZero && top0KnownOne) || (top1KnownZero && top1KnownOne)) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } - } - else if (top0KnownZero && top1KnownZero) - { +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTopStateConflict); +#endif + return false; + } + + if (topIndex1 < 0) + { + if (top0KnownZero) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } - - if (remaining == 0) - { - // known0Len is now requiredCarryParity to limit registry pressure - known0Len = 1 ^ (forced & 1); - long carryMin = AlignUpToParity(carry.Min, known0Len); - long carryMax = AlignDownToParity(carry.Max, known0Len); - if (carryMin > carryMax) - { +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTopBothZeroConflict); +#endif + return false; + } + } + else if (top0KnownZero && top1KnownZero) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithTopBothZeroConflict); +#endif + return false; + } - carry = new CarryRange(carryMin, carryMax); - minSum = carryMin; - maxSum = carryMax; - } - - minSum += forced; - maxSum += forced + remaining; - const int requiredParity = 1; - - if (minSum == maxSum) - { - if ((minSum & 1) != requiredParity) - { + if (remaining == 0) + { + // known0Len is now requiredCarryParity to limit registry pressure + known0Len = 1 ^ (forced & 1); + long carryMin = AlignUpToParity(carry.Min, known0Len); + long carryMax = AlignDownToParity(carry.Max, known0Len); + if (carryMin > carryMax) + { #if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; + reason = ContradictionReason.ParityUnreachable; #endif - return false; - } +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithCarryParityPrecheck); +#endif + return false; + } - minSum = (minSum - requiredParity) >> 1; - carry = CarryRange.Single(minSum); - } - else - { - if ((minSum & 1) != requiredParity && remaining == 0) - { -#if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; -#endif - return false; - } + carry = new CarryRange(carryMin, carryMax); + minSum = carryMin; + maxSum = carryMax; + } - if (!TryPropagateCarry( - ref carry, - forced, - forced + remaining, - requiredParity)) - { -#if DETAILED_LOG - reason = ContradictionReason.ParityUnreachable; -#endif - return false; - } - } + minSum += forced; + maxSum += forced + remaining; + const int requiredParity = 1; - startColumn++; + if (minSum == maxSum) + { + if ((minSum & 1) != requiredParity) + { #if DETAILED_LOG - _statScalarCols++; + reason = ContradictionReason.ParityUnreachable; #endif - } +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithCarryParityPrecheck); +#endif + return false; + } + + minSum = (minSum - requiredParity) >> 1; + carry = CarryRange.Single(minSum); + } + else + { + if ((minSum & 1) != requiredParity && remaining == 0) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif +#if WITH_PRUNE_STATS + IncrementPruneCounter(ref _prunedWithCarryParityPrecheck); +#endif + return false; + } + + if (!TryPropagateCarry( + ref carry, + forced, + forced + remaining, + requiredParity)) + { +#if DETAILED_LOG + reason = ContradictionReason.ParityUnreachable; +#endif + return false; + } + } + + startColumn++; +#if DETAILED_LOG + _statScalarCols++; +#endif + } #if DETAILED_LOG - reason = ContradictionReason.None; + reason = ContradictionReason.None; #endif - return true; - } + return true; + } #if DETAILED_LOG - private static bool TryProcessTopDownBlock( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - int maxAllowedA, - int startHighColumn, - int columnCount, - CarryRange carryOut, - ref int windowStart, - ref int windowEnd, - out CarryRange nextCarryOut, - out TopDownPruneFailure? failure) + private static bool TryProcessTopDownBlock( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + int maxAllowedA, + int startHighColumn, + int columnCount, + CarryRange carryOut, + ref int windowStart, + ref int windowEnd, + out CarryRange nextCarryOut, + out TopDownPruneFailure? failure) #else - private static bool TryProcessTopDownBlock( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - int maxAllowedA, - int startHighColumn, - int columnCount, - CarryRange carryOut, - ref int windowStart, - ref int windowEnd, - out CarryRange nextCarryOut) + private static bool TryProcessTopDownBlock( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + int maxAllowedA, + int startHighColumn, + int columnCount, + CarryRange carryOut, + ref int windowStart, + ref int windowEnd, + out CarryRange nextCarryOut) #endif - { + { #if DETAILED_LOG - failure = null; + failure = null; #endif - long carryOutMin = carryOut.Min, - carryOutMax = carryOut.Max; - int value; - int endColumn = startHighColumn - columnCount + 1; + long carryOutMin = carryOut.Min, + carryOutMax = carryOut.Max; + int value; + int endColumn = startHighColumn - columnCount + 1; - int column = startHighColumn; - while (column >= endColumn) - { - // value is used as high column index - value = column; - while (windowEnd > 0 && qOneOffsets[windowEnd - 1] > value) - { - windowEnd--; - } + int column = startHighColumn; + while (column >= endColumn) + { + // value is used as high column index + value = column; + while (windowEnd > 0 && qOneOffsets[windowEnd - 1] > value) + { + windowEnd--; + } - // value is used as low column index - value = column - maxAllowedA; - if (value < 0) - { - value = 0; - } + // value is used as low column index + value = column - maxAllowedA; + if (value < 0) + { + value = 0; + } - while (windowStart > 0 && qOneOffsets[windowStart - 1] >= value) - { - windowStart--; - } + while (windowStart > 0 && qOneOffsets[windowStart - 1] >= value) + { + windowStart--; + } - if (windowStart > windowEnd) - { - windowStart = windowEnd; - } + if (windowStart > windowEnd) + { + windowStart = windowEnd; + } - // value is unknown bits count here - value = windowEnd - windowStart; - if (value == 0) - { - int lastEnd = windowEnd > 0 ? qOneOffsets[windowEnd - 1] : int.MinValue; - int lastStart = windowStart > 0 ? qOneOffsets[windowStart - 1] + maxAllowedA : int.MinValue; - int chunkEnd = lastEnd > lastStart ? lastEnd : lastStart; - if (chunkEnd < endColumn) - { - chunkEnd = endColumn; - } + // value is unknown bits count here + value = windowEnd - windowStart; + if (value == 0) + { + int lastEnd = windowEnd > 0 ? qOneOffsets[windowEnd - 1] : int.MinValue; + int lastStart = windowStart > 0 ? qOneOffsets[windowStart - 1] + maxAllowedA : int.MinValue; + int chunkEnd = lastEnd > lastStart ? lastEnd : lastStart; + if (chunkEnd < endColumn) + { + chunkEnd = endColumn; + } - int steps = column - chunkEnd + 1; - if (steps > 1) - { - if (!AdvanceTopDownUnknown0(ref carryOutMin, ref carryOutMax, steps)) - { + int steps = column - chunkEnd + 1; + if (steps > 1) + { + if (!AdvanceTopDownUnknown0(ref carryOutMin, ref carryOutMax, steps)) + { #if DETAILED_LOG - failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); + failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); #endif - nextCarryOut = default; - return false; - } + nextCarryOut = default; + return false; + } - column = chunkEnd - 1; - continue; - } - } - else if (value == 1) - { - int lastEnd = windowEnd > 0 ? qOneOffsets[windowEnd - 1] : int.MinValue; - int lastStart = windowStart > 0 ? qOneOffsets[windowStart - 1] + maxAllowedA : int.MinValue; - int chunkEnd = lastEnd > lastStart ? lastEnd : lastStart; - if (chunkEnd < endColumn) - { - chunkEnd = endColumn; - } + column = chunkEnd - 1; + continue; + } + } + else if (value == 1) + { + int lastEnd = windowEnd > 0 ? qOneOffsets[windowEnd - 1] : int.MinValue; + int lastStart = windowStart > 0 ? qOneOffsets[windowStart - 1] + maxAllowedA : int.MinValue; + int chunkEnd = lastEnd > lastStart ? lastEnd : lastStart; + if (chunkEnd < endColumn) + { + chunkEnd = endColumn; + } - int steps = (int)(column - chunkEnd + 1); - if (steps > 1) - { - if (!AdvanceTopDownUnknown1(ref carryOutMin, ref carryOutMax, steps)) - { + int steps = (int)(column - chunkEnd + 1); + if (steps > 1) + { + if (!AdvanceTopDownUnknown1(ref carryOutMin, ref carryOutMax, steps)) + { #if DETAILED_LOG - failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); + failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); #endif - nextCarryOut = default; - return false; - } + nextCarryOut = default; + return false; + } - column = chunkEnd - 1; - continue; - } - } + column = chunkEnd - 1; + continue; + } + } - // carryOutMin now becomes nextCarryMin to limit registry pressure - carryOutMin = (carryOutMin << 1) + 1 - value; - // carryOutMax now becomes nextCarryMax to limit registry pressure - carryOutMax = (carryOutMax << 1) + 1; - if (carryOutMin < 0) - { - carryOutMin = 0; - } + // carryOutMin now becomes nextCarryMin to limit registry pressure + carryOutMin = (carryOutMin << 1) + 1 - value; + // carryOutMax now becomes nextCarryMax to limit registry pressure + carryOutMax = (carryOutMax << 1) + 1; + if (carryOutMin < 0) + { + carryOutMin = 0; + } - if (carryOutMax < 0) - { - carryOutMax = 0; - } + if (carryOutMax < 0) + { + carryOutMax = 0; + } - if (carryOutMin > carryOutMax) - { + if (carryOutMin > carryOutMax) + { #if DETAILED_LOG - failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); + failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); #endif - nextCarryOut = default; - return false; - } + nextCarryOut = default; + return false; + } - column--; - } + column--; + } - nextCarryOut = new CarryRange(carryOutMin, carryOutMax); - return true; - } + nextCarryOut = new CarryRange(carryOutMin, carryOutMax); + return true; + } - private static long AlignUpToParity(long value, int parity) => (value & 1L) == parity ? value : value + 1L; - private static long AlignDownToParity(long value, int parity) => (value & 1L) == parity ? value : value - 1L; + private static long AlignUpToParity(long value, int parity) => (value & 1L) == parity ? value : value + 1L; + private static long AlignDownToParity(long value, int parity) => (value & 1L) == parity ? value : value - 1L; #if DETAILED_LOG - private static bool TryTopDownCarryPrune( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - int pLong, - int maxAllowedA, - out TopDownPruneFailure? failure) + private static bool TryTopDownCarryPrune( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + int pLong, + int maxAllowedA, + out TopDownPruneFailure? failure) #else - private static bool TryTopDownCarryPrune( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - int pLong, - int maxAllowedA) + private static bool TryTopDownCarryPrune( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + int pLong, + int maxAllowedA) #endif - { + { #if DETAILED_LOG - failure = null; + failure = null; #endif - int windowStart = qOneOffsetsLength; - int windowEnd = qOneOffsetsLength; - long carryOutMin = 0, - carryOutMax = 0; - int value; + int windowStart = qOneOffsetsLength; + int windowEnd = qOneOffsetsLength; + long carryOutMin = 0, + carryOutMax = 0; + int value; - int column = pLong - 1; - while (column >= 0) - { - // value is used as high column index - value = column; - while (windowEnd > 0 && qOneOffsets[windowEnd - 1] > value) - { - windowEnd--; - } + int column = pLong - 1; + while (column >= 0) + { + // value is used as high column index + value = column; + while (windowEnd > 0 && qOneOffsets[windowEnd - 1] > value) + { + windowEnd--; + } - // value is used as low column index - value = column - maxAllowedA; - if (value < 0) - { - value = 0; - } + // value is used as low column index + value = column - maxAllowedA; + if (value < 0) + { + value = 0; + } - while (windowStart > 0 && qOneOffsets[windowStart - 1] >= value) - { - windowStart--; - } + while (windowStart > 0 && qOneOffsets[windowStart - 1] >= value) + { + windowStart--; + } - if (windowStart > windowEnd) - { - windowStart = windowEnd; - } + if (windowStart > windowEnd) + { + windowStart = windowEnd; + } - // value is used as unknown bits count here - value = windowEnd - windowStart; - if (value == 0) - { - int lastEnd = windowEnd > 0 ? qOneOffsets[windowEnd - 1] : int.MinValue; - int lastStart = windowStart > 0 ? qOneOffsets[windowStart - 1] + maxAllowedA : int.MinValue; - int chunkEnd = lastEnd > lastStart ? lastEnd : lastStart; - if (chunkEnd < 0) - { - chunkEnd = 0; - } + // value is used as unknown bits count here + value = windowEnd - windowStart; + if (value == 0) + { + int lastEnd = windowEnd > 0 ? qOneOffsets[windowEnd - 1] : int.MinValue; + int lastStart = windowStart > 0 ? qOneOffsets[windowStart - 1] + maxAllowedA : int.MinValue; + int chunkEnd = lastEnd > lastStart ? lastEnd : lastStart; + if (chunkEnd < 0) + { + chunkEnd = 0; + } - int steps = (int)(column - chunkEnd + 1); - if (steps > 1) - { - if (!AdvanceTopDownUnknown0(ref carryOutMin, ref carryOutMax, steps)) - { + int steps = (int)(column - chunkEnd + 1); + if (steps > 1) + { + if (!AdvanceTopDownUnknown0(ref carryOutMin, ref carryOutMax, steps)) + { #if DETAILED_LOG - failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); + failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); #endif - return false; - } + return false; + } - column = chunkEnd - 1; - continue; - } - } - else if (value == 1) - { - int lastEnd = windowEnd > 0 ? qOneOffsets[windowEnd - 1] : int.MinValue; - int lastStart = windowStart > 0 ? qOneOffsets[windowStart - 1] + maxAllowedA : int.MinValue; - int chunkEnd = lastEnd > lastStart ? lastEnd : lastStart; - if (chunkEnd < 0) - { - chunkEnd = 0; - } + column = chunkEnd - 1; + continue; + } + } + else if (value == 1) + { + int lastEnd = windowEnd > 0 ? qOneOffsets[windowEnd - 1] : int.MinValue; + int lastStart = windowStart > 0 ? qOneOffsets[windowStart - 1] + maxAllowedA : int.MinValue; + int chunkEnd = lastEnd > lastStart ? lastEnd : lastStart; + if (chunkEnd < 0) + { + chunkEnd = 0; + } - int steps = (int)(column - chunkEnd + 1); - if (steps > 1) - { - if (!AdvanceTopDownUnknown1(ref carryOutMin, ref carryOutMax, steps)) - { + int steps = (int)(column - chunkEnd + 1); + if (steps > 1) + { + if (!AdvanceTopDownUnknown1(ref carryOutMin, ref carryOutMax, steps)) + { #if DETAILED_LOG - failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); + failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); #endif - return false; - } + return false; + } - column = chunkEnd - 1; - continue; - } - } + column = chunkEnd - 1; + continue; + } + } - // carryOutMin now becomes nextCarryMin to limit registry pressure - carryOutMin = (carryOutMin << 1) + 1 - value; - // carryOutMax now becomes nextCarryMax to limit registry pressure - carryOutMax = (carryOutMax << 1) + 1; - if (carryOutMin < 0) - { - carryOutMin = 0; - } + // carryOutMin now becomes nextCarryMin to limit registry pressure + carryOutMin = (carryOutMin << 1) + 1 - value; + // carryOutMax now becomes nextCarryMax to limit registry pressure + carryOutMax = (carryOutMax << 1) + 1; + if (carryOutMin < 0) + { + carryOutMin = 0; + } - if (carryOutMax < 0) - { - carryOutMax = 0; - } + if (carryOutMax < 0) + { + carryOutMax = 0; + } - if (carryOutMin > carryOutMax) - { + if (carryOutMin > carryOutMax) + { #if DETAILED_LOG - failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); + failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value); #endif - return false; - } + return false; + } - column--; - } + column--; + } - if (carryOutMin > 0) - { + if (carryOutMin > 0) + { #if DETAILED_LOG - failure = new TopDownPruneFailure(0, carryOutMin, carryOutMax, 0); + failure = new TopDownPruneFailure(0, carryOutMin, carryOutMax, 0); #endif - return false; - } + return false; + } - return true; - } + return true; + } #if DETAILED_LOG - private static bool TryTopDownBorrowPrefilter( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - int pLong, - int maxAllowedA, - out TopDownPruneFailure? failure) + private static bool TryTopDownBorrowPrefilter( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + int pLong, + int maxAllowedA, + out TopDownPruneFailure? failure) #else - private static bool TryTopDownBorrowPrefilter( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - int pLong, - int maxAllowedA) + private static bool TryTopDownBorrowPrefilter( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + int pLong, + int maxAllowedA) #endif - { + { #if DETAILED_LOG - failure = null; + failure = null; #endif - CarryRange borrow = CarryRange.Zero; - int windowStart = qOneOffsetsLength; - int windowEnd = qOneOffsetsLength; + CarryRange borrow = CarryRange.Zero; + int windowStart = qOneOffsetsLength; + int windowEnd = qOneOffsetsLength; - int column = pLong - 1; - int endColumn = column - (TopDownBorrowColumns - 1); - if (endColumn < 0) - { - endColumn = 0; - } + int column = pLong - 1; + int endColumn = column - (TopDownBorrowColumns - 1); + if (endColumn < 0) + { + endColumn = 0; + } - while (column >= endColumn) - { - int value = column; - while (windowEnd > 0 && qOneOffsets[windowEnd - 1] > value) - { - windowEnd--; - } + while (column >= endColumn) + { + int value = column; + while (windowEnd > 0 && qOneOffsets[windowEnd - 1] > value) + { + windowEnd--; + } - value = column - maxAllowedA; - if (value < 0) - { - value = 0; - } + value = column - maxAllowedA; + if (value < 0) + { + value = 0; + } - while (windowStart > 0 && qOneOffsets[windowStart - 1] >= value) - { - windowStart--; - } + while (windowStart > 0 && qOneOffsets[windowStart - 1] >= value) + { + windowStart--; + } - if (windowStart > windowEnd) - { - windowStart = windowEnd; - } + if (windowStart > windowEnd) + { + windowStart = windowEnd; + } - int unknown = windowEnd - windowStart; - if (!TryPropagateCarry(ref borrow, 0, unknown, 1)) - { + int unknown = windowEnd - windowStart; + if (!TryPropagateCarry(ref borrow, 0, unknown, 1)) + { #if DETAILED_LOG - failure = new TopDownPruneFailure(column, borrow.Min, borrow.Max, unknown); + failure = new TopDownPruneFailure(column, borrow.Min, borrow.Max, unknown); #endif - return false; - } + return false; + } - column--; - } + column--; + } - return true; - } + return true; + } - private static bool ShouldRunTopDownBorrowPrefilter( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - long pLong, - long maxAllowedA) - { - if (qOneOffsetsLength < TopDownBorrowMinUnknown) - { - return false; - } + private static bool ShouldRunTopDownBorrowPrefilter( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + long pLong, + long maxAllowedA) + { + if (qOneOffsetsLength < TopDownBorrowMinUnknown) + { + return false; + } - long column = pLong - 1; - long start = column - maxAllowedA; - if (start < 0) - { - start = 0; - } + long column = pLong - 1; + long start = column - maxAllowedA; + if (start < 0) + { + start = 0; + } - FindBounds(qOneOffsets, (int)start, (int)column, out int lower, out int upper); - return upper - lower >= TopDownBorrowMinUnknown; - } + FindBounds(qOneOffsets, (int)start, (int)column, out int lower, out int upper); + return upper - lower >= TopDownBorrowMinUnknown; + } - private static bool AdvanceTopDownUnknown1(ref long carryOutMin, ref long carryOutMax, int steps) - { - while (steps > 0) - { - int step = steps > 30 ? 30 : steps; - int pow = 1 << step; + private static bool AdvanceTopDownUnknown1(ref long carryOutMin, ref long carryOutMax, int steps) + { + while (steps > 0) + { + int step = steps > 30 ? 30 : steps; + int pow = 1 << step; - if (carryOutMin > (int.MaxValue >> step) || carryOutMax > ((int.MaxValue - (pow - 1)) >> step)) - { - carryOutMin = 0; - carryOutMax = int.MaxValue; - return true; - } + if (carryOutMin > (int.MaxValue >> step) || carryOutMax > ((int.MaxValue - (pow - 1)) >> step)) + { + carryOutMin = 0; + carryOutMax = int.MaxValue; + return true; + } - carryOutMin <<= step; - carryOutMax = (carryOutMax << step) + (pow - 1); - steps -= step; - } + carryOutMin <<= step; + carryOutMax = (carryOutMax << step) + (pow - 1); + steps -= step; + } - return true; - } + return true; + } - private static bool AdvanceTopDownUnknown0(ref long carryOutMin, ref long carryOutMax, int steps) - { - while (steps > 0) - { - int step = steps > 30 ? 30 : steps; - int add = (1 << step) - 1; - if (carryOutMin > ((int.MaxValue - add) >> step) || carryOutMax > ((int.MaxValue - add) >> step)) - { - carryOutMin = 0; - carryOutMax = int.MaxValue; - return true; - } + private static bool AdvanceTopDownUnknown0(ref long carryOutMin, ref long carryOutMax, int steps) + { + while (steps > 0) + { + int step = steps > 30 ? 30 : steps; + int add = (1 << step) - 1; + if (carryOutMin > ((int.MaxValue - add) >> step) || carryOutMax > ((int.MaxValue - add) >> step)) + { + carryOutMin = 0; + carryOutMax = int.MaxValue; + return true; + } - carryOutMin = (carryOutMin << step) + add; - carryOutMax = (carryOutMax << step) + add; - steps -= step; - } + carryOutMin = (carryOutMin << step) + add; + carryOutMax = (carryOutMax << step) + add; + steps -= step; + } - return true; - } + return true; + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static int CountBitsInRange(in ulong[] bits, int start, int length) - { - if (length <= 0) - { - return 0; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static int CountBitsInRange(in ulong[] bits, int start, int length) + { + if (length <= 0) + { + return 0; + } - length += start - 1; - int firstWord = start >> 6; - int lastWord = length >> 6; - start &= 63; - length &= 63; - ulong mask; + length += start - 1; + int firstWord = start >> 6; + int lastWord = length >> 6; + start &= 63; + length &= 63; + ulong mask; - if (firstWord == lastWord) - { - mask = (length == 63 ? ulong.MaxValue : ((1UL << (length + 1)) - 1UL)) & (ulong.MaxValue << start); - return PopCount(bits[firstWord] & mask); - } + if (firstWord == lastWord) + { + mask = (length == 63 ? ulong.MaxValue : ((1UL << (length + 1)) - 1UL)) & (ulong.MaxValue << start); + return PopCount(bits[firstWord] & mask); + } - mask = ulong.MaxValue << start; - // start is count from here. We're reusing the variable to limit registry pressure. - start = PopCount(bits[firstWord] & mask); + mask = ulong.MaxValue << start; + // start is count from here. We're reusing the variable to limit registry pressure. + start = PopCount(bits[firstWord] & mask); - firstWord++; - for (; firstWord < lastWord; firstWord++) - { - start += PopCount(bits[firstWord]); - } + firstWord++; + for (; firstWord < lastWord; firstWord++) + { + start += PopCount(bits[firstWord]); + } - mask = length == 63 ? ulong.MaxValue : ((1UL << (length + 1)) - 1UL); - start += PopCount(bits[lastWord] & mask); - return start; - } + mask = length == 63 ? ulong.MaxValue : ((1UL << (length + 1)) - 1UL); + start += PopCount(bits[lastWord] & mask); + return start; + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static bool TryFindFirstUnknown(in ulong[] knownOne, in ulong[] knownZero, int start, int length, out int index) - { - if (length <= 0) - { - index = -1; - return false; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static bool TryFindFirstUnknown(in ulong[] knownOne, in ulong[] knownZero, int start, int length, out int index) + { + if (length <= 0) + { + index = -1; + return false; + } - int end = start + length - 1; - int firstWord = start >> 6; - int lastWord = end >> 6; - int startBit = start & 63; - int endBit = end & 63; + int end = start + length - 1; + int firstWord = start >> 6; + int lastWord = end >> 6; + int startBit = start & 63; + int endBit = end & 63; - ulong firstMask = ulong.MaxValue << startBit; - ulong lastMask = endBit == 63 ? ulong.MaxValue : ((1UL << (endBit + 1)) - 1UL); + ulong firstMask = ulong.MaxValue << startBit; + ulong lastMask = endBit == 63 ? ulong.MaxValue : ((1UL << (endBit + 1)) - 1UL); - for (int word = firstWord; word <= lastWord; word++) - { - ulong mask = word == firstWord ? firstMask : ulong.MaxValue; - if (word == lastWord) - { - mask &= lastMask; - } + for (int word = firstWord; word <= lastWord; word++) + { + ulong mask = word == firstWord ? firstMask : ulong.MaxValue; + if (word == lastWord) + { + mask &= lastMask; + } - ulong known = (knownOne[word] | knownZero[word]) & mask; - ulong unknown = mask & ~known; - if (unknown != 0) - { - int bit = BitOperations.TrailingZeroCount(unknown); - index = (word << 6) + bit; - return true; - } - } + ulong known = (knownOne[word] | knownZero[word]) & mask; + ulong unknown = mask & ~known; + if (unknown != 0) + { + int bit = BitOperations.TrailingZeroCount(unknown); + index = (word << 6) + bit; + return true; + } + } - index = -1; - return false; - } + index = -1; + return false; + } - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private static void UpdateZeroTailFromTop(ref int zeroTailStart, int topIndex0, int topIndex1, bool top0KnownZero, bool top1KnownZero) - { - if (!top0KnownZero) - { - return; - } + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private static void UpdateZeroTailFromTop(ref int zeroTailStart, int topIndex0, int topIndex1, bool top0KnownZero, bool top1KnownZero) + { + if (!top0KnownZero) + { + return; + } - if (zeroTailStart > topIndex0) - { - zeroTailStart = topIndex0; - } + if (zeroTailStart > topIndex0) + { + zeroTailStart = topIndex0; + } - if (top1KnownZero && topIndex1 == topIndex0 - 1 && zeroTailStart > topIndex1) - { - zeroTailStart = topIndex1; - } - } + if (top1KnownZero && topIndex1 == topIndex0 - 1 && zeroTailStart > topIndex1) + { + zeroTailStart = topIndex1; + } + } #if DETAILED_LOG - private static bool TryRunHighBitAndBorrowPrefiltersCombined( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - int pLong, - int maxAllowedA, - out TopDownPruneFailure? failure) + private static bool TryRunHighBitAndBorrowPrefiltersCombined( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + int pLong, + int maxAllowedA, + out TopDownPruneFailure? failure) #else - private static bool TryRunHighBitAndBorrowPrefiltersCombined( - ReadOnlySpan qOneOffsets, - int qOneOffsetsLength, - int pLong, - int maxAllowedA) + private static bool TryRunHighBitAndBorrowPrefiltersCombined( + ReadOnlySpan qOneOffsets, + int qOneOffsetsLength, + int pLong, + int maxAllowedA) #endif - { + { #if DETAILED_LOG - failure = null; + failure = null; #endif - int column = pLong - 1, - columnPlusOne = column + 1; + int column = pLong - 1, + columnPlusOne = column + 1; - int highBitColumns = HighBitCarryPrefilterColumns; - if (highBitColumns > columnPlusOne) - { - highBitColumns = columnPlusOne; - } + int highBitColumns = HighBitCarryPrefilterColumns; + if (highBitColumns > columnPlusOne) + { + highBitColumns = columnPlusOne; + } - int borrowColumns = 0; - bool runBorrowPrefilter = qOneOffsetsLength >= TopDownBorrowMinUnknown; - if (runBorrowPrefilter) - { - borrowColumns = TopDownBorrowColumns; - if (borrowColumns > columnPlusOne) - { - borrowColumns = columnPlusOne; - } - } + int borrowColumns = 0; + bool runBorrowPrefilter = qOneOffsetsLength >= TopDownBorrowMinUnknown; + if (runBorrowPrefilter) + { + borrowColumns = TopDownBorrowColumns; + if (borrowColumns > columnPlusOne) + { + borrowColumns = columnPlusOne; + } + } - int sequentialColumns = highBitColumns > borrowColumns ? highBitColumns : borrowColumns; - // Given the above, sequentialColumns will never <= 0, because highBitColumns is always > 0. - // if (sequentialColumns <= 0) - // { - // return true; - // } + int sequentialColumns = highBitColumns > borrowColumns ? highBitColumns : borrowColumns; + // Given the above, sequentialColumns will never <= 0, because highBitColumns is always > 0. + // if (sequentialColumns <= 0) + // { + // return true; + // } - Span lo0 = stackalloc long[64]; - Span hi0 = stackalloc long[64]; - Span lo1 = stackalloc long[64]; - Span hi1 = stackalloc long[64]; + Span lo0 = stackalloc long[64]; + Span hi0 = stackalloc long[64]; + Span lo1 = stackalloc long[64]; + Span hi1 = stackalloc long[64]; - Span outLo = lo0, outHi = hi0; - Span inLo = lo1, inHi = hi1; + Span outLo = lo0, outHi = hi0; + Span inLo = lo1, inHi = hi1; - int outCount = 1; - outLo[0] = 0; - outHi[0] = 0; + int outCount = 1; + outLo[0] = 0; + outHi[0] = 0; - int inCount = 0; - bool flip = false; - CarryRange borrow = CarryRange.Zero; + int inCount = 0; + bool flip = false; + CarryRange borrow = CarryRange.Zero; - [MethodImpl(MethodImplOptions.AggressiveInlining)] - static void AddInterval(ref int count, Span loArr, Span hiArr, long lo, long hi) - { - if (hi < lo) return; + [MethodImpl(MethodImplOptions.AggressiveInlining)] + static void AddInterval(ref int count, Span loArr, Span hiArr, long lo, long hi) + { + if (hi < lo) return; - if (lo < 0) lo = 0; - if (hi < 0) return; + if (lo < 0) lo = 0; + if (hi < 0) return; - if (count == 0) - { - loArr[0] = lo; - hiArr[0] = hi; - count = 1; - return; - } + if (count == 0) + { + loArr[0] = lo; + hiArr[0] = hi; + count = 1; + return; + } - long lastHi = hiArr[count - 1]; - if (lo <= lastHi + 1) - { - if (hi > lastHi) - hiArr[count - 1] = hi; - return; - } + long lastHi = hiArr[count - 1]; + if (lo <= lastHi + 1) + { + if (hi > lastHi) + hiArr[count - 1] = hi; + return; + } - if ((uint)count >= (uint)loArr.Length) - { - count = 0; - return; - } + if ((uint)count >= (uint)loArr.Length) + { + count = 0; + return; + } - loArr[count] = lo; - hiArr[count] = hi; - count++; - } + loArr[count] = lo; + hiArr[count] = hi; + count++; + } - int step = 0; - int upperT; - int lowerT = column - maxAllowedA; - if (lowerT < 0) - { - lowerT = 0; - } + int step = 0; + int upperT; + int lowerT = column - maxAllowedA; + if (lowerT < 0) + { + lowerT = 0; + } - FindBounds(qOneOffsets, lowerT, column, out lowerT, out upperT); - int n = upperT - lowerT; - if (n < 0) - { - return false; - } + FindBounds(qOneOffsets, lowerT, column, out lowerT, out upperT); + int n = upperT - lowerT; + if (n < 0) + { + return false; + } - if (runBorrowPrefilter && n < TopDownBorrowMinUnknown) - { - runBorrowPrefilter = false; - if (highBitColumns < sequentialColumns) - { - sequentialColumns = highBitColumns; - } - } + if (runBorrowPrefilter && n < TopDownBorrowMinUnknown) + { + runBorrowPrefilter = false; + if (highBitColumns < sequentialColumns) + { + sequentialColumns = highBitColumns; + } + } - while (true) - { - if (step < highBitColumns) - { - // Build carryIn set into inLo/inHi - inCount = 0; + while (true) + { + if (step < highBitColumns) + { + // Build carryIn set into inLo/inHi + inCount = 0; - for (int i = 0; i < outCount; i++) - { - long rMin = outLo[i]; - long rMax = outHi[i]; + for (int i = 0; i < outCount; i++) + { + long rMin = outLo[i]; + long rMax = outHi[i]; - if (rMax < 0) continue; - if (rMin < 0) rMin = 0; - if (rMax < rMin) continue; + if (rMax < 0) continue; + if (rMin < 0) rMin = 0; + if (rMax < rMin) continue; - const long TwicePlusOneOverflowLimit = (long.MaxValue - 1) >> 1; - if (rMin > TwicePlusOneOverflowLimit || rMax > TwicePlusOneOverflowLimit) - { - return true; - } + const long TwicePlusOneOverflowLimit = (long.MaxValue - 1) >> 1; + if (rMin > TwicePlusOneOverflowLimit || rMax > TwicePlusOneOverflowLimit) + { + return true; + } - rMin = (rMin << 1) + 1; - rMax = (rMax << 1) + 1; + rMin = (rMin << 1) + 1; + rMax = (rMax << 1) + 1; - if (n <= 0) - { - AddInterval(ref inCount, inLo, inHi, rMin, rMax); - if (inCount == 0) return true; - continue; - } + if (n <= 0) + { + AddInterval(ref inCount, inLo, inHi, rMin, rMax); + if (inCount == 0) return true; + continue; + } - if (n == 1) - { - AddInterval(ref inCount, inLo, inHi, rMin - 1, rMax); - if (inCount == 0) return true; - continue; - } + if (n == 1) + { + AddInterval(ref inCount, inLo, inHi, rMin - 1, rMax); + if (inCount == 0) return true; + continue; + } - if (rMax <= n) - { - AddInterval(ref inCount, inLo, inHi, 0, rMax); - if (inCount == 0) return true; - } - else if (rMin > n) - { - AddInterval(ref inCount, inLo, inHi, rMin - n, rMax); - if (inCount == 0) return true; - } - else - { - AddInterval(ref inCount, inLo, inHi, 0, rMax); - if (inCount == 0) return true; - } - } + if (rMax <= n) + { + AddInterval(ref inCount, inLo, inHi, 0, rMax); + if (inCount == 0) return true; + } + else if (rMin > n) + { + AddInterval(ref inCount, inLo, inHi, rMin - n, rMax); + if (inCount == 0) return true; + } + else + { + AddInterval(ref inCount, inLo, inHi, 0, rMax); + if (inCount == 0) return true; + } + } - if (inCount <= 0) - { - return false; - } + if (inCount <= 0) + { + return false; + } - // Swap buffers for next step. - outCount = inCount; - flip = !flip; - if (!flip) - { - outLo = lo0; outHi = hi0; - inLo = lo1; inHi = hi1; - } - else - { - outLo = lo1; outHi = hi1; - inLo = lo0; inHi = hi0; - } - } + // Swap buffers for next step. + outCount = inCount; + flip = !flip; + if (!flip) + { + outLo = lo0; outHi = hi0; + inLo = lo1; inHi = hi1; + } + else + { + outLo = lo1; outHi = hi1; + inLo = lo0; inHi = hi0; + } + } - if (runBorrowPrefilter && step < borrowColumns) - { - if (!TryPropagateCarry(ref borrow, 0, n, 1)) - { + if (runBorrowPrefilter && step < borrowColumns) + { + if (!TryPropagateCarry(ref borrow, 0, n, 1)) + { #if DETAILED_LOG - failure = new TopDownPruneFailure(column, borrow.Min, borrow.Max, n); + failure = new TopDownPruneFailure(column, borrow.Min, borrow.Max, n); #endif - return false; - } - } + return false; + } + } - step++; - column--; - if (step >= sequentialColumns || column < 0) - { - break; - } + step++; + column--; + if (step >= sequentialColumns || column < 0) + { + break; + } - lowerT = column - maxAllowedA; - if (lowerT < 0) - { - lowerT = 0; - } + lowerT = column - maxAllowedA; + if (lowerT < 0) + { + lowerT = 0; + } - FindBounds(qOneOffsets, lowerT, column, out lowerT, out upperT); - n = upperT - lowerT; - if (n < 0) - { - return false; - } - } + FindBounds(qOneOffsets, lowerT, column, out lowerT, out upperT); + n = upperT - lowerT; + if (n < 0) + { + return false; + } + } - return true; - } + return true; + } } + + + + + + + + diff --git a/PerfectNumbers.Core/Cpu/MersenneNumberDivisorByDivisorCpuTesterWithTemplate.cs b/PerfectNumbers.Core/Cpu/MersenneNumberDivisorByDivisorCpuTesterWithTemplate.cs index b509eb8..eaa0e71 100644 --- a/PerfectNumbers.Core/Cpu/MersenneNumberDivisorByDivisorCpuTesterWithTemplate.cs +++ b/PerfectNumbers.Core/Cpu/MersenneNumberDivisorByDivisorCpuTesterWithTemplate.cs @@ -1,4 +1,4 @@ -// #define DivisorSet_BitContradiction +// #define DivisorSet_BitContradiction // #define DivisorSet_BitTree // #define DEVICE_GPU @@ -5108,8 +5108,10 @@ public struct MersenneNumberDivisorByDivisorCpuTesterWithTemplate() : IMersenneN while (true) { int remainder8 = (stepMod8 * kRem8 + 1) & 7; +#if DETAILED_LOG if (prime == 138000001UL && divisor == 1209708008767) Console.WriteLine("[HIT] enumerated target q before remainder8 check"); +#endif if (remainder8 != 1 && remainder8 != 7) { @@ -5152,17 +5154,20 @@ public struct MersenneNumberDivisorByDivisorCpuTesterWithTemplate() : IMersenneN } } +#if DETAILED_LOG if (prime == 138000001UL && divisor == 1209708008767) { Console.WriteLine("[HIT] processed target q. Stopping."); Environment.Exit(1); } +#endif + RecordState(currentK); MOVE_NEXT: ContinueOuter: - RecordState(currentK); if (hasLimit && currentK >= maxK) { + RecordState(currentK); break; } @@ -5357,9 +5362,9 @@ public struct MersenneNumberDivisorByDivisorCpuTesterWithTemplate() : IMersenneN ReadOnlySpan oneOffsetsSlice = oneOffsets[..oneCount]; // BitContradictionSolverWithQMultiplier.SetDebugEnabled(true); #if DETAILED_LOG - bool decided = BitContradictionSolverWithAMultiplier.TryCheckDivisibilityFromOneOffsets(oneOffsetsSlice, prime, currentK, isPowerOfTwo, out divides, out var reason); + bool decided = BitContradictionSolverWithAMultiplier.TryCheckDivisibilityFromOneOffsets(oneOffsetsSlice, prime, divisor, currentK, isPowerOfTwo, out divides, out var reason); #else - bool decided = BitContradictionSolverWithAMultiplier.TryCheckDivisibilityFromOneOffsets(oneOffsetsSlice, prime, currentK, isPowerOfTwo, out divides); + bool decided = BitContradictionSolverWithAMultiplier.TryCheckDivisibilityFromOneOffsets(oneOffsetsSlice, prime, divisor, currentK, isPowerOfTwo, out divides); #endif // BitContradictionSolverWithQMultiplier.SetDebugEnabled(false); if (decided && divides) diff --git a/PerfectNumbers.Core/PerfectNumberConstants.cs b/PerfectNumbers.Core/PerfectNumberConstants.cs index 468e237..008ecc4 100644 --- a/PerfectNumbers.Core/PerfectNumberConstants.cs +++ b/PerfectNumbers.Core/PerfectNumberConstants.cs @@ -21,12 +21,14 @@ public static class PerfectNumberConstants public const int PooledArrayThreshold = 64; public const int Pow2WindowSize = 8; public const int RollingAccelerators = 298; - public const int ThreadsByAccelerator = 128; - public const int ByDivisorStateSaveInterval = 1_000; + public const int ThreadsByAccelerator = 4; + public const int ByDivisorFlushAndEvictInterval = 5; + public const int ByDivisorStateSaveInterval = 10_000_000; public const string ByDivisorStateDirectory = "Checks"; public const int PollardRhoMilliseconds = 100; public const int ByDivisorMersenneTailCount = 8; public const int ByDivisorMersenneBitLimit = 4096; + public const int BitContradictionForcedALowBits = 4096; public const int BitContradictionGpuBatchCount = 16; // public const int BitContradictionGpuBatchCount = 512; // public const int BitContradictionGpuBatchCount = 131_072; diff --git a/PerfectNumbers.Core/PerfectNumbers.Core.csproj b/PerfectNumbers.Core/PerfectNumbers.Core.csproj index 4f581ba..1cfe9d9 100644 --- a/PerfectNumbers.Core/PerfectNumbers.Core.csproj +++ b/PerfectNumbers.Core/PerfectNumbers.Core.csproj @@ -13,6 +13,7 @@ + diff --git a/PerfectNumbers.Core/Persistence/KStateRepository.cs b/PerfectNumbers.Core/Persistence/KStateRepository.cs index 2a8bd38..7207b59 100644 --- a/PerfectNumbers.Core/Persistence/KStateRepository.cs +++ b/PerfectNumbers.Core/Persistence/KStateRepository.cs @@ -68,12 +68,15 @@ public sealed class KStateRepository : IDisposable session.Upsert(keyString, valueString); session.CompletePending(true); var flushCount = ++_flushCount; - if (flushCount >= PerfectNumberConstants.ByDivisorStateSaveInterval) + if (flushCount >= PerfectNumberConstants.ByDivisorFlushAndEvictInterval) { _flushCount = 0; _store.Log.FlushAndEvict(wait: true); } - + else + { + _store.Log.Flush(wait: false); + } } public bool TryGet(ulong prime, out BigInteger value) diff --git a/PerfectNumbers.Core/Pow2Provider.cs b/PerfectNumbers.Core/Pow2Provider.cs index a788278..0359dd6 100644 --- a/PerfectNumbers.Core/Pow2Provider.cs +++ b/PerfectNumbers.Core/Pow2Provider.cs @@ -70,6 +70,7 @@ namespace PerfectNumbers.Core 61 => BigIntegerNumbers.Pow2Exact61, 62 => BigIntegerNumbers.Pow2Exact62, 63 => BigIntegerNumbers.Pow2Exact63, + _ when i >= 0 => System.Numerics.BigInteger.One << i, _ => throw new ArgumentOutOfRangeException(nameof(i), $"Parameter value {i} is incorrect"), }; @@ -140,7 +141,8 @@ namespace PerfectNumbers.Core 62 => BigIntegerNumbers.Pow2MinusOne62, 63 => BigIntegerNumbers.Pow2MinusOne63, 1024 => BigIntegerNumbers.Pow2MinusOne1024, + _ when i >= 0 => (System.Numerics.BigInteger.One << i) - System.Numerics.BigInteger.One, _ => throw new ArgumentOutOfRangeException(nameof(i), $"Parameter value {i} is incorrect"), }; } -} \ No newline at end of file +}