/*========================================================================
        Copyright (C) 2004 by Rune M. Jensen and Ken Friis Larsen
                            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 RUNE M. JENSEN OR KEN FRIIS LARSEN, 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.

    RUNE M. JENSEN AND KEN FRIIS LARSEN 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.
========================================================================*/

//////////////////////////////////////////////////////////////////////////
// File  : clab.cc
// Desc. : CLab implementation
// Author: Rune M. Jensen, ITU
// Date  : 7/30/04
//////////////////////////////////////////////////////////////////////////

using System;
using System.Collections.Generic;
using System.Text;
using System.IO;
using System.Runtime.InteropServices;

namespace buddy_sharp
{
    public class Bdd : IDisposable
    {
        private int root;
        private bool disposed = false;

        public Bdd() { root = 0; }
        public Bdd(Bdd r) { bdd_addref(root = r.root); }
        private Bdd(int r) { bdd_addref(root = r); }
        
        public void Dispose()
        {
            if (!this.disposed)
            {
                bdd_delref(root);
            }
            disposed = true;           
            GC.SuppressFinalize(this);
        }

        ~Bdd()
        {
            Dispose();
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_addref(int root);
       
        [DllImport("buddy.dll")]
        private static extern void bdd_delref(int root);


        ///////////////////////////////////////////////////////////////////
        // In file "bdd.h" 
        ///////////////////////////////////////////////////////////////////
        
        // Defined operators for apply calls 
        const int opAnd       = 0;
        const int opXor       = 1;
        const int opOr        = 2;
        const int opNand      = 3;
        const int opNor       = 4;
        const int opImp       = 5;
        const int opBiImp     = 6;
        const int opDiff      = 7;
        const int opLess      = 8;
        const int opInvImp    = 9;

                   /* Should *not* be used in bdd_apply calls !!! */
        const int opNot       = 10;
        const int opSimplify  = 11;

        [StructLayout(LayoutKind.Sequential)]
        public class Wrap
        {
            private int root;
            public Bdd GetBdd()
            {
                return new Bdd(root);
            }
        }

        [StructLayout(LayoutKind.Sequential)]
        public class Stat
        {
            public long produced;
            public int nodeNum;
            public int maxNodeNum;
            public int freeNodes;
            public int minFreeNodes;
            public int varNum;
            public int cacheSize;
            public int gbcNum;
        }

        [StructLayout(LayoutKind.Sequential)]
        public class GbcStat
        {
            public int  nodes;
            public int  freeNodes;
            public long time;
            public long sumTime;
            public int  num;
        }

        [StructLayout(LayoutKind.Sequential)]
        public class CacheStat
        {
            public ulong uniqueAccess;
            public ulong uniqueChain;
            public ulong uniqueHit;
            public ulong uniqueMiss;
            public ulong opHit;
            public ulong opMiss;
            public ulong swapCount;
        }

        // Reordering algorithms        
        const int REORDER_NONE     = 0;
        const int REORDER_WIN2     = 1;
        const int REORDER_WIN2ITE  = 2;
        const int REORDER_SIFT     = 3;
        const int REORDER_SIFTITE  = 4;
        const int REORDER_WIN3     = 5;
        const int REORDER_WIN3ITE  = 6;
        const int REORDER_RANDOM   = 7;

        const int REORDER_FREE     = 0;
        const int REORDER_FIXED    = 1;

        // Error codes 
        const int MEMORY           = -1;  /* Out of memory */
        const int VAR              = -2;  /* Unknown variable */
        const int RANGE            = -3;  /* Variable value out of range (not in domain) */
        const int DEREF            = -4;  /* Removing external reference to unknown node */
        const int RUNNING          = -5;  /* Called bdd_init() twice whithout bdd_done() */
        const int FILE             = -6;  /* Some file operation failed */
        const int FORMAT           = -7;  /* Incorrect file format */
        const int ORDER            = -8;  /* Vars. not in order for vector based functions */
        const int BREAK            = -9;  /* User called break */
        const int VARNUM           = -10; /* Different number of vars. for vector pair */
        const int NODES            = -11; /* Tried to set max. number of nodes to be fewer */
                                          /* than there already has been allocated */
        const int OP               = -12; /* Unknown operator */
        const int VARSET           = -13; /* Illegal variable set */
        const int VARBLK           = -14; /* Bad variable block operation */
        const int DECVNUM          = -15; /* Trying to decrease the number of variables */
        const int REPLACE          = -16; /* Replacing to already existing variables */
        const int NODENUM          = -17; /* Number of nodes reached user defined maximum */
        const int ILLBDD           = -18; /* Illegal bdd argument */
        const int SIZE             = -19; /* Illegal size argument */

        const int BVEC_SIZE        = -20; /* Mismatch in bitvector size */
        const int BVEC_SHIFT       = -21; /* Illegal shift-left/right parameter */
        const int BVEC_DIVZERO     = -22; /* Division by zero */

        const int ERRNUM = 24;



        ///////////////////////////////////////////////////////////////////
        // In file "kernel.c" 
        ///////////////////////////////////////////////////////////////////


        [DllImport("buddy.dll")]
        private static extern int bdd_init(int nodesize, int cachesize);
        public static int Init(int nodeSize, int cacheSize)
        {
            return bdd_init(nodeSize, cacheSize);
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_done();
        public static void Done()
        {
            bdd_done();
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_setvarnum(int num);
        public static int SetVarNum(int num)
        {
            return bdd_setvarnum(num);
        }   

        [DllImport("buddy.dll")]
        private static extern int bdd_extvarnum(int num);
        public static int ExtVarNum(int num)
        {
            return bdd_extvarnum(num);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_isrunning();
        public static int IsRunning()
        {
            return bdd_isrunning();
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_setmaxnodenum(int size);
        public static int SetMaxNodeNum(int size)
        {
            return bdd_setmaxnodenum(size);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_setmaxincrease(int size);
        public static int SetMaxIncrease(int size)
        {
            return bdd_setmaxincrease(size);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_setminfreenodes(int n);
        public static int SetMinFreeNodes(int n)
        {
            return bdd_setminfreenodes(n);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_getnodenum();
        public static int GetNodeNum()
        {
            return bdd_getnodenum();
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_getallocnum();
        public static int GetAllocNum()
        {
            return bdd_getallocnum();
        }

         [DllImport("buddy.dll")]
         private static extern string bdd_versionstr();
         public static string VersionStr() {
             return bdd_versionstr();
         }

        [DllImport("buddy.dll")]
        private static extern int bdd_versionnum();
        public static int VersionNum()
        {
            return bdd_versionnum();
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_stats(
                [In, MarshalAs(UnmanagedType.LPStruct)] Stat stat);
        public static void Stats(Stat stat)
        {
            bdd_stats(stat);
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_cachestats(
            [In, MarshalAs(UnmanagedType.LPStruct)] CacheStat s);
        public static void CacheStats(CacheStat s)
        {
            bdd_cachestats(s);
        }

        //RMJ: Unclear how to marshall files
        //[DllImport("buddy.dll")]
        //private static extern void bdd_fprintstat(IntPtr oFile);
        //public static void fPrintStat(IntPtr oFile)
        //{
        //    bdd_fprintstat(oFile);
        //}

        [DllImport("buddy.dll")]
        private static extern void bdd_printstat();
        public static void PrintStat()
        {
            bdd_printstat();
        }

         [DllImport("buddy.dll")]
         private static extern void bdd_default_gbchandler(
             int pre, 
             [In, MarshalAs(UnmanagedType.LPStruct)] GbcStat s);
         public static void DefaultGBCHandler(int pre, GbcStat s) 
         {
             bdd_default_gbchandler(pre,s);
         }

        [DllImport("buddy.dll")]
        private static extern void bdd_default_errhandler(int e);
        public static void DefaultErrHandler(int e)
        {
            bdd_default_errhandler(e);
        }

        [DllImport("buddy.dll")]
        private static extern string bdd_errstring(int e);
        public static string ErrString(int e) 
        {
             return bdd_errstring(e);
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_clear_error();
        public static void ClearError()
        {
            bdd_clear_error();
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_true();
        public static Bdd True()
        {
            return new Bdd(bdd_true());
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_false();
        public static Bdd False()
        {
            return new Bdd(bdd_false());
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_varnum();
        public static int VarNum()
        {
            return bdd_varnum();
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_ithvar(int var);
        public static Bdd IthVar(int var)
        {
            return new Bdd(bdd_ithvar(var));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_nithvar(int var);
        public static Bdd NithVar(int var)
        {
            return new Bdd(bdd_nithvar(var));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_var(int root);
        public static int Var(Bdd root)
        {
            return bdd_var(root.root);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_low(int root);
        public static Bdd Low(Bdd root)
        {
            return new Bdd(bdd_low(root.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_high(int root);
        public static Bdd High(Bdd root)
        {
            return new Bdd(bdd_high(root.root));
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_gbc();
        public static void Gbc()
        {
            bdd_gbc();
        }

        //RMJ: We wish to avoid deallocating memory allocated by Buddy
        //[DllImport("buddy.dll")]
        //private static extern int bdd_scanset(int r, int** v, int* n);
        //public static int bdd_scanset(BDD r, int** v, int* n);

        [DllImport("buddy.dll")]
        private static extern int bdd_makeset(int[] v, int n);
        public static Bdd MakeSet(int[] v, int n)
        {
            return new Bdd(bdd_makeset(v,n));
        }

        [DllImport("buddy.dll")]
        private static extern IntPtr bdd_newpair();
        public static IntPtr newPair()
        {
            return bdd_newpair();
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_setpair(IntPtr pair, int oldvar, int newvar);
        public static int setPair(IntPtr pair, int oldVar, int newVar)
        {
            return bdd_setpair(pair,oldVar,newVar);
        }
        
        [DllImport("buddy.dll")]
        private static extern int bdd_setpairs(IntPtr pair, int[] oldvar, int[] newvar, int size);
        public static int setPairs(IntPtr pair, int[] oldVar, int[] newVar, int size)
        {
            return bdd_setpairs(pair,oldVar,newVar, size);
        }
        
        [DllImport("buddy.dll")]
        private static extern int bdd_setbddpair(IntPtr pair, int[] oldvar, int[] newvar, int size);
        public static int setBddPair(IntPtr pair, int[] oldVar, int[] newVar, int size)
        {
            return bdd_setbddpair(pair,oldVar,newVar, size);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_setbddpairs(IntPtr pair, int[] oldvar, int newvar, int size);
        public static int setBddPairs(IntPtr pair, int[] oldVar, Bdd newVar, int size)
        {
            return bdd_setbddpairs(pair, oldVar, newVar.root, size);
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_resetpair(IntPtr pair);
        public static void resetPair(IntPtr pair)
        {
            bdd_resetpair(pair);
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_freepair(IntPtr pair);
        public static void freePair(IntPtr pair)
        {
            bdd_freepair(pair);
        }


        ///////////////////////////////////////////////////////////////////
        // In bddop.c
        ///////////////////////////////////////////////////////////////////

        [DllImport("buddy.dll")]
        private static extern int bdd_setcacheratio(int r);
        public static int SetCacheRatio(int r)
        {
            return bdd_setcacheratio(r);
        }

        // RMJ: not imported for now  
        // [DllImport("buddy.dll")]
        // private static extern BDD bdd_buildcube(int value, int width, BDD* var);
        // [DllImport("buddy.dll")]
        // private static extern BDD bdd_ibuildcube(int value, int width, int* var);

        [DllImport("buddy.dll")]
        private static extern int bdd_not(int r);
        public static Bdd Not(Bdd r)
        {
            return new Bdd(bdd_not(r.root));
        }

            
        /* Clab begin */

        //Must be called once in the Clab code before use of extract values! 
        //    IN
        //        dom             : Array of dom sizes of the CSP variables
        //        cspVarNumIn     : number of CSP variables
        //    OUT
        //        valExist allocated 
        [DllImport("buddy.dll")]
        private static extern void bdd_clabBegin(
              [In, MarshalAs(UnmanagedType.LPArray)] int[] dom,
              int cspVarNumIn);
        public static void ClabBegin(int[] dom, int cspVarNumIn)
        {
            bdd_clabBegin(dom,cspVarNumIn);
        }


        //Must be called once in the Clab code after all calls to extractvalues! 
        //  IN
        //     cspVarNumIn     : number of CSP variables
        //  OUT
        //     valExist deallocated 
        [DllImport("buddy.dll")]
        private static extern void bdd_clabEnd(int cspVarNumIn);
        public static void ClabEnd(int cspVarNumIn)
        {
            bdd_clabEnd(cspVarNumIn);
        }

        
        //IN
        //  int i;
        //  int j;
        //OUT
        //   value of valExist[i][j]   
        //   valExist[i][j] = 1 if value j of CSP variable i is possible and 
        //   otherwise 0.
        [DllImport("buddy.dll")]
        private static extern int bdd_valExist(int i, int j);
        public static int ValExist(int i, int j)
        {
            return bdd_valExist(i,j);
        }

        
        //IN
        // b               : BDD of CSP configuration space
        // dom             : Array of dom sizes of the CSP variables
        // domStartIn      : domStart[i] index of the BDD variable where the encoding of 
        //                   CSP variable i starts  
        // cspVarNumIn     : number of CSP variables
        // bddVar2cspVarIn : An allocated array mapping BDD variables to the associated CSP variables
        //                   e.g. [0->0,1->0,2->0,3->1,4->1,5->2,...]  
        //OUT
        // instantiation of valExist.
        // use above function to read the values of valExist!!
        [DllImport("buddy.dll")]
        private static extern void bdd_extractvalues(
            int b, 
            [In, MarshalAs(UnmanagedType.LPArray)] int[] dom,
            [In, MarshalAs(UnmanagedType.LPArray)] int[] domStartIn,
            int cspVarNumIn,
            [In, MarshalAs(UnmanagedType.LPArray)] int[] bddVar2cspVarIn);            
        public static void ExtractValues(Bdd b, int[] dom, int[] domStartIn,
                                         int cspVarNumIn, int[] bddVar2cspVarIn)
        {
            bdd_extractvalues(b.root, dom, domStartIn, cspVarNumIn, bddVar2cspVarIn);
        }

        /* Clab end */


        [DllImport("buddy.dll")]
        private static extern int bdd_apply(int left, int right, int opr);
        public static Bdd Apply(Bdd left, Bdd right, int opr)
        {
            return new Bdd(bdd_apply(left.root, right.root, opr));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_and(int l, int r);
        public static Bdd And(Bdd l, Bdd r)
        {
            return new Bdd(bdd_and(l.root, r.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_or(int l, int r);
        public static Bdd Or(Bdd l, Bdd r)
        {
            return new Bdd(bdd_or(l.root, r.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_xor(int l, int r);
        public static Bdd Xor(Bdd l, Bdd r)
        {
            return new Bdd(bdd_xor(l.root, r.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_imp(int l, int r);
        public static Bdd Imp(Bdd l, Bdd r)
        {
            return new Bdd(bdd_imp(l.root, r.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_biimp(int l, int r);
        public static Bdd BiImp(Bdd l, Bdd r)
        {
            return new Bdd(bdd_biimp(l.root, r.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_ite(int f, int g, int h);
        public static Bdd Ite(Bdd f, Bdd g, Bdd h)
        {
            return new Bdd(bdd_ite(f.root, g.root, h.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_restrict(int r, int var);
        public static Bdd Restrict(Bdd r, Bdd var)
        {
            return new Bdd(bdd_restrict(r.root, var.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_constrain(int f, int c);
        public static Bdd Constrain(Bdd f, Bdd c)
        {
            return new Bdd(bdd_constrain(f.root, c.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_replace(int r, IntPtr pair);
        public static Bdd Replace(Bdd r, IntPtr pair)
        {
            return new Bdd(bdd_replace(r.root,pair));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_compose(int f, int g, int var);
        public static Bdd Compose(Bdd f, Bdd g, int var)
        {
            return new Bdd(bdd_compose(f.root, g.root, var));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_veccompose(int f, IntPtr pair);
        public static Bdd VecCompose(Bdd f, IntPtr pair)
        {
            return new Bdd(bdd_veccompose(f.root, pair));
        }


        [DllImport("buddy.dll")]
        private static extern int bdd_simplify(int f, int d);
        public static Bdd Simplify(Bdd f, Bdd d)
        {
            return new Bdd(bdd_simplify(f.root, d.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_exist(int r, int var);
        public static Bdd Exist(Bdd r, Bdd var)
        {
            return new Bdd(bdd_exist(r.root, var.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_forall(int r, int var);
        public static Bdd Forall(Bdd r, Bdd var)
        {
            return new Bdd(bdd_forall(r.root, var.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_unique(int r, int var);
        public static Bdd Unique(Bdd r, Bdd var)
        {
            return new Bdd(bdd_unique(r.root, var.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_appex(int left, int right, int opr, int var);
        public static Bdd AppEx(Bdd left, Bdd right, int opr, Bdd var)
        {
            return new Bdd(bdd_appex(left.root, right.root, opr, var.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_appall(int left, int right, int opr, int var);
        public static Bdd AppAll(Bdd left, Bdd right, int opr, Bdd var)
        {
            return new Bdd(bdd_appall(left.root, right.root, opr, var.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_appuni(int left, int right, int opr, int var);
        public static Bdd AppUni(Bdd left, Bdd right, int opr, Bdd var)
        {
            return new Bdd(bdd_appuni(left.root, right.root, opr, var.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_support(int r);
        public static Bdd Support(Bdd r)
        {
            return new Bdd(bdd_support(r.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_satone(int r);
        public static Bdd SatOne(Bdd r)
        {
            return new Bdd(bdd_satone(r.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_satoneset(int r, int var, int pol);
        public static Bdd SatOneSet(Bdd r, Bdd var, Bdd pol)
        {
            return new Bdd(bdd_satoneset(r.root, var.root, pol.root));
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_fullsatone(int r);
        public static Bdd FullSatOne(Bdd r)
        {
            return new Bdd(bdd_fullsatone(r.root));
        }

        // RMJ: unknown function
        // [DllImport("buddy.dll")]
        // private static extern void bdd_allsat(int r, bddallsathandler handler);
        // public static void bdd_allsat(Bdd r, bddallsathandler handler);

        [DllImport("buddy.dll")]
        private static extern double bdd_satcount(int r);
        public static double SatCount(Bdd r)
        {
            return bdd_satcount(r.root);
        }

        [DllImport("buddy.dll")]
        private static extern double bdd_satcountset(int r, int varset);
        public static double SatCountSet(Bdd r, Bdd varSet)
        {
            return bdd_satcountset(r.root, varSet.root);
        }

        [DllImport("buddy.dll")]
        private static extern double bdd_satcountln(int r);
        public static double SatCountLn(Bdd r)
        {
            return bdd_satcountln(r.root);
        }

        [DllImport("buddy.dll")]
        private static extern double bdd_satcountlnset(int r, int varset);
        public static double SatCountLnSet(Bdd r, Bdd varSet)
        {
            return bdd_satcountlnset(r.root, varSet.root);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_nodecount(int r);
        public static int NodeCount(Bdd r)
        {
            return bdd_nodecount(r.root);
        }

        // RMJ: not imported for now
        // [DllImport("buddy.dll")]
        // private static extern int bdd_anodecount(BDD *r, int num);

        //RMJ: WeakReference want to avoid user freeing
        //[DllImport("buddy.dll")]
        //private static extern int* bdd_varprofile(BDD r);

        [DllImport("buddy.dll")]
        private static extern double bdd_pathcount(int r);
        public static double PathCount(Bdd r)
        {
            return bdd_pathcount(r.root);
        }

        ///////////////////////////////////////////////////////////////////
        // In file "bddio.c" 
        ///////////////////////////////////////////////////////////////////

        [DllImport("buddy.dll")]
        private static extern void bdd_printall();
        public static void PrintAll()
        {
            bdd_printall();
        }

        // RMJ: unclear how files are handled
        // [DllImport("buddy.dll")]
        // private static extern void bdd_fprintall(FILE* ofile);
        // [DllImport("buddy.dll")]
        // private static extern void bdd_fprinttable(FILE* ofile, BDD r);

        [DllImport("buddy.dll")]
        private static extern void bdd_printtable(int r);
        public static void PrintTable(Bdd r)
        {
            bdd_printtable(r.root);
        }

        // RMJ: unclear how files are handled
        // [DllImport("buddy.dll")]
        // private static extern void bdd_fprintset(FILE* ofile ,BDD r);

        [DllImport("buddy.dll")]
        private static extern void bdd_printset(int r);
        public static void PrintSet(Bdd r)
        {
            bdd_printset(r.root);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_fnprintdot(string fname, int r);
        public static int fnPrintDot(string fname, Bdd r)
        {
            return bdd_fnprintdot(fname, r.root);
        }

        // RMJ: unclear how files are handled
        // [DllImport("buddy.dll")]
        // private static extern void bdd_fprintdot(FILE* ofile, BDD r);

        [DllImport("buddy.dll")]
        private static extern void bdd_printdot(int r);
        public static void PrintDot(Bdd r)
        {
            bdd_printdot(r.root);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_fnsave(string fname, int r);
        public static int fnSave(string fName, Bdd r)
        {
            return bdd_fnsave(fName,r.root);
        }   

        // RMJ: unclear how files are handled
        // [DllImport("buddy.dll")]
        // private static extern int bdd_save(FILE* ofile, BDD r);

        [DllImport("buddy.dll")]
        private static extern int bdd_fnload(
            string fname, 
            [In, MarshalAs(UnmanagedType.LPStruct)] Wrap w);
        public static int fnLoad(string fName, Wrap w)
        {             
            return bdd_fnload(fName,w);
        }

        // RMJ: unclear how files are handled
        // [DllImport("buddy.dll")]
        // private static extern int bdd_load(FILE *ifile, BDD* r);

        /* In file reorder.c */
        [DllImport("buddy.dll")]
        private static extern int bdd_swapvar(int v1, int v2);
        public static int SwapVar(int v1, int v2)
        {
            return bdd_swapvar(v1, v2);
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_default_reohandler(int prestate);
        public static void DefaultReoHandler(int preState)
        {
            bdd_default_reohandler(preState);
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_reorder(int method);
        public static void Reorder(int method)
        {
            bdd_reorder(method);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_reorder_gain();
        public static int ReorderGain()
        {
            return bdd_reorder_gain();
        }

        // RMJ: not implemented for now
        // [DllImport("buddy.dll")]
        // private static extern bddsizehandler bdd_reorder_probe(bddsizehandler handler);

        [DllImport("buddy.dll")]
        private static extern void bdd_clrvarblocks();
        public static void ClrVarBlocks()
        {
            bdd_clrvarblocks();
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_addvarblock(int var, int fixxed);
        public static int AddVarBlock(Bdd var, int fixxed)
        {
            return bdd_addvarblock(var.root, fixxed);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_intaddvarblock(int first, int last, int fixxed);
        public static int IntAddVarBlock(int first, int last, int fixxed)
        {
            return bdd_intaddvarblock(first, last, fixxed);
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_varblockall();
        public static void VarBlockAll()
        {
            bdd_varblockall();
        }

        // RMJ: not implemented for now
        // [DllImport("buddy.dll")]
        // private static extern bddfilehandler bdd_blockfile_hook(bddfilehandler handler);
        // public static bddfilehandler bdd_blockfile_hook(bddfilehandler handler);

        [DllImport("buddy.dll")]
        private static extern int bdd_autoreorder(int method);
        public static int AutoReorder(int method)
        {
            return bdd_autoreorder(method);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_autoreorder_times(int method, int num);
        public static int AutorReorderTimes(int method, int num)
        {
            return bdd_autoreorder_times(method, num);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_var2level(int var);
        public static int Var2Level(int var)
        {
            return bdd_var2level(var);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_level2var(int level);
        public static int Level2Var(int level)
        {
            return bdd_level2var(level);
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_getreorder_times();
        public static int GetReorderTimes()
        {
            return bdd_getreorder_times();
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_getreorder_method();
        public static int GetReorderMethod()
        {
            return bdd_getreorder_method();
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_enable_reorder();
        public static void EnableReorder()
        {
            bdd_enable_reorder();
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_disable_reorder();
        public static void DisableReorder()
        {
            bdd_disable_reorder();
        }

        [DllImport("buddy.dll")]
        private static extern int bdd_reorder_verbose(int v);
        public static int ReorderVerbose(int v)
        {
            return bdd_reorder_verbose(v);
        }
       
        [DllImport("buddy.dll")]
        private static extern void bdd_setvarorder(int[] neworder);
        public static void setVarOrder(int[] newOrder)
        {
            bdd_setvarorder(newOrder);
        }

        [DllImport("buddy.dll")]
        private static extern void bdd_printorder();
        public static void PrintOrder()
        {
            bdd_printorder();
        }

        // RMJ: file handling unclear
        // [DllImport("buddy.dll")]
        // private static extern void bdd_fprintorder(FILE* ofile);

        // Operator overloading 
        public static Bdd operator &(Bdd l, Bdd r)
        {
            return And(l,r);
        }

        public static Bdd operator |(Bdd l, Bdd r)
        {
            return Or(l,r);
        }

        public static Bdd operator !(Bdd l)
        {
            return Not(l);
        }
        public static Bdd operator ^(Bdd l, Bdd r)
        {
            return Xor(l, r);
        }

        /* public static Bdd >> (Bdd l, Bdd r)
         {
             return Imp(l, r);
         }*/


        public static bool operator !=(Bdd l, Bdd r)
        {
            return l.root != r.root;
        }

        public static bool operator ==(Bdd l, Bdd r)
        {
            return l.root == r.root;
        }

    }
}