alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[buddy] get rid of many recursive algorithms

Browse source 
This patch addresses the BuDDy part of #396,
reported by Florian Renkin and Reed Oei.

* src/kernel.c, src/kernel.h: Declare a bddrecstack and
associated macros.  Resize it when new variable are declared.
* src/cache.h: Add a BddCache_index macro.
* src/bddop.c (not_rec, apply_rec, quant_rec, appquant_rec,
support_rec, ite_rec, compose_rec, restrict_rec, satone_rec,
satoneset_rec): Rewrite using this stack to get rid of the recursion.
This commit is contained in:
Alexandre Duret-Lutz 2020-06-08 22:19:17 +02:00
parent d7b3d05e57
commit 6f76121b89
4 changed files with 856 additions and 520 deletions
Download patch file Download diff file Expand all files Collapse all files

1336
buddy/src/bddop.c
View file

File diff suppressed because it is too large Load diff

4
buddy/src/cache.h
View file

@ -1,5 +1,5 @@
/*========================================================================
Copyright (C) 1996-2002 by Jorn Lind-Nielsen
Copyright (C) 1996-2002, 2020 by Jorn Lind-Nielsen
All rights reserved
Permission is hereby granted, without written agreement and without
@ -67,7 +67,7 @@ extern int BddCache_resize(BddCache *, int);
extern void BddCache_reset(BddCache *);
#define BddCache_lookup(cache, hash) (&(cache)->table[hash & ((cache)->tablesize - 1)])
#define BddCache_index(cache, hash, index) (&(cache)->table[index = (hash & ((cache)->tablesize - 1))])
#endif /* _CACHE_H */

11
buddy/src/kernel.c
View file

@ -45,7 +45,6 @@
#include <assert.h>
#include "kernel.h"
#include "cache.h"
#include "prime.h"
/*************************************************************************
@ -103,6 +102,8 @@ jmp_buf bddexception; /* Long-jump point for interrupting calc. */
int bddresized; /* Flag indicating a resize of the nodetable */
int bddcachesize; /* Size of the operator caches */
int bddhashsize; /* Size of the BDD node hash */
int* bddrecstack; /* Internal recursion stack */
int* bddrecstacktop; /* Internal recursion stack top */
bddCacheStat bddcachestats;
@ -273,6 +274,7 @@ void bdd_done(void)
free(bddnodes);
free(bddrefstack);
free(bddrecstack);
free(bddvarset);
free(bddvar2level);
free(bddlevel2var);
@ -280,6 +282,7 @@ void bdd_done(void)
bddnodes = NULL;
bddrefstack = NULL;
bddrecstack = NULL;
bddvarset = NULL;
bdd_operator_done();
@ -374,7 +377,11 @@ int bdd_setvarnum(int num)
if (__likely(bddrefstack != NULL))
free(bddrefstack);
bddrefstack = bddrefstacktop = (int*)malloc(sizeof(int)*(num*2+4));
bddrefstack = bddrefstacktop = (int*)malloc(sizeof(int)*((num+2)*2));
if (__likely(bddrecstack != NULL))
free(bddrecstack);
bddrecstack = bddrecstacktop = (int*)malloc(sizeof(int)*((num+1)*9));
for(bdv=bddvarnum ; bddvarnum < num; bddvarnum++)
{

25
buddy/src/kernel.h
View file

@ -43,6 +43,7 @@
#include <limits.h>
#include <setjmp.h>
#include "bddx.h"
#include "cache.h"
#ifdef HAVE_CONFIG_H
# include "config.h"
#endif
@ -133,6 +134,8 @@ extern int bddreorderdisabled;
extern int bddresized;
extern int bddcachesize;
extern bddCacheStat bddcachestats;
extern int* bddrecstack;
extern int* bddrecstacktop;
/* from reorder.c */
extern int bddreordermethod;
@ -214,6 +217,28 @@ static inline int PUSHREF(int a)
#define READREF(a) *(bddrefstacktop-(a))
#define POPREF(a) bddrefstacktop -= (a)
#define PUSHREF_(a) *(localbddrefstacktop++) = (a)
#define READREF_(a) *(localbddrefstacktop-(a))
#define POPREF_(a) localbddrefstacktop -= (a)
#define PUSHINT_(a) *(localbddrecstacktop++) = (a)
#define PUSH2INT_(a, b) {PUSHINT_(a); PUSHINT_(b);}
#define PUSH3INT_(a, b, c) {PUSHINT_(a); PUSHINT_(b); PUSHINT_(c);}
#define PUSH4INT_(a, b, c, d) {PUSHINT_(a); PUSHINT_(b); PUSHINT_(c); PUSHINT_(d);}
#define POPINT_() *(--localbddrecstacktop)
#define LOCAL_REC_STACKS \
int* restrict localbddrefstacktop = bddrefstacktop; \
int* restrict localbddrecstacktop = bddrecstacktop; \
int* localbddrecstackbot = bddrecstacktop;
#define NONEMPTY_REC_STACK (localbddrecstacktop > localbddrecstackbot)
#define SYNC_REC_STACKS \
bddrefstacktop = localbddrefstacktop; \
bddrecstacktop = localbddrecstacktop;
#define BDDONE 1
#define BDDZERO 0