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

File patch-obj-cuddObj.cc.diff, 2.7 KB (added by mij@…, 16 years ago)
  • cuddObj.cc

    old new  
    9494} // DD::DD
    9595
    9696
    97 inline DdManager *
    98 DD::checkSameManager(
    99   const DD &other) const
    100 {
    101     DdManager *mgr = ddMgr->p->manager;
    102     if (mgr != other.ddMgr->p->manager) {
    103         ddMgr->p->errorHandler("Operands come from different manager.");
    104     }
    105     return mgr;
    106 
    107 } // DD::checkSameManager
    108 
    109 
    110 inline void
    111 DD::checkReturnValue(
    112   const DdNode *result) const
    113 {
    114     if (result == 0) {
    115         DdManager *mgr = ddMgr->p->manager;
    116         Cudd_ErrorType errType = Cudd_ReadErrorCode(mgr);
    117         switch (errType) {
    118         CUDD_MEMORY_OUT:
    119             ddMgr->p->errorHandler("Out of memory.");
    120             break;
    121         CUDD_TOO_MANY_NODES:
    122             break;
    123         CUDD_MAX_MEM_EXCEEDED:
    124             ddMgr->p->errorHandler("Maximum memory exceeded.");
    125             break;
    126         CUDD_INVALID_ARG:
    127             ddMgr->p->errorHandler("Invalid argument.");
    128             break;
    129         CUDD_INTERNAL_ERROR:
    130             ddMgr->p->errorHandler("Internal error.");
    131             break;
    132         CUDD_NO_ERROR:
    133         default:
    134             ddMgr->p->errorHandler("Unexpected error.");
    135             break;
    136         }
    137     }
    138 
    139 } // DD::checkReturnValue
    140 
    141 
    142 inline void
    143 DD::checkReturnValue(
    144   const int result,
    145   const int expected) const
    146 {
    147     if (result != expected) {
    148         DdManager *mgr = ddMgr->p->manager;
    149         Cudd_ErrorType errType = Cudd_ReadErrorCode(mgr);
    150         switch (errType) {
    151         CUDD_MEMORY_OUT:
    152             ddMgr->p->errorHandler("Out of memory.");
    153             break;
    154         CUDD_TOO_MANY_NODES:
    155             break;
    156         CUDD_MAX_MEM_EXCEEDED:
    157             ddMgr->p->errorHandler("Maximum memory exceeded.");
    158             break;
    159         CUDD_INVALID_ARG:
    160             ddMgr->p->errorHandler("Invalid argument.");
    161             break;
    162         CUDD_INTERNAL_ERROR:
    163             ddMgr->p->errorHandler("Internal error.");
    164             break;
    165         CUDD_NO_ERROR:
    166         default:
    167             ddMgr->p->errorHandler("Unexpected error.");
    168             break;
    169         }
    170     }
    171 
    172 } // DD::checkReturnValue
    173 
    174 
    17597Cudd *
    17698DD::manager() const
    17799{
     
    180102} // DD::manager
    181103
    182104
    183 inline DdNode *
    184 DD::getNode() const
    185 {
    186     return node;
    187 
    188 } // DD::getNode
    189 
    190 
    191105int
    192106DD::nodeCount() const
    193107{
     
    10971011} // Cudd::getHandler
    10981012
    10991013
    1100 inline void
    1101 Cudd::checkReturnValue(
    1102   const DdNode *result) const
    1103 {
    1104     if (result == 0) {
    1105         if (Cudd_ReadErrorCode(p->manager) == CUDD_MEMORY_OUT) {
    1106             p->errorHandler("Out of memory.");
    1107         } else {
    1108             p->errorHandler("Internal error.");
    1109         }
    1110     }
    1111 
    1112 } // Cudd::checkReturnValue
    1113 
    1114 
    1115 inline void
    1116 Cudd::checkReturnValue(
    1117   const int result) const
    1118 {
    1119     if (result == 0) {
    1120         if (Cudd_ReadErrorCode(p->manager) == CUDD_MEMORY_OUT) {
    1121             p->errorHandler("Out of memory.");
    1122         } else {
    1123             p->errorHandler("Internal error.");
    1124         }
    1125     }
    1126 
    1127 } // Cudd::checkReturnValue
    1128 
    1129 
    11301014void
    11311015Cudd::info() const
    11321016{