Merge remote-tracking branch 'origin/beta'

CMakeLists.txt

@@ -20,12 +20,12 @@ set(SOURCES	"src/lruzdd.cpp"
 
 )
 
-add_subdirectory(cudd)
-add_subdirectory(extra)
-
 # script
 project(${PLUGIN})
 
+add_subdirectory(cudd)
+add_subdirectory(extra)
+
 # look for OTAWA
 if(NOT OTAWA_CONFIG)
     find_program(OTAWA_CONFIG otawa-config DOC "path to otawa-config")
@@ -56,14 +56,15 @@ add_library(${PLUGIN} SHARED ${SOURCES})
 set_property(TARGET ${PLUGIN} PROPERTY PREFIX "")
 set_property(TARGET ${PLUGIN} PROPERTY COMPILE_FLAGS "${OTAWA_CFLAGS} --std=c++11 -g -Wall -Wextra -pedantic")
 
-add_dependencies(${PLUGIN} libcudd)
-add_dependencies(${PLUGIN} libextra)
+add_dependencies(${PLUGIN} cudd)
+add_dependencies(${PLUGIN} extra)
 
 target_include_directories(${PLUGIN} PUBLIC "${CMAKE_SOURCE_DIR}/include")
-target_link_libraries(${PLUGIN} PUBLIC "${OTAWA_LDFLAGS}" cudd_core cudd_epd cudd_st cudd_util extra)
+target_link_libraries(${PLUGIN} PUBLIC "${OTAWA_LDFLAGS}" cudd extra)
 
 # installation
 set(PLUGIN_PATH "${OTAWA_PREFIX}/lib/otawa/${NAMESPACE}")
 install(TARGETS ${PLUGIN} LIBRARY DESTINATION ${PLUGIN_PATH})
 install(DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/include/lruzdd" DESTINATION "${OTAWA_PREFIX}/include")
 install(FILES ${PLUGIN}.eld DESTINATION ${PLUGIN_PATH})
+

cudd/CMakeLists.txt

-set(CUDD_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/cudd/libcudd.a)
-set(EPD_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/epd/libepd.a)
-set(ST_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/st/libst.a)
-set(UTIL_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/util/libutil.a)
+set(CUDD_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/cudd/lib/libcudd.a)
 
 add_custom_command(
 	OUTPUT ${CUDD_LIB_FILE}
-	COMMAND ${CMAKE_COMMAND} -E tar xzf ${CMAKE_CURRENT_SOURCE_DIR}/cudd-2.3.1.tar.gz
-	COMMAND patch -p0 -i ${CMAKE_CURRENT_SOURCE_DIR}/cudd-2.3.1.patch
-	COMMAND cd cudd-2.3.1 && rm -r include
-	COMMAND cd cudd-2.3.1 && ./setup.sh
-	COMMAND make -C cudd-2.3.1
+	COMMAND rm -rf cudd
+	COMMAND git clone https://github.com/kozross/cudd
+	COMMAND cd cudd && autoreconf -i
+	COMMAND cd cudd && ./configure CC=${CMAKE_C_COMPILER} CFLAGS=-fPIC --prefix=${CMAKE_CURRENT_BINARY_DIR}/cudd
+	COMMAND make -C cudd
+	COMMAND make -C cudd install
 	WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/
 )
 
@@ -18,45 +16,24 @@ add_custom_target(
 	DEPENDS ${CUDD_LIB_FILE}
 )
 
-#add_custom_target(
-#	compile_cudd
-#	COMMAND ${CMAKE_COMMAND} -E tar xzf ${CMAKE_CURRENT_SOURCE_DIR}/cudd-2.3.1.tar.gz
-#	COMMAND patch -p0 -i ${CMAKE_CURRENT_SOURCE_DIR}/cudd-2.3.1.patch
-#	COMMAND cd cudd-2.3.1 && rm -r include
-#	COMMAND cd cudd-2.3.1 && ./setup.sh
-#	COMMAND make -C cudd-2.3.1
-#	WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/
-#)
-
-set(HEADERS_FOLDER ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/include)
-file(MAKE_DIRECTORY ${HEADERS_FOLDER})
-
-add_library(cudd_core STATIC IMPORTED GLOBAL)
-add_library(cudd_epd STATIC IMPORTED GLOBAL)
-add_library(cudd_st STATIC IMPORTED GLOBAL)
-add_library(cudd_util STATIC IMPORTED GLOBAL)
-
-set_target_properties(cudd_core
-	PROPERTIES
-	IMPORTED_LOCATION ${CUDD_LIB_FILE}
-	INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER}
+#set(HEADERS_FOLDER ${CMAKE_CURRENT_BINARY_DIR}/cudd-2.3.1/include)
+SET(CUDD_INCLUDE_DIR
+	"${CMAKE_CURRENT_BINARY_DIR}/cudd/cudd/"
+	"${CMAKE_CURRENT_BINARY_DIR}/cudd/st/"
+	"${CMAKE_CURRENT_BINARY_DIR}/cudd/epd/"
+	"${CMAKE_CURRENT_BINARY_DIR}/cudd/util/"
+	"${CMAKE_CURRENT_BINARY_DIR}/cudd/dddmp/"
+	"${CMAKE_CURRENT_BINARY_DIR}/cudd/mtr/"
+	"${CMAKE_CURRENT_BINARY_DIR}/cudd/nanotrav/"
+	"${CMAKE_CURRENT_BINARY_DIR}/cudd/"
 )
 
-set_target_properties(cudd_epd
-	PROPERTIES
-	IMPORTED_LOCATION ${EPD_LIB_FILE}
-	INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER}
-)
+file(MAKE_DIRECTORY ${CUDD_INCLUDE_DIR})
 
