Version abc60614

2006-06-14 08:01:00 -07:00 · 2006-06-14 08:01:00 -07:00 · 3814121784
parent 3db1557f45
commit 3814121784
43 changed files with 5647 additions and 232346 deletions
--- a/5
+++ b/5
@ -11,13 +11,12 @@ MODULES := src/base/abc src/base/abci src/base/seq src/base/cmd src/base/io src/
           src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super \
           src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec \
 	   src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \
-	   src/temp/esop src/temp/ivy src/temp/player \
           src/sat/asat src/sat/csat src/sat/msat src/sat/fraig

 default: $(PROG)

-#OPTFLAGS  := -DNDEBUG -O3
-OPTFLAGS  := -g -O
+OPTFLAGS  := -DNDEBUG -O3
+#OPTFLAGS  := -g -O

 CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
 CXXFLAGS += $(CFLAGS) 
--- a/abc.dsp
+++ b/abc.dsp
@ -222,6 +222,10 @@ SOURCE=.\src\base\abci\abcIvy.c
 # End Source File
 # Begin Source File

+SOURCE=.\src\base\abci\abcLut.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcMap.c
 # End Source File
 # Begin Source File
--- a/abc.rc
+++ b/abc.rc
@ -63,7 +63,6 @@ alias so source -x
 alias st strash
 alias sw sweep
 alias ssw ssweep
-alias scl scleanup
 alias tr0 trace_start
 alias tr1 trace_check
 alias trt "r c.blif; st; tr0; b; tr1"
--- a/examples/C2670.blif
+++ b/examples/C2670.blif
--- a/examples/ac.v
+++ b/examples/ac.v
--- a/examples/apex4.pla
+++ b/examples/apex4.pla
@ -1,443 +0,0 @@
-.i 9
-.o 19
-.p 438
-010110011 0100000000000000011
-100100001 0110000000000000000
-100010100 0100010000000000000
-100101001 0100001000000000000
-001101010 0000001000000001001
-00-0-0001 0000000000001011100
-110101010 0000000000010100000
-010111100 0100000001000000110
-011010111 0100000001000000000
-010111010 0000110000000000000
-110000001 0100000000001010000
-0110-0011 0001100000000000000
-10011-010 0100000000000000000
-101000110 0011000000000000000
-100110110 0000101000000000000
-101110100 0001100000000000000
-111000101 0100000000100000000
-100100100 0000000001100000000
-111001110 0100000000100000000
-111111001 0000000000001100000
-001100100 0000000000100110000
-001101101 0010000000010100000
-01111101 0100000000000000000
-010001110 0100000010100000000
-001011111 0000010100000000110
-100101110 0100100100000000000
-001011011 0000000010010010000
-011111000 0010100000000000000
-100110100 0000001000001100000
-001101110 0000000100010010000
-010011100 0000000001000110000
-101111101 0000100100000000000
-111010000 0100000000000110000
-101011010 0000010100000000000
-011000001 0000100000000110000
-101101101 0000100001000000000
-011011011 0001000000010010000
-010011111 0000010001000001010
-10111111- 0100000000000000000
-010101010 0010000001000001001
-011101010 0010000000001100000
-11011111- 0100000000000000000
-111111011 0001100000000000000
-001010101 0000010000010101100
-001110111 0010000000000111001
-1001100-1 0010000000000000000
-100100111 0100000000110010000
-011101011 0101000001000000000
-011011101 0000100000010010000
-101110101 0101000001000000000
-001110100 0010000000010011001
-001110010 0001000110000000000
-110011100 0000000000110010000
-110101111 0000001000001100000
-100111111 0001000110000000000
-10-110000 0100000000000010000
-101101100 0100001010000000000
-010000011 0001000010000110000
-11000011 0001000000000000000
-100001101 0000101100000000000
-010000010 0000100000110100000
-1-0001001 0100100000000000000
-001001110 0001010010000001100
-001110001 0000100011000000000
-00101001- 0000000100000001100
-100100010 0010000001100000000
-011011110 0001110000000000000
-110110000 0000100100001000000
-101000101 0000011000001000000
-100101111 0101010010000000000
-101110110 0100000000110010000
-001110000 0000010001100000000
-011001110 0100000001000110000
-010010100 0000010001100000000
-100010010 0001000001001010000
-100011000 0000100010000110000
-01001100 0000000000010010000
-001001111 0010100010000001100
-110111110 0001110000000000000
-100110001 0000001110000000000
-001100000 0000101000100000101
-100110101 0000010011000000000
-010010010 0010000000110010000
-111100110 0000010000010010000
-100-10001 0001100000000000000
-100111101 0010010000000110000
-011010100 0001000011000000000
-101011101 0001100000011000000
-010101011 0001001100000001001
-110101100 0001100000000110000
-110101000 0001010001000000000
-001001101 0000101010000001110
-110010100 0000110100000000000
-011000101 0100000001001101100
-111000111 0100001001000000000
-001010000 0010000010001101100
-100011101 0100011010000000000
-1-0110000 0000000000100100000
-10000-011 0001000001000000000
-001011100 0000000011010010000
-101111001 0000000110100000000
-0010100-1 0000000010100000000
-010001-01 0010000000100000000
-110-11011 0000000000010010000
-1110-1011 0000010000000000000
-1001-1011 0000100000100000000
-00110001- 0010000000100000000
-100100110 0101000001010010000
-101010101 0010000000100110000
-01101011 0001010000000000000
-001001000 0000000011100100000
-110000100 0000010011000000000
-101000-00 0000000010001000000
-010011110 0000000111000001100
-110111100 0000110001000000000
-001101001 0000010100001011010
-10011-001 0010000000100000000
-0100-0001 0000010010000000000
-100111-10 0000100100000000000
-110101101 0010001100000000000
-001101000 0000001010001101100
-01111011 0001000100000000000
-001000-11 0000000011000000000
-110000101 0000101000010100000
-011100100 0000011001000000000
-011100110 0000100001000110000
-1011-0000 0010000000010000000
-100011011 0010000101001000000
-101-00000 0000001000000100000
-0011-1111 0000001000100000000
-011011100 0010000010010010000
-001010111 0001010001100000000
-110000010 0010000001011000000
-00-000-00 0000000000000010001
-0-1100110 0000000010100000000
-1001010-0 0000000011000000000
-11-001011 0010000000001000000
-011111-01 0011000000000000000
-01-110100 0010000000100000000
-101011001 0000001001001100000
-011101110 0000011000011000000
-101100001 0000000101000110000
-011111011 0010000001011000000
-011101100 0100000011100000000
-1-1001011 0000000010000010000
-01011010 0000000001100000000
-0-1001011 0000001100000000000
-0110-0000 0000100010000000000
-111001101 0101010010000000000
-111000110 0010000011000000000
-011-00111 0000100010000000000
-01100-011 0000010000100000000
-1101-1011 0000001000000010000
-11001010 0001010000000000000
-01110011- 0001001000000000000
-100011110 0010110001000000000
-110001-01 0000100100000000000
-011010110 0100000100111000000
-100010110 0001000110010100000
-100001011 0010110000000110000
-110-10010 0000110000000000000
-101-01101 0010010000000000000
-0-1100111 0000000101000000000
-110100-00 0010000000100000000
-01001100- 0000000010010010000
-110101-10 0010000000100000000
-111010100 0000101000001100000
-110-11001 0010000000100000000
-1100-1100 0010010000000000000
-1010101-0 0000010100000000000
-100001111 0010010010001100000
-11000011- 0001000000000110000
-111100011 0000010101000000000
-01010111- 0000010000100001001
-010111111 0010010110000000000
-011110000 0011000010100000000
-111110001 0010000000111000000
-100100011 0000000111100000000
-011100000 0011100001000000000
-011111110 0100001101000000000
-010110101 0010011010000000000
-010100011 0000110010001010000
-111111000 0000010101000000000
-111111101 0010000000111000000
-11101100- 0100000000011000000
-011111100 0001110100000000000
-001111011 0000101010001100000
-11100001 0010000000100000000
-0111-1000 0000001000100000000
-100100000 0101110000011000000
-010100111 0000100110010100000
-101000010 0001011100000000000
-11001-010 0000001010000000000
-010001000 0010010001001100000
-11110011 0010000000100000000
-010100101 0000001011100000000
-100--1000 0010000000000000000
-010101000 0001001001000110000
-010010101 0000100101100000110
-111101001 0000001010000110000
-111000100 0101000001000110000
-011001101 0001100100000110000
-001111111 0010010100011000000
-1010-1000 0000001001000000000
-100101100 0001000101010010000
-001110101 0001001110000001001
-0100-101- 0000000010000000000
-011100101 0000110100100000000
-110010001 0001011100000000000
-0-110-010 0000100000000000000
-111001100 0100100100011000000
-101100101 0001000110001100000
-10-001-01 0000000000100000000
-111111010 0000001001001100000
-101111110 0001010010001100000
-1-0001-00 0010000000000000000
-011001000 0001000110001010000
-001--0101 0000000001000000000
-010000101 0100101011000000000
-011011010 0010011000100000000
-110011110 0000111000100000000
-001110011 0010001100010010000
-111010110 0011110000000000000
-11101-111 0010000000100000000
-111011-00 0000100100000000000
-01-11111 0000000000100000000
-111100111 0001110000100000000
-10011000 0001110000000000000
-110001110 0001000110011000000
-01011-010 0001000110000000000
-01100001 0001010000100000000
-010100100 0000000111011000000
-01--00010 0000000100000000000
-011011001 0010101001000000000
-1101110-1 0000000010010010000
-10-10-100 0000010000000000000
--1011000 0000100000000000000
-010-0110 0000000001000000000
-10--01011 0000001000000000000
-110110100 0001000110011000000
-100010011 0100010110011000000
-101110010 0000000111100000000
-001001100 0000010110001101110
-110100001 0010000111000000000
-110100011 0010010100001100000
-010100-10 0000010100100000000
-010100000 0000100101001101001
-11101-110 0000001010000000000
-1-01010-1 0000000001000000000
-001111000 0000001101100001001
-00101100- 0010000001100000000
-0100010-0 0000001100100000000
-010000110 0001110011000000000
-001-11110 0000001010100000000
-101101111 0101110000010010000
-1-011101 0000000010000000000
-00101-101 0000000101100000000
-0101-0010 0010011000000000000
-10100010- 0000100001010000000
-1011001- 0000000001000000000
-10111100- 0100001001000000000
-1111-1100 0000001100000000000
-10000000- 0000100000110010000
-110100101 0000011101000000000
-010-01111 0000001110000000000
-001010110 0000101000110011111
-001111100 0011011100000000000
-101100-11 0010100010000000000
-11101111- 0000000000110010000
-010111011 0011101001000000000
-11001-1-1 0000000001000000000
-101110111 0010000011010010000
-111001001 0000101001100000000
-0-1001010 0000000111000000000
-100011010 0010101110000000000
-01110100- 0011000001000000000
-11-111-00 0010000000000000000
-11-1-1111 0010000000000000000
-110110-10 0010100010000000000
-011101101 0000001011001010000
-1-110110- 0000010000000000000
-0-1001001 0000000100111000000
-100100101 0011101000010010000
-1-0111011 0100011000010000000
-111110010 0010011100000000000
-11-010-10 0000001000000000000
-111101101 0000101000101100000
-010111001 0000111100100000000
-011001-01 0010001010000000000
-010110001 0001110001011000000
-10100000- 0010000000101100000
-01110-111 0000110001000000000
-111010001 0010000001100110000
-1-1101011 0010010000100000000
-100-11011 0000010010100100000
-100111100 0010100110000110000
-111000000 0010000001110010000
-100010101 0010011101000000000
-01011011- 0000010001010010000
-10100101- 0010000000110010000
-010010110 0001001101100000101
-01111001- 0010000000100110000
-11000010 0000010001100000000
-101-10001 0010000000110010000
-010000100 0010010101000110000
-10-00-100 0010000000100000000
-110000111 0010111010000000000
-1-00100-0 0010000000100000000
-100-0000 0010000000100000000
-011000000 0001011101000000000
-011-10011 0000001101000000000
-1111011-0 0000100010100000000
-11010011 0000010011000000000
-101000111 0010001110100000000
-011010001 0001000101101100000
-1-1100100 0010000101000000000
-010010011 0000000111110010000
-001111010 0000110111000001001
-111-11010 0000100110000000000
-010001011 0000011101011000000
-01110001- 0010000001010010000
-1010--011 0010000000100000000
-010010001 0010001101010010000
-110-01011 0000100110000100000
-10-011001 0001010110000000000
-10-1100-1 0000000001100000000
-010001111 0011110001100000000
-001111001 0000011011100001001
-001110110 0010011101000001001
-0101000-1 0001001101000000000
-01100-01- 0000101000000000000
-110110101 0010101101000000000
-010101100 0010011010001101001
-11001-01- 0010000000100000000
-110001111 0010001010111000000
-010110000 0000111010011001001
-1-1-00011 0010100000000000000
-0101101-0 0000111100000000000
-011010101 0010000011111000000
-110010110 0010000110110010000
-11-01-101 0001000100000000000
-101--0100 0010001000000000000
-001010100 0000001011111001100
-10-000101 0010100101000000000
-101111010 0000101001100110000
-101-01000 0001010110000000000
-111011001 0000111010100000000
-1010--110 0000001100000000000
-01-000110 0010001100100000000
-101010010 0010000111010010000
-11-10-010 0010000000100000000
-1011--011 0000010001000000000
-110110011 0010011100011000000
-110001010 0100111010001100000
-01011-110 0001001010010010000
-110-10111 0001010110000000000
-100011111 0001111000111000000
-10100111- 0000111000100000000
-11111111- 0010001000011000000
-00-0000-- 0000000000000110001
-100111000 0001111010011000000
-011000100 0011101110000000000
-1100101- 0000000101000000000
-0110-1111 0010001100100000000
-111100000 0001011100010010000
-011111111 0011111000100000000
-1111-100- 0010000000100000000
-100-01010 0100001101100000000
-010010111 0010011101100000000
-1101-1000 0000101110000000000
-111010101 0010001001101100000
-110010-11 0000101011000000000
-1-1100001 0000111010000000000
-111000001 0000000111110010000
-1100--0-0 0000000000100000000
-011001100 0001111000110100000
-001111110 0010110101001010000
-1010-100- 0001110000000000000
-111110000 0010000111001010000
-100010111 0010101101000110000
-011110101 0001111101000000000
-01111110- 0000001011100000000
-1--00011 0000001000000000000
-011111010 0011010110011000000
-101010111 0000111011100000000
-010111101 0010011100110010000
-11-01-11 0000000000100000000
-111110100 0000011101010100000
-010101001 0010001111000110000
-1-1011-1- 0010000000000000000
-011110001 0011011100010100000
-100000111 0000011111010010000
-101111100 0010010111100000000
-110100111 0001111001011000000
-101100010 0001011011000110000
-111100-10 0000101011000000000
-101101001 0010101110011000000
-10-000011 0000111010100000000
-11001010- 0010001001010010000
-101100110 0010101101001100000
-101-01110 0001111000100000000
-011010010 0010001101101100000
-10-001110 0001011011000000000
-10000-000 0001011100010010000
-110-11101 0001111000100000000
-101011100 0000101111001010000
-1-0000110 0010001101100000000
-100011100 0011011001101100000
-111110110 0001111001000110000
-0110111-1 0001011101000000000
-010000111 0001001111101100000
-11011000- 0001011011000000000
-101010000 0001101111100000000
-100110111 0011001101101010000
-1101-1001 0010010101100000000
-111100101 0010001110110010000
-110011111 0001101110100110000
-100101101 0010010111110010000
-111001000 0100001111101100000
-0010001-- 0000000011011101110
-010111000 0000011111110010000
-1-0000000 0001101111000000000
-110111010 0011011001110010000
-101101010 0010010111111000000
-011110111 0010101111001100000
-110100110 0000111011101010000
-111110111 0001111111000000000
-01-011000 0001011111000000000
-00-00-0-- 0000000000011001110
-11110-1-0 0001001101000000000
-111110101 0000111011100110000
-001101100 0010011111111000000
-010101101 0001111111001101001
-010001100 0000111111111000011
-111001111 0011101111010100000
-1000000-0 0000111111010010000
-011110110 0001111111101100000
-000------ 0000000000011111111
-.e
-
--- a/examples/frg2.blif
+++ b/examples/frg2.blif
--- a/examples/i10.blif
+++ b/examples/i10.blif
--- a/examples/pj1.blif
+++ b/examples/pj1.blif
--- a/examples/s38417.blif
+++ b/examples/s38417.blif
--- a/examples/s38584.bench
+++ b/examples/s38584.bench
--- a/examples/s444.blif
+++ b/examples/s444.blif
@ -1,353 +0,0 @@
-.model s444
-.inputs G0 G1 G2
-.outputs G118 G167 G107 G119 G168 G108
-
-.latch     G11_in        G11  0
-.latch     G12_in        G12  0
-.latch     G13_in        G13  0
-.latch     G14_in        G14  0
-.latch     G15_in        G15  0
-.latch     G16_in        G16  0
-.latch     G17_in        G17  0
-.latch     G18_in        G18  0
-.latch     G19_in        G19  0
-.latch     G20_in        G20  0
-.latch     G21_in        G21  0
-.latch     G22_in        G22  0
-.latch     G23_in        G23  0
-.latch     G24_in        G24  0
-.latch     G25_in        G25  0
-.latch     G26_in        G26  0
-.latch     G27_in        G27  0
-.latch     G28_in        G28  0
-.latch     G29_in        G29  0
-.latch     G30_in        G30  0
-.latch     G31_in        G31  0
-
-.names G12 G13 [25]
-00 1
-.names G11 [25] [26]
-01 1
-.names G14 [26] [27]
-10 1
-.names G0 G11 [28]
-00 1
-.names [27] [28] G11_in
-01 1
-.names G11 G12 [30]
-11 1
-.names G12 [30] [31]
-10 1
-.names G11 [30] [32]
-10 1
-.names [31] [32] [33]
-00 1
-.names G0 [33] [34]
-00 1
-.names [27] [34] G12_in
-01 1
-.names G13 [30] [36]
-11 1
-.names G13 [36] [37]
-10 1
-.names [30] [36] [38]
-10 1
-.names [37] [38] [39]
-00 1
-.names G0 [39] [40]
-00 1
-.names [27] [40] G13_in
-01 1
-.names G12 G13 [42]
-11 1
-.names G11 [42] [43]
-11 1
-.names G14 [43] [44]
-11 1
-.names G14 [44] [45]
-10 1
-.names [43] [44] [46]
-10 1
-.names [45] [46] [47]
-00 1
-.names G0 [47] [48]
-00 1
-.names [27] [48] G14_in
-01 1
-.names G31 [27] [50]
-00 1
-.names G16 G17 [51]
-00 1
-.names G15 [51] [52]
-01 1
-.names [50] [52] [53]
-00 1
-.names G18 [53] [54]
-11 1
-.names G15 [50] [55]
-10 1
-.names G15 [55] [56]
-10 1
-.names [50] [55] [57]
-00 1
-.names [56] [57] [58]
-00 1
-.names G0 [58] [59]
-00 1
-.names [54] [59] G15_in
-01 1
-.names G16 [55] [61]
-11 1
-.names G16 [61] [62]
-10 1
-.names [55] [61] [63]
-10 1
-.names [62] [63] [64]
-00 1
-.names G0 [64] [65]
-00 1
-.names [54] [65] G16_in
-01 1
-.names G16 [50] [67]
-10 1
-.names G15 [67] [68]
-11 1
-.names G17 [68] [69]
-11 1
-.names G17 [69] [70]
-10 1
-.names [68] [69] [71]
-10 1
-.names [70] [71] [72]
-00 1
-.names G0 [72] [73]
-00 1
-.names [54] [73] G17_in
-01 1
-.names G15 G16 [75]
-11 1
-.names G17 [50] [76]
-10 1
-.names [75] [76] [77]
-11 1
-.names G18 [77] [78]
-11 1
-.names G18 [78] [79]
-10 1
-.names [77] [78] [80]
-10 1
-.names [79] [80] [81]
-00 1
-.names G0 [81] [82]
-00 1
-.names [54] [82] G18_in
-01 1
-.names G20 G21 [84]
-00 1
-.names G19 [84] [85]
-01 1
-.names [54] [85] [86]
-10 1
-.names G22 [86] [87]
-11 1
-.names G19 [54] [88]
-11 1
-.names G19 [88] [89]
-10 1
-.names [54] [88] [90]
-10 1
-.names [89] [90] [91]
-00 1
-.names G0 [91] [92]
-00 1
-.names [87] [92] G19_in
-01 1
-.names G20 [88] [94]
-11 1
-.names G20 [94] [95]
-10 1
-.names [88] [94] [96]
-10 1
-.names [95] [96] [97]
-00 1
-.names G0 [97] [98]
-00 1
-.names [87] [98] G20_in
-01 1
-.names G20 [54] [100]
-11 1
-.names G19 [100] [101]
-11 1
-.names G21 [101] [102]
-11 1
-.names G21 [102] [103]
-10 1
-.names [101] [102] [104]
-10 1
-.names [103] [104] [105]
-00 1
-.names G0 [105] [106]
-00 1
-.names [87] [106] G21_in
-01 1
-.names G19 G20 [108]
-11 1
-.names G21 [54] [109]
-11 1
-.names [108] [109] [110]
-11 1
-.names G22 [110] [111]
-11 1
-.names G22 [111] [112]
-10 1
-.names [110] [111] [113]
-10 1
-.names [112] [113] [114]
-00 1
-.names G0 [114] [115]
-00 1
-.names [87] [115] G22_in
-01 1
-.names G2 G23 [117]
-00 1
-.names G2 G23 [118]
-11 1
-.names [117] [118] [119]
-00 1
-.names G0 [119] G23_in
-01 1
-.names G20 G21 [121]
-01 1
-.names G0 G23 [122]
-01 1
-.names [121] [122] [123]
-11 1
-.names G19 [123] [124]
-01 1
-.names G21 G22 [126]
-10 1
-.names G19 G20 [125]
-10 1
-.names G23 [125] [127]
-01 1
-.names [126] [127] [128]
-11 1
-.names G0 G24 [129]
-01 1
-.names [128] [129] [130]
-01 1
-.names [124] [130] [131]
-00 1
-.names G22 G23 [132]
-00 1
-.names [125] [132] [133]
-11 1
-.names G24 [133] [134]
-10 1
-.names G19 G20 [135]
-00 1
-.names G23 [135] [136]
-11 1
-.names G22 G23 [137]
-11 1
-.names [136] [137] [138]
-00 1
-.names G0 G21 [139]
-01 1
-.names [138] [139] [140]
-11 1
-.names [134] [140] G25_in
-01 1
-.names G19 G22 [142]
-01 1
-.names G0 [142] [143]
-01 1
-.names G0 [108] [144]
-01 1
-.names [143] [144] [145]
-00 1
-.names [129] [139] [146]
-00 1
-.names [145] [146] G26_in
-11 1
-.names G21 G24 [148]
-00 1
-.names [125] [148] [149]
-11 1
-.names G21 G22 [150]
-00 1
-.names G24 [150] [151]
-01 1
-.names G0 [151] [152]
-00 1
-.names [149] [152] [153]
-01 1
-.names G0 G22 [154]
-01 1
-.names [135] [154] [155]
-11 1
-.names [146] [155] [156]
-10 1
-.names [131] [156] [157]
-00 1
-.names G17 [157] [158]
-01 1
-.names [131] [156] [159]
-10 1
-.names [158] [159] G28_in
-00 1
-.names [122] [126] [161]
-11 1
-.names G21 G22 [162]
-01 1
-.names G0 [162] [163]
-01 1
-.names [161] [163] [164]
-00 1
-.names G20 [164] [165]
-00 1
-.names G19 [165] [166]
-01 1
-.names [130] [166] [167]
-00 1
-.names [131] [167] [168]
-00 1
-.names G17 [168] [169]
-01 1
-.names [131] [167] [170]
-10 1
-.names [169] [170] G29_in
-00 1
-.names G20 G21 [172]
-10 1
-.names G0 G24 [173]
-00 1
-.names [172] [173] [174]
-11 1
-.names G19 [174] G30_in
-11 1
-.names G1 G31 [176]
-00 1
-.names G1 G31 [177]
-11 1
-.names [176] [177] [178]
-00 1
-.names G0 [178] G31_in
-01 1
-.names [131] G24_in
-0 1
-.names [153] G27_in
-0 1
-.names G27 G118
-1 1
-.names G29 G167
-0 1
-.names G25 G107
-1 1
-.names G28 G119
-0 1
-.names G30 G168
-1 1
-.names G26 G108
-1 1
-.end
--- a/examples/s5378.blif
+++ b/examples/s5378.blif
--- a/examples/s6669.blif
+++ b/examples/s6669.blif
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@ -515,6 +515,7 @@ extern Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fIni
 /*=== abcObj.c ==========================================================*/
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
 extern void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
