using System;
using System.Linq;
using UnitTestSharp;

namespace Amphora.UnitTests
{
    public class BinaryDecisionDiagramTests : TestFixture
    {
        public const int VariableCount = 5;
        public const int AssignmentCount = 1 << VariableCount;

        public const int NeverPosition = BinaryDecisionDiagramBuilder.NeverPosition;
        public const int AlwaysPosition = BinaryDecisionDiagramBuilder.AlwaysPosition;

        // Variable v is true when bit v of the mask is set.
        public readonly struct Bits : IVariableAssignment
        {
            public readonly int Mask;

            public Bits(int mask)
            {
                Mask = mask;
            }

            public bool IsTrue(int variable)
            {
                return (Mask >> variable & 1) != 0;
            }
        }

        public static BinaryDecisionDiagram Var(int variable)
        {
            return BinaryDecisionDiagram.Variable(variable);
        }

        public static bool Eval(BinaryDecisionDiagram diagram, int mask)
        {
            return diagram.Evaluate(new Bits(mask));
        }

        public static int MaskOf(params int[] trueVariables)
        {
            int returnMe = 0;
            foreach (int variable in trueVariables)
            {
                returnMe |= 1 << variable;
            }

            return returnMe;
        }

        public static int[] Copy(ArrayView<int> view)
        {
            var returnMe = new int[view.Count];
            for (int i = 0; i < view.Count; ++i)
            {
                returnMe[i] = view[i];
            }

            return returnMe;
        }

        // x0 and x1 and ... and the last, built straight from nodes so building it takes no time.
        public static BinaryDecisionDiagram AllTrue(int variableCount)
        {
            var builder = new BinaryDecisionDiagramBuilder();
            int position = AlwaysPosition;
            for (int variable = variableCount - 1; variable >= 0; --variable)
            {
                position = builder.Make(variable, NeverPosition, position);
            }

            return new BinaryDecisionDiagram(builder, position);
        }

        public const int LongChain = 30000;

        public sealed class Sample
        {
            public BinaryDecisionDiagram Diagram;
            public BinaryDecisionDiagram Rewritten;
            public Func<int, bool> Reference;
        }

        // A random diagram, its meaning computed independently of BinaryDecisionDiagram, and the same diagram rebuilt
        // through other identities (De Morgan and the definition of xor).
        public static Sample RandomSample(Random random, int depth)
        {
            if (depth == 0 || random.Next(4) == 0)
            {
                int variable = random.Next(VariableCount);
                BinaryDecisionDiagram leaf = Var(variable);
                return new Sample
                {
                    Diagram = leaf,
                    Rewritten = ~~leaf,
                    Reference = mask => (mask >> variable & 1) != 0,
                };
            }

            Sample left = RandomSample(random, depth - 1);
            Sample right = RandomSample(random, depth - 1);
            switch (random.Next(4))
            {
                case 0:
                    return new Sample
                    {
                        Diagram = left.Diagram & right.Diagram,
                        Rewritten = ~(~left.Rewritten | ~right.Rewritten),
                        Reference = mask => left.Reference(mask) && right.Reference(mask),
                    };

                case 1:
                    return new Sample
                    {
                        Diagram = left.Diagram | right.Diagram,
                        Rewritten = ~(~left.Rewritten & ~right.Rewritten),
                        Reference = mask => left.Reference(mask) || right.Reference(mask),
                    };

                case 2:
                    return new Sample
                    {
                        Diagram = left.Diagram ^ right.Diagram,
                        Rewritten = (left.Rewritten & ~right.Rewritten) | (~left.Rewritten & right.Rewritten),
                        Reference = mask => left.Reference(mask) != right.Reference(mask),
                    };

                default:
                    return new Sample
                    {
                        Diagram = ~left.Diagram,
                        Rewritten = left.Rewritten ^ BinaryDecisionDiagram.Always,
                        Reference = mask => !left.Reference(mask),
                    };
            }
        }

        public static Sample[] RandomSamples(int seed, int count, int depth)
        {
            var random = new Random(seed);
            var returnMe = new Sample[count];
            for (int i = 0; i < count; ++i)
            {
                returnMe[i] = RandomSample(random, depth);
            }

            return returnMe;
        }

