feat(learning): cut eager-explanation allocation

Csp/BaseTypes/Constraint.cs

@@ -39,5 +39,6 @@ public record struct BoundReason(int VariableIndex, bool IsLowerBound, int Bound
 
 public interface IExplainableConstraint : IConstraint
 {
-	void Explain(int variableId, bool isLowerBound, int boundValue, IList<BoundReason> result);
+	void Explain(int variableId, bool isLowerBound, int boundValue,
+		IReadOnlyList<int> snapshotLowerBounds, IReadOnlyList<int> snapshotUpperBounds, IList<BoundReason> result);
 }

Csp/Global/AllDifferentInteger.cs

@@ -23,8 +23,6 @@ public class AllDifferentInteger : IBacktrackableConstraint, IConstraint<int>, I
 	private readonly CycleDetection cycleDetection;
 	private readonly Stack<(int Depth, int?[] Matching)> matchingTrail;
 	private int?[]? lastMatching;
-	private int[] SnapshotLB { get; set; } = Array.Empty<int>();
-	private int[] SnapshotUB { get; set; } = Array.Empty<int>();
 
 	private IState<int>? State { get; set; }
 	private int Depth
@@ -42,8 +40,6 @@ public AllDifferentInteger(IEnumerable<VariableInteger> variables)
 	{
 		this.VariableList = variables.ToArray();
 		this.GenerationList = new int[this.VariableList.Length];
-		this.SnapshotLB = new int[this.VariableList.Length];
-		this.SnapshotUB = new int[this.VariableList.Length];
 		this.cycleDetection = new CycleDetection();
 		this.matchingTrail = new Stack<(int Depth, int?[] Matching)>();
 	}
@@ -64,12 +60,6 @@ public void Check(out ConstraintOperationResult result)
 
 	public void Propagate(out ConstraintOperationResult result)
 	{
-		for (var i = 0; i < this.VariableList.Length; ++i)
-		{
-			this.SnapshotLB[i] = this.VariableList[i].Domain.LowerBound;
-			this.SnapshotUB[i] = this.VariableList[i].Domain.UpperBound;
-		}
-
 		if (this.Graph == null)
 		{
 			this.Graph = new BipartiteGraph(this.VariableList);
@@ -123,12 +113,13 @@ public void Propagate(out ConstraintOperationResult result)
 		}
 	}
 
-	public void Explain(int variableId, bool isLowerBound, int boundValue, IList<BoundReason> result)
+	public void Explain(int variableId, bool isLowerBound, int boundValue,
+		IReadOnlyList<int> snapshotLowerBounds, IReadOnlyList<int> snapshotUpperBounds, IList<BoundReason> result)
 	{
 		for (var i = 0; i < this.VariableList.Length; ++i)
 		{
-			result.Add(new BoundReason(this.VariableList[i].VariableId, true, this.SnapshotLB[i]));
-			result.Add(new BoundReason(this.VariableList[i].VariableId, false, this.SnapshotUB[i]));
+			result.Add(new BoundReason(this.VariableList[i].VariableId, true, snapshotLowerBounds[i]));
+			result.Add(new BoundReason(this.VariableList[i].VariableId, false, snapshotUpperBounds[i]));
 		}
 	}
 

Csp/Global/CumulativeInteger.cs

@@ -38,9 +38,6 @@ public class CumulativeInteger : IConstraint<int>, IExplainableConstraint
 	private Comparison<int> NotFirstComparison { get; set; }
 	private Comparison<int> NotLastComparison { get; set; }
 
-	private int[] SnapshotLB { get; set; }
-	private int[] SnapshotUB { get; set; }
-
 	private IList<DisjunctiveInteger> DisjunctiveSubproblems { get; set; }
 	private bool AllDisjunctive { get; set; }
 
@@ -74,9 +71,6 @@ public CumulativeInteger(IEnumerable<IVariable<int>> starts, IEnumerable<int> du
 		for (var i = 0; i < n; ++i)
 			this.NotFirstLastSortedTasks[i] = i;
 
-		this.SnapshotLB = new int[n];
-		this.SnapshotUB = new int[n];
-
 		this.NotFirstComparison = (a, b) => (this.Starts[a].Domain.UpperBound + this.Durations[a]).CompareTo(this.Starts[b].Domain.UpperBound + this.Durations[b]);
 		this.NotLastComparison = (a, b) => this.Starts[b].Domain.LowerBound.CompareTo(this.Starts[a].Domain.LowerBound);
 
@@ -228,12 +222,6 @@ public void Propagate(out ConstraintOperationResult result)
 	{
 		result = ConstraintOperationResult.Undecided;
 
-		for (var i = 0; i < this.Starts.Count; ++i)
-		{
-			this.SnapshotLB[i] = this.Starts[i].Domain.LowerBound;
-			this.SnapshotUB[i] = this.Starts[i].Domain.UpperBound;
-		}
-
 		var propagationOccurred = true;
 
 		while (propagationOccurred)
@@ -857,12 +845,13 @@ private ConstraintOperationResult NotFirstOrLastRule(bool notFirst)
 		return result;
 	}
 
-	public void Explain(int variableId, bool isLowerBound, int boundValue, IList<BoundReason> result)
+	public void Explain(int variableId, bool isLowerBound, int boundValue,
+		IReadOnlyList<int> snapshotLowerBounds, IReadOnlyList<int> snapshotUpperBounds, IList<BoundReason> result)
 	{
 		for (var j = 0; j < this.Starts.Count; ++j)
 		{
-			result.Add(new BoundReason(this.Starts[j].VariableId, true, this.SnapshotLB[j]));
-			result.Add(new BoundReason(this.Starts[j].VariableId, false, this.SnapshotUB[j]));
+			result.Add(new BoundReason(this.Starts[j].VariableId, true, snapshotLowerBounds[j]));
+			result.Add(new BoundReason(this.Starts[j].VariableId, false, snapshotUpperBounds[j]));
 		}
 	}
 

Csp/Global/DisjunctiveInteger.cs

@@ -25,8 +25,6 @@ public class DisjunctiveInteger : IConstraint<int>, IExplainableConstraint
 	private int[] LatestCompletionTimes { get; set; }
 	private int[] NewLowerBounds { get; set; }
 	private int[] NewUpperBounds { get; set; }
-	private int[] SnapshotLB { get; set; }
-	private int[] SnapshotUB { get; set; }
 	private int[] SortedByLct { get; set; }
 	private int[] SortedByEstDesc { get; set; }
 	private Comparison<int> LctComparison { get; set; }
@@ -49,8 +47,6 @@ public DisjunctiveInteger(IList<VariableInteger> starts, IList<int> durations)
 		this.LatestCompletionTimes = new int[n];
 		this.NewLowerBounds = new int[n];
 		this.NewUpperBounds = new int[n];
-		this.SnapshotLB = new int[n];
-		this.SnapshotUB = new int[n];
 		this.SortedByLct = new int[n];
 		this.SortedByEstDesc = new int[n];
 
@@ -104,12 +100,6 @@ public void Propagate(out ConstraintOperationResult result)
 	{
 		result = ConstraintOperationResult.Undecided;
 
-		for (var i = 0; i < this.Starts.Count; ++i)
-		{
-			this.SnapshotLB[i] = this.Starts[i].Domain.LowerBound;
-			this.SnapshotUB[i] = this.Starts[i].Domain.UpperBound;
-		}
-
 		var propagationOccurred = true;
 
 		while (propagationOccurred)
@@ -508,12 +498,13 @@ private IList<BoundReason> CollectAllReasons()
 		return reasons;
 	}
 
-	public void Explain(int variableId, bool isLowerBound, int boundValue, IList<BoundReason> result)
+	public void Explain(int variableId, bool isLowerBound, int boundValue,
+		IReadOnlyList<int> snapshotLowerBounds, IReadOnlyList<int> snapshotUpperBounds, IList<BoundReason> result)
 	{
 		for (var j = 0; j < this.Starts.Count; ++j)
 		{
-			result.Add(new BoundReason(this.Starts[j].VariableId, true, this.SnapshotLB[j]));
-			result.Add(new BoundReason(this.Starts[j].VariableId, false, this.SnapshotUB[j]));
+			result.Add(new BoundReason(this.Starts[j].VariableId, true, snapshotLowerBounds[j]));
+			result.Add(new BoundReason(this.Starts[j].VariableId, false, snapshotUpperBounds[j]));
 		}
 	}
 

Csp/Integer/ConflictAnalyser.cs

@@ -3,6 +3,7 @@
 
   This file is part of Decider.
 */
+using System;
 using System.Collections.Generic;
 
 using Decider.Csp.BaseTypes;
@@ -12,7 +13,7 @@ namespace Decider.Csp.Integer;
 internal static class ConflictAnalyser
 {
 	internal static bool Analyse(PropagationTrail trail, IList<BoundReason> conflictExplanation,
-		int currentLevel, IList<IConstraint> constraints, IList<IVariable<int>> variables,
+		int currentLevel, Func<int, IList<BoundReason>> explanationProvider,
 		out BoundReason[] learnedClause, out int assertionLevel, out bool isAsserting)
 	{
 		learnedClause = null!;
@@ -51,7 +52,7 @@ internal static bool Analyse(PropagationTrail trail, IList<BoundReason> conflict
 			nogood.Remove(key);
 			--currentLevelCount;
 
-			var explanation = GetExplanationFromEntry(i, trail, constraints, variables);
+			var explanation = explanationProvider(i);
 
 			foreach (var antecedent in explanation)
 				AddLiteral(nogood, trail, currentLevel, ref currentLevelCount, antecedent);
@@ -112,30 +113,6 @@ private static void AddLiteral(Dictionary<(int, bool), BoundReason> nogood,
 		nogood[key] = literal;
 	}
 
-	private static IList<BoundReason> GetExplanationFromEntry(int entryIndex, PropagationTrail trail,
-		IList<IConstraint> constraints, IList<IVariable<int>> variables)
-	{
-		ref var entry = ref trail.GetEntry(entryIndex);
-
-		var storedExplanation = trail.GetExplanation(entryIndex);
-		if (storedExplanation != null)
-			return storedExplanation;
-
-		if (entry.ReasonKind == PropagationTrail.ReasonConstraint &&
-			entry.ReasonIndex >= 0 && entry.ReasonIndex < constraints.Count)
-		{
-			var constraint = constraints[entry.ReasonIndex];
-			if (constraint is IExplainableConstraint explainable)
-			{
-				var result = new List<BoundReason>();
-				explainable.Explain(entry.VariableId, entry.IsLowerBound, entry.NewBound, result);
-				return result;
-			}
-		}
-
-		return new List<BoundReason>();
-	}
-
 	private static BoundReason NegateLiteral(BoundReason literal)
 	{
 		if (literal.IsLowerBound)

Csp/Integer/ConstraintInteger.cs

@@ -15,8 +15,6 @@ public class ConstraintInteger : ExpressionInteger, IConstraint<int>, IExplainab
 {
 	private VariableInteger[] VariableList { get; set; } = Array.Empty<VariableInteger>();
 	private IList<int> GenerationList { get; set; }
-	private int[] SnapshotLB { get; set; } = Array.Empty<int>();
-	private int[] SnapshotUB { get; set; } = Array.Empty<int>();
 
 	public IReadOnlyList<IVariable<int>> Variables => this.VariableList;
 	public int FailureWeight { get; set; }
@@ -35,8 +33,6 @@ public ConstraintInteger(Expression<int> expression)
 		ConstructVariableList((ExpressionInteger) expression, variableSet);
 		this.VariableList = variableSet.ToArray();
 		this.GenerationList = new int[this.VariableList.Length];
-		this.SnapshotLB = new int[this.VariableList.Length];
-		this.SnapshotUB = new int[this.VariableList.Length];
 	}
 
 	private static void ConstructVariableList(ExpressionInteger expression, ISet<VariableInteger> variableSet)
@@ -95,12 +91,6 @@ public void Check(out ConstraintOperationResult result)
 
 	public void Propagate(out ConstraintOperationResult result)
 	{
-		for (var i = 0; i < this.VariableList.Length; ++i)
-		{
-			this.SnapshotLB[i] = this.VariableList[i].Domain.LowerBound;
-			this.SnapshotUB[i] = this.VariableList[i].Domain.UpperBound;
-		}
-
 		var enforce = new Bounds<int>(1, 1);
 
 		do
@@ -109,21 +99,22 @@ public void Propagate(out ConstraintOperationResult result)
 		} while ((result & ConstraintOperationResult.Propagated) == ConstraintOperationResult.Propagated);
 	}
 
-	public void Explain(int variableId, bool isLowerBound, int boundValue, IList<BoundReason> result)
+	public void Explain(int variableId, bool isLowerBound, int boundValue,
+		IReadOnlyList<int> snapshotLowerBounds, IReadOnlyList<int> snapshotUpperBounds, IList<BoundReason> result)
 	{
 		for (var i = 0; i < this.VariableList.Length; ++i)
 		{
 			var v = this.VariableList[i];
 			if (v.VariableId == variableId)
 			{
 				result.Add(isLowerBound
-					? new BoundReason(v.VariableId, true, this.SnapshotLB[i])
-					: new BoundReason(v.VariableId, false, this.SnapshotUB[i]));
+					? new BoundReason(v.VariableId, true, snapshotLowerBounds[i])
+					: new BoundReason(v.VariableId, false, snapshotUpperBounds[i]));
 			}
 			else
 			{
-				result.Add(new BoundReason(v.VariableId, true, this.SnapshotLB[i]));
-				result.Add(new BoundReason(v.VariableId, false, this.SnapshotUB[i]));
+				result.Add(new BoundReason(v.VariableId, true, snapshotLowerBounds[i]));
+				result.Add(new BoundReason(v.VariableId, false, snapshotUpperBounds[i]));
 			}
 		}
 	}

Csp/Integer/PropagationTrail.cs

@@ -24,15 +24,18 @@ internal struct Entry
 		internal int DecisionLevel;
 		internal int ReasonKind;
 		internal int ReasonIndex;
+		internal int SnapshotBatch;
 
-		internal Entry(int variableId, bool isLowerBound, int newBound, int decisionLevel, int reasonKind, int reasonIndex)
+		internal Entry(int variableId, bool isLowerBound, int newBound, int decisionLevel,
+			int reasonKind, int reasonIndex, int snapshotBatch)
 		{
 			this.VariableId = variableId;
 			this.IsLowerBound = isLowerBound;
 			this.NewBound = newBound;
 			this.DecisionLevel = decisionLevel;
 			this.ReasonKind = reasonKind;
 			this.ReasonIndex = reasonIndex;
+			this.SnapshotBatch = snapshotBatch;
 		}
 	}
 
@@ -42,6 +45,9 @@ internal Entry(int variableId, bool isLowerBound, int newBound, int decisionLeve
 	private int[] levelStarts;
 	private List<(int Bound, int Level)>[] lowerHistory;
 	private List<(int Bound, int Level)>[] upperHistory;
+	private readonly List<int[]> snapshotLowerBatches;
+	private readonly List<int[]> snapshotUpperBatches;
+	private readonly List<int> snapshotBatchStartEntry;
 
 	internal int Count => this.entryCount;
 
@@ -56,20 +62,23 @@ internal PropagationTrail(int maxLevels, int estimatedCapacity)
 
 		this.lowerHistory = new List<(int, int)>[maxLevels];
 		this.upperHistory = new List<(int, int)>[maxLevels];
+		this.snapshotLowerBatches = new List<int[]>();
+		this.snapshotUpperBatches = new List<int[]>();
+		this.snapshotBatchStartEntry = new List<int>();
 	}
 
 	internal void RecordDecision(int variableId, int lowerBound, int upperBound, int decisionLevel)
 	{
 		EnsureLevelStart(decisionLevel);
-		AppendEntry(new Entry(variableId, true, lowerBound, decisionLevel, ReasonDecision, -1));
-		AppendEntry(new Entry(variableId, false, upperBound, decisionLevel, ReasonDecision, -1));
+		AppendEntry(new Entry(variableId, true, lowerBound, decisionLevel, ReasonDecision, -1, -1));
+		AppendEntry(new Entry(variableId, false, upperBound, decisionLevel, ReasonDecision, -1, -1));
 	}
 
 	internal void RecordPropagation(int variableId, bool isLowerBound, int newBound,
-		int decisionLevel, int reasonKind, int reasonIndex, IList<BoundReason> explanation = null!)
+		int decisionLevel, int reasonKind, int reasonIndex, IList<BoundReason> explanation = null!, int snapshotBatch = -1)
 	{
 		EnsureLevelStart(decisionLevel);
-		AppendEntry(new Entry(variableId, isLowerBound, newBound, decisionLevel, reasonKind, reasonIndex),
+		AppendEntry(new Entry(variableId, isLowerBound, newBound, decisionLevel, reasonKind, reasonIndex, snapshotBatch),
 			explanation);
 	}
 
@@ -81,6 +90,30 @@ internal IList<BoundReason> GetExplanation(int index)
 		return this.explanations[index];
 	}
 
+	internal int AddSnapshot(int[] lowerBounds, int[] upperBounds, int length)
+	{
+		var lower = new int[length];
+		var upper = new int[length];
+		Array.Copy(lowerBounds, lower, length);
+		Array.Copy(upperBounds, upper, length);
+
+		this.snapshotLowerBatches.Add(lower);
+		this.snapshotUpperBatches.Add(upper);
+		this.snapshotBatchStartEntry.Add(this.entryCount);
+
+		return this.snapshotLowerBatches.Count - 1;
+	}
+
+	internal IReadOnlyList<int> GetSnapshotLower(int batchId)
+	{
+		return batchId < 0 ? Array.Empty<int>() : this.snapshotLowerBatches[batchId];
+	}
+
+	internal IReadOnlyList<int> GetSnapshotUpper(int batchId)
+	{
+		return batchId < 0 ? Array.Empty<int>() : this.snapshotUpperBatches[batchId];
+	}
+
 	internal void Backtrack(int toLevel)
 	{
 		var markerIndex = toLevel + 1;
@@ -154,6 +187,19 @@ private void TruncateHistory(int newCount)
 		}
 
 		this.entryCount = newCount;
+		TruncateSnapshots(newCount);
+	}
+
+	private void TruncateSnapshots(int newCount)
+	{
+		var last = this.snapshotBatchStartEntry.Count - 1;
+		while (last >= 0 && this.snapshotBatchStartEntry[last] >= newCount)
+		{
+			this.snapshotBatchStartEntry.RemoveAt(last);
+			this.snapshotLowerBatches.RemoveAt(last);
+			this.snapshotUpperBatches.RemoveAt(last);
+			--last;
+		}
 	}
 
 	internal ref Entry GetEntry(int index)
@@ -172,6 +218,9 @@ internal int GetLevelStart(int level)
 	internal void Clear()
 	{
 		this.entryCount = 0;
+		this.snapshotLowerBatches.Clear();
+		this.snapshotUpperBatches.Clear();
+		this.snapshotBatchStartEntry.Clear();
 		for (var i = 0; i < this.levelStarts.Length; ++i)
 			this.levelStarts[i] = -1;