BitContradiction and DETAILED_LOG fixes
This commit is contained in:
1 parent
1a97cdf754
commit
778a36d2eb
3 files changed
+138
-126
No files matched your search
@@ -96,6 +96,19 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
[ThreadStatic]
|
[ThreadStatic]
|
||||||
private static TopDownPruneFailure? _lastTopDownFailure;
|
private static TopDownPruneFailure? _lastTopDownFailure;
|
||||||
internal static TopDownPruneFailure? LastTopDownFailure => _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
|
#else
|
||||||
[ThreadStatic]
|
[ThreadStatic]
|
||||||
private static Dictionary<TopDownCacheKey, bool>? _topDownCache;
|
private static Dictionary<TopDownCacheKey, bool>? _topDownCache;
|
||||||
@@ -1327,9 +1340,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
int maxOffset = qOneOffsets[qOneOffsetsLength - 1];
|
int maxOffset = qOneOffsets[qOneOffsetsLength - 1];
|
||||||
if ((ulong)(maxOffset + 1) >= p)
|
if ((ulong)(maxOffset + 1) >= p)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.TruncatedLength;
|
reason = ContradictionReason.TruncatedLength;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
// return true;
|
// return true;
|
||||||
}
|
}
|
||||||
@@ -1360,9 +1373,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
int maxAllowedA = pLong - (maxOffset + 1);
|
int maxAllowedA = pLong - (maxOffset + 1);
|
||||||
if (maxAllowedA < 0)
|
if (maxAllowedA < 0)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.TruncatedLength;
|
reason = ContradictionReason.TruncatedLength;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1385,10 +1398,10 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
if (qMod2k.IsEven)
|
if (qMod2k.IsEven)
|
||||||
{
|
{
|
||||||
Console.WriteLine("Pruned by qMod2k.IsEven");
|
Console.WriteLine("Pruned by qMod2k.IsEven");
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Compute inv = q^{-1} mod 2^1024 using Hensel/Newton iteration in Z/2^kZ.
|
// Compute inv = q^{-1} mod 2^1024 using Hensel/Newton iteration in Z/2^kZ.
|
||||||
@@ -1418,12 +1431,12 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if ((knownZero0[word] & mask64) != 0)
|
if ((knownZero0[word] & mask64) != 0)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
// TODO: This doesn't kickoff. Is it necessary?
|
// TODO: This doesn't kickoff. Is it necessary?
|
||||||
Console.WriteLine("Pruned by knownZero1[word] & mask64");
|
Console.WriteLine("Pruned by knownZero1[word] & mask64");
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
knownOne0[word] |= mask64;
|
knownOne0[word] |= mask64;
|
||||||
@@ -1432,12 +1445,12 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if ((knownOne0[word] & mask64) != 0)
|
if ((knownOne0[word] & mask64) != 0)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
// TODO: This doesn't kickoff. Is it necessary?
|
// TODO: This doesn't kickoff. Is it necessary?
|
||||||
Console.WriteLine("Pruned by knownOne1[word] & mask64");
|
Console.WriteLine("Pruned by knownOne1[word] & mask64");
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
knownZero0[word] |= mask64;
|
knownZero0[word] |= mask64;
|
||||||
@@ -1535,11 +1548,11 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
// It can reject entire classes of q with sparse/awkward high-bit structure before the full DP runs.
|
// It can reject entire classes of q with sparse/awkward high-bit structure before the full DP runs.
|
||||||
if (!TryHighBitTopCarryPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA))
|
if (!TryHighBitTopCarryPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA))
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
Console.WriteLine("Pruned with TryHighBitTopCarryPrefilter");
|
Console.WriteLine("Pruned with TryHighBitTopCarryPrefilter");
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
// var cacheKey = new TopDownCacheKey(qHash, qOneOffsetsLength, maxAllowedA, pLong);
|
// var cacheKey = new TopDownCacheKey(qHash, qOneOffsetsLength, maxAllowedA, pLong);
|
||||||
@@ -1582,16 +1595,16 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
|
|
||||||
if (ShouldRunTopDownBorrowPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA))
|
if (ShouldRunTopDownBorrowPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA))
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
if (!TryTopDownBorrowPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA, out _lastTopDownFailure))
|
if (!TryTopDownBorrowPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA, out _lastTopDownFailure))
|
||||||
#else
|
#else
|
||||||
if (!TryTopDownBorrowPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA))
|
if (!TryTopDownBorrowPrefilter(qOneOffsets, qOneOffsetsLength, pLong, maxAllowedA))
|
||||||
#endif
|
#endif
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return true;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1707,7 +1720,7 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
int remaining = highColumn - lowColumn + 1;
|
int remaining = highColumn - lowColumn + 1;
|
||||||
int blockSize = remaining < PingPongBlockColumns ? remaining : PingPongBlockColumns;
|
int blockSize = remaining < PingPongBlockColumns ? remaining : PingPongBlockColumns;
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
if (!TryProcessBottomUpBlockRowAware(
|
if (!TryProcessBottomUpBlockRowAware(
|
||||||
qOneOffsets, qMaskWords, qWordCount, lastWordMask, maxAllowedA,
|
qOneOffsets, qMaskWords, qWordCount, lastWordMask, maxAllowedA,
|
||||||
lowColumn, blockSize,
|
lowColumn, blockSize,
|
||||||
@@ -1715,20 +1728,20 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
ref knownOne0, ref knownOne1, ref knownZero0, ref knownZero1,
|
ref knownOne0, ref knownOne1, ref knownZero0, ref knownZero1,
|
||||||
windowSize, aOneWin, aZeroWin, ref windowColumn,
|
windowSize, aOneWin, aZeroWin, ref windowColumn,
|
||||||
out reason))
|
out reason))
|
||||||
#else
|
#else
|
||||||
if (!TryProcessBottomUpBlockRowAware(
|
if (!TryProcessBottomUpBlockRowAware(
|
||||||
qOneOffsets, qMaskWords, qWordCount, lastWordMask, maxAllowedA,
|
qOneOffsets, qMaskWords, qWordCount, lastWordMask, maxAllowedA,
|
||||||
lowColumn, blockSize,
|
lowColumn, blockSize,
|
||||||
ref carryLow, ref maxKnownA, ref segmentBase,
|
ref carryLow, ref maxKnownA, ref segmentBase,
|
||||||
ref knownOne0, ref knownOne1, ref knownZero0, ref knownZero1,
|
ref knownOne0, ref knownOne1, ref knownZero0, ref knownZero1,
|
||||||
windowSize, aOneWin, aZeroWin, ref windowColumn))
|
windowSize, aOneWin, aZeroWin, ref windowColumn))
|
||||||
#endif
|
#endif
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
PrintStats();
|
PrintStats();
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
return false;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
lowColumn += blockSize;
|
lowColumn += blockSize;
|
||||||
@@ -1749,10 +1762,10 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
// }
|
// }
|
||||||
|
|
||||||
divides = true;
|
divides = true;
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.None;
|
reason = ContradictionReason.None;
|
||||||
PrintStats();
|
PrintStats();
|
||||||
#endif
|
#endif
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1842,9 +1855,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
|
|
||||||
private static int[] GetStableUnknownDelta(int unknown)
|
private static int[] GetStableUnknownDelta(int unknown)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
_statDeltaRequests++;
|
_statDeltaRequests++;
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
// Lazily allocate the outer array. Keep it volatile to publish safely.
|
// Lazily allocate the outer array. Keep it volatile to publish safely.
|
||||||
int[][] cache = _stableUnknownDelta8ByUnknown!;
|
int[][] cache = _stableUnknownDelta8ByUnknown!;
|
||||||
@@ -1869,9 +1882,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
var cached = cache[unknown];
|
var cached = cache[unknown];
|
||||||
if (cached != null)
|
if (cached != null)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
_statDeltaHits++;
|
_statDeltaHits++;
|
||||||
#endif
|
#endif
|
||||||
return cached;
|
return cached;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1906,9 +1919,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
delta[low] = (int)((value << ColumnsAtOnce) - low);
|
delta[low] = (int)((value << ColumnsAtOnce) - low);
|
||||||
}
|
}
|
||||||
|
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
_statDeltaBuilds++;
|
_statDeltaBuilds++;
|
||||||
#endif
|
#endif
|
||||||
// Publish into cache. If a race computes it twice, that's acceptable (same deterministic result).
|
// Publish into cache. If a race computes it twice, that's acceptable (same deterministic result).
|
||||||
cache[unknown] = delta;
|
cache[unknown] = delta;
|
||||||
return delta;
|
return delta;
|
||||||
@@ -1948,18 +1961,18 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
private static bool TryAdvanceStableUnknown(ref CarryRange carry, int unknown, int columnCount)
|
private static bool TryAdvanceStableUnknown(ref CarryRange carry, int unknown, int columnCount)
|
||||||
#endif
|
#endif
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
_statStableAdvanceCalls++;
|
_statStableAdvanceCalls++;
|
||||||
_statStableAdvanceCols += columnCount;
|
_statStableAdvanceCols += columnCount;
|
||||||
if (columnCount >= 64) _statStableAdvanceBigShift++;
|
if (columnCount >= 64) _statStableAdvanceBigShift++;
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
if (columnCount <= 0)
|
if (columnCount <= 0)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.None;
|
reason = ContradictionReason.None;
|
||||||
_statStableAdvanceColsBatched += columnCount;
|
_statStableAdvanceColsBatched += columnCount;
|
||||||
#endif
|
#endif
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1967,16 +1980,16 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (!TryAdvanceZeroColumns(ref carry, columnCount))
|
if (!TryAdvanceZeroColumns(ref carry, columnCount))
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
_statStableAdvanceColsBatched += columnCount;
|
_statStableAdvanceColsBatched += columnCount;
|
||||||
reason = ContradictionReason.None;
|
reason = ContradictionReason.None;
|
||||||
#endif
|
#endif
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1985,7 +1998,7 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
int remaining = columnCount;
|
int remaining = columnCount;
|
||||||
int[] delta = GetStableUnknownDelta(unknown);
|
int[] delta = GetStableUnknownDelta(unknown);
|
||||||
|
|
||||||
const int CarryDecimalMask = (1 << ColumnsAtOnce) - 1;
|
const long CarryDecimalMask = (1L << ColumnsAtOnce) - 1L;
|
||||||
while (remaining >= ColumnsAtOnce)
|
while (remaining >= ColumnsAtOnce)
|
||||||
{
|
{
|
||||||
int low = (int)(carryMax & CarryDecimalMask);
|
int low = (int)(carryMax & CarryDecimalMask);
|
||||||
@@ -2002,16 +2015,16 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
|
|
||||||
if (carryMax < carryMin)
|
if (carryMax < carryMin)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
_statStableAdvanceColsBatched += columnCount;
|
_statStableAdvanceColsBatched += columnCount;
|
||||||
reason = ContradictionReason.None;
|
reason = ContradictionReason.None;
|
||||||
#endif
|
#endif
|
||||||
carry = new CarryRange(carryMin, carryMax);
|
carry = new CarryRange(carryMin, carryMax);
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
@@ -2313,24 +2326,24 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
// Additionally, ensure current window has no known bits (should be true if maxKnownA condition holds).
|
// 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.
|
// 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.
|
// This cannot create false negatives; it may only reduce pruning power.
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
_statBatchEntry++;
|
_statBatchEntry++;
|
||||||
_statBatchCols += remainingCols;
|
_statBatchCols += remainingCols;
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
int rem = remainingCols;
|
int rem = remainingCols;
|
||||||
while (rem > 0)
|
while (rem > 0)
|
||||||
{
|
{
|
||||||
int step = rem > TailCarryBatchColumns ? TailCarryBatchColumns : rem;
|
int step = rem > TailCarryBatchColumns ? TailCarryBatchColumns : rem;
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, step, out var propagateReason))
|
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, step, out var propagateReason))
|
||||||
#else
|
#else
|
||||||
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, step))
|
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, step))
|
||||||
#endif
|
#endif
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = propagateReason;
|
reason = propagateReason;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2384,9 +2397,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (state == 2)
|
if (state == 2)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2402,9 +2415,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (state == 1)
|
if (state == 1)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2423,9 +2436,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
int possible = forced + remaining;
|
int possible = forced + remaining;
|
||||||
if (!TryPropagateCarry(ref carry, forced, possible, 1))
|
if (!TryPropagateCarry(ref carry, forced, possible, 1))
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2448,14 +2461,14 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
|
|
||||||
startColumn++;
|
startColumn++;
|
||||||
windowColumn = startColumn;
|
windowColumn = startColumn;
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
_statScalarCols++;
|
_statScalarCols++;
|
||||||
#endif
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.None;
|
reason = ContradictionReason.None;
|
||||||
#endif
|
#endif
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2515,15 +2528,15 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
runEndIdx = runCount;
|
runEndIdx = runCount;
|
||||||
while (remaining >= TailCarryBatchColumns)
|
while (remaining >= TailCarryBatchColumns)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns, out var propagateReason))
|
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns, out var propagateReason))
|
||||||
#else
|
#else
|
||||||
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns))
|
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, TailCarryBatchColumns))
|
||||||
#endif
|
#endif
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = propagateReason;
|
reason = propagateReason;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2533,15 +2546,15 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
|
|
||||||
if (remaining > 0)
|
if (remaining > 0)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining, out var propagateReason))
|
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining, out var propagateReason))
|
||||||
#else
|
#else
|
||||||
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining))
|
if (!TryAdvanceStableUnknown(ref carry, stableUnknown, remaining))
|
||||||
#endif
|
#endif
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = propagateReason;
|
reason = propagateReason;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2791,9 +2804,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (top0KnownZero)
|
if (top0KnownZero)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2804,9 +2817,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (top1KnownZero)
|
if (top1KnownZero)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2830,9 +2843,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (top0KnownOne)
|
if (top0KnownOne)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2843,9 +2856,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (top1KnownOne)
|
if (top1KnownOne)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2860,18 +2873,18 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
var qHash = ComputeQOffsetsHash(qOneOffsets);
|
var qHash = ComputeQOffsetsHash(qOneOffsets);
|
||||||
if (!TryDynamicModularRangePrune(qOneOffsets, qHash, prime, maxAllowedA, top0KnownOne, top0KnownZero, top1KnownOne, top1KnownZero, zeroTailStart))
|
if (!TryDynamicModularRangePrune(qOneOffsets, qHash, prime, maxAllowedA, top0KnownOne, top0KnownZero, top1KnownOne, top1KnownZero, zeroTailStart))
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if ((top0KnownZero && top0KnownOne) || (top1KnownZero && top1KnownOne))
|
if ((top0KnownZero && top0KnownOne) || (top1KnownZero && top1KnownOne))
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2879,17 +2892,17 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (top0KnownZero)
|
if (top0KnownZero)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else if (top0KnownZero && top1KnownZero)
|
else if (top0KnownZero && top1KnownZero)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2901,9 +2914,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
long carryMax = AlignDownToParity(carry.Max, known0Len);
|
long carryMax = AlignDownToParity(carry.Max, known0Len);
|
||||||
if (carryMin > carryMax)
|
if (carryMin > carryMax)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2920,9 +2933,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if ((minSum & 1) != requiredParity)
|
if ((minSum & 1) != requiredParity)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2933,9 +2946,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if ((minSum & 1) != requiredParity && remaining == 0)
|
if ((minSum & 1) != requiredParity && remaining == 0)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2945,22 +2958,22 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
forced + remaining,
|
forced + remaining,
|
||||||
requiredParity))
|
requiredParity))
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.ParityUnreachable;
|
reason = ContradictionReason.ParityUnreachable;
|
||||||
#endif
|
#endif
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
startColumn++;
|
startColumn++;
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
_statScalarCols++;
|
_statScalarCols++;
|
||||||
#endif
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
reason = ContradictionReason.None;
|
reason = ContradictionReason.None;
|
||||||
#endif
|
#endif
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -2968,8 +2981,8 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
private static bool TryProcessTopDownBlock(
|
private static bool TryProcessTopDownBlock(
|
||||||
ReadOnlySpan<int> qOneOffsets,
|
ReadOnlySpan<int> qOneOffsets,
|
||||||
int qOneOffsetsLength,
|
int qOneOffsetsLength,
|
||||||
long maxAllowedA,
|
int maxAllowedA,
|
||||||
long startHighColumn,
|
int startHighColumn,
|
||||||
int columnCount,
|
int columnCount,
|
||||||
CarryRange carryOut,
|
CarryRange carryOut,
|
||||||
ref int windowStart,
|
ref int windowStart,
|
||||||
@@ -2989,9 +3002,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
out CarryRange nextCarryOut)
|
out CarryRange nextCarryOut)
|
||||||
#endif
|
#endif
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
failure = null;
|
failure = null;
|
||||||
#endif
|
#endif
|
||||||
long carryOutMin = carryOut.Min,
|
long carryOutMin = carryOut.Min,
|
||||||
carryOutMax = carryOut.Max;
|
carryOutMax = carryOut.Max;
|
||||||
int value;
|
int value;
|
||||||
@@ -3041,9 +3054,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (!AdvanceTopDownUnknown0(ref carryOutMin, ref carryOutMax, steps))
|
if (!AdvanceTopDownUnknown0(ref carryOutMin, ref carryOutMax, steps))
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value);
|
failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value);
|
||||||
#endif
|
#endif
|
||||||
nextCarryOut = default;
|
nextCarryOut = default;
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
@@ -3067,9 +3080,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
{
|
{
|
||||||
if (!AdvanceTopDownUnknown1(ref carryOutMin, ref carryOutMax, steps))
|
if (!AdvanceTopDownUnknown1(ref carryOutMin, ref carryOutMax, steps))
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value);
|
failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value);
|
||||||
#endif
|
#endif
|
||||||
nextCarryOut = default;
|
nextCarryOut = default;
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
@@ -3095,9 +3108,9 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
|
|
||||||
if (carryOutMin > carryOutMax)
|
if (carryOutMin > carryOutMax)
|
||||||
{
|
{
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value);
|
failure = new TopDownPruneFailure(column, carryOutMin, carryOutMax, value);
|
||||||
#endif
|
#endif
|
||||||
nextCarryOut = default;
|
nextCarryOut = default;
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
@@ -3256,8 +3269,8 @@ internal static class BitContradictionSolverWithAMultiplier
|
|||||||
private static bool TryTopDownBorrowPrefilter(
|
private static bool TryTopDownBorrowPrefilter(
|
||||||
ReadOnlySpan<int> qOneOffsets,
|
ReadOnlySpan<int> qOneOffsets,
|
||||||
int qOneOffsetsLength,
|
int qOneOffsetsLength,
|
||||||
long pLong,
|
int pLong,
|
||||||
long maxAllowedA,
|
int maxAllowedA,
|
||||||
out TopDownPruneFailure? failure)
|
out TopDownPruneFailure? failure)
|
||||||
#else
|
#else
|
||||||
private static bool TryTopDownBorrowPrefilter(
|
private static bool TryTopDownBorrowPrefilter(
|
||||||
|
|||||||
@@ -39,11 +39,11 @@ internal static class BitContradictionSolverWithQMultiplier
|
|||||||
private const int TopDownCacheCapacity = 16;
|
private const int TopDownCacheCapacity = 16;
|
||||||
|
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
public readonly struct TopDownPruneFailure(int column, int carryMin, int carryMax, int unknown)
|
public readonly struct TopDownPruneFailure(int column, long carryMin, long carryMax, int unknown)
|
||||||
{
|
{
|
||||||
public readonly int Column = column;
|
public readonly int Column = column;
|
||||||
public readonly int CarryMin = carryMin;
|
public readonly long CarryMin = carryMin;
|
||||||
public readonly int CarryMax = carryMax;
|
public readonly long CarryMax = carryMax;
|
||||||
public readonly int Unknown = unknown;
|
public readonly int Unknown = unknown;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -53,11 +53,11 @@ internal static class BitContradictionSolverWithQMultiplier
|
|||||||
public readonly TopDownPruneFailure? Failure = failure;
|
public readonly TopDownPruneFailure? Failure = failure;
|
||||||
}
|
}
|
||||||
|
|
||||||
internal readonly struct BottomUpFailure(int column, int carryMin, int carryMax, int forced, int unknown)
|
internal readonly struct BottomUpFailure(int column, long carryMin, long carryMax, int forced, int unknown)
|
||||||
{
|
{
|
||||||
public readonly int Column = column;
|
public readonly int Column = column;
|
||||||
public readonly int CarryMin = carryMin;
|
public readonly long CarryMin = carryMin;
|
||||||
public readonly int CarryMax = carryMax;
|
public readonly long CarryMax = carryMax;
|
||||||
public readonly int Forced = forced;
|
public readonly int Forced = forced;
|
||||||
public readonly int Unknown = unknown;
|
public readonly int Unknown = unknown;
|
||||||
}
|
}
|
||||||
@@ -647,8 +647,8 @@ internal static class BitContradictionSolverWithQMultiplier
|
|||||||
private static bool TryProcessTopDownBlock(
|
private static bool TryProcessTopDownBlock(
|
||||||
ReadOnlySpan<int> qOneOffsets,
|
ReadOnlySpan<int> qOneOffsets,
|
||||||
int qOneOffsetsLength,
|
int qOneOffsetsLength,
|
||||||
long maxAllowedA,
|
int maxAllowedA,
|
||||||
long startHighColumn,
|
int startHighColumn,
|
||||||
int columnCount,
|
int columnCount,
|
||||||
CarryRange carryOut,
|
CarryRange carryOut,
|
||||||
ref int windowStart,
|
ref int windowStart,
|
||||||
@@ -795,8 +795,8 @@ internal static class BitContradictionSolverWithQMultiplier
|
|||||||
private static bool TryTopDownCarryPrune(
|
private static bool TryTopDownCarryPrune(
|
||||||
ReadOnlySpan<int> qOneOffsets,
|
ReadOnlySpan<int> qOneOffsets,
|
||||||
int qOneOffsetsLength,
|
int qOneOffsetsLength,
|
||||||
long pLong,
|
int pLong,
|
||||||
long maxAllowedA,
|
int maxAllowedA,
|
||||||
out TopDownPruneFailure? failure)
|
out TopDownPruneFailure? failure)
|
||||||
#else
|
#else
|
||||||
private static bool TryTopDownCarryPrune(
|
private static bool TryTopDownCarryPrune(
|
||||||
|
|||||||
@@ -4799,7 +4799,6 @@ public struct MersenneNumberDivisorByDivisorCpuTesterWithTemplate() : IMersenneN
|
|||||||
#endif
|
#endif
|
||||||
// BitContradictionSolverWithQMultiplier.SetDebugEnabled(false);
|
// BitContradictionSolverWithQMultiplier.SetDebugEnabled(false);
|
||||||
// bool decided = BitContradictionSolverBaseline.TryCheckDivisibilityFromOneOffsets(oneOffsetsSlice, exponent, out divides, out var reason);
|
// bool decided = BitContradictionSolverBaseline.TryCheckDivisibilityFromOneOffsets(oneOffsetsSlice, exponent, out divides, out var reason);
|
||||||
ArgumentOutOfRangeException.ThrowIfNotEqual(decided, divides);
|
|
||||||
if (decided && divides)
|
if (decided && divides)
|
||||||
{
|
{
|
||||||
// Verify to avoid false positives on structurally admissible but non-dividing q.
|
// Verify to avoid false positives on structurally admissible but non-dividing q.
|
||||||
@@ -4838,7 +4837,7 @@ public struct MersenneNumberDivisorByDivisorCpuTesterWithTemplate() : IMersenneN
|
|||||||
}
|
}
|
||||||
|
|
||||||
#if DETAILED_LOG
|
#if DETAILED_LOG
|
||||||
Console.WriteLine($"[bitcontradiction ({sw.Elapsed})] Prime={prime}, Divisor={divisor} Decided={decided} Divides={divides} Reason={reason}");
|
Console.WriteLine($"[bitcontradiction] Prime={prime}, Divisor={divisor} Decided={decided} Divides={divides} Reason={reason}");
|
||||||
#endif
|
#endif
|
||||||
return decided;
|
return decided;
|
||||||
}
|
}
|
||||||
|
|||||||
Reference in new issue
Block a user