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

using CLab.Exceptions;
using CLab.Data;

using buddy_sharp;

using BenTools.Data;
using Iesi.Collections;

namespace CLab.BDD
{

    /// <summary>
    /// Class for making BDDs based on the types, variables and expressions
    /// of a CP problem. Uses the <see cref="T:BDDLayout"></see> mapping 
    /// of cp variables to BDD variables. 
    /// </summary>
    public class BDDSpace
    {
        private Bdd BddFalse;
        private Bdd BddTrue;
        private BDDLayout layout;
        private Bdd validDom;
        private CP cp;
        private Symbols symbols;
        private ClabBDD clabBdd;
        String unsatisfiableRule = "";

        /// <summary>
        /// Initializes a new instance of the <see cref="T:BDDSpace"/> class.
        /// </summary>
        /// <param name="cp">The CP problem.</param>
        /// <param name="layout">The <see cref="T:BDDLayout"></see> BDD layout representation of the problem.</param>
        /// <param name="symbols">The <see cref="T:CLab.Data.Symbols"></see>.</param>
        /// <param name="clabBdd">The </param>
        public BDDSpace(CP cp, BDDLayout layout, Symbols symbols, ClabBDD clabBdd)
        {
            this.clabBdd = clabBdd;
            this.BddTrue = Bdd.True();
            this.BddFalse = Bdd.False();
            this.layout = layout;
            this.validDom = this.BddTrue;
            this.cp = cp;
            this.symbols = symbols;

            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);
                }
            }
        }

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

        /// <summary>
        /// Gets the BDD representation of the CSP problem before the expressions is compiled in.
        /// </summary>
        public Bdd LayoutBdd
        {
            get { return validDom; }
        }

        /// <summary>
        /// Makes a 2-complementary BDD representation of the boolan vector representing the bdd variable.
        /// </summary>
        /// <param name="Bddvar">The boolean vector representing the bdd variable.</param>
        /// <returns>The 2-complementary BDD representation.</returns>
        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;
        }

        /// <summary>
        /// Makes a 2-complementary BDD representation of an integer value.
        /// </summary>
        /// <param name="intVal">The integer value.</param>
        /// <returns>The 2-complementary BDD representation.</returns>
        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;
        }

        /// <summary>
        /// Negates the specified 2-complentary BDD representation "x".
        /// </summary>
        /// <param name="x">2-complementary BDD representation to be negated</param>
        /// <returns>2-complementary BDD representation</returns>
        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));
        }

        /// <summary>
        /// Converts the specified 2-complementary BDD represantation
        /// "x" to a BDD.
        /// </summary>
        /// <param name="x">The 2-complementary representation.</param>
        /// <returns>The BDD representation.</returns>
        public Bdd Integer2Bool(List<Bdd> x) 
        {
            return !Equal(x, MkVal(0));
        }

        /// <summary>
        /// Converts the specified BDD "x" to a 2-complementary BDD representation.
        /// </summary>
        /// <param name="x">The BDD.</param>
        /// <returns>The 2-complementary representation.</returns>
        public List<Bdd> Bool2Integer(Bdd x)
        {
            List<Bdd> res = new List<Bdd>();
            res.Add(x);
            res.Add(BddFalse);
            return res;
        }

        /// <summary>
        /// Shifts each bit "shiftAmount" positions to the left.
        /// </summary>
        /// <param name="x">The 2-complementary representation of a BDD.</param>
        /// <param name="shiftAmount">Number of positions "x" should be shifted left.</param>
        /// <returns>A 2-complementary BDD representation.</returns>
        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.Add(x[i]);
            return res;
        }

        /// <summary>
        /// Calculates a BDD representing the less-than operation
        /// on two 2-complementary BDD representations.
        /// </summary>
        /// <param name="x">The left 2-complementary BDD representation.</param>
        /// <param name="y">The right 2-complementary BDD representation.</param>
        /// <returns>A BDD representing the result.</returns>
        public Bdd LessThan(List<Bdd> x, List<Bdd> y)
        {
            MkSameSize(x, y);
            Bdd res = y[0] & !x[0];
            for (int i = 1; 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], BddTrue, res);
            return res;
        }

        /// <summary>
        /// Calculates a BDD representing the equal operation on two
        /// 2-complementary BDD representations.
        /// </summary>
        /// <param name="x">The left 2-complementary BDD representation.</param>
        /// <param name="y">The right 2-complementary BDD representation.</param>
        /// <returns>BDD representing the result.</returns>
        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;
        }

        /// <summary>
        /// Calculates the absolute value of a 2-complementary BDD representation.
        /// </summary>
        /// <param name="x">The 2-complementary BDD representation.</param>
        /// <returns>A 2-complementary BDD representation, representing the result.</returns>
        public List<Bdd> Abs(List<Bdd> x) 
        {
            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;
        }

        /// <summary>
        /// Calculates the result of the Add operation between two 2-complementary BDD representations.
        /// </summary>
        /// <param name="x">A 2-complementary BDD representation.</param>
        /// <param name="y">Another 2-complementary BDD representatino.</param>
        /// <returns>A 2-complementary BDD representation, representing the result.</returns>
        public List<Bdd> Add(List<Bdd> x, List<Bdd> y)
        {
            MkSameSize(x, y);
            Bdd sameSign = Bdd.BiImp(x[x.Count - 1], y[y.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;
        }

        /// <summary>
        /// Calculates the result of the multiplication operation between two 2-complementary BDD representations.
        /// </summary>
        /// <param name="x">A 2-complementary BDD representation.</param>
        /// <param name="y">Another 2-complementary BDD representation.</param>
        /// <returns>A 2-complementary BDD representation, representing the result.</returns>
        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;
        }

        /// <summary>
        /// Calculates the result of the division operation between two 2-complementary BDD representations.
        /// </summary>
        /// <param name="x">2-complementary BDD representation of the numerator.</param>
        /// <param name="y">2-complementary BDD representation of the denominator.</param>
        /// <returns>A 2-complementary BDD representation, representing the result.</returns>
        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>(xa.Count);
            
            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;
        }

        /// <summary>
        /// Calculates the result of the modulo operation between two 2-complementary BDD representations.
        /// </summary>
        /// <param name="x">2-complementary BDD representation of the numerator.</param>
        /// <param name="y">2-complementary BDD representation of the denominator.</param>
        /// <returns>A 2-complementary BDD representation, representing the result.</returns>
        public List<Bdd> Mod(List<Bdd> x, List<Bdd> y)
        {
            List<Bdd> absX = Abs(x);
            List<Bdd> absY = Abs(y);
          

            //1) make sl list
            List<List<Bdd>> sl = new List<List<Bdd>>();
            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[j], absX[j]);
                }
                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;
        }

        /// <summary>
        /// Extends the smallest of the specified "x" or "y", so the lists gets equal length.
        /// Modifies one of them, if they have unequal lenght.
        /// </summary>
        /// <param name="x">2-complementary representation.</param>
        /// <param name="y">2-complementary representation.</param>
        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);
        }

        /// <summary>
        /// Truncates the specified x.
        /// </summary>
        /// <param name="x">The x.</param>
        public void Truncate(List<Bdd> x)
        {
            while ((x.Count > 2) & (x[x.Count - 1] == x[x.Count - 2]))
                x.RemoveAt(x.Count - 1);
        }

        /// <summary>
        /// Extends the specified "x" with "k" elements.
        /// </summary>
        /// <param name="x">The 2-complementary BDD representation to be extended.</param>
        /// <param name="k">Number of elements to extend with.</param>
        public void Extend(List<Bdd> x, int k)
        {
            Bdd last = x[x.Count - 1];
            for (int i = 0; i < k; i++)
                x.Add(last);
        }

        /// <summary>
        /// Tries to compile all rules defined in the problem file. Each expression is compiled to a BDD.
        /// Afterwards the BDDs are and'ed together, depending on which ordering is chosen.
        /// 
        /// The order of the compilation can be set three different ways:
        /// Static: In the same order the expressions are written in the problem.
        /// Ascending: The order depends on the node count of each expression. Smallest node count is and'ed 
        /// with the result BDD first.
        /// Dynamic: The two smallest BDDs are and'ed, and the result is placed back in the queue. This is continued until
        /// we have only one element left in the queue, which is the final result BDD.
        /// 
        /// </summary>
        /// <param name="method">The <see cref="F:CLab.Auxiliary.Common.CompileMethod"/> representing which ordering to use.</param>
        /// <returns>Result <see cref="T:buddy_sharp.Bdd"/> of the expressions.</returns>
        /// <exception cref="T:CLab.Exceptions.ClabInternalErrorException">When using an unknown <see cref="F:CLab.Auxiliary.Common.CompileMethod"/></exception>
        public Bdd CompileRules(BddCompileMethod method)
        {
            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.BDDList) & val.DefCon & validDom;
                if (expr == BddFalse)
                {
                    unsatisfiableRule = cp.Rules[i].ToString();
                    return BddFalse;
                }
                sol.Add(expr);

                clabBdd.UpdateStatus(i);
            }
            Bdd res = BddTrue;

            switch (method)
            {
                case BddCompileMethod.cm_static:
                    for (int i = 0; i < sol.Count; i++)
                    {
                        res &= sol[i];
                        clabBdd.UpdateStatus(i);
                    }
                    return res;

                case BddCompileMethod.cm_dynamic:
                    {
                        IPriorityQueue pq = new BinaryPriorityQueue();
                        for (int i = 0; i < sol.Count; i++)
                        {
                            pq.Push(new PQbdd(sol[i]));
                        }
                        int bddNum = 0;
                        while (pq.Count > 1)
                        {
                            Bdd a = ((PQbdd)pq.Pop()).BDD;
                            Bdd b = ((PQbdd)pq.Pop()).BDD;
                            Bdd newBdd = a & b;
                            pq.Push(new PQbdd(newBdd));
                            clabBdd.UpdateStatus(bddNum);
                            bddNum++;

                        }
                        clabBdd.UpdateStatus(bddNum);
                        return ((PQbdd)pq.Pop()).BDD;
                    }

                case BddCompileMethod.cm_ascending:
                    sol.Sort(new BDDComparer());
                    for (int i = 0; i < sol.Count; i++)
                    {
                        res &= sol[i];
                        clabBdd.UpdateStatus(i);
                    }
                    return res;

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

        /// <summary>
        /// Compiles the specified expression.
        /// </summary>
        /// <param name="expression">The expression.</param>
        /// <returns>Resulting <see cref="T:buddy_sharp.Bdd"/> of the expression.</returns>
        /// <exception cref="CLab.Exceptions.ClabException"></exception>
        public Bdd Compile(Expression expression)
        {
            try
            {
                symbols.CheckExpressionType(expression);
                Bval val = Expr2BddVec(expression);
                return Integer2Bool(val.BDDList) & val.DefCon & validDom;
            }
            catch (ClabSymbolException e) 
            {
                throw new ClabException("Expression could not be compiled.", e);
            }
        }

        /// <summary>
        /// Compiles a expression into a <see cref="T:Bval"></see> object.
        /// </summary>
        /// <param name="expression">The expression to be compiled.</param>
        /// <returns>Bval which represent valid solutions of the expression.</returns>
        /// <exception cref="ClabInternalErrorException"/>
        public Bval Expr2BddVec(Expression expression)
        {
            BDDVariable layoutVariable;
            BDDType ltype;
            List<Bdd> bddVariables;
            Bdd res;
            Bdd defCon;
            Bval left;
            Bval right;
            Bval bval;
            switch (expression.Type)
            {
                case Common.ExprType.et_val:
                    ExpressionInt intExpression = (ExpressionInt)expression;
                    return new Bval(MkVal(intExpression.IntegerValue), BddTrue);
                
                case Common.ExprType.et_id:
                    //Enumeration variables and enumeration constants are caught in the eq and ne expression types.
                    //Thus, we can assume ids to be range or bool variable
                    ExpressionId idExpression = (ExpressionId)expression;                  
                    layoutVariable = layout.LayoutVariables[(int)layout.VariableNameToIndex[idExpression.Id]];
                    ltype = layout.LayoutTypes[layoutVariable.TypeIndex];
                    if(ltype.GetType() == typeof(CLab.BDD.BDDTypeBool))
                        return new Bval(MkVar(layoutVariable.BddVar), BddTrue);
                    else if(ltype.GetType() == typeof(CLab.BDD.BDDTypeRange))
                    {
                        BDDTypeRange layoutTypeRange = (BDDTypeRange)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 = "";
                    ExpressionBinary binExpression = (ExpressionBinary)expression;
                    
                    if (binExpression.Left.Type.Equals(Common.ExprType.et_id))
                    {
                        ExpressionId leftIdExpression = (ExpressionId)binExpression.Left;
                        
                        if (symbols.EnumerationVariables.Contains(leftIdExpression.Id.ToLower()))
                        {                            
                            var = leftIdExpression.Id;
                            ExpressionId rightIdExpression = (ExpressionId)binExpression.Right;
                            constant = rightIdExpression.Id;
                            enumExpression = true;
                        }                    
                    }
                    if (!enumExpression && binExpression.Right.Type.Equals(Common.ExprType.et_id))
                    {
                        ExpressionId rightIdExpression = (ExpressionId)binExpression.Right;
                        
                        if (symbols.EnumerationVariables.Contains(rightIdExpression.Id.ToLower()))
                        {
                            var = rightIdExpression.Id;
                            ExpressionId leftIdExpression = (ExpressionId)binExpression.Left;
                            constant = leftIdExpression.Id;
                            enumExpression = true;
                        }
                    }
                    if (enumExpression)
                    {
                        layoutVariable = layout.LayoutVariables[(int)layout.VariableNameToIndex[var]];
                        BDDTypeEnum layoutTypeEnum = (BDDTypeEnum)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.BDDList, right.BDDList);
                        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 = (ExpressionBinary)expression;
                        left = Expr2BddVec(binExpression.Left);
                        right = Expr2BddVec(binExpression.Right);
                        Bdd l = Integer2Bool(left.BDDList);
                        Bdd r = Integer2Bool(right.BDDList);
                        defCon = left.DefCon & right.DefCon;
                        switch (binExpression.Type)
                        {
                            case Common.ExprType.et_impl:
                                return new Bval(Bool2Integer(Bdd.Imp(l, r)), defCon);
                            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 = (ExpressionBinary)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.BDDList, left.BDDList)), defCon);
                            case Common.ExprType.et_gte:
                                return new Bval(Bool2Integer(!LessThan(left.BDDList, right.BDDList)), defCon);
                            case Common.ExprType.et_lt:
                                return new Bval(Bool2Integer(LessThan(left.BDDList, right.BDDList)), defCon);
                            case Common.ExprType.et_gt:
                                return new Bval(Bool2Integer(LessThan(right.BDDList, left.BDDList)), defCon);
                            default:
                                break;
                        }
                        break;
                    }
                case Common.ExprType.et_minus:
                case Common.ExprType.et_plus:
                case Common.ExprType.et_times:
                    binExpression = (ExpressionBinary)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.BDDList);
                            Truncate(negated);
                            return new Bval(Add(left.BDDList, negated), defCon);
                        case (Common.ExprType.et_plus):
                            return new Bval(Add(left.BDDList, right.BDDList), defCon);
                        case (Common.ExprType.et_times):
                            return new Bval(Mul(left.BDDList, right.BDDList), defCon);
                        default:
                            break;
                        //Exception??
                    }
                    break;
                case Common.ExprType.et_mod:
                case Common.ExprType.et_div:
                    binExpression = (ExpressionBinary)expression;
                    left = Expr2BddVec(binExpression.Left);
                    right = Expr2BddVec(binExpression.Right);
                    List<Bdd> zero = MkVal(0);
                    Bdd rightNotZero = !Equal(right.BDDList, zero);
                    defCon = left.DefCon & right.DefCon & rightNotZero;
                    switch (binExpression.Type)
                    {
                        case (Common.ExprType.et_mod):
                            return new Bval(Mod(left.BDDList, right.BDDList), defCon);
                        case (Common.ExprType.et_div):
                            return new Bval(Div(left.BDDList, right.BDDList), defCon);
                    }
                    break;

                case Common.ExprType.et_not:
                    ExpressionNotNeg nnExpression = (ExpressionNotNeg)expression;
                    bval = Expr2BddVec(nnExpression.Left);
                    res = !Integer2Bool(bval.BDDList);
                    return new Bval(Bool2Integer(res), bval.DefCon);

                case Common.ExprType.et_neg:
                    nnExpression = (ExpressionNotNeg)expression;
                    bval = Expr2BddVec(nnExpression.Left);
                    return new Bval(Neg(bval.BDDList), bval.DefCon);
                default:
                    throw new ClabInternalErrorException("Switch case not covered, Expr2BddVec");
            }
            return null;
        }
    }
}