Let the boolean table solver be cancelled

Sources/AngouriMath/Functions/Boolean/TableSolver.cs

@@ -6,6 +6,7 @@
 //
 
 using AngouriMath.Core.Exceptions;
+using AngouriMath.Core.Multithreading;
 using System;
 using static AngouriMath.Entity;
 
@@ -91,6 +92,7 @@ private enum Verdict { False, True, Unknown }
         static void Search(Entity expr, Variable[] variables, Dictionary<Variable, int> index,
                            int[] assignment, int depth, MatrixBuilder tb)
         {
+            MultithreadingFunctional.ExitIfCancelled();
             switch (Evaluate(expr, index, assignment))
             {
                 case Verdict.False:
@@ -121,12 +123,20 @@ static void Search(Entity expr, Variable[] variables, Dictionary<Variable, int>
         /// Writes out every way of filling in the variables from <paramref name="depth"/> on,
         /// in counting order. Called where the expression is already true whatever they are.
         /// </summary>
+        /// <remarks>
+        /// This is where the cost of the method's shape lands. The search is cheap, but every
+        /// model has to be written down, and a formula that most assignments satisfy has a
+        /// great many: a tautology over 22 variables is four million rows and 2.4 GB. So this
+        /// is the loop that most needs to be interruptible — the caller cannot know in advance
+        /// that the answer will not fit.
+        /// </remarks>
         static void EmitEveryCompletion(int[] assignment, int depth, MatrixBuilder tb)
         {
             var free = assignment.Length - depth;
             var total = 1L << free;
             for (long combination = 0; combination < total; combination++)
             {
+                MultithreadingFunctional.ExitIfCancelled();
                 var row = new Entity[assignment.Length];
                 for (var i = 0; i < depth; i++)
                     row[i] = assignment[i] == 1;
@@ -241,6 +251,9 @@ static Verdict Evaluate(Entity expr, Dictionary<Variable, int> index, int[] assi
             var variablesStorage = new Dictionary<Variable, Entity>();
             do
             {
+                // A truth table is all 2^n rows by definition, so there is no pruning to be
+                // had here and the only mercy available is being able to stop.
+                MultithreadingFunctional.ExitIfCancelled();
                 for (int i = 0; i < count; i++)
                     variablesStorage[variables[i]] = states[i];
                 tb.Add(states.Select(s => (Entity)s).Append(expr.Substitute(variablesStorage).EvalBoolean()));

Sources/Tests/UnitTests/Discrete/BooleanSolver.cs

@@ -6,8 +6,10 @@
 //
 
 using AngouriMath;
+using System;
 using System.Collections.Generic;
 using System.Linq;
+using System.Threading;
 using Xunit;
 
 namespace AngouriMath.Tests.Discrete
@@ -76,7 +78,7 @@
             var solutions = MathS.SolveBooleanTable(expr, vars);
 
             Assert.NotNull(solutions);
             Assert.Equal(1, solutions.RowCount);
             for (var j = 0; j < vars.Length; j++)
                 Assert.True((bool)solutions[0, j].EvalBoolean());
         }
@@ -96,7 +98,7 @@
             var solutions = MathS.SolveBooleanTable(expr, vars);
 
             Assert.NotNull(solutions);
             Assert.Equal(vars.Length, solutions.RowCount);
             for (var row = 0; row < solutions.RowCount; row++)
             {
                 var trues = 0;
@@ -142,7 +144,7 @@
                 if ((bits[0] || bits[1]) && (bits[2] || bits[3])) expected.Add(assignment);
             }
 
             Assert.Equal(expected.Count, solutions.RowCount);
             for (var row = 0; row < solutions.RowCount; row++)
             {
                 var actual = 0;
@@ -152,6 +154,81 @@
             }
         }
 
+        /// <summary>
+        /// A tautology over n variables has 2^n models and every one has to be written down,
+        /// so the answer can be far larger than the caller could know in advance — 22
+        /// variables is four million rows and some gigabytes. Pruning cannot help, since
+        /// there is nothing to prune, which leaves stopping as the only recourse. It was not
+        /// available: the token that aborts <see cref="Entity.Solve"/> was not consulted here
+        /// at all.
+        /// </summary>
+        static Entity Tautology(int count)
+        {
+            Entity all = (Entity)"p_0" | !(Entity)"p_0";
+            for (var i = 1; i < count; i++)
+                all &= (Entity)$"p_{i}" | !(Entity)$"p_{i}";
+            return all;
+        }
+
+        [Fact]
+        public void AnAlreadyCancelledTokenStopsTheSolverAtOnce()
+        {
+            using var source = new CancellationTokenSource();
+            source.Cancel();
+            MathS.Multithreading.SetLocalCancellationToken(source.Token);
+            try
+            {
+                Assert.Throws<OperationCanceledException>(
+                    () => MathS.SolveBooleanTable(Tautology(24), Vars(24)));
+            }
+            finally
+            {
+                MathS.Multithreading.SetLocalCancellationToken(default);
+            }
+        }
+
+        [Fact]
+        public void CancellingPartwayThroughStopsTheSolver()
+        {
+            using var source = new CancellationTokenSource();
+            using var started = new ManualResetEventSlim();
+
+            var worker = new Thread(() =>
+            {
+                MathS.Multithreading.SetLocalCancellationToken(source.Token);
+                started.Set();
+                try { MathS.SolveBooleanTable(Tautology(24), Vars(24)); }
+                catch (OperationCanceledException) { cancelled = true; }
+            });
+            worker.Start();
+            started.Wait();
+            Thread.Sleep(200);
+            source.Cancel();
+
+            Assert.True(worker.Join(TimeSpan.FromSeconds(20)), "the solver ignored the cancellation");
+            Assert.True(cancelled, "the solver stopped without reporting cancellation");
+        }
+
+        private volatile bool cancelled;
+
+        /// <summary>The truth table is all 2^n rows by definition, and must stop too.</summary>
+        [Fact]
+        public void AnAlreadyCancelledTokenStopsTheTruthTableAtOnce()
+        {
+            using var source = new CancellationTokenSource();
+            source.Cancel();
+            MathS.Multithreading.SetLocalCancellationToken(source.Token);
+            try
+            {
+                Assert.Throws<OperationCanceledException>(
+                    () => MathS.Boolean.BuildTruthTable(Tautology(24), Vars(24)));
+            }
+            finally
+            {
+                MathS.Multithreading.SetLocalCancellationToken(default);
+            }
+        }
+
         [Theory]
         [InlineData("(x implies a) = b", "{ False provided a and b, True provided a and b, False provided not a and b, True provided not a and not b }")]
         [InlineData("(x and a) = b", "{ True provided b and a, False provided a and not b, True provided not a and not b, False provided not a and not b }")]