/*========================================================================
        Copyright (C) 2006 by Geir-Tore Lindsve, Torbjørn Meistad 
        and Yngve Raudberget, hereby refered to as "the authors".
        Based on the CLab source code developed by Rune Møller Jensen.
                        All rights reserved

    Permission is hereby granted, without written agreement and without
    license or royalty fees, to use, reproduce, prepare derivative
    works, distribute, and display this software and its documentation
    for NONCOMMERCIAL RESEARCH AND EDUCATIONAL PURPOSES, provided 
    that (1) the above copyright notice and the following two paragraphs 
    appear in all copies of the source code and (2) redistributions, 
    including without limitation binaries, reproduce these notices in 
    the supporting documentation. 

    IN NO EVENT SHALL THE AUTHORS, OR DISTRIBUTORS OF THIS SOFTWARE 
    BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, 
    OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE 
    AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE ABOVE 
    PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

    THE AUTHORS SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
    MODIFICATIONS.
========================================================================*/

using System;
using System.Collections.Generic;
using System.Text;
using System.Collections;

using CLab.Exceptions;
using CLab.Data;

namespace CLab.BDD
{
    /// <summary>
    /// Class representing and making the layout of the BDD problem. 
    /// The class has mapping from the CLab <see cref="T:CLab.Data.CP"></see> representation to the BDD
    /// representation and vice versa.
    /// </summary>
    public class BDDLayout
    {

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

        /// <summary>
        /// Initializes a new instance of the <see cref="T:BDDLayout"/> class.
        /// </summary>
        /// <param name="cp">The <see cref="T:CLab.Data.CP"></see> instance of the problem.</param>
        /// <exception cref="CLab.Exceptions.ClabInternalErrorException"/>
        public BDDLayout(CP cp)
        {
            stringComparer = StringComparer.Create(System.Globalization.CultureInfo.CurrentCulture, true);
            this.cp = cp;
            typeNameToIndex = new Hashtable(stringComparer);
            variableNameToIndex = new Hashtable(stringComparer);
            layoutTypes = new List<BDDType>();
            layoutVariables = new List<BDDVariable>();
            makeBoolType();
            try
            {
                makeTypeObjects();
                makeVariableObjects();
            }
            catch (ClabInternalErrorException)
            {
                throw;
            }
        }

        /// <summary>
        /// Gets the number of BDD variables.
        /// </summary>
        /// <value>The BDD var num.</value>
        public int BddVarNum
        {
            get { return bddVarNum; }
        }

        /// <summary>
        /// Gets the hash table mapping type names to index.
        /// </summary>
        public Hashtable TypeNameToIndex
        {
            get { return typeNameToIndex; }
        }

        /// <summary>
        /// Gets the the list of types used by layout.
        /// </summary>
        /// <value>The layout types.</value>
        public List<BDDType> LayoutTypes
        {
            get { return layoutTypes; }
        }

        /// <summary>
        /// Gets the hash table mapping variable names to index.
        /// </summary>
        public Hashtable VariableNameToIndex
        {
            get { return variableNameToIndex; }
        }

        /// <summary>
        /// Gets the variables used by layout.
        /// </summary>
        public List<BDDVariable> LayoutVariables
        {
            get { return layoutVariables; }
        }

        /// <summary>
        /// Makes the bool type. For internal use by this class.
        /// </summary>
        private void makeBoolType()
        {
            layoutTypes.Add(new BDDTypeBool("bool", 2));
            typeNameToIndex["bool"] = layoutTypes.Count - 1;
        }

        /// <summary>
        /// Makes the <see cref="T:CLab.BDD.BDDLayoutType"></see> 
        /// objects using the CP representation. 
        /// For internal use by this class.
        /// </summary>
        /// <exception cref="ClabInternalErrorException"/>
        private void makeTypeObjects()
        {
            for (int i = 0; i < cp.Types.Count; i++)
            {
                CLab.Data.Type type = cp.Types[i];
                if (type.GetType() == typeof(CLab.Data.TypeEnum))
                {
                    Hashtable valueToIndex = new Hashtable(stringComparer);
                    ArrayList indexToValue = new ArrayList();
                    TypeEnum t = (TypeEnum)cp.Types[i];
                    foreach (String enumerator in t.EnumeratorsList)
                    {
                        indexToValue.Add(enumerator);
                        valueToIndex[enumerator] = indexToValue.Count - 1;
                    }
                    int domainSize = indexToValue.Count;
                    layoutTypes.Add(new BDDTypeEnum(t.TypeName, domainSize, indexToValue, valueToIndex));
                    typeNameToIndex[t.TypeName] = layoutTypes.Count - 1;
                }
                else if (type.GetType() == typeof(CLab.Data.TypeRange))
                {
                    TypeRange t = (TypeRange)cp.Types[i];
                    int domainSize = t.EndOfRange - t.StartOfRange + 1;
                    layoutTypes.Add(new BDDTypeRange(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));
            }
        }

        /// <summary>
        /// Makes the <see cref="CLab.BDD.BDDLayoutVariable"></see> classes of the 
        /// using the CP representation of the problem. 
        /// For internal use by this class.
        /// </summary>
        /// <exception cref="ClabInternalErrorException"/>
        private 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));
                BDDType lt = (BDDType)layoutTypes[(int)typeIndexNumber];
                layoutVariables.Add(new BDDVariable(BooleanVector(nextBDDvar, (int)lt.BDDvarNum), (int)typeIndexNumber));
                nextBDDvar += (int) lt.BDDvarNum;
                Console.WriteLine(v.VariableName);
                variableNameToIndex[v.VariableName] = layoutVariables.Count - 1;
            }
            bddVarNum = nextBDDvar;
        }

        /// <summary>
        /// Makes boolean vectors of variables.
        /// </summary>
        /// <param name="nextBDDvar">The next BDD variable.</param>
        /// <param name="varNumber">The variable number.</param>
        /// <returns>List representing the boolean vector.</returns>
        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;
        }

        /// <summary>
        /// Returns a <see cref="T:System.String"></see> that represents the current <see cref="T:CLab.BDD.BDDLayout"></see>.
        /// </summary>
        /// <returns>
        /// A <see cref="T:System.String"></see> that represents the current <see cref="T:CLab.BDD.BDDLayout"></see>.
        /// </returns>
        public override String ToString()
        {
            String res = "";
            res += "\n\n**** BINARY ENCODING OF TYPES ***** \n";

            for (int i = 0; i < layoutTypes.Count; i++)
            {
                res += ((CLab.Data.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;
        }
    }
}