        public static bool[] TruthTable(Func<int, bool> predicate)
        {
            var returnMe = new bool[AssignmentCount];
            for (int mask = 0; mask < AssignmentCount; ++mask)
            {
                returnMe[mask] = predicate(mask);
            }

            return returnMe;
        }

        public static bool Subset(bool[] smaller, bool[] larger)
        {
            for (int i = 0; i < smaller.Length; ++i)
            {
                if (smaller[i] && !larger[i])
                {
                    return false;
                }
            }

            return true;
        }

        public static string FirstDisagreement(BinaryDecisionDiagram diagram, Func<int, bool> reference)
        {
            for (int mask = 0; mask < AssignmentCount; ++mask)
            {
                if (Eval(diagram, mask) != reference(mask))
                {
                    return diagram + " under " + mask;
                }
            }

            return "";
        }

        public static BinaryDecisionDiagram ParityOf(int variableCount)
        {
            BinaryDecisionDiagram returnMe = BinaryDecisionDiagram.Never;
            for (int variable = 0; variable < variableCount; ++variable)
            {
                returnMe ^= Var(variable);
            }

            return returnMe;
        }

        public class NeverTests : TestFixture
        {
            public void IsFalseUnderEveryAssignment()
            {
                for (int mask = 0; mask < AssignmentCount; ++mask)
                {
                    CheckFalse(Eval(BinaryDecisionDiagram.Never, mask));
                }
            }

            public void HasNoNodes()
            {
                CheckEqual(0, BinaryDecisionDiagram.Never.NodeCount);
            }

            public void IsNotAlways()
            {
                CheckNotEqual(BinaryDecisionDiagram.Always, BinaryDecisionDiagram.Never);
            }
        }

        public class AlwaysTests : TestFixture
        {
            public void IsTrueUnderEveryAssignment()
            {
                for (int mask = 0; mask < AssignmentCount; ++mask)
                {
                    Check(Eval(BinaryDecisionDiagram.Always, mask));
                }
            }

            public void HasNoNodes()
            {
                CheckEqual(0, BinaryDecisionDiagram.Always.NodeCount);
            }
        }

        public class CtorTests : TestFixture
        {
            public void OutcomeRoots_AreNeverAndAlways()
            {
                var builder = new BinaryDecisionDiagramBuilder();

                CheckEqual(BinaryDecisionDiagram.Never,
                    new BinaryDecisionDiagram(builder, NeverPosition));
                CheckEqual(BinaryDecisionDiagram.Always,
                    new BinaryDecisionDiagram(builder, AlwaysPosition));
            }

            public void SingleNode_IsTheVariable()
            {
                var builder = new BinaryDecisionDiagramBuilder();
                int root = builder.Make(2, NeverPosition, AlwaysPosition);

                CheckEqual(Var(2), new BinaryDecisionDiagram(builder, root));
            }

            public void NodesMadeInAnyOrder_GiveEqualDiagrams()
            {
                const int never = NeverPosition;
                const int always = AlwaysPosition;

                var inOrder = new BinaryDecisionDiagramBuilder();
                int rootInOrder = inOrder.Make(0, never, inOrder.Make(1, never, always));

                var withDetours = new BinaryDecisionDiagramBuilder();
                withDetours.Make(4, always, never);
                int second = withDetours.Make(1, never, always);
                withDetours.Make(0, second, always);
                int rootWithDetours = withDetours.Make(0, never, second);

                CheckEqual(Var(0) & Var(1), new BinaryDecisionDiagram(inOrder, rootInOrder));
                CheckEqual(Var(0) & Var(1), new BinaryDecisionDiagram(withDetours, rootWithDetours));
            }

            public void NodesTheRootDoesNotReach_AreIgnored()
            {
                var builder = new BinaryDecisionDiagramBuilder();
                builder.Make(3, NeverPosition, AlwaysPosition);
                int root = builder.Make(0, NeverPosition, AlwaysPosition);

                var diagram = new BinaryDecisionDiagram(builder, root);

                CheckEqual(1, diagram.NodeCount);
                CheckEqual(new[] { 0 }, Copy(diagram.Variables));
            }