-set_target_properties(cudd_st
-	PROPERTIES
-	IMPORTED_LOCATION ${ST_LIB_FILE}
-	INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER}
-)
+add_library(cudd STATIC IMPORTED GLOBAL)
 
-set_target_properties(cudd_util
-	PROPERTIES
-	IMPORTED_LOCATION ${UTIL_LIB_FILE}
-	INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER}
+set_target_properties(cudd PROPERTIES
+	IMPORTED_LOCATION ${CUDD_LIB_FILE}
+	INTERFACE_INCLUDE_DIRECTORIES "${CUDD_INCLUDE_DIR}"
 )
 

cudd/cudd-2.3.1.patch

-diff -r -c cudd-2.3.1/Makefile cudd-2.3.1/Makefile
-*** cudd-2.3.1/Makefile	2001-05-18 02:54:26.000000000 +0200
---- cudd-2.3.1/Makefile	2018-05-24 15:35:42.034516245 +0200
-***************
-*** 42,48 ****
-  #ICFLAGS	=
-  # These two are typical settings for optimized code with gcc.
-  #ICFLAGS	= -g -O6 -Wall
-! ICFLAGS	= -g -O6
-  
-  # Use XCFLAGS to specify machine-dependent compilation flags.
-  # For some platforms no special flags are needed.
---- 42,49 ----
-  #ICFLAGS	=
-  # These two are typical settings for optimized code with gcc.
-  #ICFLAGS	= -g -O6 -Wall
-! #ICFLAGS	= -g -O6
-! ICFLAGS	= -g -O6 -fPIC
-  
-  # Use XCFLAGS to specify machine-dependent compilation flags.
-  # For some platforms no special flags are needed.
-***************
-*** 52,58 ****
-  #  Linux
-  #
-  # Gcc 2.8.1 or higher on i686.
-! XCFLAGS	= -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
-  #
-  #==========================
-  #  Solaris
---- 53,60 ----
-  #  Linux
-  #
-  # Gcc 2.8.1 or higher on i686.
-! #XCFLAGS	= -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
-! XCFLAGS	= -malign-double -DHAVE_IEEE_754 -DBSD
-  #
-  #==========================
-  #  Solaris
-diff -r -c cudd-2.3.1/util/pipefork.c cudd-2.3.1/util/pipefork.c
-*** cudd-2.3.1/util/pipefork.c	2001-03-19 11:59:06.000000000 +0100
---- cudd-2.3.1/util/pipefork.c	2018-05-24 15:38:43.370514254 +0200
-***************
-*** 40,50 ****
-      int forkpid, waitPid;
-      int topipe[2], frompipe[2];
-      char buffer[1024];
-- #if (defined __hpux) || (defined __osf__) || (defined _IBMR2) || (defined __SVR4) || (defined __CYGWIN32__)
-      int status;
-- #else
--     union wait status;
-- #endif
-  
-      /* create the PIPES...
-       * fildes[0] for reading from command
---- 40,46 ----
-diff -r -c cudd-2.3.1/util/util.h cudd-2.3.1/util/util.h
-*** cudd-2.3.1/util/util.h	2001-02-14 19:08:51.000000000 +0100
---- cudd-2.3.1/util/util.h	2018-05-24 15:35:42.018516245 +0200
-***************
-*** 138,144 ****
-  /* most machines don't give us a header file for these */
-  #if (defined(__STDC__) || defined(__cplusplus) || defined(ultrix)) && !defined(MNEMOSYNE) || defined(__SVR4)
-  # include <stdlib.h>
-! EXTERN void free ARGS((void *));
-  #else
-  # ifndef _IBMR2
-      extern VOID_OR_INT abort(), exit();
---- 138,144 ----
-  /* most machines don't give us a header file for these */
-  #if (defined(__STDC__) || defined(__cplusplus) || defined(ultrix)) && !defined(MNEMOSYNE) || defined(__SVR4)
-  # include <stdlib.h>
-! /* EXTERN void free ARGS((void *)); */
-  #else
-  # ifndef _IBMR2
-      extern VOID_OR_INT abort(), exit();