+extern void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj );
 extern Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
@ -598,6 +599,7 @@ extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams
 extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
 extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
 extern Vec_Ptr_t *        Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
+extern Vec_Ptr_t *        Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p );
 extern Vec_Ptr_t *        Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
 extern Vec_Ptr_t *        Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
 extern void               Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@ -264,8 +264,33 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
    Abc_ObjRecycle( pObj );
 }

+/**Function*************************************************************

+  Synopsis    [Deletes the node and MFFC of the node.]

+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    Vec_Ptr_t * vNodes;
+    int i;
+    assert( !Abc_ObjIsComplement(pObj) );
+    assert( Abc_ObjFanoutNum(pObj) == 0 );
+    // delete fanins and fanouts
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NodeCollectFanins( pObj, vNodes );
+    Abc_NtkDeleteObj( pObj );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
+            Abc_NtkDeleteObj_rec( pObj );
+    Vec_PtrFree( vNodes );
+}


 /**Function*************************************************************
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@ -915,7 +915,7 @@ void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )

 /**Function*************************************************************

-  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+  Synopsis    [Procedure used for sorting the nodes in increasing order of levels.]

  Description []
               
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@ -31,96 +31,97 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////

-static int Abc_CommandPrintStats   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintExdc    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintIo      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintLatch   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintLevel   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSymms   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintUnate   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintAuto    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintKMap    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintGates   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintStats     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintExdc      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintIo        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintLatch     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFanio     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFactor    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintLevel     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSupport   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSymms     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintUnate     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintAuto      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintKMap      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintGates     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSharing   ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandShowBdd      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowCut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowAig      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowNtk      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowBdd        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowCut        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowAig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowNtk        ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandCollapse     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandStrash       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandBalance      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRenode       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCleanup      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSweep        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFastExtract  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandDisjoint     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCollapse       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandStrash         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBalance        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRenode         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCleanup        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSweep          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFastExtract    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDisjoint       ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandRewrite      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRefactor     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRestructure  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRr           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRewrite        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRefactor       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRestructure    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandResubstitute   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRr             ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandDemiter      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOrPos        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFrames       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandReorder      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandMuxes        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExtSeqDcs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOneOutput    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOneNode      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShortNames   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExdcFree     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExdcGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExdcSet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCut          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandEspresso     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandGen          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandXyz          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandTest         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandLogic          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMiter          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDemiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOrPos          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFrames         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSop            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBdd            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandReorder        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMuxes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExtSeqDcs      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneOutput      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneNode        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShortNames     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcFree       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcGet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcSet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCut            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEspresso       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXyz            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigTrust   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigStore   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigClean   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigSweep   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraig          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigTrust     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigStore     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigRestore   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigClean     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigSweep     ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandMap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandUnmap        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAttach       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMap            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnmap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAttach         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSuperChoice    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPga          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFpga           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPga            ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandScut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandInit         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPipe         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandUnseq        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqFpga      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqMap       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqSweep     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqCleanup   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandScut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInit           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPipe           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeq            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnseq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRetime         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqFpga        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqMap         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqSweep       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqCleanup     ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandProve        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSat            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** argv );

-static int Abc_CommandTraceStart   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandTraceCheck   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );

 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@ -209,6 +210,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
    Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Abc_CommandUnmap,            1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "attach",        Abc_CommandAttach,           1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "sc",            Abc_CommandSuperChoice,      1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "scl",           Abc_CommandSuperChoiceLut,   1 );

    Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
    Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
@ -5483,6 +5485,110 @@ usage:
    return 1;
 }

+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSuperChoiceLut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int nLutSize;
+    int nCutSizeMax;
+    int fVerbose;
+    extern int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 1;
+    nLutSize = 4;
+    nCutSizeMax = 10;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KNh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nCutSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCutSizeMax < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Superchoicing works only for the AIG representation (run \"strash\").\n" );
+        return 1;
+    }
+
+    // convert the network into the SOP network
+    pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+
+    // get the new network
+    if ( !Abc_NtkSuperChoiceLut( pNtkRes, nLutSize, nCutSizeMax, fVerbose ) )
+    {
+        Abc_NtkDelete( pNtkRes );
+        fprintf( pErr, "Superchoicing has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: scl [-K num] [-N num] [-vh]\n" );
+    fprintf( pErr, "\t        performs superchoicing for K-LUTs\n" );
+    fprintf( pErr, "\t        (accumulate: \"r file.blif; b; scl; f -ac; wb file_sc.blif\")\n" );
+    fprintf( pErr, "\t        (FPGA map: \"r file_sc.blif; ft; read_lut lutlibK; fpga\")\n" );
+    fprintf( pErr, "\t-K num : the number of LUT inputs [default = %d]\n", nLutSize );
+    fprintf( pErr, "\t-N num : the max size of the cut [default = %d]\n", nCutSizeMax );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************

  Synopsis    []
@ -5497,12 +5603,14 @@ usage:
 int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
    char Buffer[100];
+    char LutSize[100];
    FILE * pOut, * pErr;
    Abc_Ntk_t * pNtk, * pNtkRes;
    int c;
    int fRecovery;
    int fSwitching;
    int fVerbose;
+    int nLutSize;
    float DelayTarget;

    extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fVerbose );
@ -5516,8 +5624,9 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
    fSwitching  = 0;
    fVerbose    = 0;
    DelayTarget =-1;
+    nLutSize    =-1;
    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "apvhD" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "apvhDK" ) ) != EOF )
    {
        switch ( c )
        {
@ -5543,6 +5652,17 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
            if ( DelayTarget <= 0.0 ) 
                goto usage;
            break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 ) 
+                goto usage;
+            break;
        default:
            goto usage;
        }
@ -5560,6 +5680,10 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
        return 1;
    }

+    // create the new LUT library
+    if ( nLutSize >= 3 && nLutSize <= 6 )
+        Fpga_SetSimpleLutLib( nLutSize );
+
    if ( !Abc_NtkIsStrash(pNtk) )
    {
        // strash and balance the network
@ -5606,13 +5730,18 @@ usage:
        sprintf( Buffer, "not used" );
    else
        sprintf( Buffer, "%.2f", DelayTarget );
-    fprintf( pErr, "usage: fpga [-D float] [-apvh]\n" );
-    fprintf( pErr, "\t        performs FPGA mapping of the current network\n" );
-    fprintf( pErr, "\t-a    : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
-    fprintf( pErr, "\t-p    : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" );
-    fprintf( pErr, "\t-D    : sets the required time for the mapping [default = %s]\n", Buffer );  
-    fprintf( pErr, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h    : prints the command usage\n");
+    if ( nLutSize == -1 ) 
+        sprintf( LutSize, "library" );
+    else
+        sprintf( LutSize, "%d", nLutSize );
+    fprintf( pErr, "usage: fpga [-D float] [-K num] [-apvh]\n" );
+    fprintf( pErr, "\t           performs FPGA mapping of the current network\n" );
+    fprintf( pErr, "\t-a       : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
+    fprintf( pErr, "\t-p       : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" );
+    fprintf( pErr, "\t-D float : sets the required time for the mapping [default = %s]\n", Buffer );  
+    fprintf( pErr, "\t-K num   : the number of LUT inputs [default = %s]%s\n", LutSize, (nLutSize == -1 ? " (type \"print_lut\")" : "") );
+    fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h       : prints the command usage\n");
    return 1;
 }

--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@ -314,7 +314,7 @@ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
 {
    Abc_Obj_t * pFanin;
    int fDagNode, fTriv, TreeCode = 0;
-    assert( Abc_NtkIsStrash(pObj->pNtk) );
+//    assert( Abc_NtkIsStrash(pObj->pNtk) );
    assert( Abc_ObjFaninNum(pObj) == 2 );
    // check if the node is a DAG node
    fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj));
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@ -85,7 +85,9 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )

 //    Ivy_MffcTest( pMan );
    Ivy_ManPrintStats( pMan );
-    Ivy_ManSeqRewrite( pMan, 0, 0 );
+//    Ivy_ManSeqRewrite( pMan, 0, 0 );
+//    Ivy_ManTestCutsAlg( pMan );
+    Ivy_ManTestCutsBool( pMan );
    Ivy_ManPrintStats( pMan );

    // convert from the AIG manager
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@ -0,0 +1,786 @@
+/**CFile****************************************************************
+
+  FileName    [abcLut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Superchoicing for K-LUTs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcLut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define SCL_LUT_MAX          6   // the maximum LUT size
+#define SCL_VARS_MAX        15   // the maximum number of variables
+#define SCL_NODE_MAX      1000   // the maximum number of nodes
+
+typedef struct Abc_ManScl_t_ Abc_ManScl_t;
+struct Abc_ManScl_t_
+{
+    // paramers
+    int                nLutSize;    // the LUT size
+    int                nCutSizeMax; // the max number of leaves of the cone
+    int                nNodesMax;   // the max number of divisors in the cone
+    int                nWords;      // the number of machine words in sim info
+    // structural representation of the cone
+    Vec_Ptr_t *        vLeaves;     // leaves of the cut
+    Vec_Ptr_t *        vVolume;     // volume of the cut
+    int                pBSet[SCL_VARS_MAX]; // bound set
+    // functional representation of the cone
+    unsigned *         uTruth;      // truth table of the cone
+    // representation of truth tables
+    unsigned **        uVars;       // elementary truth tables
+    unsigned **        uSims;       // truth tables of the nodes
+    unsigned **        uCofs;       // truth tables of the cofactors
+};
+
+static Vec_Ptr_t * s_pLeaves = NULL;
+
+static Cut_Man_t * Abc_NtkStartCutManForScl( Abc_Ntk_t * pNtk, int nLutSize );
+static Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax );
+static void Abc_ManSclStop( Abc_ManScl_t * p );
+static void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj );
+
+static Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * pManScl, Abc_Obj_t * pObj );
+static int Abc_NodeDecomposeStep( Abc_ManScl_t * pManScl );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for K-LUTs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int fVerbose )
+{
+    ProgressBar * pProgress;
+    Abc_ManCut_t * pManCut;
+    Abc_ManScl_t * pManScl;
+    Cut_Man_t * pManCuts;
+    Abc_Obj_t * pObj, * pFanin, * pObjTop;
+    int i, LevelMax, nNodes;
+    int nNodesTried, nNodesDec, nNodesExist, nNodesUsed;
+
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    if ( nLutSize < 3 || nLutSize > SCL_LUT_MAX )
+    {
+        printf( "LUT size (%d) does not belong to the interval: 3 <= LUT size <= %d\n", nLutSize, SCL_LUT_MAX );
+        return 0;
+    }
+    if ( nCutSizeMax <= nLutSize || nCutSizeMax > SCL_VARS_MAX )
+    {
+        printf( "Cut size (%d) does not belong to the interval: LUT size (%d) < Cut size <= %d\n", nCutSizeMax, nLutSize, SCL_VARS_MAX );
+        return 0;
+    }
+
+    assert( nLutSize <= SCL_LUT_MAX );
+    assert( nCutSizeMax <= SCL_VARS_MAX );
+    nNodesTried = nNodesDec = nNodesExist = nNodesUsed = 0;
+
+    // set the delays of the CIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->Level = 0;
+
+//Abc_NtkGetLevelNum( pNtk );
+ 
+    // start the managers
+    pManScl = Abc_ManSclStart( nLutSize, nCutSizeMax, 1000 );
+    pManCuts = Abc_NtkStartCutManForScl( pNtk, nLutSize );
+    pManCut = Abc_NtkManCutStart( nCutSizeMax, 100000, 100000, 100000 );
+    s_pLeaves = Abc_NtkManCutReadCutSmall( pManCut );
+    pManScl->vVolume = Abc_NtkManCutReadVisited( pManCut );
+
+    // process each internal node (assuming topological order of nodes!!!)
+    nNodes = Abc_NtkObjNumMax(pNtk);
+    pProgress = Extra_ProgressBarStart( stdout, nNodes );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+//        if ( i != nNodes-1 )
+//            continue;
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( i >= nNodes )
+            break;
+        if ( Abc_ObjFaninNum(pObj) != 2 )
+            continue;
+        nNodesTried++;
+
+        // map this node using regular cuts
+//        pObj->Level = 0;
+        Abc_NodeLutMap( pManCuts, pObj );
+        // compute the cut
+        pManScl->vLeaves = Abc_NodeFindCut( pManCut, pObj, 0 );
+        if ( Vec_PtrSize(pManScl->vLeaves) <= nLutSize )
+            continue;
+        // get the volume of the cut
+        if ( Vec_PtrSize(pManScl->vVolume) > SCL_NODE_MAX )
+            continue;
+        nNodesDec++;
+
+        // decompose the cut
+        pObjTop = Abc_NodeSuperChoiceLut( pManScl, pObj );
+        if ( pObjTop == NULL )
+            continue;
+        nNodesExist++;
+
+        // if there is no delay improvement, skip; otherwise, update level
+        if ( pObjTop->Level >= pObj->Level )
+        {
+            Abc_NtkDeleteObj_rec( pObjTop );
+            continue;
+        }
+        pObj->Level = pObjTop->Level;
+        nNodesUsed++;
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // delete the managers
+    Abc_ManSclStop( pManScl );
+    Abc_NtkManCutStop( pManCut );
+    Cut_ManStop( pManCuts );
+
+    // get the largest arrival time
+    LevelMax = 0;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0( pObj );
+        // skip inv/buf
+        if ( Abc_ObjFaninNum(pFanin) == 1 )
+            pFanin = Abc_ObjFanin0( pFanin );
+        // get the new level
+        LevelMax = ABC_MAX( LevelMax, (int)pFanin->Level );
+    }
+
+    if ( fVerbose )
+    printf( "Try = %d. Dec = %d. Exist = %d. Use = %d. SUPER = %d levels of %d-LUTs.\n", 
+        nNodesTried, nNodesDec, nNodesExist, nNodesUsed, LevelMax, nLutSize );
+//    if ( fVerbose )
+//    printf( "The network is superchoiced for %d levels of %d-LUTs.\n", LevelMax, nLutSize );
+
+    // clean the data field
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pNext = NULL;
+
+    // check
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkSuperChoiceLut: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs LUT mapping of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj )
+{
+    Cut_Cut_t * pCut;
+    Abc_Obj_t * pFanin;
+    int i, DelayMax;
+    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCuts, pObj, 0, 0 );
+    assert( pCut != NULL );
+    assert( pObj->Level == 0 );
+    // go through the cuts
+    pObj->Level = ABC_INFINITY;
+    for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
+    {
+        DelayMax = 0;
+        for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        {
+            pFanin = Abc_NtkObj( pObj->pNtk, pCut->pLeaves[i] );
+//            assert( Abc_ObjIsCi(pFanin) || pFanin->Level > 0 ); // should hold if node ordering is topological
+            if ( DelayMax < (int)pFanin->Level )
+                DelayMax = pFanin->Level;
+        }
+        if ( (int)pObj->Level > DelayMax )
+            pObj->Level = DelayMax;
+    }
+    assert( pObj->Level < ABC_INFINITY );
+    pObj->Level++;
+//    printf( "%d(%d) ", pObj->Id, pObj->Level );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut manager for rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkStartCutManForScl( Abc_Ntk_t * pNtk, int nLutSize )
+{
+    static Cut_Params_t Params, * pParams = &Params;
+    Cut_Man_t * pManCut;
+    Abc_Obj_t * pObj;
+    int i;
+    // start the cut manager
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = nLutSize; // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 500;   // the max number of cuts kept at a node
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
+    pParams->fSeq      = 0;     // compute sequential cuts
+    pParams->fDrop     = 0;     // drop cuts on the fly
+    pParams->fVerbose  = 0;     // the verbosiness flag
+    pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
+    pManCut = Cut_ManStart( pParams );
+    if ( pParams->fDrop )
+        Cut_ManSetFanoutCounts( pManCut, Abc_NtkFanoutCounts(pNtk) );
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_NodeSetTriv( pManCut, pObj->Id );
+    return pManCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax )
+{
+    Abc_ManScl_t * p;
+    int i, k;
+    assert( sizeof(unsigned) == 4 );
+    p = ALLOC( Abc_ManScl_t, 1 );
+    memset( p, 0, sizeof(Abc_ManScl_t) );
+    p->nLutSize    = nLutSize;
+    p->nCutSizeMax = nCutSizeMax;
+    p->nNodesMax   = nNodesMax;
+    p->nWords      = Extra_TruthWordNum(nCutSizeMax);
+    // allocate simulation info
+    p->uVars = (unsigned **)Extra_ArrayAlloc( nCutSizeMax, p->nWords, 4 );
+    p->uSims = (unsigned **)Extra_ArrayAlloc( nNodesMax, p->nWords, 4 );
+    p->uCofs = (unsigned **)Extra_ArrayAlloc( 2 << nLutSize, p->nWords, 4 );
+    memset( p->uVars[0], 0, nCutSizeMax * p->nWords * 4 );
+    // assign elementary truth tables
+    for ( k = 0; k < p->nCutSizeMax; k++ )
+        for ( i = 0; i < p->nWords * 32; i++ )
+            if ( i & (1 << k) )
+                p->uVars[k][i>>5] |= (1 << (i&31));
+    // other data structures
+//    p->vBound = Vec_IntAlloc( nCutSizeMax );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManSclStop( Abc_ManScl_t * p )
+{
+//    Vec_IntFree( p->vBound );
+    free( p->uVars );
+    free( p->uSims );
+    free( p->uCofs );
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Abc_NodeSuperChoiceTruth( Abc_ManScl_t * pManScl )
+{
+    Abc_Obj_t * pObj;
+    unsigned * puData0, * puData1, * puData;
+    char * pSop;
+    int i, k;
+    // set elementary truth tables
+    Vec_PtrForEachEntry( pManScl->vLeaves, pObj, i )
+        pObj->pNext = (Abc_Obj_t *)pManScl->uVars[i];
+    // compute truth tables for internal nodes
+    Vec_PtrForEachEntry( pManScl->vVolume, pObj, i )
+    {
+        // set storage for the node's simulation info
+        pObj->pNext = (Abc_Obj_t *)pManScl->uSims[i];
+        // get pointer to the simulation info
+        puData  = (unsigned *)pObj->pNext;
+        puData0 = (unsigned *)Abc_ObjFanin0(pObj)->pNext;
+        puData1 = (unsigned *)Abc_ObjFanin1(pObj)->pNext;
+        // simulate
+        pSop = pObj->pData;
+        if ( pSop[0] == '0' && pSop[1] == '0' )
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = ~puData0[k] & ~puData1[k];
+        else if ( pSop[0] == '0' )
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = ~puData0[k] & puData1[k];
+        else if ( pSop[1] == '0' )
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = puData0[k] & ~puData1[k];
+        else 
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = puData0[k] & puData1[k];
+    }
+    return puData;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect2_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vVolume )
+{
+    if ( pObj->fMarkC )
+        return;
+    pObj->fMarkC = 1;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    Abc_NodeSuperChoiceCollect2_rec( Abc_ObjFanin0(pObj), vVolume );
+    Abc_NodeSuperChoiceCollect2_rec( Abc_ObjFanin1(pObj), vVolume );
+    Vec_PtrPush( vVolume, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect2( Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkC = 1;
+    Vec_PtrClear( vVolume );
+    Abc_NodeSuperChoiceCollect2_rec( pRoot, vVolume );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkC = 0;
+    Vec_PtrForEachEntry( vVolume, pObj, i )
+        pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+    if ( pObj->fMarkB )
+    {
+        Vec_PtrPush( vLeaves, pObj );
+        pObj->fMarkB = 0;
+    }
+    if ( pObj->fMarkC )
+        return;
+    pObj->fMarkC = 1;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    Abc_NodeSuperChoiceCollect_rec( Abc_ObjFanin0(pObj), vLeaves, vVolume );
+    Abc_NodeSuperChoiceCollect_rec( Abc_ObjFanin1(pObj), vLeaves, vVolume );
+    Vec_PtrPush( vVolume, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description [Orders the leaves topologically.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect( Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+    Abc_Obj_t * pObj;
+    int i, nLeaves;
+    nLeaves = Vec_PtrSize(vLeaves);
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkB = pObj->fMarkC = 1;
+    Vec_PtrClear( vVolume );
+    Vec_PtrClear( vLeaves );
+    Abc_NodeSuperChoiceCollect_rec( pRoot, vLeaves, vVolume );
+    assert( Vec_PtrSize(vLeaves) == nLeaves );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkC = 0;
+    Vec_PtrForEachEntry( vVolume, pObj, i )
+        pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeLeavesRemove( Vec_Ptr_t * vLeaves, unsigned uPhase, int nVars )
+{
+    int i;
+    for ( i = nVars - 1; i >= 0; i-- )
+        if ( uPhase & (1 << i) )
+            Vec_PtrRemove( vLeaves, Vec_PtrEntry(vLeaves, i) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeGetLevel( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, Level;
+    Level = 0;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Level = ABC_MAX( Level, (int)pFanin->Level );
+    return Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * p, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin, * pObjNew;
+    int i, nVars, uSupport, nSuppVars;
+    // collect the cone using DFS (excluding leaves)
+    Abc_NodeSuperChoiceCollect2( pObj, p->vLeaves, p->vVolume );
+    assert( Vec_PtrEntryLast(p->vVolume) == pObj );  
+    // compute the truth table
+    p->uTruth = Abc_NodeSuperChoiceTruth( p );
+    // get the support of this truth table
+    nVars = Vec_PtrSize(p->vLeaves);
+    uSupport = Extra_TruthSupport(p->uTruth, nVars);
+    nSuppVars = Extra_WordCountOnes(uSupport);
+    assert( nSuppVars <= nVars );
+    if ( nSuppVars == 0 )
+    {
+        pObj->Level = 0;
+        return NULL;
+    }
+    if ( nSuppVars == 1 )
+    {
+        // find the variable
+        for ( i = 0; i < nVars; i++ )
+            if ( uSupport & (1 << i) )
+                break;
+        assert( i < nVars );
+        pFanin = Vec_PtrEntry( p->vLeaves, i );
+        pObj->Level = pFanin->Level;
+        return NULL;
+    }
+    // support-minimize the truth table
+    if ( nSuppVars != nVars )
+    {
+        Extra_TruthShrink( p->uCofs[0], p->uTruth, nSuppVars, nVars, uSupport );
+        Extra_TruthCopy( p->uTruth, p->uCofs[0], nVars );
+        Abc_NodeLeavesRemove( p->vLeaves, ((1 << nVars) - 1) & ~uSupport, nVars );
+    }
+//    return NULL;
+    // decompose the truth table recursively
+    while ( Vec_PtrSize(p->vLeaves) > p->nLutSize )
+        if ( !Abc_NodeDecomposeStep( p ) )
+        {
+            Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
+                if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 0 )
+                    Abc_NtkDeleteObj_rec( pFanin );
+            return NULL;
+        }
+    // create the topmost node
+    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+    Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
+        Abc_ObjAddFanin( pObjNew, pFanin );
+    // create the function
+    pObjNew->pData = Abc_SopCreateFromTruth( pObj->pNtk->pManFunc, Vec_PtrSize(p->vLeaves), p->uTruth ); // need ISOP
+    pObjNew->Level = Abc_NodeGetLevel( pObjNew );
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in increasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeCompareLevelsInc( int * pp1, int * pp2 )
+{
+    Abc_Obj_t * pNode1, * pNode2;
+    pNode1 = Vec_PtrEntry(s_pLeaves, *pp1);
+    pNode2 = Vec_PtrEntry(s_pLeaves, *pp2);
+    if ( pNode1->Level < pNode2->Level )
+        return -1;
+    if ( pNode1->Level > pNode2->Level ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects the earliest arriving nodes from the array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeDecomposeSort( Abc_Obj_t ** pLeaves, int nVars, int * pBSet, int nLutSize )
+{
+    Abc_Obj_t * pTemp[SCL_VARS_MAX];
+    int i, k, kBest, LevelMin;
+    assert( nLutSize < nVars );
+    assert( nVars <= SCL_VARS_MAX );
+    // copy nodes into the internal storage
+//    printf( "(" );
+    for ( i = 0; i < nVars; i++ )
+    {
+        pTemp[i] = pLeaves[i];
+//        printf( " %d", pLeaves[i]->Level );
+    }
+//    printf( " )\n" );
+    // choose one node at a time
+    for ( i = 0; i < nLutSize; i++ )
+    {
+        kBest = -1;
+        LevelMin = ABC_INFINITY;
+        for ( k = 0; k < nVars; k++ )
+            if ( pTemp[k] && LevelMin > (int)pTemp[k]->Level )
+            {
+                LevelMin = pTemp[k]->Level;
+                kBest = k;
+            }
+        pBSet[i] = kBest;
+        pTemp[kBest] = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeDecomposeStep( Abc_ManScl_t * p )
+{
+    static char pCofClasses[1<<SCL_LUT_MAX][1<<SCL_LUT_MAX];
+    static char nCofClasses[1<<SCL_LUT_MAX];
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObjNew, * pFanin, * pNodesNew[SCL_LUT_MAX];
+    unsigned * pTruthCof, * pTruthClass, * pTruth, uPhase;
+    int i, k, c, v, w, nVars, nVarsNew, nClasses, nCofs;
+    // set the network
+    pNtk = ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, 0))->pNtk;
+    // find the earliest nodes
+    nVars = Vec_PtrSize(p->vLeaves);
+    assert( nVars > p->nLutSize );
+/*
+    for ( v = 0; v < nVars; v++ )
+        p->pBSet[v] = v;
+    qsort( (void *)p->pBSet, nVars, sizeof(int), 
+            (int (*)(const void *, const void *)) Abc_NodeCompareLevelsInc );
+*/
+    Abc_NodeDecomposeSort( (Abc_Obj_t **)Vec_PtrArray(p->vLeaves), Vec_PtrSize(p->vLeaves), p->pBSet, p->nLutSize );
+    assert( ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, p->pBSet[0]))->Level <=
+        ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, p->pBSet[1]))->Level );
+    // cofactor w.r.t. the selected variables
+    Extra_TruthCopy( p->uCofs[1], p->uTruth, nVars );
+    c = 2;
+    for ( v = 0; v < p->nLutSize; v++ )
+        for ( k = 0; k < (1<<v); k++ )
+        {
+            Extra_TruthCopy( p->uCofs[c], p->uCofs[c/2], nVars );
+            Extra_TruthCopy( p->uCofs[c+1], p->uCofs[c/2], nVars );
+            Extra_TruthCofactor0( p->uCofs[c], nVars, p->pBSet[v] );
+            Extra_TruthCofactor1( p->uCofs[c+1], nVars, p->pBSet[v] );
+            c += 2;
+        }
+    assert( c == (2 << p->nLutSize) );
+    // count unique cofactors
+    nClasses = 0;
+    nCofs = (1 << p->nLutSize);
+    for ( i = 0; i < nCofs; i++ )
+    {
+        pTruthCof = p->uCofs[ nCofs + i ];
+        for ( k = 0; k < nClasses; k++ )
+        {
+            pTruthClass = p->uCofs[ nCofs + pCofClasses[k][0] ];
+            if ( Extra_TruthIsEqual( pTruthCof, pTruthClass, nVars ) )
+            {
+                pCofClasses[k][ nCofClasses[k]++ ] = i;
+                break;
+            }
+        }
+        if ( k != nClasses )
+            continue;
+        // not found
+        pCofClasses[nClasses][0] = i;
+        nCofClasses[nClasses] = 1;
+        nClasses++;
+        if ( nClasses > nCofs/2 )
+            return 0;
+    }
+    // the number of cofactors is acceptable
+    nVarsNew = Extra_Base2Log( nClasses );
+    assert( nVarsNew < p->nLutSize );
+    // create the remainder truth table
+    // for each class of cofactors, multiply cofactor truth table by its code
+    Extra_TruthClear( p->uTruth, nVars );
+    for ( k = 0; k < nClasses; k++ )
+    {
+        pTruthClass = p->uCofs[ nCofs + pCofClasses[k][0] ];
+        for ( v = 0; v < nVarsNew; v++ )
+            if ( k & (1 << v) )
+                Extra_TruthAnd( pTruthClass, pTruthClass, p->uVars[p->pBSet[v]], nVars );
+            else
+                Extra_TruthSharp( pTruthClass, pTruthClass, p->uVars[p->pBSet[v]], nVars );
+        Extra_TruthOr( p->uTruth, p->uTruth, pTruthClass, nVars );
+    }
+    // create nodes
+    pTruth = p->uCofs[0];
+    for ( v = 0; v < nVarsNew; v++ )
+    {
+        Extra_TruthClear( pTruth, p->nLutSize );
+        for ( k = 0; k < nClasses; k++ )
+            if ( k & (1 << v) )
+                for ( i = 0; i < nCofClasses[k]; i++ )
+                {
+                    pTruthCof = p->uCofs[1];
+                    Extra_TruthFill( pTruthCof, p->nLutSize );
+                    for ( w = 0; w < p->nLutSize; w++ )
+                        if ( pCofClasses[k][i] & (1 << (p->nLutSize-1-w)) )
+                            Extra_TruthAnd( pTruthCof, pTruthCof, p->uVars[w], p->nLutSize );
+                        else
+                            Extra_TruthSharp( pTruthCof, pTruthCof, p->uVars[w], p->nLutSize );
+                    Extra_TruthOr( pTruth, pTruth, pTruthCof, p->nLutSize );
+                }
+        // implement the node
+        pObjNew = Abc_NtkCreateNode( pNtk );
+        for ( i = 0; i < p->nLutSize; i++ )
+        {
+            pFanin = Vec_PtrEntry( p->vLeaves, p->pBSet[i] );
+            Abc_ObjAddFanin( pObjNew, pFanin );
+        }
+        // create the function
+        pObjNew->pData = Abc_SopCreateFromTruth( pNtk->pManFunc, p->nLutSize, pTruth ); // need ISOP
+        pObjNew->Level = Abc_NodeGetLevel( pObjNew );
+        pNodesNew[v] = pObjNew;
+    }
+    // put the new nodes back into the list
+    for ( v = 0; v < nVarsNew; v++ )
+        Vec_PtrWriteEntry( p->vLeaves, p->pBSet[v], pNodesNew[v] );
+    // compute the variables that should be removed
+    uPhase = 0;
+    for ( v = nVarsNew; v < p->nLutSize; v++ )
+        uPhase |= (1 << p->pBSet[v]);
+    // remove entries from the array
+    Abc_NodeLeavesRemove( p->vLeaves, uPhase, nVars );
+    // update truth table
+    Extra_TruthShrink( p->uCofs[0], p->uTruth, nVars - p->nLutSize + nVarsNew, nVars, ((1 << nVars) - 1) & ~uPhase );
+    Extra_TruthCopy( p->uTruth, p->uCofs[0], nVars );
+    assert( !Extra_TruthVarInSupport( p->uTruth, nVars, nVars - p->nLutSize + nVarsNew ) );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@ -135,18 +135,18 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
    }
 */

