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

using CLab.Exceptions;
using CLab.Data;

namespace CLab.BDD
{
    /// <summary>
    /// The main class for finding valid solutions the BDD way.
    /// The class is designed to be used by <see cref="T:CLab.Clab"></see>, which
    /// provides the data needed for this class to work. 
    /// </summary>
    public class ClabBDD
    {
        private Clab clab;
        private BDDLayout layout;
        private BDDSpace space;
        private Bdd resultBdd;
        private Boolean resultBddMade = false;
        private BddCompileMethod compileMethod;
        private ValidAssignmentData validAsnData;
        private ValidDomains vDomains;
        private CP cp;
        private Symbols symbols;
        private Hashtable cpVarNameToVDomainID;

        /// <summary>
        /// Initializes a new instance of the <see cref="T:ClabBDD"/> class.
        /// </summary>
        /// <param name="clab">The current Clab instance.</param>
        /// <param name="cp">The cp object of the problem.</param>
        /// <param name="symbols">The symbols object of the problem.</param>
        /// <param name="initdbcache">The initial db cache.</param>
        /// <param name="initbddnodes">The initial number of bdd nodes.</param>
        /// <param name="maxincrease">The maximum increase number.</param>
        /// <exception cref="CLab.Exceptions.ClabException"/>
        public ClabBDD(Clab clab, CP cp, Symbols symbols, int initdbcache, int initbddnodes, int maxincrease)
        {
            compileMethod = BddCompileMethod.cm_static;
            this.clab = clab;
            clab.SetStatusUpdateCount(cp.Rules.Count * 2);
            this.cp = cp;
            this.symbols = symbols;
            cpVarNameToVDomainID = new Hashtable();
            try
            {
                layout = new BDDLayout(cp);
                Console.WriteLine("Initializing 'Buddy#'...");
                Bdd.Init(initbddnodes, initdbcache);
                Bdd.SetMaxIncrease(maxincrease);
                Bdd.SetVarNum(layout.BddVarNum);
                Console.WriteLine("Making space...");
                space = new BDDSpace(cp, layout, symbols, this);
                validAsnData = new ValidAssignmentData(layout);
                CreateValidDomainsData();
            }
            catch (ClabInternalErrorException e)
            {
                throw new ClabException(e.Message, e);
            }
        }

        /// <summary>
        /// Gets the <see cref="BDDLayout"></see> of the problem.
        /// </summary>
        public BDDLayout Layout
        {
            get { return layout; }
        }

        /// <summary>
        /// Gets the <see cref="BDDSpace"></see> of the problem.
        /// </summary>
        public BDDSpace Space
        {
            get { return space; }
        }

        /// <summary>
        /// Gets the unsatisfiable rule if one exist.
        /// </summary>
        public String UnsatisfiableRule
        {
            get { return Space.UnsatisfiableRule; }
        }

        /// <summary>
        /// Prints the specified list of BDDs.
        /// </summary>
        /// <param name="b">The list of BDDs.</param>
        public void printout(List<Bdd> b)
        {
            Console.WriteLine("\n");
            for (int i = 0; i < b.Count; i++)
            {
                Bdd.PrintSet(b[i]);
            }
        }

        /// <summary>
        /// Method which creates the <see cref="T:ValidDomains"></see>
        /// object and fills it with the problem data.
        /// </summary>
        private void CreateValidDomainsData()
        {
            vDomains = new ValidDomains();
            List<Variable> variables = cp.Variables;

            foreach (Variable cpVar in variables)
            {
                String typeName = cpVar.TypeName;
                int typeIndex = (int) layout.TypeNameToIndex[typeName];
                BDDType lt = layout.LayoutTypes[typeIndex];
                CPTypes TypeFormat = lt.TypeFormat();
                ValidDomain valid = new ValidDomain(cpVar.VariableName, typeName, TypeFormat);
                int validId = vDomains.addValidDomain(valid);
                cpVarNameToVDomainID[cpVar.VariableName] = validId;
                
                for (int j = 0; j < lt.DomainSize; j++)
                {
                    valid.AddValidDomain(lt.GetDomainValue(j));
                }
            }
        }

        /// <summary>
        /// Sets the compile method.
        /// </summary>
        /// <param name="compileMethod">The compile method.</param>
        public void SetCompileMethod(BddCompileMethod compileMethod)
        {
            this.compileMethod = compileMethod;
        }

