[Javabdd-checkins] JavaBDD/buddy/src bddop.c,1.2,1.3 cache.c,1.1.1.1,1.2 cache.h,1.1.1.1,1.2

[John W. <joe...@us...>]

Update of /cvsroot/javabdd/JavaBDD/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv7752/buddy/src

Modified Files:
	bddop.c cache.c cache.h 
Log Message:
Updates to buddy to improve cache architecture.



Index: cache.c
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/cache.c,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -C2 -d -r1.1.1.1 -r1.2
*** cache.c	29 Sep 2004 09:50:25 -0000	1.1.1.1
--- cache.c	30 Sep 2004 03:21:38 -0000	1.2
***************
*** 43,47 ****
  *************************************************************************/
  
! int BddCache_init(BddCache *cache, int size)
  {
     int n;
--- 43,47 ----
  *************************************************************************/
  
! int BddCache3_init(BddCache3 *cache, int size)
  {
     int n;
***************
*** 49,53 ****
     size = bdd_prime_gte(size);
     
!    if ((cache->table=NEW(BddCacheData,size)) == NULL)
        return bdd_error(BDD_MEMORY);
     
--- 49,53 ----
     size = bdd_prime_gte(size);
     
!    if ((cache->table=NEW(BddCacheData3,size)) == NULL)
        return bdd_error(BDD_MEMORY);
     
***************
*** 59,64 ****
  }
  
  
! void BddCache_done(BddCache *cache)
  {
     free(cache->table);
--- 59,80 ----
  }
  
+ int BddCache4_init(BddCache4 *cache, int size)
+ {
+    int n;
  
!    size = bdd_prime_gte(size);
!    
!    if ((cache->table=NEW(BddCacheData4,size)) == NULL)
!       return bdd_error(BDD_MEMORY);
!    
!    for (n=0 ; n<size ; n++)
!       cache->table[n].a = -1;
!    cache->tablesize = size;
!    
!    return 0;
! }
! 
! 
! void BddCache3_done(BddCache3 *cache)
  {
     free(cache->table);
***************
*** 68,72 ****
  
  
! int BddCache_resize(BddCache *cache, int newsize)
  {
     int n;
--- 84,96 ----
  
  
! void BddCache4_done(BddCache4 *cache)
! {
!    free(cache->table);
!    cache->table = NULL;
!    cache->tablesize = 0;
! }
! 
! 
! int BddCache3_resize(BddCache3 *cache, int newsize)
  {
     int n;
***************
*** 76,80 ****
     newsize = bdd_prime_gte(newsize);
     
!    if ((cache->table=NEW(BddCacheData,newsize)) == NULL)
        return bdd_error(BDD_MEMORY);
     
--- 100,104 ----
     newsize = bdd_prime_gte(newsize);
     
!    if ((cache->table=NEW(BddCacheData3,newsize)) == NULL)
        return bdd_error(BDD_MEMORY);
     
***************
*** 86,91 ****
  }
  
  
! void BddCache_reset(BddCache *cache)
  {
     register int n;
--- 110,140 ----
  }
  
+ int BddCache4_resize(BddCache4 *cache, int newsize)
+ {
+    int n;
  
!    free(cache->table);
! 
!    newsize = bdd_prime_gte(newsize);
!    
!    if ((cache->table=NEW(BddCacheData4,newsize)) == NULL)
!       return bdd_error(BDD_MEMORY);
!    
!    for (n=0 ; n<newsize ; n++)
!       cache->table[n].a = -1;
!    cache->tablesize = newsize;
!    
!    return 0;
! }
! 
! 
! void BddCache3_reset(BddCache3 *cache)
! {
!    register int n;
!    for (n=0 ; n<cache->tablesize ; n++)
!       cache->table[n].a = -1;
! }
! 
! void BddCache4_reset(BddCache4 *cache)
  {
     register int n;

Index: bddop.c
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v
retrieving revision 1.2
retrieving revision 1.3
diff -C2 -d -r1.2 -r1.3
*** bddop.c	29 Sep 2004 10:00:50 -0000	1.2
--- bddop.c	30 Sep 2004 03:21:38 -0000	1.3
***************
*** 102,111 ****
  static int supportMax;              /* Max. used level in support calc. */
  static int* supportSet;             /* The found support set */
! static BddCache applycache;         /* Cache for apply results */
! static BddCache itecache;           /* Cache for ITE results */
! static BddCache quantcache;         /* Cache for exist/forall results */
! static BddCache appexcache;         /* Cache for appex/appall results */
! static BddCache replacecache;       /* Cache for replace results */
! static BddCache misccache;          /* Cache for other results */
  static int cacheratio;
  static BDD satPolarity;
[...1304 lines suppressed...]
  
--- 3390,3394 ----
  
     entry = BddCache_lookup(&misccache, PATHCOUHASH(r));
!    if (entry->a == r  &&  entry->b == miscid)
        return entry->r.dres;
  
***************
*** 3146,3150 ****
  
     entry->a = r;
!    entry->c = miscid;
     entry->r.dres = size;
     
--- 3396,3400 ----
  
     entry->a = r;
!    entry->b = miscid;
     entry->r.dres = size;
     

Index: cache.h
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/cache.h,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -C2 -d -r1.1.1.1 -r1.2
*** cache.h	29 Sep 2004 09:50:25 -0000	1.1.1.1
--- cache.h	30 Sep 2004 03:21:38 -0000	1.2
***************
*** 41,67 ****
  typedef struct
  {
!    union
!    {
!       double dres;
!       int res;
!    } r;
!    int a,b,c;
! } BddCacheData;
  
  
  typedef struct
  {
!    BddCacheData *table;
     int tablesize;
! } BddCache;
  
  
! extern int  BddCache_init(BddCache *, int);
! extern void BddCache_done(BddCache *);
! extern int  BddCache_resize(BddCache *, int);
! extern void BddCache_reset(BddCache *);
  
! #define BddCache_lookup(cache, hash) (&(cache)->table[hash % (cache)->tablesize])
  
  
  #endif /* _CACHE_H */
--- 41,80 ----
  typedef struct
  {
!   int a,b,res;
! } BddCacheData3;
  
+ typedef struct
+ {
+   int a,b;
+   union
+   {
+     struct { int c,res; };
+     double dres;
+   } r;
+ } BddCacheData4;
  
  typedef struct
  {
!    BddCacheData3 *table;
     int tablesize;
! } BddCache3;
  
+ typedef struct
+ {
+    BddCacheData4 *table;
+    int tablesize;
+ } BddCache4;
  
! extern int  BddCache3_init(BddCache3 *, int);
! extern void BddCache3_done(BddCache3 *);
! extern int  BddCache3_resize(BddCache3 *, int);
! extern void BddCache3_reset(BddCache3 *);
  
! extern int  BddCache4_init(BddCache4 *, int);
! extern void BddCache4_done(BddCache4 *);
! extern int  BddCache4_resize(BddCache4 *, int);
! extern void BddCache4_reset(BddCache4 *);
  
+ #define BddCache_lookup(cache, hash) (&(cache)->table[hash % (cache)->tablesize])
  
  #endif /* _CACHE_H */