extra/CMakeLists.txt

-set(EXTRA_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/extra20/libextra.a)
 
-add_custom_command(
-	OUTPUT ${EXTRA_LIB_FILE}
-	COMMAND ${CMAKE_COMMAND} -E tar xzf ${CMAKE_CURRENT_SOURCE_DIR}/extra20a.tar.gz
-	COMMAND patch -p0 -i ${CMAKE_CURRENT_SOURCE_DIR}/extra20.patch
-	COMMAND make -C extra20
-	WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/
+add_library(extra STATIC
+	src/maxDotProduct.c
+	src/maxUnion.c
+	src/minDotProduct.c
+	src/minUnion.c
+	src/notSubSet.c
+	src/notSupSet.c
+	src/emptyBelongs.c
 )
 
-add_custom_target(
-	libextra
-	DEPENDS ${EXTRA_LIB_FILE}
+set_target_properties(extra
+	PROPERTIES
+	PUBLIC_HEADER extra.h
+	POSITION_INDEPENDENT_CODE ON
 )
+target_link_libraries(extra cudd)
 
-add_dependencies(libextra libcudd)
-
-set(HEADERS_FOLDER ${CMAKE_CURRENT_BINARY_DIR}/extra20/)
-file(MAKE_DIRECTORY ${HEADERS_FOLDER})
-
-set(EXTRA_LIB_FILE ${CMAKE_CURRENT_BINARY_DIR}/extra20/libextra.a)
+target_include_directories(extra PUBLIC include)
 
-add_library(extra STATIC IMPORTED GLOBAL)
+add_dependencies(extra libcudd)
 
-set_target_properties(extra
-	PROPERTIES
-	IMPORTED_LOCATION ${EXTRA_LIB_FILE}
-	INTERFACE_INCLUDE_DIRECTORIES ${HEADERS_FOLDER}
-)
 

extra/README

+Most of the code in this directory was taken from the extra library of Alan Mishchenko.

extra/extra20.patch

-diff -r -c extra20/Makefile extra20/Makefile
-*** extra20/Makefile	2003-10-11 12:25:38.000000000 +0200
---- extra20/Makefile	2018-05-04 16:25:52.535788756 +0200
-***************
-*** 4,11 ****
-  .SILENT:
-  
-  # modify these macros to point to your include and lib directory
-! INCDIR = /u/alanmi/local/include/
-! LIBDIR = /u/alanmi/local/lib/
-  
-  # modify this line to compile with compilers other than g++
-  CC       = gcc
---- 4,11 ----
-  .SILENT:
-  
-  # modify these macros to point to your include and lib directory
-! INCDIR = ../../cudd/cudd-2.3.1/include/
-! LIBDIR = /tmp/
-  
-  # modify this line to compile with compilers other than g++
-  CC       = gcc
-***************
-*** 25,31 ****
-  #CFLAGS  = -c -O -D_UNIX -D_HP_
-  
-  # these are compiler flags for SunOS
-! CFLAGS  = -c -O -D_UNIX
-  
-  #LFLAGS = -pg -Wall
-  LFLAGS  =
---- 25,32 ----
-  #CFLAGS  = -c -O -D_UNIX -D_HP_
-  
-  # these are compiler flags for SunOS
-! #CFLAGS  = -c -O -D_UNIX
-! CFLAGS  = -c -O -D_UNIX -fPIC
-  
-  #LFLAGS = -pg -Wall
-  LFLAGS  =

extra/include/extra.h

+#ifndef EXTRA_H
+#define EXTRA_H
+
+#include <stdio.h>
+#include <cudd.h>
+#include <cuddInt.h>
+
+extern int         Extra_zddEmptyBelongs( DdManager *dd, DdNode* zS );
+
+extern DdNode *    Extra_zddMaxUnion( DdManager *dd, DdNode * S, DdNode * T );
+extern DdNode *     extraZddMaxUnion( DdManager *dd, DdNode * S, DdNode * T );
+extern DdNode *    Extra_zddMinUnion( DdManager *dd, DdNode * S, DdNode * T );
+extern DdNode *     extraZddMinUnion( DdManager *dd, DdNode * S, DdNode * T );
+
+extern DdNode *    Extra_zddMaxDotProduct( DdManager *dd, DdNode * S, DdNode * T );
+extern DdNode *     extraZddMaxDotProduct( DdManager *dd, DdNode * S, DdNode * T );
+extern DdNode *    Extra_zddMinDotProduct( DdManager *dd, DdNode * S, DdNode * T );
+extern DdNode *     extraZddMinDotProduct( DdManager *dd, DdNode * S, DdNode * T );
+
+extern DdNode *    Extra_zddNotSubSet( DdManager *dd, DdNode * X, DdNode * Y );
+extern DdNode *     extraZddNotSubSet( DdManager *dd, DdNode * X, DdNode * Y );
+extern DdNode *    Extra_zddNotSupSet( DdManager *dd, DdNode * X, DdNode * Y );
+extern DdNode *     extraZddNotSupSet( DdManager *dd, DdNode * X, DdNode * Y );
+
+#endif // EXTRA_H
+

extra/src/emptyBelongs.c

+#include <extra.h>
+
+int 
+Extra_zddEmptyBelongs(
+  DdManager *dd,
+  DdNode* zS )
+{
+	while ( zS->index != CUDD_MAXINDEX )
+		zS = cuddE( zS );
+	return (int)( zS == DD_ONE(dd) );
+
+} /* end of Extra_zddEmptyBelongs */
+
+

extra/src/maxDotProduct.c

+#include <extra.h>
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the maximal of the DotProduct of the union of two sets represented by ZDDs.]
+
+  Description [This procedure assumes that the arguments are already
+  maximal.]
+
+  SideEffects []
+
+  SeeAlso     [Extra_zddDotProduct Extra_zddMaximal Extra_zddMinCrossProduct]
+
+******************************************************************************/
+DdNode  *
+Extra_zddMaxDotProduct(
+  DdManager * dd,
+  DdNode * S,
+  DdNode * T)
+{
+    DdNode  *res;
+    do {
+    dd->reordered = 0;
+    res = extraZddMaxDotProduct(dd, S, T);
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_zddMaxDotProduct */
+
+/**Function********************************************************************
+
+  Synopsis [Performs the recursive step of Extra_zddMaxDotProduct.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode  *
+extraZddMaxDotProduct(
+  DdManager * dd,
+  DdNode * S,
+  DdNode * T)
+{
+    DdNode *zRes;
+    int TopS, TopT;
+    statLine(dd); 
+
+    /* consider terminal cases */
+    if ( S == DD_ZERO(dd) || T == DD_ZERO(dd) )
+        return DD_ZERO(dd);
+    if ( S == DD_ONE(dd) )
+        return T;
+    if ( T == DD_ONE(dd) )
+        return S;
+
+    /* the operation is commutative - normalize the problem */
+    TopS = dd->permZ[S->index];
+    TopT = dd->permZ[T->index];
+
+    if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) )
+        return extraZddMaxDotProduct(dd, T, S);
+
+    /* check cache */
+    zRes = cuddCacheLookup2Zdd(dd, extraZddMaxDotProduct, S, T);
+    if (zRes)
+        return zRes;
+    else
+    {
+        DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp;
+        if ( TopS == TopT )
+        {
+            /* compute the union of two cofactors of T (T0+T1) */
+            zTemp = extraZddMaxUnion(dd, cuddE(T), cuddT(T) );
+            if ( zTemp == NULL )
+                return NULL;
+            cuddRef( zTemp );
+
+            /* compute MaxDotProduct with the top element for subsets (S1, T0+T1) */
+            zSet0 = extraZddMaxDotProduct(dd, cuddT(S), zTemp );
+            if ( zSet0 == NULL )
+            {
+                Cudd_RecursiveDerefZdd(dd, zTemp);
+                return NULL;
+            }
+            cuddRef( zSet0 );
+            Cudd_RecursiveDerefZdd(dd, zTemp);
+
+            /* compute MaxDotProduct with the top element for subsets (S0, T1) */
+            zSet1 = extraZddMaxDotProduct(dd, cuddE(S), cuddT(T) );
+            if ( zSet1 == NULL )
+            {
+                Cudd_RecursiveDerefZdd(dd, zSet0);
+                return NULL;
+            }
+            cuddRef( zSet1 );
+
+            /* compute the union of these two partial results (zSet0 + zSet1) */
+            zRes1 = extraZddMaxUnion(dd, zSet0, zSet1 );
+            if ( zRes1 == NULL )
+            {
+                Cudd_RecursiveDerefZdd(dd, zSet0);
+                Cudd_RecursiveDerefZdd(dd, zSet1);
+                return NULL;
+            }
+            cuddRef( zRes1 );
+            Cudd_RecursiveDerefZdd(dd, zSet0);
+            Cudd_RecursiveDerefZdd(dd, zSet1);
+
+            /* compute MaxDotProduct for subsets without the top-most element */
+            zRes0 = extraZddMaxDotProduct(dd, cuddE(S), cuddE(T) );
+            if ( zRes0 == NULL )
+            {
+                Cudd_RecursiveDerefZdd(dd, zRes1);
+                return NULL;
+            }
+            cuddRef( zRes0 );
+        }
+        else /* if ( TopS < TopT ) */
+        {
+            /* compute MaxDotProduct with the top element for subsets (S1, T) */
+            zRes1 = extraZddMaxDotProduct(dd, cuddT(S), T );
+            if ( zRes1 == NULL )
+                return NULL;
+            cuddRef( zRes1 );
+
+            /* compute MaxDotProduct for subsets without the top-most element */
+            zRes0 = extraZddMaxDotProduct(dd, cuddE(S), T );
+            if ( zRes0 == NULL )
+            {
+                Cudd_RecursiveDerefZdd(dd, zRes1);
+                return NULL;
+            }
+            cuddRef( zRes0 );
+        }
+
+        /* remove subsets without this element covered by subsets with this element */
+        zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1);
+        if ( zRes0 == NULL )
+        {
+            Cudd_RecursiveDerefZdd(dd, zTemp);
+            Cudd_RecursiveDerefZdd(dd, zRes1);
+            return NULL;
+        }
+        cuddRef( zRes0 );
+        Cudd_RecursiveDerefZdd(dd, zTemp);
+
+        /* create the new node */
+        zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
+        if ( zRes == NULL ) 
+        {
+            Cudd_RecursiveDerefZdd( dd, zRes0 );
+            Cudd_RecursiveDerefZdd( dd, zRes1 );
+            return NULL;
+        }
+        cuddDeref( zRes0 );
+        cuddDeref( zRes1 );
+
+        /* insert the result into cache */
+        cuddCacheInsert2(dd, extraZddMaxDotProduct, S, T, zRes);
+        return zRes;
+    }
+} /* end of extraZddMaxDotProduct */
+

