Ignore:
Timestamp:
Feb 13, 2016, 3:56:25 PM (4 years ago)
Author:
nmedfort
Message:

Bug fix for Buddy in 'apply_rec' function; replaced setjmp/longjmp exception handling with try/catch for node reallocation handling. Removed unnecessary files.

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

Legend:

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

    r4867 r4928  
    249249extern int      bdd_varlevel(int);
    250250extern BDD      bdd_addref(BDD);
     251extern BDD      bdd_addref(BDD, unsigned int);
    251252extern BDD      bdd_delref(BDD);
     253extern BDD      bdd_recursive_deref(BDD root);
    252254extern void     bdd_gbc(void);
    253255extern int      bdd_scanset(BDD, int**, int*);
     
    268270extern BDD      bdd_not(BDD);
    269271extern BDD      bdd_apply(BDD, BDD, int);
    270 extern BDD      bdd_and(BDD, BDD);
    271 extern BDD      bdd_or(BDD, BDD);
    272 extern BDD      bdd_xor(BDD, BDD);
    273 extern BDD      bdd_imp(BDD, BDD);
    274 extern BDD      bdd_biimp(BDD, BDD);
    275272extern BDD      bdd_ite(BDD, BDD, BDD);
    276273extern BDD      bdd_restrict(BDD, BDD);
     
    361358}
    362359
     360/*=== BDD helpers ====================================================*/
     361
     362static inline BDD bdd_and(BDD l, BDD r) {
     363    return bdd_apply(l, r, bddop_and);
     364}
     365
     366static inline BDD bdd_or(BDD l, BDD r) {
     367    return bdd_apply(l, r, bddop_or);
     368}
     369
     370static inline BDD bdd_xor(BDD l, BDD r) {
     371    return bdd_apply(l, r, bddop_xor);
     372}
     373
     374static inline BDD bdd_nor(BDD l, BDD r) {
     375    return bdd_apply(l, r, bddop_nor);
     376}
     377
     378static inline BDD bdd_imp(BDD l, BDD r) {
     379    return bdd_apply(l, r, bddop_imp);
     380}
     381
     382static inline BDD bdd_biimp(BDD l, BDD r) {
     383    return bdd_apply(l, r, bddop_biimp);
     384}
     385
    363386/*=== Reordering algorithms ============================================*/
    364387
  • icGREP/icgrep-devel/buddy-2.4/src/bddop.cpp

    r4867 r4928  
    4040#include <time.h>
    4141#include <assert.h>
     42#include <stdexcept>
    4243
    4344#include "kernel.h"
     
    110111static int cacheratio;
    111112static BDD satPolarity;
    112 static int firstReorder;            /* Used instead of local variable in order
    113                        to avoid compiler warning about 'first'
    114                        being clobbered by setjmp */
    115 
    116113static char*            allsatProfile; /* Variable profile for bdd_allsat() */
    117114static bddallsathandler allsatHandler; /* Callback handler for bdd_allsat() */
     
    297294*************************************************************************/
    298295
    299 static void checkresize(void)
    300 {
     296inline static void checkresize(void) {
    301297    if (bddresized)
    302298        bdd_operator_noderesize();
     
    328324ALSO    {* bdd\_ithvar, fdd\_ithvar *}
    329325*/
    330 BDD bdd_buildcube(int value, int width, BDD *variables)
     326BDD bdd_buildcube(int value, int width, BDD * variables)
    331327{
    332328    BDD result = BDDONE;
    333     int z;
    334 
    335     for (z=0 ; z<width ; z++, value>>=1)
    336     {
    337         BDD tmp;
    338         BDD v;
    339 
    340         if (value & 0x1)
    341             v = bdd_addref( variables[width-z-1] );
    342         else
    343             v = bdd_addref( bdd_not(variables[width-z-1]) );
     329
     330    for (int z = 0; z < width ; z++, value>>=1) {
     331        BDD v = variables[width - z - 1];
     332        if ((value & 1) == 0) {
     333            v = bdd_not(v);
     334        }
     335        v = bdd_addref(v);
    344336
    345337        bdd_addref(result);
    346         tmp = bdd_apply(result,v,bddop_and);
     338        BDD tmp = bdd_apply(result, v, bddop_and);
    347339        bdd_delref(result);
     340
    348341        bdd_delref(v);
    349342
     
    358351{
    359352    BDD result = BDDONE;
    360     int z;
    361 
    362     for (z=0 ; z<width ; z++, value>>=1)
     353
     354    for (int z = 0 ; z<width ; z++, value>>=1)
    363355    {
    364356        BDD tmp;
     
    379371    return result;
    380372}
    381 
    382373
    383374/*=== NOT ==============================================================*/
     
    395386BDD bdd_not(BDD r)
    396387{
    397     BDD res;
    398     firstReorder = 1;
     388    BDD res = BDDZERO;
    399389    CHECKa(r, bdd_zero());
    400390
    401 again:
    402     if (setjmp(bddexception) == 0)
    403     {
     391    try {
    404392        INITREF;
    405 
    406         if (!firstReorder)
    407             bdd_disable_reorder();
    408393        res = not_rec(r);
    409         if (!firstReorder)
    410             bdd_enable_reorder();
    411     }
    412     else
    413     {
     394        checkresize();
     395    } catch (...) {
    414396        bdd_checkreorder();
    415         if (firstReorder-- == 1)
    416             goto again;
    417         res = BDDZERO;  /* avoid warning about res being uninitialized */
    418     }
    419 
    420     checkresize();
     397        bdd_disable_reorder();
     398        res = bdd_not(r);
     399        bdd_enable_reorder();
     400    }
     401
    421402    return res;
    422403}
     
    426407{
    427408    BddCacheData *entry;
    428     BDD res;
     409    BDD res = BDDZERO;
    429410
    430411    if (ISZERO(r))
     
    499480BDD bdd_apply(BDD l, BDD r, int op)
    500481{
    501     BDD res;
    502     firstReorder = 1;
     482    BDD res = BDDZERO;
    503483
    504484    CHECKa(l, bdd_zero());
    505485    CHECKa(r, bdd_zero());
    506486
    507     if (op<0 || op>bddop_invimp)
    508     {
    509         bdd_error(BDD_OP);
    510         return bdd_zero();
    511     }
    512 
    513 again:
    514     if (setjmp(bddexception) == 0)
    515     {
     487    assert (op >= 0 && op <= bddop_invimp);
     488
     489    try {
    516490        INITREF;
    517491        applyop = op;
    518 
    519         if (!firstReorder)
    520             bdd_disable_reorder();
    521492        res = apply_rec(l, r);
    522         if (!firstReorder)
    523             bdd_enable_reorder();
    524     }
    525     else
    526     {
     493        checkresize();
     494    } catch (...) {
    527495        bdd_checkreorder();
    528 
    529         if (firstReorder-- == 1)
    530             goto again;
    531         res = BDDZERO;  /* avoid warning about res being uninitialized */
    532     }
    533 
    534     checkresize();
     496        bdd_disable_reorder();
     497        res = bdd_apply(l, r, op);
     498        bdd_enable_reorder();
     499    }
     500
    535501    return res;
    536502}
     
    540506{
    541507    BddCacheData *entry;
    542     BDD res;
    543 
    544     switch (applyop)
    545     {
    546     case bddop_and:
    547         if (l == r)
    548             return l;
    549         if (ISZERO(l)  ||  ISZERO(r))
    550             return 0;
    551         if (ISONE(l))
    552             return r;
    553         if (ISONE(r))
    554             return l;
    555         break;
    556     case bddop_or:
    557         if (l == r)
    558             return l;
    559         if (ISONE(l)  ||  ISONE(r))
    560             return 1;
    561         if (ISZERO(l))
    562             return r;
    563         if (ISZERO(r))
    564             return l;
    565         break;
    566     case bddop_xor:
    567         if (l == r)
    568             return 0;
    569         if (ISZERO(l))
    570             return r;
    571         if (ISZERO(r))
    572             return l;
    573         break;
    574     case bddop_nand:
    575         if (ISZERO(l) || ISZERO(r))
    576             return 1;
    577         break;
    578     case bddop_nor:
    579         if (ISONE(l)  ||  ISONE(r))
    580             return 0;
    581         break;
    582     case bddop_imp:
    583         if (ISZERO(l))
    584             return 1;
    585         if (ISONE(l))
    586             return r;
    587         if (ISONE(r))
    588             return 1;
    589         break;
    590     }
    591 
    592     if (ISCONST(l)  &&  ISCONST(r))
     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)) {
    593564        res = oprres[applyop][l<<1 | r];
    594     else
    595     {
     565    } else {
    596566        entry = BddCache_lookup(&applycache, APPLYHASH(l,r,applyop));
    597567
     
    607577#endif
    608578
    609         if (LEVEL(l) == LEVEL(r))
    610         {
     579        if (LEVEL(l) == LEVEL(r)) {
    611580            PUSHREF( apply_rec(LOW(l), LOW(r)) );
    612581            PUSHREF( apply_rec(HIGH(l), HIGH(r)) );
    613582            res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
    614         }
    615         else
    616             if (LEVEL(l) < LEVEL(r))
    617             {
    618                 PUSHREF( apply_rec(LOW(l), r) );
    619                 PUSHREF( apply_rec(HIGH(l), r) );
    620                 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
    621             }
    622             else
    623             {
    624                 PUSHREF( apply_rec(l, LOW(r)) );
    625                 PUSHREF( apply_rec(l, HIGH(r)) );
    626                 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
    627             }
     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        }
    628592
    629593        POPREF(2);
     
    637601    return res;
    638602}
    639 
    640 
    641 /*
    642 NAME    {* bdd\_and *}
    643 SECTION {* operator *}
    644 SHORT   {* The logical 'and' of two BDDs *}
    645 PROTO   {* BDD bdd_and(BDD l, BDD r) *}
    646 DESCR   {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_and)}. *}
    647 RETURN  {* The logical 'and' of {\tt l} and {\tt r}. *}
    648 ALSO    {* bdd\_apply, bdd\_or, bdd\_xor *}
    649 */
    650 BDD bdd_and(BDD l, BDD r)
    651 {
    652     return bdd_apply(l,r,bddop_and);
    653 }
    654 
    655 
    656 /*
    657 NAME    {* bdd\_or *}
    658 SECTION {* operator *}
    659 SHORT   {* The logical 'or' of two BDDs *}
    660 PROTO   {* BDD bdd_or(BDD l, BDD r) *}
    661 DESCR   {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_or)}. *}
    662 RETURN  {* The logical 'or' of {\tt l} and {\tt r}. *}
    663 ALSO    {* bdd\_apply, bdd\_xor, bdd\_and *}
    664 */
    665 BDD bdd_or(BDD l, BDD r)
    666 {
    667     return bdd_apply(l,r,bddop_or);
    668 }
    669 
    670 
    671 /*
    672 NAME    {* bdd\_xor *}
    673 SECTION {* operator *}
    674 SHORT   {* The logical 'xor' of two BDDs *}
    675 PROTO   {* BDD bdd_xor(BDD l, BDD r) *}
    676 DESCR   {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_xor)}. *}
    677 RETURN  {* The logical 'xor' of {\tt l} and {\tt r}. *}
    678 ALSO    {* bdd\_apply, bdd\_or, bdd\_and *}
    679 */
    680 BDD bdd_xor(BDD l, BDD r)
    681 {
    682     return bdd_apply(l,r,bddop_xor);
    683 }
    684 
    685 
    686 /*
    687 NAME    {* bdd\_imp *}
    688 SECTION {* operator *}
    689 SHORT   {* The logical 'implication' between two BDDs *}
    690 PROTO   {* BDD bdd_imp(BDD l, BDD r) *}
    691 DESCR   {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_imp)}. *}
    692 RETURN  {* The logical 'implication' of {\tt l} and {\tt r} ($l \Rightarrow r$). *}
    693 ALSO    {* bdd\_apply, bdd\_biimp *}
    694 */
    695 BDD bdd_imp(BDD l, BDD r)
    696 {
    697     return bdd_apply(l,r,bddop_imp);
    698 }
    699 
    700 
    701 /*
    702 NAME    {* bdd\_biimp *}
    703 SECTION {* operator *}
    704 SHORT   {* The logical 'bi-implication' between two BDDs *}
    705 PROTO   {* BDD bdd_biimp(BDD l, BDD r) *}
    706 DESCR   {* This a wrapper that calls {\tt bdd\_apply(l,r,bddop\_biimp)}. *}
    707 RETURN  {* The logical 'bi-implication' of {\tt l} and {\tt r} ($l \Leftrightarrow r$). *}
    708 ALSO    {* bdd\_apply, bdd\_imp *}
    709 */
    710 BDD bdd_biimp(BDD l, BDD r)
    711 {
    712     return bdd_apply(l,r,bddop_biimp);
    713 }
    714 
    715603
    716604/*=== ITE ==============================================================*/
     
    731619BDD bdd_ite(BDD f, BDD g, BDD h)
    732620{
    733     BDD res;
    734     firstReorder = 1;
     621    BDD res = BDDZERO;
    735622
    736623    CHECKa(f, bdd_zero());
     
    738625    CHECKa(h, bdd_zero());
    739626
    740 again:
    741     if (setjmp(bddexception) == 0)
    742     {
     627    try {
    743628        INITREF;
    744 
    745         if (!firstReorder)
    746             bdd_disable_reorder();
    747         res = ite_rec(f,g,h);
    748         if (!firstReorder)
    749             bdd_enable_reorder();
    750     }
    751     else
    752     {
     629        res = ite_rec(f, g, h);
     630        checkresize();
     631    } catch (...) {
    753632        bdd_checkreorder();
    754 
    755         if (firstReorder-- == 1)
    756             goto again;
    757         res = BDDZERO;  /* avoid warning about res being uninitialized */
    758     }
    759 
    760     checkresize();
     633        bdd_disable_reorder();
     634        res = bdd_ite(f, g, h);
     635        bdd_enable_reorder();
     636    }
     637
    761638    return res;
    762639}
     
    766643{
    767644    BddCacheData *entry;
    768     BDD res;
     645    BDD res = BDDZERO;
    769646
    770647    if (ISONE(f))
     
    900777BDD bdd_restrict(BDD r, BDD var)
    901778{
    902     BDD res;
    903     firstReorder = 1;
    904 
    905     CHECKa(r,bdd_zero());
    906     CHECKa(var,bdd_zero());
     779    BDD res = BDDZERO;
     780
     781    CHECKa(r, bdd_zero());
     782    CHECKa(var, bdd_zero());
    907783
    908784    if (var < 2)  /* Empty set */
    909785        return r;
    910786
    911 again:
    912     if (setjmp(bddexception) == 0)
    913     {
     787    try {
    914788        if (varset2svartable(var) < 0)
    915789            return bdd_zero();
    916 
    917790        INITREF;
    918791        miscid = (var << 3) | CACHEID_RESTRICT;
    919 
    920         if (!firstReorder)
    921             bdd_disable_reorder();
    922792        res = restrict_rec(r);
    923         if (!firstReorder)
    924             bdd_enable_reorder();
    925     }
    926     else
    927     {
     793        checkresize();
     794    } catch (...) {
    928795        bdd_checkreorder();
    929 
    930         if (firstReorder-- == 1)
    931             goto again;
    932         res = BDDZERO;  /* avoid warning about res being uninitialized */
    933     }
    934 
    935     checkresize();
     796        bdd_disable_reorder();
     797        res = bdd_restrict(r, var);
     798        bdd_enable_reorder();
     799    }
     800
    936801    return res;
    937802}
     
    995860BDD bdd_constrain(BDD f, BDD c)
    996861{
    997     BDD res;
    998     firstReorder = 1;
     862    BDD res = BDDZERO;
    999863
    1000864    CHECKa(f,bdd_zero());
    1001865    CHECKa(c,bdd_zero());
    1002866
    1003 again:
    1004     if (setjmp(bddexception) == 0)
    1005     {
     867    try {
    1006868        INITREF;
    1007869        miscid = CACHEID_CONSTRAIN;
    1008 
    1009         if (!firstReorder)
    1010             bdd_disable_reorder();
    1011870        res = constrain_rec(f, c);
    1012         if (!firstReorder)
    1013             bdd_enable_reorder();
    1014     }
    1015     else
    1016     {
     871        checkresize();
     872    } catch (...) {
    1017873        bdd_checkreorder();
    1018 
    1019         if (firstReorder-- == 1)
    1020             goto again;
    1021         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1022     }
    1023 
    1024     checkresize();
     874        bdd_disable_reorder();
     875        res = bdd_constrain(f, c);
     876        bdd_enable_reorder();
     877    }
     878
    1025879    return res;
    1026880}
     
    1030884{
    1031885    BddCacheData *entry;
    1032     BDD res;
     886    BDD res = BDDZERO;
    1033887
    1034888    if (ISONE(c))
     
    1116970BDD bdd_replace(BDD r, bddPair *pair)
    1117971{
    1118     BDD res;
    1119     firstReorder = 1;
     972    BDD res = BDDZERO;
    1120973
    1121974    CHECKa(r, bdd_zero());
    1122975
    1123 again:
    1124     if (setjmp(bddexception) == 0)
    1125     {
     976    try {
    1126977        INITREF;
    1127978        replacepair = pair->result;
    1128979        replacelast = pair->last;
    1129980        replaceid = (pair->id << 2) | CACHEID_REPLACE;
    1130 
    1131         if (!firstReorder)
    1132             bdd_disable_reorder();
    1133981        res = replace_rec(r);
    1134         if (!firstReorder)
    1135             bdd_enable_reorder();
    1136     }
    1137     else
    1138     {
     982        checkresize();
     983    } catch (...) {
    1139984        bdd_checkreorder();
    1140 
    1141         if (firstReorder-- == 1)
    1142             goto again;
    1143         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1144     }
    1145 
    1146     checkresize();
     985        bdd_disable_reorder();
     986        res = bdd_replace(r, pair);
     987        bdd_enable_reorder();
     988    }
     989
    1147990    return res;
    1148991}
     
    1152995{
    1153996    BddCacheData *entry;
    1154     BDD res;
     997    BDD res = BDDZERO;
    1155998
    1156999    if (ISCONST(r)  ||  LEVEL(r) > replacelast)
     
    11851028static BDD bdd_correctify(int level, BDD l, BDD r)
    11861029{
    1187     BDD res;
     1030    BDD res = BDDZERO;
    11881031
    11891032    if (level < LEVEL(l)  &&  level < LEVEL(r))
     
    12351078BDD bdd_compose(BDD f, BDD g, int var)
    12361079{
    1237     BDD res;
    1238     firstReorder = 1;
     1080    BDD res = BDDZERO;
    12391081
    12401082    CHECKa(f, bdd_zero());
    12411083    CHECKa(g, bdd_zero());
    1242     if (var < 0 || var >= bddvarnum)
    1243     {
     1084    if (var < 0 || var >= bddvarnum) {
    12441085        bdd_error(BDD_VAR);
    12451086        return bdd_zero();
    12461087    }
    12471088
    1248 again:
    1249     if (setjmp(bddexception) == 0)
    1250     {
     1089    try {
    12511090        INITREF;
    12521091        composelevel = bddvar2level[var];
    12531092        replaceid = (composelevel << 2) | CACHEID_COMPOSE;
    1254 
    1255         if (!firstReorder)
    1256             bdd_disable_reorder();
    12571093        res = compose_rec(f, g);
    1258         if (!firstReorder)
    1259             bdd_enable_reorder();
    1260     }
    1261     else
    1262     {
     1094        checkresize();
     1095    } catch (...) {
    12631096        bdd_checkreorder();
    1264 
    1265         if (firstReorder-- == 1)
    1266             goto again;
    1267         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1268     }
    1269 
    1270     checkresize();
     1097        bdd_disable_reorder();
     1098        res = bdd_compose(f, g, var);
     1099        bdd_enable_reorder();
     1100    }
     1101
    12711102    return res;
    12721103}
     
    12751106static BDD compose_rec(BDD f, BDD g)
    12761107{
    1277     BddCacheData *entry;
    1278     BDD res;
     1108
     1109    BDD res = BDDZERO;
    12791110
    12801111    if (LEVEL(f) > composelevel)
    12811112        return f;
    12821113
    1283     entry = BddCache_lookup(&replacecache, COMPOSEHASH(f,g));
     1114    BddCacheData * entry = BddCache_lookup(&replacecache, COMPOSEHASH(f,g));
    12841115    if (entry->a == f  &&  entry->b == g  &&  entry->c == replaceid)
    12851116    {
     
    13531184BDD bdd_veccompose(BDD f, bddPair *pair)
    13541185{
    1355     BDD res;
    1356     firstReorder = 1;
     1186    BDD res = BDDZERO;
    13571187
    13581188    CHECKa(f, bdd_zero());
    13591189
    1360 again:
    1361     if (setjmp(bddexception) == 0)
    1362     {
     1190    try {
    13631191        INITREF;
    13641192        replacepair = pair->result;
    13651193        replaceid = (pair->id << 2) | CACHEID_VECCOMPOSE;
    13661194        replacelast = pair->last;
    1367 
    1368         if (!firstReorder)
    1369             bdd_disable_reorder();
    13701195        res = veccompose_rec(f);
    1371         if (!firstReorder)
    1372             bdd_enable_reorder();
    1373     }
    1374     else
    1375     {
     1196        checkresize();
     1197    } catch (...) {
    13761198        bdd_checkreorder();
    1377 
    1378         if (firstReorder-- == 1)
    1379             goto again;
    1380         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1381     }
    1382 
    1383     checkresize();
     1199        bdd_disable_reorder();
     1200        res = bdd_veccompose(f, pair);
     1201        bdd_enable_reorder();
     1202    }
    13841203    return res;
    13851204}
     
    13891208{
    13901209    BddCacheData *entry;
    1391     BDD res;
     1210    BDD res = BDDZERO;
    13921211
    13931212    if (LEVEL(f) > replacelast)
     
    14351254BDD bdd_simplify(BDD f, BDD d)
    14361255{
    1437     BDD res;
    1438     firstReorder = 1;
     1256    BDD res = BDDZERO;
    14391257
    14401258    CHECKa(f, bdd_zero());
    14411259    CHECKa(d, bdd_zero());
    14421260
    1443 again:
    1444     if (setjmp(bddexception) == 0)
    1445     {
     1261    try {
    14461262        INITREF;
    14471263        applyop = bddop_or;
    1448 
    1449         if (!firstReorder)
    1450             bdd_disable_reorder();
    14511264        res = simplify_rec(f, d);
    1452         if (!firstReorder)
    1453             bdd_enable_reorder();
    1454     }
    1455     else
    1456     {
     1265        checkresize();
     1266    } catch (...) {
    14571267        bdd_checkreorder();
    1458 
    1459         if (firstReorder-- == 1)
    1460             goto again;
    1461         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1462     }
    1463 
    1464     checkresize();
     1268        bdd_disable_reorder();
     1269        res = bdd_simplify(f, d);
     1270        bdd_enable_reorder();
     1271    }
     1272
    14651273    return res;
    14661274}
     
    14701278{
    14711279    BddCacheData *entry;
    1472     BDD res;
     1280    BDD res = BDDZERO;
    14731281
    14741282    if (ISONE(d)  ||  ISCONST(f))
     
    15451353BDD bdd_exist(BDD r, BDD var)
    15461354{
    1547     BDD res;
    1548     firstReorder = 1;
     1355    BDD res = BDDZERO;
    15491356
    15501357    CHECKa(r, bdd_zero());
     
    15541361        return r;
    15551362
    1556 again:
    1557     if (setjmp(bddexception) == 0)
    1558     {
     1363    try {
    15591364        if (varset2vartable(var) < 0)
    15601365            return bdd_zero();
    1561 
    15621366        INITREF;
    15631367        quantid = (var << 3) | CACHEID_EXIST; /* FIXME: range */
    15641368        applyop = bddop_or;
    1565 
    1566         if (!firstReorder)
    1567             bdd_disable_reorder();
    15681369        res = quant_rec(r);
    1569         if (!firstReorder)
    1570             bdd_enable_reorder();
    1571     }
    1572     else
    1573     {
     1370        checkresize();
     1371    } catch (...) {
    15741372        bdd_checkreorder();
    1575 
    1576         if (firstReorder-- == 1)
    1577             goto again;
    1578         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1579     }
    1580 
    1581     checkresize();
     1373        bdd_disable_reorder();
     1374        res = bdd_exist(r, var);
     1375        bdd_enable_reorder();
     1376    }
     1377
    15821378    return res;
    15831379}
     
    15961392BDD bdd_forall(BDD r, BDD var)
    15971393{
    1598     BDD res;
    1599     firstReorder = 1;
     1394    BDD res = BDDZERO;
    16001395
    16011396    CHECKa(r, bdd_zero());
     
    16051400        return r;
    16061401
    1607 again:
    1608     if (setjmp(bddexception) == 0)
    1609     {
     1402    try {
    16101403        if (varset2vartable(var) < 0)
    16111404            return bdd_zero();
    1612 
    16131405        INITREF;
    16141406        quantid = (var << 3) | CACHEID_FORALL;
    16151407        applyop = bddop_and;
    1616 
    1617         if (!firstReorder)
    1618             bdd_disable_reorder();
    16191408        res = quant_rec(r);
    1620         if (!firstReorder)
    1621             bdd_enable_reorder();
    1622     }
    1623     else
    1624     {
     1409        checkresize();
     1410    } catch (...) {
    16251411        bdd_checkreorder();
    1626 
    1627         if (firstReorder-- == 1)
    1628             goto again;
    1629         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1630     }
    1631 
    1632     checkresize();
     1412        bdd_disable_reorder();
     1413        res = bdd_forall(r, var);
     1414        bdd_enable_reorder();
     1415    }
     1416
    16331417    return res;
    16341418}
     
    16501434BDD bdd_unique(BDD r, BDD var)
    16511435{
    1652     BDD res;
    1653     firstReorder = 1;
     1436    BDD res = BDDZERO;
    16541437
    16551438    CHECKa(r, bdd_zero());
     
    16591442        return r;
    16601443
    1661 again:
    1662     if (setjmp(bddexception) == 0)
    1663     {
     1444    try {
    16641445        if (varset2vartable(var) < 0)
    16651446            return bdd_zero();
    1666 
    16671447        INITREF;
    16681448        quantid = (var << 3) | CACHEID_UNIQUE;
    16691449        applyop = bddop_xor;
    1670 
    1671         if (!firstReorder)
    1672             bdd_disable_reorder();
    16731450        res = quant_rec(r);
    1674         if (!firstReorder)
    1675             bdd_enable_reorder();
    1676     }
    1677     else
    1678     {
     1451        checkresize();
     1452    } catch (...) {
    16791453        bdd_checkreorder();
    1680 
    1681         if (firstReorder-- == 1)
    1682             goto again;
    1683         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1684     }
    1685 
    1686     checkresize();
     1454        bdd_disable_reorder();
     1455        res = bdd_unique(r, var);
     1456        bdd_enable_reorder();
     1457    }
     1458
    16871459    return res;
    16881460}
     
    17491521BDD bdd_appex(BDD l, BDD r, int opr, BDD var)
    17501522{
    1751     BDD res;
    1752     firstReorder = 1;
     1523    BDD res = BDDZERO;
    17531524
    17541525    CHECKa(l, bdd_zero());
     
    17561527    CHECKa(var, bdd_zero());
    17571528
    1758     if (opr<0 || opr>bddop_invimp)
    1759     {
     1529    if (opr<0 || opr>bddop_invimp) {
    17601530        bdd_error(BDD_OP);
    17611531        return bdd_zero();
     
    17631533
    17641534    if (var < 2)  /* Empty set */
    1765         return bdd_apply(l,r,opr);
    1766 
    1767 again:
    1768     if (setjmp(bddexception) == 0)
    1769     {
     1535        return bdd_apply(l, r, opr);
     1536
     1537    try {
    17701538        if (varset2vartable(var) < 0)
    17711539            return bdd_zero();
    1772 
    17731540        INITREF;
    17741541        applyop = bddop_or;
     
    17761543        appexid = (var << 5) | (appexop << 1); /* FIXME: range! */
    17771544        quantid = (appexid << 3) | CACHEID_APPEX;
    1778 
    1779         if (!firstReorder)
    1780             bdd_disable_reorder();
    17811545        res = appquant_rec(l, r);
    1782         if (!firstReorder)
    1783             bdd_enable_reorder();
    1784     }
    1785     else
    1786     {
     1546        checkresize();
     1547    } catch (...) {
    17871548        bdd_checkreorder();
    1788 
    1789         if (firstReorder-- == 1)
    1790             goto again;
    1791         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1792     }
    1793 
    1794     checkresize();
     1549        bdd_disable_reorder();
     1550        res = bdd_appex(l, r, opr, var);
     1551        bdd_enable_reorder();
     1552    }
     1553
    17951554    return res;
    17961555}
     
    18151574BDD bdd_appall(BDD l, BDD r, int opr, BDD var)
    18161575{
    1817     BDD res;
    1818     firstReorder = 1;
     1576    BDD res = BDDZERO;
    18191577
    18201578    CHECKa(l, bdd_zero());
     
    18311589        return bdd_apply(l,r,opr);
    18321590
    1833 again:
    1834     if (setjmp(bddexception) == 0)
    1835     {
     1591    try {
    18361592        if (varset2vartable(var) < 0)
    18371593            return bdd_zero();
    1838 
    18391594        INITREF;
    18401595        applyop = bddop_and;
     
    18421597        appexid = (var << 5) | (appexop << 1) | 1; /* FIXME: range! */
    18431598        quantid = (appexid << 3) | CACHEID_APPAL;
    1844 
    1845         if (!firstReorder)
    1846             bdd_disable_reorder();
    18471599        res = appquant_rec(l, r);
    1848         if (!firstReorder)
    1849             bdd_enable_reorder();
    1850     }
    1851     else
    1852     {
     1600        checkresize();
     1601    } catch (...) {
    18531602        bdd_checkreorder();
    1854 
    1855         if (firstReorder-- == 1)
    1856             goto again;
    1857         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1858     }
    1859 
    1860     checkresize();
     1603        bdd_disable_reorder();
     1604        res = bdd_appall(l, r, opr, var);
     1605        bdd_enable_reorder();
     1606    }
     1607
    18611608    return res;
    18621609}
     
    18811628BDD bdd_appuni(BDD l, BDD r, int opr, BDD var)
    18821629{
    1883     BDD res;
    1884     firstReorder = 1;
     1630    BDD res = BDDZERO;
    18851631
    18861632    CHECKa(l, bdd_zero());
     
    18971643        return bdd_apply(l,r,opr);
    18981644
    1899 again:
    1900     if (setjmp(bddexception) == 0)
    1901     {
     1645    try {
    19021646        if (varset2vartable(var) < 0)
    19031647            return bdd_zero();
    1904 
    19051648        INITREF;
    19061649        applyop = bddop_xor;
     
    19081651        appexid = (var << 5) | (appexop << 1) | 1; /* FIXME: range! */
    19091652        quantid = (appexid << 3) | CACHEID_APPUN;
    1910 
    1911         if (!firstReorder)
    1912             bdd_disable_reorder();
    19131653        res = appquant_rec(l, r);
    1914         if (!firstReorder)
    1915             bdd_enable_reorder();
    1916     }
    1917     else
    1918     {
     1654        checkresize();
     1655    } catch (...) {
    19191656        bdd_checkreorder();
    1920 
    1921         if (firstReorder-- == 1)
    1922             goto again;
    1923         res = BDDZERO;  /* avoid warning about res being uninitialized */
    1924     }
    1925 
    1926     checkresize();
     1657        bdd_disable_reorder();
     1658        res = bdd_appuni(l, r, opr, var);
     1659        bdd_enable_reorder();
     1660    }
     1661
    19271662    return res;
    19281663}
     
    21541889BDD bdd_satone(BDD r)
    21551890{
    2156     BDD res;
     1891    BDD res = BDDZERO;
    21571892
    21581893    CHECKa(r, bdd_zero());
     
    22071942BDD bdd_satoneset(BDD r, BDD var, BDD pol)
    22081943{
    2209     BDD res;
     1944    BDD res = BDDZERO;
    22101945
    22111946    CHECKa(r, bdd_zero());
     
    22892024BDD bdd_fullsatone(BDD r)
    22902025{
    2291     BDD res;
     2026    BDD res = BDDZERO;
    22922027    int v;
    22932028
  • icGREP/icgrep-devel/buddy-2.4/src/kernel.cpp

    r4867 r4928  
    3939
    4040*************************************************************************/
    41 #include "config.h"
    4241#include <stdlib.h>
    4342#include <string.h>
     
    7877int*         bddvar2level;      /* Variable -> level table */
    7978int*         bddlevel2var;      /* Level -> variable table */
    80 jmp_buf      bddexception;      /* Long-jump point for interrupting calc. */
    8179int          bddresized;        /* Flag indicating a resize of the nodetable */
    8280
     
    130128ALSO   {* bdd\_done, bdd\_resize\_hook *}
    131129*/
    132 int bdd_init(int initnodesize, int cs)
    133 {
    134     int n, err;
     130int bdd_init(int initnodesize, int cs) {
    135131
    136132    if (bddrunning)
     
    139135    bddnodesize = bdd_prime_gte(initnodesize);
    140136
    141     if ((bddnodes=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == NULL)
     137    if ((bddnodes=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == NULL) {
    142138        return bdd_error(BDD_MEMORY);
     139    }
    143140
    144141    bddresized = 0;
    145142
    146     for (n=0 ; n<bddnodesize ; n++)
     143    for (unsigned n = 0 ; n != bddnodesize ; n++)
    147144    {
    148145        bddnodes[n].refcou = 0;
     
    158155    LOW(1) = HIGH(1) = 1;
    159156
    160     if ((err=bdd_operator_init(cs)) < 0)
    161     {
     157    const auto err = bdd_operator_init(cs);
     158    if (err < 0) {
    162159        bdd_done();
    163160        return err;
     
    184181    bddcachestats.swapCount = 0;
    185182
    186     bdd_gbc_hook(bdd_default_gbchandler);
    187183    bdd_error_hook(bdd_default_errhandler);
    188     bdd_resize_hook(NULL);
     184    bdd_gbc_hook(nullptr);
     185    bdd_resize_hook(nullptr);
    189186    bdd_pairs_init();
    190187    bdd_reorder_init();
    191     bdd_fdd_init();
    192 
    193     if (setjmp(bddexception) != 0)
    194         assert(0);
     188//    bdd_fdd_init();
    195189
    196190    return 0;
    197191}
    198192
     193void bdd_default_errhandler(int e) {
     194    throw std::runtime_error("BDD error: " + bdd_errstring(e));
     195}
    199196
    200197/*
     
    210207{
    211208    /*sanitycheck(); FIXME */
    212     bdd_fdd_done();
     209    // bdd_fdd_done();
    213210    bdd_reorder_done();
    214211    bdd_pairs_done();
     
    748745}
    749746
    750 
    751 void bdd_default_errhandler(int e) {
    752     throw std::runtime_error("BDD error: " + bdd_errstring(e));
    753 }
    754 
    755 
    756747int bdd_error(int e)
    757748{
     
    849840{
    850841    CHECK(root);
    851     if (root < 2)
     842    if (ISCONST(root)) {
    852843        return bdd_error(BDD_ILLBDD);
    853 
     844    }
    854845    return (bddlevel2var[LEVEL(root)]);
    855846}
     
    868859{
    869860    CHECK(root);
    870     if (root < 2)
     861    if (ISCONST(root)) {
    871862        return bdd_error(BDD_ILLBDD);
    872 
     863    }
    873864    return (LOW(root));
    874865}
     
    887878{
    888879    CHECK(root);
    889     if (root < 2)
     880    if (ISCONST(root)) {
    890881        return bdd_error(BDD_ILLBDD);
    891 
     882    }
    892883    return (HIGH(root));
    893884}
     
    898889  Garbage collection and node referencing
    899890*************************************************************************/
    900 
    901 void bdd_default_gbchandler(int, bddGbcStat *) { }
    902891
    903892static void bdd_gbc_rehash(void)
     
    1000989}
    1001990
    1002 
    1003991/*
    1004992NAME    {* bdd\_addref *}
     
    10131001RETURN  {* The BDD node {\tt r}. *}
    10141002*/
    1015 BDD bdd_addref(BDD root)
    1016 {
    1017     if (root < 2  ||  !bddrunning)
     1003BDD bdd_addref(BDD root) {
     1004    assert (bddrunning);
     1005    if (ISCONST(root)) {
    10181006        return root;
    1019     if (root >= bddnodesize)
     1007    }
     1008    if (LOW(root) == -1 || root >= bddnodesize) {
    10201009        return bdd_error(BDD_ILLBDD);
    1021     if (LOW(root) == -1)
    1022         return bdd_error(BDD_ILLBDD);
     1010    }
    10231011
    10241012    INCREF(root);
     
    10261014}
    10271015
     1016/*
     1017NAME    {* bdd\_addref *}
     1018SECTION {* kernel *}
     1019SHORT   {* increases the reference count on a node by n *}
     1020PROTO   {* BDD bdd_addref(BDD r) *}
     1021DESCR   {* Reference counting is done on externaly referenced nodes only
     1022           and the count for a specific node {\tt r} can and must be
     1023       increased using this function to avoid loosing the node in the next
     1024       garbage collection. *}
     1025ALSO    {* bdd\_delref *}
     1026RETURN  {* The BDD node {\tt r}. *}
     1027*/
     1028BDD bdd_addref(BDD root, unsigned int n) {
     1029    assert (bddrunning);
     1030    if (ISCONST(root)) {
     1031        return root;
     1032    }
     1033    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);
     1037    return root;
     1038}
    10281039
    10291040/*
     
    10391050RETURN  {* The BDD node {\tt r}. *}
    10401051*/
    1041 BDD bdd_delref(BDD root)
    1042 {
    1043     if (root < 2  ||  !bddrunning)
     1052BDD bdd_delref(BDD root) {
     1053    assert (bddrunning);
     1054    if (ISCONST(root)) {
    10441055        return root;
    1045     if (root >= bddnodesize)
     1056    }
     1057    if (LOW(root) == -1 || root >= bddnodesize) {
    10461058        return bdd_error(BDD_ILLBDD);
    1047     if (LOW(root) == -1)
    1048         return bdd_error(BDD_ILLBDD);
    1049 
     1059    }
    10501060    /* if the following line is present, fails there much earlier */
    10511061    if (!HASREF(root)) bdd_error(BDD_BREAK); /* distinctive */
    10521062
    10531063    DECREF(root);
     1064    return root;
     1065}
     1066
     1067/*
     1068NAME    {* bdd\_bdd_recursive\_deref *}
     1069SECTION {* kernel *}
     1070SHORT   {* recursively decreases the reference count on a node *}
     1071PROTO   {* BDD bdd_delref(BDD r) *}
     1072DESCR   {* Reference counting is done on externaly referenced nodes only
     1073           and the count for a specific node {\tt r} can and must be
     1074       decreased using this function to make it possible to reclaim the
     1075       node in the next garbage collection. *}
     1076ALSO    {* bdd\_addref *}
     1077RETURN  {* The BDD node {\tt r}. *}
     1078*/
     1079BDD bdd_recursive_deref(BDD root) {
     1080    assert (bddrunning);
     1081    if (ISCONST(root)) {
     1082        return root;
     1083    }
     1084    if (root >= bddnodesize)
     1085        return bdd_error(BDD_ILLBDD);   
     1086    BddNode * node = bddnodes + root;
     1087    if (node->low == -1)
     1088        return bdd_error(BDD_ILLBDD);
     1089    if (node->low == -1 || node->refcou == 0) {
     1090        return root;
     1091    }
     1092    if (--node->refcou == 0) {
     1093        bdd_recursive_deref(node->low);
     1094        bdd_recursive_deref(node->high);
     1095    }
    10541096    return root;
    10551097}
     
    11621204    unsigned int hash;
    11631205    int res;
     1206
     1207    assert (low >= 0);
     1208    assert (high >= 0);
    11641209
    11651210#ifdef CACHESTATS
     
    12051250        bdd_gbc();
    12061251
    1207         if ((bddnodesize-bddfreenum) >= usednodes_nextreorder  &&
    1208                 bdd_reorder_ready())
    1209         {
    1210             longjmp(bddexception,1);
     1252        if ((bddnodesize - bddfreenum) >= usednodes_nextreorder && bdd_reorder_ready()) {
     1253            throw std::runtime_error("restarting without reallocation");
    12111254        }
    12121255
     
    13051348
    13061349    /* And if very little was gained this time (< 20%) then wait until
    1307        * even more nodes (upto twice as many again) have been used */
    1308     if (bdd_reorder_gain() < 20)
    1309         usednodes_nextreorder +=
    1310                 (usednodes_nextreorder * (20-bdd_reorder_gain())) / 20;
     1350     * even more nodes (upto twice as many again) have been used */
     1351    const auto gain = bdd_reorder_gain();
     1352    if (gain < 20) {
     1353        usednodes_nextreorder += (usednodes_nextreorder * (20 - gain)) / 20;
     1354    }
    13111355}
    13121356
  • icGREP/icgrep-devel/buddy-2.4/src/kernel.h

    r4867 r4928  
    4242
    4343#include <limits.h>
    44 #include <setjmp.h>
    4544#include "bdd.h"
    4645
     
    7372    else if (r >= 2 && LOW(r) == -1)\
    7473{ bdd_error(BDD_ILLBDD); return; }
    75 
    7674
    7775/*=== SEMI-INTERNAL TYPES ==============================================*/
     
    105103extern int*      bddvar2level;
    106104extern int*      bddlevel2var;
    107 extern jmp_buf   bddexception;
    108105extern int       bddreorderdisabled;
    109106extern int       bddresized;
     
    209206extern void   bdd_pairs_vardown(int);
    210207
    211 extern void   bdd_fdd_init(void);
    212 extern void   bdd_fdd_done(void);
    213 
    214208extern void   bdd_reorder_init(void);
    215209extern void   bdd_reorder_done(void);
Note: See TracChangeset for help on using the changeset viewer.