using System;
using System.Collections.Generic;
using System.Text;
using System.Collections;
using System.Web;
using CLab.Exceptions;
using CLab.Auxiliary;
using BenTools.Data;
using Iesi.Collections;
using buddy_sharp;

namespace CLab
{
    public class Space
    {
        private Bdd BddFalse;
        private Bdd BddTrue;
        private Layout layout;
        private Bdd validDom;
        private CP cp;
        private Symbols symbols;
        public int recCount = 0;
        String unsatisfiableRule = "";


        public Space(CP cp, Layout layout)
        {
            this.BddTrue = Bdd.True();
            this.BddFalse = Bdd.False();
            this.layout = layout;
            this.validDom = this.BddTrue;
            this.cp = cp;
            this.symbols = new Symbols(this.cp);

            for (int i = 0; i < this.layout.LayoutVariables.Count; i++)
            {
                if (string.Compare(this.layout.LayoutTypes[this.layout.LayoutVariables[i].TypeIndex].TypeName, "bool", true) != 0)
                {
                    List<Bdd> var = MkVar(this.layout.LayoutVariables[i].BddVar);
                    List<Bdd> domSize = MkVal(this.layout.LayoutTypes[this.layout.LayoutVariables[i].TypeIndex].DomainSize);
                    validDom &= LessThan(var, domSize);
                }
            }
        }

        public String UnsatisfiableRule
        {
            get { return UnsatisfiableRule; }
        }

        public List<Bdd> MkVar(List<int> Bddvar)
        {
            List<Bdd> var = new List<Bdd>();
            for (int i = 0; i < Bddvar.Count; i++)
            {
                var.Add(Bdd.IthVar(Bddvar[i]));
            }
            var.Add(BddFalse);
            return var;
        }

        public List<Bdd> MkVal(int intVal)
        {
            List<Bdd> res = new List<Bdd>();
            int remainder = Math.Abs(intVal);
            do
            {
                if ((remainder % 2) != 0)
                    res.Add(BddTrue);
                else
                    res.Add(BddFalse);
                remainder /= 2;
            } while (remainder != 0);

            res.Add(BddFalse);

            if (intVal < 0)
                return Neg(res);
            else
                return res;
        }

        public List<Bdd> Neg(List<Bdd> x)
        {
            List<Bdd> r = new List<Bdd>();
            for (int i = 0; i < x.Count; i++)
                r.Add(!x[i]);
            return Add(r, MkVal(1));
        }

        public Bdd Integer2Bool(List<Bdd> x) //denne kan vel fjernes, slik at vi kaller Equal direkte
        {
            return !Equal(x, MkVal(0));
        }

        public List<Bdd> Bool2Integer(Bdd x)
        {
            List<Bdd> res = new List<Bdd>();
            res.Add(x);
            res.Add(BddFalse);
            return res;
        }

        public List<Bdd> ShiftLeft(List<Bdd> x, int shiftAmount)
        {
            List<Bdd> res = new List<Bdd>();
            for (int i = 0; i < shiftAmount; i++)
                res.Add(BddFalse);
            for (int i = 0; i < x.Count; i++)
                res.Insert(i + shiftAmount, x[i]);
            return res;
        }

        public Bdd LessThan(List<Bdd> x, List<Bdd> y)
        {
            MkSameSize(x, y);
            Bdd res = x[0] &= !y[0];
            for (int i = 0; i < x.Count - 1; i++)
            {
                res = Bdd.Ite(!y[i] & x[i], BddFalse, res);
                res = Bdd.Ite(y[i] & !x[i], BddTrue, res);
            }
            res = Bdd.Ite(!x[x.Count - 1] & y[x.Count - 1], BddFalse, res);
            res = Bdd.Ite(x[x.Count - 1] & !y[x.Count - 1], BddFalse, res);
            return res;
        }

        public Bdd Equal(List<Bdd> x, List<Bdd> y)
        {
            MkSameSize(x, y);
            Bdd res = BddTrue;
            for (int i = 0; i < x.Count; i++)
            {
                res &= Bdd.BiImp(x[i], y[i]);
            }
            return res;
        }

