using System.IO;
using System.Linq;
using UnitTestSharp;
using Vellum;

namespace Amphora.Vellum.UnitTests
{
    public class BinaryDecisionDiagramConverterTests : TestFixture
    {
        public static SaveSession Session()
        {
            return SaveConverters.For(typeof(BinaryDecisionDiagramConverterTests).Assembly).CreateSession();
        }

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

        public static BinaryDecisionDiagram ThroughLuaText(BinaryDecisionDiagram value)
        {
            SaveSession session = Session();
            SaveNode save = SaveNode.NewTable();
            save.Entries["value"] = session.ToNode(value, typeof(BinaryDecisionDiagram));
            SaveNode read = LuaSaveFormat.Parse(LuaSaveFormat.Format(save));
            return (BinaryDecisionDiagram)session.FromNode(read.RequireEntry("value"),
                typeof(BinaryDecisionDiagram));
        }

        /// <summary>
        /// Returns a saved node asking about <paramref name="variable"/>, going to the positions given.
        /// </summary>
        public static SaveNode Decision(int variable, int ifFalse, int ifTrue)
        {
            SaveNode returnMe = SaveNode.NewTable();
            returnMe.Entries[BinaryDecisionDiagramConverter.VariableKey] = SaveNode.OfText(variable.ToString());
            returnMe.Entries[BinaryDecisionDiagramConverter.IfFalseKey] = SaveNode.OfText(ifFalse.ToString());
            returnMe.Entries[BinaryDecisionDiagramConverter.IfTrueKey] = SaveNode.OfText(ifTrue.ToString());
            return returnMe;
        }

        public static SaveNode Saved(int root, params SaveNode[] nodes)
        {
            SaveNode list = SaveNode.NewList();
            list.Items.AddRange(nodes);
            SaveNode returnMe = SaveNode.NewTable();
            returnMe.Entries[BinaryDecisionDiagramConverter.NodesKey] = list;
            returnMe.Entries[BinaryDecisionDiagramConverter.RootKey] = SaveNode.OfText(root.ToString());
            return returnMe;
        }

        public static BinaryDecisionDiagram Loaded(SaveNode node)
        {
            return (BinaryDecisionDiagram)Session().FromNode(node, typeof(BinaryDecisionDiagram));
        }

        public class WriteTests : TestFixture
        {
            public void Never_IsNoNodesStartingAtTheNeverOutcome()
            {
                SaveNode node = Session().ToNode(BinaryDecisionDiagram.Never, typeof(BinaryDecisionDiagram));

                CheckEqual(0, node.RequireEntry("nodes").Items.Count);
                CheckEqual("0", node.RequireEntry("root").Text);
            }

            public void Always_IsNoNodesStartingAtTheAlwaysOutcome()
            {
                SaveNode node = Session().ToNode(BinaryDecisionDiagram.Always, typeof(BinaryDecisionDiagram));

                CheckEqual(0, node.RequireEntry("nodes").Items.Count);
                CheckEqual("1", node.RequireEntry("root").Text);
            }

            public void SingleVariable_IsOneNodeGoingToTheOutcomes()
            {
                SaveNode node = Session().ToNode(Var(3), typeof(BinaryDecisionDiagram));
                SaveNode only = node.RequireEntry("nodes").Items.Single();

                CheckEqual("2", node.RequireEntry("root").Text);
                CheckEqual("3", only.RequireEntry("variable").Text);
                CheckEqual("0", only.RequireEntry("ifFalse").Text);
                CheckEqual("1", only.RequireEntry("ifTrue").Text);
            }

            public void Conjunction_ListsTheLaterVariableFirst()
            {
                SaveNode node = Session().ToNode(Var(0) & Var(1), typeof(BinaryDecisionDiagram));
                SaveNode[] nodes = node.RequireEntry("nodes").Items.ToArray();

                CheckEqual("1", nodes[0].RequireEntry("variable").Text);
                CheckEqual("0", nodes[1].RequireEntry("variable").Text);
                CheckEqual("2", nodes[1].RequireEntry("ifTrue").Text);
                CheckEqual("3", node.RequireEntry("root").Text);
            }

            public void NullDiagram_IsNull()
            {
                CheckEqual(SaveNode.Kinds.Null,
                    Session().ToNode(null, typeof(BinaryDecisionDiagram)).Kind);
            }
        }

        public class ReadTests : TestFixture
        {
            public void Diagrams_RoundTripToEqualOnes()
            {
                BinaryDecisionDiagram[] diagrams =
                {
                    BinaryDecisionDiagram.Never,
                    BinaryDecisionDiagram.Always,
                    Var(0),
                    ~Var(2),
                    Var(0) & Var(1),
                    (Var(0) & Var(1)) | Var(2),
                    Var(0) ^ Var(3),
                    (Var(1) ^ Var(2)) & ~(Var(0) | Var(4)),
                };

                foreach (BinaryDecisionDiagram diagram in diagrams)
                {
                    BinaryDecisionDiagram loaded = ThroughLuaText(diagram);

                    CheckTrue(diagram.Equals(loaded));
                    CheckEqual(diagram.GetHashCode(), loaded.GetHashCode());
                    CheckEqual(diagram.NodeCount, loaded.NodeCount);
                }
            }

