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

namespace buddy_sharp
{
    // why not a struct?! 
    public class Bdd : IDisposable
    {
        // A bdd root.
        private int root;
        // Track whether Dispose has been called.
        private bool disposed = false;

        // Constructors for the Bdd object.
        public Bdd() { root = 0; }
        public Bdd(Bdd r) { bdd_addref(root = r.root);}
        private Bdd(int r) { bdd_addref(root = r); }

        // Implement IDisposable.
        // Do not make this method virtual.
        // A derived class should not be able to override this method.
        public void Dispose()
        {
            // Check to see if Dispose has already been called.
            if (!this.disposed)
            {
                bdd_delref(root);
                // Note that this is not thread safe.
                // Another thread could start disposing the object
                // after the managed resources are disposed,
                // but before the disposed flag is set to true.
                // If thread safety is necessary, it must be
                // implemented by the client.

            }
            disposed = true;
            // Take yourself off the Finalization queue 
            // to prevent finalization code for this object
            // from executing a second time.
            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 "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(void);
	public static void Done(void) {
	    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(void);
	public static bool IsRunning(void) {
	    return bdd_isrunning() == 1;
	}

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

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

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

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

        // [DllImport("buddy.dll")]
	// private static extern char* bdd_versionstr(void);
	// public static char* VersionStr(void) {
	//     return bdd_versionstr();
	// }

        [DllImport("buddy.dll")]
	private static extern int bdd_versionnum(void);	
	public static int VersionNum(void) {
	    return bdd_versionnum(void);
	}
  	
        // [DllImport("buddy.dll")]
	// private static extern void bdd_stats(bddStat* stat);	
	// public static void Stats(bddStat* stat) {	
        //     bdd_stats(bddStat* stat);
	// }

        // [DllImport("buddy.dll")]
	// private static extern void bdd_cachestats(bddCacheStat* s);
	// public static void CacheStats(bddCacheStat* s) {
        //     bdd_cachestats(bddCacheStat* s);
	// }	

        // [DllImport("buddy.dll")]
	// private static extern void bdd_fprintstat(FILE* ofile);
 	// public static void FPrintStat(FILE* ofile) {
	//     bdd_fprintstat(FILE* ofile);
	// }

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

        // [DllImport("buddy.dll")]
	// private static extern void bdd_default_gbchandler(int pre, bddGbcStat* s);
	// public static void DefaultGBCHandler(int pre, bddGbcStat* s) {
	//     bdd_default_gbchandler(int pre, bddGbcStat* s);
	// }

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

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

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

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

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

        [DllImport("buddy.dll")]
	private static extern int bdd_varnum(void);
	publick static int VarNum(void) {
	    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(int 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(void);
	public static void Gbc(void) {
	    bdd_gbc();
	}

        // [DllImport("buddy.dll")]
	// private static extern int bdd_scanset(BDD r, int** v, int* n);
	// public static int bdd_scanset(BDD r, int** v, int* n);


        // [DllImport("buddy.dll")]
	// private static extern BDD bdd_makeset(int* v, int n);
        
        // [DllImport("buddy.dll")]
	// private static extern bddPair* bdd_newpair(void);
        // [DllImport("buddy.dll")]
	// private static extern intbdd_setpair(bddPair* pair, int oldvar, int newvar);
        // [DllImport("buddy.dll")]
	// private static extern int bdd_setpairs(bddPair* pair, int* oldvar, int* newvar, int size);
        // [DllImport("buddy.dll")]
	// private static extern int bdd_setbddpair(bddPair* pair, int* oldvar, int* newvar, int size);
        // [DllImport("buddy.dll")]
	// private static extern int bdd_setbddpairs(bddPair* pair, int* oldvar, BDD* newvar, int size);
        // [DllImport("buddy.dll")]
	// private static extern void bdd_resetpair(bddPair* pair);
        // [DllImport("buddy.dll")]
	// private static extern void bdd_freepair(bddPair* 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);
	}

        // [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 Bdd(bdd_not(r.root));
	}	
	
        [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 int Constrain(Bdd f, Bdd c) {
	    return new Bdd(bdd_constrain(f.root,c.root));
	}

        // [DllImport("buddy.dll")]
	// private static extern BDD bdd_replace(BDD r, bddPair* 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 BDD bdd_veccompose(BDD f, bddPair* pair);

        [DllImport("buddy.dll")]
	private static extern int bdd_simplify(int f, int d);
	public static int 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 int Exist(Bdd r, Bdd var) {
	    return new Bdd(bdd_exist(int r, int var));
	}

        [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 int 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 int AppEx(int left, int right, int opr, int var);

        [DllImport("buddy.dll")]
	private static extern int bdd_appall(int left, int right, int opr, int var);
	public static int AppAll(Bdd left, Bdd right, int opr, Bdd var) {
	    return 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);
	publoic static int 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));
	}

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

        // [DllImport("buddy.dll")]
	// private static extern int bdd_anodecount(BDD *r, int num);
        // [DllImport("buddy.dll")]
	// private static extern int* bdd_varprofile(BDD r);
        
	[DllImport("buddy.dll")]
	private static extern double bdd_pathcount(BDD 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(void);
	public static void PrintAll(void) {
	    bdd_printall();
	}

        // [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);
	}
       
        // [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(char* fname, BDD r);
        // [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(char* fname, BDD r);
        // [DllImport("buddy.dll")]
	// private static extern int bdd_save(FILE* ofile, BDD r);
        // [DllImport("buddy.dll")]
	// private static extern int bdd_fnload(char* fname, BDD* r);
        // [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(int  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(void);
	public static int ReorderGain(void) {
	    return bdd_reorder_gain();
	}

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

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

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

        [DllImport("buddy.dll")]
	private static extern void bdd_varblockall(void);
	public static void VarBlockAll(void) {
	    bdd_varblockall();
	}
	
        // [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(void);
	public  static int GetReorderTimes(void) {
	    return bdd_getreorder_times(void);
	}

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

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

        [DllImport("buddy.dll")]
	private static extern void bdd_disable_reorder(void);
	public static void DisableReorder(void) {
	    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);

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

        // [DllImport("buddy.dll")]
	// private static extern void bdd_fprintorder(FILE* ofile);






        // ken's stuff
	// 
        // [DllImport("buddy.dll")]
        // private static extern int bdd_isrunning();
        // public static bool IsRunning()
        // {
        //     return bdd_isrunning() == 1;
        // }
	// 
        // [DllImport("buddy.dll")]
        // private static extern int bdd_low(int root);
        // public Bdd Low()
        // {
        //     if (this.disposed) throw new ObjectDisposedException("Bdd("+ root + ")");
	// 
        //     return new Bdd(bdd_low(root));
        // }
	// 
        // [DllImport("buddy.dll")]
        // private static extern int bdd_high(int root);
        // public Bdd High()
        // {
        //     if (this.disposed) throw new ObjectDisposedException("Bdd(" + root + ")");
	// 
        //     return new Bdd(bdd_high(root));
        // }
	// 
        // [DllImport("buddy.dll")]
        // private static extern int bdd_var(int root);
        // public int Var()
        // {
        //     if (this.disposed) throw new ObjectDisposedException("Bdd(" + root + ")");
	// 
        //     return bdd_var(root);
        // }
	// 
        // [DllImport("buddy.dll")]
        // private static extern int bdd_ithvar(int varnum);
        // public static Bdd IthVar(int varnum)
        // {
        //     return new Bdd(bdd_ithvar(varnum));
        // }
	// 
        // public enum ApplyOpr
        // {
        //     And = 0,
        //     Xor = 1,
        //     Or = 2,
        //     Nand = 3,
        //     Nor = 4,
        //     Imp = 5,
        //     Biimp = 6,
        //     Diff = 7,
        //     Less = 8,
        //     Invimp = 9
        // }
	// 
        // [DllImport("buddy.dll")]
        // private static extern int bdd_apply(int l, int r, int opr);
        // public static Bdd Apply(Bdd l, Bdd r, ApplyOpr opr)
        // {
        //     return new Bdd(bdd_apply(l.root, r.root, (int) opr));
        // }
	// 
        // public static Bdd operator & (Bdd l, Bdd r) {
        //     return Apply(l, r, ApplyOpr.And);
        // }
        // public static Bdd operator |(Bdd l, Bdd r)
        // {
        //     return Apply(l, r, ApplyOpr.Or);
        // }



    }
}