Changeset 4938 for icGREP/icgrep-devel


Ignore:
Timestamp:
Feb 21, 2016, 1:07:03 PM (3 years ago)
Author:
nmedfort
Message:

Some performance improvements to BuDDy for functions called by the multiplexing pass.

Location:
icGREP/icgrep-devel/buddy-2.4/src
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • icGREP/icgrep-devel/buddy-2.4/src/bdd.h

    r4928 r4938  
    4848
    4949#define bddop_and       0
    50 #define bddop_xor       1
    51 #define bddop_or        2
     50#define bddop_or        1
     51#define bddop_xor       2
    5252#define bddop_nand      3
    5353#define bddop_nor       4
     
    7575   struct s_bddPair *next;
    7676} bddPair;
    77 
    78 
    79 /*=== Status information ===============================================*/
    80 
    81 /*
    82 NAME    {* bddStat *}
    83 SECTION {* kernel *}
    84 SHORT   {* Status information about the bdd package *}
    85 PROTO   {* typedef struct s_bddStat
    86 {
    87    long int produced;
    88    int nodenum;
    89    int maxnodenum;
    90    int freenodes;
    91    int minfreenodes;
    92    int varnum;
    93    int cachesize;
    94    int gbcnum;
    95 } bddStat;  *}
    96 DESCR   {* The fields are \\[\baselineskip] \begin{tabular}{lp{10cm}}
    97   {\tt produced}     & total number of new nodes ever produced \\
    98   {\tt nodenum}      & currently allocated number of bdd nodes \\
    99   {\tt maxnodenum}   & user defined maximum number of bdd nodes \\
    100   {\tt freenodes}    & number of currently free nodes \\
    101   {\tt minfreenodes} & minimum number of nodes that should be left after a
    102                        garbage collection. \\
    103   {\tt varnum}       & number of defined bdd variables \\
    104   {\tt cachesize}    & number of entries in the internal caches \\
    105   {\tt gbcnum}       & number of garbage collections done until now
    106   \end{tabular} *}
    107 ALSO    {* bdd\_stats *}
    108 */
    109 typedef struct s_bddStat
    110 {
    111    long int produced;
    112    int nodenum;
    113    int maxnodenum;
    114    int freenodes;
    115    int minfreenodes;
    116    int varnum;
    117    int cachesize;
    118    int gbcnum;
    119 } bddStat;
    120 
    121 
    122 /*
    123 NAME    {* bddGbcStat *}
    124 SECTION {* kernel *}
    125 SHORT   {* Status information about garbage collections *}
    126 PROTO   {* typedef struct s_bddGbcStat
    127 {
    128    int nodes;
    129    int freenodes;
    130    long time;
    131    long sumtime;
    132    int num;
    133 } bddGbcStat;  *}
    134 DESCR   {* The fields are \\[\baselineskip] \begin{tabular}{ll}
    135   {\tt nodes}     & Total number of allocated nodes in the nodetable \\
    136   {\tt freenodes} & Number of free nodes in the nodetable \\
    137   {\tt time}      & Time used for garbage collection this time \\
    138   {\tt sumtime}   & Total time used for garbage collection \\
    139   {\tt num}       & number of garbage collections done until now
    140   \end{tabular} *}
    141 ALSO    {* bdd\_gbc\_hook *}
    142 */
    143 typedef struct s_bddGbcStat
    144 {
    145    int nodes;
    146    int freenodes;
    147    long time;
    148    long sumtime;
    149    int num;
    150 } bddGbcStat;
    151 
    152 
    153 /*
    154 NAME    {* bddCacheStat *}
    155 SECTION {* kernel *}
    156 SHORT   {* Status information about cache usage *}
    157 PROTO   {* typedef struct s_bddCacheStat
    158 {
    159    long unsigned int uniqueAccess;
    160    long unsigned int uniqueChain;
    161    long unsigned int uniqueHit;
    162    long unsigned int uniqueMiss;
    163    long unsigned int opHit;
    164    long unsigned int opMiss;
    165    long unsigned int swapCount;
    166 } bddCacheStat; *}
    167 DESCR   {* The fields are \\[\baselineskip] \begin{tabular}{ll}
    168   {\bf Name}         & {\bf Number of } \\
    169   uniqueAccess & accesses to the unique node table \\
    170   uniqueChain  & iterations through the cache chains in the unique node table\\
    171   uniqueHit    & entries actually found in the the unique node table \\
    172   uniqueMiss   & entries not found in the the unique node table \\
    173   opHit        & entries found in the operator caches \\
    174   opMiss       & entries not found in the operator caches \\
    175   swapCount    & number of variable swaps in reordering \\
    176 \end{tabular} *}
    177 ALSO    {* bdd\_cachestats *}
    178 */
    179 typedef struct s_bddCacheStat
    180 {
    181    long unsigned int uniqueAccess;
    182    long unsigned int uniqueChain;
    183    long unsigned int uniqueHit;
    184    long unsigned int uniqueMiss;
    185    long unsigned int opHit;
    186    long unsigned int opMiss;
    187    long unsigned int swapCount;
    188 } bddCacheStat;
    18977
    19078/*=== BDD interface prototypes =========================================*/
     
    21199
    212100typedef void (*bddinthandler)(int);
    213 typedef void (*bddgbchandler)(int,bddGbcStat*);
    214101typedef void (*bdd2inthandler)(int,int);
    215102typedef int  (*bddsizehandler)(void);
     
    217104typedef void (*bddallsathandler)(char*, int);
    218105   
    219 extern bddinthandler  bdd_error_hook(bddinthandler);
    220 extern bddgbchandler  bdd_gbc_hook(bddgbchandler);
    221106extern bdd2inthandler bdd_resize_hook(bdd2inthandler);
    222107extern bddinthandler  bdd_reorder_hook(bddinthandler);
     
    233118extern int      bdd_getnodenum(void);
    234119extern int      bdd_getallocnum(void);
    235 extern void     bdd_stats(bddStat *);
    236 extern void     bdd_cachestats(bddCacheStat *);
    237 extern void     bdd_fprintstat(FILE *);
    238 extern void     bdd_printstat(void);
    239 extern void     bdd_default_gbchandler(int, bddGbcStat *);
    240 extern void     bdd_default_errhandler(int);
    241 extern std::string bdd_errstring(const int);
    242 extern void     bdd_clear_error(void);
    243120extern int      bdd_varnum(void);
    244121extern BDD      bdd_ithvar(int);
     
    268145extern BDD      bdd_buildcube(int, int, BDD *);
    269146extern BDD      bdd_ibuildcube(int, int, int *);
    270 extern BDD      bdd_not(BDD);
    271 extern BDD      bdd_apply(BDD, BDD, int);
    272 extern BDD      bdd_ite(BDD, BDD, BDD);
    273 extern BDD      bdd_restrict(BDD, BDD);
    274 extern BDD      bdd_constrain(BDD, BDD);
    275 extern BDD      bdd_replace(BDD, bddPair*);
     147extern BDD      bdd_not(const BDD);
     148extern BDD      bdd_apply(const BDD, const BDD, const int);
     149extern BDD      bdd_ite(const BDD, const BDD, const BDD);
     150extern BDD      bdd_restrict(const BDD, const BDD);
     151extern BDD      bdd_constrain(const BDD, const BDD);
     152extern BDD      bdd_replace(const BDD, const bddPair * const);
    276153extern BDD      bdd_compose(BDD, BDD, BDD);
    277154extern BDD      bdd_veccompose(BDD, bddPair*);
     
    346223/*=== BDD constants ====================================================*/
    347224
    348 static inline BDD bdd_one(void) {
     225static inline BDD bdd_one() {
    349226   return 1;
    350227}
    351228
    352 static inline BDD bdd_zero(void) {
     229static inline BDD bdd_zero() {
    353230   return 0;
    354231}
     
    360237/*=== BDD helpers ====================================================*/
    361238
    362 static inline BDD bdd_and(BDD l, BDD r) {
     239static inline BDD bdd_and(const BDD l, const BDD r) {
    363240    return bdd_apply(l, r, bddop_and);
    364241}
    365242
    366 static inline BDD bdd_or(BDD l, BDD r) {
     243static inline BDD bdd_or(const BDD l, const BDD r) {
    367244    return bdd_apply(l, r, bddop_or);
    368245}
    369246
    370 static inline BDD bdd_xor(BDD l, BDD r) {
     247static inline BDD bdd_xor(const BDD l, const BDD r) {
    371248    return bdd_apply(l, r, bddop_xor);
    372249}
    373250
    374 static inline BDD bdd_nor(BDD l, BDD r) {
     251static inline BDD bdd_nor(const BDD l, const BDD r) {
    375252    return bdd_apply(l, r, bddop_nor);
    376253}
    377254
    378 static inline BDD bdd_imp(BDD l, BDD r) {
     255static inline BDD bdd_imp(const BDD l, const BDD r) {
    379256    return bdd_apply(l, r, bddop_imp);
    380257}
    381258
    382 static inline BDD bdd_biimp(BDD l, BDD r) {
     259static inline BDD bdd_biimp(const BDD l, const BDD r) {
    383260    return bdd_apply(l, r, bddop_biimp);
    384261}
     
    401278/*=== Error codes ======================================================*/
    402279
    403 #define BDD_MEMORY (-1)   /* Out of memory */
    404 #define BDD_VAR (-2)      /* Unknown variable */
    405 #define BDD_RANGE (-3)    /* Variable value out of range (not in domain) */
    406 #define BDD_DEREF (-4)    /* Removing external reference to unknown node */
    407 #define BDD_RUNNING (-5)  /* Called bdd_init() twice whithout bdd_done() */
    408 #define BDD_FILE (-6)     /* Some file operation failed */
    409 #define BDD_FORMAT (-7)   /* Incorrect file format */
    410 #define BDD_ORDER (-8)    /* Vars. not in order for vector based functions */
    411 #define BDD_BREAK (-9)    /* User called break */
    412 #define BDD_VARNUM (-10)  /* Different number of vars. for vector pair */
    413 #define BDD_NODES (-11)   /* Tried to set max. number of nodes to be fewer */
     280#define BDD_MEMORY (0)    /* Out of memory */
     281#define BDD_VAR (1)       /* Unknown variable */
     282#define BDD_RANGE (2)     /* Variable value out of range (not in domain) */
     283#define BDD_DEREF (3)     /* Removing external reference to unknown node */
     284#define BDD_RUNNING (4)   /* Called bdd_init() twice whithout bdd_done() */
     285#define BDD_FILE (5)      /* Some file operation failed */
     286#define BDD_FORMAT (6)    /* Incorrect file format */
     287#define BDD_ORDER (7)     /* Vars. not in order for vector based functions */
     288#define BDD_BREAK (8)     /* User called break */
     289#define BDD_VARNUM (9)   /* Different number of vars. for vector pair */
     290#define BDD_NODES (10)    /* Tried to set max. number of nodes to be fewer */
    414291                          /* than there already has been allocated */
    415 #define BDD_OP (-12)      /* Unknown operator */
    416 #define BDD_VARSET (-13)  /* Illegal variable set */
    417 #define BDD_VARBLK (-14)  /* Bad variable block operation */
    418 #define BDD_DECVNUM (-15) /* Trying to decrease the number of variables */
    419 #define BDD_REPLACE (-16) /* Replacing to already existing variables */
    420 #define BDD_NODENUM (-17) /* Number of nodes reached user defined maximum */
    421 #define BDD_ILLBDD (-18)  /* Illegal bdd argument */
    422 #define BDD_SIZE (-19)    /* Illegal size argument */
    423 
    424 #define BVEC_SIZE (-20)    /* Mismatch in bitvector size */
    425 #define BVEC_SHIFT (-21)   /* Illegal shift-left/right parameter */
    426 #define BVEC_DIVZERO (-22) /* Division by zero */
    427 
    428 #define BDD_ERRNUM 24
     292#define BDD_OP (11)       /* Unknown operator */
     293#define BDD_VARSET (12)   /* Illegal variable set */
     294#define BDD_VARBLK (13)   /* Bad variable block operation */
     295#define BDD_DECVNUM (14) /* Trying to decrease the number of variables */
     296#define BDD_REPLACE (15) /* Replacing to already existing variables */
     297#define BDD_NODENUM (16) /* Number of nodes reached user defined maximum */
     298#define BDD_ILLBDD (17)   /* Illegal bdd argument */
     299#define BDD_SIZE (18)     /* Illegal size argument */
     300
     301#define BVEC_SIZE (19)    /* Mismatch in bitvector size */
     302#define BVEC_SHIFT (20)   /* Illegal shift-left/right parameter */
     303#define BVEC_DIVZERO (21) /* Division by zero */
     304
     305#define BDD_ERRNUM 22
    429306
    430307#ifdef CPLUSPLUS
  • icGREP/icgrep-devel/buddy-2.4/src/bddop.cpp

    r4928 r4938  
    4141#include <assert.h>
    4242#include <stdexcept>
     43#include <functional>
    4344
    4445#include "kernel.h"
     
    9697static int *replacepair;            /* Current replace pair */
    9798static int replacelast;             /* Current last var. level to replace */
    98 static int composelevel;            /* Current variable used for compose */
    9999static int miscid;                  /* Current cache id for other results */
    100100static int *varprofile;             /* Current variable profile */
     
    104104static int* supportSet;             /* The found support set */
    105105static BddCache applycache;         /* Cache for apply results */
    106 static BddCache itecache;           /* Cache for ITE results */
    107106static BddCache quantcache;         /* Cache for exist/forall results */
    108107static BddCache appexcache;         /* Cache for appex/appall results */
     
    114113static bddallsathandler allsatHandler; /* Callback handler for bdd_allsat() */
    115114
    116 extern bddCacheStat bddcachestats;
    117 
    118115/* Internal prototypes */
    119 static BDD    not_rec(BDD);
    120 static BDD    apply_rec(BDD, BDD);
    121 static BDD    ite_rec(BDD, BDD, BDD);
    122116static int    simplify_rec(BDD, BDD);
    123117static int    quant_rec(int);
    124118static int    appquant_rec(int, int);
    125 static int    restrict_rec(int);
    126 static BDD    constrain_rec(BDD, BDD);
    127 static BDD    replace_rec(BDD);
    128 static BDD    bdd_correctify(int, BDD, BDD);
    129 static BDD    compose_rec(BDD, BDD);
    130119static BDD    veccompose_rec(BDD);
    131120static void   support_rec(int, int*);
     
    172161{
    173162    if (BddCache_init(&applycache,cachesize) < 0)
    174         return bdd_error(BDD_MEMORY);
    175 
    176     if (BddCache_init(&itecache,cachesize) < 0)
    177         return bdd_error(BDD_MEMORY);
     163        bdd_error(BDD_MEMORY);
    178164
    179165    if (BddCache_init(&quantcache,cachesize) < 0)
    180         return bdd_error(BDD_MEMORY);
     166        bdd_error(BDD_MEMORY);
    181167
    182168    if (BddCache_init(&appexcache,cachesize) < 0)
    183         return bdd_error(BDD_MEMORY);
     169        bdd_error(BDD_MEMORY);
    184170
    185171    if (BddCache_init(&replacecache,cachesize) < 0)
    186         return bdd_error(BDD_MEMORY);
     172        bdd_error(BDD_MEMORY);
    187173
    188174    if (BddCache_init(&misccache,cachesize) < 0)
    189         return bdd_error(BDD_MEMORY);
     175        bdd_error(BDD_MEMORY);
    190176
    191177    quantvarsetID = 0;
    192     quantvarset = NULL;
     178    quantvarset = nullptr;
    193179    cacheratio = 0;
    194     supportSet = NULL;
     180    supportSet = nullptr;
    195181
    196182    return 0;
     
    200186void bdd_operator_done(void)
    201187{
    202     if (quantvarset != NULL)
     188    if (quantvarset != nullptr)
    203189        free(quantvarset);
    204190
    205191    BddCache_done(&applycache);
    206     BddCache_done(&itecache);
    207192    BddCache_done(&quantcache);
    208193    BddCache_done(&appexcache);
     
    210195    BddCache_done(&misccache);
    211196
    212     if (supportSet != NULL)
     197    if (supportSet != nullptr)
    213198        free(supportSet);
    214199}
     
    218203{
    219204    BddCache_reset(&applycache);
    220     BddCache_reset(&itecache);
    221205    BddCache_reset(&quantcache);
    222206    BddCache_reset(&appexcache);
     
    228212void bdd_operator_varresize(void)
    229213{
    230     if (quantvarset != NULL)
     214    if (quantvarset != nullptr)
    231215        free(quantvarset);
    232216
    233     if ((quantvarset=NEW(int,bddvarnum)) == NULL)
     217    if ((quantvarset=NEW(int,bddvarnum)) == nullptr)
    234218        bdd_error(BDD_MEMORY);
    235219
     
    246230
    247231        BddCache_resize(&applycache, newcachesize);
    248         BddCache_resize(&itecache, newcachesize);
    249232        BddCache_resize(&quantcache, newcachesize);
    250233        BddCache_resize(&appexcache, newcachesize);
     
    280263
    281264    if (r <= 0)
    282         return bdd_error(BDD_RANGE);
     265        bdd_error(BDD_RANGE);
    283266    if (bddnodesize == 0)
    284267        return old;
     
    324307ALSO    {* bdd\_ithvar, fdd\_ithvar *}
    325308*/
    326 BDD bdd_buildcube(int value, int width, BDD * variables)
    327 {
     309BDD bdd_buildcube(int value, int width, BDD * variables) {
    328310    BDD result = BDDONE;
    329 
    330311    for (int z = 0; z < width ; z++, value>>=1) {
    331312        BDD v = variables[width - z - 1];
    332         if ((value & 1) == 0) {
    333             v = bdd_not(v);
    334         }
    335         v = bdd_addref(v);
    336 
     313        v = bdd_addref((value & 1) ? v : bdd_not(v));
    337314        bdd_addref(result);
    338315        BDD tmp = bdd_apply(result, v, bddop_and);
    339316        bdd_delref(result);
    340 
    341317        bdd_delref(v);
    342 
    343318        result = tmp;
    344319    }
    345 
    346320    return result;
    347321}
    348322
    349323
    350 BDD bdd_ibuildcube(int value, int width, int *variables)
    351 {
     324BDD bdd_ibuildcube(int value, int width, int *variables) {
    352325    BDD result = BDDONE;
    353 
    354     for (int z = 0 ; z<width ; z++, value>>=1)
    355     {
    356         BDD tmp;
    357         BDD v;
    358 
    359         if (value & 0x1)
    360             v = bdd_ithvar(variables[width-z-1]);
    361         else
    362             v = bdd_nithvar(variables[width-z-1]);
    363 
     326    for (int z = 0 ; z<width ; z++, value>>=1) {
     327        BDD v = variables[width - z - 1];
     328        v = (value & 0x1) ? bdd_ithvar(v) : bdd_nithvar(v);
    364329        bdd_addref(result);
    365         tmp = bdd_apply(result,v,bddop_and);
     330        BDD tmp = bdd_apply(result, v, bddop_and);
    366331        bdd_delref(result);
    367 
    368332        result = tmp;
    369333    }
    370 
    371334    return result;
    372335}
     
    384347RETURN  {* The negated bdd. *}
    385348*/
    386 BDD bdd_not(BDD r)
    387 {
     349BDD bdd_not(const BDD r) {
     350
     351    CHECK(r);
     352
     353    struct RUN {
     354
     355        RUN(const BDD r) : r(r) { INITREF; }
     356
     357        BDD operator()() {
     358
     359            const BDD a = r;
     360
     361            if (UNLIKELY(ISCONST(a))) {
     362                return UNLIKELY(a < 0) ? a : (a ^ BDDONE);
     363            }
     364
     365            BddCacheData * const entry = BddCache_lookup(&applycache, NOTHASH(a));
     366            if (entry->a == a && entry->c == bddop_not) {
     367                return entry->r.res;
     368            }
     369
     370            r = LOW(a);
     371            PUSHREF(operator()());
     372            r = HIGH(a);
     373            PUSHREF(operator()());
     374            const BDD res = bdd_makenode(LEVEL(a), READREF(2), READREF(1));
     375            POPREF(2);
     376
     377            entry->a = a;
     378            entry->c = bddop_not;
     379            entry->r.res = res;
     380
     381            return res;
     382        }
     383
     384    private:
     385        BDD r;
     386    };
     387
    388388    BDD res = BDDZERO;
    389     CHECKa(r, bdd_zero());
    390 
    391389    try {
    392         INITREF;
    393         res = not_rec(r);
    394         checkresize();
    395     } catch (...) {
     390        res = RUN(r)();
     391    } catch (reordering_required) {
    396392        bdd_checkreorder();
    397393        bdd_disable_reorder();
    398         res = bdd_not(r);
     394        res = RUN(r)();
    399395        bdd_enable_reorder();
    400396    }
     397    checkresize();
    401398
    402399    return res;
    403400}
    404 
    405 
    406 static BDD not_rec(BDD r)
    407 {
    408     BddCacheData *entry;
    409     BDD res = BDDZERO;
    410 
    411     if (ISZERO(r))
    412         return BDDONE;
    413     if (ISONE(r))
    414         return BDDZERO;
    415 
    416     entry = BddCache_lookup(&applycache, NOTHASH(r));
    417 
    418     if (entry->a == r  &&  entry->c == bddop_not)
    419     {
    420 #ifdef CACHESTATS
    421         bddcachestats.opHit++;
    422 #endif
    423         return entry->r.res;
    424     }
    425 #ifdef CACHESTATS
    426     bddcachestats.opMiss++;
    427 #endif
    428 
    429     PUSHREF( not_rec(LOW(r)) );
    430     PUSHREF( not_rec(HIGH(r)) );
    431     res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
    432     POPREF(2);
    433 
    434     entry->a = r;
    435     entry->c = bddop_not;
    436     entry->r.res = res;
    437 
    438     return res;
    439 }
    440 
    441401
    442402/*=== APPLY ============================================================*/
     
    453413       operation and must be one of the following\\
    454414
    455    \begin{tabular}{lllc}
    456      {\bf Identifier}    & {\bf Description} & {\bf Truth table}
    457         & {\bf C++ opr.} \\
    458      {\tt bddop\_and}    & logical and    ($A \wedge B$)         & [0,0,0,1]
    459         & \verb%&% \\
    460      {\tt bddop\_xor}    & logical xor    ($A \oplus B$)         & [0,1,1,0]
    461         & \verb%^% \\
    462      {\tt bddop\_or}     & logical or     ($A \vee B$)           & [0,1,1,1]
    463         & \verb%|% \\
    464      {\tt bddop\_nand}   & logical not-and                       & [1,1,1,0] \\
    465      {\tt bddop\_nor}    & logical not-or                        & [1,0,0,0] \\
    466      {\tt bddop\_imp}    & implication    ($A \Rightarrow B$)    & [1,1,0,1]
    467         & \verb%>>% \\
    468      {\tt bddop\_biimp}  & bi-implication ($A \Leftrightarrow B$)& [1,0,0,1] \\
    469      {\tt bddop\_diff}   & set difference ($A \setminus B$)      & [0,0,1,0]
    470         & \verb%-% \\
    471      {\tt bddop\_less}   & less than      ($A < B$)              & [0,1,0,0]
    472         & \verb%<% \\
    473      {\tt bddop\_invimp} & reverse implication ($A \Leftarrow B$)& [1,0,1,1]
    474         & \verb%<<% \\
    475    \end{tabular}
    476    *}
    477    RETURN  {* The result of the operation. *}
    478    ALSO    {* bdd\_ite *}
    479 */
    480 BDD bdd_apply(BDD l, BDD r, int op)
    481 {
     415*/
     416
     417BDD bdd_apply(const BDD l, const BDD r, const int op) {
     418
     419    CHECK(l);
     420    CHECK(r);
     421
     422    assert (op >= 0 && op <= bddop_invimp);
     423
     424    struct RUN {
     425
     426        RUN(const int op, const BDD l, const BDD r) : op(op), l(l), r(r) { INITREF; }
     427
     428        BDD operator()() {
     429
     430            const BDD a = l;
     431            const BDD b = r;
     432
     433            if (UNLIKELY(a == b)) {
     434                switch (op) {
     435                    case bddop_and:
     436                    case bddop_or:
     437                        return a;
     438                    case bddop_xor:
     439                        return 0;
     440                    case bddop_nand:
     441                    case bddop_nor:
     442                        return bdd_not(a);
     443                    case bddop_imp:
     444                        return 1;
     445                }
     446            } else if (UNLIKELY(ISCONST(a) || ISCONST(b))) {
     447
     448                if (UNLIKELY(a < 0)) {
     449                    return b;
     450                } else if (UNLIKELY(b < 0)) {
     451                    return a;
     452                } else if (UNLIKELY(ISCONST(a) && ISCONST(b))) {
     453                    return oprres[op][b << 1 | a];
     454                }
     455
     456                switch (op) {
     457                    case bddop_and:
     458                        if (ISZERO(a) || ISZERO(b))
     459                            return 0;
     460                        if (ISONE(a))
     461                            return b;
     462                        if (ISONE(a))
     463                            return b;
     464                        break;
     465                    case bddop_or:
     466                        if (ISONE(a) || ISONE(b))
     467                            return 1;
     468                        if (ISZERO(a))
     469                            return b;
     470                        if (ISZERO(b))
     471                            return a;
     472                        break;
     473                    case bddop_xor:
     474                        if (ISZERO(a))
     475                            return b;
     476                        if (ISZERO(b))
     477                            return a;
     478                        break;
     479                    case bddop_nand:
     480                        if (ISZERO(a) || ISZERO(b))
     481                            return 1;
     482                        break;
     483                    case bddop_nor:
     484                        if (ISONE(a) || ISONE(b))
     485                            return 0;
     486                        break;
     487                    case bddop_imp:
     488                        if (ISZERO(a) || ISONE(b))
     489                            return 1;
     490                        if (ISONE(a))
     491                            return b;
     492                        break;
     493                }
     494            }
     495
     496            BddCacheData * const entry = BddCache_lookup(&applycache, APPLYHASH(a, b, op));
     497            if (entry->a == a &&  entry->b == b && entry->c == op) {
     498                return entry->r.res;
     499            }
     500
     501            int La = LEVEL(a);
     502            const int Lb = LEVEL(b);
     503
     504            if (La == Lb) {               
     505                l = LOW(a);
     506                r = LOW(b);
     507                PUSHREF(operator()());
     508                l = HIGH(a);
     509                r = HIGH(b);
     510                PUSHREF(operator()());
     511            } else if (La < Lb) {
     512                l = LOW(a);
     513                PUSHREF(operator()());
     514                l = HIGH(a);
     515                PUSHREF(operator()());
     516            } else { // if (levelA > levelB) {
     517                La = Lb;
     518                r = LOW(b);
     519                PUSHREF(operator()());
     520                r = HIGH(b);
     521                PUSHREF(operator()());
     522            }
     523
     524            const BDD res = bdd_makenode(La, READREF(2), READREF(1));
     525
     526            POPREF(2);
     527
     528            entry->a = a;
     529            entry->b = b;
     530            entry->c = op;
     531            entry->r.res = res;
     532
     533            return res;
     534        }
     535    private:
     536        const int op;
     537        BDD l;
     538        BDD r;
     539    };
     540
    482541    BDD res = BDDZERO;
    483 
    484     CHECKa(l, bdd_zero());
    485     CHECKa(r, bdd_zero());
    486 
    487     assert (op >= 0 && op <= bddop_invimp);
    488 
    489542    try {
    490         INITREF;
    491         applyop = op;
    492         res = apply_rec(l, r);
    493         checkresize();
    494     } catch (...) {
     543        res = RUN(op, l, r)();
     544    } catch (reordering_required) {
    495545        bdd_checkreorder();
    496546        bdd_disable_reorder();
    497         res = bdd_apply(l, r, op);
     547        res = RUN(op, l, r)();
    498548        bdd_enable_reorder();
    499549    }
     550    checkresize();
    500551
    501552    return res;
    502553}
    503 
    504 
    505 static BDD apply_rec(BDD l, BDD r)
    506 {
    507     BddCacheData *entry;
    508     BDD res = BDDZERO;
    509 
    510     if (l < 0) {
    511         return r;
    512     } else if (r  < 0) {
    513         return l;
    514     }
    515 
    516     switch (applyop) {
    517         case bddop_and:
    518             if (l == r)
    519                 return l;
    520             if (ISZERO(l) || ISZERO(r))
    521                 return 0;
    522             if (ISONE(l))
    523                 return r;
    524             if (ISONE(r))
    525                 return l;
    526             break;
    527         case bddop_or:
    528             if (l == r)
    529                 return l;
    530             if (ISONE(l) || ISONE(r))
    531                 return 1;
    532             if (ISZERO(l))
    533                 return r;
    534             if (ISZERO(r))
    535                 return l;
    536             break;
    537         case bddop_xor:
    538             if (l == r)
    539                 return 0;
    540             if (ISZERO(l))
    541                 return r;
    542             if (ISZERO(r))
    543                 return l;
    544             break;
    545         case bddop_nand:
    546             if (ISZERO(l) || ISZERO(r))
    547                 return 1;
    548             break;
    549         case bddop_nor:
    550             if (ISONE(l) || ISONE(r))
    551                 return 0;
    552             break;
    553         case bddop_imp:
    554             if (ISZERO(l))
    555                 return 1;
    556             if (ISONE(l))
    557                 return r;
    558             if (ISONE(r))
    559                 return 1;
    560             break;
    561     }
    562 
    563     if (ISCONST(l) && ISCONST(r)) {
    564         res = oprres[applyop][l<<1 | r];
    565     } else {
    566         entry = BddCache_lookup(&applycache, APPLYHASH(l,r,applyop));
    567 
    568         if (entry->a == l  &&  entry->b == r  &&  entry->c == applyop)
    569         {
    570 #ifdef CACHESTATS
    571             bddcachestats.opHit++;
    572 #endif
    573             return entry->r.res;
    574         }
    575 #ifdef CACHESTATS
    576         bddcachestats.opMiss++;
    577 #endif
    578 
    579         if (LEVEL(l) == LEVEL(r)) {
    580             PUSHREF( apply_rec(LOW(l), LOW(r)) );
    581             PUSHREF( apply_rec(HIGH(l), HIGH(r)) );
    582             res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
    583         } else if (LEVEL(l) < LEVEL(r)) {
    584             PUSHREF( apply_rec(LOW(l), r) );
    585             PUSHREF( apply_rec(HIGH(l), r) );
    586             res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
    587         } else {
    588             PUSHREF( apply_rec(l, LOW(r)) );
    589             PUSHREF( apply_rec(l, HIGH(r)) );
    590             res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
    591         }
    592 
    593         POPREF(2);
    594 
    595         entry->a = l;
    596         entry->b = r;
    597         entry->c = applyop;
    598         entry->r.res = res;
    599     }
    600 
    601     return res;
    602 }
    603 
    604554/*=== ITE ==============================================================*/
    605555
     
    617567ALSO    {* bdd\_apply *}
    618568*/
    619 BDD bdd_ite(BDD f, BDD g, BDD h)
    620 {
     569BDD bdd_ite(const BDD f, const BDD g, const BDD h) {
     570
     571    CHECK(f);
     572    CHECK(g);
     573    CHECK(h);
     574
     575    struct RUN {
     576
     577        RUN(const BDD f, const BDD g, const BDD h) : f(f), g(g), h(h) { INITREF; }
     578
     579        BDD operator()() {
     580
     581            const BDD a = f;
     582            const BDD b = g;
     583            const BDD c = h;
     584
     585            if (ISONE(a))
     586                return b;
     587            if (ISZERO(a))
     588                return c;
     589            if (b == c)
     590                return b;
     591            if (ISONE(b) && ISZERO(c))
     592                return a;
     593            if (ISZERO(b) && ISONE(c))
     594                return bdd_not(a);
     595
     596            BddCacheData * const entry = BddCache_lookup(&applycache, APPLYHASH(a, b, (c + OPERATOR_NUM)));
     597            if (entry->a == a  &&  entry->b == b  &&  entry->c == (c + OPERATOR_NUM)) {
     598                return entry->r.res;
     599            }
     600
     601            BDD res = BDDZERO;
     602
     603            if (LEVEL(a) == LEVEL(b)) {
     604                if (LEVEL(a) == LEVEL(c)) {
     605                    f = LOW(a);
     606                    g = LOW(b);
     607                    h = LOW(c);
     608                    PUSHREF(operator()());
     609                    f = HIGH(a);
     610                    g = HIGH(b);
     611                    h = HIGH(c);
     612                    PUSHREF(operator()());
     613                    res = bdd_makenode(LEVEL(a), READREF(2), READREF(1));
     614                } else if (LEVEL(a) < LEVEL(c)) {
     615                    f = LOW(a);
     616                    g = LOW(b);
     617                    PUSHREF(operator()());
     618                    f = HIGH(a);
     619                    g = HIGH(b);
     620                    PUSHREF(operator()());
     621                    res = bdd_makenode(LEVEL(a), READREF(2), READREF(1));
     622                } else { // f > h
     623                    h = LOW(c);
     624                    PUSHREF(operator()());
     625                    h = HIGH(c);
     626                    PUSHREF(operator()());
     627                    res = bdd_makenode(LEVEL(c), READREF(2), READREF(1));
     628                }
     629            } else if (LEVEL(a) < LEVEL(b)) {
     630                if (LEVEL(a) == LEVEL(c)) {
     631                    f = LOW(a);
     632                    h = LOW(c);
     633                    PUSHREF(operator()());
     634                    f = HIGH(a);
     635                    h = HIGH(c);
     636                    PUSHREF(operator()());
     637                    res = bdd_makenode(LEVEL(a), READREF(2), READREF(1));
     638                } else if (LEVEL(a) < LEVEL(c)) {
     639                    f = LOW(a);
     640                    PUSHREF(operator()());
     641                    f = HIGH(a);
     642                    PUSHREF(operator()());
     643                    res = bdd_makenode(LEVEL(a), READREF(2), READREF(1));
     644                } else { // f > h
     645                    h = LOW(c);
     646                    PUSHREF(operator()());
     647                    h = HIGH(c);
     648                    PUSHREF(operator()());
     649                    res = bdd_makenode(LEVEL(c), READREF(2), READREF(1));
     650                }
     651            } else { // f > g
     652                if (LEVEL(b) == LEVEL(c)) {
     653                    g = LOW(b);
     654                    h = LOW(c);
     655                    PUSHREF(operator()());
     656                    g = HIGH(b);
     657                    h = HIGH(c);
     658                    PUSHREF(operator()());
     659                    res = bdd_makenode(LEVEL(b), READREF(2), READREF(1));
     660                } else if (LEVEL(b) < LEVEL(c)) {
     661                    g = LOW(b);
     662                    PUSHREF(operator()());
     663                    g = HIGH(b);
     664                    PUSHREF(operator()());
     665                    res = bdd_makenode(LEVEL(b), READREF(2), READREF(1));
     666                } else { // g > h
     667                    h = LOW(c);
     668                    PUSHREF(operator()());
     669                    h = HIGH(c);
     670                    PUSHREF(operator()());
     671                    res = bdd_makenode(LEVEL(c), READREF(2), READREF(1));
     672                }
     673            }
     674
     675            POPREF(2);
     676
     677            entry->a = a;
     678            entry->b = b;
     679            entry->c = c + OPERATOR_NUM;
     680            entry->r.res = res;
     681
     682            return res;
     683
     684        }
     685    private:
     686        BDD f;
     687        BDD g;
     688        BDD h;
     689    };
     690
     691
    621692    BDD res = BDDZERO;
    622 
    623     CHECKa(f, bdd_zero());
    624     CHECKa(g, bdd_zero());
    625     CHECKa(h, bdd_zero());
    626 
    627693    try {
    628         INITREF;
    629         res = ite_rec(f, g, h);
    630         checkresize();
    631     } catch (...) {
     694        res = RUN(f, g, h)();
     695    } catch (reordering_required) {
    632696        bdd_checkreorder();
    633697        bdd_disable_reorder();
    634         res = bdd_ite(f, g, h);
     698        res = RUN(f, g, h)();
    635699        bdd_enable_reorder();
    636700    }
     701    checkresize();
    637702
    638703    return res;
    639704}
    640 
    641 
    642 static BDD ite_rec(BDD f, BDD g, BDD h)
    643 {
    644     BddCacheData *entry;
    645     BDD res = BDDZERO;
    646 
    647     if (ISONE(f))
    648         return g;
    649     if (ISZERO(f))
    650         return h;
    651     if (g == h)
    652         return g;
    653     if (ISONE(g) && ISZERO(h))
    654         return f;
    655     if (ISZERO(g) && ISONE(h))
    656         return not_rec(f);
    657 
    658     entry = BddCache_lookup(&itecache, ITEHASH(f,g,h));
    659     if (entry->a == f  &&  entry->b == g  &&  entry->c == h)
    660     {
    661 #ifdef CACHESTATS
    662         bddcachestats.opHit++;
    663 #endif
    664         return entry->r.res;
    665     }
    666 #ifdef CACHESTATS
    667     bddcachestats.opMiss++;
    668 #endif
    669 
    670     if (LEVEL(f) == LEVEL(g))
    671     {
    672         if (LEVEL(f) == LEVEL(h))
    673         {
    674             PUSHREF( ite_rec(LOW(f), LOW(g), LOW(h)) );
    675             PUSHREF( ite_rec(HIGH(f), HIGH(g), HIGH(h)) );
    676             res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    677         }
    678         else
    679             if (LEVEL(f) < LEVEL(h))
    680             {
    681                 PUSHREF( ite_rec(LOW(f), LOW(g), h) );
    682                 PUSHREF( ite_rec(HIGH(f), HIGH(g), h) );
    683                 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    684             }
    685             else /* f > h */
    686             {
    687                 PUSHREF( ite_rec(f, g, LOW(h)) );
    688                 PUSHREF( ite_rec(f, g, HIGH(h)) );
    689                 res = bdd_makenode(LEVEL(h), READREF(2), READREF(1));
    690             }
    691     }
    692     else
    693         if (LEVEL(f) < LEVEL(g))
    694         {
    695             if (LEVEL(f) == LEVEL(h))
    696             {
    697                 PUSHREF( ite_rec(LOW(f), g, LOW(h)) );
    698                 PUSHREF( ite_rec(HIGH(f), g, HIGH(h)) );
    699                 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    700             }
    701             else
    702                 if (LEVEL(f) < LEVEL(h))
    703                 {
    704                     PUSHREF( ite_rec(LOW(f), g, h) );
    705                     PUSHREF( ite_rec(HIGH(f), g, h) );
    706                     res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    707                 }
    708                 else /* f > h */
    709                 {
    710                     PUSHREF( ite_rec(f, g, LOW(h)) );
    711                     PUSHREF( ite_rec(f, g, HIGH(h)) );
    712                     res = bdd_makenode(LEVEL(h), READREF(2), READREF(1));
    713                 }
    714         }
    715         else /* f > g */
    716         {
    717             if (LEVEL(g) == LEVEL(h))
    718             {
    719                 PUSHREF( ite_rec(f, LOW(g), LOW(h)) );
    720                 PUSHREF( ite_rec(f, HIGH(g), HIGH(h)) );
    721                 res = bdd_makenode(LEVEL(g), READREF(2), READREF(1));
    722             }
    723             else
    724                 if (LEVEL(g) < LEVEL(h))
    725                 {
    726                     PUSHREF( ite_rec(f, LOW(g), h) );
    727                     PUSHREF( ite_rec(f, HIGH(g), h) );
    728                     res = bdd_makenode(LEVEL(g), READREF(2), READREF(1));
    729                 }
    730                 else /* g > h */
    731                 {
    732                     PUSHREF( ite_rec(f, g, LOW(h)) );
    733                     PUSHREF( ite_rec(f, g, HIGH(h)) );
    734                     res = bdd_makenode(LEVEL(h), READREF(2), READREF(1));
    735                 }
    736         }
    737 
    738     POPREF(2);
    739 
    740     entry->a = f;
    741     entry->b = g;
    742     entry->c = h;
    743     entry->r.res = res;
    744 
    745     return res;
    746 }
    747 
    748705
    749706/*=== RESTRICT =========================================================*/
     
    775732ALSO    {* bdd\_makeset, bdd\_exist, bdd\_forall *}
    776733*/
    777 BDD bdd_restrict(BDD r, BDD var)
     734BDD bdd_restrict(const BDD r, const BDD var)
    778735{
    779736    BDD res = BDDZERO;
    780737
    781     CHECKa(r, bdd_zero());
    782     CHECKa(var, bdd_zero());
     738    CHECK(r);
     739    CHECK(var);
    783740
    784741    if (var < 2)  /* Empty set */
    785742        return r;
    786743
     744    if (varset2svartable(var) < 0)
     745        return bdd_zero();
     746
     747    const int miscid = (var << 3) | CACHEID_RESTRICT;
     748
     749    std::function<int(const int)> restrict_rec = [&](const int r) -> int {
     750        if (ISCONST(r)  ||  LEVEL(r) > quantlast)
     751            return r;
     752
     753        BddCacheData * entry = BddCache_lookup(&misccache, RESTRHASH(r, miscid));
     754        if (entry->a == r  &&  entry->c == miscid) {
     755            return entry->r.res;
     756        }
     757
     758        int res = 0;
     759        if (INSVARSET(LEVEL(r))) {
     760            if (quantvarset[LEVEL(r)] > 0) {
     761                res = restrict_rec(HIGH(r));
     762            } else {
     763                res = restrict_rec(LOW(r));
     764            }
     765        } else {
     766            PUSHREF(restrict_rec(LOW(r)));
     767            PUSHREF(restrict_rec(HIGH(r)));
     768            res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
     769            POPREF(2);
     770        }
     771
     772        entry->a = r;
     773        entry->c = miscid;
     774        entry->r.res = res;
     775
     776        return res;
     777    };
     778
     779
    787780    try {
    788         if (varset2svartable(var) < 0)
    789             return bdd_zero();
    790781        INITREF;
    791         miscid = (var << 3) | CACHEID_RESTRICT;
    792782        res = restrict_rec(r);
    793         checkresize();
    794     } catch (...) {
     783    } catch (reordering_required) {
    795784        bdd_checkreorder();
    796785        bdd_disable_reorder();
    797         res = bdd_restrict(r, var);
     786        INITREF;
     787        res = restrict_rec(r);
    798788        bdd_enable_reorder();
    799789    }
     790    checkresize();
    800791
    801792    return res;
    802793}
    803 
    804 
    805 static int restrict_rec(int r)
    806 {
    807     BddCacheData *entry;
    808     int res;
    809 
    810     if (ISCONST(r)  ||  LEVEL(r) > quantlast)
    811         return r;
    812 
    813     entry = BddCache_lookup(&misccache, RESTRHASH(r,miscid));
    814     if (entry->a == r  &&  entry->c == miscid)
    815     {
    816 #ifdef CACHESTATS
    817         bddcachestats.opHit++;
    818 #endif
    819         return entry->r.res;
    820     }
    821 #ifdef CACHESTATS
    822     bddcachestats.opMiss++;
    823 #endif
    824 
    825     if (INSVARSET(LEVEL(r)))
    826     {
    827         if (quantvarset[LEVEL(r)] > 0)
    828             res = restrict_rec(HIGH(r));
    829         else
    830             res = restrict_rec(LOW(r));
    831     }
    832     else
    833     {
    834         PUSHREF( restrict_rec(LOW(r)) );
    835         PUSHREF( restrict_rec(HIGH(r)) );
    836         res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
    837         POPREF(2);
    838     }
    839 
    840     entry->a = r;
    841     entry->c = miscid;
    842     entry->r.res = res;
    843 
    844     return res;
    845 }
    846 
    847794
    848795/*=== GENERALIZED COFACTOR =============================================*/
     
    858805ALSO    {* bdd\_restrict, bdd\_simplify *}
    859806*/
    860 BDD bdd_constrain(BDD f, BDD c)
    861 {
    862     BDD res = BDDZERO;
    863 
    864     CHECKa(f,bdd_zero());
    865     CHECKa(c,bdd_zero());
    866 
    867     try {
    868         INITREF;
    869         miscid = CACHEID_CONSTRAIN;
    870         res = constrain_rec(f, c);
    871         checkresize();
    872     } catch (...) {
    873         bdd_checkreorder();
    874         bdd_disable_reorder();
    875         res = bdd_constrain(f, c);
    876         bdd_enable_reorder();
    877     }
    878 
    879     return res;
    880 }
    881 
    882 
    883 static BDD constrain_rec(BDD f, BDD c)
    884 {
    885     BddCacheData *entry;
    886     BDD res = BDDZERO;
    887 
    888     if (ISONE(c))
    889         return f;
    890     if (ISCONST(f))
    891         return f;
    892     if (c == f)
    893         return BDDONE;
    894     if (ISZERO(c))
    895         return BDDZERO;
    896 
    897     entry = BddCache_lookup(&misccache, CONSTRAINHASH(f,c));
    898     if (entry->a == f  &&  entry->b == c  &&  entry->c == miscid)
    899     {
    900 #ifdef CACHESTATS
    901         bddcachestats.opHit++;
    902 #endif
    903         return entry->r.res;
    904     }
    905 #ifdef CACHESTATS
    906     bddcachestats.opMiss++;
    907 #endif
    908 
    909     if (LEVEL(f) == LEVEL(c))
    910     {
    911         if (ISZERO(LOW(c)))
    912             res = constrain_rec(HIGH(f), HIGH(c));
    913         else if (ISZERO(HIGH(c)))
    914             res = constrain_rec(LOW(f), LOW(c));
    915         else
    916         {
    917             PUSHREF( constrain_rec(LOW(f), LOW(c)) );
    918             PUSHREF( constrain_rec(HIGH(f), HIGH(c)) );
    919             res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    920             POPREF(2);
    921         }
    922     }
    923     else
    924         if (LEVEL(f) < LEVEL(c))
    925         {
     807BDD bdd_constrain(const BDD f, const BDD c) {
     808
     809    CHECK(f);
     810    CHECK(c);
     811
     812    std::function<BDD(const BDD, const BDD)> constrain_rec = [&](const BDD f, const BDD c) -> BDD {
     813
     814        if (ISONE(c) || ISCONST(f))
     815            return f;
     816        if (c == f)
     817            return BDDONE;
     818        if (ISZERO(c))
     819            return BDDZERO;
     820
     821        BddCacheData * entry = BddCache_lookup(&misccache, CONSTRAINHASH(f,c));
     822        if (entry->a == f  &&  entry->b == c  &&  entry->c == CACHEID_CONSTRAIN) {
     823            return entry->r.res;
     824        }
     825
     826        BDD res = BDDZERO;
     827
     828        if (LEVEL(f) == LEVEL(c)) {
     829            if (ISZERO(LOW(c))) {
     830                res = constrain_rec(HIGH(f), HIGH(c));
     831            } else if (ISZERO(HIGH(c))) {
     832                res = constrain_rec(LOW(f), LOW(c));
     833            } else {
     834                PUSHREF( constrain_rec(LOW(f), LOW(c)) );
     835                PUSHREF( constrain_rec(HIGH(f), HIGH(c)) );
     836                res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
     837                POPREF(2);
     838            }
     839        } else if (LEVEL(f) < LEVEL(c)) {
    926840            PUSHREF( constrain_rec(LOW(f), c) );
    927841            PUSHREF( constrain_rec(HIGH(f), c) );
    928842            res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    929843            POPREF(2);
    930         }
    931         else
    932         {
    933             if (ISZERO(LOW(c)))
    934                 res = constrain_rec(f, HIGH(c));
    935             else if (ISZERO(HIGH(c)))
    936                 res = constrain_rec(f, LOW(c));
    937             else
    938             {
    939                 PUSHREF( constrain_rec(f, LOW(c)) );
    940                 PUSHREF( constrain_rec(f, HIGH(c)) );
    941                 res = bdd_makenode(LEVEL(c), READREF(2), READREF(1));
    942                 POPREF(2);
    943             }
    944         }
    945 
    946     entry->a = f;
    947     entry->b = c;
    948     entry->c = miscid;
    949     entry->r.res = res;
     844        } else if (ISZERO(LOW(c))) {
     845            res = constrain_rec(f, HIGH(c));
     846        } else if (ISZERO(HIGH(c))) {
     847            res = constrain_rec(f, LOW(c));
     848        } else {
     849            PUSHREF( constrain_rec(f, LOW(c)) );
     850            PUSHREF( constrain_rec(f, HIGH(c)) );
     851            res = bdd_makenode(LEVEL(c), READREF(2), READREF(1));
     852            POPREF(2);
     853        }
     854
     855        entry->a = f;
     856        entry->b = c;
     857        entry->c = CACHEID_CONSTRAIN;
     858        entry->r.res = res;
     859
     860        return res;
     861
     862    };
     863
     864    BDD res = BDDZERO;
     865    try {
     866        INITREF;
     867        res = constrain_rec(f, c);
     868    } catch (reordering_required) {
     869        bdd_checkreorder();
     870        bdd_disable_reorder();
     871        INITREF;
     872        res = constrain_rec(f, c);
     873        bdd_enable_reorder();
     874    }
     875    checkresize();
    950876
    951877    return res;
    952878}
    953 
    954879
    955880/*=== REPLACE ==========================================================*/
     
    968893RETURN {* The result of the operation. *}
    969894*/
    970 BDD bdd_replace(BDD r, bddPair *pair)
    971 {
    972     BDD res = BDDZERO;
    973 
    974     CHECKa(r, bdd_zero());
    975 
    976     try {
    977         INITREF;
    978         replacepair = pair->result;
    979         replacelast = pair->last;
    980         replaceid = (pair->id << 2) | CACHEID_REPLACE;
    981         res = replace_rec(r);
    982         checkresize();
    983     } catch (...) {
    984         bdd_checkreorder();
    985         bdd_disable_reorder();
    986         res = bdd_replace(r, pair);
    987         bdd_enable_reorder();
    988     }
    989 
    990     return res;
    991 }
    992 
    993 
    994 static BDD replace_rec(BDD r)
    995 {
    996     BddCacheData *entry;
    997     BDD res = BDDZERO;
    998 
    999     if (ISCONST(r)  ||  LEVEL(r) > replacelast)
    1000         return r;
    1001 
    1002     entry = BddCache_lookup(&replacecache, REPLACEHASH(r));
    1003     if (entry->a == r  &&  entry->c == replaceid)
    1004     {
    1005 #ifdef CACHESTATS
    1006         bddcachestats.opHit++;
    1007 #endif
    1008         return entry->r.res;
    1009     }
    1010 #ifdef CACHESTATS
    1011     bddcachestats.opMiss++;
    1012 #endif
    1013 
    1014     PUSHREF( replace_rec(LOW(r)) );
    1015     PUSHREF( replace_rec(HIGH(r)) );
    1016 
    1017     res = bdd_correctify(LEVEL(replacepair[LEVEL(r)]), READREF(2), READREF(1));
    1018     POPREF(2);
    1019 
    1020     entry->a = r;
    1021     entry->c = replaceid;
    1022     entry->r.res = res;
    1023 
    1024     return res;
    1025 }
    1026 
    1027 
    1028 static BDD bdd_correctify(int level, BDD l, BDD r)
    1029 {
    1030     BDD res = BDDZERO;
    1031 
    1032     if (level < LEVEL(l)  &&  level < LEVEL(r))
    1033         return bdd_makenode(level, l, r);
    1034 
    1035     if (level == LEVEL(l)  ||  level == LEVEL(r))
    1036     {
    1037         bdd_error(BDD_REPLACE);
    1038         return 0;
    1039     }
    1040 
    1041     if (LEVEL(l) == LEVEL(r))
    1042     {
    1043         PUSHREF( bdd_correctify(level, LOW(l), LOW(r)) );
    1044         PUSHREF( bdd_correctify(level, HIGH(l), HIGH(r)) );
    1045         res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
    1046     }
    1047     else
    1048         if (LEVEL(l) < LEVEL(r))
    1049         {
     895BDD bdd_replace(const BDD r, const bddPair * const pair) {
     896
     897    CHECK(r);
     898
     899    const int replaceid = (pair->id << 2) | CACHEID_REPLACE;
     900
     901    std::function<BDD(const int, const BDD, const BDD)> bdd_correctify = [&](const int level, const BDD l, const BDD r) -> BDD {
     902
     903        if (level < LEVEL(l) && level < LEVEL(r)) {
     904            return bdd_makenode(level, l, r);
     905        }
     906
     907        if (level == LEVEL(l) || level == LEVEL(r)) {
     908            bdd_error(BDD_REPLACE);
     909        }
     910
     911        BDD res = BDDZERO;
     912        if (LEVEL(l) == LEVEL(r)) {
     913            PUSHREF( bdd_correctify(level, LOW(l), LOW(r)) );
     914            PUSHREF( bdd_correctify(level, HIGH(l), HIGH(r)) );
     915            res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
     916        } else if (LEVEL(l) < LEVEL(r)) {
    1050917            PUSHREF( bdd_correctify(level, LOW(l), r) );
    1051918            PUSHREF( bdd_correctify(level, HIGH(l), r) );
    1052919            res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
    1053         }
    1054         else
    1055         {
     920        } else {
    1056921            PUSHREF( bdd_correctify(level, l, LOW(r)) );
    1057922            PUSHREF( bdd_correctify(level, l, HIGH(r)) );
    1058923            res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
    1059924        }
    1060     POPREF(2);
    1061 
    1062     return res; /* FIXME: cache ? */
    1063 }
    1064 
     925        POPREF(2);
     926
     927        return res; /* FIXME: cache ? */
     928    };
     929
     930
     931    std::function<BDD(const BDD)> replace_rec = [&](const BDD r) -> BDD {
     932
     933        if (ISCONST(r)  ||  LEVEL(r) > pair->last)
     934            return r;
     935
     936        BddCacheData * entry = BddCache_lookup(&replacecache, REPLACEHASH(r));
     937        if (entry->a == r  &&  entry->c == replaceid) {
     938            return entry->r.res;
     939        }
     940
     941        PUSHREF(replace_rec(LOW(r)));
     942        PUSHREF(replace_rec(HIGH(r)));
     943        const BDD res = bdd_correctify(LEVEL(pair->result[LEVEL(r)]), READREF(2), READREF(1));
     944        POPREF(2);
     945
     946        entry->a = r;
     947        entry->c = replaceid;
     948        entry->r.res = res;
     949
     950        return res;
     951    };
     952
     953    BDD res = BDDZERO;
     954    try {
     955        INITREF;
     956        res = replace_rec(r);
     957    } catch (reordering_required) {
     958        bdd_checkreorder();
     959        bdd_disable_reorder();
     960        INITREF;
     961        res = replace_rec(r);
     962        bdd_enable_reorder();
     963    }
     964    checkresize();
     965
     966    return res;
     967}
    1065968
    1066969/*=== COMPOSE ==========================================================*/
     
    1076979ALSO    {* bdd\_veccompose, bdd\_replace, bdd\_restrict *}
    1077980*/
    1078 BDD bdd_compose(BDD f, BDD g, int var)
    1079 {
    1080     BDD res = BDDZERO;
    1081 
    1082     CHECKa(f, bdd_zero());
    1083     CHECKa(g, bdd_zero());
    1084     if (var < 0 || var >= bddvarnum) {
     981BDD bdd_compose(BDD f, BDD g, int var) {
     982
     983    CHECK(f);
     984    CHECK(g);
     985    if (UNLIKELY(var < 0 || var >= bddvarnum)) {
    1085986        bdd_error(BDD_VAR);
    1086         return bdd_zero();
    1087     }
    1088 
    1089     try {
    1090         INITREF;
    1091         composelevel = bddvar2level[var];
    1092         replaceid = (composelevel << 2) | CACHEID_COMPOSE;
    1093         res = compose_rec(f, g);
    1094         checkresize();
    1095     } catch (...) {
    1096         bdd_checkreorder();
    1097         bdd_disable_reorder();
    1098         res = bdd_compose(f, g, var);
    1099         bdd_enable_reorder();
    1100     }
    1101 
    1102     return res;
    1103 }
    1104 
    1105 
    1106 static BDD compose_rec(BDD f, BDD g)
    1107 {
    1108 
    1109     BDD res = BDDZERO;
    1110 
    1111     if (LEVEL(f) > composelevel)
    1112         return f;
    1113 
    1114     BddCacheData * entry = BddCache_lookup(&replacecache, COMPOSEHASH(f,g));
    1115     if (entry->a == f  &&  entry->b == g  &&  entry->c == replaceid)
    1116     {
    1117 #ifdef CACHESTATS
    1118         bddcachestats.opHit++;
    1119 #endif
    1120         return entry->r.res;
    1121     }
    1122 #ifdef CACHESTATS
    1123     bddcachestats.opMiss++;
    1124 #endif
    1125 
    1126     if (LEVEL(f) < composelevel)
    1127     {
    1128         if (LEVEL(f) == LEVEL(g))
    1129         {
    1130             PUSHREF( compose_rec(LOW(f), LOW(g)) );
    1131             PUSHREF( compose_rec(HIGH(f), HIGH(g)) );
    1132             res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    1133         }
    1134         else
    1135             if (LEVEL(f) < LEVEL(g))
    1136             {
     987    }
     988
     989    const int composelevel = bddvar2level[var];
     990    const int replaceid = (composelevel << 2) | CACHEID_COMPOSE;
     991
     992    std::function<BDD(const BDD, const BDD)> compose_rec = [&](const BDD f, const BDD g) -> BDD {
     993
     994        if (LEVEL(f) > composelevel)
     995            return f;
     996
     997        BddCacheData * entry = BddCache_lookup(&replacecache, COMPOSEHASH(f,g));
     998        if (entry->a == f  &&  entry->b == g  &&  entry->c == replaceid) {
     999            return entry->r.res;
     1000        }
     1001
     1002        BDD res = BDDZERO;
     1003
     1004        if (LEVEL(f) < composelevel) {
     1005            if (LEVEL(f) == LEVEL(g)) {
     1006                PUSHREF( compose_rec(LOW(f), LOW(g)) );
     1007                PUSHREF( compose_rec(HIGH(f), HIGH(g)) );
     1008                res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
     1009            } else if (LEVEL(f) < LEVEL(g)) {
    11371010                PUSHREF( compose_rec(LOW(f), g) );
    11381011                PUSHREF( compose_rec(HIGH(f), g) );
    11391012                res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    1140             }
    1141             else
    1142             {
     1013            } else {
    11431014                PUSHREF( compose_rec(f, LOW(g)) );
    11441015                PUSHREF( compose_rec(f, HIGH(g)) );
    11451016                res = bdd_makenode(LEVEL(g), READREF(2), READREF(1));
    11461017            }
    1147         POPREF(2);
    1148     }
    1149     else
    1150         /*if (LEVEL(f) == composelevel) changed 2-nov-98 */
    1151     {
    1152         res = ite_rec(g, HIGH(f), LOW(f));
    1153     }
    1154 
    1155     entry->a = f;
    1156     entry->b = g;
    1157     entry->c = replaceid;
    1158     entry->r.res = res;
     1018            POPREF(2);
     1019        } else {
     1020            res = bdd_ite(g, HIGH(f), LOW(f));
     1021        }
     1022
     1023        entry->a = f;
     1024        entry->b = g;
     1025        entry->c = replaceid;
     1026        entry->r.res = res;
     1027
     1028        return res;
     1029
     1030    };
     1031
     1032    BDD res = BDDZERO;
     1033    try {
     1034        INITREF;
     1035        res = compose_rec(f, g);
     1036    } catch (reordering_required) {
     1037        bdd_checkreorder();
     1038        bdd_disable_reorder();
     1039        INITREF;
     1040        res = compose_rec(f, g);
     1041        bdd_enable_reorder();
     1042    }
     1043    checkresize();
    11591044
    11601045    return res;
    11611046}
    1162 
    11631047
    11641048/*
     
    11861070    BDD res = BDDZERO;
    11871071
    1188     CHECKa(f, bdd_zero());
     1072    CHECK(f);
    11891073
    11901074    try {
     
    11951079        res = veccompose_rec(f);
    11961080        checkresize();
    1197     } catch (...) {
     1081    } catch (reordering_required) {
    11981082        bdd_checkreorder();
    11991083        bdd_disable_reorder();
     
    12101094    BDD res = BDDZERO;
    12111095
    1212     if (LEVEL(f) > replacelast)
     1096    if (LEVEL(f) > replacelast) {
    12131097        return f;
     1098    }
    12141099
    12151100    entry = BddCache_lookup(&replacecache, VECCOMPOSEHASH(f));
    1216     if (entry->a == f  &&  entry->c == replaceid)
    1217     {
    1218 #ifdef CACHESTATS
    1219         bddcachestats.opHit++;
    1220 #endif
     1101    if (entry->a == f  &&  entry->c == replaceid) {
    12211102        return entry->r.res;
    12221103    }
    1223 #ifdef CACHESTATS
    1224     bddcachestats.opMiss++;
    1225 #endif
    12261104
    12271105    PUSHREF( veccompose_rec(LOW(f)) );
    12281106    PUSHREF( veccompose_rec(HIGH(f)) );
    1229     res = ite_rec(replacepair[LEVEL(f)], READREF(1), READREF(2));
     1107    res = bdd_ite(replacepair[LEVEL(f)], READREF(1), READREF(2));
    12301108    POPREF(2);
    12311109
     
    12541132BDD bdd_simplify(BDD f, BDD d)
    12551133{
     1134    CHECK(f);
     1135    CHECK(d);
     1136
    12561137    BDD res = BDDZERO;
    1257 
    1258     CHECKa(f, bdd_zero());
    1259     CHECKa(d, bdd_zero());
    1260 
    12611138    try {
    12621139        INITREF;
    1263         applyop = bddop_or;
    12641140        res = simplify_rec(f, d);
    1265         checkresize();
    1266     } catch (...) {
     1141    } catch (reordering_required) {
    12671142        bdd_checkreorder();
    12681143        bdd_disable_reorder();
    1269         res = bdd_simplify(f, d);
     1144        res = simplify_rec(f, d);
    12701145        bdd_enable_reorder();
    12711146    }
     1147    checkresize();
    12721148
    12731149    return res;
     
    12751151
    12761152
    1277 static BDD simplify_rec(BDD f, BDD d)
    1278 {
    1279     BddCacheData *entry;
    1280     BDD res = BDDZERO;
    1281 
    1282     if (ISONE(d)  ||  ISCONST(f))
     1153static BDD simplify_rec(const BDD f, const BDD d) {
     1154
     1155    if (ISONE(d) || ISCONST(f))
    12831156        return f;
    12841157    if (d == f)
     
    12871160        return BDDZERO;
    12881161
    1289     entry = BddCache_lookup(&applycache, APPLYHASH(f,d,bddop_simplify));
    1290 
    1291     if (entry->a == f  &&  entry->b == d  &&  entry->c == bddop_simplify)
    1292     {
    1293 #ifdef CACHESTATS
    1294         bddcachestats.opHit++;
    1295 #endif
     1162    BddCacheData * entry = BddCache_lookup(&applycache, APPLYHASH(f, d, bddop_simplify));
     1163    if (entry->a == f  &&  entry->b == d  &&  entry->c == bddop_simplify) {
    12961164        return entry->r.res;
    12971165    }
    1298 #ifdef CACHESTATS
    1299     bddcachestats.opMiss++;
    1300 #endif
    1301 
    1302     if (LEVEL(f) == LEVEL(d))
    1303     {
    1304         if (ISZERO(LOW(d)))
     1166
     1167    BDD res = BDDZERO;
     1168
     1169    if (LEVEL(f) == LEVEL(d)) {
     1170        if (ISZERO(LOW(d))) {
    13051171            res = simplify_rec(HIGH(f), HIGH(d));
    1306         else
    1307             if (ISZERO(HIGH(d)))
    1308                 res = simplify_rec(LOW(f), LOW(d));
    1309             else
    1310             {
    1311                 PUSHREF( simplify_rec(LOW(f),   LOW(d)) );
    1312                 PUSHREF( simplify_rec(HIGH(f), HIGH(d)) );
    1313                 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    1314                 POPREF(2);
    1315             }
    1316     }
    1317     else
    1318         if (LEVEL(f) < LEVEL(d))
    1319         {
    1320             PUSHREF( simplify_rec(LOW(f), d) );
    1321             PUSHREF( simplify_rec(HIGH(f), d) );
     1172        } else if (ISZERO(HIGH(d))) {
     1173            res = simplify_rec(LOW(f), LOW(d));
     1174        } else {
     1175            PUSHREF( simplify_rec(LOW(f),       LOW(d)) );
     1176            PUSHREF( simplify_rec(HIGH(f), HIGH(d)) );
    13221177            res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
    13231178            POPREF(2);
    13241179        }
    1325         else /* LEVEL(d) < LEVEL(f) */
    1326         {
    1327             PUSHREF( apply_rec(LOW(d), HIGH(d)) ); /* Exist quant */
    1328             res = simplify_rec(f, READREF(1));
    1329             POPREF(1);
    1330         }
     1180    } else if (LEVEL(f) < LEVEL(d)) {
     1181        PUSHREF( simplify_rec(LOW(f), d) );
     1182        PUSHREF( simplify_rec(HIGH(f), d) );
     1183        res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
     1184        POPREF(2);
     1185    } else { // LEVEL(d) < LEVEL(f)
     1186        PUSHREF(bdd_apply(LOW(d), HIGH(d), bddop_or) ); /* Exist quant */
     1187        res = simplify_rec(f, READREF(1));
     1188        POPREF(1);
     1189    }
    13311190
    13321191    entry->a = f;
     
    13551214    BDD res = BDDZERO;
    13561215
    1357     CHECKa(r, bdd_zero());
    1358     CHECKa(var, bdd_zero());
     1216    CHECK(r);
     1217    CHECK(var);
    13591218
    13601219    if (var < 2)  /* Empty set */
     
    13691228        res = quant_rec(r);
    13701229        checkresize();
    1371     } catch (...) {
     1230    } catch (reordering_required) {
    13721231        bdd_checkreorder();
    13731232        bdd_disable_reorder();
     
    13941253    BDD res = BDDZERO;
    13951254
    1396     CHECKa(r, bdd_zero());
    1397     CHECKa(var, bdd_zero());
     1255    CHECK(r);
     1256    CHECK(var);
    13981257
    13991258    if (var < 2)  /* Empty set */
     
    14081267        res = quant_rec(r);
    14091268        checkresize();
    1410     } catch (...) {
     1269    } catch (reordering_required) {
    14111270        bdd_checkreorder();
    14121271        bdd_disable_reorder();
     
    14361295    BDD res = BDDZERO;
    14371296
    1438     CHECKa(r, bdd_zero());
    1439     CHECKa(var, bdd_zero());
     1297    CHECK(r);
     1298    CHECK(var);
    14401299
    14411300    if (var < 2)  /* Empty set */
     
    14501309        res = quant_rec(r);
    14511310        checkresize();
    1452     } catch (...) {
     1311    } catch (reordering_required) {
    14531312        bdd_checkreorder();
    14541313        bdd_disable_reorder();
     
    14611320
    14621321
    1463 static int quant_rec(int r)
    1464 {
    1465     BddCacheData *entry;
     1322static int quant_rec(int r) {
    14661323    int res;
    14671324
     
    14691326        return r;
    14701327
    1471     entry = BddCache_lookup(&quantcache, QUANTHASH(r));
    1472     if (entry->a == r  &&  entry->c == quantid)
    1473     {
    1474 #ifdef CACHESTATS
    1475         bddcachestats.opHit++;
    1476 #endif
     1328    BddCacheData * entry = BddCache_lookup(&quantcache, QUANTHASH(r));
     1329    if (entry->a == r  &&  entry->c == quantid) {
    14771330        return entry->r.res;
    14781331    }
    1479 #ifdef CACHESTATS
    1480     bddcachestats.opMiss++;
    1481 #endif
    14821332
    14831333    PUSHREF( quant_rec(LOW(r)) );
     
    14851335
    14861336    if (INVARSET(LEVEL(r)))
    1487         res = apply_rec(READREF(2), READREF(1));
     1337        res = bdd_apply(READREF(2), READREF(1), applyop);
    14881338    else
    14891339        res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
     
    15231373    BDD res = BDDZERO;
    15241374
    1525     CHECKa(l, bdd_zero());
    1526     CHECKa(r, bdd_zero());
    1527     CHECKa(var, bdd_zero());
    1528 
    1529     if (opr<0 || opr>bddop_invimp) {
     1375    CHECK(l);
     1376    CHECK(r);
     1377    CHECK(var);
     1378
     1379    if (UNLIKELY(opr < 0 || opr > bddop_invimp)) {
    15301380        bdd_error(BDD_OP);
    1531         return bdd_zero();
    15321381    }
    15331382
     
    15451394        res = appquant_rec(l, r);
    15461395        checkresize();
    1547     } catch (...) {
     1396    } catch (reordering_required) {
    15481397        bdd_checkreorder();
    15491398        bdd_disable_reorder();
     
    15761425    BDD res = BDDZERO;
    15771426
    1578     CHECKa(l, bdd_zero());
    1579     CHECKa(r, bdd_zero());
    1580     CHECKa(var, bdd_zero());
    1581 
    1582     if (opr<0 || opr>bddop_invimp)
    1583     {
     1427    CHECK(l);
     1428    CHECK(r);
     1429    CHECK(var);
     1430
     1431    if (UNLIKELY(opr < 0 || opr > bddop_invimp)) {
    15841432        bdd_error(BDD_OP);
    1585         return bdd_zero();
    15861433    }
    15871434
     
    15991446        res = appquant_rec(l, r);
    16001447        checkresize();
    1601     } catch (...) {
     1448    } catch (reordering_required) {
    16021449        bdd_checkreorder();
    16031450        bdd_disable_reorder();
     
    16301477    BDD res = BDDZERO;
    16311478
    1632     CHECKa(l, bdd_zero());
    1633     CHECKa(r, bdd_zero());
    1634     CHECKa(var, bdd_zero());
    1635 
    1636     if (opr<0 || opr>bddop_invimp)
    1637     {
     1479    CHECK(l);
     1480    CHECK(r);
     1481    CHECK(var);
     1482
     1483    if (UNLIKELY(opr < 0 || opr > bddop_invimp)) {
    16381484        bdd_error(BDD_OP);
    1639         return bdd_zero();
    16401485    }
    16411486
    16421487    if (var < 2)  /* Empty set */
    1643         return bdd_apply(l,r,opr);
     1488        return bdd_apply(l, r, opr);
    16441489
    16451490    try {
     
    16531498        res = appquant_rec(l, r);
    16541499        checkresize();
    1655     } catch (...) {
     1500    } catch (reordering_required) {
    16561501        bdd_checkreorder();
    16571502        bdd_disable_reorder();
     
    16641509
    16651510
    1666 static int appquant_rec(int l, int r)
    1667 {
    1668     BddCacheData *entry;
     1511static int appquant_rec(int l, int r) {
    16691512    int res;
    16701513
    1671     switch (appexop)
    1672     {
     1514    switch (appexop) {
    16731515    case bddop_and:
    16741516        if (l == 0  ||  r == 0)
     
    17141556        if (LEVEL(l) > quantlast  &&  LEVEL(r) > quantlast)
    17151557        {
    1716             int oldop = applyop;
    1717             applyop = appexop;
    1718             res = apply_rec(l,r);
     1558            const int oldop = applyop;
     1559            res = bdd_apply(l, r, appexop);
    17191560            applyop = oldop;
    17201561        }
    17211562        else
    17221563        {
    1723             entry = BddCache_lookup(&appexcache, APPEXHASH(l,r,appexop));
    1724             if (entry->a == l  &&  entry->b == r  &&  entry->c == appexid)
    1725             {
    1726 #ifdef CACHESTATS
    1727                 bddcachestats.opHit++;
    1728 #endif
     1564            BddCacheData * entry = BddCache_lookup(&appexcache, APPEXHASH(l,r,appexop));
     1565            if (entry->a == l  &&  entry->b == r  &&  entry->c == appexid) {
    17291566                return entry->r.res;
    17301567            }
    1731 #ifdef CACHESTATS
    1732             bddcachestats.opMiss++;
    1733 #endif
    17341568
    17351569            if (LEVEL(l) == LEVEL(r))
     
    17381572                PUSHREF( appquant_rec(HIGH(l), HIGH(r)) );
    17391573                if (INVARSET(LEVEL(l)))
    1740                     res = apply_rec(READREF(2), READREF(1));
     1574                    res = bdd_apply(READREF(2), READREF(1), applyop);
    17411575                else
    17421576                    res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
     
    17481582                    PUSHREF( appquant_rec(HIGH(l), r) );
    17491583                    if (INVARSET(LEVEL(l)))
    1750                         res = apply_rec(READREF(2), READREF(1));
     1584                        res = bdd_apply(READREF(2), READREF(1), applyop);
    17511585                    else
    17521586                        res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
     
    17571591                    PUSHREF( appquant_rec(l, HIGH(r)) );
    17581592                    if (INVARSET(LEVEL(r)))
    1759                         res = apply_rec(READREF(2), READREF(1));
     1593                        res = bdd_apply(READREF(2), READREF(1), applyop);
    17601594                    else
    17611595                        res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
     
    17961630    int res=1;
    17971631
    1798     CHECKa(r, bdd_zero());
     1632    CHECK(r);
    17991633
    18001634    if (r < 2)
     
    18041638    if (supportSize < bddvarnum)
    18051639    {
    1806         if ((supportSet=(int*)malloc(bddvarnum*sizeof(int))) == NULL)
    1807         {
     1640        if ((supportSet=(int*)malloc(bddvarnum*sizeof(int))) == nullptr) {
    18081641            bdd_error(BDD_MEMORY);
    1809             return bdd_zero();
    18101642        }
    18111643        memset(supportSet, 0, bddvarnum*sizeof(int));
     
    18531685static void support_rec(int r, int* support)
    18541686{
    1855     BddNode *node;
    1856 
    18571687    if (r < 2)
    18581688        return;
    18591689
    1860     node = &bddnodes[r];
    1861     if (LEVELp(node) & MARKON  ||  LOWp(node) == -1)
     1690    BddNode * node = &bddnodes[r];
     1691    if (MARKED(node)  ||  LOW(node) == -1)
    18621692        return;
    18631693
    1864     support[LEVELp(node)] = supportID;
    1865 
    1866     if (LEVELp(node) > supportMax)
    1867         supportMax = LEVELp(node);
    1868 
    1869     LEVELp(node) |= MARKON;
    1870 
    1871     support_rec(LOWp(node), support);
    1872     support_rec(HIGHp(node), support);
     1694    support[LEVEL(node)] = supportID;
     1695
     1696    if (LEVEL(node) > supportMax)
     1697        supportMax = LEVEL(node);
     1698
     1699    SETMARK(node);
     1700
     1701    support_rec(LOW(node), support);
     1702    support_rec(HIGH(node), support);
    18731703}
    18741704
     
    18911721    BDD res = BDDZERO;
    18921722
    1893     CHECKa(r, bdd_zero());
     1723    CHECK(r);
    18941724    if (r < 2)
    18951725        return r;
     
    19441774    BDD res = BDDZERO;
    19451775
    1946     CHECKa(r, bdd_zero());
     1776    CHECK(r);
    19471777    if (ISZERO(r))
    19481778        return r;
    1949     if (!ISCONST(pol))
    1950     {
     1779    if (!ISCONST(pol)) {
    19511780        bdd_error(BDD_ILLBDD);
    1952         return bdd_zero();
    19531781    }
    19541782
     
    20271855    int v;
    20281856
    2029     CHECKa(r, bdd_zero());
     1857    CHECK(r);
    20301858    if (r == 0)
    20311859        return 0;
     
    21181946    int v;
    21191947
    2120     CHECKn(r);
    2121 
    2122     if ((allsatProfile=(char*)malloc(bddvarnum)) == NULL)
    2123     {
     1948    CHECK(r);
     1949
     1950    if ((allsatProfile=(char*)malloc(bddvarnum)) == nullptr) {
    21241951        bdd_error(BDD_MEMORY);
    2125         return;
    21261952    }
    21271953
     
    22012027    double size=1;
    22022028
    2203     CHECKa(r, 0.0);
     2029    CHECK(r);
    22042030
    22052031    miscid = CACHEID_SATCOU;
     
    22442070    s = 1;
    22452071
    2246     s *= pow(2.0, (float)(LEVEL(LOWp(node)) - LEVELp(node) - 1));
    2247     size += s * satcount_rec(LOWp(node));
     2072    s *= pow(2.0, (float)(LEVEL(LOW(node)) - LEVEL(node) - 1));
     2073    size += s * satcount_rec(LOW(node));
    22482074
    22492075    s = 1;
    2250     s *= pow(2.0, (float)(LEVEL(HIGHp(node)) - LEVELp(node) - 1));
    2251     size += s * satcount_rec(HIGHp(node));
     2076    s *= pow(2.0, (float)(LEVEL(HIGH(node)) - LEVEL(node) - 1));
     2077    size += s * satcount_rec(HIGH(node));
    22522078
    22532079    entry->a = root;
     
    22822108    double size;
    22832109
    2284     CHECKa(r, 0.0);
     2110    CHECK(r);
    22852111
    22862112    miscid = CACHEID_SATCOULN;
     
    23282154    node = &bddnodes[root];
    23292155
    2330     s1 = satcountln_rec(LOWp(node));
     2156    s1 = satcountln_rec(LOW(node));
    23312157    if (s1 >= 0.0)
    2332         s1 += LEVEL(LOWp(node)) - LEVELp(node) - 1;
    2333 
    2334     s2 = satcountln_rec(HIGHp(node));
     2158        s1 += LEVEL(LOW(node)) - LEVEL(node) - 1;
     2159
     2160    s2 = satcountln_rec(HIGH(node));
    23352161    if (s2 >= 0.0)
    2336         s2 += LEVEL(HIGHp(node)) - LEVELp(node) - 1;
     2162        s2 += LEVEL(HIGH(node)) - LEVEL(node) - 1;
    23372163
    23382164    if (s1 < 0.0)
     
    24172243       variable occured in the BDD. It is the users responsibility to
    24182244       free the array again using a call to {\tt free}. *}
    2419 RETURN  {* A pointer to an integer array with the profile or NULL if an
     2245RETURN  {* A pointer to an integer array with the profile or nullptr if an
    24202246           error occured. *}
    24212247*/
    24222248int *bdd_varprofile(BDD r)
    24232249{
    2424     CHECKa(r, NULL);
    2425 
    2426     if ((varprofile=(int*)malloc(sizeof(int)*bddvarnum)) == NULL)
    2427     {
     2250    CHECK(r);
     2251
     2252    if ((varprofile=(int*)malloc(sizeof(int)*bddvarnum)) == nullptr) {
    24282253        bdd_error(BDD_MEMORY);
    2429         return NULL;
    24302254    }
    24312255
     
    24452269
    24462270    node = &bddnodes[r];
    2447     if (LEVELp(node) & MARKON)
     2271    if (MARKED(node))
    24482272        return;
    24492273
    2450     varprofile[bddlevel2var[LEVELp(node)]]++;
    2451     LEVELp(node) |= MARKON;
    2452 
    2453     varprofile_rec(LOWp(node));
    2454     varprofile_rec(HIGHp(node));
     2274    varprofile[bddlevel2var[LEVEL(node)]]++;
     2275    SETMARK(node);
     2276
     2277    varprofile_rec(LOW(node));
     2278    varprofile_rec(HIGH(node));
    24552279}
    24562280
     
    24702294double bdd_pathcount(BDD r)
    24712295{
    2472     CHECKa(r, 0.0);
     2296    CHECK(r);
    24732297
    24742298    miscid = CACHEID_PATHCOU;
     
    25112335
    25122336    if (r < 2)
    2513         return bdd_error(BDD_VARSET);
     2337        bdd_error(BDD_VARSET);
    25142338
    25152339    quantvarsetID++;
     
    25362360
    25372361    if (r < 2)
    2538         return bdd_error(BDD_VARSET);
     2362        bdd_error(BDD_VARSET);
    25392363
    25402364    quantvarsetID++;
     
    25632387    return 0;
    25642388}
    2565 
    2566 
    2567 /* EOF */
  • icGREP/icgrep-devel/buddy-2.4/src/cache.cpp

    r4867 r4938  
    4949    size = bdd_prime_gte(size);
    5050
    51     if ((cache->table=NEW(BddCacheData,size)) == NULL)
    52         return bdd_error(BDD_MEMORY);
     51    if ((cache->table=NEW(BddCacheData,size)) == nullptr)
     52        bdd_error(BDD_MEMORY);
    5353
    5454    for (n=0 ; n<size ; n++)
     
    6363{
    6464    free(cache->table);
    65     cache->table = NULL;
     65    cache->table = nullptr;
    6666    cache->tablesize = 0;
    6767}
     
    7676    newsize = bdd_prime_gte(newsize);
    7777
    78     if ((cache->table=NEW(BddCacheData,newsize)) == NULL)
    79         return bdd_error(BDD_MEMORY);
     78    if ((cache->table=NEW(BddCacheData,newsize)) == nullptr)
     79        bdd_error(BDD_MEMORY);
    8080
    8181    for (n=0 ; n<newsize ; n++)
  • icGREP/icgrep-devel/buddy-2.4/src/imatrix.cpp

    r4867 r4938  
    4949
    5050    if (!mtx)
    51         return NULL;
     51        return nullptr;
    5252
    53     if ((mtx->rows=NEW(char*,size)) == NULL)
     53    if ((mtx->rows=NEW(char*,size)) == nullptr)
    5454    {
    5555        free(mtx);
    56         return NULL;
     56        return nullptr;
    5757    }
    5858
    5959    for (n=0 ; n<size ; n++)
    6060    {
    61         if ((mtx->rows[n]=NEW(char,size/8+1)) == NULL)
     61        if ((mtx->rows[n]=NEW(char,size/8+1)) == nullptr)
    6262        {
    6363            for (m=0 ; m<n ; m++)
    6464                free(mtx->rows[m]);
    6565            free(mtx);
    66             return NULL;
     66            return nullptr;
    6767        }
    6868
  • icGREP/icgrep-devel/buddy-2.4/src/kernel.cpp

    r4928 r4938  
    6464
    6565int          bddrunning;            /* Flag - package initialized */
    66 int          bdderrorcond;          /* Some error condition */
    6766int          bddnodesize;           /* Number of allocated nodes */
    6867int          bddmaxnodesize;        /* Maximum allowed number of nodes */
     
    7978int          bddresized;        /* Flag indicating a resize of the nodetable */
    8079
    81 bddCacheStat bddcachestats;
    82 
    83 
    8480/*=== PRIVATE KERNEL VARIABLES =========================================*/
    8581
     
    9086static int      usednodes_nextreorder; /* When to do reorder next time */
    9187static bddinthandler  err_handler;     /* Error handler */
    92 static bddgbchandler  gbc_handler;     /* Garbage collection handler */
    9388static bdd2inthandler resize_handler;  /* Node-table-resize handler */
    9489
     
    131126
    132127    if (bddrunning)
    133         return bdd_error(BDD_RUNNING);
     128        bdd_error(BDD_RUNNING);
    134129
    135130    bddnodesize = bdd_prime_gte(initnodesize);
    136131
    137     if ((bddnodes=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == NULL) {
    138         return bdd_error(BDD_MEMORY);
     132    if ((bddnodes=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == nullptr) {
     133        bdd_error(BDD_MEMORY);
    139134    }
    140135
    141136    bddresized = 0;
    142137
    143     for (unsigned n = 0 ; n != bddnodesize ; n++)
    144     {
    145         bddnodes[n].refcou = 0;
    146         LOW(n) = -1;
    147         bddnodes[n].hash = 0;
    148         LEVEL(n) = 0;
    149         bddnodes[n].next = n+1;
    150     }
    151     bddnodes[bddnodesize-1].next = 0;
    152 
    153     bddnodes[0].refcou = bddnodes[1].refcou = MAXREF;
    154     LOW(0) = HIGH(0) = 0;
    155     LOW(1) = HIGH(1) = 1;
     138    for (unsigned i = 0 ; i != 2 ; ++i) {
     139        BddNode & n = bddnodes[i];
     140        n.refcount = MAXREF;
     141        n.level = 0;
     142        n.low = i;
     143        n.high = i;
     144        n.hash = 0;
     145        n.next = i + 1;
     146    }
     147    for (unsigned i = 2; i != bddnodesize ; ++i) {
     148        BddNode & n = bddnodes[i];
     149        n.refcount = 0;
     150        n.level = 0;
     151        n.low = -1;
     152        n.high = -1;
     153        n.hash = 0;
     154        n.next = i + 1;
     155    }
     156    bddnodes[bddnodesize - 1].next = 0;
    156157
    157158    const auto err = bdd_operator_init(cs);
     
    171172    bddmaxnodeincrease = DEFAULTMAXNODEINC;
    172173
    173     bdderrorcond = 0;
    174 
    175     bddcachestats.uniqueAccess = 0;
    176     bddcachestats.uniqueChain = 0;
    177     bddcachestats.uniqueHit = 0;
    178     bddcachestats.uniqueMiss = 0;
    179     bddcachestats.opHit = 0;
    180     bddcachestats.opMiss = 0;
    181     bddcachestats.swapCount = 0;
    182 
    183     bdd_error_hook(bdd_default_errhandler);
    184     bdd_gbc_hook(nullptr);
    185174    bdd_resize_hook(nullptr);
    186175    bdd_pairs_init();
    187176    bdd_reorder_init();
    188 //    bdd_fdd_init();
    189177
    190178    return 0;
    191179}
    192180
    193 void bdd_default_errhandler(int e) {
    194     throw std::runtime_error("BDD error: " + bdd_errstring(e));
    195 }
    196181
    197182/*
     
    217202    free(bddlevel2var);
    218203
    219     bddnodes = NULL;
    220     bddrefstack = NULL;
    221     bddvarset = NULL;
     204    bddnodes = nullptr;
     205    bddrefstack = nullptr;
     206    bddvarset = nullptr;
    222207
    223208    bdd_operator_done();
     
    229214    bddproduced = 0;
    230215
    231     err_handler = NULL;
    232     gbc_handler = NULL;
    233     resize_handler = NULL;
     216    err_handler = nullptr;
     217    resize_handler = nullptr;
    234218}
    235219
     
    261245
    262246    if (num < bddvarnum)
    263         return bdd_error(BDD_DECVNUM);
     247        bdd_error(BDD_DECVNUM);
    264248    if (num == bddvarnum)
    265249        return 0;
    266250
    267     if (bddvarset == NULL)
     251    if (bddvarset == nullptr)
    268252    {
    269         if ((bddvarset=(BDD*)malloc(sizeof(BDD)*num*2)) == NULL)
    270             return bdd_error(BDD_MEMORY);
    271         if ((bddlevel2var=(int*)malloc(sizeof(int)*(num+1))) == NULL)
     253        if ((bddvarset=(BDD*)malloc(sizeof(BDD)*num*2)) == nullptr)
     254            bdd_error(BDD_MEMORY);
     255        if ((bddlevel2var=(int*)malloc(sizeof(int)*(num+1))) == nullptr)
    272256        {
    273257            free(bddvarset);
    274             return bdd_error(BDD_MEMORY);
    275         }
    276         if ((bddvar2level=(int*)malloc(sizeof(int)*(num+1))) == NULL)
     258            bdd_error(BDD_MEMORY);
     259        }
     260        if ((bddvar2level=(int*)malloc(sizeof(int)*(num+1))) == nullptr)
    277261        {
    278262            free(bddvarset);
    279263            free(bddlevel2var);
    280             return bdd_error(BDD_MEMORY);
     264            bdd_error(BDD_MEMORY);
    281265        }
    282266    }
    283267    else
    284268    {
    285         if ((bddvarset=(BDD*)realloc(bddvarset,sizeof(BDD)*num*2)) == NULL)
    286             return bdd_error(BDD_MEMORY);
    287         if ((bddlevel2var=(int*)realloc(bddlevel2var,sizeof(int)*(num+1))) == NULL)
     269        if ((bddvarset=(BDD*)realloc(bddvarset,sizeof(BDD)*num*2)) == nullptr)
     270            bdd_error(BDD_MEMORY);
     271        if ((bddlevel2var=(int*)realloc(bddlevel2var,sizeof(int)*(num+1))) == nullptr)
    288272        {
    289273            free(bddvarset);
    290             return bdd_error(BDD_MEMORY);
    291         }
    292         if ((bddvar2level=(int*)realloc(bddvar2level,sizeof(int)*(num+1))) == NULL)
     274            bdd_error(BDD_MEMORY);
     275        }
     276        if ((bddvar2level=(int*)realloc(bddvar2level,sizeof(int)*(num+1))) == nullptr)
    293277        {
    294278            free(bddvarset);
    295279            free(bddlevel2var);
    296             return bdd_error(BDD_MEMORY);
    297         }
    298     }
    299 
    300     if (bddrefstack != NULL)
     280            bdd_error(BDD_MEMORY);
     281        }
     282    }
     283
     284    if (bddrefstack != nullptr)
    301285        free(bddrefstack);
    302286    bddrefstack = bddrefstacktop = (int*)malloc(sizeof(int)*(num*2+4));
     
    308292        POPREF(1);
    309293
    310         if (bdderrorcond)
    311         {
    312             bddvarnum = bdv;
    313             return -bdderrorcond;
    314         }
    315 
    316         bddnodes[bddvarset[bddvarnum*2]].refcou = MAXREF;
    317         bddnodes[bddvarset[bddvarnum*2+1]].refcou = MAXREF;
     294        bddnodes[bddvarset[bddvarnum*2]].refcount = MAXREF;
     295        bddnodes[bddvarset[bddvarnum*2+1]].refcount = MAXREF;
    318296        bddlevel2var[bddvarnum] = bddvarnum;
    319297        bddvar2level[bddvarnum] = bddvarnum;
    320298    }
    321299
    322     LEVEL(0) = num;
    323     LEVEL(1) = num;
     300    bddnodes[0].level = num;
     301    bddnodes[1].level = num;
    324302    bddvar2level[num] = num;
    325303    bddlevel2var[num] = num;
     
    349327
    350328    if (num < 0  ||  num > 0x3FFFFFFF)
    351         return bdd_error(BDD_RANGE);
     329        bdd_error(BDD_RANGE);
    352330
    353331    bdd_setvarnum(bddvarnum+num);
    354332    return start;
    355333}
    356 
    357 
    358 /*
    359 NAME  {* bdd\_error\_hook *}
    360 SECTION {* kernel *}
    361 SHORT {* set a handler for error conditions *}
    362 PROTO {* bddinthandler bdd_error_hook(bddinthandler handler) *}
    363 DESCR {* Whenever an error occurs in the bdd package a test is done to
    364         see if an error handler is supplied by the user and if such exists
    365     then it will be called
    366     with an error code in the variable {\tt errcode}. The handler may
    367     then print any usefull information and return or exit afterwards.
    368 
    369     This function sets the handler to be {\tt handler}. If a {\tt NULL}
    370     argument is supplied then no calls are made when an error occurs.
    371     Possible error codes are found in {\tt bdd.h}. The default handler
    372     is {\tt bdd\_default\_errhandler} which will use {\tt exit()} to
    373     terminate the program.
    374 
    375     Any handler should be defined like this:
    376     \begin{verbatim}
    377 void my_error_handler(int errcode)
    378 {
    379    ...
    380 }
    381 \end{verbatim} *}
    382 RETURN {* The previous handler *}
    383 ALSO  {* bdd\_errstring *}
    384 */
    385 bddinthandler bdd_error_hook(bddinthandler handler)
    386 {
    387     bddinthandler tmp = err_handler;
    388     err_handler = handler;
    389     return tmp;
    390 }
    391 
    392 
    393 /*
    394 NAME    {* bdd\_clear\_error *}
    395 SECTION {* kernel *}
    396 SHORT   {* clears an error condition in the kernel *}
    397 PROTO   {* void bdd_clear_error(void) *}
    398 DESCR   {* The BuDDy kernel may at some point run out of new ROBDD nodes if
    399            a maximum limit is set with {\tt bdd\_setmaxnodenum}. In this case
    400        the current error handler is called and an internal error flag
    401        is set. Further calls to BuDDy will always return {\tt bdd_false()}.
    402        From here BuDDy must either be restarted or {\tt bdd\_clear\_error}
    403        may be called after action is taken to let BuDDy continue. This may
    404        not be especially usefull since the default error handler exits
    405        the program - other needs may of course exist.*}
    406 ALSO    {* bdd\_error\_hook, bdd\_setmaxnodenum *}
    407 */
    408 void bdd_clear_error(void)
    409 {
    410     bdderrorcond = 0;
    411     bdd_operator_reset();
    412 }
    413 
    414 
    415 /*
    416 NAME  {* bdd\_gbc\_hook *}
    417 SECTION {* kernel *}
    418 SHORT {* set a handler for garbage collections *}
    419 PROTO {* bddgbchandler bdd_gbc_hook(bddgbchandler handler) *}
    420 DESCR {* Whenever a garbage collection is required, a test is done to
    421          see if a handler for this event is supplied by the user and if such
    422      exists then it is called, both before and after the garbage collection
    423      takes places. This is indicated by an integer flag {\tt pre} passed to
    424      the handler, which will be one before garbage collection and zero
    425      after garbage collection.
    426 
    427      This function sets the handler to be {\tt handler}. If a {\tt
    428      NULL} argument is supplied then no calls are made when a
    429      garbage collection takes place. The argument {\tt pre}
    430      indicates pre vs. post garbage collection and the argument
    431      {\tt stat} contains information about the garbage
    432      collection. The default handler is {\tt bdd\_default\_gbchandler}.
    433 
    434      Any handler should be defined like this:
    435      \begin{verbatim}
    436 void my_gbc_handler(int pre, bddGbcStat *stat)
    437 {
    438    ...
    439 }
    440 \end{verbatim} *}
    441 RETURN {* The previous handler *}
    442 ALSO {* bdd\_resize\_hook, bdd\_reorder\_hook *} */
    443 bddgbchandler bdd_gbc_hook(bddgbchandler handler)
    444 {
    445     bddgbchandler tmp = gbc_handler;
    446     gbc_handler = handler;
    447     return tmp;
    448 }
    449 
    450334
    451335/*
     
    460344     {\tt newsize} being the new nodetable size.
    461345
    462      This function sets the handler to be {\tt handler}. If a {\tt NULL}
     346     This function sets the handler to be {\tt handler}. If a {\tt nullptr}
    463347     argument is supplied then no calls are made when a table resize
    464348     is done. No default handler is supplied.
     
    499383
    500384    if (size < 0)
    501         return bdd_error(BDD_SIZE);
     385        bdd_error(BDD_SIZE);
    502386
    503387    bddmaxnodeincrease = size;
     
    524408int bdd_setmaxnodenum(int size)
    525409{
    526     if (size > bddnodesize  ||  size == 0)
    527     {
     410    if (size > bddnodesize || size == 0) {
    528411        int old = bddmaxnodesize;
    529412        bddmaxnodesize = size;
     
    531414    }
    532415
    533     return bdd_error(BDD_NODES);
     416    bdd_error(BDD_NODES);
     417    return bddmaxnodesize;
    534418}
    535419
     
    558442
    559443    if (mf<0 || mf>100)
    560         return bdd_error(BDD_RANGE);
     444        bdd_error(BDD_RANGE);
    561445
    562446    minfreenodes = mf;
     
    577461ALSO    {* bdd\_getallocnum, bdd\_setmaxnodenum *}
    578462*/
    579 int bdd_getnodenum(void)
    580 {
     463int bdd_getnodenum(void) {
    581464    return bddnodesize - bddfreenum;
    582465}
     
    593476ALSO    {* bdd\_getnodenum, bdd\_setmaxnodenum *}
    594477*/
    595 int bdd_getallocnum(void)
    596 {
     478int bdd_getallocnum(void) {
    597479    return bddnodesize;
    598480}
     
    609491ALSO    {* bdd\_init, bdd\_done *}
    610492*/
    611 int bdd_isrunning(void)
    612 {
     493int bdd_isrunning(void) {
    613494    return bddrunning;
    614495}
    615 
    616 /*
    617 NAME    {* bdd\_stats *}
    618 SECTION {* kernel *}
    619 SHORT   {* returns some status information about the bdd package *}
    620 PROTO   {* void bdd_stats(bddStat* stat) *}
    621 DESCR   {* This function acquires information about the internal state of
    622            the bdd package. The status information is written into the
    623        {\tt stat} argument. *}
    624 ALSO    {* bddStat *}
    625 */
    626 void bdd_stats(bddStat *s)
    627 {
    628     s->produced = bddproduced;
    629     s->nodenum = bddnodesize;
    630     s->maxnodenum = bddmaxnodesize;
    631     s->freenodes = bddfreenum;
    632     s->minfreenodes = minfreenodes;
    633     s->varnum = bddvarnum;
    634     s->cachesize = cachesize;
    635     s->gbcnum = gbcollectnum;
    636 }
    637 
    638 
    639 
    640 /*
    641 NAME    {* bdd\_cachestats *}
    642 SECTION {* kernel *}
    643 SHORT   {* Fetch cache access usage *}
    644 PROTO   {* void bdd_cachestats(bddCacheStat *s) *}
    645 DESCR   {* Fetches cache usage information and stores it in {\tt s}. The
    646            fields of {\tt s} can be found in the documentaion for
    647        {\tt bddCacheStat}. This function may or may not be compiled
    648        into the BuDDy package - depending on the setup at compile
    649        time of BuDDy. *}
    650 ALSO    {* bddCacheStat, bdd\_printstat *}
    651 */
    652 void bdd_cachestats(bddCacheStat *s)
    653 {
    654     *s = bddcachestats;
    655 }
    656 
    657 
    658 /*
    659 NAME    {* bdd\_printstat *}
    660 EXTRA   {* bdd\_fprintstat *}
    661 SECTION {* kernel *}
    662 SHORT   {* print cache statistics *}
    663 PROTO   {* void bdd_printstat(void)
    664 void bdd_fprintstat(FILE *ofile) *}
    665 DESCR   {* Prints information about the cache performance on standard output
    666            (or the supplied file). The information contains the number of
    667        accesses to the unique node table, the number of times a node
    668        was (not) found there and how many times a hash chain had to
    669        traversed. Hit and miss count is also given for the operator
    670        caches. *}
    671 ALSO    {* bddCacheStat, bdd\_cachestats *}
    672 */
    673 void bdd_fprintstat(FILE *ofile)
    674 {
    675     bddCacheStat s;
    676     bdd_cachestats(&s);
    677 
    678     fprintf(ofile, "\nCache statistics\n");
    679     fprintf(ofile, "----------------\n");
    680 
    681     fprintf(ofile, "Unique Access:  %ld\n", s.uniqueAccess);
    682     fprintf(ofile, "Unique Chain:   %ld\n", s.uniqueChain);
    683     fprintf(ofile, "Unique Hit:     %ld\n", s.uniqueHit);
    684     fprintf(ofile, "Unique Miss:    %ld\n", s.uniqueMiss);
    685     fprintf(ofile, "=> Hit rate =   %.2f\n",
    686             (s.uniqueHit+s.uniqueMiss > 0) ?
    687                 ((float)s.uniqueHit)/((float)s.uniqueHit+s.uniqueMiss) : 0);
    688     fprintf(ofile, "Operator Hits:  %ld\n", s.opHit);
    689     fprintf(ofile, "Operator Miss:  %ld\n", s.opMiss);
    690     fprintf(ofile, "=> Hit rate =   %.2f\n",
    691             (s.opHit+s.opMiss > 0) ?
    692                 ((float)s.opHit)/((float)s.opHit+s.opMiss) : 0);
    693     fprintf(ofile, "Swap count =    %ld\n", s.swapCount);
    694 }
    695 
    696 
    697 void bdd_printstat(void)
    698 {
    699     bdd_fprintstat(stdout);
    700 }
    701 
    702496
    703497/*************************************************************************
     
    705499*************************************************************************/
    706500
    707 /*
    708 NAME    {* bdd\_errstring *}
    709 SECTION {* kernel *}
    710 SHORT   {* converts an error code to a string*}
    711 PROTO   {* const char *bdd_errstring(int errorcode) *}
    712 DESCR   {* Converts a negative error code {\tt errorcode} to a descriptive
    713            string that can be used for error handling. *}
    714 RETURN  {* An error description string if {\tt e} is known, otherwise {\tt NULL}. *}
    715 ALSO    {* bdd\_err\_hook *}
    716 */
    717 std::string bdd_errstring(const int code) {
    718 
    719     unsigned e = -code;
    720 
    721     if (e < 1 || e > BDD_ERRNUM)
    722         return "unknown error code: " + std::to_string(e);
    723 
    724     /* Strings for all error mesages */
    725     static std::string errorstrings[BDD_ERRNUM] = {
    726         "Out of memory", "Unknown variable", "Value out of range",
    727         "Unknown BDD root dereferenced", "bdd_init() called twice",
    728         "File operation failed", "Incorrect file format",
    729         "Variables not in ascending order", "User called break",
    730         "Mismatch in size of variable sets",
    731         "Cannot allocate fewer nodes than already in use",
    732         "Unknown operator", "Illegal variable set",
    733         "Bad variable block operation",
    734         "Trying to decrease the number of variables",
    735         "Trying to replace with variables already in the bdd",
    736         "Number of nodes reached user defined maximum",
    737         "Unknown BDD - was not in node table",
    738         "Bad size argument",
    739         "Mismatch in bitvector size",
    740         "Illegal shift-left/right parameter",
    741         "Division by zero"
    742     };
    743 
    744     return errorstrings[e - 1];
    745 }
    746 
    747 int bdd_error(int e)
    748 {
    749     if (err_handler != NULL)
    750         err_handler(e);
    751 
    752     return e;
    753 }
    754 
     501void bdd_error(const unsigned code) {
     502    if (code >= BDD_ERRNUM) {
     503        throw std::runtime_error("Unknown error " + std::to_string(code));
     504    } else {
     505        static std::string errorstrings[BDD_ERRNUM] = {
     506            "Out of memory", "Unknown variable", "Value out of range",
     507            "Unknown BDD root dereferenced", "bdd_init() called twice",
     508            "File operation failed", "Incorrect file format",
     509            "Variables not in ascending order", "User called break",
     510            "Mismatch in size of variable sets",
     511            "Cannot allocate fewer nodes than already in use",
     512            "Unknown operator", "Illegal variable set",
     513            "Bad variable block operation",
     514            "Trying to decrease the number of variables",
     515            "Trying to replace with variables already in the bdd",
     516            "Number of nodes reached user defined maximum",
     517            "Unknown BDD - was not in node table",
     518            "Bad size argument",
     519            "Mismatch in bitvector size",
     520            "Illegal shift-left/right parameter",
     521            "Division by zero"
     522        };
     523        throw std::runtime_error(errorstrings[code]);
     524    }
     525}
    755526
    756527/*************************************************************************
     
    775546RETURN  {* The I'th variable on succes, otherwise the constant false bdd *}
    776547ALSO {* bdd\_setvarnum, bdd\_nithvar, bdd_true(), bdd_false() *} */
    777 BDD bdd_ithvar(int var)
    778 {
    779     if (var < 0  ||  var >= bddvarnum)
    780     {
     548BDD bdd_ithvar(int var) {
     549    if (UNLIKELY(var < 0 || var >= bddvarnum)) {
    781550        bdd_error(BDD_VAR);
    782         return bdd_zero();
    783     }
    784 
    785     return bddvarset[var*2];
     551    }
     552    return bddvarset[var * 2];
    786553}
    787554
     
    801568ALSO    {* bdd\_setvarnum, bdd\_ithvar, bdd_true(), bdd_false() *}
    802569*/
    803 BDD bdd_nithvar(int var)
    804 {
    805     if (var < 0  ||  var >= bddvarnum)
    806     {
     570BDD bdd_nithvar(int var) {
     571    if (UNLIKELY(var < 0 || var >= bddvarnum)) {
    807572        bdd_error(BDD_VAR);
    808         return bdd_zero();
    809     }
    810 
     573    }
    811574    return bddvarset[var*2+1];
    812575}
     
    823586ALSO    {* bdd\_setvarnum, bdd\_ithvar *}
    824587*/
    825 int bdd_varnum(void)
    826 {
     588int bdd_varnum(void) {
    827589    return bddvarnum;
    828590}
     
    837599RETURN  {* The variable number. *}
    838600*/
    839 int bdd_var(BDD root)
    840 {
     601int bdd_var(BDD root) {
    841602    CHECK(root);
    842603    if (ISCONST(root)) {
    843         return bdd_error(BDD_ILLBDD);
     604        bdd_error(BDD_ILLBDD);
    844605    }
    845606    return (bddlevel2var[LEVEL(root)]);
     
    856617ALSO    {* bdd\_high *}
    857618*/
    858 BDD bdd_low(BDD root)
    859 {
     619BDD bdd_low(BDD root) {
    860620    CHECK(root);
    861621    if (ISCONST(root)) {
    862         return bdd_error(BDD_ILLBDD);
     622        bdd_error(BDD_ILLBDD);
    863623    }
    864624    return (LOW(root));
     
    875635ALSO    {* bdd\_low *}
    876636*/
    877 BDD bdd_high(BDD root)
    878 {
     637BDD bdd_high(BDD root) {
    879638    CHECK(root);
    880639    if (ISCONST(root)) {
    881         return bdd_error(BDD_ILLBDD);
     640        bdd_error(BDD_ILLBDD);
    882641    }
    883642    return (HIGH(root));
    884643}
    885 
    886 
    887644
    888645/*************************************************************************
     
    901658        BddNode *node = &bddnodes[n];
    902659
    903         if (LOWp(node) != -1)
     660        if (LOW(node) != -1)
    904661        {
    905662            unsigned int hash;
    906663
    907             hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
     664            hash = NODEHASH(LEVEL(node), LOW(node), HIGH(node));
    908665            node->next = bddnodes[hash].hash;
    909666            bddnodes[hash].hash = n;
     
    923680    int *r;
    924681    int n;
    925     long int c2, c1 = clock();
    926 
    927     if (gbc_handler != NULL)
    928     {
    929         bddGbcStat s;
    930         s.nodes = bddnodesize;
    931         s.freenodes = bddfreenum;
    932         s.time = 0;
    933         s.sumtime = gbcclock;
    934         s.num = gbcollectnum;
    935         gbc_handler(1, &s);
    936     }
    937682
    938683    for (r=bddrefstack ; r<bddrefstacktop ; r++)
     
    941686    for (n=0 ; n<bddnodesize ; n++)
    942687    {
    943         if (bddnodes[n].refcou > 0)
     688        if (bddnodes[n].refcount > 0)
    944689            bdd_mark(n);
    945690        bddnodes[n].hash = 0;
     
    953698        BddNode *node = &bddnodes[n];
    954699
    955         if ((LEVELp(node) & MARKON)  &&  LOWp(node) != -1)
    956         {
    957             unsigned int hash;
    958 
    959             LEVELp(node) &= MARKOFF;
    960             hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
     700        if (MARKED(node) && LOW(node) != -1) {
     701            UNMARK(node);
     702            unsigned int hash = NODEHASH(LEVEL(node), LOW(node), HIGH(node));
    961703            node->next = bddnodes[hash].hash;
    962704            bddnodes[hash].hash = n;
     
    964706        else
    965707        {
    966             LOWp(node) = -1;
     708            node->low = -1;
    967709            node->next = bddfreepos;
    968710            bddfreepos = n;
     
    973715    bdd_operator_reset();
    974716
    975     c2 = clock();
    976     gbcclock += c2-c1;
    977717    gbcollectnum++;
    978718
    979     if (gbc_handler != NULL)
    980     {
    981         bddGbcStat s;
    982         s.nodes = bddnodesize;
    983         s.freenodes = bddfreenum;
    984         s.time = c2-c1;
    985         s.sumtime = gbcclock;
    986         s.num = gbcollectnum;
    987         gbc_handler(0, &s);
    988     }
    989719}
    990720
     
    1007737    }
    1008738    if (LOW(root) == -1 || root >= bddnodesize) {
    1009         return bdd_error(BDD_ILLBDD);
     739        bdd_error(BDD_ILLBDD);
    1010740    }
    1011741
     
    1032762    }
    1033763    if (LOW(root) == -1 || root >= bddnodesize) {
    1034         return bdd_error(BDD_ILLBDD);
    1035     }
    1036     bddnodes[root].refcou = std::min<unsigned int>(n + bddnodes[root].refcou, MAXREF);
     764        bdd_error(BDD_ILLBDD);
     765    }
     766    bddnodes[root].refcount = std::min<unsigned int>(n + bddnodes[root].refcount, MAXREF);
    1037767    return root;
    1038768}
     
    1056786    }
    1057787    if (LOW(root) == -1 || root >= bddnodesize) {
    1058         return bdd_error(BDD_ILLBDD);
     788        bdd_error(BDD_ILLBDD);
    1059789    }
    1060790    /* if the following line is present, fails there much earlier */
     
    1083813    }
    1084814    if (root >= bddnodesize)
    1085         return bdd_error(BDD_ILLBDD);   
     815        bdd_error(BDD_ILLBDD);
    1086816    BddNode * node = bddnodes + root;
    1087817    if (node->low == -1)
    1088         return bdd_error(BDD_ILLBDD);
    1089     if (node->low == -1 || node->refcou == 0) {
     818        bdd_error(BDD_ILLBDD);
     819    if (node->low == -1 || node->refcount == 0) {
    1090820        return root;
    1091821    }
    1092     if (--node->refcou == 0) {
     822    if (--node->refcount == 0) {
    1093823        bdd_recursive_deref(node->low);
    1094824        bdd_recursive_deref(node->high);
     
    1108838
    1109839    node = &bddnodes[i];
    1110     if (LEVELp(node) & MARKON  ||  LOWp(node) == -1)
     840    if (MARKED(node) || LOW(node) == -1)
    1111841        return;
    1112842
    1113     LEVELp(node) |= MARKON;
    1114 
    1115     bdd_mark(LOWp(node));
    1116     bdd_mark(HIGHp(node));
     843    SETMARK(node);
     844    bdd_mark(LOW(node));
     845    bdd_mark(HIGH(node));
    1117846}
    1118847
     
    1125854        return;
    1126855
    1127     if (LEVELp(node) & MARKON  ||  LOWp(node) == -1)
     856    if (MARKED(node) || LOW(node) == -1)
    1128857        return;
    1129858
    1130     if (LEVELp(node) > level)
     859    if (LEVEL(node) > level)
    1131860        return;
    1132861
    1133     LEVELp(node) |= MARKON;
    1134 
    1135     bdd_mark_upto(LOWp(node), level);
    1136     bdd_mark_upto(HIGHp(node), level);
     862    SETMARK(node);
     863    bdd_mark_upto(LOW(node), level);
     864    bdd_mark_upto(HIGH(node), level);
    1137865}
    1138866
     
    1146874
    1147875    node = &bddnodes[i];
    1148     if (MARKEDp(node)  ||  LOWp(node) == -1)
     876    if (MARKED(node)  ||  LOW(node) == -1)
    1149877        return;
    1150878
    1151     SETMARKp(node);
     879    SETMARK(node);
    1152880    *cou += 1;
    1153881
    1154     bdd_markcount(LOWp(node), cou);
    1155     bdd_markcount(HIGHp(node), cou);
     882    bdd_markcount(LOW(node), cou);
     883    bdd_markcount(HIGH(node), cou);
    1156884}
    1157885
     
    1159887void bdd_unmark(int i)
    1160888{
    1161     BddNode *node;
    1162 
    1163889    if (i < 2)
    1164890        return;
    1165 
    1166     node = &bddnodes[i];
    1167 
    1168     if (!MARKEDp(node)  ||  LOWp(node) == -1)
    1169         return;
    1170     UNMARKp(node);
    1171 
    1172     bdd_unmark(LOWp(node));
    1173     bdd_unmark(HIGHp(node));
     891    BddNode * node = &bddnodes[i];
     892    if (MARKED(node) && LOW(node) >= 0) {
     893        UNMARK(node);
     894        bdd_unmark(LOW(node));
     895        bdd_unmark(HIGH(node));
     896    }
    1174897}
    1175898
     
    1177900void bdd_unmark_upto(int i, int level)
    1178901{
    1179     BddNode *node = &bddnodes[i];
    1180 
    1181902    if (i < 2)
    1182903        return;
    1183 
    1184     if (!(LEVELp(node) & MARKON))
    1185         return;
    1186 
    1187     LEVELp(node) &= MARKOFF;
    1188 
    1189     if (LEVELp(node) > level)
    1190         return;
    1191 
    1192     bdd_unmark_upto(LOWp(node), level);
    1193     bdd_unmark_upto(HIGHp(node), level);
     904    BddNode * node = &bddnodes[i];
     905    if (MARKED(node)) {
     906        UNMARK(node);
     907        if (LEVEL(node) <= level) {
     908            bdd_unmark_upto(LOW(node), level);
     909            bdd_unmark_upto(HIGH(node), level);
     910        }
     911    }
    1194912}
    1195913
     
    1199917*************************************************************************/
    1200918
    1201 int bdd_makenode(unsigned int level, int low, int high)
    1202 {
    1203     BddNode *node;
     919int bdd_makenode(unsigned int level, int low, int high) {
     920
    1204921    unsigned int hash;
    1205922    int res;
     
    1208925    assert (high >= 0);
    1209926
    1210 #ifdef CACHESTATS
    1211     bddcachestats.uniqueAccess++;
    1212 #endif
    1213 
    1214927    /* check whether childs are equal */
    1215     if (low == high)
     928    if (UNLIKELY(low == high)) {
    1216929        return low;
     930    }
    1217931
    1218932    /* Try to find an existing node of this kind */
     
    1220934    res = bddnodes[hash].hash;
    1221935
    1222     while(res != 0)
    1223     {
    1224         if (LEVEL(res) == level  &&  LOW(res) == low  &&  HIGH(res) == high)
    1225         {
    1226 #ifdef CACHESTATS
    1227             bddcachestats.uniqueHit++;
    1228 #endif
     936    while (res) {
     937        if (LEVEL(res) == level && LOW(res) == low && HIGH(res) == high) {
    1229938            return res;
    1230939        }
    1231 
    1232940        res = bddnodes[res].next;
    1233 #ifdef CACHESTATS
    1234         bddcachestats.uniqueChain++;
    1235 #endif
    1236941    }
    1237942
    1238943    /* No existing node -> build one */
    1239 #ifdef CACHESTATS
    1240     bddcachestats.uniqueMiss++;
    1241 #endif
    1242944
    1243945    /* Any free nodes to use ? */
    1244     if (bddfreepos == 0)
    1245     {
    1246         if (bdderrorcond)
    1247             return 0;
     946    if (bddfreepos == 0) {
    1248947
    1249948        /* Try to allocate more nodes */
     
    1251950
    1252951        if ((bddnodesize - bddfreenum) >= usednodes_nextreorder && bdd_reorder_ready()) {
    1253             throw std::runtime_error("restarting without reallocation");
    1254         }
    1255 
    1256         if ((bddfreenum*100) / bddnodesize <= minfreenodes)
    1257         {
     952            throw reordering_required();
     953        }
     954
     955        if ((bddfreenum*100) / bddnodesize <= minfreenodes) {
    1258956            bdd_noderesize(1);
    1259957            hash = NODEHASH(level, low, high);
     
    1261959
    1262960        /* Panic if that is not possible */
    1263         if (bddfreepos == 0)
    1264         {
     961        if (bddfreepos == 0) {
    1265962            bdd_error(BDD_NODENUM);
    1266             bdderrorcond = abs(BDD_NODENUM);
    1267             return 0;
    1268963        }
    1269964    }
     
    1275970    bddproduced++;
    1276971
    1277     node = &bddnodes[res];
    1278     LEVELp(node) = level;
    1279     LOWp(node) = low;
    1280     HIGHp(node) = high;
     972    BddNode * node = bddnodes + res;
     973    node->level = level;
     974    node->low = low;
     975    node->high = high;
    1281976
    1282977    /* Insert node */
     
    1290985int bdd_noderesize(int doRehash)
    1291986{
    1292     BddNode *newnodes;
    1293     int oldsize = bddnodesize;
    1294     int n;
     987    const int oldsize = bddnodesize;
    1295988
    1296989    if (bddnodesize >= bddmaxnodesize  &&  bddmaxnodesize > 0)
     
    13071000    bddnodesize = bdd_prime_lte(bddnodesize);
    13081001
    1309     if (resize_handler != NULL)
     1002    if (resize_handler != nullptr)
    13101003        resize_handler(oldsize, bddnodesize);
    13111004
    1312     newnodes = (BddNode*)realloc(bddnodes, sizeof(BddNode)*bddnodesize);
    1313     if (newnodes == NULL)
    1314         return bdd_error(BDD_MEMORY);
     1005    BddNode * newnodes = (BddNode*)realloc(bddnodes, sizeof(BddNode)*bddnodesize);
     1006    if (newnodes == nullptr)
     1007        bdd_error(BDD_MEMORY);
    13151008    bddnodes = newnodes;
    13161009
    13171010    if (doRehash)
    1318         for (n=0 ; n<oldsize ; n++)
     1011        for (unsigned n=0 ; n<oldsize ; n++)
    13191012            bddnodes[n].hash = 0;
    13201013
    1321     for (n=oldsize ; n<bddnodesize ; n++)
    1322     {
    1323         bddnodes[n].refcou = 0;
     1014    for (unsigned n=oldsize ; n<bddnodesize ; n++) {
     1015        bddnodes[n].refcount = 0;
     1016        bddnodes[n].level = 0;
     1017        bddnodes[n].low = -1;
    13241018        bddnodes[n].hash = 0;
    1325         LEVEL(n) = 0;
    1326         LOW(n) = -1;
    1327         bddnodes[n].next = n+1;
     1019        bddnodes[n].next = n + 1;
    13281020    }
    13291021    bddnodes[bddnodesize-1].next = bddfreepos;
     
    13831075    {
    13841076        *varnum = 0;
    1385         *varset = NULL;
     1077        *varset = nullptr;
    13861078        return 0;
    13871079    }
     
    13901082        num++;
    13911083
    1392     if (((*varset) = (int *)malloc(sizeof(int)*num)) == NULL)
    1393         return bdd_error(BDD_MEMORY);
     1084    if (((*varset) = (int *)malloc(sizeof(int)*num)) == nullptr)
     1085        bdd_error(BDD_MEMORY);
    13941086
    13951087    for (n=r, num=0 ; n > 1 ; n=HIGH(n))
  • icGREP/icgrep-devel/buddy-2.4/src/kernel.h

    r4928 r4938  
    4242
    4343#include <limits.h>
     44#include <stdexcept>
    4445#include "bdd.h"
     46
     47/*=== BUILT-INS ==========================================================*/
     48
     49#ifndef __has_builtin
     50#define __has_builtin(x) 0
     51#endif
     52
     53#ifndef __GNUC_PREREQ
     54#if defined(__GNUC__) && defined(__GNUC_MINOR__)
     55  #define __GNUC_PREREQ(maj, min) ((__GNUC__ << 16) + __GNUC_MINOR__ >= ((maj) << 16) + (min))
     56#else
     57  #define __GNUC_PREREQ(maj, min) 0
     58#endif
     59#endif
     60
     61#if __has_builtin(__builtin_expect) || __GNUC_PREREQ(4, 0)
     62#define LIKELY(EXPR) __builtin_expect((bool)(EXPR), true)
     63#define UNLIKELY(EXPR) __builtin_expect((bool)(EXPR), false)
     64#else
     65#define LIKELY(EXPR) (EXPR)
     66#define UNLIKELY(EXPR) (EXPR)
     67#endif
     68
     69#ifndef NDEBUG
     70#define ALWAYS_INLINE
     71#elif defined _MSC_VER
     72#define ALWAYS_INLINE   __forceinline
     73#elif defined __GNUC__
     74#define ALWAYS_INLINE   __attribute__((always_inline)) inline
     75#else
     76#define ALWAYS_INLINE   inline
     77#endif
    4578
    4679/*=== SANITY CHECKS ====================================================*/
     
    5184#endif
    5285
    53 
    54 /* Sanity check argument and return eventual error code */
    55 #define CHECK(r)\
    56     if (!bddrunning) return bdd_error(BDD_RUNNING);\
    57     else if ((r) < 0  ||  (r) >= bddnodesize) return bdd_error(BDD_ILLBDD);\
    58     else if (r >= 2 && LOW(r) == -1) return bdd_error(BDD_ILLBDD)\
    59 
    60 /* Sanity check argument and return eventually the argument 'a' */
    61 #define CHECKa(r,a)\
    62     if (!bddrunning) { bdd_error(BDD_RUNNING); return (a); }\
    63     else if ((r) < 0  ||  (r) >= bddnodesize)\
    64 { bdd_error(BDD_ILLBDD); return (a); }\
    65     else if (r >= 2 && LOW(r) == -1)\
    66 { bdd_error(BDD_ILLBDD); return (a); }
    67 
    68 #define CHECKn(r)\
    69     if (!bddrunning) { bdd_error(BDD_RUNNING); return; }\
    70     else if ((r) < 0  ||  (r) >= bddnodesize)\
    71 { bdd_error(BDD_ILLBDD); return; }\
    72     else if (r >= 2 && LOW(r) == -1)\
    73 { bdd_error(BDD_ILLBDD); return; }
    74 
    7586/*=== SEMI-INTERNAL TYPES ==============================================*/
    7687
    7788typedef struct s_BddNode /* Node table entry */
    7889{
    79     unsigned int refcou : 10;
    80     unsigned int level  : 22;
     90    unsigned int refcount : 10;
     91    unsigned int level : 22;
    8192    int low;
    8293    int high;
    83     int hash;
    84     int next;
     94    unsigned hash;
     95    unsigned next;
    8596} BddNode;
    8697
     
    93104
    94105extern int       bddrunning;         /* Flag - package initialized */
    95 extern int       bdderrorcond;       /* Some error condition was met */
    96106extern int       bddnodesize;        /* Number of allocated nodes */
    97107extern int       bddmaxnodesize;     /* Maximum allowed number of nodes */
     
    105115extern int       bddreorderdisabled;
    106116extern int       bddresized;
    107 extern bddCacheStat bddcachestats;
    108117
    109118#ifdef CPLUSPLUS
     
    111120#endif
    112121
     122/*=== KERNEL DEFINITIONS ===============================================*/
     123
     124class reordering_required : public std::exception {
     125public:
     126reordering_required() = default;
     127virtual char const * what() const  _GLIBCXX_USE_NOEXCEPT { return nullptr; }
     128};
    113129
    114130/*=== KERNEL DEFINITIONS ===============================================*/
     
    117133#define MAXREF 0x3FF
    118134
     135static ALWAYS_INLINE void DECREF(const BDD i) {
     136    BddNode & n = bddnodes[i];
     137    if (LIKELY(n.refcount != 0 && n.refcount != MAXREF)) {
     138        n.refcount--;
     139    }
     140}
     141
     142static ALWAYS_INLINE void INCREF(const BDD i) {
     143    BddNode & n = bddnodes[i];
     144    if (LIKELY(n.refcount != MAXREF)) {
     145        n.refcount++;
     146    }
     147}
     148
    119149/* Reference counting */
    120 #define DECREF(n) if (bddnodes[n].refcou!=MAXREF && bddnodes[n].refcou>0) bddnodes[n].refcou--
    121 #define INCREF(n) if (bddnodes[n].refcou<MAXREF) bddnodes[n].refcou++
    122 #define DECREFp(n) if (n->refcou!=MAXREF && n->refcou>0) n->refcou--
    123 #define INCREFp(n) if (n->refcou<MAXREF) n->refcou++
    124 #define HASREF(n) (bddnodes[n].refcou > 0)
     150static ALWAYS_INLINE bool HASREF(const BDD i) {
     151    return (bddnodes[i].refcount != 0);
     152}
    125153
    126154/* Marking BDD nodes */
     
    128156#define MARKOFF  0x1FFFFF    /* - unmark */
    129157#define MARKHIDE 0x1FFFFF
    130 #define SETMARK(n)  (bddnodes[n].level |= MARKON)
    131 #define UNMARK(n)   (bddnodes[n].level &= MARKOFF)
    132 #define MARKED(n)   (bddnodes[n].level & MARKON)
    133 #define SETMARKp(p) (node->level |= MARKON)
    134 #define UNMARKp(p)  (node->level &= MARKOFF)
    135 #define MARKEDp(p)  (node->level & MARKON)
     158
     159static ALWAYS_INLINE void SETMARK(BddNode * const p) {
     160    p->level |= MARKON;
     161}
     162
     163static ALWAYS_INLINE void SETMARK(const BDD i) {
     164    SETMARK(bddnodes + i);
     165}
     166
     167static ALWAYS_INLINE void UNMARK(BddNode * const p) {
     168    p->level &= MARKOFF;
     169}
     170
     171static ALWAYS_INLINE void UNMARK(const BDD i) {
     172    UNMARK(bddnodes + i);
     173}
     174
     175static ALWAYS_INLINE bool MARKED(const BddNode * const p) {
     176    return (p->level & MARKON) != 0;
     177}
     178
     179static ALWAYS_INLINE bool MARKED(const BDD i) {
     180    return MARKED(bddnodes + i);
     181}
     182
     183
     184
    136185
    137186/* Hashfunctions */
     
    146195#define ISONE(a)   ((a) == 1)
    147196#define ISZERO(a)  ((a) == 0)
    148 #define LEVEL(a)   (bddnodes[a].level)
    149 #define LOW(a)     (bddnodes[a].low)
    150 #define HIGH(a)    (bddnodes[a].high)
    151 #define LEVELp(p)   ((p)->level)
    152 #define LOWp(p)     ((p)->low)
    153 #define HIGHp(p)    ((p)->high)
     197
     198static ALWAYS_INLINE unsigned LEVEL(const BddNode * const p) {
     199    return p->level;
     200}
     201
     202static ALWAYS_INLINE unsigned LEVEL(const BDD i) {
     203    return LEVEL(bddnodes + i);
     204}
     205
     206static ALWAYS_INLINE int LOW(const BddNode * const p) {
     207    return p->low;
     208}
     209
     210static ALWAYS_INLINE int LOW(const BDD i) {
     211    return LOW(bddnodes + i);
     212}
     213
     214static ALWAYS_INLINE int HIGH(const BddNode * const p) {
     215    return p->high;
     216}
     217
     218static ALWAYS_INLINE int HIGH(const BDD i) {
     219    return HIGH(bddnodes + i);
     220}
    154221
    155222/* Stacking for garbage collector */
    156 #define INITREF    bddrefstacktop = bddrefstack
    157 #define PUSHREF(a) *(bddrefstacktop++) = (a)
    158 #define READREF(a) *(bddrefstacktop-(a))
    159 #define POPREF(a)  bddrefstacktop -= (a)
     223#define INITREF bddrefstacktop = bddrefstack
     224
     225static ALWAYS_INLINE BDD PUSHREF(const BDD n) {
     226    *bddrefstacktop++ = n;
     227    return n;
     228}
     229
     230static ALWAYS_INLINE BDD READREF(const int i) {
     231    return bddrefstacktop[-i];
     232}
     233
     234static ALWAYS_INLINE void POPREF(const int i) {
     235    bddrefstacktop -= i;
     236}
    160237
    161238#define BDDONE 1
     
    177254#define NEW(t,n) ( (t*)malloc(sizeof(t)*(n)) )
    178255
    179 
    180256/*=== KERNEL PROTOTYPES ================================================*/
    181257
     
    184260#endif
    185261
    186 extern int    bdd_error(int);
     262extern void   bdd_error(const unsigned code);
    187263extern int    bdd_makenode(unsigned int, int, int);
    188264extern int    bdd_noderesize(int);
     
    219295#endif
    220296
     297
     298/*=== INPUT VALIDATION ==================================================*/
     299
     300inline void CHECK(const BDD r) {
     301    if (UNLIKELY(!bddrunning)) {
     302        bdd_error(BDD_RUNNING);
     303    } else if (UNLIKELY(r < 0 || r >= bddnodesize)) {
     304        bdd_error(BDD_ILLBDD);
     305    } else if (UNLIKELY(r >= 2 && LOW(r) == -1)) {
     306        bdd_error(BDD_ILLBDD);
     307    }
     308}
     309
    221310#endif /* _KERNEL_H */
    222311
  • icGREP/icgrep-devel/buddy-2.4/src/pairs.cpp

    r4867 r4938  
    5151{
    5252    pairsid = 0;
    53     pairs = NULL;
     53    pairs = nullptr;
    5454}
    5555
     
    6060    int n;
    6161
    62     while (p != NULL)
     62    while (p != nullptr)
    6363    {
    6464        bddPair *next = p->next;
     
    8080        bddPair *p;
    8181        pairsid = 0;
    82         for (p=pairs ; p!=NULL ; p=p->next)
     82        for (p=pairs ; p!=nullptr ; p=p->next)
    8383            p->id = pairsid++;
    8484        bdd_operator_reset();
     
    100100    bddPair *p;
    101101
    102     for (p=pairs ; p!=NULL ; p=p->next)
     102    for (p=pairs ; p!=nullptr ; p=p->next)
    103103    {
    104104        int tmp;
     
    119119    int n;
    120120
    121     for (p=pairs ; p!=NULL ; p=p->next)
    122     {
    123         if ((p->result=(BDD*)realloc(p->result,sizeof(BDD)*newsize)) == NULL)
    124             return bdd_error(BDD_MEMORY);
     121    for (p=pairs ; p!=nullptr ; p=p->next)
     122    {
     123        if ((p->result=(BDD*)realloc(p->result,sizeof(BDD)*newsize)) == nullptr)
     124            bdd_error(BDD_MEMORY);
    125125
    126126        for (n=oldsize ; n<newsize ; n++)
     
    149149    bddPair *p;
    150150
    151     if ((p=(bddPair*)malloc(sizeof(bddPair))) == NULL)
     151    if ((p=(bddPair*)malloc(sizeof(bddPair))) == nullptr)
    152152    {
    153153        bdd_error(BDD_MEMORY);
    154         return NULL;
    155     }
    156 
    157     if ((p->result=(BDD*)malloc(sizeof(BDD)*bddvarnum)) == NULL)
     154    }
     155
     156    if ((p->result=(BDD*)malloc(sizeof(BDD)*bddvarnum)) == nullptr)
    158157    {
    159158        free(p);
    160159        bdd_error(BDD_MEMORY);
    161         return NULL;
    162160    }
    163161
     
    196194int bdd_setpair(bddPair *pair, int oldvar, int newvar)
    197195{
    198     if (pair == NULL)
     196    if (pair == nullptr)
    199197        return 0;
    200198
    201199    if (oldvar < 0  ||  oldvar > bddvarnum-1)
    202         return bdd_error(BDD_VAR);
     200        bdd_error(BDD_VAR);
    203201    if (newvar < 0  ||  newvar > bddvarnum-1)
    204         return bdd_error(BDD_VAR);
     202        bdd_error(BDD_VAR);
    205203
    206204    bdd_delref( pair->result[bddvar2level[oldvar]] );
     
    219217    int oldlevel;
    220218
    221     if (pair == NULL)
     219    if (pair == nullptr)
    222220        return 0;
    223221
    224222    CHECK(newvar);
    225223    if (oldvar < 0  ||  oldvar >= bddvarnum)
    226         return bdd_error(BDD_VAR);
     224        bdd_error(BDD_VAR);
    227225    oldlevel = bddvar2level[oldvar];
    228226
     
    253251{
    254252    int n,e;
    255     if (pair == NULL)
     253    if (pair == nullptr)
    256254        return 0;
    257255
     
    267265{
    268266    int n,e;
    269     if (pair == NULL)
     267    if (pair == nullptr)
    270268        return 0;
    271269
     
    291289    int n;
    292290
    293     if (p == NULL)
     291    if (p == nullptr)
    294292        return;
    295293
     
    297295    {
    298296        bddPair *bp = pairs;
    299         while (bp != NULL  &&  bp->next != p)
     297        while (bp != nullptr  &&  bp->next != p)
    300298            bp = bp->next;
    301299
    302         if (bp != NULL)
     300        if (bp != nullptr)
    303301            bp->next = p->next;
    304302    }
  • icGREP/icgrep-devel/buddy-2.4/src/reorder.cpp

    r4867 r4938  
    5252 */
    5353
    54 /* Change macros to reflect the above idea */
    55 #define VAR(n) (bddnodes[n].level)
    56 #define VARp(p) (p->level)
    57 
    58 /* Avoid these - they are misleading! */
    59 #undef LEVEL
    60 #undef LEVELp
     54#define MARKHIDE 0x1FFFFF
     55
     56static ALWAYS_INLINE unsigned VAR(const BddNode * const p) {
     57    return (p->level);
     58}
     59
     60static ALWAYS_INLINE unsigned VAR(const BDD i) {
     61    return VAR(bddnodes + i);
     62}
    6163
    6264
     
    141143{
    142144    reorderdisabled = 0;
    143     vartree = NULL;
     145    vartree = nullptr;
    144146
    145147    bdd_clrvarblocks();
     
    157159    bddtree_del(vartree);
    158160    bdd_operator_reset();
    159     vartree = NULL;
     161    vartree = nullptr;
    160162}
    161163
     
    171173    BddTree *current=t, *first=t;
    172174
    173     if (t == NULL)
     175    if (t == nullptr)
    174176        return t;
    175177
     
    178180    fflush(stdout);
    179181
    180     while (current->next != NULL)
     182    while (current->next != nullptr)
    181183    {
    182184        int best = reorder_nodenum();
     
    213215    int c=1;
    214216
    215     if (t == NULL)
     217    if (t == nullptr)
    216218        return t;
    217219
     
    224226
    225227        current = t;
    226         while (current->next != NULL)
     228        while (current->next != nullptr)
    227229        {
    228230            int best = reorder_nodenum();
     
    260262static BddTree *reorder_swapwin3(BddTree *current, BddTree **first)
    261263{
    262     int setfirst = (current->prev == NULL ? 1 : 0);
     264    int setfirst = (current->prev == nullptr ? 1 : 0);
    263265    BddTree *next = current;
    264266    int best = reorder_nodenum();
    265267
    266     if (current->next->next == NULL) /* Only two blocks left -> win2 swap */
     268    if (current->next->next == nullptr) /* Only two blocks left -> win2 swap */
    267269    {
    268270        blockdown(current);
     
    396398    BddTree *current=t, *first=t;
    397399
    398     if (t == NULL)
     400    if (t == nullptr)
    399401        return t;
    400402
     
    403405    fflush(stdout);
    404406
    405     while (current->next != NULL)
     407    while (current->next != nullptr)
    406408    {
    407409        current = reorder_swapwin3(current, &first);
     
    427429    int lastsize;
    428430
    429     if (t == NULL)
     431    if (t == nullptr)
    430432        return t;
    431433
     
    438440        current = first;
    439441
    440         while (current->next != NULL  &&  current->next->next != NULL)
     442        while (current->next != nullptr  &&  current->next->next != nullptr)
    441443        {
    442444            current = reorder_swapwin3(current, &first);
     
    490492        if (dirIsUp)
    491493        {
    492             while (blk->prev != NULL  &&
     494            while (blk->prev != nullptr  &&
    493495                   (reorder_nodenum() <= maxAllowed || first))
    494496            {
     
    518520        else
    519521        {
    520             while (blk->next != NULL  &&
     522            while (blk->next != nullptr  &&
    521523                   (reorder_nodenum() <= maxAllowed  ||  first))
    522524            {
     
    576578    int n;
    577579
    578     if (t == NULL)
     580    if (t == nullptr)
    579581        return t;
    580582
     
    604606
    605607    /* Find first block */
    606     for (current=t ; current->prev != NULL ; current=current->prev)
     608    for (current=t ; current->prev != nullptr ; current=current->prev)
    607609        /* nil */;
    608610
     
    634636    int n, num;
    635637
    636     for (current=t,num=0 ; current!=NULL ; current=current->next)
     638    for (current=t,num=0 ; current!=nullptr ; current=current->next)
    637639        current->pos = num++;
    638640
    639     if ((p=NEW(sizePair,num)) == NULL)
     641    if ((p=NEW(sizePair,num)) == nullptr)
    640642        return t;
    641     if ((seq=NEW(BddTree*,num)) == NULL)
     643    if ((seq=NEW(BddTree*,num)) == nullptr)
    642644    {
    643645        free(p);
     
    645647    }
    646648
    647     for (current=t,n=0 ; current!=NULL ; current=current->next,n++)
     649    for (current=t,n=0 ; current!=nullptr ; current=current->next,n++)
    648650    {
    649651        int v;
     
    682684    int c=1;
    683685
    684     if (t == NULL)
     686    if (t == nullptr)
    685687        return t;
    686688
     
    707709    int n, num=0;
    708710
    709     if (t == NULL)
     711    if (t == nullptr)
    710712        return t;
    711713
    712     for (current=t ; current!=NULL ; current=current->next)
     714    for (current=t ; current!=nullptr ; current=current->next)
    713715        num++;
    714716    seq = NEW(BddTree*,num);
    715     for (current=t,num=0 ; current!=NULL ; current=current->next)
     717    for (current=t,num=0 ; current!=nullptr ; current=current->next)
    716718        seq[num++] = current;
    717719
     
    719721    {
    720722        int blk = random(num);
    721         if (seq[blk]->next != NULL)
     723        if (seq[blk]->next != nullptr)
    722724            blockdown(seq[blk]);
    723725    }
    724726
    725727    /* Find first block */
    726     for (current=t ; current->prev != NULL ; current=current->prev)
     728    for (current=t ; current->prev != nullptr ; current=current->prev)
    727729        /* nil */;
    728730
     
    789791    right->next = left;
    790792
    791     if (right->prev != NULL)
     793    if (right->prev != nullptr)
    792794        right->prev->next = right;
    793     if (left->next != NULL)
     795    if (left->next != nullptr)
    794796        left->next->prev = left;
    795797
     
    813815        return;
    814816
    815     if (bddnodes[r].refcou == 0)
     817    if (bddnodes[r].refcount == 0)
    816818    {
    817819        bddfreenum--;
     
    873875        bddnodes[n].level = bddlevel2var[bddnodes[n].level];
    874876
    875         if (bddnodes[n].refcou > 0)
     877        if (bddnodes[n].refcount > 0)
    876878        {
    877879            SETMARK(n);
     
    880882    }
    881883
    882     if ((extroots=(int*)(malloc(sizeof(int)*extrootsize))) == NULL)
    883         return bdd_error(BDD_MEMORY);
     884    if ((extroots=(int*)(malloc(sizeof(int)*extrootsize))) == nullptr)
     885        bdd_error(BDD_MEMORY);
    884886
    885887    iactmtx = imatrixNew(bddvarnum);
     
    889891        BddNode *node = &bddnodes[n];
    890892
    891         if (MARKEDp(node))
    892         {
    893             UNMARKp(node);
     893        if (MARKED(node))
     894        {
     895            UNMARK(node);
    894896            extroots[extrootsize++] = n;
    895897
    896898            memset(dep,0,bddvarnum);
    897             dep[VARp(node)] = 1;
    898             levels[VARp(node)].nodenum++;
    899 
    900             addref_rec(LOWp(node), dep);
    901             addref_rec(HIGHp(node), dep);
     899            dep[VAR(node)] = 1;
     900            levels[VAR(node)].nodenum++;
     901
     902            addref_rec(LOW(node), dep);
     903            addref_rec(HIGH(node), dep);
    902904
    903905            addDependencies(dep);
     
    934936        BddNode *node = &bddnodes[n];
    935937
    936         if (node->refcou > 0)
     938        if (node->refcount > 0)
    937939        {
    938940            unsigned int hash;
    939941
    940             hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
     942            hash = NODEHASH(VAR(node), LOW(node), HIGH(node));
    941943            node->next = bddnodes[hash].hash;
    942944            bddnodes[hash].hash = n;
     
    945947        else
    946948        {
    947             LOWp(node) = -1;
     949            node->low = -1;
    948950            node->next = bddfreepos;
    949951            bddfreepos = n;
     
    995997        BddNode *node = &bddnodes[n];
    996998
    997         if (node->refcou > 0)
     999        if (node->refcount > 0)
    9981000        {
    9991001            unsigned int hash;
    10001002
    1001             hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
     1003            hash = NODEHASH(VAR(node), LOW(node), HIGH(node));
    10021004            node->next = bddnodes[hash].hash;
    10031005            bddnodes[hash].hash = n;
     
    10411043    res = bddnodes[hash].hash;
    10421044
    1043     while(res != 0)
    1044     {
    1045         if (LOW(res) == low  &&  HIGH(res) == high)
    1046         {
    1047 #ifdef CACHESTATS
    1048             bddcachestats.uniqueHit++;
    1049 #endif
     1045    while (res) {
     1046        if (LOW(res) == low  &&  HIGH(res) == high) {
    10501047            INCREF(res);
    10511048            return res;
    10521049        }
    10531050        res = bddnodes[res].next;
    1054 
    1055 #ifdef CACHESTATS
    1056         bddcachestats.uniqueChain++;
    1057 #endif
    1058     }
    1059 
    1060     /* No existing node -> build one */
    1061 #ifdef CACHESTATS
    1062     bddcachestats.uniqueMiss++;
    1063 #endif
     1051    }
    10641052
    10651053    /* Any free nodes to use ? */
    10661054    if (bddfreepos == 0)
    10671055    {
    1068         if (bdderrorcond)
    1069             return 0;
    10701056
    10711057        /* Try to allocate more nodes - call noderesize without
     
    10771063
    10781064        /* Panic if that is not possible */
    1079         if (bddfreepos == 0)
    1080         {
     1065        if (bddfreepos == 0) {
    10811066            bdd_error(BDD_NODENUM);
    1082             bdderrorcond = abs(BDD_NODENUM);
    1083             return 0;
    10841067        }
    10851068    }
     
    10931076
    10941077    node = &bddnodes[res];
    1095     VARp(node) = var;
    1096     LOWp(node) = low;
    1097     HIGHp(node) = high;
     1078    node->level = var;
     1079    node->low = low;
     1080    node->high = high;
    10981081
    10991082    /* Insert node in hash chain */
     
    11021085
    11031086    /* Make sure it is reference counted */
    1104     node->refcou = 1;
    1105     INCREF(LOWp(node));
    1106     INCREF(HIGHp(node));
     1087    node->refcount = 1;
     1088    INCREF(LOW(node));
     1089    INCREF(HIGH(node));
    11071090
    11081091    return res;
     
    11371120            int next = node->next;
    11381121
    1139             if (VAR(LOWp(node)) != var1  &&  VAR(HIGHp(node)) != var1)
     1122            if (VAR(LOW(node)) != var1  &&  VAR(HIGH(node)) != var1)
    11401123            {
    11411124                /* Node does not depend on next var, let it stay in the chain */
     
    11761159        BddNode *node = &bddnodes[toBeProcessed];
    11771160        int next = node->next;
    1178         int f0 = LOWp(node);
    1179         int f1 = HIGHp(node);
     1161        int f0 = LOW(node);
     1162        int f1 = HIGH(node);
    11801163        int f00, f01, f10, f11, hash;
    11811164
     
    12051188      * is greater than one (these are f00...f11), so there is
    12061189      * no need to do a recursive refcou decrease. It is also
    1207       * possible for the LOWp(node)/high nodes to come alive again,
     1190      * possible for the LOW(node)/high nodes to come alive again,
    12081191      * so deref. of the childs is delayed until the local GBC. */
    12091192
    1210         DECREF(LOWp(node));
    1211         DECREF(HIGHp(node));
     1193        DECREF(LOW(node));
     1194        DECREF(HIGH(node));
    12121195
    12131196        /* Update in-place */
    1214         VARp(node) = var1;
    1215         LOWp(node) = f0;
    1216         HIGHp(node) = f1;
     1197        node->level = var1;
     1198        node->low = f0;
     1199        node->high = f1;
    12171200
    12181201        levels[var1].nodenum++;
    12191202
    12201203        /* Rehash the node since it got new childs */
    1221         hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
     1204        hash = NODEHASH(VAR(node), LOW(node), HIGH(node));
    12221205        node->next = bddnodes[hash].hash;
    12231206        bddnodes[hash].hash = toBeProcessed;
     
    12501233            int next = node->next;
    12511234
    1252             if (node->refcou > 0)
     1235            if (node->refcount > 0)
    12531236            {
    12541237                node->next = bddnodes[hash].hash;
     
    12571240            else
    12581241            {
    1259                 DECREF(LOWp(node));
    1260                 DECREF(HIGHp(node));
    1261 
    1262                 LOWp(node) = -1;
     1242                DECREF(LOW(node));
     1243                DECREF(HIGH(node));
     1244
     1245                node->low = -1;
    12631246                node->next = bddfreepos;
    12641247                bddfreepos = r;
     
    12851268        BddNode *node = &bddnodes[toBeProcessed];
    12861269        int next = node->next;
    1287         int f0 = LOWp(node);
    1288         int f1 = HIGHp(node);
     1270        int f0 = LOW(node);
     1271        int f1 = HIGH(node);
    12891272        int f00, f01, f10, f11;
    12901273
     
    13141297      * is greater than one (these are f00...f11), so there is
    13151298      * no need to do a recursive refcou decrease. It is also
    1316       * possible for the LOWp(node)/high nodes to come alive again,
     1299      * possible for the LOW(node)/high nodes to come alive again,
    13171300      * so deref. of the childs is delayed until the local GBC. */
    13181301
    1319         DECREF(LOWp(node));
    1320         DECREF(HIGHp(node));
     1302        DECREF(LOW(node));
     1303        DECREF(HIGH(node));
    13211304
    13221305        /* Update in-place */
    1323         VARp(node) = var1;
    1324         LOWp(node) = f0;
    1325         HIGHp(node) = f1;
     1306        VAR(node) = var1;
     1307        LOW(node) = f0;
     1308        HIGH(node) = f1;
    13261309
    13271310        levels[var1].nodenum++;
     
    13591342            else
    13601343            {
    1361                 DECREF(LOWp(node));
    1362                 DECREF(HIGHp(node));
    1363 
    1364                 LOWp(node) = -1;
     1344                DECREF(LOW(node));
     1345                DECREF(HIGH(node));
     1346
     1347                LOW(node) = -1;
    13651348                node->next = bddfreepos;
    13661349                bddfreepos = r;
     
    13871370        BddNode *node = &bddnodes[toBeProcessed];
    13881371        int next = node->next;
    1389         int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
     1372        int hash = NODEHASH(VAR(node), LOW(node), HIGH(node));
    13901373
    13911374        node->next = bddnodes[hash].hash;
     
    14021385{
    14031386    if (var < 0  ||  var >= bddvarnum)
    1404         return bdd_error(BDD_VAR);
     1387        bdd_error(BDD_VAR);
    14051388    if (bddvar2level[var] == 0)
    14061389        return 0;
     
    14541437
    14551438    if (var < 0  ||  var >= bddvarnum)
    1456         return bdd_error(BDD_VAR);
     1439        bdd_error(BDD_VAR);
    14571440    if ((level=bddvar2level[var]) >= bddvarnum-1)
    14581441        return 0;
     
    15251508
    15261509    /* Do not swap when variable-blocks are used */
    1527     if (vartree != NULL)
    1528         return bdd_error(BDD_VARBLK);
     1510    if (vartree != nullptr)
     1511        bdd_error(BDD_VARBLK);
    15291512
    15301513    /* Don't bother swapping x with x */
     
    15341517    /* Make sure the variable exists */
    15351518    if (v1 < 0  ||  v1 >= bddvarnum  ||  v2 < 0  ||  v2 >= bddvarnum)
    1536         return bdd_error(BDD_VAR);
     1519        bdd_error(BDD_VAR);
    15371520
    15381521    l1 = bddvar2level[v1];
     
    16101593ALSO    {* bdd\_disable\_reorder *}
    16111594*/
    1612 void bdd_enable_reorder(void)
    1613 {
     1595void bdd_enable_reorder(void) {
    16141596    reorderdisabled = 0;
    16151597}
    16161598
    16171599
    1618 int bdd_reorder_ready(void)
    1619 {
    1620     if (bddreordermethod == BDD_REORDER_NONE  ||  vartree == NULL  ||
    1621             bddreordertimes == 0  ||  reorderdisabled)
    1622         return 0;
    1623     return 1;
    1624 }
    1625 
     1600int bdd_reorder_ready(void) {
     1601    return (bddreordermethod == BDD_REORDER_NONE || vartree == nullptr || bddreordertimes == 0  || reorderdisabled) ? 0 : 1;
     1602}
    16261603
    16271604void bdd_reorder_auto(void)
    16281605{
    1629     if (reorder_handler != NULL)
     1606    if (reorder_handler != nullptr)
    16301607        reorder_handler(1);
    16311608
     
    16331610    bddreordertimes--;
    16341611
    1635     if (reorder_handler != NULL)
     1612    if (reorder_handler != nullptr)
    16361613        reorder_handler(0);
    16371614}
     
    16421619    int n;
    16431620
    1644     if ((levels=NEW(levelData,bddvarnum)) == NULL)
     1621    if ((levels=NEW(levelData,bddvarnum)) == nullptr)
    16451622        return -1;
    16461623
     
    16781655            UNMARK(n);
    16791656        else
    1680             bddnodes[n].refcou = 0;
     1657            bddnodes[n].refcount = 0;
    16811658
    16821659        /* This is where we go from .var to .level again!
     
    17201697    BddTree *current;
    17211698
    1722     if (t == NULL)
    1723         return NULL;
    1724 
    1725     if (t->fixed == BDD_REORDER_FREE  &&  t->nextlevel!=NULL)
     1699    if (t == nullptr)
     1700        return nullptr;
     1701
     1702    if (t->fixed == BDD_REORDER_FREE  &&  t->nextlevel!=nullptr)
    17261703    {
    17271704        switch(method)
     
    17541731        reorder_block(current, method);
    17551732
    1756     if (t->seq != NULL)
     1733    if (t->seq != nullptr)
    17571734        qsort(t->seq, t->last-t->first+1, sizeof(int), varseqCmp);
    17581735
     
    18051782    bddreordertimes = 1;
    18061783
    1807     if ((top=bddtree_new(-1)) == NULL)
     1784    if ((top=bddtree_new(-1)) == nullptr)
    18081785        return;
    18091786    if (reorder_init() < 0)
     
    18151792    top->last = bdd_varnum()-1;
    18161793    top->fixed = 0;
    1817     top->next = NULL;
     1794    top->next = nullptr;
    18181795    top->nextlevel = vartree;
    18191796
     
    19071884           the block numbers returned by {\tt bdd\_addvarblock} as arguments.
    19081885       No default handler is supplied. The argument {\tt handler} may be
    1909        NULL if no handler is needed. *}
     1886       nullptr if no handler is needed. *}
    19101887RETURN  {* The old handler *}
    19111888ALSO    {* bdd\_printorder *}
     
    19721949{
    19731950    if (var < 0  ||  var >= bddvarnum)
    1974         return bdd_error(BDD_VAR);
     1951        bdd_error(BDD_VAR);
    19751952
    19761953    return bddvar2level[var];
     
    19901967{
    19911968    if (level < 0  ||  level >= bddvarnum)
    1992         return bdd_error(BDD_VAR);
     1969        bdd_error(BDD_VAR);
    19931970
    19941971    return bddlevel2var[level];
     
    20672044\end{verbatim}
    20682045       No default handler is supplied. The argument {\tt handler} may be
    2069        NULL if no handler is needed. *}
     2046       nullptr if no handler is needed. *}
    20702047       *}
    20712048RETURN  {* The old handler *}
     
    20752052{
    20762053    bddsizehandler old = reorder_nodenum;
    2077     if (handler == NULL)
     2054    if (handler == nullptr)
    20782055        return reorder_nodenum;
    20792056    reorder_nodenum = handler;
     
    20942071{
    20952072    bddtree_del(vartree);
    2096     vartree = NULL;
     2073    vartree = nullptr;
    20972074    blockid = 0;
    20982075}
     
    21432120        return n;
    21442121    if (size < 1)
    2145         return bdd_error(BDD_VARBLK);
     2122        bdd_error(BDD_VARBLK);
    21462123
    21472124    first = last = v[0];
     
    21552132    }
    21562133
    2157     if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL)
    2158         return bdd_error(BDD_VARBLK);
     2134    if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == nullptr)
     2135        bdd_error(BDD_VARBLK);
    21592136
    21602137    vartree = t;
     
    21682145
    21692146    if (first < 0  ||  first >= bddvarnum  ||  last < 0  ||  last >= bddvarnum)
    2170         return bdd_error(BDD_VAR);
    2171 
    2172     if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL)
    2173         return bdd_error(BDD_VARBLK);
     2147        bdd_error(BDD_VAR);
     2148
     2149    if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == nullptr)
     2150        bdd_error(BDD_VARBLK);
    21742151
    21752152    vartree = t;
     
    22502227
    22512228    /* Do not set order when variable-blocks are used */
    2252     if (vartree != NULL)
    2253     {
     2229    if (vartree != nullptr) {
    22542230        bdd_error(BDD_VARBLK);
    2255         return;
    22562231    }
    22572232
     
    22722247static void print_order_rec(FILE *o, BddTree *t, int level)
    22732248{
    2274     if (t == NULL)
     2249    if (t == nullptr)
    22752250        return;
    22762251
  • icGREP/icgrep-devel/buddy-2.4/src/tree.cpp

    r4867 r4938  
    6565{
    6666    BddTree *t = NEW(BddTree,1);
    67     if (t == NULL)
    68         return NULL;
     67    if (t == nullptr)
     68        return nullptr;
    6969
    7070    t->first = t->last = -1;
    7171    t->fixed = 1;
    72     t->next = t->prev = t->nextlevel = NULL;
    73     t->seq = NULL;
     72    t->next = t->prev = t->nextlevel = nullptr;
     73    t->seq = nullptr;
    7474    t->id = id;
    7575    return t;
     
    7979void bddtree_del(BddTree *t)
    8080{
    81     if (t == NULL)
     81    if (t == nullptr)
    8282        return;
    8383
    8484    bddtree_del(t->nextlevel);
    8585    bddtree_del(t->next);
    86     if (t->seq != NULL)
     86    if (t->seq != nullptr)
    8787        free(t->seq);
    8888    free(t);
     
    9494{
    9595    if (first < 0  ||  last < 0  ||  last < first)
    96         return NULL;
     96        return nullptr;
    9797
    9898    /* Empty tree -> build one */
    99     if (t == NULL)
    100     {
    101         if ((t=bddtree_new(id)) == NULL)
    102             return NULL;
     99    if (t == nullptr)
     100    {
     101        if ((t=bddtree_new(id)) == nullptr)
     102            return nullptr;
    103103        t->first = first;
    104104        t->fixed = fixed;
     
    118118    {
    119119        BddTree *tnew = bddtree_new(id);
    120         if (tnew == NULL)
    121             return NULL;
     120        if (tnew == nullptr)
     121            return nullptr;
    122122        tnew->first = first;
    123123        tnew->last = last;
     
    142142    {
    143143        t->nextlevel =
    144                 bddtree_addrange_rec(t->nextlevel,NULL,first,last,fixed,id);
     144                bddtree_addrange_rec(t->nextlevel,nullptr,first,last,fixed,id);
    145145        return t;
    146146    }
     
    156156            /* Partial cover ->error */
    157157            if (last >= current->first  &&  last < current->last)
    158                 return NULL;
    159 
    160             if (current->next == NULL  ||  last < current->next->first)
     158                return nullptr;
     159
     160            if (current->next == nullptr  ||  last < current->next->first)
    161161            {
    162162                tnew = bddtree_new(id);
    163                 if (tnew == NULL)
    164                     return NULL;
     163                if (tnew == nullptr)
     164                    return nullptr;
    165165                tnew->first = first;
    166166                tnew->last = last;
     
    171171                tnew->next = current->next;
    172172                tnew->prev = t->prev;
    173                 if (current->next != NULL)
     173                if (current->next != nullptr)
    174174                    current->next->prev = tnew;
    175                 current->next = NULL;
    176                 t->prev = NULL;
     175                current->next = nullptr;
     176                t->prev = nullptr;
    177177                return tnew;
    178178            }
     
    183183    }
    184184
    185     return NULL;
     185    return nullptr;
    186186}
    187187
     
    189189BddTree *bddtree_addrange(BddTree *t, int first, int last, int fixed,int id)
    190190{
    191     return bddtree_addrange_rec(t,NULL,first,last,fixed,id);
     191    return bddtree_addrange_rec(t,nullptr,first,last,fixed,id);
    192192}
    193193
     
    196196int main(void)
    197197{
    198     BddTree *t = NULL;
     198    BddTree *t = nullptr;
    199199
    200200    t = bddtree_addrange(t, 8,10,1);
Note: See TracChangeset for help on using the changeset viewer.