extra/src/maxUnion.c

+#include <extra.h>
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the maximal of the union of two sets represented by ZDDs.]
+
+  Description [This procedure assumes that the arguments are already
+  maximal. This is why Maximal(X) is not computed in the bottom cases 
+  MaxUnion(X, {}) = MaxUnion({}, X) = Maximal(X), and X is returned.]
+
+  SideEffects []
+
+  SeeAlso     [Extra_zddMaximal Extra_zddMimimal Extra_zddMinUnion]
+
+******************************************************************************/
+
+DdNode  *
+Extra_zddMaxUnion(
+  DdManager * dd,
+  DdNode * S,
+  DdNode * T)
+{
+    DdNode  *res;
+    do {
+    dd->reordered = 0;
+    res = extraZddMaxUnion(dd, S, T);
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_zddMaxUnion */
+
+
+/**Function********************************************************************
+
+  Synopsis [Performs the recursive step of Extra_zddMaxUnion.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode  *
+extraZddMaxUnion(
+  DdManager * dd,
+  DdNode * S,
+  DdNode * T)
+{
+    DdNode *zRes;
+    int TopS, TopT;
+    statLine(dd); 
+
+    /* consider terminal cases */
+    if ( S == DD_ZERO(dd) )
+        return T;
+    if ( T == DD_ZERO(dd) )
+        return S;
+    if ( S == T )
+        return S;
+    if ( S == DD_ONE(dd) )
+        return T;
+    if ( T == DD_ONE(dd) )
+        return S;
+
+    /* the operation is commutative - normalize the problem */
+    TopS = dd->permZ[S->index];
+    TopT = dd->permZ[T->index];
+
+    if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) )
+        return extraZddMaxUnion(dd, T, S);
+
+    /* check cache */
+    zRes = cuddCacheLookup2Zdd(dd, extraZddMaxUnion, S, T);
+    if (zRes)
+        return zRes;
+    else
+    {
+        DdNode *zSet0, *zSet1, *zRes0, *zRes1;
+
+        if ( TopS == TopT )
+        {
+            /* compute maximal for subsets without the top-most element */
+            zSet0 = extraZddMaxUnion(dd, cuddE(S), cuddE(T) );
+            if ( zSet0 == NULL )
+                return NULL;
+            cuddRef( zSet0 );
+
+            /* compute maximal for subsets with the top-most element */
+            zSet1 = extraZddMaxUnion(dd, cuddT(S), cuddT(T) );
+            if ( zSet1 == NULL )
+            {
+                Cudd_RecursiveDerefZdd(dd, zSet0);
+                return NULL;
+            }
+            cuddRef( zSet1 );
+        }
+        else /* if ( TopS < TopT ) */
+        {
+            /* compute maximal for subsets without the top-most element */
+            zSet0 = extraZddMaxUnion(dd, cuddE(S), T );
+            if ( zSet0 == NULL )
+                return NULL;
+            cuddRef( zSet0 );
+
+            /* subset with this element is just the cofactor of S */
+            zSet1 = cuddT(S);
+            cuddRef( zSet1 );
+        }
+
+        /* remove subsets without this element covered by subsets with this element */
+        zRes0 = extraZddNotSubSet(dd, zSet0, zSet1);
+        if ( zRes0 == NULL )
+        {
+            Cudd_RecursiveDerefZdd(dd, zSet0);
+            Cudd_RecursiveDerefZdd(dd, zSet1);
+            return NULL;
+        }
+        cuddRef( zRes0 );
+        Cudd_RecursiveDerefZdd(dd, zSet0);
+
+        /* subset with this element remains unchanged */
+        zRes1 = zSet1;
+
+        /* create the new node */
+        zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
+        if ( zRes == NULL ) 
+        {
+            Cudd_RecursiveDerefZdd( dd, zRes0 );
+            Cudd_RecursiveDerefZdd( dd, zRes1 );