            public void LoadedDiagram_MeansTheSameFunction()
            {
                BinaryDecisionDiagram original = (Var(1) ^ Var(2)) & ~(Var(0) | Var(4));
                BinaryDecisionDiagram loaded = ThroughLuaText(original);

                for (int mask = 0; mask < 32; ++mask)
                {
                    CheckEqual(original.Evaluate(new Bits(mask)), loaded.Evaluate(new Bits(mask)));
                }
            }

            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 void NodeThatGoesTheSameWayEitherWay_LoadsReduced()
            {
                BinaryDecisionDiagram loaded = Loaded(Saved(2, Decision(0, 1, 1)));

                CheckTrue(BinaryDecisionDiagram.Always.Equals(loaded));
            }

            public void TwoEqualNodes_LoadAsOneAndTheNodeAboveThemReduces()
            {
                BinaryDecisionDiagram loaded = Loaded(Saved(4, Decision(1, 0, 1), Decision(1, 0, 1),
                    Decision(0, 2, 3)));

                CheckTrue(Var(1).Equals(loaded));
            }

            public void TwoEqualNodes_LoadAsOneWhenTheNodeAboveStillDiffers()
            {
                BinaryDecisionDiagram loaded = Loaded(Saved(5, Decision(2, 0, 1), Decision(2, 0, 1),
                    Decision(1, 2, 1), Decision(0, 3, 4)));

                CheckEqual(3, loaded.NodeCount);
            }

            public void MissingNodes_Throw()
            {
                SaveNode node = SaveNode.NewTable();
                node.Entries["root"] = SaveNode.OfText("1");

                CheckThrow(typeof(InvalidDataException));
                Loaded(node);
            }

            public void MissingRoot_Throws()
            {
                SaveNode node = Saved(1);
                node.Entries.Remove("root");

                CheckThrow(typeof(InvalidDataException));
                Loaded(node);
            }

            public void RootPastTheLastNode_Throws()
            {
                CheckThrow(typeof(InvalidDataException));
                Loaded(Saved(3, Decision(0, 0, 1)));
            }

            public void NegativeRoot_Throws()
            {
                CheckThrow(typeof(InvalidDataException));
                Loaded(Saved(-1));
            }

            public void NodeGoingToItself_Throws()
            {
                CheckThrow(typeof(InvalidDataException));
                Loaded(Saved(2, Decision(0, 2, 1)));
            }

            public void NodeGoingToALaterNode_Throws()
            {
                CheckThrow(typeof(InvalidDataException));
                Loaded(Saved(3, Decision(0, 3, 1), Decision(1, 0, 1)));
            }

            public void NodeGoingToANegativePosition_Throws()
            {
                CheckThrow(typeof(InvalidDataException));
                Loaded(Saved(2, Decision(0, -1, 1)));
            }

            public void NodeAskingAboutAnEarlierVariableThanItsDestination_Throws()
            {
                CheckThrow(typeof(InvalidDataException));
                Loaded(Saved(3, Decision(0, 0, 1), Decision(1, 2, 1)));
            }

            public void NodeAskingAboutTheReservedVariable_Throws()
            {
                CheckThrow(typeof(InvalidDataException));
                Loaded(Saved(2, Decision(int.MaxValue, 0, 1)));
            }

            public void NodeWithMissingEntry_Throws()
            {
                SaveNode node = Decision(0, 0, 1);
                node.Entries.Remove("ifTrue");

                CheckThrow(typeof(InvalidDataException));
                Loaded(Saved(2, node));
            }

            public void NodeThatIsNotATable_Throws()
            {
                CheckThrow(typeof(InvalidDataException));
                Loaded(SaveNode.OfText("never"));
            }

            public void NullForADiagram_IsNull()
            {
                CheckNull(Session().FromNode(SaveNode.Null, typeof(BinaryDecisionDiagram)));
            }
        }

        public class TryListChildrenTests : TestFixture
        {
            public void DiagramOfBuiltInValues_ListsNothingAndSucceeds()
            {
                SaveNode node = Session().ToNode(Var(1) & Var(2), typeof(BinaryDecisionDiagram));
                var children = new ChildList();

                CheckTrue(new BinaryDecisionDiagramConverter().TryListChildren(node, children));
                CheckEqual(0, children.Count);
            }

            public void NodeWithoutNodes_ReturnsFalse()
            {
                CheckFalse(new BinaryDecisionDiagramConverter().TryListChildren(SaveNode.NewTable(), new ChildList()));
            }

            public void NodeThatIsNotATable_ReturnsFalse()
            {
                CheckFalse(new BinaryDecisionDiagramConverter().TryListChildren(SaveNode.OfText("3"), new ChildList()));
            }
        }
    }
}