            public void BuilderChangedAfterwards_DoesNotAffectTheDiagram()
            {
                var builder = new BinaryDecisionDiagramBuilder();
                int root = builder.Make(0, NeverPosition, AlwaysPosition);
                var diagram = new BinaryDecisionDiagram(builder, root);

                builder.Make(1, NeverPosition, AlwaysPosition);

                CheckEqual(Var(0), diagram);
            }

            public void VeryLongChainOnTheTrueSide_DoesNotOverflowTheStack()
            {
                CheckEqual(LongChain, AllTrue(LongChain).NodeCount);
            }

            public void VeryLongChainOnTheFalseSide_DoesNotOverflowTheStack()
            {
                var builder = new BinaryDecisionDiagramBuilder();
                int position = NeverPosition;
                for (int variable = LongChain - 1; variable >= 0; --variable)
                {
                    position = builder.Make(variable, position, AlwaysPosition);
                }

                var diagram = new BinaryDecisionDiagram(builder, position);

                CheckEqual(LongChain, diagram.NodeCount);
            }

            public void NullBuilder_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                new BinaryDecisionDiagram(null, NeverPosition);
            }

            public void RootBeyondTheEnd_Throws()
            {
                var builder = new BinaryDecisionDiagramBuilder();

                CheckThrow(typeof(ArgumentOutOfRangeException));
                new BinaryDecisionDiagram(builder, 2);
            }

            public void NegativeRoot_Throws()
            {
                var builder = new BinaryDecisionDiagramBuilder();

                CheckThrow(typeof(ArgumentOutOfRangeException));
                new BinaryDecisionDiagram(builder, -1);
            }
        }

        public class VariableTests : TestFixture
        {
            public void IsTrueExactlyWhenTheVariableIs()
            {
                Check(Eval(Var(2), MaskOf(2)));
                Check(Eval(Var(2), MaskOf(0, 2, 4)));
                CheckFalse(Eval(Var(2), 0));
                CheckFalse(Eval(Var(2), MaskOf(0, 1, 3, 4)));
            }

            public void IsOneNode()
            {
                CheckEqual(1, Var(3).NodeCount);
            }

            public void ReservedValue_Throws()
            {
                CheckThrow(typeof(ArgumentOutOfRangeException));
                BinaryDecisionDiagram.Variable(int.MaxValue);
            }

            public void LargestAllowedValue_Works()
            {
                CheckEqual(1, BinaryDecisionDiagram.Variable(int.MaxValue - 1).NodeCount);
            }
        }

        public class AndTests : TestFixture
        {
            public void IsTrueWhenBothAre()
            {
                BinaryDecisionDiagram diagram = Var(0) & Var(1);

                Check(Eval(diagram, MaskOf(0, 1)));
                CheckFalse(Eval(diagram, MaskOf(0)));
                CheckFalse(Eval(diagram, MaskOf(1)));
                CheckFalse(Eval(diagram, 0));
            }

            public void VeryLongChain_DoesNotOverflowTheStack()
            {
                BinaryDecisionDiagram diagram = Var(-1) & AllTrue(LongChain);

                CheckEqual(LongChain + 1, diagram.NodeCount);
            }

            public void WithItsNegation_IsNever()
            {
                CheckEqual(BinaryDecisionDiagram.Never, Var(0) & ~Var(0));
            }

            public void WithAlways_IsUnchanged()
            {
                CheckEqual(Var(0), Var(0) & BinaryDecisionDiagram.Always);
            }

            public void WithNever_IsNever()
            {
                CheckEqual(BinaryDecisionDiagram.Never, Var(0) & BinaryDecisionDiagram.Never);
            }

            public void NullLeft_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                BinaryDecisionDiagram unused = null & Var(0);
            }