-/*
+
    // print the statistic into a file
    {
        FILE * pTable;
-        pTable = fopen( "stats.txt", "a+" );
+        pTable = fopen( "fpga_stats.txt", "a+" );
        fprintf( pTable, "%s ",  pNtk->pName );
        fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
        fprintf( pTable, "%d ", Abc_AigGetLevelNum(pNtk) );
        fprintf( pTable, "\n" );
        fclose( pTable );
    }
-*/
+
 /*
    // print the statistic into a file
    {
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@ -321,7 +321,8 @@ int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int
    {
        CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
 //printf( "    Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur );
-        if ( CostBest > CostCur )
+        if ( CostBest > CostCur ||
+             (CostBest == CostCur && pNode->Level > pFaninBest->Level) )
        {
            CostBest   = CostCur;
            pFaninBest = pNode;
@ -632,6 +633,22 @@ Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p )
    return p->vConeLeaves;
 }

+/**Function*************************************************************
+
+  Synopsis    [Returns the leaves of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p )
+{
+    return p->vNodeLeaves;
+}
+
 /**Function*************************************************************

  Synopsis    [Returns the leaves of the cone.]
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@ -11,7 +11,7 @@ SRC +=    src/base/abci/abc.c \
    src/base/abci/abcFraig.c \
        src/base/abci/abcFxu.c \
        src/base/abci/abcGen.c \
-    src/base/abci/abcIvy.c \
+    src/base/abci/abcLut.c \
    src/base/abci/abcMap.c \
    src/base/abci/abcMiter.c \
    src/base/abci/abcNtbdd.c \
--- a/src/map/fpga/fpga.c
+++ b/src/map/fpga/fpga.c
@ -235,6 +235,39 @@ usage:
    return 1;       /* error exit */
 }