        /// <summary>
        /// Compiles all expressions.
        /// </summary>
        /// <param name="compileMethod">The compile method.</param>
        /// <returns>The BDD with the results.</returns>
        /// <exception cref="CLab.Exceptions.ClabException"/>
        public Bdd CompileAllExpressions(BddCompileMethod compileMethod)
        {
            if (resultBddMade)
                return resultBdd;
            try
            {
                resultBdd = space.CompileRules(compileMethod);
                resultBddMade = true;
            }
            catch (ClabInternalErrorException e)
            {
                throw new ClabException("Error during compiling all expressions.", e);
            }
            clab.SetStatusUpdateCount(2); //Max status updates for a search is two after first call.
            return resultBdd;
        }

        /// <summary>
        /// Gets the valid domains.
        /// </summary>
        /// <returns>The valid domain representation.</returns>
        /// <exception cref="CLab.Exceptions.ClabException"/>
        public ValidDomains GetValidDomains()
        {
            try
            {
                if (resultBddMade)
                {
                    for (int i = 0; i < cp.Variables.Count; i++)
                    {
                        Variable var = cp.Variables[i];
                        int vDomainIndex = (int)cpVarNameToVDomainID[var.VariableName];
                        ValidDomain vDomain = vDomains.ValidDoms[vDomainIndex];
                        vDomain.EmptyValidDomain();
                        validAsnData.CreateValidAssignmentData(resultBdd);
                        int ltIndex = (int)layout.TypeNameToIndex[var.TypeName];
                        BDDType lt = layout.LayoutTypes[ltIndex];

                        for (int j = 0; j < lt.DomainSize; j++)
                        {
                            int valOk = Bdd.ValExist(i, j);
                            if (valOk == 1) vDomain.AddValidDomain(lt.GetDomainValue(j));
                        }
                        validAsnData.ClabEnd();
                    }
                }
            }
            catch (Exception e)
            {
                throw new ClabException(e.Message, e);
            }
            return vDomains;
        }

        /// <summary>
        /// Updates the result BDD with a user chosen variable and domain value.
        /// Makes an expression out of the variable and value, and ands it with the
        /// old result BDD.
        /// </summary>
        /// <param name="var">The chosen variable.</param>
        /// <param name="domain">The chosen domain value.</param>
        /// <returns>The new result BDD.</returns>
        /// <exception cref="CLab.Exceptions.ClabException"/>
        public Bdd UpdateResultBDDUserChoice(String var, String domain)
        {
            if (!resultBddMade) throw new ClabException("Problem expressions has to be compiled first!");
            Expression expr;
            if (symbols.EnumerationVariables.Contains(var.ToLower()))
            {
                expr = new ExpressionBinary(new ExpressionId(var), Common.ExprType.et_eq, new ExpressionId(domain));
            }
            else if (symbols.RangeVariables.Contains(var.ToLower()) || symbols.BoolVariables.Contains(var.ToLower()))
            {
                int intDomain;
                try
                {
                    intDomain = Int32.Parse(domain);
                }
                catch (Exception e)
                {
                    throw new ClabException("Range or Bool type, but not integer domain value!", e);
                }
                expr = new ExpressionBinary(new ExpressionId(var), Common.ExprType.et_eq, new ExpressionInt(intDomain));
            }
            else throw new ClabException(String.Format("Variable {0} is not a valid variable.", var));
            try
            {
                Bdd userchoiceBdd = space.Compile(expr);
                UpdateStatus(0);
                resultBdd = Bdd.And(resultBdd, userchoiceBdd);
                UpdateStatus(1);
            }
            catch (Exception e)
            {
                throw new ClabException("Result BDD could not be updated", e);
            }
            return resultBdd;
        }

        /// <summary>
        /// Updates the result BDD with the results from an extre expression.
        /// </summary>
        /// <param name="extraExpr">The extra expression.</param>
        /// <returns>The new result BDD.</returns>
        /// <exception cref="CLab.Exceptions.ClabException"/>
        public Bdd UpdateResultBddExpr(Expression extraExpr)
        {
            try
            {
                if (!resultBddMade) throw new ClabException("Problem expressions has to be compiled first!");
                Bdd extraRule = space.Compile(extraExpr);
                UpdateStatus(0);
                resultBdd = Bdd.And(resultBdd, extraRule);
                UpdateStatus(1);
            }
            catch (Exception e) 
            {
                throw new ClabException("Result BDD could not be updated", e);
            }
            return resultBdd;
        }

        /// <summary>
        /// Updates the CLab status method.
        /// </summary>
        /// <param name="value">The value.</param>
        public void UpdateStatus(int value)
        {
            clab.UpdateStatus(value);
        }
    }
}