        public List<Bdd> Abs(List<Bdd> x) //old abs-method
        {
            Bdd xPos = LessThan(MkVal(0), x);
            List<Bdd> negX = Neg(x);
            MkSameSize(x, negX);
            List<Bdd> res = new List<Bdd>();
            for (int i = 0; i < x.Count; i++)
                res.Add(Bdd.Ite(xPos, x[i], negX[i]));
            Truncate(res);
            return res;
        }

        public List<Bdd> Add(List<Bdd> x, List<Bdd> y)
        {
            MkSameSize(x, y);
            Bdd sameSign = Bdd.BiImp(x[x.Count - 1], y[x.Count - 1]);
            List<Bdd> z = new List<Bdd>();
            Bdd c = BddFalse;
            for (int i = 0; i < x.Count; i++)
            {
                z.Add(x[i] ^ y[i] ^ c);
                c = (x[i] & y[i]) | ((x[i] ^ y[i]) & c);
            }
            z.Add(Bdd.Ite(sameSign, c, z[x.Count - 1]));
            Truncate(z);
            return z;
        }

        public List<Bdd> Mul(List<Bdd> x, List<Bdd> y)
        {
            // 1)
            Bdd xPos = LessThan(MkVal(0), x);
            Bdd yPos = LessThan(MkVal(0), y);

            // 2)
            List<Bdd> xa = Abs(x);
            List<Bdd> ya = Abs(y);

            // 3)
            List<List<Bdd>> sl = new List<List<Bdd>>();
            for (int i = 0; i < xa.Count; i++)
                sl.Add(ShiftLeft(ya, i));

            // 4)
            List<Bdd> sum = MkVal(0);
            for (int i = 0; i < xa.Count; i++)
            {
                List<Bdd> nextSum = new List<Bdd>();
                List<Bdd> incSum = Add(sum, sl[i]);
                MkSameSize(incSum, sum);
                for (int j = 0; j < incSum.Count; j++)
                    nextSum.Add(Bdd.Ite(xa[i], incSum[j], sum[j]));
                Truncate(nextSum);
                sum = nextSum;
            }

            // 5)
            List<Bdd> negated = Neg(sum);
            MkSameSize(sum, negated);

            List<Bdd> res = new List<Bdd>();
            Bdd resPos = Bdd.BiImp(xPos, yPos);
            for (int i = 0; i < sum.Count; i++)
                res.Add(Bdd.Ite(resPos, sum[i], negated[i]));

            Truncate(res);
            return res;
        }

        public List<Bdd> Div(List<Bdd> x, List<Bdd> y)
        {
            // 1) Check sign
            Bdd xPos = LessThan(MkVal(0), x);
            Bdd yPos = LessThan(MkVal(0), y);
            List<Bdd> xa = Abs(x);
            List<Bdd> ya = Abs(y);

            // 2) Make sl vectors
            List<List<Bdd>> sl = new List<List<Bdd>>();
            for (int i = 0; i < xa.Count; i++)
                sl.Add(ShiftLeft(ya, i));

            // 3) Compute z vector
            int xaValue = xa.Count;
            List<Bdd> z = new List<Bdd>();
            for (int i = xaValue - 1; i >= 0; i--)
            {
                List<Bdd> sub = Add(xa, Neg(sl[i]));
                Bdd subNotNeg = !LessThan(sub, MkVal(0));
                z.Insert(0, subNotNeg);
                MkSameSize(sub, xa);
                for (int j = 0; j < sub.Count; j++)
                {
                    xa[j] = Bdd.Ite(subNotNeg, sub[j], xa[j]);
                    Truncate(xa);
                }
            }

            // 4) Glue sign back
            Truncate(z);
            List<Bdd> negated = Neg(z);
            MkSameSize(z, negated);
            List<Bdd> res = new List<Bdd>();
            Bdd resPos = Bdd.BiImp(xPos, yPos);
            for (int i = 0; i < z.Count; i++)
                res.Add(Bdd.Ite(resPos, z[i], negated[i]));
            Truncate(res);
            return res;
        }

