--- oldobj/cuddObj.hh	2004-08-24 23:13:14.000000000 +0200
+++ obj/cuddObj.hh	2008-08-16 18:37:32.000000000 +0200
@@ -89,6 +89,232 @@
 
 /**Class***********************************************************************
 
+  Synopsis     [Class for CUDD managers.]
+
+  Description  []
+
+  SeeAlso      [DD]
+
+******************************************************************************/
+class Cudd {
+    friend class DD;
+    friend class ABDD;
+    friend class ADD;
+    friend class BDD;
+    friend class ZDD;
+    struct capsule {
+	DdManager *manager;
+	PFC errorHandler;
+	int verbose;
+	int ref;
+    };
+    capsule *p;
+public:
+    Cudd(
+      unsigned int numVars = 0,
+      unsigned int numVarsZ = 0,
+      unsigned int numSlots = CUDD_UNIQUE_SLOTS,
+      unsigned int cacheSize = CUDD_CACHE_SLOTS,
+      unsigned long maxMemory = 0);
+    Cudd(Cudd& x);
+    ~Cudd();
+    PFC setHandler(PFC newHandler);
+    PFC getHandler() const;
+    DdManager *getManager() const {return p->manager;}
+    inline void makeVerbose() {p->verbose = 1;}
+    inline void makeTerse() {p->verbose = 0;}
+    inline int isVerbose() const {return p->verbose;}
+    inline void checkReturnValue(const DdNode *result) const {
+        if (result == 0) {
+            if (Cudd_ReadErrorCode(p->manager) == CUDD_MEMORY_OUT) {
+                p->errorHandler("Out of memory.");
+            } else {
+                p->errorHandler("Internal error.");
+            }
+        }
+    }
+    inline void checkReturnValue(const int result) const {
+        if (result == 0) {
+            if (Cudd_ReadErrorCode(p->manager) == CUDD_MEMORY_OUT) {
+                p->errorHandler("Out of memory.");
+            } else {
+                p->errorHandler("Internal error.");
+            }
+        }
+    }
+    Cudd& operator=(const Cudd& right);
+    void info() const;
+    BDD bddVar();
+    BDD bddVar(int index);
+    BDD bddOne();
+    BDD bddZero();
+    ADD addVar();
+    ADD addVar(int index);
+    ADD addOne();
+    ADD addZero();
+    ADD constant(CUDD_VALUE_TYPE c);
+    ADD plusInfinity();
+    ADD minusInfinity();
+    ZDD zddVar(int index);
+    ZDD zddOne(int i);
+    ZDD zddZero();
+    ADD addNewVarAtLevel(int level);
+    BDD bddNewVarAtLevel(int level);
+    void zddVarsFromBddVars(int multiplicity);
+    void AutodynEnable(Cudd_ReorderingType method);
+    void AutodynDisable();
+    int ReorderingStatus(Cudd_ReorderingType * method) const;
+    void AutodynEnableZdd(Cudd_ReorderingType method);
+    void AutodynDisableZdd();
+    int ReorderingStatusZdd(Cudd_ReorderingType * method) const;
+    int zddRealignmentEnabled() const;
+    void zddRealignEnable();
+    void zddRealignDisable();
+    int bddRealignmentEnabled() const;
+    void bddRealignEnable();
+    void bddRealignDisable();
+    ADD background();
+    void SetBackground(ADD bg);
+    unsigned int ReadCacheSlots() const;
+    double ReadCacheUsedSlots() const;
+    double ReadCacheLookUps() const;
+    double ReadCacheHits() const;
+    unsigned int ReadMinHit() const;
+    void SetMinHit(unsigned int hr);
+    unsigned int ReadLooseUpTo() const;
+    void SetLooseUpTo(unsigned int lut);
+    unsigned int ReadMaxCache() const;
+    unsigned int ReadMaxCacheHard() const;
+    void SetMaxCacheHard(unsigned int mc);
+    int ReadSize() const;
+    int ReadZddSize() const;
+    unsigned int ReadSlots() const;
+    unsigned int ReadKeys() const;
+    unsigned int ReadDead() const;
+    unsigned int ReadMinDead() const;
+    int ReadReorderings() const;
+    long ReadReorderingTime() const;
+    int ReadGarbageCollections() const;
+    long ReadGarbageCollectionTime() const;
+    int ReadSiftMaxVar() const;
+    void SetSiftMaxVar(int smv);
+    int ReadSiftMaxSwap() const;
+    void SetSiftMaxSwap(int sms);
+    double ReadMaxGrowth() const;
+    void SetMaxGrowth(double mg);
+    MtrNode * ReadTree() const;
+    void SetTree(MtrNode * tree);
+    void FreeTree();
+    MtrNode * ReadZddTree() const;
+    void SetZddTree(MtrNode * tree);
+    void FreeZddTree();
+    int ReadPerm(int i) const;
+    int ReadPermZdd(int i) const;
+    int ReadInvPerm(int i) const;
+    int ReadInvPermZdd(int i) const;
+    BDD ReadVars(int i);
+    CUDD_VALUE_TYPE ReadEpsilon() const;
+    void SetEpsilon(CUDD_VALUE_TYPE ep);
+    Cudd_AggregationType ReadGroupcheck() const;
+    void SetGroupcheck(Cudd_AggregationType gc);
+    int GarbageCollectionEnabled() const;
+    void EnableGarbageCollection();
+    void DisableGarbageCollection();
+    int DeadAreCounted() const;
+    void TurnOnCountDead();
+    void TurnOffCountDead();
+    int ReadRecomb() const;
+    void SetRecomb(int recomb);
+    int ReadSymmviolation() const;
+    void SetSymmviolation(int symmviolation);
+    int ReadArcviolation() const;
+    void SetArcviolation(int arcviolation);
+    int ReadPopulationSize() const;
+    void SetPopulationSize(int populationSize);
+    int ReadNumberXovers() const;
+    void SetNumberXovers(int numberXovers);
+    unsigned long ReadMemoryInUse() const;
+    long ReadPeakNodeCount() const;
+    long ReadNodeCount() const;
+    long zddReadNodeCount() const;
+    void AddHook(DD_HFP f, Cudd_HookType where);
+    void RemoveHook(DD_HFP f, Cudd_HookType where);
+    int IsInHook(DD_HFP f, Cudd_HookType where) const;
+    void EnableReorderingReporting();
+    void DisableReorderingReporting();
+    int ReorderingReporting();
+    int ReadErrorCode() const;
+    void ClearErrorCode();
+    FILE *ReadStdout() const;
+    void SetStdout(FILE *);
+    FILE *ReadStderr() const;
+    void SetStderr(FILE *);
+    unsigned int ReadNextReordering() const;
+    double ReadSwapSteps() const;
+    unsigned int ReadMaxLive() const;
+    void SetMaxLive(unsigned int);
+    unsigned long ReadMaxMemory() const;
+    void SetMaxMemory(unsigned long);
+    int bddBindVar(int);
+    int bddUnbindVar(int);
+    int bddVarIsBound(int) const;
+    ADD Walsh(ADDvector x, ADDvector y);
+    ADD addResidue(int n, int m, int options, int top);
+    int ApaNumberOfDigits(int binaryDigits) const;
+    DdApaNumber NewApaNumber(int digits) const;
+    void ApaCopy(int digits, DdApaNumber source, DdApaNumber dest) const;
+    DdApaDigit ApaAdd(int digits, DdApaNumber a, DdApaNumber b, DdApaNumber
+		      sum) const;
+    DdApaDigit ApaSubtract(int digits, DdApaNumber a, DdApaNumber b,
+			   DdApaNumber diff) const;
+    DdApaDigit ApaShortDivision(int digits, DdApaNumber dividend, DdApaDigit
+				divisor, DdApaNumber quotient) const;
+    void ApaShiftRight(int digits, DdApaDigit in, DdApaNumber a, DdApaNumber
+		       b) const;
+    void ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal)
+      const;
+    void ApaPowerOfTwo(int digits, DdApaNumber number, int power) const;
+    void ApaPrintHex(FILE * fp, int digits, DdApaNumber number) const;
+    void ApaPrintDecimal(FILE * fp, int digits, DdApaNumber number) const;
+    void DebugCheck();
+    void CheckKeys();
+    MtrNode * MakeTreeNode(unsigned int low, unsigned int size, unsigned int type);
+    // 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);
+    void PrintLinear();
+    int ReadLinear(int x, int y);
+    BDD Xgty(BDDvector z, BDDvector x, BDDvector y);
+    BDD Xeqy(BDDvector x, BDDvector y);
+    ADD Xeqy(ADDvector x, ADDvector y);
+    BDD Dxygtdxz(BDDvector x, BDDvector y, BDDvector z);
+    BDD Dxygtdyz(BDDvector x, BDDvector y, BDDvector z);
+    ADD Hamming(ADDvector xVars, ADDvector yVars);
+    // 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);
+    // 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);
+    void ReduceHeap(Cudd_ReorderingType heuristic, int minsize);
+    void ShuffleHeap(int * permutation);
+    void SymmProfile(int lower, int upper) const;
+    unsigned int Prime(unsigned int pr) const;
+    int SharingSize(DD* nodes, int n) const;
+    BDD bddComputeCube(BDD * vars, int * phase, int n);
+    ADD addComputeCube(ADD * vars, int * phase, int n);
+    int NextNode(DdGen * gen, BDD * nnode);
+    BDD IndicesToCube(int * array, int n);
+    void PrintVersion(FILE * fp) const;
+    double AverageDistance() const;
+    long Random();
+    void Srandom(long seed);
+    MtrNode * MakeZddTreeNode(unsigned int low, unsigned int size, unsigned int type);
+    void zddPrintSubtable() const;
+    void zddReduceHeap(Cudd_ReorderingType heuristic, int minsize);
+    void zddShuffleHeap(int * permutation);
+    void zddSymmProfile(int lower, int upper) const;
+  //void DumpDot(int n, ZDD* f, char ** inames, char ** onames, FILE * fp);
+
+}; // Cudd
+
+
+/**Class***********************************************************************
+
   Synopsis     [Base class for all decision diagrams in CUDD.]
 
   Description  []
@@ -103,16 +329,73 @@
     friend class ZDD;
     Cudd *ddMgr;
     DdNode *node;
-    inline DdManager * checkSameManager(const DD &other) const;
-    inline void checkReturnValue(const DdNode *result) const;
-    inline void checkReturnValue(const int result, const int expected = 1)
-	const;
+    inline DdManager * checkSameManager(const DD &other) const {
+        DdManager *mgr = ddMgr->p->manager;
+        if (mgr != other.ddMgr->p->manager) {
+            ddMgr->p->errorHandler("Operands come from different manager.");
+        }
+        return mgr;
+    }
+    inline void checkReturnValue(const DdNode *result) const {
+        if (result == 0) {
+            DdManager *mgr = ddMgr->p->manager;
+            Cudd_ErrorType errType = Cudd_ReadErrorCode(mgr);
+            switch (errType) {
+                case CUDD_MEMORY_OUT:
+                    ddMgr->p->errorHandler("Out of memory.");
+                    break;
+                case CUDD_TOO_MANY_NODES:
+                    break;
+                case CUDD_MAX_MEM_EXCEEDED:
+                    ddMgr->p->errorHandler("Maximum memory exceeded.");
+                    break;
+                case CUDD_INVALID_ARG:
+                    ddMgr->p->errorHandler("Invalid argument.");
+                    break;
+                case CUDD_INTERNAL_ERROR:
+                    ddMgr->p->errorHandler("Internal error.");
+                    break;
+                case CUDD_NO_ERROR:
+                default:
+                    ddMgr->p->errorHandler("Unexpected error.");
+                    break;
+            }
+        }
+    }
+    inline void checkReturnValue(const int result, const int expected = 1) const {
+        if (result != expected) {
+            DdManager *mgr = ddMgr->p->manager;
+            Cudd_ErrorType errType = Cudd_ReadErrorCode(mgr);
+            switch (errType) {
+                case CUDD_MEMORY_OUT:
+                    ddMgr->p->errorHandler("Out of memory.");
+                    break;
+                case CUDD_TOO_MANY_NODES:
+                    break;
+                case CUDD_MAX_MEM_EXCEEDED:
+                    ddMgr->p->errorHandler("Maximum memory exceeded.");
+                    break;
+                case CUDD_INVALID_ARG:
+                    ddMgr->p->errorHandler("Invalid argument.");
+                    break;
+                case CUDD_INTERNAL_ERROR:
+                    ddMgr->p->errorHandler("Internal error.");
+                    break;
+                case CUDD_NO_ERROR:
+                default:
+                    ddMgr->p->errorHandler("Unexpected error.");
+                    break;
+            }
+        }
+    }
 public:
     DD(Cudd *ddManager, DdNode *ddNode);
     DD();
     DD(const DD &from);
     Cudd *manager() const;
-    inline DdNode * getNode() const;
+    inline DdNode * getNode() const {
+        return node;
+    }
     int nodeCount() const;
     unsigned int NodeReadIndex() const;
 
@@ -442,215 +725,6 @@
 }; // ZDD
 
 
-/**Class***********************************************************************
-
-  Synopsis     [Class for CUDD managers.]
-
-  Description  []
-
-  SeeAlso      [DD]
-
-******************************************************************************/
-class Cudd {
-    friend class DD;
-    friend class ABDD;
-    friend class ADD;
-    friend class BDD;
-    friend class ZDD;
-    struct capsule {
-	DdManager *manager;
-	PFC errorHandler;
-	int verbose;
-	int ref;
-    };
-    capsule *p;
-public:
-    Cudd(
-      unsigned int numVars = 0,
-      unsigned int numVarsZ = 0,
-      unsigned int numSlots = CUDD_UNIQUE_SLOTS,
-      unsigned int cacheSize = CUDD_CACHE_SLOTS,
-      unsigned long maxMemory = 0);
-    Cudd(Cudd& x);
-    ~Cudd();
-    PFC setHandler(PFC newHandler);
-    PFC getHandler() const;
-    DdManager *getManager() const {return p->manager;}
-    inline void makeVerbose() {p->verbose = 1;}
-    inline void makeTerse() {p->verbose = 0;}
-    inline int isVerbose() const {return p->verbose;}
-    inline void checkReturnValue(const DdNode *result) const;
-    inline void checkReturnValue(const int result) const;
-    Cudd& operator=(const Cudd& right);
-    void info() const;
-    BDD bddVar();
-    BDD bddVar(int index);
-    BDD bddOne();
-    BDD bddZero();
-    ADD addVar();
-    ADD addVar(int index);
-    ADD addOne();
-    ADD addZero();
-    ADD constant(CUDD_VALUE_TYPE c);
-    ADD plusInfinity();
-    ADD minusInfinity();
-    ZDD zddVar(int index);
-    ZDD zddOne(int i);
-    ZDD zddZero();
-    ADD addNewVarAtLevel(int level);
-    BDD bddNewVarAtLevel(int level);
-    void zddVarsFromBddVars(int multiplicity);
-    void AutodynEnable(Cudd_ReorderingType method);
-    void AutodynDisable();
-    int ReorderingStatus(Cudd_ReorderingType * method) const;
-    void AutodynEnableZdd(Cudd_ReorderingType method);
-    void AutodynDisableZdd();
-    int ReorderingStatusZdd(Cudd_ReorderingType * method) const;
-    int zddRealignmentEnabled() const;
-    void zddRealignEnable();
-    void zddRealignDisable();
-    int bddRealignmentEnabled() const;
-    void bddRealignEnable();
-    void bddRealignDisable();
-    ADD background();
-    void SetBackground(ADD bg);
-    unsigned int ReadCacheSlots() const;
-    double ReadCacheUsedSlots() const;
-    double ReadCacheLookUps() const;
-    double ReadCacheHits() const;
-    unsigned int ReadMinHit() const;
-    void SetMinHit(unsigned int hr);
-    unsigned int ReadLooseUpTo() const;
-    void SetLooseUpTo(unsigned int lut);
-    unsigned int ReadMaxCache() const;
-    unsigned int ReadMaxCacheHard() const;
-    void SetMaxCacheHard(unsigned int mc);
-    int ReadSize() const;
-    int ReadZddSize() const;
-    unsigned int ReadSlots() const;
-    unsigned int ReadKeys() const;
-    unsigned int ReadDead() const;
-    unsigned int ReadMinDead() const;
-    int ReadReorderings() const;
-    long ReadReorderingTime() const;
-    int ReadGarbageCollections() const;
-    long ReadGarbageCollectionTime() const;
-    int ReadSiftMaxVar() const;
-    void SetSiftMaxVar(int smv);
-    int ReadSiftMaxSwap() const;
-    void SetSiftMaxSwap(int sms);
-    double ReadMaxGrowth() const;
-    void SetMaxGrowth(double mg);
-    MtrNode * ReadTree() const;
-    void SetTree(MtrNode * tree);
-    void FreeTree();
-    MtrNode * ReadZddTree() const;
-    void SetZddTree(MtrNode * tree);
-    void FreeZddTree();
-    int ReadPerm(int i) const;
-    int ReadPermZdd(int i) const;
-    int ReadInvPerm(int i) const;
-    int ReadInvPermZdd(int i) const;
-    BDD ReadVars(int i);
-    CUDD_VALUE_TYPE ReadEpsilon() const;
-    void SetEpsilon(CUDD_VALUE_TYPE ep);
-    Cudd_AggregationType ReadGroupcheck() const;
-    void SetGroupcheck(Cudd_AggregationType gc);
-    int GarbageCollectionEnabled() const;
-    void EnableGarbageCollection();
-    void DisableGarbageCollection();
-    int DeadAreCounted() const;
-    void TurnOnCountDead();
-    void TurnOffCountDead();
-    int ReadRecomb() const;
-    void SetRecomb(int recomb);
-    int ReadSymmviolation() const;
-    void SetSymmviolation(int symmviolation);
-    int ReadArcviolation() const;
-    void SetArcviolation(int arcviolation);
-    int ReadPopulationSize() const;
-    void SetPopulationSize(int populationSize);
-    int ReadNumberXovers() const;
-    void SetNumberXovers(int numberXovers);
-    unsigned long ReadMemoryInUse() const;
-    long ReadPeakNodeCount() const;
-    long ReadNodeCount() const;
-    long zddReadNodeCount() const;
-    void AddHook(DD_HFP f, Cudd_HookType where);
-    void RemoveHook(DD_HFP f, Cudd_HookType where);
-    int IsInHook(DD_HFP f, Cudd_HookType where) const;
-    void EnableReorderingReporting();
-    void DisableReorderingReporting();
-    int ReorderingReporting();
-    int ReadErrorCode() const;
-    void ClearErrorCode();
-    FILE *ReadStdout() const;
-    void SetStdout(FILE *);
-    FILE *ReadStderr() const;
-    void SetStderr(FILE *);
-    unsigned int ReadNextReordering() const;
-    double ReadSwapSteps() const;
-    unsigned int ReadMaxLive() const;
-    void SetMaxLive(unsigned int);
-    unsigned long ReadMaxMemory() const;
-    void SetMaxMemory(unsigned long);
-    int bddBindVar(int);
-    int bddUnbindVar(int);
-    int bddVarIsBound(int) const;
-    ADD Walsh(ADDvector x, ADDvector y);
-    ADD addResidue(int n, int m, int options, int top);
-    int ApaNumberOfDigits(int binaryDigits) const;
-    DdApaNumber NewApaNumber(int digits) const;
-    void ApaCopy(int digits, DdApaNumber source, DdApaNumber dest) const;
-    DdApaDigit ApaAdd(int digits, DdApaNumber a, DdApaNumber b, DdApaNumber
-		      sum) const;
-    DdApaDigit ApaSubtract(int digits, DdApaNumber a, DdApaNumber b,
-			   DdApaNumber diff) const;
-    DdApaDigit ApaShortDivision(int digits, DdApaNumber dividend, DdApaDigit
-				divisor, DdApaNumber quotient) const;
-    void ApaShiftRight(int digits, DdApaDigit in, DdApaNumber a, DdApaNumber
-		       b) const;
-    void ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal)
-      const;
-    void ApaPowerOfTwo(int digits, DdApaNumber number, int power) const;
-    void ApaPrintHex(FILE * fp, int digits, DdApaNumber number) const;
-    void ApaPrintDecimal(FILE * fp, int digits, DdApaNumber number) const;
-    void DebugCheck();
-    void CheckKeys();
-    MtrNode * MakeTreeNode(unsigned int low, unsigned int size, unsigned int type);
-    // 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);
-    void PrintLinear();
-    int ReadLinear(int x, int y);
-    BDD Xgty(BDDvector z, BDDvector x, BDDvector y);
-    BDD Xeqy(BDDvector x, BDDvector y);
-    ADD Xeqy(ADDvector x, ADDvector y);
-    BDD Dxygtdxz(BDDvector x, BDDvector y, BDDvector z);
-    BDD Dxygtdyz(BDDvector x, BDDvector y, BDDvector z);
-    ADD Hamming(ADDvector xVars, ADDvector yVars);
-    // 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);
-    // 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);
-    void ReduceHeap(Cudd_ReorderingType heuristic, int minsize);
-    void ShuffleHeap(int * permutation);
-    void SymmProfile(int lower, int upper) const;
-    unsigned int Prime(unsigned int pr) const;
-    int SharingSize(DD* nodes, int n) const;
-    BDD bddComputeCube(BDD * vars, int * phase, int n);
-    ADD addComputeCube(ADD * vars, int * phase, int n);
-    int NextNode(DdGen * gen, BDD * nnode);
-    BDD IndicesToCube(int * array, int n);
-    void PrintVersion(FILE * fp) const;
-    double AverageDistance() const;
-    long Random();
-    void Srandom(long seed);
-    MtrNode * MakeZddTreeNode(unsigned int low, unsigned int size, unsigned int type);
-    void zddPrintSubtable() const;
-    void zddReduceHeap(Cudd_ReorderingType heuristic, int minsize);
-    void zddShuffleHeap(int * permutation);
-    void zddSymmProfile(int lower, int upper) const;
-  //void DumpDot(int n, ZDD* f, char ** inames, char ** onames, FILE * fp);
-
-}; // Cudd
-
 
 /**Class***********************************************************************
 
