Ticket #16210: patch-obj-cuddObj.hh.diff

File patch-obj-cuddObj.hh.diff, 19.9 KB (added by mij@…, 16 years ago)

  • cuddObj.hh

    old new  
    8989
    9090/**Class***********************************************************************
    9191
     92  Synopsis     [Class for CUDD managers.]
     93
     94  Description  []
     95
     96  SeeAlso      [DD]
     97
     98******************************************************************************/
     99class Cudd {
     100    friend class DD;
     101    friend class ABDD;
     102    friend class ADD;
     103    friend class BDD;
     104    friend class ZDD;
     105    struct capsule {
     106        DdManager *manager;
     107        PFC errorHandler;
     108        int verbose;
     109        int ref;
     110    };
     111    capsule *p;
     112public:
     113    Cudd(
     114      unsigned int numVars = 0,
     115      unsigned int numVarsZ = 0,
     116      unsigned int numSlots = CUDD_UNIQUE_SLOTS,
     117      unsigned int cacheSize = CUDD_CACHE_SLOTS,
     118      unsigned long maxMemory = 0);
     119    Cudd(Cudd& x);
     120    ~Cudd();
     121    PFC setHandler(PFC newHandler);
     122    PFC getHandler() const;
     123    DdManager *getManager() const {return p->manager;}
     124    inline void makeVerbose() {p->verbose = 1;}
     125    inline void makeTerse() {p->verbose = 0;}
     126    inline int isVerbose() const {return p->verbose;}
     127    inline void checkReturnValue(const DdNode *result) const {
     128        if (result == 0) {
     129            if (Cudd_ReadErrorCode(p->manager) == CUDD_MEMORY_OUT) {
     130                p->errorHandler("Out of memory.");
     131            } else {
     132                p->errorHandler("Internal error.");
     133            }
     134        }
     135    }
     136    inline void checkReturnValue(const int result) const {
     137        if (result == 0) {
     138            if (Cudd_ReadErrorCode(p->manager) == CUDD_MEMORY_OUT) {
     139                p->errorHandler("Out of memory.");
     140            } else {
     141                p->errorHandler("Internal error.");
     142            }
     143        }
     144    }
     145    Cudd& operator=(const Cudd& right);
     146    void info() const;
     147    BDD bddVar();
     148    BDD bddVar(int index);
     149    BDD bddOne();
     150    BDD bddZero();
     151    ADD addVar();
     152    ADD addVar(int index);
     153    ADD addOne();
     154    ADD addZero();
     155    ADD constant(CUDD_VALUE_TYPE c);
     156    ADD plusInfinity();
     157    ADD minusInfinity();
     158    ZDD zddVar(int index);
     159    ZDD zddOne(int i);
     160    ZDD zddZero();
     161    ADD addNewVarAtLevel(int level);
     162    BDD bddNewVarAtLevel(int level);
     163    void zddVarsFromBddVars(int multiplicity);
     164    void AutodynEnable(Cudd_ReorderingType method);
     165    void AutodynDisable();
     166    int ReorderingStatus(Cudd_ReorderingType * method) const;
     167    void AutodynEnableZdd(Cudd_ReorderingType method);
     168    void AutodynDisableZdd();
     169    int ReorderingStatusZdd(Cudd_ReorderingType * method) const;
     170    int zddRealignmentEnabled() const;
     171    void zddRealignEnable();
     172    void zddRealignDisable();
     173    int bddRealignmentEnabled() const;
     174    void bddRealignEnable();
     175    void bddRealignDisable();
     176    ADD background();
     177    void SetBackground(ADD bg);
     178    unsigned int ReadCacheSlots() const;
     179    double ReadCacheUsedSlots() const;
     180    double ReadCacheLookUps() const;
     181    double ReadCacheHits() const;
     182    unsigned int ReadMinHit() const;
     183    void SetMinHit(unsigned int hr);
     184    unsigned int ReadLooseUpTo() const;
     185    void SetLooseUpTo(unsigned int lut);
     186    unsigned int ReadMaxCache() const;
     187    unsigned int ReadMaxCacheHard() const;
     188    void SetMaxCacheHard(unsigned int mc);
     189    int ReadSize() const;
     190    int ReadZddSize() const;
     191    unsigned int ReadSlots() const;
     192    unsigned int ReadKeys() const;
     193    unsigned int ReadDead() const;
     194    unsigned int ReadMinDead() const;
     195    int ReadReorderings() const;
     196    long ReadReorderingTime() const;
     197    int ReadGarbageCollections() const;
     198    long ReadGarbageCollectionTime() const;
     199    int ReadSiftMaxVar() const;
     200    void SetSiftMaxVar(int smv);
     201    int ReadSiftMaxSwap() const;
     202    void SetSiftMaxSwap(int sms);
     203    double ReadMaxGrowth() const;
     204    void SetMaxGrowth(double mg);
     205    MtrNode * ReadTree() const;
     206    void SetTree(MtrNode * tree);
     207    void FreeTree();
     208    MtrNode * ReadZddTree() const;
     209    void SetZddTree(MtrNode * tree);
     210    void FreeZddTree();
     211    int ReadPerm(int i) const;
     212    int ReadPermZdd(int i) const;
     213    int ReadInvPerm(int i) const;
     214    int ReadInvPermZdd(int i) const;
     215    BDD ReadVars(int i);
     216    CUDD_VALUE_TYPE ReadEpsilon() const;
     217    void SetEpsilon(CUDD_VALUE_TYPE ep);
     218    Cudd_AggregationType ReadGroupcheck() const;
     219    void SetGroupcheck(Cudd_AggregationType gc);
     220    int GarbageCollectionEnabled() const;
     221    void EnableGarbageCollection();
     222    void DisableGarbageCollection();
     223    int DeadAreCounted() const;
     224    void TurnOnCountDead();
     225    void TurnOffCountDead();
     226    int ReadRecomb() const;
     227    void SetRecomb(int recomb);
     228    int ReadSymmviolation() const;
     229    void SetSymmviolation(int symmviolation);
     230    int ReadArcviolation() const;
     231    void SetArcviolation(int arcviolation);
     232    int ReadPopulationSize() const;
     233    void SetPopulationSize(int populationSize);
     234    int ReadNumberXovers() const;
     235    void SetNumberXovers(int numberXovers);
     236    unsigned long ReadMemoryInUse() const;
     237    long ReadPeakNodeCount() const;
     238    long ReadNodeCount() const;
     239    long zddReadNodeCount() const;
     240    void AddHook(DD_HFP f, Cudd_HookType where);
     241    void RemoveHook(DD_HFP f, Cudd_HookType where);
     242    int IsInHook(DD_HFP f, Cudd_HookType where) const;
     243    void EnableReorderingReporting();
     244    void DisableReorderingReporting();
     245    int ReorderingReporting();
     246    int ReadErrorCode() const;
     247    void ClearErrorCode();
     248    FILE *ReadStdout() const;
     249    void SetStdout(FILE *);
     250    FILE *ReadStderr() const;
     251    void SetStderr(FILE *);
     252    unsigned int ReadNextReordering() const;
     253    double ReadSwapSteps() const;
     254    unsigned int ReadMaxLive() const;
     255    void SetMaxLive(unsigned int);
     256    unsigned long ReadMaxMemory() const;
     257    void SetMaxMemory(unsigned long);
     258    int bddBindVar(int);
     259    int bddUnbindVar(int);
     260    int bddVarIsBound(int) const;
     261    ADD Walsh(ADDvector x, ADDvector y);
     262    ADD addResidue(int n, int m, int options, int top);
     263    int ApaNumberOfDigits(int binaryDigits) const;
     264    DdApaNumber NewApaNumber(int digits) const;
     265    void ApaCopy(int digits, DdApaNumber source, DdApaNumber dest) const;
     266    DdApaDigit ApaAdd(int digits, DdApaNumber a, DdApaNumber b, DdApaNumber
     267                      sum) const;
     268    DdApaDigit ApaSubtract(int digits, DdApaNumber a, DdApaNumber b,
     269                           DdApaNumber diff) const;
     270    DdApaDigit ApaShortDivision(int digits, DdApaNumber dividend, DdApaDigit
     271                                divisor, DdApaNumber quotient) const;
     272    void ApaShiftRight(int digits, DdApaDigit in, DdApaNumber a, DdApaNumber
     273                       b) const;
     274    void ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal)
     275      const;
     276    void ApaPowerOfTwo(int digits, DdApaNumber number, int power) const;
     277    void ApaPrintHex(FILE * fp, int digits, DdApaNumber number) const;
     278    void ApaPrintDecimal(FILE * fp, int digits, DdApaNumber number) const;
     279    void DebugCheck();
     280    void CheckKeys();
     281    MtrNode * MakeTreeNode(unsigned int low, unsigned int size, unsigned int type);
     282    // void Harwell(FILE * fp, ADD* E, ADD** x, ADD** y, ADD** xn, ADD** yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy, int pr);
     283    void PrintLinear();
     284    int ReadLinear(int x, int y);
     285    BDD Xgty(BDDvector z, BDDvector x, BDDvector y);
     286    BDD Xeqy(BDDvector x, BDDvector y);
     287    ADD Xeqy(ADDvector x, ADDvector y);
     288    BDD Dxygtdxz(BDDvector x, BDDvector y, BDDvector z);
     289    BDD Dxygtdyz(BDDvector x, BDDvector y, BDDvector z);
     290    ADD Hamming(ADDvector xVars, ADDvector yVars);
     291    // void Read(FILE * fp, ADD* E, ADD** x, ADD** y, ADD** xn, ADD** yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy);
     292    // void Read(FILE * fp, BDD* E, BDD** x, BDD** y, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy);
     293    void ReduceHeap(Cudd_ReorderingType heuristic, int minsize);
     294    void ShuffleHeap(int * permutation);
     295    void SymmProfile(int lower, int upper) const;
     296    unsigned int Prime(unsigned int pr) const;
     297    int SharingSize(DD* nodes, int n) const;
     298    BDD bddComputeCube(BDD * vars, int * phase, int n);
     299    ADD addComputeCube(ADD * vars, int * phase, int n);
     300    int NextNode(DdGen * gen, BDD * nnode);
     301    BDD IndicesToCube(int * array, int n);
     302    void PrintVersion(FILE * fp) const;
     303    double AverageDistance() const;
     304    long Random();
     305    void Srandom(long seed);
     306    MtrNode * MakeZddTreeNode(unsigned int low, unsigned int size, unsigned int type);
     307    void zddPrintSubtable() const;
     308    void zddReduceHeap(Cudd_ReorderingType heuristic, int minsize);
     309    void zddShuffleHeap(int * permutation);
     310    void zddSymmProfile(int lower, int upper) const;
     311  //void DumpDot(int n, ZDD* f, char ** inames, char ** onames, FILE * fp);
     312
     313}; // Cudd
     314
     315
     316/**Class***********************************************************************
     317
    92318  Synopsis     [Base class for all decision diagrams in CUDD.]
    93319
    94320  Description  []
    … …  
    103329    friend class ZDD;
    104330    Cudd *ddMgr;
    105331    DdNode *node;
    106     inline DdManager * checkSameManager(const DD &other) const;
    107     inline void checkReturnValue(const DdNode *result) const;
    108     inline void checkReturnValue(const int result, const int expected = 1)
    109         const;
     332    inline DdManager * checkSameManager(const DD &other) const {
     333        DdManager *mgr = ddMgr->p->manager;
     334        if (mgr != other.ddMgr->p->manager) {
     335            ddMgr->p->errorHandler("Operands come from different manager.");
     336        }
     337        return mgr;
     338    }
     339    inline void checkReturnValue(const DdNode *result) const {
     340        if (result == 0) {
     341            DdManager *mgr = ddMgr->p->manager;
     342            Cudd_ErrorType errType = Cudd_ReadErrorCode(mgr);
     343            switch (errType) {
     344                case CUDD_MEMORY_OUT:
     345                    ddMgr->p->errorHandler("Out of memory.");
     346                    break;
     347                case CUDD_TOO_MANY_NODES:
     348                    break;
     349                case CUDD_MAX_MEM_EXCEEDED:
     350                    ddMgr->p->errorHandler("Maximum memory exceeded.");
     351                    break;
     352                case CUDD_INVALID_ARG:
     353                    ddMgr->p->errorHandler("Invalid argument.");
     354                    break;
     355                case CUDD_INTERNAL_ERROR:
     356                    ddMgr->p->errorHandler("Internal error.");
     357                    break;
     358                case CUDD_NO_ERROR:
     359                default:
     360                    ddMgr->p->errorHandler("Unexpected error.");
     361                    break;
     362            }
     363        }
     364    }
     365    inline void checkReturnValue(const int result, const int expected = 1) const {
     366        if (result != expected) {
     367            DdManager *mgr = ddMgr->p->manager;
     368            Cudd_ErrorType errType = Cudd_ReadErrorCode(mgr);
     369            switch (errType) {
     370                case CUDD_MEMORY_OUT:
     371                    ddMgr->p->errorHandler("Out of memory.");
     372                    break;
     373                case CUDD_TOO_MANY_NODES:
     374                    break;
     375                case CUDD_MAX_MEM_EXCEEDED:
     376                    ddMgr->p->errorHandler("Maximum memory exceeded.");
     377                    break;
     378                case CUDD_INVALID_ARG:
     379                    ddMgr->p->errorHandler("Invalid argument.");
     380                    break;
     381                case CUDD_INTERNAL_ERROR:
     382                    ddMgr->p->errorHandler("Internal error.");
     383                    break;
     384                case CUDD_NO_ERROR:
     385                default:
     386                    ddMgr->p->errorHandler("Unexpected error.");
     387                    break;
     388            }
     389        }
     390    }
    110391public:
    111392    DD(Cudd *ddManager, DdNode *ddNode);
    112393    DD();
    113394    DD(const DD &from);
    114395    Cudd *manager() const;
    115     inline DdNode * getNode() const;
     396    inline DdNode * getNode() const {
     397        return node;
     398    }
    116399    int nodeCount() const;
    117400    unsigned int NodeReadIndex() const;
    118401
    … …  
    442725}; // ZDD
    443726
    444727
    445 /**Class***********************************************************************
    446 
    447   Synopsis     [Class for CUDD managers.]
    448 
    449   Description  []
    450 
    451   SeeAlso      [DD]
    452 
    453 ******************************************************************************/
    454 class Cudd {
    455     friend class DD;
    456     friend class ABDD;
    457     friend class ADD;
    458     friend class BDD;
    459     friend class ZDD;
    460     struct capsule {
    461         DdManager *manager;
    462         PFC errorHandler;
    463         int verbose;
    464         int ref;
    465     };
    466     capsule *p;
    467 public:
    468     Cudd(
    469       unsigned int numVars = 0,
    470       unsigned int numVarsZ = 0,
    471       unsigned int numSlots = CUDD_UNIQUE_SLOTS,
    472       unsigned int cacheSize = CUDD_CACHE_SLOTS,
    473       unsigned long maxMemory = 0);
    474     Cudd(Cudd& x);
    475     ~Cudd();
    476     PFC setHandler(PFC newHandler);
    477     PFC getHandler() const;
    478     DdManager *getManager() const {return p->manager;}
    479     inline void makeVerbose() {p->verbose = 1;}
    480     inline void makeTerse() {p->verbose = 0;}
    481     inline int isVerbose() const {return p->verbose;}
    482     inline void checkReturnValue(const DdNode *result) const;
    483     inline void checkReturnValue(const int result) const;
    484     Cudd& operator=(const Cudd& right);
    485     void info() const;
    486     BDD bddVar();
    487     BDD bddVar(int index);
    488     BDD bddOne();
    489     BDD bddZero();
    490     ADD addVar();
    491     ADD addVar(int index);
    492     ADD addOne();
    493     ADD addZero();
    494     ADD constant(CUDD_VALUE_TYPE c);
    495     ADD plusInfinity();
    496     ADD minusInfinity();
    497     ZDD zddVar(int index);
    498     ZDD zddOne(int i);
    499     ZDD zddZero();
    500     ADD addNewVarAtLevel(int level);
    501     BDD bddNewVarAtLevel(int level);
    502     void zddVarsFromBddVars(int multiplicity);
    503     void AutodynEnable(Cudd_ReorderingType method);
    504     void AutodynDisable();
    505     int ReorderingStatus(Cudd_ReorderingType * method) const;
    506     void AutodynEnableZdd(Cudd_ReorderingType method);
    507     void AutodynDisableZdd();
    508     int ReorderingStatusZdd(Cudd_ReorderingType * method) const;
    509     int zddRealignmentEnabled() const;
    510     void zddRealignEnable();
    511     void zddRealignDisable();
    512     int bddRealignmentEnabled() const;
    513     void bddRealignEnable();
    514     void bddRealignDisable();
    515     ADD background();
    516     void SetBackground(ADD bg);
    517     unsigned int ReadCacheSlots() const;
    518     double ReadCacheUsedSlots() const;
    519     double ReadCacheLookUps() const;
    520     double ReadCacheHits() const;
    521     unsigned int ReadMinHit() const;
    522     void SetMinHit(unsigned int hr);
    523     unsigned int ReadLooseUpTo() const;
    524     void SetLooseUpTo(unsigned int lut);
    525     unsigned int ReadMaxCache() const;
    526     unsigned int ReadMaxCacheHard() const;
    527     void SetMaxCacheHard(unsigned int mc);
    528     int ReadSize() const;
    529     int ReadZddSize() const;
    530     unsigned int ReadSlots() const;
    531     unsigned int ReadKeys() const;
    532     unsigned int ReadDead() const;
    533     unsigned int ReadMinDead() const;
    534     int ReadReorderings() const;
    535     long ReadReorderingTime() const;
    536     int ReadGarbageCollections() const;
    537     long ReadGarbageCollectionTime() const;
    538     int ReadSiftMaxVar() const;
    539     void SetSiftMaxVar(int smv);
    540     int ReadSiftMaxSwap() const;
    541     void SetSiftMaxSwap(int sms);
    542     double ReadMaxGrowth() const;
    543     void SetMaxGrowth(double mg);
    544     MtrNode * ReadTree() const;
    545     void SetTree(MtrNode * tree);
    546     void FreeTree();
    547     MtrNode * ReadZddTree() const;
    548     void SetZddTree(MtrNode * tree);
    549     void FreeZddTree();
    550     int ReadPerm(int i) const;
    551     int ReadPermZdd(int i) const;
    552     int ReadInvPerm(int i) const;
    553     int ReadInvPermZdd(int i) const;
    554     BDD ReadVars(int i);
    555     CUDD_VALUE_TYPE ReadEpsilon() const;
    556     void SetEpsilon(CUDD_VALUE_TYPE ep);
    557     Cudd_AggregationType ReadGroupcheck() const;
    558     void SetGroupcheck(Cudd_AggregationType gc);
    559     int GarbageCollectionEnabled() const;
    560     void EnableGarbageCollection();
    561     void DisableGarbageCollection();
    562     int DeadAreCounted() const;
    563     void TurnOnCountDead();
    564     void TurnOffCountDead();
    565     int ReadRecomb() const;
    566     void SetRecomb(int recomb);
    567     int ReadSymmviolation() const;
    568     void SetSymmviolation(int symmviolation);
    569     int ReadArcviolation() const;
    570     void SetArcviolation(int arcviolation);
    571     int ReadPopulationSize() const;
    572     void SetPopulationSize(int populationSize);
    573     int ReadNumberXovers() const;
    574     void SetNumberXovers(int numberXovers);
    575     unsigned long ReadMemoryInUse() const;
    576     long ReadPeakNodeCount() const;
    577     long ReadNodeCount() const;
    578     long zddReadNodeCount() const;
    579     void AddHook(DD_HFP f, Cudd_HookType where);
    580     void RemoveHook(DD_HFP f, Cudd_HookType where);
    581     int IsInHook(DD_HFP f, Cudd_HookType where) const;
    582     void EnableReorderingReporting();
    583     void DisableReorderingReporting();
    584     int ReorderingReporting();
    585     int ReadErrorCode() const;
    586     void ClearErrorCode();
    587     FILE *ReadStdout() const;
    588     void SetStdout(FILE *);
    589     FILE *ReadStderr() const;
    590     void SetStderr(FILE *);
    591     unsigned int ReadNextReordering() const;
    592     double ReadSwapSteps() const;
    593     unsigned int ReadMaxLive() const;
    594     void SetMaxLive(unsigned int);
    595     unsigned long ReadMaxMemory() const;
    596     void SetMaxMemory(unsigned long);
    597     int bddBindVar(int);
    598     int bddUnbindVar(int);
    599     int bddVarIsBound(int) const;
    600     ADD Walsh(ADDvector x, ADDvector y);
    601     ADD addResidue(int n, int m, int options, int top);
    602     int ApaNumberOfDigits(int binaryDigits) const;
    603     DdApaNumber NewApaNumber(int digits) const;
    604     void ApaCopy(int digits, DdApaNumber source, DdApaNumber dest) const;
    605     DdApaDigit ApaAdd(int digits, DdApaNumber a, DdApaNumber b, DdApaNumber
    606                       sum) const;
    607     DdApaDigit ApaSubtract(int digits, DdApaNumber a, DdApaNumber b,
    608                            DdApaNumber diff) const;
    609     DdApaDigit ApaShortDivision(int digits, DdApaNumber dividend, DdApaDigit
    610                                 divisor, DdApaNumber quotient) const;
    611     void ApaShiftRight(int digits, DdApaDigit in, DdApaNumber a, DdApaNumber
    612                        b) const;
    613     void ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal)
    614       const;
    615     void ApaPowerOfTwo(int digits, DdApaNumber number, int power) const;
    616     void ApaPrintHex(FILE * fp, int digits, DdApaNumber number) const;
    617     void ApaPrintDecimal(FILE * fp, int digits, DdApaNumber number) const;
    618     void DebugCheck();
    619     void CheckKeys();
    620     MtrNode * MakeTreeNode(unsigned int low, unsigned int size, unsigned int type);
    621     // void Harwell(FILE * fp, ADD* E, ADD** x, ADD** y, ADD** xn, ADD** yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy, int pr);
    622     void PrintLinear();
    623     int ReadLinear(int x, int y);
    624     BDD Xgty(BDDvector z, BDDvector x, BDDvector y);
    625     BDD Xeqy(BDDvector x, BDDvector y);
    626     ADD Xeqy(ADDvector x, ADDvector y);
    627     BDD Dxygtdxz(BDDvector x, BDDvector y, BDDvector z);
    628     BDD Dxygtdyz(BDDvector x, BDDvector y, BDDvector z);
    629     ADD Hamming(ADDvector xVars, ADDvector yVars);
    630     // void Read(FILE * fp, ADD* E, ADD** x, ADD** y, ADD** xn, ADD** yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy);
    631     // void Read(FILE * fp, BDD* E, BDD** x, BDD** y, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy);
    632     void ReduceHeap(Cudd_ReorderingType heuristic, int minsize);
    633     void ShuffleHeap(int * permutation);
    634     void SymmProfile(int lower, int upper) const;
    635     unsigned int Prime(unsigned int pr) const;
    636     int SharingSize(DD* nodes, int n) const;
    637     BDD bddComputeCube(BDD * vars, int * phase, int n);
    638     ADD addComputeCube(ADD * vars, int * phase, int n);
    639     int NextNode(DdGen * gen, BDD * nnode);
    640     BDD IndicesToCube(int * array, int n);
    641     void PrintVersion(FILE * fp) const;
    642     double AverageDistance() const;
    643     long Random();
    644     void Srandom(long seed);
    645     MtrNode * MakeZddTreeNode(unsigned int low, unsigned int size, unsigned int type);
    646     void zddPrintSubtable() const;
    647     void zddReduceHeap(Cudd_ReorderingType heuristic, int minsize);
    648     void zddShuffleHeap(int * permutation);
    649     void zddSymmProfile(int lower, int upper) const;
    650   //void DumpDot(int n, ZDD* f, char ** inames, char ** onames, FILE * fp);
    651 
    652 }; // Cudd
    653 
    654728
    655729/**Class***********************************************************************
    656730