using System;
using System.Collections.Generic;
using System.Text;
using System.Collections;
using CLab.Exceptions;
using CLab.Auxiliary;

namespace CLab
{
    public class Layout
    {

        private int bddVarNum;
        private Hashtable typeNameToIndex;
        private List<LayoutType> layoutTypes;
        private Hashtable variableNameToIndex;
        private List<LayoutVariable> layoutVariables;
        private CP cp;
        StringComparer stringComparer;

        public Layout(CP cp)
        {
            stringComparer = StringComparer.Create(System.Globalization.CultureInfo.CurrentCulture, true);
            this.cp = cp;
            typeNameToIndex = new Hashtable(stringComparer);
            variableNameToIndex = new Hashtable(stringComparer);
            layoutTypes = new List<LayoutType>();
            layoutVariables = new List<LayoutVariable>();
            makeBoolType();
            makeTypeObjects();
            makeVariableObjects();
        }

        public int BddVarNum
        {
            get { return bddVarNum; }
        }

        public Hashtable TypeNameToIndex
        {
            get { return typeNameToIndex; }
        }

        public List<LayoutType> LayoutTypes
        {
            get { return layoutTypes; }
        }

        public Hashtable VariableNameToIndex
        {
            get { return variableNameToIndex; }
        }

        public List<LayoutVariable> LayoutVariables
        {
            get { return layoutVariables; }
        }
 
        public void makeBoolType()
        {
            layoutTypes.Add(new LayoutTypeBool("bool", 2));
            typeNameToIndex["bool"] = layoutTypes.Count - 1;
        }

        public void makeTypeObjects()
        {
            for (int i = 0; i < cp.Types.Count; i++)
            {
                Type type = cp.Types[i];
                if (type.GetType() == typeof(CLab.TypeEnumeration))
                {
                    Hashtable valueToIndex = new Hashtable(stringComparer);
                    ArrayList indexToValue = new ArrayList();
                    TypeEnumeration t = (TypeEnumeration)cp.Types[i];
                    foreach (String enumerator in t.EnumeratorsList)
                    {
                        indexToValue.Add(enumerator);
                        valueToIndex[enumerator] = indexToValue.Count - 1;
                    }
                    int domainSize = indexToValue.Count;
                    layoutTypes.Add(new LayoutTypeEnumeration(t.TypeName, domainSize, indexToValue, valueToIndex));
                    typeNameToIndex[t.TypeName] = layoutTypes.Count - 1;
                }
                else if (type.GetType() == typeof(CLab.TypeRange))
                {
                    TypeRange t = (TypeRange)cp.Types[i];
                    int domainSize = t.EndOfRange - t.StartOfRange + 1;
                    layoutTypes.Add(new LayoutTypeRange(t.TypeName, t.StartOfRange, domainSize));
                    typeNameToIndex[t.TypeName] = layoutTypes.Count - 1;
                }
                else throw new ClabInternalErrorException(string.Format("Type '{0}' is not a valid type. Valid types should consist of a type name, and either a range '[x1 .. xn]' or a value list '{{v1, v2, v3}}'", cp.Types[i].TypeName));
            }
        }

        public void makeVariableObjects()
        {
            int nextBDDvar = 0;
            for (int i = 0; i < cp.Variables.Count; i++)
            {
                Variable v = cp.Variables[i];
                int? typeIndexNumber = null;
                if (string.Compare(v.TypeName, "bool", true) == 0)
                    typeIndexNumber = (int?)typeNameToIndex["bool"];
                else typeIndexNumber = (int?)typeNameToIndex[v.TypeName];
                if (typeIndexNumber == null) 
                    throw new ClabInternalErrorException(String.Format("Type '{0}' used by variable '{1}' is not a valid variable type. Valid variable types should be defined in the element 'type'. In addition, ClabSharp has a built-in boolean type 'bool' which can be used.", v.TypeName, v.VariableName));
                LayoutType lt = (LayoutType)layoutTypes[(int)typeIndexNumber];
                layoutVariables.Add(new LayoutVariable(BooleanVector(nextBDDvar, (int)lt.BDDvarNum), (int)typeIndexNumber));
                nextBDDvar += (int) lt.BDDvarNum;
                Console.WriteLine(v.VariableName);
                variableNameToIndex[v.VariableName] = layoutVariables.Count - 1;
            }
            bddVarNum = nextBDDvar;
        }

        public List<int> BooleanVector(int nextBDDvar, int varNumber)
        {
            List<int> res = new List<int>();
            for (int i = varNumber - 1; i >= 0; i--)
            {
                res.Add(nextBDDvar + i);
            }
            return res;
        }

        public override String ToString()
        {
            String res = "";
            res += "\n\n**** BINARY ENCODING OF TYPES ***** \n";

            for (int i = 0; i < layoutTypes.Count; i++)
            {
                res += ((Type)layoutTypes[i]).ToString() + "\n";
            }

            res += "\n\n**** BINARY ENCODING OF VARIABLES *****\n";

            for (int i = 0; i < layoutVariables.Count; i++)
            {
                res += layoutVariables[i].ToString();
            }

            res += "\n\ntypeNameToIndex \n";
            ICollection col = typeNameToIndex.Keys;
            IEnumerator en = col.GetEnumerator();
            while (en.MoveNext())
            {
                res += en.Current + " = ";
                res += typeNameToIndex[en.Current] + ", ";
            }

            res += "\n\nvarNameToIndex \n";
            col = variableNameToIndex.Keys;
            en = col.GetEnumerator();
            while (en.MoveNext())
            {
                res += en.Current + " = ";
                res += variableNameToIndex[en.Current] + ", ";
            }
            
            res += "\n\nTotal number of BDD variables in encoding: " + bddVarNum + "\n";
            
            return res;
        }
    }
}