/*========================================================================
        Copyright (C) 2006 by Geir-Tore Lindsve, Torbjørn Meistad 
        and Yngve Raudberget, hereby refered to as "the authors".
                        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 CLab.Exceptions;

namespace CLab
{
    /// <summary>
    /// Defines common enum types and constant values used within CLab.
    /// </summary>
    public static class Common
    {
        /// <summary>
        /// Number of initial BDD nodes.
        /// </summary>
        public const int INITBDDNODES = 1000000;
        /// <summary>
        /// The initial cache used by BDD.
        /// </summary>
        public const int BDDINITDBCACHE = 100000;

        /// <summary>
        /// The max increase of BDD.
        /// </summary>
        public const int BDDMAXINCREASE = 50000;

        /// <summary>
        /// Defines enum values for expression types.
        /// </summary>
        public enum ExprType
        {
            /// <summary>
            /// Integer
            /// </summary>
            et_val,
            /// <summary>
            /// ID
            /// </summary>
            et_id,
            /// <summary>
            /// Negated expression (Neg)
            /// </summary>
            et_neg,
            /// <summary>
            /// Inverted expression (Not)
            /// </summary>
            et_not,
            /// <summary>
            /// Expression with imply operator
            /// </summary>
            et_impl,
            /// <summary>
            /// Expression with OR operator
            /// </summary>
            et_or,
            /// <summary>
            /// Expression with AND operator
            /// </summary>
            et_and,
            /// <summary>
            /// Expression with Less than or equal operator
            /// </summary>
            et_lte,
            /// <summary>
            /// Expression with Greater than or equal operator
            /// </summary>
            et_gte,
            /// <summary>
            /// Expression with Less than operator
            /// </summary>
            et_lt,
            /// <summary>
            /// Expression with Greater than operator
            /// </summary>
            et_gt,
            /// <summary>
            /// Expression with Not equal operator
            /// </summary>
            et_ne,
            /// <summary>
            /// Expression with Equal operator
            /// </summary>
            et_eq,
            /// <summary>
            /// Expression with substract operator
            /// </summary>
            et_minus,
            /// <summary>
            /// Expression with add operator
            /// </summary>
            et_plus,
            /// <summary>
            /// Expression with modulo operator
            /// </summary>
            et_mod,
            /// <summary>
            /// Expression with division operator
            /// </summary>
            et_div,
            /// <summary>
            /// Expression with multiply operator
            /// </summary>
            et_times
        };
    }
    
    /// <summary>
    /// The different BDD compile types.
    /// </summary>
    public enum BddCompileMethod {
        /// <summary>
        /// Static compilation.
        /// </summary>
        cm_static,
        /// <summary>
        /// Dynamic compilation.
        /// </summary>
        cm_dynamic,
        /// <summary>
        /// Compile with ascending BDD sizes.
        /// </summary>
        cm_ascending
    };

    /// <summary>
    /// The different csp variable orderings.
    /// </summary>
    public enum CspVariableOrdering
    {
        /// <summary>
        /// Static variable ordering.
        /// </summary>
        vo_static,
        /// <summary>
        /// Minimum width variable ordering.
        /// </summary>
        vo_minwidth
    };

    /// <summary>
    /// The different CP types.
    /// </summary>
    public enum CPTypes
    {
        /// <summary>
        /// Bool type.
        /// </summary>
        bool_type,
        /// <summary>
        /// Enum type.
        /// </summary>
        enum_type,
        /// <summary>
        /// Range type.
        /// </summary>
        range_type
    };

    /// <summary>
    /// The different moduses CLab can run under.
    /// </summary>
    public enum CLabModus
    {
        /// <summary>
        /// BDD modus.
        /// </summary>
        bdd_modus,
        /// <summary>
        /// CSP modus.
        /// </summary>
        csp_modus
    };
}