+/**Function*************************************************************
+
+  Synopsis    [Sets simple LUT library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fpga_SetSimpleLutLib( int nLutSize )
+{
+    Fpga_LutLib_t s_LutLib6 = { "lutlib", 6, {0,1,1,1,1,1,1}, {0,1,1,1,1,1,1} };
+    Fpga_LutLib_t s_LutLib5 = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
+    Fpga_LutLib_t s_LutLib4 = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} };
+    Fpga_LutLib_t s_LutLib3 = { "lutlib", 3, {0,1,1,1}, {0,1,1,1} };
+    Fpga_LutLib_t * pLutLib;
+    assert( nLutSize >= 3 && nLutSize <= 6 );
+    switch ( nLutSize )
+    {
+        case 3: pLutLib = &s_LutLib3; break;
+        case 4: pLutLib = &s_LutLib4; break;
+        case 5: pLutLib = &s_LutLib5; break;
+        case 6: pLutLib = &s_LutLib6; break;
+        default: pLutLib = NULL; break;
+    }
+    if ( pLutLib == NULL )
+        return;
+    Fpga_LutLibFree( Abc_FrameReadLibLut() );
+    Abc_FrameSetLibLut( Fpga_LutLibDup(pLutLib) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
--- a/src/map/fpga/fpga.h
+++ b/src/map/fpga/fpga.h
@ -156,6 +156,8 @@ extern int             Fpga_CutVolume( Fpga_Cut_t * pCut );
 extern int             Fpga_ManCheckConsistency( Fpga_Man_t * p );
 extern void            Fpga_ManCleanData0( Fpga_Man_t * pMan );
 extern Fpga_NodeVec_t * Fpga_CollectNodeTfo( Fpga_Man_t * pMan, Fpga_Node_t * pNode );
+/*=== fpga.c =============================================================*/
+extern void            Fpga_SetSimpleLutLib( int nLutSize );

 #ifdef __cplusplus
 }
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@ -28,7 +28,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include "extra.h"
-#include "fraig.h"
 #include "fpga.h"

 ////////////////////////////////////////////////////////////////////////
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@ -417,12 +417,40 @@ static inline int Extra_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVar
            return 0;
    return 1;
 }
+static inline int Extra_TruthIsConst0( unsigned * pIn, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        if ( pIn[w] )
+            return 0;
+    return 1;
+}
+static inline int Extra_TruthIsConst1( unsigned * pIn, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        if ( pIn[w] != ~(unsigned)0 )
+            return 0;
+    return 1;
+}
 static inline void Extra_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
 {
    int w;
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn[w];
 }
+static inline void Extra_TruthClear( unsigned * pOut, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = 0;
+}
+static inline void Extra_TruthFill( unsigned * pOut, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = ~(unsigned)0;
+}
 static inline void Extra_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
 {
    int w;
@ -435,6 +463,18 @@ static inline void Extra_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned *
    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn0[w] & pIn1[w];
 }
+static inline void Extra_TruthOr( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = pIn0[w] | pIn1[w];
+}
+static inline void Extra_TruthSharp( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = pIn0[w] & ~pIn1[w];
+}
 static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
 {
    int w;
--- a/src/misc/extra/extraUtilTruth.c
+++ b/src/misc/extra/extraUtilTruth.c
@ -184,8 +184,8 @@ void Extra_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, i
  Synopsis    [Expands the truth table according to the phase.]

  Description [The input and output truth tables are in pIn/pOut. The current number
-  of variables is nVars. The total number of variables in nVarsAll. The last variable
-  (Phase) contains shows how the variables should be moved.]
+  of variables is nVars. The total number of variables in nVarsAll. The last argument
+  (Phase) contains shows where the variables should go.]
               
  SideEffects []

@ -218,8 +218,8 @@ void Extra_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAl
  Synopsis    [Shrinks the truth table according to the phase.]

  Description [The input and output truth tables are in pIn/pOut. The current number
-  of variables is nVars. The total number of variables in nVarsAll. The last variable
-  (Phase) contains shows how the variables should be moved.]
+  of variables is nVars. The total number of variables in nVarsAll. The last argument
+  (Phase) contains shows what variables should remain.]
               
  SideEffects []

--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@ -17,7 +17,6 @@
 ***********************************************************************/

 #include "fxuInt.h" 
-//#include "mvc.h"
 #include "fxu.h"

 ////////////////////////////////////////////////////////////////////////
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@ -198,6 +198,481 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi
    assert( Vec_IntSize(vFront) <= nSize );
 }