            public void NullRight_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                BinaryDecisionDiagram unused = Var(0) & null;
            }
        }

        public class OrTests : TestFixture
        {
            public void IsTrueWhenEitherIs()
            {
                BinaryDecisionDiagram diagram = Var(0) | Var(1);

                Check(Eval(diagram, MaskOf(0)));
                Check(Eval(diagram, MaskOf(1)));
                Check(Eval(diagram, MaskOf(0, 1)));
                CheckFalse(Eval(diagram, 0));
            }

            public void VeryLongChain_DoesNotOverflowTheStack()
            {
                BinaryDecisionDiagram diagram = Var(-1) | AllTrue(LongChain);

                CheckEqual(LongChain + 1, diagram.NodeCount);
            }

            public void WithItsNegation_IsAlways()
            {
                CheckEqual(BinaryDecisionDiagram.Always, Var(0) | ~Var(0));
            }

            public void WithNever_IsUnchanged()
            {
                CheckEqual(Var(0), Var(0) | BinaryDecisionDiagram.Never);
            }

            public void WithAlways_IsAlways()
            {
                CheckEqual(BinaryDecisionDiagram.Always, Var(0) | BinaryDecisionDiagram.Always);
            }

            public void NullLeft_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                BinaryDecisionDiagram unused = null | Var(0);
            }

            public void NullRight_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                BinaryDecisionDiagram unused = Var(0) | null;
            }
        }

        public class XorTests : TestFixture
        {
            public void IsTrueWhenExactlyOneIs()
            {
                BinaryDecisionDiagram diagram = Var(0) ^ Var(1);

                Check(Eval(diagram, MaskOf(0)));
                Check(Eval(diagram, MaskOf(1)));
                CheckFalse(Eval(diagram, MaskOf(0, 1)));
                CheckFalse(Eval(diagram, 0));
            }

            public void VeryLongChain_DoesNotOverflowTheStack()
            {
                BinaryDecisionDiagram diagram = Var(-1) ^ AllTrue(LongChain);

                CheckEqual(2 * LongChain + 1, diagram.NodeCount);
            }

            public void WithItself_IsNever()
            {
                CheckEqual(BinaryDecisionDiagram.Never, Var(0) ^ Var(0));
            }

            public void WithAlways_IsTheNegation()
            {
                CheckEqual(~Var(0), Var(0) ^ BinaryDecisionDiagram.Always);
            }

            public void NullLeft_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                BinaryDecisionDiagram unused = null ^ Var(0);
            }

            public void NullRight_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                BinaryDecisionDiagram unused = Var(0) ^ null;
            }
        }

        public class NotTests : TestFixture
        {
            public void IsTrueWhereTheOperandIsNot()
            {
                BinaryDecisionDiagram diagram = ~Var(0);

                Check(Eval(diagram, 0));
                CheckFalse(Eval(diagram, MaskOf(0)));
            }

            public void VeryLongChain_DoesNotOverflowTheStack()
            {
                BinaryDecisionDiagram diagram = ~AllTrue(LongChain);

                CheckEqual(LongChain, diagram.NodeCount);
            }

            public void Twice_IsTheOriginal()
            {
                CheckEqual(Var(0) & Var(1), ~~(Var(0) & Var(1)));
            }

            public void OfNever_IsAlways()
            {
                CheckEqual(BinaryDecisionDiagram.Always, ~BinaryDecisionDiagram.Never);
            }

            public void OfAlways_IsNever()
            {
                CheckEqual(BinaryDecisionDiagram.Never, ~BinaryDecisionDiagram.Always);
            }

            public void Null_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                BinaryDecisionDiagram unused = ~(BinaryDecisionDiagram)null;
            }
        }

        public class EvaluateTests : TestFixture
        {
            public void ThreeWayCombination_IsTrueOnlyForThatCombination()
            {
                BinaryDecisionDiagram diagram = Var(0) & ~Var(1) & Var(2);

                Check(Eval(diagram, MaskOf(0, 2)));
                Check(Eval(diagram, MaskOf(0, 2, 4)));
                CheckFalse(Eval(diagram, MaskOf(0, 1, 2)));
                CheckFalse(Eval(diagram, MaskOf(0)));
            }

            public void XorOfOneVariableWithAnAnd_IsTrueForExactlyOneSide()
            {
                BinaryDecisionDiagram diagram = Var(0) ^ (Var(1) & Var(2));

                Check(Eval(diagram, MaskOf(0)));
                Check(Eval(diagram, MaskOf(0, 1)));
                Check(Eval(diagram, MaskOf(1, 2)));
                CheckFalse(Eval(diagram, MaskOf(0, 1, 2)));
                CheckFalse(Eval(diagram, MaskOf(1)));
            }

            public void RandomDiagrams_AgreeWithTheirReferenceUnderEveryAssignment()
            {
                foreach (Sample sample in RandomSamples(seed: 1, count: 200, depth: 4))
                {
                    CheckEqual("", FirstDisagreement(sample.Diagram, sample.Reference));
                    CheckEqual("", FirstDisagreement(sample.Rewritten, sample.Reference));
                }
            }
        }

        public class RootPositionTests : TestFixture
        {
            public void Outcomes_AreTheirOwnPositions()
            {
                CheckEqual(NeverPosition, BinaryDecisionDiagram.Never.RootPosition);
                CheckEqual(AlwaysPosition, BinaryDecisionDiagram.Always.RootPosition);
            }

            public void DecisionDiagram_StartsAfterTheNodesItGoesTo()
            {
                BinaryDecisionDiagram diagram = Var(0) & Var(1);

                CheckEqual(diagram.NodeCount + 1, diagram.RootPosition);
            }
        }

        public class NodeAccessTests : TestFixture
        {
            public void SingleVariable_AsksAboutItAndGoesToTheOutcomes()
            {
                BinaryDecisionDiagram diagram = Var(3);

                CheckEqual(3, diagram.VariableAt(diagram.RootPosition));
                CheckEqual(NeverPosition, diagram.IfFalseAt(diagram.RootPosition));
                CheckEqual(AlwaysPosition, diagram.IfTrueAt(diagram.RootPosition));
            }

            public void Outcomes_ReportTheReservedVariableAndGoToNever()
            {
                CheckEqual(BinaryDecisionDiagramBuilder.ReservedVariable, Var(3).VariableAt(AlwaysPosition));
                CheckEqual(NeverPosition, Var(3).IfFalseAt(AlwaysPosition));
                CheckEqual(NeverPosition, Var(3).IfTrueAt(NeverPosition));
            }

            public void Conjunction_GoesThroughTheLaterVariable()
            {
                BinaryDecisionDiagram diagram = Var(0) & Var(1);
                int root = diagram.RootPosition;

                CheckEqual(0, diagram.VariableAt(root));
                CheckEqual(NeverPosition, diagram.IfFalseAt(root));
                CheckEqual(1, diagram.VariableAt(diagram.IfTrueAt(root)));
            }

            public void PositionOutsideTheDiagram_Throws()
            {
                CheckThrow(typeof(ArgumentOutOfRangeException));
                Var(3).VariableAt(3);
            }

            public void NegativePosition_Throws()
            {
                CheckThrow(typeof(ArgumentOutOfRangeException));
                Var(3).IfFalseAt(-1);
            }

            public void IfTrueAtPositionOutsideTheDiagram_Throws()
            {
                CheckThrow(typeof(ArgumentOutOfRangeException));
                Var(3).IfTrueAt(3);
            }
        }

        public class VariablesTests : TestFixture
        {
            public void Never_HasNone()
            {
                CheckEqual(0, BinaryDecisionDiagram.Never.Variables.Count);
            }

            public void Always_HasNone()
            {
                CheckEqual(0, BinaryDecisionDiagram.Always.Variables.Count);
            }

            public void Variable_IsThatVariable()
            {
                CheckEqual(new[] { 3 }, Copy(Var(3).Variables));
            }

            public void VariablesBuiltOutOfOrder_AreListedAscending()
            {
                BinaryDecisionDiagram diagram = Var(4) & Var(1) & Var(3);

                CheckEqual(new[] { 1, 3, 4 }, Copy(diagram.Variables));
            }

            public void VariableUsedInSeveralNodes_IsListedOnce()
            {
                BinaryDecisionDiagram diagram = (Var(0) & Var(2)) | (~Var(0) & Var(1) & Var(2));

                CheckEqual(new[] { 0, 1, 2 }, Copy(diagram.Variables));
            }

            public void VariableThatCancelsOut_IsLeftOut()
            {
                BinaryDecisionDiagram diagram = (Var(0) & Var(1)) | (Var(0) & ~Var(1));

                CheckEqual(new[] { 0 }, Copy(diagram.Variables));
            }

            public void RandomDiagrams_ListExactlyTheVariablesTheirResultDependsOn()
            {
                foreach (Sample sample in RandomSamples(seed: 2, count: 200, depth: 4))
                {
                    var dependsOn = Enumerable.Range(0, VariableCount)
                        .Where(variable => Enumerable.Range(0, AssignmentCount).Any(
                            mask => sample.Reference(mask) != sample.Reference(mask ^ (1 << variable))))
                        .ToArray();

                    CheckEqual(dependsOn, Copy(sample.Diagram.Variables));
                }
            }
        }

        public class NodeCountTests : TestFixture
        {
            public void Variable_IsOne()
            {
                CheckEqual(1, Var(0).NodeCount);
            }

            public void EveryVariableAnded_NeedsOneNodePerVariable()
            {
                BinaryDecisionDiagram diagram = Var(0) & Var(1) & Var(2) & Var(3) & Var(4) & Var(5) & Var(6) & Var(7)
                    & Var(8) & Var(9);

                CheckEqual(10, diagram.NodeCount);
            }

            public void ParityOfManyVariables_GrowsLinearly()
            {
                CheckEqual(19, ParityOf(10).NodeCount);
            }
        }

        public class IsNeverTests : TestFixture
        {
            public void Never_IsNever()
            {
                Check(BinaryDecisionDiagram.Never.IsNever);
            }

            public void Always_IsNot()
            {
                CheckFalse(BinaryDecisionDiagram.Always.IsNever);
            }

            public void Variable_IsNot()
            {
                CheckFalse(Var(0).IsNever);
            }

            public void ContradictionBuiltFromVariables_IsNever()
            {
                Check((Var(0) & Var(1) & ~Var(0)).IsNever);
            }

            public void RandomDiagrams_AreNeverExactlyWhenNoAssignmentMakesThemTrue()
            {
                foreach (Sample sample in RandomSamples(seed: 3, count: 200, depth: 4))
                {
                    CheckEqual(!Enumerable.Range(0, AssignmentCount).Any(sample.Reference), sample.Diagram.IsNever);
                }
            }
        }

        public class TryFindWitnessTests : TestFixture
        {
            public void Never_HasNone()
            {
                CheckFalse(BinaryDecisionDiagram.Never.TryFindWitness(out int[] trueVariables));
                CheckEqual(0, trueVariables.Length);
            }

            public void Always_NeedsNothingTrue()
            {
                Check(BinaryDecisionDiagram.Always.TryFindWitness(out int[] trueVariables));
                CheckEqual(0, trueVariables.Length);
            }

            public void Variable_SetsThatVariable()
            {
                Check(Var(3).TryFindWitness(out int[] trueVariables));
                CheckEqual(new[] { 3 }, trueVariables);
            }

            public void NegatedVariable_SetsNothing()
            {
                Check((~Var(3)).TryFindWitness(out int[] trueVariables));
                CheckEqual(0, trueVariables.Length);
            }

            public void ABranchThatCanNeverBeTrue_IsSkipped()
            {
                Check((~Var(0) & Var(1)).TryFindWitness(out int[] trueVariables));
                CheckEqual(new[] { 1 }, trueVariables);
            }

            public void SeveralVariables_AreListedAscending()
            {
                Check((Var(4) & Var(0) & Var(2)).TryFindWitness(out int[] trueVariables));
                CheckEqual(new[] { 0, 2, 4 }, trueVariables);
            }

            public void RandomDiagrams_HaveAWitnessExactlyWhenSatisfiable_AndItSatisfiesThem()
            {
                foreach (Sample sample in RandomSamples(seed: 4, count: 200, depth: 4))
                {
                    bool found = sample.Diagram.TryFindWitness(out int[] trueVariables);

                    CheckEqual(Enumerable.Range(0, AssignmentCount).Any(sample.Reference), found);
                    if (found)
                    {
                        Check(Eval(sample.Diagram, MaskOf(trueVariables)));
                    }
                }
            }
        }

        public class ImpliesTests : TestFixture
        {
            public void Itself_IsImplied()
            {
                BinaryDecisionDiagram diagram = Var(0) | Var(1);

                Check(diagram.Implies(diagram));
            }

            public void ConjunctionImpliesEitherOperand()
            {
                BinaryDecisionDiagram conjunction = Var(0) & Var(1);

                Check(conjunction.Implies(Var(0)));
                Check(conjunction.Implies(Var(1)));
            }

            public void OperandDoesNotImplyConjunction()
            {
                CheckFalse(Var(0).Implies(Var(0) & Var(1)));
            }

            public void UnrelatedVariables_DoNotImplyEachOther()
            {
                CheckFalse(Var(0).Implies(Var(1)));
            }

            public void Never_ImpliesAnything()
            {
                Check(BinaryDecisionDiagram.Never.Implies(Var(0)));
                Check(BinaryDecisionDiagram.Never.Implies(BinaryDecisionDiagram.Never));
            }

            public void AnythingImpliesAlways()
            {
                Check(Var(0).Implies(BinaryDecisionDiagram.Always));
                Check(BinaryDecisionDiagram.Always.Implies(BinaryDecisionDiagram.Always));
            }

            public void Always_DoesNotImplyAnythingNarrower()
            {
                CheckFalse(BinaryDecisionDiagram.Always.Implies(Var(0)));
            }

            public void EquivalentDiagrams_ImplyEachOther()
            {
                BinaryDecisionDiagram first = Var(0) & Var(1);
                BinaryDecisionDiagram second = ~(~Var(1) | ~Var(0));

                Check(first.Implies(second));
                Check(second.Implies(first));
            }

            public void EitherOfTwoVariables_DoesNotImplyOne()
            {
                CheckFalse((Var(0) | Var(1)).Implies(Var(0)));
            }

            public void RandomPairs_AgreeWithBruteForce()
            {
                Sample[] samples = RandomSamples(seed: 5, count: 40, depth: 4);
                bool[][] tables = samples.Select(sample => TruthTable(sample.Reference)).ToArray();

                for (int i = 0; i < samples.Length; ++i)
                {
                    for (int j = 0; j < samples.Length; ++j)
                    {
                        CheckEqual(Subset(tables[i], tables[j]), samples[i].Diagram.Implies(samples[j].Diagram));
                    }
                }
            }

            public void Null_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                Var(0).Implies(null);
            }
        }

        public class EqualsTests : TestFixture
        {
            public void DiagramsBuiltDifferentlyButMeaningTheSame_AreEqual()
            {
                BinaryDecisionDiagram first = Var(0) & Var(1);
                BinaryDecisionDiagram second = ~(~Var(0) | ~Var(1));

                CheckEqual(first, second);
                Check(first.Equals(second));
                Check(first.Equals((object)second));
            }

            public void DifferentMeanings_AreNotEqual()
            {
                CheckNotEqual(Var(0), Var(1));
                CheckNotEqual(Var(0) & Var(1), Var(0) | Var(1));
            }

            public void Null_IsNotEqual()
            {
                CheckFalse(Var(0).Equals((BinaryDecisionDiagram)null));
                CheckFalse(Var(0).Equals((object)null));
            }

            public void AnotherType_IsNotEqual()
            {
                CheckFalse(Var(0).Equals("x0"));
            }

            public void DiagramsWithTheSameNodeCountButDifferentNodes_AreNotEqual()
            {
                CheckNotEqual(Var(0) & Var(1), Var(0) & Var(2));
            }

            public void DiagramsThatDifferOnlyInWhereTheirIfTrueEdgesGo_AreNotEqual()
            {
                BinaryDecisionDiagram noneTrue = ~Var(0) & ~Var(1) & ~Var(2);
                BinaryDecisionDiagram noTwoAndNotOnlyOne = ~Var(2) & (Var(0) | ~Var(1));

                CheckNotEqual(noneTrue, noTwoAndNotOnlyOne);
            }

            public void DiagramsThatDifferOnlyInWhereTheirIfFalseEdgesGo_AreNotEqual()
            {
                BinaryDecisionDiagram onlyZeroTrue = Var(0) & ~Var(1) & ~Var(2);
                BinaryDecisionDiagram noTwoAndNotBothZeroAndOne = ~Var(2) & ~(Var(0) & Var(1));

                CheckNotEqual(onlyZeroTrue, noTwoAndNotBothZeroAndOne);
            }

            public void RewrittenDiagrams_AreEqual()
            {
                foreach (Sample sample in RandomSamples(seed: 6, count: 200, depth: 4))
                {
                    CheckEqual(sample.Diagram, sample.Rewritten);
                }
            }

            public void RandomPairs_AreEqualExactlyWhenTheyMeanTheSame()
            {
                Sample[] samples = RandomSamples(seed: 7, count: 40, depth: 4);
                bool[][] tables = samples.Select(sample => TruthTable(sample.Reference)).ToArray();

                for (int i = 0; i < samples.Length; ++i)
                {
                    for (int j = 0; j < samples.Length; ++j)
                    {
                        CheckEqual(tables[i].SequenceEqual(tables[j]), samples[i].Diagram.Equals(samples[j].Diagram));
                    }
                }
            }
        }

        public class GetHashCodeTests : TestFixture
        {
            public void EqualDiagrams_HaveEqualHashCodes()
            {
                BinaryDecisionDiagram first = Var(0) & Var(1);
                BinaryDecisionDiagram second = ~(~Var(0) | ~Var(1));

                CheckEqual(first.GetHashCode(), second.GetHashCode());
            }

            public void DifferentDiagrams_HaveDifferentHashCodes()
            {
                CheckNotEqual(Var(0).GetHashCode(), Var(1).GetHashCode());
            }

            public void RewrittenDiagrams_HaveEqualHashCodes()
            {
                foreach (Sample sample in RandomSamples(seed: 8, count: 100, depth: 4))
                {
                    CheckEqual(sample.Diagram.GetHashCode(), sample.Rewritten.GetHashCode());
                }
            }
        }

        public class ToStringTests : TestFixture
        {
            public void Never_SaysSo()
            {
                CheckEqual("Never", BinaryDecisionDiagram.Never.ToString());
            }

            public void Always_SaysSo()
            {
                CheckEqual("Always", BinaryDecisionDiagram.Always.ToString());
            }

            public void Variable_IsNamedByNumberByDefault()
            {
                CheckEqual("x3", Var(3).ToString());
            }

            public void Variable_IsNamedByTheCallbackWhenGiven()
            {
                CheckEqual("v3", Var(3).ToString(variable => "v" + variable));
            }

            public void Negation_PutsABangBeforeIt()
            {
                CheckEqual("!x0", (~Var(0)).ToString());
            }

            public void Conjunction_JoinsWithAnd()
            {
                CheckEqual("x0 & x1", (Var(0) & Var(1)).ToString());
            }

            public void Disjunction_JoinsDisjointCasesWithOr()
            {
                CheckEqual("x0 | !x0 & x1", (Var(0) | Var(1)).ToString());
            }

            public void BranchingOnBothSides_GivesEachPathItsOwnLiterals()
            {
                BinaryDecisionDiagram diagram = (Var(0) & Var(1)) | (~Var(0) & Var(2));

                CheckEqual("x0 & x1 | !x0 & x2", diagram.ToString());
            }

            public void ABranchNestedUnderATrueBranch_DoesNotLeakItsLiteralsIntoLaterPaths()
            {
                BinaryDecisionDiagram diagram = Var(0) & (Var(1) | Var(2));

                CheckEqual("x0 & x1 | x0 & !x1 & x2", diagram.ToString());
            }

            public void ThreeVariableParity_ListsEveryPathExactly()
            {
                CheckEqual("x0 & x1 & x2 | x0 & !x1 & !x2 | !x0 & x1 & !x2 | !x0 & !x1 & x2",
                    ParityOf(3).ToString());
            }

            public void SixteenCases_AreAllShown()
            {
                string text = ParityOf(5).ToString();

                CheckFalse(text.EndsWith("..."));
                CheckEqual(16, text.Split(new[] { " | " }, StringSplitOptions.None).Length);
            }

            public void MoreThanSixteenCases_AreCutShort()
            {
                string text = ParityOf(6).ToString();

                Check(text.EndsWith(" | ..."));
                CheckEqual(17, text.Split(new[] { " | " }, StringSplitOptions.None).Length);
            }

            public void VeryLongChain_DoesNotOverflowTheStack()
            {
                string text = AllTrue(LongChain).ToString();

                Check(text.StartsWith("x0 & x1 & x2 & "));
                Check(text.EndsWith(" & x" + (LongChain - 1)));
            }

            public void NullNamer_Throws()
            {
                CheckThrow(typeof(ArgumentNullException));
                Var(0).ToString(null);
            }
        }
    }
}