        public List<Bdd> Mod(List<Bdd> x, List<Bdd> y)
        {
            List<Bdd> absX = Abs(x);
            List<Bdd> absY = Abs(y);
            List<List<Bdd>> sl = new List<List<Bdd>>();

            //1) make sl list
            for (int i = 0; i < absX.Count; i++)
            {
                sl.Add(ShiftLeft(absY, i));
            }

            // 2) compute r list (same operations as for div, just with no z vector)
            int valueAbsX = absX.Count;
            for (int i = valueAbsX - 1; i >= 0; i--)
            {
                List<Bdd> sub = Add(absX, Neg(sl[i]));
                Bdd subNotNeg = !LessThan(sub, MkVal(0));

                MkSameSize(sub, absX);

                for (int j = 0; j < sub.Count; j++)
                {
                    absX[j] = Bdd.Ite(subNotNeg, sub[i], absX[i]);
                }
                Truncate(absX);
            }

            // 3) compute remainder if (x<0) & (r<>0)
            Bdd xNeg = LessThan(x, MkVal(0));
            Bdd rNotZero = !Equal(absX, MkVal(0));

            //adjustedRemainder
            List<Bdd> ar = Add(Neg(absX), absY);
            MkSameSize(ar, absX);
            List<Bdd> res = new List<Bdd>();
            for (int i = 0; i < ar.Count; i++)
            {
                res.Add(Bdd.Ite(xNeg & rNotZero, ar[i], absX[i]));
            }
            Truncate(res);
            return res;
        }

        public void MkSameSize(List<Bdd> x, List<Bdd> y)
        {
            if (x.Count > y.Count)
                Extend(y, x.Count - y.Count);
            else if (x.Count < y.Count)
                Extend(x, y.Count - x.Count);
            //Pair<List<Bdd>, List<Bdd>> bddPair = new Pair<List<Bdd>, List<Bdd>>(x, y);
            //return bddPair;
        }

        public void Truncate(List<Bdd> x)
        {
            while ((x.Count > 2) & (x[x.Count - 1] == x[x.Count - 2]))
                x.RemoveAt(x.Count - 1);
        }

        public void Extend(List<Bdd> x, int k)
        {
            Bdd last = x[x.Count - 1];
            for (int i = 0; i < k; i++)
                x.Add(last);
            //return x;
        }

        public Bdd CompileRules(CompileMethod method)
        {

            /* sol:
             * ArrayList of BDDs representing the configuration solution space
             * of each rule. Variable domain constraints and operator definition constraints
             * are included in these expressions
             */

            List<Bdd> sol = new List<Bdd>();

            //Compute BDD for each rule
            for (int i = 0; i < cp.Rules.Count; i++)
            {
                Bval val = Expr2BddVec(cp.Rules[i]);
                Bdd expr = Integer2Bool(val.B) & val.DefCon & validDom; //Legge sammen tre BDDer
                if (expr == BddFalse)
                {
                    unsatisfiableRule = cp.Rules[i].ToString();
                    return BddFalse;
                }
                sol.Add(expr);
            }
            Bdd res = BddTrue;
            switch (method)
            {
                case CompileMethod.cm_static:
                    for (int i = 0; i < sol.Count; i++)
                        res &= sol[i];
                    break;

                case CompileMethod.cm_dynamic:
                    {
                        IPriorityQueue pq = new BinaryPriorityQueue();
                        for (int i = 0; i < sol.Count; i++)
                        {
                            pq.Push(new PQbdd(sol[i]));
                        }
                        while (pq.Count > 1)
                        {
                            Bdd a = ((PQbdd)pq.Pop()).B;
                            Bdd b = ((PQbdd)pq.Pop()).B;
                            pq.Push(a & b);
                        }
                        return ((PQbdd)pq.Pop()).B; // Neida, ok dette : Ehem...denne er det vel noe rart med? Må vel løses litt annerledes her, for her vil den tulle med for-løkka?
                    }
                //break;

                case CompileMethod.cm_ascending:
                    sol.Sort(new BDDComparer()); // Sort the BDDs in the solution space based on their nodecounts (MÅ LAGE EN COMPARABLE-IMPLEMENTASJON FOR BDDer OM IKKE BUDDY HAR DET)
                    for (int i = 0; i < sol.Count; i++)
                    {
                        res &= sol[i];

                    }
                    break;

                default:
                    throw new ClabInternalErrorException("Space.cs: Unknown CompileMethod error");
            }
            return res;
        }

        public Bdd Compile(Expression expression)
        {
            symbols.TypeCheck(expression);
            Bval val = Expr2BddVec(expression);
            return Integer2Bool(val.B) & val.DefCon & validDom;
        }