+
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison for node pointers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
+{
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing one algebraic cut.]
+
+  Description [Returns 1 if the tree-leaves of this node where traversed 
+  and found to have no external references (and have not been collected). 
+  Returns 0 if the tree-leaves have external references and are collected.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pRoot, Ivy_Type_t Type, Vec_Ptr_t * vFront )
+{
+    int RetValue0, RetValue1;
+    Ivy_Obj_t * pRootR = Ivy_Regular(pRoot);
+    assert( Type != IVY_EXOR || !Ivy_IsComplement(pRoot) );
+    // if the node is a buffer skip through it
+    if ( Ivy_ObjIsBuf(pRootR) )
+        return Ivy_ManFindAlgCut_rec( Ivy_NotCond(Ivy_ObjChild0(pRootR), Ivy_IsComplement(pRoot)), Type, vFront );
+    // if the node is the end of the tree, return
+    if ( Ivy_IsComplement(pRoot) || Ivy_ObjIsCi(pRoot) || Ivy_ObjType(pRoot) != Type )
+    {
+        if ( Ivy_ObjRefs(pRootR) == 1 )
+            return 1;
+        assert( Ivy_ObjRefs(pRootR) > 1 );
+        Vec_PtrPush( vFront, pRoot );
+        return 0;
+    }
+    // branch on the node
+    assert( Ivy_ObjIsNode(pRoot) );
+    RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild0(pRoot), Type, vFront );
+    RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild1(pRoot), Type, vFront );
+    // the case when both have no external referenced
+    if ( RetValue0 && RetValue1 )
+    {
+        if ( Ivy_ObjRefs(pRoot) == 1 )
+            return 1;
+        assert( Ivy_ObjRefs(pRoot) > 1 );
+        Vec_PtrPush( vFront, pRoot );
+        return 0;
+    }
+    // the case when one of them has external references
+    if ( RetValue0 )
+        Vec_PtrPush( vFront, Ivy_ObjChild0(pRoot) );
+    if ( RetValue1 )
+        Vec_PtrPush( vFront, Ivy_ObjChild1(pRoot) );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing one algebraic cut.]
+
+  Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge,
+  (c) boundary of different gates. Returns 1 if this is a pure tree.
+  Returns -1 if the contant 0 is detected. Return 0 if the array can be used.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront )
+{
+    Ivy_Obj_t * pObj, * pPrev;
+    int RetValue, i, k;
+    assert( !Ivy_IsComplement(pRoot) );
+    // clear the frontier and collect the nodes
+    Vec_PtrClear( vFront );
+    RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront );
+    // return if the node is the root of a tree
+    if ( RetValue == 1 )
+        return 1;
+    // sort the entries to in increasing order
+    Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare );
+    // remove duplicated
+    k = 1;
+    Vec_PtrForEachEntryStart( vFront, pObj, i, 1 )
+    {
+        pPrev = (k == 0 ? NULL : Vec_PtrEntry(vFront, k-1));
+        if ( pObj == pPrev )
+        {
+            if ( Ivy_ObjIsExor(pRoot) )
+                k--;
+            continue;
+        }
+        if ( pObj == Ivy_Not(pPrev) )
+            return -1;
+        Vec_PtrWriteEntry( vFront, k++, pObj );
+    }
+    if ( k == 0 )
+        return -1;
+    Vec_PtrShrink( vFront, k );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManTestCutsAlg( Ivy_Man_t * p )
+{
+    Vec_Ptr_t * vFront;
+    Ivy_Obj_t * pObj, * pTemp;
+    int i, k, RetValue;
+    vFront = Vec_PtrAlloc( 100 );
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        if ( !Ivy_ObjIsNode(pObj) )
+            continue;
+        if ( Ivy_ObjIsMuxType(pObj) )
+        {
+            printf( "m " );
+            continue;
+        }
+        if ( pObj->Id == 509 )
+        {
+            int y = 0;
+        }
+
+        RetValue = Ivy_ManFindAlgCut( pObj, vFront );
+        if ( Ivy_ObjIsExor(pObj) )
+            printf( "x" );
+        if ( RetValue == -1 )
+            printf( "Const0 " );
+        else if ( RetValue == 1 || Vec_PtrSize(vFront) <= 2 )
+            printf( ". " );
+        else
+            printf( "%d ", Vec_PtrSize(vFront) );
+        
+        printf( "( " );
+        Vec_PtrForEachEntry( vFront, pTemp, k )
+            printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
+        printf( ")\n" );
+
+        if ( Vec_PtrSize(vFront) == 5 )
+        {
+            int x = 0;
+        }
+    }
+    printf( "\n" );
+    Vec_PtrFree( vFront );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computing Boolean cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindBoolCut_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume, Ivy_Obj_t * pPivot )
+{
+    int RetValue0, RetValue1;
+    if ( pObj == pPivot )
+    {
+        Vec_PtrPushUnique( vLeaves, pObj );
+        Vec_PtrPushUnique( vVolume, pObj );
+        return 1;        
+    }
+    if ( pObj->fMarkA )
+        return 0;
+
+//    assert( !Ivy_ObjIsCi(pObj) );
+    if ( Ivy_ObjIsCi(pObj) )
+        return 0;
+
+    if ( Ivy_ObjIsBuf(pObj) )
+    {
+        RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
+        if ( !RetValue0 )
+            return 0;
+        Vec_PtrPushUnique( vVolume, pObj );
+        return 1;
+    }
+    assert( Ivy_ObjIsNode(pObj) );
+    RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
+    RetValue1 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin1(pObj), vLeaves, vVolume, pPivot );
+    if ( !RetValue0 && !RetValue1 )
+        return 0;
+    // add new leaves
+    if ( !RetValue0 )
+    {
+        Vec_PtrPushUnique( vLeaves, Ivy_ObjFanin0(pObj) );
+        Vec_PtrPushUnique( vVolume, Ivy_ObjFanin0(pObj) );
+    }
+    if ( !RetValue1 )
+    {
+        Vec_PtrPushUnique( vLeaves, Ivy_ObjFanin1(pObj) );
+        Vec_PtrPushUnique( vVolume, Ivy_ObjFanin1(pObj) );
+    }
+    Vec_PtrPushUnique( vVolume, pObj );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the cost of one node (how many new nodes are added.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindBoolCutCost( Ivy_Obj_t * pObj )
+{
+    int Cost;
+    // make sure the node is in the construction zone
+    assert( pObj->fMarkA == 1 );  
+    // cannot expand over the PI node
+    if ( Ivy_ObjIsCi(pObj) )
+        return 999;
+    // always expand over the buffer
+    if ( Ivy_ObjIsBuf(pObj) )
+        return !Ivy_ObjFanin0(pObj)->fMarkA;
+    // get the cost of the cone
+    Cost = (!Ivy_ObjFanin0(pObj)->fMarkA) + (!Ivy_ObjFanin1(pObj)->fMarkA);
+    // return the number of nodes to be added to the leaves if this node is removed
+    return Cost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing Boolean cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolume, Vec_Ptr_t * vLeaves )
+{
+    Ivy_Obj_t * pObj, * pFaninC, * pFanin0, * pFanin1, * pPivot;
+    int RetValue, LevelLimit, Lev, k;
+    assert( !Ivy_IsComplement(pRoot) );
+    // clear the frontier and collect the nodes
+    Vec_PtrClear( vFront );
+    Vec_PtrClear( vVolume );
+    if ( Ivy_ObjIsMuxType(pRoot) )
+        pFaninC = Ivy_ObjRecognizeMux( pRoot, &pFanin0, &pFanin1 );
+    else
+    {
+        pFaninC = NULL;
+        pFanin0 = Ivy_ObjFanin0(pRoot);
+        pFanin1 = Ivy_ObjFanin1(pRoot); 
+    }
+    // start cone A
+    pFanin0->fMarkA = 1;
+    Vec_PtrPush( vFront, pFanin0 );
+    Vec_PtrPush( vVolume, pFanin0 );
+    // start cone B
+    pFanin1->fMarkB = 1;
+    Vec_PtrPush( vFront, pFanin1 );
+    Vec_PtrPush( vVolume, pFanin1 );
+    // iteratively expand until the common node (pPivot) is found or limit is reached
+    assert( Ivy_ObjLevel(pRoot) == Ivy_ObjLevelNew(pRoot) );
+    pPivot = NULL;
+    LevelLimit = IVY_MAX( Ivy_ObjLevel(pRoot) - 10, 1 );
+    for ( Lev = Ivy_ObjLevel(pRoot) - 1; Lev >= LevelLimit; Lev-- )
+    {
+        while ( 1 )
+        {
+            // find the next node to expand on this level
+            Vec_PtrForEachEntry( vFront, pObj, k )
+                if ( (int)pObj->Level == Lev )
+                    break;
+            if ( k == Vec_PtrSize(vFront) )
+                break;
+            assert( (int)pObj->Level <= Lev );
+            assert( pObj->fMarkA ^ pObj->fMarkB );
+            // remove the old node
+            Vec_PtrRemove( vFront, pObj );
+
+            // expand this node
+            pFanin0 = Ivy_ObjFanin0(pObj);
+            if ( !pFanin0->fMarkA && !pFanin0->fMarkB )
+            {
+                Vec_PtrPush( vFront, pFanin0 );
+                Vec_PtrPush( vVolume, pFanin0 );
+            }
+            // mark the new nodes
+            if ( pObj->fMarkA )
+                pFanin0->fMarkA = 1; 
+            if ( pObj->fMarkB )
+                pFanin0->fMarkB = 1; 
+
+            if ( Ivy_ObjIsBuf(pObj) )
+            {
+                if ( pFanin0->fMarkA && pFanin0->fMarkB )
+                {
+                    pPivot = pFanin0;
+                    break;
+                }
+                continue;
+            }
+
+            // expand this node
+            pFanin1 = Ivy_ObjFanin1(pObj); 
+            if ( !pFanin1->fMarkA && !pFanin1->fMarkB )
+            {
+                Vec_PtrPush( vFront, pFanin1 );
+                Vec_PtrPush( vVolume, pFanin1 );
+            }
+            // mark the new nodes
+            if ( pObj->fMarkA )
+                pFanin1->fMarkA = 1; 
+            if ( pObj->fMarkB )
+                pFanin1->fMarkB = 1; 
+
+            // consider if it is time to quit
+            if ( pFanin0->fMarkA && pFanin0->fMarkB )
+            {
+                pPivot = pFanin0;
+                break;
+            }
+            if ( pFanin1->fMarkA && pFanin1->fMarkB )
+            {
+                pPivot = pFanin1;
+                break;
+            }
+        }
+        if ( pPivot != NULL )
+            break;
+    }
+    if ( pPivot == NULL )
+        return 0;
+    // if the MUX control is defined, it should not be
+    if ( pFaninC && !pFaninC->fMarkA && !pFaninC->fMarkB )
+        Vec_PtrPush( vFront, pFaninC );
+    // clean the markings
+    Vec_PtrForEachEntry( vVolume, pObj, k )
+        pObj->fMarkA = pObj->fMarkB = 0;
+
+    // mark the nodes on the frontier (including the pivot)
+    Vec_PtrForEachEntry( vFront, pObj, k )
+        pObj->fMarkA = 1;
+    // cut exists, collect all the nodes on the shortest path to the pivot
+    Vec_PtrClear( vLeaves );
+    Vec_PtrClear( vVolume );
+    RetValue = Ivy_ManFindBoolCut_rec( pRoot, vLeaves, vVolume, pPivot );
+    assert( RetValue == 1 );
+    // unmark the nodes on the frontier (including the pivot)
+    Vec_PtrForEachEntry( vFront, pObj, k )
+        pObj->fMarkA = 0;
+
+    // mark the nodes in the volume
+    Vec_PtrForEachEntry( vVolume, pObj, k )
+        pObj->fMarkA = 1;
+    // expand the cut without increasing its size
+    while ( 1 )
+    {
+        Vec_PtrForEachEntry( vLeaves, pObj, k )
+            if ( Ivy_ManFindBoolCutCost(pObj) < 2 )
+                break;
+        if ( k == Vec_PtrSize(vLeaves) )
+            break;
+        // the node can be expanded
+        // remove the old node
+        Vec_PtrRemove( vLeaves, pObj );
+        // expand this node
+        pFanin0 = Ivy_ObjFanin0(pObj);
+        if ( !pFanin0->fMarkA )
+        {
+            pFanin0->fMarkA = 1;
+            Vec_PtrPush( vVolume, pFanin0 );
+            Vec_PtrPush( vLeaves, pFanin0 );
+        }
+        if ( Ivy_ObjIsBuf(pObj) )
+            continue;
+        // expand this node
+        pFanin1 = Ivy_ObjFanin1(pObj);
+        if ( !pFanin1->fMarkA )
+        {
+            pFanin1->fMarkA = 1;
+            Vec_PtrPush( vVolume, pFanin1 );
+            Vec_PtrPush( vLeaves, pFanin1 );
+        }        
+    }
+    // unmark the nodes in the volume
+    Vec_PtrForEachEntry( vVolume, pObj, k )
+        pObj->fMarkA = 0;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManTestCutsBool( Ivy_Man_t * p )
+{
+    Vec_Ptr_t * vFront, * vVolume, * vLeaves;
+    Ivy_Obj_t * pObj, * pTemp;
+    int i, k, RetValue;
+    vFront = Vec_PtrAlloc( 100 );
+    vVolume = Vec_PtrAlloc( 100 );
+    vLeaves = Vec_PtrAlloc( 100 );
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        if ( !Ivy_ObjIsNode(pObj) )
+            continue;
+        if ( Ivy_ObjIsMuxType(pObj) )
+        {
+            printf( "m" );
+            continue;
+        }
+        if ( Ivy_ObjIsExor(pObj) )
+            printf( "x" );
+        RetValue = Ivy_ManFindBoolCut( pObj, vFront, vVolume, vLeaves );
+        if ( RetValue == 0 )
+            printf( "- " );
+        else
+            printf( "%d ", Vec_PtrSize(vLeaves) );
+/*        
+        printf( "( " );
+        Vec_PtrForEachEntry( vFront, pTemp, k )
+            printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
+        printf( ")\n" );
+*/
+    }
+    printf( "\n" );
+    Vec_PtrFree( vFront );
+    Vec_PtrFree( vVolume );
+    Vec_PtrFree( vLeaves );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@ -5,6 +5,7 @@ SRC +=    src/temp/ivy/ivyBalance.c \
    src/temp/ivy/ivyDfs.c \
    src/temp/ivy/ivyDsd.c \
    src/temp/ivy/ivyMan.c \
+    src/temp/ivy/ivyMulti.c \
    src/temp/ivy/ivyObj.c \
    src/temp/ivy/ivyOper.c \
    src/temp/ivy/ivyRewrite.c \
--- a/src/temp/xyz/module.make
+++ b/src/temp/xyz/module.make
@ -0,0 +1,8 @@
+SRC +=    src/opt/xyz/xyzBuild.c \
+    src/opt/xyz/xyzCore.c \
+    src/opt/xyz/xyzMan.c \
+    src/opt/xyz/xyzMinEsop.c \
+    src/opt/xyz/xyzMinMan.c \
+    src/opt/xyz/xyzMinSop.c \
+    src/opt/xyz/xyzMinUtil.c \
+    src/opt/xyz/xyzTest.c 
--- a/src/temp/xyz/xyz.h
+++ b/src/temp/xyz/xyz.h
@ -0,0 +1,110 @@
+/**CFile****************************************************************
+
+  FileName    [xyz.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyz.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __XYZ_H__
+#define __XYZ_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#include "abc.h"
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Xyz_Man_t_  Xyz_Man_t;
+typedef struct Xyz_Obj_t_  Xyz_Obj_t;
+
+// storage for node information
+struct Xyz_Obj_t_
+{
+    Min_Cube_t *      pCover[3];    // pos/neg/esop
+    Vec_Int_t *       vSupp;        // computed support (all nodes except CIs)
+};
+
+// storage for additional information
+struct Xyz_Man_t_
+{
+    // general characteristics
+    int               nFaninMax;    // the number of vars
+    int               nCubesMax;    // the limit on the number of cubes in the intermediate covers
+    int               nWords;       // the number of words
+    Vec_Int_t *       vFanCounts;   // fanout counts
+    Vec_Ptr_t *       vObjStrs;     // object structures
+    void *            pMemory;      // memory for the internal data strctures
+    Min_Man_t *       pManMin;      // the cub manager
+    int               fUseEsop;     // enables ESOPs
+    int               fUseSop;      // enables SOPs
+    // arrays to map local variables
+    Vec_Int_t *       vComTo0;      // mapping of common variables into first fanin
+    Vec_Int_t *       vComTo1;      // mapping of common variables into second fanin
+    Vec_Int_t *       vPairs0;      // the first var in each pair of common vars
+    Vec_Int_t *       vPairs1;      // the second var in each pair of common vars
+    Vec_Int_t *       vTriv0;       // trival support of the first node
+    Vec_Int_t *       vTriv1;       // trival support of the second node
+    // statistics
+    int               nSupps;       // supports created
+    int               nSuppsMax;    // the maximum number of supports
+    int               nBoundary;    // the boundary size
+    int               nNodes;       // the number of nodes processed
+};
+
+static inline Xyz_Obj_t *  Abc_ObjGetStr( Abc_Obj_t * pObj )                       { return Vec_PtrEntry(((Xyz_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); }
+
+static inline void         Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec )    { Abc_ObjGetStr(pObj)->vSupp = vVec;   }
+static inline Vec_Int_t *  Abc_ObjGetSupp( Abc_Obj_t * pObj )                      { return Abc_ObjGetStr(pObj)->vSupp;   }
+
+static inline void         Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; }
+static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj )                    { return Abc_ObjGetStr(pObj)->pCover[2]; }
+
+static inline void         Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; }
+static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol )                    { return Abc_ObjGetStr(pObj)->pCover[Pol]; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== xyzBuild.c ==========================================================*/
+extern Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
+/*=== xyzCore.c ===========================================================*/
+extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
+/*=== xyzMan.c ============================================================*/
+extern Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax );
+extern void        Xyz_ManFree( Xyz_Man_t * p );
+extern void        Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj );
+/*=== xyzTest.c ===========================================================*/
+extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+
--- a/src/temp/xyz/xyzBuild.c
+++ b/src/temp/xyz/xyzBuild.c
@ -0,0 +1,379 @@
+/**CFile****************************************************************
+
+  FileName    [xyzBuild.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Network construction procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzBuild.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyz.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveCube( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp )
+{
+    Vec_Int_t * vLits;
+    Abc_Obj_t * pNodeNew, * pFanin;
+    int i, iFanin, Lit;
+    // create empty cube
+    if ( pCube->nLits == 0 )
+        return Abc_NodeCreateConst1(pNtkNew);
+    // get the literals of this cube
+    vLits = Vec_IntAlloc( 10 );
+    Min_CubeGetLits( pCube, vLits );
+    assert( pCube->nLits == (unsigned)vLits->nSize );
+    // create special case when there is only one literal
+    if ( pCube->nLits == 1 )
+    {
+        iFanin = Vec_IntEntry(vLits,0);
+        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
+        Lit = Min_CubeGetVar(pCube, iFanin);
+        assert( Lit == 1 || Lit == 2 );
+        Vec_IntFree( vLits );
+        if ( Lit == 1 )// negative
+            return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy );
+        return pFanin->pCopy;
+    }
+    assert( pCube->nLits > 1 );
+    // create the AND cube
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    for ( i = 0; i < vLits->nSize; i++ )
+    {
+        iFanin = Vec_IntEntry(vLits,i);
+        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
+        Lit = Min_CubeGetVar(pCube, iFanin);
+        assert( Lit == 1 || Lit == 2 );
+        Vec_IntWriteEntry( vLits, i, Lit==1 );
+        Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
+    }
+    pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
+    Vec_IntFree( vLits );
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveNode_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int Level )
+{
+    Min_Cube_t * pCover, * pCube;
+    Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
+    Vec_Int_t * vSupp;
+    int Entry, nCubes, i;
+
+    if ( Abc_ObjIsCi(pObj) )
+        return pObj->pCopy;
+    assert( Abc_ObjIsNode(pObj) );
+    // skip if already computed
+    if ( pObj->pCopy )
+        return pObj->pCopy;
+
+    // get the support and the cover
+    vSupp  = Abc_ObjGetSupp( pObj ); 
+    pCover = Abc_ObjGetCover2( pObj );
+    assert( vSupp );
+/*
+    if ( pCover &&  pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) > 0 )
+    {
+        printf( "%d\n ", pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) );
+        Min_CoverWrite( stdout, pCover );
+    }
+*/
+/*
+    // print the support of this node
+    printf( "{ " );
+    Vec_IntForEachEntry( vSupp, Entry, i )
+        printf( "%d ", Entry );
+    printf( "}  cubes = %d\n", Min_CoverCountCubes( pCover ) );
+*/
+    // process the fanins
+    Vec_IntForEachEntry( vSupp, Entry, i )
+    {
+        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
+        Abc_NtkXyzDeriveNode_rec( p, pNtkNew, pFanin, Level+1 );
+    }
+
+    // for each cube, construct the node
+    nCubes = Min_CoverCountCubes( pCover );
+    if ( nCubes == 0 )
+        pNodeNew = Abc_NodeCreateConst0(pNtkNew);
+    else if ( nCubes == 1 )
+        pNodeNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCover, vSupp );
+    else
+    {
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        Min_CoverForEachCube( pCover, pCube )
+        {
+            pFaninNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCube, vSupp );
+            Abc_ObjAddFanin( pNodeNew, pFaninNew );
+        }
+        pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes );
+    }
+/*
+    printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level );
+    Vec_IntForEachEntry( vSupp, Entry, i )
+    {
+        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
+        printf( "%d(%d) ", pFanin->pCopy->Id, pFanin->Id );
+    }
+    printf( "\n" );
+    Min_CoverWrite( stdout, pCover );
+*/
+    pObj->pCopy = pNodeNew;
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // perform strashing
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    // reconstruct the network
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        Abc_NtkXyzDeriveNode_rec( p, pNtkNew, Abc_ObjFanin0(pObj), 0 );
+//        printf( "*** CO %s : %d -> %d \n", Abc_ObjName(pObj), pObj->pCopy->Id, Abc_ObjFanin0(pObj)->pCopy->Id );
+    }
+    // add the COs
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkXyzDerive: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
+{
+    assert( pObj->pCopy );
+    if ( !fCompl )
+        return pObj->pCopy;
+    if ( pObj->pCopy->pCopy == NULL )
+        pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
+    return pObj->pCopy->pCopy;
+ }
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveCubeInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp )
+{
+    Vec_Int_t * vLits;
+    Abc_Obj_t * pNodeNew, * pFanin;
+    int i, iFanin, Lit;
+    // create empty cube
+    if ( pCube->nLits == 0 )
+        return Abc_NodeCreateConst1(pNtkNew);
+    // get the literals of this cube
+    vLits = Vec_IntAlloc( 10 );
+    Min_CubeGetLits( pCube, vLits );
+    assert( pCube->nLits == (unsigned)vLits->nSize );
+    // create special case when there is only one literal
+    if ( pCube->nLits == 1 )
+    {
+        iFanin = Vec_IntEntry(vLits,0);
+        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
+        Lit = Min_CubeGetVar(pCube, iFanin);
+        assert( Lit == 1 || Lit == 2 );
+        Vec_IntFree( vLits );
+//        if ( Lit == 1 )// negative
+//            return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy );
+//        return pFanin->pCopy;
+        return Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 );
+    }
+    assert( pCube->nLits > 1 );
+    // create the AND cube
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    for ( i = 0; i < vLits->nSize; i++ )
+    {
+        iFanin = Vec_IntEntry(vLits,i);
+        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
+        Lit = Min_CubeGetVar(pCube, iFanin);
+        assert( Lit == 1 || Lit == 2 );
+        Vec_IntWriteEntry( vLits, i, Lit==1 );
+//        Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
+        Abc_ObjAddFanin( pNodeNew, Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ) );
+    }
+//    pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
+    pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, NULL );
+    Vec_IntFree( vLits );
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveNodeInv_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
+{
+    Min_Cube_t * pCover, * pCube;
+    Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
+    Vec_Int_t * vSupp;
+    int Entry, nCubes, i;
+
+    // skip if already computed
+    if ( pObj->pCopy )
+        return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl );
+    assert( Abc_ObjIsNode(pObj) );
+
+    // get the support and the cover
+    vSupp  = Abc_ObjGetSupp( pObj ); 
+    pCover = Abc_ObjGetCover2( pObj );
+    assert( vSupp );
+
+    // process the fanins
+    Vec_IntForEachEntry( vSupp, Entry, i )
+    {
+        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
+        Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, pFanin, 0 );
+    }
+
+    // for each cube, construct the node
+    nCubes = Min_CoverCountCubes( pCover );
+    if ( nCubes == 0 )
+        pNodeNew = Abc_NodeCreateConst0(pNtkNew);
+    else if ( nCubes == 1 )
+        pNodeNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCover, vSupp );
+    else
+    {
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        Min_CoverForEachCube( pCover, pCube )
+        {
+            pFaninNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCube, vSupp );
+            Abc_ObjAddFanin( pNodeNew, pFaninNew );
+        }
+        pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes );
+    }
+
+    pObj->pCopy = pNodeNew;
+    return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description [The resulting network contains only pure AND/OR/EXOR gates
+  and inverters. This procedure is usedful to generate Verilog.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pNodeNew;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // perform strashing
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    // reconstruct the network
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pNodeNew = Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pNodeNew );
+    }
+    // add the COs
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkXyzDeriveInv: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
--- a/src/temp/xyz/xyzCore.c
+++ b/src/temp/xyz/xyzCore.c
--- a/src/temp/xyz/xyzInt.h
+++ b/src/temp/xyz/xyzInt.h
@ -0,0 +1,642 @@
+/**CFile****************************************************************
+
+  FileName    [xyzInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Min_Man_t_  Min_Man_t;
+typedef struct Min_Cube_t_ Min_Cube_t;
+
+struct Min_Man_t_
+{
+    int               nVars;          // the number of vars
+    int               nWords;         // the number of words
+    Extra_MmFixed_t * pMemMan;        // memory manager for cubes
+    // temporary cubes
+    Min_Cube_t *      pOne0;          // tautology cube
+    Min_Cube_t *      pOne1;          // tautology cube
+    Min_Cube_t *      pTriv0[2];      // trivial cube
+    Min_Cube_t *      pTriv1[2];      // trivial cube
+    Min_Cube_t *      pTemp;          // cube for computing the distance
+    Min_Cube_t *      pBubble;        // cube used as a separator
+    // temporary storage for the new cover
+    int               nCubes;         // the number of cubes
+    Min_Cube_t **     ppStore;        // storage for cubes by number of literals
+};
+
+struct Min_Cube_t_
+{
+    Min_Cube_t *      pNext;          // the pointer to the next cube in the cover
+    unsigned          nVars    : 10;  // the number of variables
+    unsigned          nWords   : 12;  // the number of machine words
+    unsigned          nLits    : 10;  // the number of literals in the cube
+    unsigned          uData[1];       // the bit-data for the cube
+};
+
+
+// iterators through the entries in the linked lists of cubes
+#define Min_CoverForEachCube( pCover, pCube )                   \
+    for ( pCube = pCover;                                       \
+          pCube;                                                \
+          pCube = pCube->pNext )
+#define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )       \
+    for ( pCube = pCover,                                       \
+          pCube2 = pCube? pCube->pNext: NULL;                   \
+          pCube;                                                \
+          pCube = pCube2,                                       \
+          pCube2 = pCube? pCube->pNext: NULL )
+#define Min_CoverForEachCubePrev( pCover, pCube, ppPrev )       \
+    for ( pCube = pCover,                                       \
+          ppPrev = &(pCover);                                   \
+          pCube;                                                \
+          ppPrev = &pCube->pNext,                               \
+          pCube = pCube->pNext )
+
+// macros to get hold of bits and values in the cubes
+static inline int  Min_CubeHasBit( Min_Cube_t * p, int i )              { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0;     }
+static inline void Min_CubeSetBit( Min_Cube_t * p, int i )              { p->uData[(i)>>5] |= (1<<((i) & 31));                 }
+static inline void Min_CubeXorBit( Min_Cube_t * p, int i )              { p->uData[(i)>>5] ^= (1<<((i) & 31));                 }
+static inline int  Min_CubeGetVar( Min_Cube_t * p, int Var )            { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); }
+static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31));     }
+
+/*=== xyzMinEsop.c ==========================================================*/
+extern void         Min_EsopMinimize( Min_Man_t * p );
+extern void         Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+/*=== xyzMinSop.c ==========================================================*/
+extern void         Min_SopMinimize( Min_Man_t * p );
+extern void         Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+/*=== xyzMinMan.c ==========================================================*/
+extern Min_Man_t *  Min_ManAlloc( int nVars );
+extern void         Min_ManClean( Min_Man_t * p, int nSupp );
+extern void         Min_ManFree( Min_Man_t * p );
+/*=== xyzMinUtil.c ==========================================================*/
+extern void         Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube );
+extern void         Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover );
+extern void         Min_CoverWriteStore( FILE * pFile, Min_Man_t * p );
+extern void         Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
+extern void         Min_CoverCheck( Min_Man_t * p );
+extern int          Min_CubeCheck( Min_Cube_t * pCube );
+extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize );
+extern void         Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover );
+extern int          Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p )
+{
+    Min_Cube_t * pCube;
+    pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan );
+    pCube->pNext  = NULL;
+    pCube->nVars  = p->nVars;
+    pCube->nWords = p->nWords;
+    pCube->nLits  = 0;
+    memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords );
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the cube representing elementary var.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl )
+{
+    Min_Cube_t * pCube;
+    pCube = Min_CubeAlloc( p );
+    Min_CubeXorBit( pCube, iVar*2+fCompl );
+    pCube->nLits = 1;
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy )
+{
+    Min_Cube_t * pCube;
+    pCube = Min_CubeAlloc( p );
+    memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
+    pCube->nLits = pCopy->nLits;
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the cube cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube, * pCube2;
+    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+        Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of cubes in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubeCountLits( Min_Cube_t * pCube )
+{
+    unsigned uData;
+    int Count = 0, i, w;
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+    {
+        uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
+        for ( i = 0; i < 32; i += 2 )
+            if ( uData & (1 << i) )
+                Count++;
+    }
+    return Count;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of cubes in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits )
+{
+    unsigned uData;
+    int i, w;
+    Vec_IntClear( vLits );
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+    {
+        uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
+        for ( i = 0; i < 32; i += 2 )
+            if ( uData & (1 << i) )
+                Vec_IntPush( vLits, w*16 + i/2 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of cubes in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CoverCountCubes( Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube;
+    int Count = 0;
+    Min_CoverForEachCube( pCover, pCube )
+        Count++;
+    return Count;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if two cubes are disjoint.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    unsigned uData;
+    int i;
+    assert( pCube0->nVars == pCube1->nVars );
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+    {
+        uData = pCube0->uData[i] & pCube1->uData[i];
+        uData = (uData | (uData >> 1)) & 0x55555555;
+        if ( uData != 0x55555555 )
+            return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the disjoint variables of the two cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars )
+{
+    unsigned uData;
+    int i, w;
+    Vec_IntClear( vVars );
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+    {
+        uData  = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555;
+        uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1));
+        if ( uData == 0 )
+            continue;
+        for ( i = 0; i < 32; i += 2 )
+            if ( uData & (1 << i) )
+                Vec_IntPush( vVars, w*16 + i/2 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if two cubes are disjoint.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp )
+{
+    unsigned uData;
+    int i, fFound = 0;
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+    {
+        uData = pCube0->uData[i] ^ pCube1->uData[i];
+        if ( uData == 0 )
+        {
+            if ( pTemp ) pTemp->uData[i] = 0;
+            continue;
+        }
+        if ( fFound )
+            return 0;
+        uData = (uData | (uData >> 1)) & 0x55555555;
+        if ( (uData & (uData-1)) > 0 ) // more than one 1
+            return 0;
+        if ( pTemp ) pTemp->uData[i] = uData | (uData << 1);
+        fFound = 1;
+    }
+    if ( fFound == 0 )
+    {
+        printf( "\n" );
+        Min_CubeWrite( stdout, pCube0 );
+        Min_CubeWrite( stdout, pCube1 );
+        printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if two cubes are disjoint.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 )
+{
+    unsigned uData;//, uData2;
+    int i, k, Var0 = -1, Var1 = -1;
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+    {
+        uData = pCube0->uData[i] ^ pCube1->uData[i];
+        if ( uData == 0 )
+            continue;
+        if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s
+            return 0;
+        uData = (uData | (uData >> 1)) & 0x55555555;
+        if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 )
+            return 0;
+        for ( k = 0; k < 32; k += 2 )
+            if ( uData & (1 << k) )
+            {
+                if ( Var0 == -1 )
+                    Var0 = 16 * i + k/2;
+                else if ( Var1 == -1 )
+                    Var1 = 16 * i + k/2;
+                else
+                    return 0;
+            }
+        /*
+        if ( Var0 >= 0 )
+        {
+            uData &= 0xFFFF;
+            uData2 = (uData >> 16);
+            if ( uData && uData2 )
+                return 0;
+            if ( uData )
+            {
+            }
+            uData }= uData2;
+            uData &= 0x
+        }
+        */
+    }
+    if ( Var0 >= 0 && Var1 >= 0 )
+    {
+        *pVar0 = Var0;
+        *pVar1 = Var1;
+        return 1;
+    }
+    if ( Var0 == -1 || Var1 == -1 )
+    {
+        printf( "\n" );
+        Min_CubeWrite( stdout, pCube0 );
+        Min_CubeWrite( stdout, pCube1 );
+        printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" );
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the produce of two cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    Min_Cube_t * pCube;
+    int i;
+    assert( pCube0->nVars == pCube1->nVars );
+    pCube = Min_CubeAlloc( p );
+    for ( i = 0; i < p->nWords; i++ )
+        pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i];
+    pCube->nLits = Min_CubeCountLits( pCube );
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the produce of two cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    Min_Cube_t * pCube;
+    int i;
+    assert( pCube0->nVars == pCube1->nVars );
+    pCube = Min_CubeAlloc( p );
+    for ( i = 0; i < p->nWords; i++ )
+        pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i];
+    pCube->nLits = Min_CubeCountLits( pCube );
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the produce of two cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    int i;
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+        if ( pCube0->uData[i] != pCube1->uData[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pCube1 is contained in pCube0, bitwise.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    int i;
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+        if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the cube into the result of merging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask )
+{
+    int w;
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+    {
+        pCube->uData[w]  =  pCube->uData[w] ^ pDist->uData[w];
+        pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the cube into the result of distance-1 merging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist )
+{
+    int w;
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+        pCube->uData[w] |= pDist->uData[w];
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube, * pCube2, * pThis;
+    if ( pCover == NULL )
+    {
+        Min_ManClean( p, p->nVars );
+        return;
+    }
+    Min_ManClean( p, pCover->nVars );
+    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+    {
+        // go through the linked list
+        Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+            if ( Min_CubesAreEqual( pCube, pThis ) )
+            {
+                Min_CubeRecycle( p, pCube );
+                break;
+            }
+        if ( pThis != NULL )
+            continue;
+        pCube->pNext = p->ppStore[pCube->nLits];
+        p->ppStore[pCube->nLits] = pCube;
+        p->nCubes++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the given cube is contained in one of the cubes of the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    Min_Cube_t * pThis;
+    int i;
+/*
+    // this cube cannot be equal to any cube
+    Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            Min_CubeWrite( stdout, pCube );
+            assert( 0 );
+        }
+    }
+*/
+    // try to find a containing cube
+    for ( i = 0; i <= (int)pCube->nLits; i++ )
+    Min_CoverForEachCube( p->ppStore[i], pThis )
+    {
+        // skip the bubble
+        if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+            return 1;
+    }
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
--- a/src/temp/xyz/xyzMan.c
+++ b/src/temp/xyz/xyzMan.c
@ -0,0 +1,144 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Decomposition manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyz.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax )
+{
+    Xyz_Man_t * pMan;
+    Xyz_Obj_t * pMem;
+    Abc_Obj_t * pObj;
+    int i;
+    assert( pNtk->pManCut == NULL );
+
+    // start the manager
+    pMan = ALLOC( Xyz_Man_t, 1 );
+    memset( pMan, 0, sizeof(Xyz_Man_t) );
+    pMan->nFaninMax = nFaninMax;
+    pMan->nCubesMax = 2 * pMan->nFaninMax;
+    pMan->nWords    = Abc_BitWordNum( nFaninMax * 2 );
+
+    // get the cubes
+    pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax );
+    pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax );
+    pMan->vPairs0 = Vec_IntAlloc( nFaninMax );
+    pMan->vPairs1 = Vec_IntAlloc( nFaninMax );
+    pMan->vTriv0  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv0, -1 ); 
+    pMan->vTriv1  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv1, -1 ); 
+
+    // allocate memory for object structures
+    pMan->pMemory = pMem = ALLOC( Xyz_Obj_t, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
+    memset( pMem, 0, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
+    // allocate storage for the pointers to the memory
+    pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) );
+    Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i );
+    // create the cube manager
+    pMan->pManMin = Min_ManAlloc( nFaninMax );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Xyz_ManFree( Xyz_Man_t * p )
+{
+    Vec_Int_t * vSupp;
+    int i;
+    for ( i = 0; i < p->vObjStrs->nSize; i++ )
+    {
+        vSupp = ((Xyz_Obj_t *)p->vObjStrs->pArray[i])->vSupp;
+        if ( vSupp ) Vec_IntFree( vSupp );
+    }
+
+    Min_ManFree( p->pManMin );
+    Vec_PtrFree( p->vObjStrs );
+    Vec_IntFree( p->vFanCounts );
+    Vec_IntFree( p->vTriv0 );
+    Vec_IntFree( p->vTriv1 );
+    Vec_IntFree( p->vComTo0 );
+    Vec_IntFree( p->vComTo1 );
+    Vec_IntFree( p->vPairs0 );
+    Vec_IntFree( p->vPairs1 );
+    free( p->pMemory );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Drop the covers at the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj )
+{
+    int nFanouts;
+    assert( p->vFanCounts );
+    nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id );
+    assert( nFanouts > 0 );
+    if ( --nFanouts == 0 )
+    {
+        Vec_IntFree( Abc_ObjGetSupp(pObj) );
+        Abc_ObjSetSupp( pObj, NULL );
+        Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) );
+        Abc_ObjSetCover2( pObj, NULL );
+        p->nSupps--;
+    }
+    Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
--- a/src/temp/xyz/xyzMinEsop.c
+++ b/src/temp/xyz/xyzMinEsop.c
@ -0,0 +1,299 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMinEsop.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [ESOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Min_EsopRewrite( Min_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopMinimize( Min_Man_t * p )
+{
+    int nCubesInit, nCubesOld, nIter;
+    if ( p->nCubes < 3 )
+        return;
+    nIter = 0;
+    nCubesInit = p->nCubes;
+    do {
+        nCubesOld = p->nCubes;
+        Min_EsopRewrite( p );
+        nIter++;
+    }
+    while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+
+//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of rewriting using distance 2 cubes.]
+
+  Description [The weakness of this procedure is that it tries each cube
+  with only one distance-2 cube. If this pair does not lead to improvement
+  the cube is inserted into the cover anyhow, and we try another pair.
+  A possible improvement would be to try this cube with all distance-2
+  cubes, until an improvement is found, or until all such cubes are tried.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopRewrite( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, ** ppPrev;
+    Min_Cube_t * pThis, ** ppPrevT;
+    int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
+    int nPairs = 0;
+
+    // insert the bubble before the first cube
+    p->pBubble->pNext = p->ppStore[0];
+    p->ppStore[0] = p->pBubble;
+    p->pBubble->nLits = 0;
+
+    // go through the cubes
+    while ( 1 )
+    {
+        // get the index of the bubble
+        Index = p->pBubble->nLits;
+
+        // find the bubble
+        Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
+            if ( pCube == p->pBubble )
+                break;
+        assert( pCube == p->pBubble );
+
+        // remove the bubble, get the next cube after the bubble
+        *ppPrev = p->pBubble->pNext;
+        pCube = p->pBubble->pNext;
+        if ( pCube == NULL )
+            for ( Index++; Index <= p->nVars; Index++ )
+                if ( p->ppStore[Index] )
+                {
+                    ppPrev = &(p->ppStore[Index]);
+                    pCube = p->ppStore[Index];
+                    break;
+                }
+        // stop if there is no more cubes
+        if ( pCube == NULL )
+            break;
+
+        // find the first dist2 cube
+        Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars )
+        Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars - 1 )
+        Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        // continue if there is no dist2 cube
+        if ( pThis == NULL )
+        {
+            // insert the bubble after the cube
+            p->pBubble->pNext = pCube->pNext;
+            pCube->pNext = p->pBubble;
+            p->pBubble->nLits = pCube->nLits;
+            continue;
+        }
+        nPairs++;
+
+        // remove the cubes, insert the bubble instead of pCube
+        *ppPrevT = pThis->pNext;
+        *ppPrev = p->pBubble;
+        p->pBubble->pNext = pCube->pNext;
+        p->pBubble->nLits = pCube->nLits;
+        p->nCubes -= 2;
+
+        // Exorlink-2:
+        // A{v00}     B{v01}      +  A{v10}     B{v11}     =
+        // A{v00+v10} B{v01}      +  A{v10}     B{v01+v11} =
+        // A{v00}     B{v01+v11}  +  A{v00+v10} B{v11}
+
+        // save the dist2 parameters
+        v00 = Min_CubeGetVar( pCube, Var0 );
+        v01 = Min_CubeGetVar( pCube, Var1 );
+        v10 = Min_CubeGetVar( pThis, Var0 );
+        v11 = Min_CubeGetVar( pThis, Var1 );
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+        // derive the first pair of resulting cubes
+        Min_CubeXorVar( pCube, Var0, v10 );
+        pCube->nLits -= (v00 != 3);
+        pCube->nLits += ((v00 ^ v10) != 3);
+        Min_CubeXorVar( pThis, Var1, v01 );
+        pThis->nLits -= (v11 != 3);
+        pThis->nLits += ((v01 ^ v11) != 3);
+
+        // add the cubes
+        nCubesOld = p->nCubes;
+        Min_EsopAddCube( p, pCube );
+        Min_EsopAddCube( p, pThis );
+        // check if the cubes were absorbed
+        if ( p->nCubes < nCubesOld + 2 )
+            continue;
+
+        // pull out both cubes
+        assert( pThis == p->ppStore[pThis->nLits] );
+        p->ppStore[pThis->nLits] = pThis->pNext;
+        assert( pCube == p->ppStore[pCube->nLits] );
+        p->ppStore[pCube->nLits] = pCube->pNext;
+        p->nCubes -= 2;
+
+        // derive the second pair of resulting cubes
+        Min_CubeXorVar( pCube, Var0, v10 );
+        pCube->nLits -= ((v00 ^ v10) != 3);
+        pCube->nLits += (v00 != 3);
+        Min_CubeXorVar( pCube, Var1, v11 );
+        pCube->nLits -= (v01 != 3);
+        pCube->nLits += ((v01 ^ v11) != 3);
+
+        Min_CubeXorVar( pThis, Var0, v00 );
+        pThis->nLits -= (v10 != 3);
+        pThis->nLits += ((v00 ^ v10) != 3);
+        Min_CubeXorVar( pThis, Var1, v01 );
+        pThis->nLits -= ((v01 ^ v11) != 3);
+        pThis->nLits += (v11 != 3);
+
+        // add them anyhow
+        Min_EsopAddCube( p, pCube );
+        Min_EsopAddCube( p, pThis );
+    }
+//    printf( "Pairs = %d  ", nPairs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description [Returns 0 if the cube is added or removed. Returns 1
+  if the cube is glued with some other cube and has to be added again.
+  Do not forget to clean the storage!]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    Min_Cube_t * pThis, ** ppPrev;
+    // try to find the identical cube
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubeRecycle( p, pCube );
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 0;
+        }
+    }
+    // find a distance-1 cube if it exists
+    if ( pCube->nLits < pCube->nVars )
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransform( pCube, pThis, p->pTemp );
+            pCube->nLits++;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransform( pCube, pThis, p->pTemp );
+            pCube->nLits--;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    if ( pCube->nLits > 0 )
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransform( pCube, pThis, p->pTemp );
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    // add the cube
+    pCube->pNext = p->ppStore[pCube->nLits];
+    p->ppStore[pCube->nLits] = pCube;
+    p->nCubes++;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    assert( pCube != p->pBubble );
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    while ( Min_EsopAddCubeInt( p, pCube ) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
--- a/src/temp/xyz/xyzMinMan.c
+++ b/src/temp/xyz/xyzMinMan.c
@ -0,0 +1,113 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMinMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [SOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMinMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Man_t * Min_ManAlloc( int nVars )
+{
+    Min_Man_t * pMan;
+    // start the manager
+    pMan = ALLOC( Min_Man_t, 1 );
+    memset( pMan, 0, sizeof(Min_Man_t) );
+    pMan->nVars   = nVars;
+    pMan->nWords  = Abc_BitWordNum( nVars * 2 );
+    pMan->pMemMan = Extra_MmFixedStart( sizeof(Min_Cube_t) + sizeof(unsigned) * (pMan->nWords - 1) );
+    // allocate storage for the temporary cover
+    pMan->ppStore = ALLOC( Min_Cube_t *, pMan->nVars + 1 );
+    // create tautology cubes
+    Min_ManClean( pMan, nVars );
+    pMan->pOne0  = Min_CubeAlloc( pMan );
+    pMan->pOne1  = Min_CubeAlloc( pMan );
+    pMan->pTemp  = Min_CubeAlloc( pMan );
+    pMan->pBubble = Min_CubeAlloc( pMan );  pMan->pBubble->uData[0] = 0;
+    // create trivial cubes
+    Min_ManClean( pMan, 1 );
+    pMan->pTriv0[0] = Min_CubeAllocVar( pMan, 0, 0 );
+    pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 );   
+    pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 );
+    pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 );   
+    Min_ManClean( pMan, nVars );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_ManClean( Min_Man_t * p, int nSupp )
+{
+    // set the size of the cube manager
+    p->nVars  = nSupp;
+    p->nWords = Abc_BitWordNum(2*nSupp);
+    // clean the storage
+    memset( p->ppStore, 0, sizeof(Min_Cube_t *) * (nSupp + 1) );
+    p->nCubes = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_ManFree( Min_Man_t * p )
+{
+    Extra_MmFixedStop ( p->pMemMan, 0 );
+    free( p->ppStore );
+    free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
--- a/src/temp/xyz/xyzMinSop.c
+++ b/src/temp/xyz/xyzMinSop.c
@ -0,0 +1,615 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMinSop.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [SOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Min_SopRewrite( Min_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopMinimize( Min_Man_t * p )
+{
+    int nCubesInit, nCubesOld, nIter;
+    if ( p->nCubes < 3 )
+        return;
+    nIter = 0;
+    nCubesInit = p->nCubes;
+    do {
+        nCubesOld = p->nCubes;
+        Min_SopRewrite( p );
+        nIter++;
+//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
+    }
+    while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+//    printf( "\n" );
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopRewrite( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, ** ppPrev;
+    Min_Cube_t * pThis, ** ppPrevT;
+    Min_Cube_t * pTemp;
+    int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld;
+    int nPairs = 0;
+/*    
+    {
+        Min_Cube_t * pCover;
+        pCover = Min_CoverCollect( p, p->nVars );
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCover );
+        Min_CoverExpand( p, pCover );
+    }
+*/
+
+    // insert the bubble before the first cube
+    p->pBubble->pNext = p->ppStore[0];
+    p->ppStore[0] = p->pBubble;
+    p->pBubble->nLits = 0;
+
+    // go through the cubes
+    while ( 1 )
+    {
+        // get the index of the bubble
+        Index = p->pBubble->nLits;
+
+        // find the bubble
+        Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
+            if ( pCube == p->pBubble )
+                break;
+        assert( pCube == p->pBubble );
+
+        // remove the bubble, get the next cube after the bubble
+        *ppPrev = p->pBubble->pNext;
+        pCube = p->pBubble->pNext;
+        if ( pCube == NULL )
+            for ( Index++; Index <= p->nVars; Index++ )
+                if ( p->ppStore[Index] )
+                {
+                    ppPrev = &(p->ppStore[Index]);
+                    pCube = p->ppStore[Index];
+                    break;
+                }
+        // stop if there is no more cubes
+        if ( pCube == NULL )
+            break;
+
+        // find the first dist2 cube
+        Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars )
+        Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        // continue if there is no dist2 cube
+        if ( pThis == NULL )
+        {
+            // insert the bubble after the cube
+            p->pBubble->pNext = pCube->pNext;
+            pCube->pNext = p->pBubble;
+            p->pBubble->nLits = pCube->nLits;
+            continue;
+        }
+        nPairs++;
+/*
+printf( "\n" );
+Min_CubeWrite( stdout, pCube );
+Min_CubeWrite( stdout, pThis );
+*/
+        // remove the cubes, insert the bubble instead of pCube
+        *ppPrevT = pThis->pNext;
+        *ppPrev = p->pBubble;
+        p->pBubble->pNext = pCube->pNext;
+        p->pBubble->nLits = pCube->nLits;
+        p->nCubes -= 2;
+
+        assert( pCube != p->pBubble && pThis != p->pBubble );
+
+
+        // save the dist2 parameters
+        v00 = Min_CubeGetVar( pCube, Var0 );
+        v01 = Min_CubeGetVar( pCube, Var1 );
+        v10 = Min_CubeGetVar( pThis, Var0 );
+        v11 = Min_CubeGetVar( pThis, Var1 );
+        assert( v00 != v10 && v01 != v11 );
+        assert( v00 != 3   || v01 != 3 );
+        assert( v10 != 3   || v11 != 3 );
+
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+        // consider the case when both cubes have non-empty literals
+        if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
+        {
+            assert( v00 == (v10 ^ 3) );
+            assert( v01 == (v11 ^ 3) );
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, 3 );
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pCube );
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, 3 );
+            Min_CubeXorVar( pCube, Var1, 3 );
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+            // check if this cube is contained
+            fCont1 = Min_CoverContainsCube( p, pCube );
+            // undo the change
+            Min_CubeXorVar( pCube, Var1, 3 );
+
+            // check if the cubes can be overwritten
+            if ( fCont0 && fCont1 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits -= 2;
+                Min_SopAddCube( p, pCube );
+            }
+            else if ( fCont0 )
+            {
+                // expand both cubes and add them
+                Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+                Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+                pThis->nLits--;
+                Min_SopAddCube( p, pThis );
+            }
+            else if ( fCont1 )
+            {
+                // expand both cubes and add them
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+                Min_CubeXorVar( pThis, Var0, v10 ^ 3 );
+                pThis->nLits--;
+                Min_SopAddCube( p, pThis );
+            }
+            else
+            {
+                Min_SopAddCube( p, pCube );
+                Min_SopAddCube( p, pThis );
+            }
+            // otherwise, no change is possible
+            continue;
+        }
+
+        // if one of them does not have DC lit, move it
+        if ( v00 != 3 && v01 != 3 )
+        {
+            assert( v10 == 3 || v11 == 3 );
+            pTemp = pCube; pCube = pThis; pThis = pTemp;
+            Index = v00; v00 = v10; v10 = Index;
+            Index = v01; v01 = v11; v11 = Index;
+        }
+
+        // make sure the first cube has first var DC
+        if ( v00 != 3 )
+        {
+            assert( v01 == 3 );
+            Index = Var0; Var0 = Var1; Var1 = Index;
+            Index = v00; v00 = v01; v01 = Index;
+            Index = v10; v10 = v11; v11 = Index;
+        }
+
+        // consider both cases: both have DC lit
+        if ( v00 == 3 && v11 == 3 )
+        {
+            assert( v01 != 3 && v10 != 3 );
+            // try the remaining minterm
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, v10 );
+            Min_CubeXorVar( pCube, Var1, 3   );
+            pCube->nLits++;
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pCube );
+            // undo the cube transformations
+            Min_CubeXorVar( pCube, Var0, v10 );
+            Min_CubeXorVar( pCube, Var1, 3   );
+            pCube->nLits--;
+            // check the case when both are covered
+            if ( fCont0 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+            }
+            else
+            {
+                // try two reduced cubes
+                Min_CubeXorVar( pCube, Var0, v10 );
+                pCube->nLits++;
+                // remember the cubes
+                nCubesOld = p->nCubes;
+                Min_SopAddCube( p, pCube );
+                // check if the cube is absorbed
+                if ( p->nCubes < nCubesOld + 1 )
+                { // absorbed - add the second cube
+                    Min_SopAddCube( p, pThis );
+                }
+                else
+                { // remove this cube, and try another one
+                    assert( pCube == p->ppStore[pCube->nLits] );
+                    p->ppStore[pCube->nLits] = pCube->pNext;
+                    p->nCubes--;
+
+                    // return the cube to the previous state
+                    Min_CubeXorVar( pCube, Var0, v10 );
+                    pCube->nLits--;
+
+                    // generate another reduced cube
+                    Min_CubeXorVar( pThis, Var1, v01 );
+                    pThis->nLits++;
+
+                    // add both cubes
+                    Min_SopAddCube( p, pCube );
+                    Min_SopAddCube( p, pThis );
+                }
+            }
+        }
+        else // the first cube has DC lit
+        {
+            assert( v01 != 3 && v10 != 3 && v11 != 3 );
+            // try the remaining minterm
+            // create the temporary cube equal to the minterm
+            Min_CubeXorVar( pThis, Var0, 3 );
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pThis );
+            // undo the cube transformations
+            Min_CubeXorVar( pThis, Var0, 3 );
+            // check the case when both are covered
+            if ( fCont0 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+            }
+            else
+            {
+                // try reshaping the cubes
+                // reduce the first cube
+                Min_CubeXorVar( pCube, Var0, v10 );
+                pCube->nLits++;
+                // expand the second cube
+                Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+                pThis->nLits--;
+                // add both cubes
+                Min_SopAddCube( p, pCube );
+                Min_SopAddCube( p, pThis );
+            }
+        }
+    }
+//    printf( "Pairs = %d  ", nPairs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds cube to the SOP cover stored in the manager.]
+
+  Description [Returns 0 if the cube is added or removed. Returns 1
+  if the cube is glued with some other cube and has to be added again.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    Min_Cube_t * pThis, * pThis2, ** ppPrev;
+    int i;
+    // try to find the identical cube
+    Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            Min_CubeRecycle( p, pCube );
+            return 0;
+        }
+    }
+    // try to find a containing cube
+    for ( i = 0; i < (int)pCube->nLits; i++ )
+    Min_CoverForEachCube( p->ppStore[i], pThis )
+    {
+        if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+        {
+            Min_CubeRecycle( p, pCube );
+            return 0;
+        }
+    }
+    // try to find distance one in the same bin
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, NULL ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransformOr( pCube, pThis );
+            pCube->nLits--;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+
+    // clean the other cubes using this one
+    for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ )
+    {
+        ppPrev = &p->ppStore[i];
+        Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 )
+        {
+            if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) )
+            {
+                *ppPrev = pThis->pNext;
+                Min_CubeRecycle( p, pThis );
+                p->nCubes--;
+            }
+            else
+                ppPrev = &pThis->pNext;
+        }
+    }
+
+    // add the cube
+    pCube->pNext = p->ppStore[pCube->nLits];
+    p->ppStore[pCube->nLits] = pCube;
+    p->nCubes++;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    assert( Min_CubeCheck( pCube ) );
+    assert( pCube != p->pBubble );
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    while ( Min_SopAddCubeInt( p, pCube ) );
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopContain( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pCube2, ** ppPrev;
+    int i, k;
+    for ( i = 0; i <= p->nVars; i++ )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev )
+        {
+            if ( !Min_CubesAreEqual( pCube, pCube2 ) )
+                continue;
+            *ppPrev = pCube2->pNext;
+            Min_CubeRecycle( p, pCube2 );
+            p->nCubes--;
+        }
+        for ( k = i + 1; k <= p->nVars; k++ )
+        Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev )
+        {
+            if ( !Min_CubeIsContained( pCube, pCube2 ) )
+                continue;
+            *ppPrev = pCube2->pNext;
+            Min_CubeRecycle( p, pCube2 );
+            p->nCubes--;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopDist1Merge( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pCube2, * pCubeNew;
+    int i;
+    for ( i = p->nVars; i >= 0; i-- )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        Min_CoverForEachCube( pCube->pNext, pCube2 )
+        {
+            assert( pCube->nLits == pCube2->nLits );
+            if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
+                continue;
+            pCubeNew = Min_CubesXor( p, pCube, pCube2 );
+            assert( pCubeNew->nLits == pCube->nLits - 1 );
+            pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
+            p->ppStore[pCubeNew->nLits] = pCubeNew;
+            p->nCubes++;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
+{
+     Vec_Int_t * vVars;
+     Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev;
+     int Num, Value, i;
+
+     // get the variables
+     vVars = Vec_IntAlloc( 100 );
+    // create the tautology cube
+     pCover = Min_CubeAlloc( p );
+     // sharp it with all cubes
+     Min_CoverForEachCube( pSharp, pCube )
+     Min_CoverForEachCubePrev( pCover, pThis, ppPrev )
+     {
+        if ( Min_CubesDisjoint( pThis, pCube ) )
+            continue;
+        // remember the next pointer
+        pNext = pThis->pNext;
+        // get the variables, in which pThis is '-' while pCube is fixed
+        Min_CoverGetDisjVars( pThis, pCube, vVars );
+        // generate the disjoint cubes
+        pReady = pThis;
+        Vec_IntForEachEntryReverse( vVars, Num, i )
+        {
+            // correct the literal
+            Min_CubeXorVar( pReady, vVars->pArray[i], 3 );
+            if ( i == 0 )
+                break;
+            // create the new cube and clean this value
+            Value = Min_CubeGetVar( pReady, vVars->pArray[i] );
+            pReady = Min_CubeDup( p, pReady );
+            Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value );
+            // add to the cover
+            *ppPrev = pReady;
+            ppPrev = &pReady->pNext;
+        }
+        pThis = pReady;
+        pThis->pNext = pNext;
+     }
+     Vec_IntFree( vVars );
+
+     // perform dist-1 merge and contain
+     Min_CoverExpandRemoveEqual( p, pCover );
+     Min_SopDist1Merge( p );
+     Min_SopContain( p );
+     return Min_CoverCollect( p, p->nVars );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_SopCheck( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pThis;
+    int i;
+
+    pCube = Min_CubeAlloc( p );
+    Min_CubeXorBit( pCube, 2*0+1 );
+    Min_CubeXorBit( pCube, 2*1+1 );
+    Min_CubeXorBit( pCube, 2*2+0 );
+    Min_CubeXorBit( pCube, 2*3+0 );
+    Min_CubeXorBit( pCube, 2*4+0 );
+    Min_CubeXorBit( pCube, 2*5+1 );
+    Min_CubeXorBit( pCube, 2*6+1 );
+    pCube->nLits = 7;
+
+//    Min_CubeWrite( stdout, pCube );
+
+    // check that the cubes contain it
+    for ( i = 0; i <= p->nVars; i++ )
+        Min_CoverForEachCube( p->ppStore[i], pThis )
+            if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+            {
+                Min_CubeRecycle( p, pCube );
+                return 1;
+            }
+    Min_CubeRecycle( p, pCube );
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
--- a/src/temp/xyz/xyzMinUtil.c
+++ b/src/temp/xyz/xyzMinUtil.c
@ -0,0 +1,277 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMinUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMinUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube )
+{
+    int i;
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Min_CubeHasBit(pCube, i*2) )
+        {
+            if ( Min_CubeHasBit(pCube, i*2+1) )
+                fprintf( pFile, "-" );
+            else
+                fprintf( pFile, "0" );
+        }
+        else
+        {
+            if ( Min_CubeHasBit(pCube, i*2+1) )
+                fprintf( pFile, "1" );
+            else
+                fprintf( pFile, "?" );
+        }
+    fprintf( pFile, " 1\n" );
+//    fprintf( pFile, " %d\n", pCube->nLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube;
+    Min_CoverForEachCube( pCover, pCube )
+        Min_CubeWrite( pFile, pCube );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p )
+{
+    Min_Cube_t * pCube;
+    int i;
+    for ( i = 0; i <= p->nVars; i++ )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        {
+            printf( "%2d : ", i );
+            if ( pCube == p->pBubble )
+            {
+                printf( "Bubble\n" );
+                continue;
+            }
+            Min_CubeWrite( pFile, pCube );
+        }
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
+{
+    char Buffer[1000];
+    Min_Cube_t * pCube;
+    FILE * pFile;
+    int i;
+    sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
+    for ( i = strlen(Buffer) - 1; i >= 0; i-- )
+        if ( Buffer[i] == '<' || Buffer[i] == '>' )
+            Buffer[i] = '_';
+    pFile = fopen( Buffer, "w" );
+    fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() );
+    fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 );
+    fprintf( pFile, ".o %d\n", 1 );
+    fprintf( pFile, ".p %d\n", Min_CoverCountCubes(pCover) );
+    if ( fEsop ) fprintf( pFile, ".type esop\n" );
+    Min_CoverForEachCube( pCover, pCube )
+        Min_CubeWrite( pFile, pCube );
+    fprintf( pFile, ".e\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverCheck( Min_Man_t * p )
+{
+    Min_Cube_t * pCube;
+    int i;
+    for ( i = 0; i <= p->nVars; i++ )
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+            assert( i == (int)pCube->nLits );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_CubeCheck( Min_Cube_t * pCube )
+{
+    int i;
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Min_CubeGetVar( pCube, i ) == 0 )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the cover from the sorted structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
+{
+    Min_Cube_t * pCov = NULL, ** ppTail = &pCov;
+    Min_Cube_t * pCube, * pCube2;
+    int i;
+    for ( i = 0; i <= nSuppSize; i++ )
+    {
+        Min_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 )
+        {
+            assert( i == (int)pCube->nLits );
+            *ppTail = pCube; 
+            ppTail = &pCube->pNext;
+            assert( pCube->uData[0] ); // not a bubble
+        }
+    }
+    *ppTail = NULL;
+    return pCov;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube, * pCube2;
+    Min_ManClean( p, p->nVars );
+    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+    {
+        pCube->pNext = p->ppStore[pCube->nLits];
+        p->ppStore[pCube->nLits] = pCube;
+        p->nCubes++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube;
+    int i, Counter;
+    if ( pCover == NULL )
+        return 0;
+    // clean the cube
+    for ( i = 0; i < (int)pCover->nWords; i++ )
+        p->pTemp->uData[i]  = ~((unsigned)0);
+    // add the bit data
+    Min_CoverForEachCube( pCover, pCube )
+        for ( i = 0; i < (int)pCover->nWords; i++ )
+            p->pTemp->uData[i] &= pCube->uData[i];
+    // count the vars
+    Counter = 0;
+    for ( i = 0; i < (int)pCover->nVars; i++ )
+        Counter += ( Min_CubeGetVar(p->pTemp, i) != 3 );
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
--- a/src/temp/xyz/xyzTest.c
+++ b/src/temp/xyz/xyzTest.c
@ -0,0 +1,417 @@
+/**CFile****************************************************************
+
+  FileName    [xyzTest.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Testing procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyz.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeDeriveCoverPro( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
+{
+    Min_Cube_t * pCover;
+    Min_Cube_t * pCube0, * pCube1, * pCube;
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return NULL;
+    // clean storage
+    Min_ManClean( p, p->nVars );
+    // go through the cube pairs
+    Min_CoverForEachCube( pCover0, pCube0 )
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        if ( Min_CubesDisjoint( pCube0, pCube1 ) )
+            continue;
+        pCube = Min_CubesProduct( p, pCube0, pCube1 );
+        // add the cube to storage
+        Min_SopAddCube( p, pCube );
+    }
+    Min_SopMinimize( p );
+    pCover = Min_CoverCollect( p, p->nVars );
+    assert( p->nCubes == Min_CoverCountCubes(pCover) );
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeDeriveCoverSum( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
+{
+    Min_Cube_t * pCover;
+    Min_Cube_t * pThis, * pCube;
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return NULL;
+    // clean storage
+    Min_ManClean( p, p->nVars );
+    // add the cubes to storage
+    Min_CoverForEachCube( pCover0, pThis )
+    {
+        pCube = Min_CubeDup( p, pThis );
+        Min_SopAddCube( p, pCube );
+    }
+    Min_CoverForEachCube( pCover1, pThis )
+    {
+        pCube = Min_CubeDup( p, pThis );
+        Min_SopAddCube( p, pCube );
+    }
+    Min_SopMinimize( p );
+    pCover = Min_CoverCollect( p, p->nVars );
+    assert( p->nCubes == Min_CoverCountCubes(pCover) );
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeDeriveSops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
+{
+    Min_Cube_t * pCov0[2], * pCov1[2];
+    Min_Cube_t * pCoverP, * pCoverN;
+    Abc_Obj_t * pObj;
+    int i, nCubes, fCompl0, fCompl1;
+
+    // set elementary vars
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+    {
+        pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
+        pObj->pNext = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 1 );
+    }
+
+    // get the cover for each node in the array
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // get the complements
+        fCompl0 = Abc_ObjFaninC0(pObj);
+        fCompl1 = Abc_ObjFaninC1(pObj);
+        // get the covers
+        pCov0[0] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy;
+        pCov0[1] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pNext;
+        pCov1[0] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy;
+        pCov1[1] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pNext;
+        // compute the covers
+        pCoverP = Abc_NodeDeriveCoverPro( p, pCov0[ fCompl0], pCov1[ fCompl1] );
+        pCoverN = Abc_NodeDeriveCoverSum( p, pCov0[!fCompl0], pCov1[!fCompl1] );
+        // set the covers
+        pObj->pCopy = (Abc_Obj_t *)pCoverP;
+        pObj->pNext = (Abc_Obj_t *)pCoverN;
+    }
+
+     nCubes = ABC_MIN( Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverP) );
+
+/*
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCoverP );
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCoverN );
+*/
+
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+
+//    Min_CoverExpand( p, pCoverP );
+//    Min_SopMinimize( p );
+//    pCoverP = Min_CoverCollect( p, p->nVars );
+
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+
+//    nCubes = Min_CoverCountCubes(pCoverP);
+
+    // clean the copy fields
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = pObj->pNext = NULL;
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = pObj->pNext = NULL;
+
+//    Min_CoverWriteFile( pCoverP, Abc_ObjName(pRoot), 0 );
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverN );
+    return nCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkTestSop( Abc_Ntk_t * pNtk )
+{
+    Min_Man_t * p;
+    Vec_Ptr_t * vSupp, * vNodes;
+    Abc_Obj_t * pObj;
+    int i, nCubes;
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    Abc_NtkCleanCopy(pNtk);
+    Abc_NtkCleanNext(pNtk);
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
+        {
+            printf( "%-20s :  Trivial.\n", Abc_ObjName(pObj) );
+            continue;
+        }
+
+        vSupp  = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+
+        printf( "%20s :  Cone = %5d.  Supp = %5d.  ", 
+            Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+//        if ( vSupp->nSize <= 128 )
+        {
+            p = Min_ManAlloc( vSupp->nSize );
+            nCubes = Abc_NodeDeriveSops( p, pObj, vSupp, vNodes );
+            printf( "Cubes = %5d.  ", nCubes );
+            Min_ManFree( p );
+        }
+        printf( "\n" );
+
+
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeDeriveCover( Min_Man_t * p, Min_Cube_t * pCov0, Min_Cube_t * pCov1, int fComp0, int fComp1 )
+{
+    Min_Cube_t * pCover0, * pCover1, * pCover;
+    Min_Cube_t * pCube0, * pCube1, * pCube;
+
+    // complement the first if needed
+    if ( !fComp0 )
+        pCover0 = pCov0;
+    else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
+        pCover0 = pCov0->pNext;
+    else
+        pCover0 = p->pOne0, p->pOne0->pNext = pCov0;
+
+    // complement the second if needed
+    if ( !fComp1 )
+        pCover1 = pCov1;
+    else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
+        pCover1 = pCov1->pNext;
+    else
+        pCover1 = p->pOne1, p->pOne1->pNext = pCov1;
+
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return NULL;
+
+    // clean storage
+    Min_ManClean( p, p->nVars );
+    // go through the cube pairs
+    Min_CoverForEachCube( pCover0, pCube0 )
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        if ( Min_CubesDisjoint( pCube0, pCube1 ) )
+            continue;
+        pCube = Min_CubesProduct( p, pCube0, pCube1 );
+        // add the cube to storage
+        Min_EsopAddCube( p, pCube );
+    }
+ 
+    if ( p->nCubes > 10 )
+    {
+//        printf( "(%d,", p->nCubes );
+        Min_EsopMinimize( p );
+//        printf( "%d) ", p->nCubes );
+    }
+
+    pCover = Min_CoverCollect( p, p->nVars );
+    assert( p->nCubes == Min_CoverCountCubes(pCover) );
+
+//    if ( p->nCubes > 1000 )
+//        printf( "%d ", p->nCubes );
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeDeriveEsops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
+{
+    Min_Cube_t * pCover, * pCube;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // set elementary vars
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
+
+    // get the cover for each node in the array
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        pCover = Abc_NodeDeriveCover( p,  
+            (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy,  
+            (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy,
+            Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        pObj->pCopy = (Abc_Obj_t *)pCover;
+        if ( p->nCubes > 3000 )
+            return -1;
+    }
+
+    // add complement if needed
+    if ( Abc_ObjFaninC0(pRoot) )
+    {
+        if ( pCover && pCover->nLits == 0 ) // topmost one is the tautology cube
+        {
+            pCube = pCover;
+            pCover = pCover->pNext;
+            Min_CubeRecycle( p, pCube );
+            p->nCubes--;
+        }
+        else
+        {
+            pCube = Min_CubeAlloc( p );
+            pCube->pNext = pCover;
+            p->nCubes++;
+        }
+    }
+/*
+    Min_CoverExpand( p, pCover );
+    Min_EsopMinimize( p );
+    pCover = Min_CoverCollect( p, p->nVars );
+*/
+    // clean the copy fields
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = NULL;
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = NULL;
+
+//    Min_CoverWriteFile( pCover, Abc_ObjName(pRoot), 1 );
+//    Min_CoverWrite( stdout, pCover );
+    return p->nCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkTestEsop( Abc_Ntk_t * pNtk )
+{
+    Min_Man_t * p;
+    Vec_Ptr_t * vSupp, * vNodes;
+    Abc_Obj_t * pObj;
+    int i, nCubes;
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    Abc_NtkCleanCopy(pNtk);
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
+        {
+            printf( "%-20s :  Trivial.\n", Abc_ObjName(pObj) );
+            continue;
+        }
+
+        vSupp  = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+
+        printf( "%20s :  Cone = %5d.  Supp = %5d.  ", 
+            Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+//        if ( vSupp->nSize <= 128 )
+        {
+            p = Min_ManAlloc( vSupp->nSize );
+            nCubes = Abc_NodeDeriveEsops( p, pObj, vSupp, vNodes );
+            printf( "Cubes = %5d.  ", nCubes );
+            Min_ManFree( p );
+        }
+        printf( "\n" );
+
+
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+