/*========================================================================
        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 buddy_sharp;

namespace CLab.BDD
{
    /// <summary>
    /// Class which is used to get valid assignment data from the result BDD of the CP problem.
    /// Contains data structures which is filled with result data by Buddy_sharp and Buddy. 
    /// </summary>
    public class ValidAssignmentData
    {

        private int cpVarNum;
        private int[] dom;
        private int[] bddVarToCpVar;
        private int[] domStart;
        private BDDLayout layout;
       
        /// <summary>
        /// Initializes a new instance of the <see cref="T:ValidAssignmentData"/> class.
        /// </summary>
        /// <param name="layout">The <see cref="T:BDDLayout"></see> instance.</param>
        public ValidAssignmentData(BDDLayout layout)
        {
            this.layout = layout;
            CreateValidAssignmentStructures(layout);
        }

        /// <summary>
        /// Gets the number of CP variables.
        /// </summary>
        public int CpVarNum
        {
            get { return cpVarNum; }
        }

        /// <summary>
        /// Gets the list of domain size for each variable.
        /// </summary>
        public int[] Dom
        {
            get { return dom; }
        }

        /// <summary>
        /// Gets the Bdd variable to CP variable mapping.
        /// </summary>
        public int[] BddVarTocpVar
        {
            get { return bddVarToCpVar; }
        }

        /// <summary>
        /// Gets the list with the index of the BDD variable where the encoding of each CP variable starts.
        /// DomStart[i] = index of the BDD variable where the encoding of CSP variable "i" starts  
        /// </summary>
        public int[] DomStart
        {
            get { return domStart; }
        }

        /// <summary>
        /// Creates the valid assignment data structures.
        /// For internal use by this class.
        /// </summary>
        /// <param name="layout">The <see cref="T:BDDLayout"></see> instance.</param>
        private void CreateValidAssignmentStructures(BDDLayout layout)
        {
            cpVarNum = layout.LayoutVariables.Count;
            dom = new int[cpVarNum];
            domStart = new int[cpVarNum];
            bddVarToCpVar = new int[layout.BddVarNum];
            for (int i = 0; i < cpVarNum; i++)
            {
                BDDVariable lv = layout.LayoutVariables[i];
                BDDType lt = layout.LayoutTypes[lv.TypeIndex];
                dom[i] = lt.DomainSize;
                domStart[i] = (int) lv.BddVar[lv.BddVar.Count - 1];
                for (int j = 0; j < lv.BddVar.Count; j++) bddVarToCpVar[(int) lv.BddVar[j]] = i; 
            }
        }

        /// <summary>
        /// Method to create the valid assignment data. Use the Bdd.valExist(i, j) method
        /// to retrieve the results.
        /// </summary>
        /// <param name="resultBdd">The result BDD to create the valid assigment data on.</param>
        public void CreateValidAssignmentData(Bdd resultBdd)
        {
            Bdd.ClabBegin(dom, cpVarNum);
            Bdd.ExtractValues(resultBdd, dom, domStart, cpVarNum, bddVarToCpVar);
        }

        /// <summary>
        /// Runs the ClabEnd method of <see cref="T:buddy_sharp.Bdd"></see>.
        /// </summary>
        public void ClabEnd() 
        {
            Bdd.ClabEnd(cpVarNum);
        
        }

        /// <summary>
        /// Returns a <see cref="T:System.String"></see> that represents the current <see cref="T:ValidAssignmentData"></see>.
        /// </summary>
        /// <returns>
        /// A <see cref="T:System.String"></see> that represents the current <see cref="T:ValidAssignmentData"></see>.
        /// </returns>
        public override String ToString()
        {
            String res = "";
            res += "cpVarNum = " + cpVarNum + "\n";
            res += "dom = \n";
            for (int i = 0; i < dom.Length; i++)
            {
                res += "" +i + " -> " +dom[i] + ", ";
            }
            res += "\ndomStart = \n";
            for (int i = 0; i < domStart.Length; i++)
            {
                res += "" + i + " -> " + domStart[i] +", ";
            }
            res += "\nbddVarTocpVar = \n";
            for (int i = 0; i < bddVarToCpVar.Length; i++)
            {
                res += "" + i + " -> " + bddVarToCpVar[i] + ", "; 
            }
            res += "\nvalExist = \n";
            for (int i = 0; i < cpVarNum; i++)
            {
                BDDVariable lv = layout.LayoutVariables[i];
                BDDType lt = layout.LayoutTypes[lv.TypeIndex];
                res += "" + i + " : ";
                for (int j = 0; j < lt.DomainSize; j++)
                {
                    res += "" + j + " -> " + Bdd.ValExist(i, j) + ", ";
                }
                res += "\n";
            }
            return res;
        }
    }
}