        Bval Expr2BddVec(Expression expression)
        {
            LayoutVariable layoutVariable;
            LayoutType ltype;
            List<Bdd> bddVariables;
            Bdd res;
            Bdd defCon;
            Bval left;
            Bval right;
            Bval bval;
            switch (expression.Type)
            {
                case Common.ExprType.et_val:
                    IntExpression intExpression = (IntExpression)expression;
                    return new Bval(MkVal(intExpression.IntegerValue), BddTrue);
                case Common.ExprType.et_id:
                    //Enumeration variables and enumeration constants are caught in the eq, ne, in and notin expressions.
                    //Thus, we can assume ids to be range or bool variable
                    IdExpression idExpression = (IdExpression)expression;                  
                    layoutVariable = layout.LayoutVariables[(int)layout.VariableNameToIndex[idExpression.Id]];
                    ltype = layout.LayoutTypes[layoutVariable.TypeIndex];
                    if(ltype.GetType() == typeof(CLab.LayoutTypeBool))
                        return new Bval(MkVar(layoutVariable.BddVar), BddTrue);
                    else if(ltype.GetType() == typeof(CLab.LayoutTypeRange))
                    {
                        LayoutTypeRange layoutTypeRange = (LayoutTypeRange)ltype;
                        bddVariables = MkVar(layoutVariable.BddVar);
                        List<Bdd> start = MkVal(layoutTypeRange.StartOfRange);
                        return new Bval(Add(bddVariables, start), BddTrue);
                    }
                    else throw new ClabInternalErrorException(String.Format("Space - Expr2BddVec - case ExprType.et_id, unhandled case '{1}'", ltype.GetType().ToString()));
                case Common.ExprType.et_ne:
                case Common.ExprType.et_eq:
                    Boolean enumExpression = false;
                    String var = "";
                    String constant = "";
                    BinaryExpression binExpression = (BinaryExpression)expression;
                    if (binExpression.Left.Type.Equals(Common.ExprType.et_id))
                    {
                        IdExpression leftIdExpression = (IdExpression)binExpression.Left;
                        IdExpression rightIdExpression = (IdExpression)binExpression.Right;
                        enumExpression = true;
                        
                        if (symbols.EnumerationVariables.Contains(leftIdExpression.Id.ToLower()))
                        {                            
                            var = leftIdExpression.Id;
                            constant = rightIdExpression.Id;
                        }                    
                        else
                    
                        {
                            var = rightIdExpression.Id;
                            constant = leftIdExpression.Id;
                        }
                    }
                    if (enumExpression)
                    {
                        layoutVariable = layout.LayoutVariables[(int)layout.VariableNameToIndex[var]];
                        LayoutTypeEnumeration layoutTypeEnum = (LayoutTypeEnumeration)layout.LayoutTypes[layoutVariable.TypeIndex];
                        bddVariables = MkVar(layoutVariable.BddVar);
                        res = Equal(bddVariables, MkVal((int) layoutTypeEnum.ValueToIndex[constant]));
                        if (binExpression.Type.Equals(Common.ExprType.et_eq))
                        {
                            return new Bval(Bool2Integer(res), BddTrue);
                        }
                        else
                        {
                            return new Bval(Bool2Integer(!res), BddTrue);
                        }
                    }
                    else
                    {
                        left = Expr2BddVec(binExpression.Left);
                        right = Expr2BddVec(binExpression.Right);
                        res = Equal(left.B, right.B);
                        if (binExpression.Type.Equals(Common.ExprType.et_eq))
                        {
                            return new Bval(Bool2Integer(res), left.DefCon & right.DefCon);
                        }
                        else
                        {
                            return new Bval(Bool2Integer(!res), left.DefCon & right.DefCon);
                        }
                    }
                case Common.ExprType.et_impl:
                case Common.ExprType.et_or:
                case Common.ExprType.et_and:
                    {
                        binExpression = (BinaryExpression)expression;
                        left = Expr2BddVec(binExpression.Left);
                        right = Expr2BddVec(binExpression.Right);
                        Bdd l = Integer2Bool(left.B);
                        Bdd r = Integer2Bool(right.B);
                        defCon = left.DefCon & right.DefCon;
                        
                        /* denne gav feilmelding(deklarasjon av ExprType..., rettet den opp til den under: av yngve 13.04.06*/
                        //ExprType temType = binExpression.Type;
                        //rettet opp til denne... vet ikke hva som er riktig her...?  av yngve 13.04.06
                        Common.ExprType temType = binExpression.Type;
                        Console.Out.WriteLine("type: " + binExpression.Type.ToString());
                        switch (binExpression.Type)
                        {
                            case Common.ExprType.et_impl:
                                return new Bval(Bool2Integer(Bdd.Imp(l, r)), defCon);
                                // den over er egentlig denne:
                                // temp = new Bval(Bool2Integer(l >> r), defCon);
                                // men vi får ikke overloaded >> til impl da det egentlig er 
                                // en shiftright-operator og argumentlisten vil ikke stemme.
                            case Common.ExprType.et_or:
                                return new Bval(Bool2Integer(l | r), defCon);
                            case Common.ExprType.et_and:
                                return new Bval(Bool2Integer(l & r), defCon);
                            default:
                                break;
                        }
                        break;
                    }
                case Common.ExprType.et_lte:
                case Common.ExprType.et_gte:
                case Common.ExprType.et_lt:
                case Common.ExprType.et_gt:
                    {
                        binExpression = (BinaryExpression)expression;                       
                        left = Expr2BddVec(binExpression.Left);
                        right = Expr2BddVec(binExpression.Right);
                        defCon = left.DefCon & right.DefCon;
                        switch (binExpression.Type)
                        {
                            case Common.ExprType.et_lte:
                                return new Bval(Bool2Integer(!LessThan(right.B, left.B)), defCon);
                            case Common.ExprType.et_gte:
                                return new Bval(Bool2Integer(!LessThan(left.B, right.B)), defCon);
                            case Common.ExprType.et_lt:
                                return new Bval(Bool2Integer(LessThan(left.B, right.B)), defCon);
                            case Common.ExprType.et_gt:
                                return new Bval(Bool2Integer(LessThan(right.B, left.B)), defCon);
                            default:
                                break;
                        }
                        break;
                    }
                case Common.ExprType.et_minus:
                case Common.ExprType.et_plus:
                case Common.ExprType.et_times:
                    binExpression = (BinaryExpression)expression;
                    left = Expr2BddVec(binExpression.Left);
                    right = Expr2BddVec(binExpression.Right);
                    defCon = left.DefCon & right.DefCon;
                    switch (binExpression.Type)
                    {
                        case (Common.ExprType.et_minus):
                            List<Bdd> negated = Neg(right.B);
                            Truncate(negated);
                            return new Bval(Add(left.B, negated), defCon);
                        case (Common.ExprType.et_plus):
                            return new Bval(Add(left.B, right.B), defCon);
                        case (Common.ExprType.et_times):
                            return new Bval(Mul(left.B, right.B), defCon);
                        default:
                            break;
                        //Exception??
                    }
                    break;
                case Common.ExprType.et_mod:
                case Common.ExprType.et_div:
                    binExpression = (BinaryExpression)expression;
                    left = Expr2BddVec(binExpression.Left);
                    right = Expr2BddVec(binExpression.Right);
                    List<Bdd> zero = MkVal(0);
                    Bdd rightNotZero = !Equal(right.B, zero);
                    defCon = left.DefCon & right.DefCon & rightNotZero;
                    switch (binExpression.Type)
                    {
                        case (Common.ExprType.et_mod):
                            return new Bval(Mod(left.B, right.B), defCon);
                        case (Common.ExprType.et_div):
                            return new Bval(Div(left.B, right.B), defCon);
                    }
                    break;

                case Common.ExprType.et_not:

                    NotNegExpression nnExpression = (NotNegExpression)expression;
                    bval = Expr2BddVec(nnExpression.Left);
                    res = !Integer2Bool(bval.B);
                    return new Bval(Bool2Integer(res), bval.DefCon);
                case Common.ExprType.et_neg:

                    nnExpression = (NotNegExpression)expression;
                    bval = Expr2BddVec(nnExpression.Left);
                    return new Bval(Neg(bval.B), bval.DefCon);
                default:
                    //exception??
                    break;
            }
            return null;
        }
    }
}