Version abc50905

2005-09-05 08:01:00 -07:00 · 2005-09-05 08:01:00 -07:00 · 1260d20cc0
parent 33012d9530
commit 1260d20cc0
84 changed files with 172612 additions and 1899 deletions
--- a/abc.dsp
+++ b/abc.dsp
@ -1158,6 +1158,10 @@ SOURCE=.\src\opt\sim\simSym.c
 # End Source File
 # Begin Source File

+SOURCE=.\src\opt\sim\simSymSat.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\sim\simSymSim.c
 # End Source File
 # Begin Source File
--- a/abc.opt
+++ b/abc.opt
--- a/abc.plg
+++ b/abc.plg
--- a/abc.rc
+++ b/abc.rc
@ -1,3 +1,21 @@
+# global parameters
+#set check         # checks intermediate networks
+#set checkfio      # prints warnings when fanins/fanouts are duplicated
+set checkread     # checks new networks after reading from file
+set backup        # saves backup networks retrived by "undo" and "recall"
+set savesteps 1   # sets the maximum number of backup networks to save
+
+# program names for internal calls
+set dotwin dot.exe
+set dotunix dot
+set gsviewwin gsview32.exe
+set gsviewunix gv
+set siswin sis.exe
+set sisunix sis
+set mvsiswin mvsis.exe
+set mvsisunix mvsis
+
+# standard aliases
 alias b balance
 alias cl cleanup
 alias clp collapse
@ -30,16 +48,18 @@ alias sa set autoexec ps
 alias so source -x
 alias st strash
 alias sw sweep
-alias t "r dalu.blif; st; psu"
 alias u undo
 alias wb write_blif
 alias wl write_blif
 alias wp write_pla
-alias cnf      "st; renode -c; write_cnf"
-alias prove    "st; renode -c; sat"
-alias opt      "b; renode; b"
-alias share    "b; renode; fx; b"
-alias sharem   "b; renode -m; fx; b"
-alias sharedsd "b; renode; dsd -g; sw; fx; b"
-alias resyn    "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
+
+# standard scripts
+alias cnf      "st; ren -c; write_cnf"
+alias prove    "st; ren -c; sat"
+alias opt      "b; ren; b"
+alias share    "b; ren; fx; b"
+alias sharem   "b; ren -m; fx; b"
+alias sharedsd "b; ren; dsd -g; sw; fx; b"
+alias resyn    "b; rw; rwz; b; rwz; b"
+alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"

--- a/examples/C2670.blif
+++ b/examples/C2670.blif
--- a/examples/ac.v
+++ b/examples/ac.v
--- a/examples/apex4.pla
+++ b/examples/apex4.pla
@ -0,0 +1,443 @@
+.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/s38584.bench
+++ b/examples/s38584.bench
--- a/examples/s444.blif
+++ b/examples/s444.blif
@ -0,0 +1,353 @@
+.model iscas\s444.bench
+.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/regtest.script
+++ b/regtest.script
@ -0,0 +1,103 @@
+r examples/apex4.pla
+resyn
+sharem
+fpga
+cec
+ps
+
+clp
+share
+resyn
+map
+cec
+ps
+
+r examples/C2670.blif
+resyn
+fpga
+cec
+ps
+
+u
+map
+cec
+ps
+
+r examples/frg2.blif
+dsd
+muxes
+cec
+clp
+share
+resyn
+map
+cec
+ps
+
+r examples/pj1.blif
+resyn
+fpga
+cec
+ps
+
+u
+map
+cec
+ps
+
+r examples/s38584.bench
+resyn
+fpga
+cec
+ps
+
+u
+map
+cec
+ps
+
+r examples/ac.v
+resyn
+fpga
+cec
+ps
+
+u
+map
+cec
+ps
+
+r examples/s444.blif
+b
+esd -v
+dsd
+cec
+ps
+
+r examples/i10.blif
+fpga
+cec
+ps
+u
+map
+cec
+ps
+
+r examples/i10.blif
+b
+fraig_store
+resyn
+fraig_store
+resyn2
+fraig_store
+fraig_restore
+fpga
+cec
+ps
+
+u
+map
+cec
+ps
+
+time
--- a/regtest_output.txt
+++ b/regtest_output.txt
@ -0,0 +1,165 @@
+UC Berkeley, ABC 1.01 (compiled Sep  5 2005 23:36:08)
+abc 01> so regtest.script
+abc - > r examples/apex4.pla
+abc - > resyn
+abc - > sharem
+abc - > fpga
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+examples/apex4.pla: i/o =    9/  19  lat =    0  nd =   784  cube =  1985  lev =   5
+abc - >
+abc - > clp
+The shared BDD size is 917 nodes.
+abc - > share
+abc - > resyn
+abc - > map
+A simple supergate library is derived from gate library "mcnc_temp.genlib".
+Loaded 20 unique 5-input supergates from "mcnc_temp.super".  Time =   0.02 sec
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+examples/apex4.pla: i/o =    9/  19  lat =    0  nd =  1816  area = 4599.00  delay = 11.50  lev =  11
+abc - >
+abc - > r examples/C2670.blif
+abc - > resyn
+abc - > fpga
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+C2670.iscas  : i/o =  233/ 140  lat =    0  nd =   169  cube =   482  lev =   6
+abc - >
+abc - > u
+abc - > map
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+C2670.iscas  : i/o =  233/ 140  lat =    0  nd =   465  area = 1142.00  delay = 15.50  lev =  14
+abc - >
+abc - > r examples/frg2.blif
+abc - > dsd
+abc - > muxes
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > clp
+The shared BDD size is 1111 nodes.
+abc - > share
+abc - > resyn
+abc - > map
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+frg2         : i/o =  143/ 139  lat =    0  nd =   540  area = 1360.00  delay = 10.10  lev =   9
+abc - >
+abc - > r examples/pj1.blif
+abc - > resyn
+abc - > fpga
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+exCombCkt    : i/o = 1769/1063  lat =    0  nd =  4730  cube = 10662  lev =  12
+abc - >
+abc - > u
+abc - > map
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+exCombCkt    : i/o = 1769/1063  lat =    0  nd = 10396  area = 25170.00  delay = 29.20  lev =  27
+abc - >
+abc - > r examples/s38584.bench
+abc - > resyn
+The network has 26 self-feeding latches.
+abc - > fpga
+abc - > cec
+The network has 26 self-feeding latches.
+The network has 26 self-feeding latches.
+Networks are equivalent after fraiging.
+abc - > ps
+examples/s38584.bench: i/o =   12/ 278  lat = 1452  nd =  3239  cube =  6769  lev =   7
+abc - >
+abc - > u
+abc - > map
+The network has 26 self-feeding latches.
+abc - > cec
+The network has 26 self-feeding latches.
+The network has 26 self-feeding latches.
+Networks are equivalent after fraiging.
+abc - > ps
+examples/s38584.bench: i/o =   12/ 278  lat = 1452  nd =  8522  area = 19305.00  delay = 20.60  lev =  17
+abc - >
+abc - > r examples/ac.v
+abc - > resyn
+abc - > fpga
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+ac97_ctrl    : i/o =   84/  48  lat = 2199  nd =  3652  cube =  9391  lev =   3
+abc - >
+abc - > u
+abc - > map
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+ac97_ctrl    : i/o =   84/  48  lat = 2199  nd =  8337  area = 19861.00  delay =  8.10  lev =   8
+abc - >
+abc - > r examples/s444.blif
+abc - > b
+abc - > esd -v
+The shared BDD size is 181 nodes.
+BDD nodes in the transition relation before reordering 557.
+BDD nodes in the transition relation after reordering 456.
+Reachability analysis completed in 151 iterations.
+The number of minterms in the reachable state set = 8865.
+BDD nodes in the unreachable states before reordering 124.
+BDD nodes in the unreachable states after reordering 113.
+abc - > dsd
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+iscas\s444.bench: i/o =    3/   6  lat =   21  nd =    81  cube =   119  lev =   7
+abc - >
+abc - > r examples/i10.blif
+abc - > fpga
+The network was strashed and balanced before FPGA mapping.
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+i10          : i/o =  257/ 224  lat =    0  nd =   741  cube =  1616  lev =  11
+abc - > u
+abc - > map
+The network was strashed and balanced before mapping.
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+i10          : i/o =  257/ 224  lat =    0  nd =  1659  area = 4215.00  delay = 30.80  lev =  27
+abc - >
+abc - > r examples/i10.blif
+abc - > b
+abc - > fraig_store
+The number of AIG nodes added to storage =  2425.
+abc - > resyn
+abc - > fraig_store
+The number of AIG nodes added to storage =  1678.
+abc - > resyn2
+abc - > fraig_store
+The number of AIG nodes added to storage =  1323.
+abc - > fraig_restore
+Currently stored 3 networks with 5426 nodes will be fraiged.
+abc - > fpga
+Performing FPGA mapping with choices.
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+i10          : i/o =  257/ 224  lat =    0  nd =   674  cube =  1498  lev =  10
+abc - >
+abc - > u
+abc - > map
+Performing mapping with choices.
+abc - > cec
+Networks are equivalent after fraiging.
+abc - > ps
+i10          : i/o =  257/ 224  lat =    0  nd =  1505  area = 3561.00  delay = 25.00  lev =  22
+abc - >
+abc 109> time
+elapse: 77.52 seconds, total: 77.52 seconds
+abc 109>
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@ -413,6 +413,7 @@ extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
 /*=== abcCheck.c ==========================================================*/
 extern bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
+extern bool               Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@ -25,6 +25,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////

+static bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 static bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk );
 static bool Abc_NtkCheckPis( Abc_Ntk_t * pNtk );
 static bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk );
@ -53,6 +54,38 @@ static bool Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fCo

 ***********************************************************************/
 bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
+{
+   return !Abc_FrameIsFlagEnabled( "check" ) || Abc_NtkDoCheck( pNtk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the integrity of the network after reading.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk )
+{
+   return !Abc_FrameIsFlagEnabled( "checkread" ) || Abc_NtkDoCheck( pNtk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the integrity of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
 {
    Abc_Obj_t * pObj, * pNet, * pNode;
    int i;
@ -402,6 +435,9 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
        }
    }

+    if ( !Abc_FrameIsFlagEnabled("checkfio") )
+        return Value;
+
    // make sure fanins are not duplicated
    for ( i = 0; i < pObj->vFanins.nSize; i++ )
        for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
@ -412,7 +448,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
            }

    // save time: do not check large fanout lists
-    if ( pObj->vFanouts.nSize > 20 )
+    if ( pObj->vFanouts.nSize > 100 )
        return Value;

    // make sure fanouts are not duplicated
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@ -41,7 +41,6 @@
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew; 
    Abc_Obj_t * pObj, * pFanin;
    int i, k;
@ -65,7 +64,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
    // duplicate EXDC 
    if ( pNtk->pExdc )
        pNtkNew->pExdc = Abc_NtkNetlistToLogic( pNtk->pExdc );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkNetlistToLogic(): Network check has failed.\n" );
    return pNtkNew;
 }
@ -146,7 +145,6 @@ Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew; 
    Abc_Obj_t * pObj, * pNet, * pDriver, * pFanin;
    char * pNameCo;
@ -214,7 +212,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
    // duplicate EXDC 
    if ( pNtk->pExdc )
        pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkLogicSopToNetlist(): Network check has failed.\n" );
    return pNtkNew;
 }
@ -232,7 +230,6 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew; 
    Abc_Obj_t * pObj, * pFanin, * pNodeNew;
    int i, k;
@ -289,7 +286,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
        else
            pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
    }
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkAigToLogicSop(): Network check has failed.\n" );
    return pNtkNew;
 }
@ -307,7 +304,6 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew; 
    Abc_Obj_t * pObj, * pFanin;
    Vec_Ptr_t * vNodes;
@ -360,7 +356,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
    // duplicate the EXDC Ntk
    if ( pNtk->pExdc )
        printf( "Warning: The EXDc network is skipped.\n" );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkAigToLogicSopBench(): Network check has failed.\n" );
    return pNtkNew;
 }
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@ -1,6 +1,6 @@
 /**CFile****************************************************************

-  FileName    [abcCreate.c]
+  FileName    [abcObj.c]

  SystemName  [ABC: Logic synthesis and verification system.]

@ -14,7 +14,7 @@

  Date        [Ver. 1.0. Started - June 20, 2005.]

-  Revision    [$Id: abcCreate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcObj.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

 ***********************************************************************/

--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@ -23,6 +23,7 @@
 #endif

 #include "abc.h"
+#include "main.h"
 #include "io.h"

 ////////////////////////////////////////////////////////////////////////
@ -195,22 +196,26 @@ void Abc_ShowFile( char * FileNameDot )
    char * FileGeneric;
    char FileNamePs[200];
    char CommandDot[1000];
-#ifndef WIN32
-    char CommandPs[1000];
-#endif
-    char * pProgDotName;
-    char * pProgGsViewName;
+    char * pDotName;
+    char * pDotNameWin = "dot.exe";
+    char * pDotNameUnix = "dot";
+    char * pGsNameWin = "gsview32.exe";
+    char * pGsNameUnix = "gv";
    int RetValue;

+    // get DOT names from the resource file
+    if ( Abc_FrameReadFlag("dotwin") )
+        pDotNameWin = Abc_FrameReadFlag("dotwin");
+    if ( Abc_FrameReadFlag("dotunix") )
+        pDotNameUnix = Abc_FrameReadFlag("dotunix");
+
 #ifdef WIN32
-    pProgDotName = "dot.exe";
-    pProgGsViewName = NULL;
+    pDotName = pDotNameWin;
 #else
-    pProgDotName = "dot";
-    pProgGsViewName = "gv";
+    pDotName = pDotNameUnix;
 #endif

-    // check that the input file is okay
+    // check if the input DOT file is okay
    if ( (pFile = fopen( FileNameDot, "r" )) == NULL )
    {
        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
@ -218,27 +223,20 @@ void Abc_ShowFile( char * FileNameDot )
    }
    fclose( pFile );

-    // get the generic file name
-    FileGeneric = Extra_FileNameGeneric( FileNameDot );
    // create the PostScript file name
+    FileGeneric = Extra_FileNameGeneric( FileNameDot );
    sprintf( FileNamePs,  "%s.ps",  FileGeneric ); 
    free( FileGeneric );

-    // generate the DOT file
-    sprintf( CommandDot,  "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot ); 
+    // generate the PostScript file using DOT
+    sprintf( CommandDot,  "%s -Tps -o %s %s", pDotName, FileNamePs, FileNameDot ); 
    RetValue = system( CommandDot );
-#ifdef WIN32
-        _unlink( FileNameDot );
-#else
-        unlink( FileNameDot );
-#endif
    if ( RetValue == -1 )
    {
-        fprintf( stdout, "Cannot find \"%s\".\n", pProgDotName );
+        fprintf( stdout, "Command \"%s\" did not succeed.\n", CommandDot );
        return;
    }
-
-    // check that the input file is okay
+    // check that the input PostScript file is okay
    if ( (pFile = fopen( FileNamePs, "r" )) == NULL )
    {
        fprintf( stdout, "Cannot open intermediate file \"%s\".\n", FileNamePs );
@ -246,20 +244,33 @@ void Abc_ShowFile( char * FileNameDot )
    }
    fclose( pFile ); 

+
+    // get GSVIEW names from the resource file
+    if ( Abc_FrameReadFlag("gsviewwin") )
+        pGsNameWin = Abc_FrameReadFlag("gsviewwin");
+    if ( Abc_FrameReadFlag("gsviewunix") )
+        pGsNameUnix = Abc_FrameReadFlag("gsviewunix");
+
+    // spawn the viewer
 #ifdef WIN32
-    if ( _spawnl( _P_NOWAIT, "gsview32.exe", "gsview32.exe", FileNamePs, NULL ) == -1 )
+    _unlink( FileNameDot );
+    if ( _spawnl( _P_NOWAIT, pGsNameWin, pGsNameWin, FileNamePs, NULL ) == -1 )
        if ( _spawnl( _P_NOWAIT, "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", 
            "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", FileNamePs, NULL ) == -1 )
        {
-            fprintf( stdout, "Cannot find \"%s\".\n", "gsview32.exe" );
+            fprintf( stdout, "Cannot find \"%s\".\n", pGsNameWin );
            return;
        }
 #else
-    sprintf( CommandPs,  "%s %s &", pProgGsViewName, FileNamePs ); 
-    if ( system( CommandPs ) == -1 )
    {
-        fprintf( stdout, "Cannot execute \"%s\".\n", FileNamePs );
-        return;
+        char CommandPs[1000];
+        unlink( FileNameDot );
+        sprintf( CommandPs,  "%s %s &", pGsNameUnix, FileNamePs ); 
+        if ( system( CommandPs ) == -1 )
+        {
+            fprintf( stdout, "Cannot execute \"%s\".\n", CommandPs );
+            return;
+        }
    }
 #endif
 }
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@ -546,7 +546,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )

    if ( !fProfile && !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "This command works only for AIGs.\n" );
+        fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
        return 1;
    }

@ -597,18 +597,23 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
    FILE * pOut, * pErr;
    Abc_Ntk_t * pNtk;
    int c;
-    extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk );
+    int fVerbose;
+    extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );

    pNtk = Abc_FrameReadNet(pAbc);
    pOut = Abc_FrameReadOut(pAbc);
    pErr = Abc_FrameReadErr(pAbc);

    // set defaults
+    fVerbose = 0;
    util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
    {
        switch ( c )
        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
        case 'h':
            goto usage;
        default:
@ -621,26 +626,25 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
        fprintf( pErr, "Empty network.\n" );
        return 1;
    }
-
    if ( !Abc_NtkIsComb(pNtk) )
    {
        fprintf( pErr, "This command works only for combinational networks.\n" );
        return 1;
    }
-
    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "This command works only for AIGs.\n" );
+        fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
        return 1;
    }
-    vSuppFun = Sim_ComputeFunSupp( pNtk );
+    vSuppFun = Sim_ComputeFunSupp( pNtk, fVerbose );
    free( vSuppFun->pArray[0] );
    Vec_PtrFree( vSuppFun );
    return 0;

 usage:
-    fprintf( pErr, "usage: print_supp [-h]\n" );
+    fprintf( pErr, "usage: print_supp [-vh]\n" );
    fprintf( pErr, "\t        prints the supports of the CO nodes\n" );
+    fprintf( pErr, "\t-v    : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
    fprintf( pErr, "\t-h    : print the command usage\n");
    return 1;
 }
@ -706,7 +710,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
    }
    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "This command works only for AIGs.\n" );
+        fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
        return 1;
    }
    Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fVerbose );
@ -715,7 +719,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
    fprintf( pErr, "usage: print_symm [-nbvh]\n" );
    fprintf( pErr, "\t         computes symmetries of the PO functions\n" );
-    fprintf( pErr, "\t-b     : enable efficient BDD-based computation [default = %s].\n", fUseBdds? "yes": "no" );  
+    fprintf( pErr, "\t-b     : toggle BDD-based or SAT-based computations [default = %s].\n", fUseBdds? "bdd": "sat" );  
    fprintf( pErr, "\t-n     : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" );  
    fprintf( pErr, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
    fprintf( pErr, "\t-h     : print the command usage\n");
@ -867,7 +871,7 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv )

    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "Visualizing cuts only works for AIGs.\n" );
+        fprintf( pErr, "Visualizing cuts only works for AIGs (run \"strash\").\n" );
        return 1;
    }
    if ( argc != util_optind + 1 )
@ -942,7 +946,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )

    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "Visualizing AIG can only be done for AIGs.\n" );
+        fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\").\n" );
        return 1;
    }
    Abc_NtkShowAig( pNtk );
@ -1002,7 +1006,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )

    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "Can only collapse a logic network.\n" );
+        fprintf( pErr, "Can only collapse a logic network or an AIG.\n" );
        return 1;
    }

@ -1262,7 +1266,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
    }
    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "Cannot renode a network that is not an AIG.\n" );
+        fprintf( pErr, "Cannot renode a network that is not an AIG (run \"strash\").\n" );
        return 1;
    }

@ -1504,7 +1508,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )

    if ( !Abc_NtkIsLogic(pNtk) )
    {
-        fprintf( pErr, "Fast extract can only be applied to a logic network.\n" );
+        fprintf( pErr, "Fast extract can only be applied to a logic network (run \"renode\").\n" );
        Abc_NtkFxuFreeInfo( p );
        return 1;
    }
@ -1717,7 +1721,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
    }
    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "This command can only be applied to an AIG.\n" );
+        fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" );
        return 1;
    }
    if ( Abc_NtkGetChoiceNum(pNtk) )
@ -1826,7 +1830,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
    }
    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "This command can only be applied to an AIG.\n" );
+        fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" );
        return 1;
    }
    if ( Abc_NtkGetChoiceNum(pNtk) )
@ -2322,7 +2326,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
    }
    if ( !Abc_NtkIsLogic(pNtk) )
    {
-        fprintf( stdout, "This command can only be applied to logic network.\n" );
+        fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" );
        return 0;
    }
    if ( Abc_NtkIsMappedLogic(pNtk) )
@ -2397,7 +2401,7 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
    }
    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( stdout, "This command works only for AIGs.\n" );
+        fprintf( stdout, "This command works only for AIGs (run \"strash\").\n" );
        return 0;
    }
    if ( !Abc_NtkExtractSequentialDcs( pNtk, fVerbose ) )
@ -2751,7 +2755,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
    }
    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "Cut computation is available only for AIGs.\n" );
+        fprintf( pErr, "Cut computation is available only for AIGs (run \"strash\").\n" );
        return 1;
    }
    pCutMan = Abc_NtkCuts( pNtk, pParams );
@ -3606,7 +3610,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )

    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "Works only for the AIG representation.\n" );
+        fprintf( pErr, "Works only for the AIG representation (run \"strash\").\n" );
        return 1;
    }

@ -3785,7 +3789,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )

    if ( !Abc_NtkIsStrash(pNtk) )
    {
-        fprintf( pErr, "Works only for AIG.\n" );
+        fprintf( pErr, "Works only for AIG (run \"strash\").\n" );
        return 1;
    }

--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@ -56,7 +56,6 @@ static int s_nPerms;
 ***********************************************************************/
 int Abc_NtkAttach( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Mio_Library_t * pGenlib;
    unsigned ** puTruthGates;
    unsigned uTruths[6][2];
@ -149,7 +148,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
    printf( "Library gates are successfully attached to the nodes.\n" );

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
    {
        printf( "Abc_NtkAttach: The network check has failed.\n" );
        return 0;
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@ -46,7 +46,6 @@ static int         Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSupe
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkAig;
    assert( Abc_NtkIsStrash(pNtk) );
    // perform balancing
@ -54,7 +53,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
    Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate );
    Abc_NtkFinalize( pNtk, pNtkAig );
    // make sure everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkAig ) )
+    if ( !Abc_NtkCheck( pNtkAig ) )
    {
        printf( "Abc_NtkBalance: The network check has failed.\n" );
        Abc_NtkDelete( pNtkAig );
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@ -44,7 +44,6 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew;

    assert( Abc_NtkIsStrash(pNtk) );
@ -71,7 +70,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
    Abc_NtkMinimumBase( pNtkNew );

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkCollapse: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@ -55,7 +55,6 @@ static int             Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int n
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew;

    assert( Abc_NtkIsStrash(pNtk) );
@ -78,7 +77,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
    pNtk->pManGlob = NULL;

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkDsdGlobal: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
@ -304,7 +303,6 @@ Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNode
 ***********************************************************************/
 int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive )
 {
-    int fCheck = 1;
    Dsd_Manager_t * pManDsd;
    DdManager * dd = pNtk->pManFunc;
    Vec_Ptr_t * vNodes;
@ -328,7 +326,7 @@ int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive )
    Dsd_ManagerStop( pManDsd );

    // make sure everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
    {
        printf( "Abc_NtkDsdRecursive: The network check has failed.\n" );
        return 0;
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@ -46,12 +46,11 @@ static Abc_Obj_t *  Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNo
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fVerbose )
 {
-    int fCheck = 1;
+    int fShowSwitching = 1;
    Abc_Ntk_t * pNtkNew;
    Fpga_Man_t * pMan;
    Vec_Int_t * vSwitching;
    float * pSwitching = NULL;
-    int fShowSwitching = 0;

    assert( Abc_NtkIsStrash(pNtk) );

@ -90,7 +89,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fV
    Abc_NtkMinimumBase( pNtkNew );

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkFpga: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@ -51,7 +51,6 @@ static Abc_Obj_t *   Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
 {
-    int fCheck = 1;
    Fraig_Params_t * pPars = pParams;
    Abc_Ntk_t * pNtkNew;
    Fraig_Man_t * pMan;
@ -64,7 +63,7 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
    pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
    Fraig_ManFree( pMan );
    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkFraig: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
@ -249,7 +248,6 @@ Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFrai
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew;

    if ( !Abc_NtkIsSopLogic(pNtk) )
@ -273,7 +271,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
    printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkFraigTrust: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
@ -420,7 +418,6 @@ Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
 ***********************************************************************/
 int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
 {
-    Abc_Frame_t * p;
    Abc_Ntk_t * pStore;
    int nAndsOld;

@ -431,8 +428,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
    }

    // get the network currently stored
-    p = Abc_FrameGetGlobalFrame();
-    pStore = Abc_FrameReadNtkStore(p);
+    pStore = Abc_FrameReadNtkStore();
    if ( pStore == NULL )
    {
        // start the stored network
@ -443,8 +439,8 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
            return 0;
        }
        // save the parameters
-        Abc_FrameSetNtkStore( p, pStore );
-        Abc_FrameSetNtkStoreSize( p, 1 );
+        Abc_FrameSetNtkStore( pStore );
+        Abc_FrameSetNtkStoreSize( 1 );
        nAndsOld = 0;
    }
    else
@ -457,7 +453,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
            return 0;
        }
        // set the number of networks stored
-        Abc_FrameSetNtkStoreSize( p, Abc_FrameReadNtkStoreSize(p) + 1 );
+        Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
    }
    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
    return 1;
@ -476,22 +472,20 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFraigRestore()
 {
-    Abc_Frame_t * p;
    Fraig_Params_t Params;
    Abc_Ntk_t * pStore, * pFraig;
    int nWords1, nWords2, nWordsMin;

    // get the stored network
-    p = Abc_FrameGetGlobalFrame();
-    pStore   = Abc_FrameReadNtkStore(p);
-    Abc_FrameSetNtkStore( p, NULL );
+    pStore = Abc_FrameReadNtkStore();
+    Abc_FrameSetNtkStore( NULL );
    if ( pStore == NULL )
    {
        printf( "There are no network currently in storage.\n" );
        return NULL;
    }
    printf( "Currently stored %d networks with %d nodes will be fraiged.\n", 
-        Abc_FrameReadNtkStoreSize(p), Abc_NtkNodeNum(pStore) );
+        Abc_FrameReadNtkStoreSize(), Abc_NtkNodeNum(pStore) );

    // to determine the number of simulation patterns
    // use the following strategy
@ -536,14 +530,12 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
 ***********************************************************************/
 void Abc_NtkFraigStoreClean()
 {
-    Abc_Frame_t * p;
    Abc_Ntk_t * pStore;
    // get the stored network
-    p = Abc_FrameGetGlobalFrame();
-    pStore = Abc_FrameReadNtkStore(p);
+    pStore = Abc_FrameReadNtkStore();
    if ( pStore )
        Abc_NtkDelete( pStore );
-    Abc_FrameSetNtkStore( p, NULL );
+    Abc_FrameSetNtkStore( NULL );
 }

 /**Function*************************************************************
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@ -52,8 +52,6 @@ static void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
 ***********************************************************************/
 bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
-    int fCheck = 1;
-
    assert( Abc_NtkIsLogic(pNtk) );
    // convert nodes to SOPs
    if ( Abc_NtkIsMappedLogic(pNtk) )
@ -81,7 +79,7 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
        // update the network
        Abc_NtkFxuReconstruct( pNtk, p );
        // make sure everything is okay
-        if ( fCheck && !Abc_NtkCheck( pNtk ) )
+        if ( !Abc_NtkCheck( pNtk ) )
            printf( "Abc_NtkFastExtract: The network check has failed.\n" );
        return 1;
    }
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@ -56,7 +56,6 @@ static Abc_Obj_t *  Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Sup
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew;
    Map_Man_t * pMan;
    Vec_Int_t * vSwitching;
@ -106,7 +105,7 @@ clk = clock();
        Map_ManFree( pMan );
        return NULL;
    }
-    Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk );
+//    Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk );

    // reconstruct the network after mapping
    pNtkNew = Abc_NtkFromMap( pMan, pNtk );
@ -115,7 +114,7 @@ clk = clock();
    Map_ManFree( pMan );

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkMap: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
@ -440,7 +439,6 @@ int Abc_NtkUnmap( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew;

    Map_Man_t * pMan;
@ -483,7 +481,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
    Map_ManFree( pMan );

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkMap: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@ -77,7 +77,6 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 {
-    int fCheck = 1;
    char Buffer[100];
    Abc_Ntk_t * pNtkMiter;

@ -96,7 +95,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
    Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb );

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkMiter ) )
+    if ( !Abc_NtkCheck( pNtkMiter ) )
    {
        printf( "Abc_NtkMiter: The network check has failed.\n" );
        Abc_NtkDelete( pNtkMiter );
@ -312,7 +311,6 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
 {
-    int fCheck = 1;
    char Buffer[100];
    Abc_Ntk_t * pNtkMiter;
    Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
@ -357,7 +355,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
    Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkMiter ) )
+    if ( !Abc_NtkCheck( pNtkMiter ) )
    {
        printf( "Abc_NtkMiter: The network check has failed.\n" );
        Abc_NtkDelete( pNtkMiter );
@ -470,7 +468,6 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
 {
-    int fCheck = 1;
    char Buffer[100];
    ProgressBar * pProgress;
    Abc_Ntk_t * pNtkFrames;
@ -531,7 +528,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
        }
    }
    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkFrames ) )
+    if ( !Abc_NtkCheck( pNtkFrames ) )
    {
        printf( "Abc_NtkFrames: The network check has failed.\n" );
        Abc_NtkDelete( pNtkFrames );
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@ -119,14 +119,13 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew;
    assert( Abc_NtkIsBddLogic(pNtk) );
    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
    Abc_NtkBddToMuxesPerform( pNtk, pNtkNew );
    Abc_NtkFinalize( pNtk, pNtkNew );
    // make sure everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkBddToMuxes: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@ -1,12 +1,12 @@
 /**CFile****************************************************************

-  FileName    [abcRes.c]
+  FileName    [abcReconv.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

-  Synopsis    [Reconvergence=driven cut computation.]
+  Synopsis    [Computation of reconvergence-driven cuts.]

  Author      [Alan Mishchenko]
  
@ -14,7 +14,7 @@

  Date        [Ver. 1.0. Started - June 20, 2005.]

-  Revision    [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcReconv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

 ***********************************************************************/

--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@ -1,12 +1,12 @@
 /**CFile****************************************************************

-  FileName    [abcResRef.c]
+  FileName    [abcRefactor.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

-  Synopsis    [Resynthesis based on refactoring.]
+  Synopsis    [Resynthesis based on collapsing and refactoring.]

  Author      [Alan Mishchenko]
  
@ -14,7 +14,7 @@

  Date        [Ver. 1.0. Started - June 20, 2005.]

-  Revision    [$Id: abcResRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcRefactor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

 ***********************************************************************/

@ -82,7 +82,6 @@ static Dec_Graph_t *  Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec
 ***********************************************************************/
 int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseZeros, bool fUseDcs, bool fVerbose )
 {
-    int fCheck = 1;
    ProgressBar * pProgress;
    Abc_ManRef_t * pManRef;
    Abc_ManCut_t * pManCut;
@ -110,6 +109,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
        // skip the constant node
        if ( Abc_NodeIsConst(pNode) )
            continue;
+        // skip the nodes with many fanouts
+        if ( Abc_ObjFanoutNum(pNode) > 1000 )
+            continue;
        // stop if all nodes have been tried once
        if ( i >= nNodes )
            break;
@ -140,7 +142,7 @@ pManRef->timeTotal = clock() - clkStart;
    Abc_NtkManRefStop( pManRef );
    Abc_NtkStopReverseLevels( pNtk );
    // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
    {
        printf( "Abc_NtkRefactor: The network check has failed.\n" );
        return 0;
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@ -6,7 +6,7 @@

  PackageName [Network and node package.]

-  Synopsis    [Procedures which transform an AIG into the network of nodes.]
+  Synopsis    [Procedures which transform an AIG into the network of SOP logic nodes.]

  Author      [Alan Mishchenko]
  
@ -52,7 +52,6 @@ static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew;

    assert( Abc_NtkIsStrash(pNtk) );
@ -93,7 +92,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
 //printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );

    // make sure everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkRenode: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@ -1,12 +1,12 @@
 /**CFile****************************************************************

-  FileName    [abcRes.c]
+  FileName    [abcRewrite.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

-  Synopsis    [Technology-independent resynthesis of the AIG.]
+  Synopsis    [Technology-independent resynthesis of the AIG based on DAG aware rewriting.]

  Author      [Alan Mishchenko]
  
@ -14,7 +14,7 @@

  Date        [Ver. 1.0. Started - June 20, 2005.]

-  Revision    [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcRewrite.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

 ***********************************************************************/

@ -22,6 +22,12 @@
 #include "rwr.h"
 #include "dec.h"

+/*
+    The ideas realized in this package are inspired by the paper:
+    Per Bjesse, Arne Boralv, "DAG-aware circuit compression for 
+    formal verification", Proc. ICCAD 2004, pp. 42-49.
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@ -46,7 +52,6 @@ static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
 ***********************************************************************/
 int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
 {
-    int fCheck = 1;
    int fDrop = 0;
    ProgressBar * pProgress;
    Cut_Man_t * pManCut;
@ -81,6 +86,9 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
        // skip the constant node
        if ( Abc_NodeIsConst(pNode) )
            continue;
+        // skip the nodes with many fanouts
+        if ( Abc_ObjFanoutNum(pNode) > 1000 )
+            continue;
        // for each cut, try to resynthesize it
        nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUseZeros );
        if ( nGain > 0 || nGain == 0 && fUseZeros )
@ -104,7 +112,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
    pNtk->pManCut = NULL;
    Abc_NtkStopReverseLevels( pNtk );
    // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
    {
        printf( "Abc_NtkRewrite: The network check has failed.\n" );
        return 0;
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@ -51,7 +51,6 @@ extern char *      Mio_GateReadSop( void * pGate );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkAig;
    int nNodes;

@ -74,7 +73,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
    if ( pNtk->pExdc )
        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 );
    // make sure everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkAig ) )
+    if ( !Abc_NtkCheck( pNtkAig ) )
    {
        printf( "Abc_NtkStrash: The network check has failed.\n" );
        Abc_NtkDelete( pNtkAig );
@ -99,7 +98,6 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
 ***********************************************************************/
 int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 {
-    int fCheck = 1;
    Abc_Obj_t * pObj;
    int i;
    // the first network should be an AIG
@ -118,7 +116,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
    // add pNtk2 to pNtk1 while strashing
    Abc_NtkStrashPerform( pNtk2, pNtk1, 1 );
    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtk1 ) )
+    if ( !Abc_NtkCheck( pNtk1 ) )
    {
        printf( "Abc_NtkAppend: The network check has failed.\n" );
        return 0;
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@ -56,7 +56,6 @@ static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pF
 ***********************************************************************/
 bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
 {
-    int fCheck = 1;
    Fraig_Params_t Params;
    Abc_Ntk_t * pNtkAig;
    Fraig_Man_t * pMan;
@ -83,7 +82,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
    // cleanup the dangling nodes
    Abc_NtkCleanup( pNtk, fVerbose );
    // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
    {
        printf( "Abc_NtkFraigSweep: The network check has failed.\n" );
        return 0;
@ -394,7 +393,6 @@ int Abc_NodeDroppingCost( Abc_Obj_t * pNode )
 ***********************************************************************/
 int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    int fCheck = 1;
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pNode;
    int i, Counter;
@ -423,7 +421,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
    if ( fVerbose )
        printf( "Cleanup removed %d dangling nodes.\n", Counter );
    // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
    {
        printf( "Abc_NtkCleanup: The network check has failed.\n" );
        return -1;
@ -447,7 +445,6 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    int fCheck = 1;
    Abc_Obj_t * pNode;
    int i, fConvert, nSwept, nSweptNew;
    assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsBddLogic(pNtk) ); 
@ -481,7 +478,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
    if ( fVerbose )
        printf( "Sweep removed %d nodes.\n", nSwept );
    // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
    {
        printf( "Abc_NtkSweep: The network check has failed.\n" );
        return -1;
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@ -46,7 +46,7 @@ static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms )
 ***********************************************************************/
 void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose )
 {
-    if ( fUseBdds || fNaive )
+    if ( fUseBdds )
        Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose );
    else
        Abc_NtkSymmetriesUsingSandS( pNtk, fVerbose );
@ -65,8 +65,8 @@ void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose
 ***********************************************************************/
 void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk );
-    int nSymms = Sim_ComputeTwoVarSymms( pNtk );
+    extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose );
+    int nSymms = Sim_ComputeTwoVarSymms( pNtk, fVerbose );
    printf( "The total number of symmetries is %d.\n", nSymms );
 }

@ -123,12 +123,14 @@ void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVer
    Abc_Obj_t * pNode;
    DdNode * bFunc;
    int nSymms = 0;
+    int nSupps = 0;
    int i;

    // compute symmetry info for each PO
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
        bFunc = pNtk->vFuncsGlob->pArray[i];
+        nSupps += Cudd_SupportSize( dd, bFunc );
        if ( Cudd_IsConstant(bFunc) )
            continue;
        if ( fNaive )
@ -144,7 +146,8 @@ void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVer
 //Extra_SymmPairsPrint( pSymms );
        Extra_SymmPairsDissolve( pSymms );
    }
-    printf( "The total number of symmetries is %d.\n", nSymms );
+    printf( "Total number of vars in functional supports = %8d.\n", nSupps );
+    printf( "Total number of two-variable symmetries     = %8d.\n", nSymms );
 }

 /**Function*************************************************************
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@ -46,7 +46,6 @@ static Abc_Ntk_t * Abc_NtkConstructExdc     ( DdManager * dd, Abc_Ntk_t * pNtk,
 ***********************************************************************/
 int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
 {
-    int fCheck   = 1;
    int fReorder = 1;
    DdManager * dd;
    DdNode * bRelation, * bInitial, * bUnreach;
@ -94,7 +93,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
    pNtk->pManGlob = NULL;

    // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) )
+    if ( !Abc_NtkCheck( pNtk->pExdc ) )
    {
        printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" );
        Abc_NtkDelete( pNtk->pExdc );
--- a/src/base/abcs/abcSeq.c
+++ b/src/base/abcs/abcSeq.c
@ -60,7 +60,6 @@ static void        Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew;
    Abc_Aig_t * pManNew;
    Vec_Ptr_t * vNodes;
@ -176,7 +175,7 @@ printf( "\n" );

    if ( pNtk->pExdc )
        fprintf( stdout, "Warning: EXDC is dropped when converting to sequential AIG.\n" );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" );
    return pNtkNew;
 }
@ -194,7 +193,6 @@ printf( "\n" );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
    Abc_Ntk_t * pNtkNew; 
    Abc_Obj_t * pObj, * pFanin, * pFaninNew;
    int i, k, c;
@ -233,7 +231,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
    // duplicate the EXDC network
    if ( pNtk->pExdc )
        fprintf( stdout, "Warning: EXDC network is not copied.\n" );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" );
    return pNtkNew;
 }
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@ -29,7 +29,6 @@
 static int CmdCommandTime          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandEcho          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandQuit          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int CmdCommandUsage         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandWhich         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandHistory       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandAlias         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -70,7 +69,6 @@ void Cmd_Init( Abc_Frame_t * pAbc )
    Cmd_CommandAdd( pAbc, "Basic", "time",      CmdCommandTime,           0);
    Cmd_CommandAdd( pAbc, "Basic", "echo",      CmdCommandEcho,           0);
    Cmd_CommandAdd( pAbc, "Basic", "quit",      CmdCommandQuit,           0);
-//    Cmd_CommandAdd( pAbc, "Basic", "usage",     CmdCommandUsage,          0);
    Cmd_CommandAdd( pAbc, "Basic", "history",   CmdCommandHistory,        0);
    Cmd_CommandAdd( pAbc, "Basic", "alias",     CmdCommandAlias,          0);
    Cmd_CommandAdd( pAbc, "Basic", "unalias",   CmdCommandUnalias,        0);
@ -79,7 +77,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
    Cmd_CommandAdd( pAbc, "Basic", "set",       CmdCommandSetVariable,    0);
    Cmd_CommandAdd( pAbc, "Basic", "unset",     CmdCommandUnsetVariable,  0);
    Cmd_CommandAdd( pAbc, "Basic", "undo",      CmdCommandUndo,           0); 
-//    Cmd_CommandAdd( pAbc, "Basic", "recall",    CmdCommandRecall,         0); 
+    Cmd_CommandAdd( pAbc, "Basic", "recall",    CmdCommandRecall,         0); 
    Cmd_CommandAdd( pAbc, "Basic", "empty",     CmdCommandEmpty,          0); 
 #ifdef WIN32
    Cmd_CommandAdd( pAbc, "Basic", "ls",        CmdCommandLs,             0 );
@ -264,45 +262,6 @@ int CmdCommandQuit( Abc_Frame_t * pAbc, int argc, char **argv )
    return 1;
 }

-/**Function********************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-int CmdCommandUsage( Abc_Frame_t * pAbc, int argc, char **argv )
-{
-    int c;
-
-    util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( argc != util_optind )
-        goto usage;
-    util_print_cpu_stats( pAbc->Out );
-    return 0;
-
-  usage:
-    fprintf( pAbc->Err, "usage: usage [-h]\n" );
-    fprintf( pAbc->Err, "   -h \t\tprint the command usage\n" );
-    return 1;
-}
-
 /**Function********************************************************************

  Synopsis    []
@ -332,11 +291,9 @@ int CmdCommandWhich( Abc_Frame_t * pAbc, int argc, char **argv )
 ******************************************************************************/
 int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
 {
-    int i, num;
-    int size;
-    int c;
-    num = 50;
+    int i, c, num, size;

+    num = 20;
    util_getopt_reset();
    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
    {
@ -344,23 +301,28 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
        {
            case 'h':
                goto usage;
-            break;
+            default :
+                goto usage;
        }
    }
-
-    if ( argc > 3 )
+    if ( argc > 2 )
        goto usage;

+    // get the number of commands to print
+    if ( argc == util_optind + 1 )
+        num = atoi(argv[util_optind]);
+    // print the commands
    size = pAbc->aHistory->nSize;
    num = ( num < size ) ? num : size;
    for ( i = size - num; i < size; i++ )
        fprintf( pAbc->Out, "%s", pAbc->aHistory->pArray[i] );
    return 0;

-  usage:
-    fprintf( pAbc->Err, "usage: history [-h] [num]\n" );
-    fprintf( pAbc->Err, "   -h \t\tprint the command usage\n" );
-    fprintf( pAbc->Err, "   num \t\tprint the last num commands\n" );
+usage:
+    fprintf( pAbc->Err, "usage: history [-h] <num>\n" );
+    fprintf( pAbc->Err, "          prints the latest command entered on the command line\n" );
+    fprintf( pAbc->Err, " -h     : print the command usage\n" );
+    fprintf( pAbc->Err, "num     : print the last num commands\n" );
    return ( 1 );
 }

@ -378,7 +340,6 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
 int CmdCommandAlias( Abc_Frame_t * pAbc, int argc, char **argv )
 {
    char *key, *value;
-    st_generator *gen;
    int c;

    util_getopt_reset();
@ -397,8 +358,7 @@ int CmdCommandAlias( Abc_Frame_t * pAbc, int argc, char **argv )

    if ( argc == 1 )
    {
-        st_foreach_item( pAbc->tAliases, gen, &key, &value )
-            CmdCommandAliasPrint( pAbc, ( Abc_Alias * ) value );
+        CmdPrintTable( pAbc->tAliases, 1 );
        return 0;

    }
@ -712,7 +672,6 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv )
 int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
 {
    char *flag_value, *key, *value;
-    st_generator *gen;
    int c;

    util_getopt_reset();
@ -722,7 +681,6 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
        {
        case 'h':
            goto usage;
-            break;
        default:
            goto usage;
        }
@ -733,10 +691,7 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
    }
    else if ( argc == 1 )
    {
-        st_foreach_item( pAbc->tFlags, gen, &key, &value )
-        {
-            fprintf( pAbc->Out, "%s\t%s\n", key, value );
-        }
+        CmdPrintTable( pAbc->tFlags, 0 );
        return 0;
    }
    else
@ -749,25 +704,18 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
        }

        flag_value = argc == 2 ? util_strsav( "" ) : util_strsav( argv[2] );
-
-        ( void ) st_insert( pAbc->tFlags, util_strsav( argv[1] ),
-                             flag_value );
+//        flag_value = argc == 2 ? NULL : util_strsav(argv[2]);
+        st_insert( pAbc->tFlags, util_strsav(argv[1]), flag_value );

        if ( strcmp( argv[1], "abcout" ) == 0 )
        {
            if ( pAbc->Out != stdout )
-            {
-                ( void ) fclose( pAbc->Out );
-            }
+                fclose( pAbc->Out );
            if ( strcmp( flag_value, "" ) == 0 )
-            {
                flag_value = "-";
-            }
            pAbc->Out = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 );
            if ( pAbc->Out == NULL )
-            {
                pAbc->Out = stdout;
-            }
 #if HAVE_SETVBUF
            setvbuf( pAbc->Out, ( char * ) NULL, _IOLBF, 0 );
 #endif
@ -775,18 +723,12 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
        if ( strcmp( argv[1], "abcerr" ) == 0 )
        {
            if ( pAbc->Err != stderr )
-            {
-                ( void ) fclose( pAbc->Err );
-            }
+                fclose( pAbc->Err );
            if ( strcmp( flag_value, "" ) == 0 )
-            {
                flag_value = "-";
-            }
            pAbc->Err = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 );
            if ( pAbc->Err == NULL )
-            {
                pAbc->Err = stderr;
-            }
 #if HAVE_SETVBUF
            setvbuf( pAbc->Err, ( char * ) NULL, _IOLBF, 0 );
 #endif
@ -794,28 +736,21 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
        if ( strcmp( argv[1], "history" ) == 0 )
        {
            if ( pAbc->Hst != NIL( FILE ) )
-            {
-                ( void ) fclose( pAbc->Hst );
-            }
+                fclose( pAbc->Hst );
            if ( strcmp( flag_value, "" ) == 0 )
-            {
                pAbc->Hst = NIL( FILE );
-            }
            else
            {
-                pAbc->Hst =
-                    CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 );
+                pAbc->Hst = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 );
                if ( pAbc->Hst == NULL )
-                {
                    pAbc->Hst = NIL( FILE );
-                }
            }
        }
        return 0;
    }

  usage:
-    fprintf( pAbc->Err, "usage: set [-h] [name] [value]\n" );
+    fprintf( pAbc->Err, "usage: set [-h] <name> <value>\n" );
    fprintf( pAbc->Err, "\t        sets the value of parameter <name>\n" );
    fprintf( pAbc->Err, "\t-h    : print the command usage\n" );
    return 1;
@ -870,8 +805,9 @@ int CmdCommandUnsetVariable( Abc_Frame_t * pAbc, int argc, char **argv )


  usage:
-    fprintf( pAbc->Err, "usage: unset [-h] variables \n" );
-    fprintf( pAbc->Err, "   -h \t\tprint the command usage\n" );
+    fprintf( pAbc->Err, "usage: unset [-h] <name> \n" );
+    fprintf( pAbc->Err, "\t        removes the value of parameter <name>\n" );
+    fprintf( pAbc->Err, "\t-h    : print the command usage\n" );
    return 1;
 }

@ -1014,9 +950,10 @@ int CmdCommandRecall( Abc_Frame_t * pAbc, int argc, char **argv )

 usage:

-    fprintf( pAbc->Err, "usage: recall <num>\n" );
+    fprintf( pAbc->Err, "usage: recall -h <num>\n" );
    fprintf( pAbc->Err, "         set the current network to be one of the previous networks\n" );
    fprintf( pAbc->Err, "<num> :  level to return to [default = previous]\n" );
+    fprintf( pAbc->Err, "   -h :  print the command usage\n");
    return 1;
 }

@ -1260,7 +1197,9 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
 {
    FILE * pFile;
    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkNew;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNetlist;
+    char * pNameWin = "sis.exe";
+    char * pNameUnix = "sis";
    char Command[1000], Buffer[100];
    char * pSisName;
    int i;
@ -1288,23 +1227,28 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
    if ( strcmp( argv[1], "-?" ) == 0 )
        goto usage;

+    // get the names from the resource file
+    if ( Cmd_FlagReadByName(pAbc, "siswin") )
+        pNameWin = Cmd_FlagReadByName(pAbc, "siswin");
+    if ( Cmd_FlagReadByName(pAbc, "sisunix") )
+        pNameUnix = Cmd_FlagReadByName(pAbc, "sisunix");
+
    // check if SIS is available
-    if ( (pFile = fopen( "sis.exe", "r" )) )
-        pSisName = "sis.exe";
-    else if ( (pFile = fopen( "sis", "r" )) )
-        pSisName = "sis";
+    if ( (pFile = fopen( pNameWin, "r" )) )
+        pSisName = pNameWin;
+    else if ( (pFile = fopen( pNameUnix, "r" )) )
+        pSisName = pNameUnix;
    else if ( pFile == NULL )
    {
-        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", "sis.exe", "sis" );
+        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pNameWin, pNameUnix );
        goto usage;
    }
    fclose( pFile );

-    if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
-
    // write out the current network
-    Io_WriteBlifLogic( pNtk, "_sis_in.blif", 1 );
+    pNetlist = Abc_NtkLogicToNetlist(pNtk);
+    Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
+    Abc_NtkDelete( pNetlist );

    // create the file for sis
    sprintf( Command, "%s -x -c ", pSisName );
@ -1383,8 +1327,10 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
 {
    FILE * pFile;
    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkNew;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNetlist;
    char Command[1000], Buffer[100];
+    char * pNameWin = "mvsis.exe";
+    char * pNameUnix = "mvsis";
    char * pMvsisName;
    int i;

@ -1411,23 +1357,29 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
    if ( strcmp( argv[1], "-?" ) == 0 )
        goto usage;

+    // get the names from the resource file
+    if ( Cmd_FlagReadByName(pAbc, "mvsiswin") )
+        pNameWin = Cmd_FlagReadByName(pAbc, "mvsiswin");
+    if ( Cmd_FlagReadByName(pAbc, "mvsisunix") )
+        pNameUnix = Cmd_FlagReadByName(pAbc, "mvsisunix");
+
    // check if MVSIS is available
-    if ( (pFile = fopen( "mvsis.exe", "r" )) )
-        pMvsisName = "mvsis.exe";
-    else if ( (pFile = fopen( "mvsis", "r" )) )
-        pMvsisName = "mvsis";
+    if ( (pFile = fopen( pNameWin, "r" )) )
+        pMvsisName = pNameWin;
+    else if ( (pFile = fopen( pNameUnix, "r" )) )
+        pMvsisName = pNameUnix;
    else if ( pFile == NULL )
    {
-        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", "mvsis.exe", "mvsis" );
+        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pNameWin, pNameUnix );
        goto usage;
    }
    fclose( pFile );

-    if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);

    // write out the current network
-    Io_WriteBlifLogic( pNtk, "_mvsis_in.blif", 1 );
+    pNetlist = Abc_NtkLogicToNetlist(pNtk);
+    Io_WriteBlif( pNetlist, "_mvsis_in.blif", 1 );
+    Abc_NtkDelete( pNetlist );

    // create the file for MVSIS
    sprintf( Command, "%s -x -c ", pMvsisName );
--- a/src/base/cmd/cmdAlias.c
+++ b/src/base/cmd/cmdAlias.c
@ -68,7 +68,7 @@ void CmdCommandAliasAdd( Abc_Frame_t * pAbc, char * sName, int argc, char ** arg
 void CmdCommandAliasPrint( Abc_Frame_t * pAbc, Abc_Alias * pAlias )
 {
    int i;
-    fprintf(pAbc->Out, "%s\t", pAlias->sName);
+    fprintf(pAbc->Out, "%-15s", pAlias->sName);
    for(i = 0; i < pAlias->argc; i++) 
        fprintf( pAbc->Out, " %s", pAlias->argv[i] );
    fprintf( pAbc->Out, "\n" );
--- a/src/base/cmd/cmdFlag.c
+++ b/src/base/cmd/cmdFlag.c
@ -43,14 +43,10 @@
 ******************************************************************************/
 char * Cmd_FlagReadByName( Abc_Frame_t * pAbc, char * flag )
 {
-  char *value;
-
-  if (st_lookup(pAbc->tFlags, flag, &value)) {
-    return value;
-  }
-  else {
-    return NIL(char);
-  }
+    char * value;
+    if ( st_lookup(pAbc->tFlags, flag, &value) )
+        return value;
+    return NULL;
 }


@ -65,19 +61,17 @@ char * Cmd_FlagReadByName( Abc_Frame_t * pAbc, char * flag )
 ******************************************************************************/
 void Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * value )
 {
-  char *oldValue, *newValue;
-
-  if (!key)
-    return;
-  if (value)
-    newValue = util_strsav(value);
-  else
-    newValue = util_strsav("");
-
-  if (st_delete(pAbc->tFlags, &key, &oldValue))
-    FREE(oldValue);
-
-  st_insert(pAbc->tFlags, key, newValue);
+    char * oldValue, * newValue;
+    if ( !key )
+        return;
+    if ( value )
+        newValue = util_strsav(value);
+    else
+        newValue = util_strsav("");
+//        newValue = NULL;
+    if ( st_delete(pAbc->tFlags, &key, &oldValue) )
+        FREE(oldValue);
+    st_insert( pAbc->tFlags, key, newValue );
 }


@ -92,15 +86,14 @@ void Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * value )
 ******************************************************************************/
 void Cmd_FlagDeleteByName( Abc_Frame_t * pAbc, char * key )
 {
-  char *value;
-
-  if (!key)
-    return;
-
-  if (st_delete(pAbc->tFlags, &key, &value)) {
-    FREE(key);
-    FREE(value);
-  }
+    char *value;
+    if ( !key )
+        return;
+    if ( st_delete( pAbc->tFlags, &key, &value ) ) 
+    {
+        FREE(key);
+        FREE(value);
+    }
 }


--- a/src/base/cmd/cmdInt.h
+++ b/src/base/cmd/cmdInt.h
@ -73,6 +73,7 @@ extern FILE *     CmdFileOpen( Abc_Frame_t * pAbc, char * sFileName, char * sMod
 extern void       CmdFreeArgv( int argc, char ** argv );
 extern void       CmdCommandFree( Abc_Command * pCommand );
 extern void       CmdCommandPrint( Abc_Frame_t * pAbc, bool fPrintAll );
+extern void       CmdPrintTable( st_table * tTable, int fAliases );

 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
--- a/src/base/cmd/cmdUtils.c
+++ b/src/base/cmd/cmdUtils.c
@ -110,7 +110,7 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
    // get the backup network if the command is going to change the network
    if ( pCommand->fChange ) 
    {
-        if ( pAbc->pNtkCur )
+        if ( pAbc->pNtkCur && Abc_FrameIsFlagEnabled( "backup" ) )
        {
            pNetCopy = Abc_NtkDup( pAbc->pNtkCur );
            Abc_FrameSetCurrentNetwork( pAbc, pNetCopy );
@ -122,15 +122,10 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )

    // execute the command
    clk = util_cpu_time();
-    pFunc = ( int (*)( Abc_Frame_t *, int, char ** ) ) pCommand->pFunc;
+    pFunc = (int (*)(Abc_Frame_t *, int, char **))pCommand->pFunc;
    fError = (*pFunc)( pAbc, argc, argv );
    pAbc->TimeCommand += (util_cpu_time() - clk);

-//    if ( !fError && pCommand->fChange && pAbc->pNtkCur ) 
-//    {
-//    Cmd_HistoryAddSnapshot(pAbc, pAbc->pNet);
-//    }
-
    // automatic execution of arbitrary command after each command 
    // usually this is a passive command ... 
    if ( fError == 0 && !pAbc->fAutoexac )
@ -592,6 +587,62 @@ int CmdCommandPrintCompare( Abc_Command ** ppC1, Abc_Command ** ppC2 )
    assert( 0 );
    return 0;
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    [Comparision function used for sorting commands.]
+
+  Description []
+                
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CmdNamePrintCompare( char ** ppC1, char ** ppC2 )
+{
+    return strcmp( *ppC1, *ppC2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparision function used for sorting commands.]
+
+  Description []
+                
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CmdPrintTable( st_table * tTable, int fAliases )
+{
+    st_generator * gen;
+    char ** ppNames;
+    char * key, * value;
+    int nNames, i;
+
+    // collect keys in the array
+    ppNames = ALLOC( char *, st_count(tTable) );
+    nNames = 0;
+    st_foreach_item( tTable, gen, &key, &value )
+        ppNames[nNames++] = key;
+
+    // sort array by name
+    qsort( (void *)ppNames, nNames, sizeof(char *), 
+        (int (*)(const void *, const void *))CmdNamePrintCompare );
+
+    // print in this order
+    for ( i = 0; i < nNames; i++ )
+    {
+        st_lookup( tTable, ppNames[i], &value );
+        if ( fAliases )
+            CmdCommandAliasPrint( Abc_FrameGetGlobalFrame(), (Abc_Alias *)value );
+        else
+            fprintf( stdout, "%-15s %-15s\n", ppNames[i], value );
+    }
+    free( ppNames );
+}

 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@ -58,7 +58,7 @@ Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck )
        return NULL;

    // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadBench: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@ -109,7 +109,7 @@ Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck )
    Io_ReadBlifFree( p );

    // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadBlif: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@ -58,7 +58,7 @@ Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck )
        return NULL;

    // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadEdif: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
--- a/src/base/io/ioReadEqn.c
+++ b/src/base/io/ioReadEqn.c
@ -61,7 +61,7 @@ Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck )
        return NULL;

    // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadEqn: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@ -58,7 +58,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
        return NULL;

    // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadPla: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@ -150,7 +150,7 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
        return NULL;

    // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "Io_ReadVerilog: The network check has failed.\n" );
        Abc_NtkDelete( pNtk );
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@ -231,29 +231,22 @@ usage:

  Synopsis    [Returns 1 if s is a file type recognized, else returns 0.]

-  Description [Returns 1 if s is a file type recognized by VIS, else returns
-  0. Recognized types are "blif", "blif_mv", "blif_mvs", and "none".]
+  Description [Returns 1 if s is a file type recognized by ABC, else returns 0. 
+  Recognized types are "blif", "bench", "pla", and "none".]

  SideEffects []

 ******************************************************************************/
-static int
-TypeCheck(
-    Abc_Frame_t * pAbc,
-    char       * s)
+static int TypeCheck( Abc_Frame_t * pAbc, char * s )
 {
-    if (strcmp(s, "blif") == 0) {
+    if (strcmp(s, "blif") == 0)
        return 1;
-    }
-    else if (strcmp(s, "blif_mv") == 0) {
+    else if (strcmp(s, "bench") == 0)
        return 1;
-    }
-    else if (strcmp(s, "blif_mvs") == 0) {
+    else if (strcmp(s, "pla") == 0)
        return 1;
-    }
-    else if (strcmp(s, "none") == 0) {
+    else if (strcmp(s, "none") == 0)
        return 1;
-    }
    else {
        fprintf( pAbc->Err, "unknown type %s\n", s );
        return 0;
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@ -90,21 +90,22 @@ extern void            Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
 extern void               Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
 extern Abc_Frame_t *   Abc_FrameGetGlobalFrame();

-extern Abc_Ntk_t *     Abc_FrameReadNtkStore       ( Abc_Frame_t * pFrame );
-extern int             Abc_FrameReadNtkStoreSize   ( Abc_Frame_t * pFrame );
-extern void            Abc_FrameSetNtkStore        ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk );
-extern void            Abc_FrameSetNtkStoreSize    ( Abc_Frame_t * pFrame, int nStored  );
-
-extern void *          Abc_FrameReadLibLut         ( Abc_Frame_t * pFrame );
-extern void *          Abc_FrameReadLibGen         ( Abc_Frame_t * pFrame );
-extern void *          Abc_FrameReadLibSuper       ( Abc_Frame_t * pFrame );
-extern void            Abc_FrameSetLibLut          ( Abc_Frame_t * pFrame, void * pLib );
-extern void            Abc_FrameSetLibGen          ( Abc_Frame_t * pFrame, void * pLib );
-extern void            Abc_FrameSetLibSuper        ( Abc_Frame_t * pFrame, void * pLib );
-
-extern void *          Abc_FrameReadManDd          ( Abc_Frame_t * pFrame );
-extern void *          Abc_FrameReadManDec         ( Abc_Frame_t * pFrame );
+extern Abc_Ntk_t *     Abc_FrameReadNtkStore();                  
+extern int             Abc_FrameReadNtkStoreSize();              
+extern void *          Abc_FrameReadLibLut();                    
+extern void *          Abc_FrameReadLibGen();                    
+extern void *          Abc_FrameReadLibSuper();                  
+extern void *          Abc_FrameReadManDd();                     
+extern void *          Abc_FrameReadManDec();                    
+extern char *          Abc_FrameReadFlag( char * pFlag ); 
+extern bool            Abc_FrameIsFlagEnabled( char * pFlag );

+extern void            Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); 
+extern void            Abc_FrameSetNtkStoreSize( int nStored );  
+extern void            Abc_FrameSetLibLut( void * pLib );        
+extern void            Abc_FrameSetLibGen( void * pLib );        
+extern void            Abc_FrameSetLibSuper( void * pLib );      
+extern void            Abc_FrameSetFlag( char * pFlag, char * pValue );

 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@ -26,12 +26,63 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////

-static Abc_Frame_t * Abc_FrameGlobalFrame = 0;
+static Abc_Frame_t * s_GlobalFrame = NULL;

 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////

+/**Function*************************************************************
+
+  Synopsis    [APIs to access parameters in the flobal frame.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_FrameReadNtkStore()                  { return s_GlobalFrame->pStored;      } 
+int         Abc_FrameReadNtkStoreSize()              { return s_GlobalFrame->nStored;      }
+void *      Abc_FrameReadLibLut()                    { return s_GlobalFrame->pLibLut;      } 
+void *      Abc_FrameReadLibGen()                    { return s_GlobalFrame->pLibGen;      } 
+void *      Abc_FrameReadLibSuper()                  { return s_GlobalFrame->pLibSuper;    } 
+void *      Abc_FrameReadManDd()                     { return s_GlobalFrame->dd;           } 
+void *      Abc_FrameReadManDec()                    { return s_GlobalFrame->pManDec;      } 
+char *      Abc_FrameReadFlag( char * pFlag )        { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );  } 
+
+void        Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ) { s_GlobalFrame->pStored  = pNtk;     } 
+void        Abc_FrameSetNtkStoreSize( int nStored )  { s_GlobalFrame->nStored  = nStored;  }
+void        Abc_FrameSetLibLut( void * pLib )        { s_GlobalFrame->pLibLut   = pLib;    } 
+void        Abc_FrameSetLibGen( void * pLib )        { s_GlobalFrame->pLibGen   = pLib;    } 
+void        Abc_FrameSetLibSuper( void * pLib )      { s_GlobalFrame->pLibSuper = pLib;    } 
+void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue );  } 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the flag is enabled without value or with value 1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_FrameIsFlagEnabled( char * pFlag )
+{
+    char * pValue;
+    // if flag is not defined, it is not enabled
+    pValue = Abc_FrameReadFlag( pFlag );
+    if ( pValue == NULL )
+        return 0;
+    // if flag is defined but value is not empty (no parameter) or "1", it is not enabled
+    if ( strcmp(pValue, "") && strcmp(pValue, "1") )
+        return 0;
+    return 1;
+}
+
 /**Function*************************************************************

  Synopsis    []
@ -311,7 +362,7 @@ void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk )
        return;

    // transfer the parameters to the new network
-    if ( p->pNtkCur )
+    if ( p->pNtkCur && Abc_FrameIsFlagEnabled( "backup" ) )
    {
        Abc_NtkSetBackup( pNtk, Abc_NtkBackup(p->pNtkCur) );
        Abc_NtkSetStep( pNtk, Abc_NtkStep(p->pNtkCur) );
@ -322,6 +373,9 @@ void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk )
    {
        Abc_NtkSetBackup( pNtk, NULL );
        Abc_NtkSetStep( pNtk, ++p->nSteps );
+        // delete the current network if present but backup is disabled
+        if ( p->pNtkCur )
+            Abc_NtkDelete( p->pNtkCur );
    }
    // set the new current network
    p->pNtkCur = pNtk;
@ -385,7 +439,7 @@ void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p )
 ***********************************************************************/
 void Abc_FrameSetGlobalFrame( Abc_Frame_t * p )
 {
-    Abc_FrameGlobalFrame = p;
+    s_GlobalFrame = p;
 }

 /**Function*************************************************************
@ -401,43 +455,17 @@ void Abc_FrameSetGlobalFrame( Abc_Frame_t * p )
 ***********************************************************************/
 Abc_Frame_t * Abc_FrameGetGlobalFrame()
 {
-    if ( Abc_FrameGlobalFrame == 0 )
+    if ( s_GlobalFrame == 0 )
    {
        // start the framework
-        Abc_FrameGlobalFrame = Abc_FrameAllocate();
+        s_GlobalFrame = Abc_FrameAllocate();
        // perform initializations
-        Abc_FrameInit( Abc_FrameGlobalFrame );
+        Abc_FrameInit( s_GlobalFrame );
    }
-    return Abc_FrameGlobalFrame;
+    return s_GlobalFrame;
 }


-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_FrameReadNtkStore       ( Abc_Frame_t * pFrame )                     { return pFrame->pStored;    } 
-int         Abc_FrameReadNtkStoreSize   ( Abc_Frame_t * pFrame )                     { return pFrame->nStored;    }
-void        Abc_FrameSetNtkStore        ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk )   { pFrame->pStored  = pNtk;   } 
-void        Abc_FrameSetNtkStoreSize    ( Abc_Frame_t * pFrame, int nStored )        { pFrame->nStored  = nStored;}
-
-void *      Abc_FrameReadLibLut         ( Abc_Frame_t * pFrame )                     { return pFrame->pLibLut;    } 
-void *      Abc_FrameReadLibGen         ( Abc_Frame_t * pFrame )                     { return pFrame->pLibGen;    } 
-void *      Abc_FrameReadLibSuper       ( Abc_Frame_t * pFrame )                     { return pFrame->pLibSuper;  } 
-void        Abc_FrameSetLibLut          ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibLut   = pLib;  } 
-void        Abc_FrameSetLibGen          ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibGen   = pLib;  } 
-void        Abc_FrameSetLibSuper        ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibSuper = pLib;  } 
-
-void *      Abc_FrameReadManDd          ( Abc_Frame_t * pFrame )                     { return pFrame->dd;         } 
-void *      Abc_FrameReadManDec         ( Abc_Frame_t * pFrame )                     { return pFrame->pManDec;    } 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@ -32,7 +32,7 @@
 ////////////////////////////////////////////////////////////////////////

 // the current version
-#define ABC_VERSION "UC Berkeley, ABC 1.0"
+#define ABC_VERSION "UC Berkeley, ABC 1.01"

 // the maximum length of an input line 
 #define MAX_STR     32768
@ -53,8 +53,8 @@ struct Abc_Frame_t_
    // the functionality
    Abc_Ntk_t *     pNtkCur;     // the current network
    int             nSteps;      // the counter of different network processed
-    // when this flag is 1, the current command is executed in autoexec mode
-    int             fAutoexac;  
+    int             fAutoexac;   // marks the autoexec mode
+    int                fBatchMode;     // are we invoked in batch mode?
    // output streams
    FILE *          Out;
    FILE *          Err;
@ -62,14 +62,13 @@ struct Abc_Frame_t_
    // used for runtime measurement
    int             TimeCommand; // the runtime of the last command
    int             TimeTotal;   // the total runtime of all commands
-    int                fBatchMode;     // are we invoked in batch mode?
    // temporary storage for structural choices
    Abc_Ntk_t *     pStored;     // the stored networks
    int             nStored;     // the number of stored networks
    // decomposition package
-    DdManager *     dd;          // temporary BDD package
    void *          pManDec;     // decomposition manager
-
+    DdManager *     dd;          // temporary BDD package
+    // libraries for mapping
    void *          pLibLut;     // the current LUT library
    void *          pLibGen;     // the current genlib
    void *          pLibSuper;   // the current supergate library
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@ -161,8 +161,14 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc )
    Cmd_CommandExecute( pAbc, "source -s abc.rc" );
    }
 #endif //WIN32
-
-    return;
+    {
+        // reset command history
+        char * pName; 
+        int i;
+        Vec_PtrForEachEntry( pAbc->aHistory, pName, i )
+            free( pName );
+        pAbc->aHistory->nSize = 0;
+    }
 }

 /**Function********************************************************************
--- a/src/map/fpga/fpga.c
+++ b/src/map/fpga/fpga.c
@ -56,9 +56,9 @@ static int Fpga_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
 void Fpga_Init( Abc_Frame_t * pAbc )
 {
    // set the default library
-    //Fpga_LutLib_t    s_LutLib = { "lutlib", 6, {0,1,2,4,8,16,32}, {0,1,2,3,4,5,6} };
-    Fpga_LutLib_t    s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
-    Abc_FrameSetLibLut( pAbc, Fpga_LutLibDup(&s_LutLib) );
+    //Fpga_LutLib_t s_LutLib = { "lutlib", 6, {0,1,2,4,8,16,32}, {0,1,2,3,4,5,6} };
+    Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
+    Abc_FrameSetLibLut( Fpga_LutLibDup(&s_LutLib) );

    Cmd_CommandAdd( pAbc, "FPGA mapping", "read_lut",   Fpga_CommandReadLibrary,   0 ); 
    Cmd_CommandAdd( pAbc, "FPGA mapping", "print_lut",  Fpga_CommandPrintLibrary,  0 ); 
@ -150,8 +150,8 @@ int Fpga_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
        goto usage;
    }
    // replace the current library
-    Fpga_LutLibFree( Abc_FrameReadLibLut(Abc_FrameGetGlobalFrame()) );
-    Abc_FrameSetLibLut( Abc_FrameGetGlobalFrame(), pLib );
+    Fpga_LutLibFree( Abc_FrameReadLibLut() );
+    Abc_FrameSetLibLut( pLib );
    return 0;

 usage:
--- a/src/map/fpga/fpgaCore.c
+++ b/src/map/fpga/fpgaCore.c
@ -97,7 +97,7 @@ int Fpga_Mapping( Fpga_Man_t * p )
 ***********************************************************************/
 int Fpga_MappingPostProcess( Fpga_Man_t * p )
 {
-    int fShowSwitching    = 0;
+    int fShowSwitching    = 1;
    int fRecoverAreaFlow  = 1;
    int fRecoverArea      = 1;
    float aAreaTotalCur, aAreaTotalCur2;
--- a/src/map/fpga/fpgaSwitch.c
+++ b/src/map/fpga/fpgaSwitch.c
@ -22,8 +22,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////

-static float Fpga_CutGetSwitching( Fpga_Cut_t * pCut );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@ -64,10 +62,10 @@ float Fpga_CutRefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pC
    Fpga_Node_t * pNodeChild;
    float aArea;
    int i;
-    if ( pCut->nLeaves == 1 )
-        return 0;
    // start the area of this cut
-    aArea = Fpga_CutGetSwitching( pCut );
+    aArea = pNode->Switching;
+    if ( pCut->nLeaves == 1 )
+        return aArea;
    // go through the children
    for ( i = 0; i < pCut->nLeaves; i++ )
    {
@ -96,10 +94,10 @@ float Fpga_CutDerefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t *
    Fpga_Node_t * pNodeChild;
    float aArea;
    int i;
-    if ( pCut->nLeaves == 1 )
-        return 0;
    // start the area of this cut
-    aArea = Fpga_CutGetSwitching( pCut );
+    aArea = pNode->Switching;
+    if ( pCut->nLeaves == 1 )
+        return aArea;
    // go through the children
    for ( i = 0; i < pCut->nLeaves; i++ )
    {
@ -112,27 +110,6 @@ float Fpga_CutDerefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t *
    return aArea;
 }

-/**function*************************************************************
-
-  synopsis    [Computes the exact area associated with the cut.]
-
-  description []
-               
-  sideeffects []
-
-  seealso     []
-
-***********************************************************************/
-float Fpga_CutGetSwitching( Fpga_Cut_t * pCut )
-{
-    float Result;
-    int i;
-    Result = 0.0;
-    for ( i = 0; i < pCut->nLeaves; i++ )
-        Result += pCut->ppLeaves[i]->Switching;
-    return Result;
-}
-
 /**Function*************************************************************

  Synopsis    [Computes the array of mapping.]
@ -153,10 +130,8 @@ float Fpga_MappingGetSwitching( Fpga_Man_t * pMan, Fpga_NodeVec_t * vMapping )
    for ( i = 0; i < vMapping->nSize; i++ )
    {
        pNode = vMapping->pArray[i];
-        if ( !Fpga_NodeIsAnd(pNode) )
-            continue;
        // at least one phase has the best cut assigned
-        assert( pNode->pCutBest != NULL );
+        assert( !Fpga_NodeIsAnd(pNode) || pNode->pCutBest != NULL );
        // at least one phase is used in the mapping
        assert( pNode->nRefs > 0 );
        // compute the array due to the supergate
--- a/src/map/fpga/fpgaUtils.c
+++ b/src/map/fpga/fpgaUtils.c
@ -314,7 +314,7 @@ float Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan )

    // reconnect the nodes in reverse topological order
    pMan->vMapping->nSize = 0;
-    for ( i = LevelMax; i > 0; i-- )
+    for ( i = LevelMax; i >= 0; i-- )
        for ( pNode = ppStore[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 )
            Fpga_NodeVecPush( pMan->vMapping, pNode );
    free( ppStore );
--- a/src/map/mapper/mapper.c
+++ b/src/map/mapper/mapper.c
@ -149,13 +149,13 @@ int Map_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
    // replace the current library
 //    Map_SuperLibFree( s_pSuperLib );
 //    s_pSuperLib = pLib;
-    Map_SuperLibFree( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) );
-    Abc_FrameSetLibSuper( Abc_FrameGetGlobalFrame(), pLib );
+    Map_SuperLibFree( Abc_FrameReadLibSuper() );
+    Abc_FrameSetLibSuper( pLib );
    // replace the current genlib library
 //    if ( s_pLib ) Mio_LibraryDelete( s_pLib );
 //    s_pLib = s_pSuperLib->pGenlib;
-    Mio_LibraryDelete( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
-    Abc_FrameSetLibGen( Abc_FrameGetGlobalFrame(), pLib->pGenlib );
+    Mio_LibraryDelete( Abc_FrameReadLibGen() );
+    Abc_FrameSetLibGen( pLib->pGenlib );
    return 0;

 usage:
--- a/src/map/mapper/mapperLib.c
+++ b/src/map/mapper/mapperLib.c
@ -139,15 +139,9 @@ void Map_SuperLibFree( Map_SuperLib_t * p )
    if ( p == NULL ) return;
    if ( p->pGenlib )
    {
-//        if ( s_pLib == p->pGenlib )
-//            s_pLib = NULL;
-//        if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == p->pGenlib )
-//            Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL);
-//        Mio_LibraryDelete( p->pGenlib );
-
-        assert( p->pGenlib == Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+        assert( p->pGenlib == Abc_FrameReadLibGen() );
        Mio_LibraryDelete( p->pGenlib );
-        Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL);
+        Abc_FrameSetLibGen( NULL );
    }
    if ( p->tTableC )
        Map_SuperTableFree( p->tTableC );
--- a/src/map/mapper/mapperRefs.c
+++ b/src/map/mapper/mapperRefs.c
@ -542,7 +542,7 @@ float Map_MappingGetArea( Map_Man_t * pMan, Map_NodeVec_t * vMapping )
             (pNode->pCutBest[1] == NULL && pNode->nRefAct[1] > 0) )
            Area += pMan->pSuperLib->AreaInv;
    }
-    // add buffer for each CO driven by a CI
+    // add buffers for each CO driven by a CI
    for ( i = 0; i < pMan->nOutputs; i++ )
        if ( Map_NodeIsVar(pMan->pOutputs[i]) && !Map_IsComplement(pMan->pOutputs[i]) )
            Area += pMan->pSuperLib->AreaBuf;
--- a/src/map/mapper/mapperSwitch.c
+++ b/src/map/mapper/mapperSwitch.c
@ -23,7 +23,6 @@
 ////////////////////////////////////////////////////////////////////////

 static float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, int fReference );
-static float Map_CutGetSwitching( Map_Cut_t * pCut );

 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@ -100,11 +99,13 @@ float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, i
    Map_Cut_t * pCutChild;
    float aSwitchActivity;
    int i, fPhaseChild;
+
+    // start switching activity for the node
+    aSwitchActivity = pNode->Switching;
    // consider the elementary variable
    if ( pCut->nLeaves == 1 )
-        return 0;
-    // start the area of this cut
-    aSwitchActivity = Map_CutGetSwitching( pCut );
+        return aSwitchActivity;
+
    // go through the children
    assert( pCut->M[fPhase].pSuperBest );
    for ( i = 0; i < pCut->nLeaves; i++ )
@ -127,7 +128,7 @@ float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, i
                // inverter should be added if the phase
                // (a) has no reference and (b) is implemented using other phase
                if ( pNodeChild->nRefAct[fPhaseChild]++ == 0 && pNodeChild->pCutBest[fPhaseChild] == NULL )
-                    aSwitchActivity += pNodeChild->Switching;
+                    aSwitchActivity += pNodeChild->Switching; // inverter switches the same as the node
                // if the node is referenced, there is no recursive call
                if ( pNodeChild->nRefAct[2]++ > 0 )
                    continue;
@ -147,7 +148,7 @@ float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, i
                // inverter should be added if the phase
                // (a) has no reference and (b) is implemented using other phase
                if ( --pNodeChild->nRefAct[fPhaseChild] == 0 && pNodeChild->pCutBest[fPhaseChild] == NULL )
-                    aSwitchActivity += pNodeChild->Switching;
+                    aSwitchActivity += pNodeChild->Switching; // inverter switches the same as the node
                // if the node is referenced, there is no recursive call
                if ( --pNodeChild->nRefAct[2] > 0 )
                    continue;
@ -169,27 +170,6 @@ float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, i
    return aSwitchActivity;
 }

-/**function*************************************************************
-
-  synopsis    [Computes the exact area associated with the cut.]
-
-  description []
-               
-  sideeffects []
-
-  seealso     []
-
-***********************************************************************/
-float Map_CutGetSwitching( Map_Cut_t * pCut )
-{
-    float Result;
-    int i;
-    Result = 0.0;
-    for ( i = 0; i < pCut->nLeaves; i++ )
-        Result += pCut->ppLeaves[i]->Switching;
-    return Result;
-}
-
 /**Function*************************************************************

  Synopsis    [Computes the array of mapping.]
@ -227,9 +207,9 @@ float Map_MappingGetSwitching( Map_Man_t * pMan, Map_NodeVec_t * vMapping )
        // count switching of the interver if we need to implement one phase with another phase
        if ( (pNode->pCutBest[0] == NULL && pNode->nRefAct[0] > 0) || 
             (pNode->pCutBest[1] == NULL && pNode->nRefAct[1] > 0) )
-            Switch += pNode->Switching;
+            Switch += pNode->Switching; // inverter switches the same as the node
    }
-    // add buffer for each CO driven by a CI
+    // add buffers for each CO driven by a CI
    for ( i = 0; i < pMan->nOutputs; i++ )
        if ( Map_NodeIsVar(pMan->pOutputs[i]) && !Map_IsComplement(pMan->pOutputs[i]) )
            Switch += pMan->pOutputs[i]->Switching;
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@ -83,7 +83,7 @@ void Mio_Init( Abc_Frame_t * pAbc )
    fclose( pFile );
    // read genlib from file
    pLibGen = Mio_LibraryRead( pAbc, pFileTemp, NULL, 0 );
-    Abc_FrameSetLibGen( pAbc, pLibGen );
+    Abc_FrameSetLibGen( pLibGen );
 #ifdef WIN32
        _unlink( pFileTemp );
 #else
@ -186,15 +186,15 @@ int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
        extern void Map_SuperLibFree( Map_SuperLib_t * p );
 //        Map_SuperLibFree( s_pSuperLib );
 //        s_pSuperLib = NULL;
-        Map_SuperLibFree( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) );
-        Abc_FrameSetLibSuper(Abc_FrameGetGlobalFrame(), NULL);
+        Map_SuperLibFree( Abc_FrameReadLibSuper() );
+        Abc_FrameSetLibSuper( NULL );
    }

    // replace the current library
 //    Mio_LibraryDelete( s_pLib );
 //    s_pLib = pLib;
-    Mio_LibraryDelete( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
-    Abc_FrameSetLibGen( Abc_FrameGetGlobalFrame(), pLib );
+    Mio_LibraryDelete( Abc_FrameReadLibGen() );
+    Abc_FrameSetLibGen( pLib );
    return 0;

 usage:
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@ -185,6 +185,8 @@ extern void         Extra_BitMatrixDelete2( Extra_BitMat_t * p, int i, int k );
 extern void         Extra_BitMatrixOr( Extra_BitMat_t * p, int i, unsigned * pInfo );
 extern void         Extra_BitMatrixOrTwo( Extra_BitMat_t * p, int i, int j );
 extern int          Extra_BitMatrixCountOnesUpper( Extra_BitMat_t * p );
+extern int          Extra_BitMatrixIsDisjoint( Extra_BitMat_t * p1, Extra_BitMat_t * p2 );
+extern int          Extra_BitMatrixIsClique( Extra_BitMat_t * p );

 /*=== extraUtilFile.c ========================================================*/

--- a/src/misc/extra/extraUtilBitMatrix.c
+++ b/src/misc/extra/extraUtilBitMatrix.c
@ -28,14 +28,14 @@

 struct Extra_BitMat_t_
 {
-    unsigned ** ppData;
-    int         nSize;
-    int         nWords;
-    int         nBitShift;
-    unsigned    uMask;
-    int         nLookups;
-    int         nInserts;
-    int         nDeletes;
+    unsigned ** ppData;      // bit data
+    int         nSize;       // the number of bits in one dimension
+    int         nWords;      // the number of words in one dimension
+    int         nBitShift;   // the number of bits to shift to get words
+    unsigned    uMask;       // the mask to get the number of bits in the word
+    int         nLookups;    // the number of lookups  
+    int         nInserts;    // the number of inserts
+    int         nDeletes;    // the number of deletions
 };

 /*---------------------------------------------------------------------------*/
@ -352,6 +352,62 @@ int Extra_BitMatrixCountOnesUpper( Extra_BitMat_t * p )
    return nTotal;
 }

+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the matrices have no entries in common.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_BitMatrixIsDisjoint( Extra_BitMat_t * p1, Extra_BitMat_t * p2 )
+{
+    int i, w;
+    assert( p1->nSize == p2->nSize );
+    for ( i = 0; i < p1->nSize; i++ )
+        for ( w = 0; w < p1->nWords; w++ )
+            if ( p1->ppData[i][w] & p2->ppData[i][w] )
+                return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the matrix is a set of cliques.]
+
+  Description [For example pairwise symmetry info should satisfy this property.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_BitMatrixIsClique( Extra_BitMat_t * pMat )
+{
+    int v, u, i;
+    for ( v = 0; v < pMat->nSize; v++ )
+    for ( u = v+1; u < pMat->nSize; u++ )
+    {
+        if ( !Extra_BitMatrixLookup1( pMat, v, u ) )
+            continue;
+        // v and u are symmetric
+        for ( i = 0; i < pMat->nSize; i++ )
+        {
+            if ( i == v || i == u )
+                continue;
+            // i is neither v nor u
+            // the symmetry status of i is the same w.r.t. to v and u
+            if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) )
+                return 0;
+        }
+    }
+    return 1;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@ -78,13 +78,13 @@ clk = clock();
    if ( fPrecompute )
    {   // precompute subgraphs
        Rwr_ManPrecompute( p );
+//        Rwr_ManPrint( p );
        Rwr_ManWriteToArray( p );
-        Rwr_ManPrint( p );
    }
    else
    {   // load saved subgraphs
        Rwr_ManLoadFromArray( p, 0 );
-        Rwr_ManPrint( p );
+//        Rwr_ManPrint( p );
        Rwr_ManPreprocess( p );
    }
 p->timeStart = clock() - clk;
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@ -21,6 +21,12 @@
 #ifndef __SIM_H__
 #define __SIM_H__

+/*
+    The ideas realized in this package are described in the paper:
+    "Detecting Symmetries in Boolean Functions using Circuit Representation, 
+    Simulation, and Satisfiability".
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@ -45,7 +51,8 @@ struct Sym_Man_t_
    int               nSimWords;     // the number of bits in simulation info
    Vec_Ptr_t *       vSim;          // simulation info
    // support information
-    Vec_Ptr_t *       vSuppFun;      // functional supports
+    Vec_Ptr_t *       vSuppFun;      // bit representation
+    Vec_Vec_t *       vSupports;     // integer representation
    // symmetry info for each output
    Vec_Ptr_t *       vMatrSymms;    // symmetric pairs
    Vec_Ptr_t *       vMatrNonSymms; // non-symmetric pairs
@ -56,6 +63,14 @@ struct Sym_Man_t_
    unsigned *        uPatRand;
    unsigned *        uPatCol;
    unsigned *        uPatRow;
+    // temporary
+    Vec_Int_t *       vVarsU;
+    Vec_Int_t *       vVarsV;
+    int               iOutput;
+    int               iVar1;
+    int               iVar2;
+    int               iVar1Old;
+    int               iVar2Old;
    // internal data structures
    int               nSatRuns;
    int               nSatRunsSat;
@ -64,8 +79,12 @@ struct Sym_Man_t_
    int               nPairsSymm;
    int               nPairsSymmStr;
    int               nPairsNonSymm;
+    int               nPairsRem;
    int               nPairsTotal;
    // runtime statistics
+    int               timeStruct;
+    int               timeCount;
+    int               timeMatr;
    int               timeSim;
    int               timeFraig;
    int               timeSat;
@ -91,6 +110,7 @@ struct Sim_Man_t_
    Vec_Ptr_t *       vSuppFun;      // functional supports
    // simulation targets
    Vec_Vec_t *       vSuppTargs;    // support targets
+    int               iInput;        // the input current processed
    // internal data structures
    Extra_MmFixed_t * pMmPat;   
    Vec_Ptr_t *       vFifo;
@ -148,7 +168,7 @@ struct Sim_Pat_t_
 ////////////////////////////////////////////////////////////////////////

 /*=== simMan.c ==========================================================*/
-extern Sym_Man_t *     Sym_ManStart( Abc_Ntk_t * pNtk );
+extern Sym_Man_t *     Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose );
 extern void            Sym_ManStop( Sym_Man_t * p );
 extern void            Sym_ManPrintStats( Sym_Man_t * p );
 extern Sim_Man_t *     Sim_ManStart( Abc_Ntk_t * pNtk );
@ -158,11 +178,13 @@ extern Sim_Pat_t *     Sim_ManPatAlloc( Sim_Man_t * p );
 extern void            Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat );
 /*=== simSupp.c ==========================================================*/
 extern Vec_Ptr_t *     Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *     Sim_ComputeFunSupp( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *     Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== simSym.c ==========================================================*/
-extern int             Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk );
+extern int             Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== simSymSat.c ==========================================================*/
+extern int             Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern );
 /*=== simSymStr.c ==========================================================*/
-extern void            Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs );
+extern void            Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun );
 /*=== simSymSim.c ==========================================================*/
 extern void            Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPatRand, Vec_Ptr_t * vMatrsNonSym );
 /*=== simUtil.c ==========================================================*/
@ -180,7 +202,8 @@ extern int             Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
 extern int             Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
 extern void            Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords );
 extern int             Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
-extern int             Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters );
+extern void            Sim_UtilCountPairsAll( Sym_Man_t * p );
+extern int             Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );

 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
--- a/src/opt/sim/simMan.c
+++ b/src/opt/sim/simMan.c
@ -40,10 +40,10 @@
  SeeAlso     []

 ***********************************************************************/
-Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk )
+Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
 {
    Sym_Man_t * p;
-    int i;
+    int i, v; 
    // start the manager
    p = ALLOC( Sym_Man_t, 1 );
    memset( p, 0, sizeof(Sym_Man_t) );
@ -69,8 +69,15 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk )
    p->uPatRand = ALLOC( unsigned, p->nSimWords );
    p->uPatCol  = ALLOC( unsigned, p->nSimWords );
    p->uPatRow  = ALLOC( unsigned, p->nSimWords );
+    p->vVarsU   = Vec_IntStart( 100 );
+    p->vVarsV   = Vec_IntStart( 100 );
    // compute supports
-    p->vSuppFun = Sim_ComputeFunSupp( pNtk );
+    p->vSuppFun  = Sim_ComputeFunSupp( pNtk, fVerbose );
+    p->vSupports = Vec_VecStart( p->nOutputs );
+    for ( i = 0; i < p->nOutputs; i++ )
+        for ( v = 0; v < p->nInputs; v++ )
+            if ( Sim_SuppFunHasVar( p->vSuppFun, i, v ) )
+                Vec_VecPush( p->vSupports, i, (void *)v );
    return p;
 }

@ -92,11 +99,14 @@ void Sym_ManStop( Sym_Man_t * p )
    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );   
    if ( p->vSim )         Sim_UtilInfoFree( p->vSim );   
    if ( p->vNodes )       Vec_PtrFree( p->vNodes );
+    if ( p->vSupports )    Vec_VecFree( p->vSupports );
    for ( i = 0; i < p->nOutputs; i++ )
    {
        Extra_BitMatrixStop( p->vMatrSymms->pArray[i] );
        Extra_BitMatrixStop( p->vMatrNonSymms->pArray[i] );
    }
+    Vec_IntFree( p->vVarsU );
+    Vec_IntFree( p->vVarsV );
    Vec_PtrFree( p->vMatrSymms );
    Vec_PtrFree( p->vMatrNonSymms );
    Vec_IntFree( p->vPairsTotal );
@ -121,17 +131,18 @@ void Sym_ManStop( Sym_Man_t * p )
 ***********************************************************************/
 void Sym_ManPrintStats( Sym_Man_t * p )
 {
-    printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", 
-        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
-/*
-    printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) );
-    printf( "Total func supps   = %6d.\n", Sim_UtilCountSuppSizes(p, 0) );
-    printf( "Total targets      = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) );
-    printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
-*/
-    printf( "Sat runs SAT       = %6d.\n", p->nSatRunsSat );
-    printf( "Sat runs UNSAT     = %6d.\n", p->nSatRunsUnsat );
+//    printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", 
+//        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
+    printf( "Total symm         = %8d.\n", p->nPairsSymm );
+    printf( "Structural symm    = %8d.\n", p->nPairsSymmStr );
+    printf( "Total non-sym      = %8d.\n", p->nPairsNonSymm );
+    printf( "Total var pairs    = %8d.\n", p->nPairsTotal );
+    printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
+    printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
+    PRT( "Structural  ", p->timeStruct );
    PRT( "Simulation  ", p->timeSim );
+    PRT( "Matrix      ", p->timeMatr );
+    PRT( "Counting    ", p->timeCount );
    PRT( "Fraiging    ", p->timeFraig );
    PRT( "SAT         ", p->timeSat );
    PRT( "TOTAL       ", p->timeTotal );
@ -217,14 +228,12 @@ void Sim_ManStop( Sim_Man_t * p )
 ***********************************************************************/
 void Sim_ManPrintStats( Sim_Man_t * p )
 {
-    printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", 
-        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
-    printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) );
-    printf( "Total func supps   = %6d.\n", Sim_UtilCountSuppSizes(p, 0) );
-    printf( "Total targets      = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) );
-    printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
-    printf( "Sat runs SAT       = %6d.\n", p->nSatRunsSat );
-    printf( "Sat runs UNSAT     = %6d.\n", p->nSatRunsUnsat );
+//    printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", 
+//        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
+    printf( "Total func supps   = %8d.\n", Sim_UtilCountSuppSizes(p, 0) );
+    printf( "Total struct supps = %8d.\n", Sim_UtilCountSuppSizes(p, 1) );
+    printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
+    printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
    PRT( "Simulation  ", p->timeSim );
    PRT( "Traversal   ", p->timeTrav );
    PRT( "Fraiging    ", p->timeFraig );
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@ -99,13 +99,12 @@ Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk )
  SeeAlso     []

 ***********************************************************************/
-Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose )
 {
    Sim_Man_t * p;
    Vec_Ptr_t * vResult;
    int nSolved, i, clk = clock();

-//    srand( time(NULL) );
    srand( 0xABC );

    // start the simulation manager
@ -117,35 +116,40 @@ Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk )

    // set the support targets 
    Sim_ComputeSuppSetTargets( p );
-printf( "Initial targets    = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
+if ( fVerbose )
+    printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
    if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
        goto exit;

    for ( i = 0; i < 1; i++ )
    {
-    // compute patterns using one round of random simulation
-    Sim_UtilAssignRandom( p );
-    nSolved = Sim_ComputeSuppRound( p, 1 );
-printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n", Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
-    if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
-        goto exit;
+        // compute patterns using one round of random simulation
+        Sim_UtilAssignRandom( p );
+        nSolved = Sim_ComputeSuppRound( p, 1 );
+        if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
+            goto exit;
+
+if ( fVerbose )
+    printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n", 
+       Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
    }

-
-    // simulate until saturation
+    // try to solve the support targets
    while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
    {
-        // solve randomly a given number of targets
+        // solve targets until the first disproved one (which gives counter-example)
        Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
        // compute additional functional support
-//        Sim_UtilAssignRandom( p );
        Sim_UtilAssignFromFifo( p );
        nSolved = Sim_ComputeSuppRound( p, 1 );
-printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
+
+if ( fVerbose )
+    printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
            Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
    }

 exit:
+p->timeTotal = clock() - clk;
    vResult = p->vSuppFun;  
    //  p->vSuppFun = NULL;
    Sim_ManStop( p );
@ -166,7 +170,6 @@ exit:
 int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets )
 {
    Vec_Int_t * vTargets;
-    Abc_Obj_t * pNode;
    int i, Counter = 0;
    int clk;
    // perform one round of random simulation
@ -174,7 +177,7 @@ clk = clock();
    Sim_UtilSimulate( p, 0 );
 p->timeSim += clock() - clk;
    // iterate through the CIs and detect COs that depend on them
-    Abc_NtkForEachCi( p->pNtk, pNode, i )
+    for ( i = p->iInput; i < p->nInputs; i++ )
    {
        vTargets = p->vSuppTargs->pArray[i];
        if ( fUseTargets && vTargets->nSize == 0 )
@ -207,7 +210,8 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
    int fFirst = 1;
    int clk;
    // collect nodes by level in the TFO of the CI 
-    // (this procedure increments TravId of the collected nodes)
+    // this proceduredoes not collect the CIs and COs
+    // but it increments TravId of the collected nodes and CIs/COs
 clk = clock();
    pNodeCi       = Abc_NtkCi( p->pNtk, iNumCi );
    vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
@ -232,13 +236,10 @@ p->timeSim += clock() - clk;
            // get the target output
            Output = vTargets->pArray[i];
            // get the target node
-            pNode  = Abc_NtkCo( p->pNtk, Output );
+            pNode  = Abc_ObjFanin0( Abc_NtkCo(p->pNtk, Output) );
            // the output should be in the cone
            assert( Abc_NodeIsTravIdCurrent(pNode) );

-            // simulate the node
-            Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
-
            // skip if the simulation info is equal
            if ( Sim_UtilInfoCompare( p, pNode ) )
                continue;
@ -283,12 +284,13 @@ printf( "\n" );
        {
            if ( !Abc_NodeIsTravIdCurrent( pNode ) )
                continue;
-            Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
-            if ( !Sim_UtilInfoCompare( p, pNode ) )
+            if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(pNode) ) )
            {
                if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) )
+                {
                    Counter++;
-                Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
+                    Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
+                }
            }
        }
    }
@ -365,7 +367,7 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
    Abc_Obj_t * pNode;
    Sim_Pat_t * pPat;
    unsigned * pSimInfo;
-    int iWord, iWordLim, i, w;
+    int nWordsNew, iWord, iWordLim, i, w;
    int iBeg, iEnd;
    int Counter = 0;
    // go through the patterns and fill in the dist-1 minterms for each
@ -379,7 +381,7 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
            // get the first word of the next series
            iWordLim = iWord + 1; 
            // set the pattern for all PIs from iBit to iWord + p->nInputs
-            iBeg = ABC_MAX( 0, pPat->Input - 16 );
+            iBeg = p->iInput;
            iEnd = ABC_MIN( iBeg + 32, p->nInputs );
 //            for ( i = iBeg; i < iEnd; i++ )
            Abc_NtkForEachCi( p->pNtk, pNode, i )
@ -397,9 +399,12 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
        }
        else
        {
+            // get the number of words for the remaining inputs
+            nWordsNew = p->nSuppWords;
+//            nWordsNew = SIM_NUM_WORDS( p->nInputs - p->iInput );
            // get the first word of the next series
-            iWordLim = (iWord + p->nSuppWords < p->nSimWords)? iWord + p->nSuppWords : p->nSimWords; 
-            // set the pattern for all PIs from iBit to iWord + p->nInputs
+            iWordLim = (iWord + nWordsNew < p->nSimWords)? iWord + nWordsNew : p->nSimWords; 
+            // set the pattern for all CIs from iWord to iWord + nWordsNew
            Abc_NtkForEachCi( p->pNtk, pNode, i )
            {
                pSimInfo = p->vSim0->pArray[pNode->Id];
@ -413,8 +418,10 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
                    for ( w = iWord; w < iWordLim; w++ )
                        pSimInfo[w] = 0;
                }
-                // flip one bit
                Sim_XorBit( pSimInfo + iWord, i );
+                // flip one bit
+//                if ( i >= p->iInput )
+//                    Sim_XorBit( pSimInfo + iWord, i-p->iInput );
            }
        }
        Sim_ManPatFree( p, pPat );
@ -456,10 +463,11 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
    {
        p->nSatRuns++;
        Output = (int)pEntry;
+
        // set up the miter for the two cofactors of this output w.r.t. this input
        pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 );

-        // transform the target into a fraig
+        // transform the miter into a fraig
        Fraig_ParamsSetDefault( &Params );
        Params.fInternal = 1;
 clk = clock();
@ -502,23 +510,23 @@ p->timeSat += clock() - clk;
            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
                if ( pModel[v] )
                    Sim_SetBit( pPat->pData, v );
-            Sim_XorBit( pPat->pData, Input ); // flip the given bit
+            Sim_XorBit( pPat->pData, Input );  // add this bit in the opposite polarity
            Vec_PtrPush( p->vFifo, pPat );
 */
            Counter++;
        }
        // delete the fraig manager
        Fraig_ManFree( pMan );
-        // delete the target
+        // delete the miter
        Abc_NtkDelete( pMiter );

+        // makr the input, which we are processing
+        p->iInput = Input;
+
        // stop when we found enough patterns
 //        if ( Counter == Limit )
        if ( Counter == 1 )
            return;
-        // switch to the next input if we found one model
-        if ( pModel )
-            break;
    }
 }

--- a/src/opt/sim/simSwitch.c
+++ b/src/opt/sim/simSwitch.c
@ -72,8 +72,8 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
    vNodes  = Abc_AigDfs( pNtk, 1, 0 );
    Vec_PtrForEachEntry( vNodes, pNode, i )
    {
-        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords );
        pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords );
        pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
    }
    Vec_PtrFree( vNodes );
--- a/src/opt/sim/simSym.c
+++ b/src/opt/sim/simSym.c
@ -40,52 +40,100 @@
  SeeAlso     []

 ***********************************************************************/
-int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk )
+int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose )
 {
    Sym_Man_t * p;
    Vec_Ptr_t * vResult;
    int Result;
-    int i, clk = clock();
+    int i, clk, clkTotal = clock();

-//    srand( time(NULL) );
    srand( 0xABC );

    // start the simulation manager
-    p = Sym_ManStart( pNtk );
-    p->nPairsTotal = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
+    p = Sym_ManStart( pNtk, fVerbose );
+    p->nPairsTotal = p->nPairsRem = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
+    if ( fVerbose )
+        printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
+               p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );

    // detect symmetries using circuit structure
-    Sim_SymmsStructCompute( pNtk, p->vMatrSymms );
-    p->nPairsSymm = p->nPairsSymmStr = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym );
+clk = clock();
+    Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
+p->timeStruct = clock() - clk;

-printf( "Total = %6d.  Sym = %6d.  NonSym = %6d.  Remaining = %6d.\n", 
-       p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm );
+    Sim_UtilCountPairsAll( p );
+    p->nPairsSymmStr = p->nPairsSymm;
+    if ( fVerbose )
+        printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
+            p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );

    // detect symmetries using simulation
    for ( i = 1; i <= 1000; i++ )
    {
-        // generate random pattern
-        Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
        // simulate this pattern
+        Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
-        if ( i % 100 != 0 )
+        if ( i % 50 != 0 )
            continue;
+        // check disjointness
+        assert( Sim_UtilMatrsAreDisjoint( p ) );
        // count the number of pairs
-        p->nPairsSymm    = Sim_UtilCountPairs( p->vMatrSymms,    p->vPairsSym );
-        p->nPairsNonSymm = Sim_UtilCountPairs( p->vMatrNonSymms, p->vPairsNonSym );
-
-printf( "Total = %6d.  Sym = %6d.  NonSym = %6d.  Remaining = %6d.\n", 
-       p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm );
+        Sim_UtilCountPairsAll( p );
+        if ( i % 500 != 0 )
+            continue;
+        if ( fVerbose )
+            printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
+                p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
    }

+    // detect symmetries using SAT
+    for ( i = 1; Sim_SymmsGetPatternUsingSat( p, p->uPatRand ); i++ )
+    {
+        // simulate this pattern in four polarities
+        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+        Sim_XorBit( p->uPatRand, p->iVar1 );
+        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+        Sim_XorBit( p->uPatRand, p->iVar2 );
+        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+        Sim_XorBit( p->uPatRand, p->iVar1 );
+        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+        Sim_XorBit( p->uPatRand, p->iVar2 );
+/*
+        // try the previuos pair
+        Sim_XorBit( p->uPatRand, p->iVar1Old );
+        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+        Sim_XorBit( p->uPatRand, p->iVar2Old );
+        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+        Sim_XorBit( p->uPatRand, p->iVar1Old );
+        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+*/
+        if ( i % 10 != 0 )
+            continue;
+        // check disjointness
+        assert( Sim_UtilMatrsAreDisjoint( p ) );
+        // count the number of pairs
+        Sim_UtilCountPairsAll( p );
+        if ( i % 50 != 0 )
+            continue;
+        if ( fVerbose )
+            printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
+                p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
+    }
+
+    // count the number of pairs
+    Sim_UtilCountPairsAll( p );
+    if ( fVerbose )
+        printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
+            p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
+
    Result = p->nPairsSymm;
    vResult = p->vMatrSymms;  
+p->timeTotal = clock() - clkTotal;
    //  p->vMatrSymms = NULL;
    Sym_ManStop( p );
    return Result;
 }

-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@ -20,13 +20,14 @@

 #include "abc.h"
 #include "sim.h"
+#include "fraig.h"

 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////

-static int   Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 );
-static int   Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat );
+extern int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
+extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );

 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@ -34,95 +35,88 @@ static int   Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat )

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

-  Synopsis    [Performs the SAT based check.]
+  Synopsis    [Tries to prove the remaining pairs using SAT.]

-  Description [Given two bit matrices, with symm info and non-symm info, 
-  checks the remaining pairs.]
+  Description [Continues to prove as long as it encounters symmetric pairs.
+  Returns 1 if a non-symmetric pair is found (which gives a counter-example).
+  Returns 0 if it finishes considering all pairs for all outputs.]
               
  SideEffects []

  SeeAlso     []

 ***********************************************************************/
-void Fraig_SymmsSatComputeOne( Fraig_Man_t * p, Extra_BitMat_t * pMatSym, Extra_BitMat_t * pMatNonSym )
+int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern )
 {
-    int VarsU[512], VarsV[512];
-    int nVarsU, nVarsV;
-    int v, u, i, k;
-    int Counter = 0;
-    int satCalled = 0;
-    int satProved = 0;
-    double Density;
-    int clk = clock();
+    Vec_Int_t * vSupport;
+    Extra_BitMat_t * pMatSym, * pMatNonSym;
+    int Index1, Index2, Index3, IndexU, IndexV;
+    int v, u, i, k, b, out;

-    extern int symsSat;
-    extern int Fraig_CountBits( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
-
-
-    // count undecided pairs
-    for ( v = 0; v < p->vInputs->nSize; v++ )
-    for ( u = v+1; u < p->vInputs->nSize; u++ )
+    // iterate through outputs
+    for ( out = p->iOutput; out < p->nOutputs; out++ )
    {
-        if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
-            continue;
-        Counter++;
-    }
-    // compute the density of 1's in the input space of the functions
-    Density = (double)Fraig_CountBits(p, Fraig_Regular(p->vOutputs->pArray[0])) * 100.0 / FRAIG_SIM_ROUNDS / 32;
+        pMatSym    = Vec_PtrEntry( p->vMatrSymms,    out );
+        pMatNonSym = Vec_PtrEntry( p->vMatrNonSymms, out );

-    printf( "Ins = %3d. Pairs to test = %4d. Dens = %5.2f %%. ", 
-        p->vInputs->nSize, Counter, Density );
-
-
-    // go through the remaining variable pairs
-    for ( v = 0; v < p->vInputs->nSize; v++ )
-    for ( u = v+1; u < p->vInputs->nSize; u++ )
-    {
-        if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
-            continue;
-        symsSat++;
-        satCalled++;
-
-        // collect the variables that are symmetric with each
-        nVarsU = nVarsV = 0;
-        for ( i = 0; i < p->vInputs->nSize; i++ )
+        // go through the remaining variable pairs
+        vSupport = Vec_VecEntry( p->vSupports, out );
+        Vec_IntForEachEntry( vSupport, v, Index1 )
+        Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 )
        {
-            if ( Extra_BitMatrixLookup1( pMatSym, u, i ) )
-                VarsU[nVarsU++] = i;
-            if ( Extra_BitMatrixLookup1( pMatSym, v, i ) )
-                VarsV[nVarsV++] = i;
-        }
+            if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
+                continue;
+            p->nSatRuns++;

-        if ( Fraig_SymmsSatProveOne( p, v, u ) )
-        { // update the symmetric variable info            
-//printf( "%d sym %d\n", v, u );
-            for ( i = 0; i < nVarsU; i++ )
-            for ( k = 0; k < nVarsV; k++ )
+            // collect the support variables that are symmetric with u and v
+            Vec_IntClear( p->vVarsU );
+            Vec_IntClear( p->vVarsV );
+            Vec_IntForEachEntry( vSupport, b, Index3 )
            {
-                Extra_BitMatrixInsert1( pMatSym, VarsU[i], VarsV[k] );   // Theorem 1
-                Extra_BitMatrixInsert2( pMatSym, VarsU[i], VarsV[k] );   // Theorem 1
-                Extra_BitMatrixOrTwo( pMatNonSym, VarsU[i], VarsV[k] );  // Theorem 2
+                if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
+                    Vec_IntPush( p->vVarsU, b );
+                if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
+                    Vec_IntPush( p->vVarsV, b );
            }
-            satProved++;
-        }
-        else
-        { // update the assymmetric variable info
-//printf( "%d non-sym %d\n", v, u );
-            for ( i = 0; i < nVarsU; i++ )
-            for ( k = 0; k < nVarsV; k++ )
-            {
-                Extra_BitMatrixInsert1( pMatNonSym, VarsU[i], VarsV[k] );   // Theorem 3
-                Extra_BitMatrixInsert2( pMatNonSym, VarsU[i], VarsV[k] );   // Theorem 3
+
+            if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) )
+            { // update the symmetric variable info            
+                p->nSatRunsUnsat++;
+                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
+                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
+                {
+                    Extra_BitMatrixInsert1( pMatSym,  i, k );  // Theorem 1
+                    Extra_BitMatrixInsert2( pMatSym,  i, k );  // Theorem 1
+                    Extra_BitMatrixOrTwo( pMatNonSym, i, k );  // Theorem 2
+                }
+            }
+            else
+            { // update the assymmetric variable info
+                p->nSatRunsSat++;
+                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
+                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
+                {
+                    Extra_BitMatrixInsert1( pMatNonSym, i, k );   // Theorem 3
+                    Extra_BitMatrixInsert2( pMatNonSym, i, k );   // Theorem 3
+                }
+
+                // remember the out
+                p->iOutput = out;
+                p->iVar1Old = p->iVar1;
+                p->iVar2Old = p->iVar2;
+                p->iVar1 = v;
+                p->iVar2 = u;
+                return 1;
+
            }
        }
-//Extra_BitMatrixPrint( pMatSym );
-//Extra_BitMatrixPrint( pMatNonSym );
+        // make sure that the symmetry matrix contains only cliques
+        assert( Extra_BitMatrixIsClique( pMatSym ) );
    }
-printf( "SAT calls = %3d. Proved = %3d. ", satCalled, satProved );
-PRT( "Time", clock() - clk );

-    // make sure that the symmetry matrix contains only cliques
-    assert( Fraig_SymmsIsCliqueMatrix( p, pMatSym ) );
+    // mark that we finished all outputs
+    p->iOutput = p->nOutputs;
+    return 0;
 }

 /**Function*************************************************************
@ -136,64 +130,67 @@ PRT( "Time", clock() - clk );
  SeeAlso     []

 ***********************************************************************/
-int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 )
+int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern )
 {
-    Fraig_Node_t * pCof01, * pCof10, * pVar1, * pVar2;
-    int RetValue;
-    int nSatRuns = p->nSatCalls;
-    int nSatProof = p->nSatProof;
+    Fraig_Params_t Params;
+    Fraig_Man_t * pMan;
+    Abc_Ntk_t * pMiter;
+    int RetValue, i, clk;
+    int * pModel;

-    p->nBTLimit = 10;  // set the backtrack limit
+    // get the miter for this problem
+    pMiter = Abc_NtkMiterForCofactors( p->pNtk, Out, Var1, Var2 );
+    // transform the miter into a fraig
+    Fraig_ParamsSetDefault( &Params );
+    Params.fInternal = 1;
+    Params.nPatsRand = 512;
+    Params.nPatsDyna = 512;

-    pVar1 = p->vInputs->pArray[Var1];
-    pVar2 = p->vInputs->pArray[Var2];
-    pCof01 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], pVar1, Fraig_Not(pVar2) );
-    pCof10 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], Fraig_Not(pVar1), pVar2 );
+clk = clock();
+    pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); 
+p->timeFraig += clock() - clk;
+clk = clock();
+    Fraig_ManProveMiter( pMan );
+p->timeSat += clock() - clk;

-//printf( "(%d,%d)", p->nSatCalls - nSatRuns, p->nSatProof - nSatProof );
-
-//    RetValue = (pCof01 == pCof10);
-//    RetValue = Fraig_NodesAreaEqual( p, pCof01, pCof10 );
-    RetValue = Fraig_NodesAreEqual( p, pCof01, pCof10, -1 );
+    // analyze the result
+    RetValue = Fraig_ManCheckMiter( pMan );
+//    assert( RetValue >= 0 );
+    // save the pattern
+    if ( RetValue == 0 )
+    {
+        // get the pattern
+        pModel = Fraig_ManReadModel( pMan );
+        assert( pModel != NULL );
+//printf( "Disproved by SAT: out = %d  pair = (%d, %d)\n", Out, Var1, Var2 );
+        // transfer the model into the pattern
+        for ( i = 0; i < p->nSimWords; i++ )
+            pPattern[i] = 0;
+        for ( i = 0; i < p->nInputs; i++ )
+            if ( pModel[i] )
+                Sim_SetBit( pPattern, i );
+        // make sure these variables have the same value (1)
+        Sim_SetBit( pPattern, Var1 );
+        Sim_SetBit( pPattern, Var2 );
+    }
+    else if ( RetValue == -1 )
+    {
+        // this should never happen; if it happens, such is life
+        // we are conservative and assume that there is no symmetry
+//printf( "STRANGE THING: out = %d %s  pair = (%d %s, %d %s)\n", 
+//                        Out, Abc_ObjName(Abc_NtkCo(p->pNtk,Out)), 
+//                        Var1, Abc_ObjName(Abc_NtkCi(p->pNtk,Var1)), 
+//                        Var2, Abc_ObjName(Abc_NtkCi(p->pNtk,Var2)) );
+        memset( pPattern, 0, sizeof(unsigned) * p->nSimWords );
+        RetValue = 0;
+    }
+    // delete the fraig manager
+    Fraig_ManFree( pMan );
+    // delete the miter
+    Abc_NtkDelete( pMiter );
    return RetValue;
 }

-/**Function*************************************************************
-
-  Synopsis    [A sanity check procedure.]
-
-  Description [Makes sure that the symmetry information in the matrix
-  is closed w.r.t. the relationship of transitivity (that is the symmetry
-  graph is composed of cliques).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat )
-{
-    int v, u, i;
-    for ( v = 0; v < p->vInputs->nSize; v++ )
-    for ( u = v+1; u < p->vInputs->nSize; u++ )
-    {
-        if ( !Extra_BitMatrixLookup1( pMat, v, u ) )
-            continue;
-        // v and u are symmetric
-        for ( i = 0; i < p->vInputs->nSize; i++ )
-        {
-            if ( i == v || i == u )
-                continue;
-            // i is neither v nor u
-            // the symmetry status of i is the same w.r.t. to v and u
-            if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) )
-                return 0;
-        }
-    }
-    return 1;
-}
-
-

 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
--- a/src/opt/sim/simSymSim.c
+++ b/src/opt/sim/simSymSim.c
@ -26,7 +26,7 @@
 ////////////////////////////////////////////////////////////////////////

 static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat );
-static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMatrix, int Output );
+static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output );

 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@ -46,26 +46,36 @@ static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNo
 void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym )
 {
    Abc_Obj_t * pNode;
-    int i;
+    int i, nPairsTotal, nPairsSym, nPairsNonSym;
+    int clk;
+
    // create the simulation matrix
    Sim_SymmsCreateSquare( p, pPat );
    // simulate each node in the DFS order
+clk = clock();
    Vec_PtrForEachEntry( p->vNodes, pNode, i )
    {
        if ( Abc_NodeIsConst(pNode) )
            continue;
        Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords );
    }
+p->timeSim += clock() - clk;
    // collect info into the CO matrices
+clk = clock();
    Abc_NtkForEachCo( p->pNtk, pNode, i )
    {
        pNode = Abc_ObjFanin0(pNode);
        if ( Abc_ObjIsCi(pNode) || Abc_NodeIsConst(pNode) )
            continue;
-        if ( Vec_IntEntry(p->vPairsTotal,i) == Vec_IntEntry(p->vPairsSym,i) + Vec_IntEntry(p->vPairsNonSym,i) )
+        nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
+        nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
+        nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
+        assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
+        if ( nPairsTotal == nPairsSym + nPairsNonSym )
            continue;
-        Sim_SymmsDeriveInfo( p, pPat, pNode, Vec_PtrEntry(vMatrsNonSym, i), i );
+        Sim_SymmsDeriveInfo( p, pPat, pNode, vMatrsNonSym, i );
    }
+p->timeMatr += clock() - clk;
 }

 /**Function*************************************************************
@ -114,40 +124,44 @@ void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat )
  SeeAlso     []

 ***********************************************************************/
-void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMat, int Output )
+void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output )
 {
-    unsigned * pSuppInfo;
+    Extra_BitMat_t * pMat;
+    Vec_Int_t * vSupport;
+    unsigned * pSupport;
    unsigned * pSimInfo;
-    int i, w;
-    // get the simuation info for the node
+    int i, w, Index;
+    // get the matrix, the support, and the simulation info
+    pMat = Vec_PtrEntry( vMatrsNonSym, Output );
+    vSupport = Vec_VecEntry( p->vSupports, Output );
+    pSupport = Vec_PtrEntry( p->vSuppFun, Output );
    pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id );
-    pSuppInfo = Vec_PtrEntry( p->vSuppFun, Output );
    // generate vectors A1 and A2
    for ( w = 0; w < p->nSimWords; w++ )
    {
-        p->uPatCol[w] = pSuppInfo[w] & pPat[w] &  pSimInfo[w];
-        p->uPatRow[w] = pSuppInfo[w] & pPat[w] & ~pSimInfo[w];
+        p->uPatCol[w] = pSupport[w] & pPat[w] &  pSimInfo[w];
+        p->uPatRow[w] = pSupport[w] & pPat[w] & ~pSimInfo[w];
    }
    // add two dimensions
-    for ( i = 0; i < p->nInputs; i++ )
+    Vec_IntForEachEntry( vSupport, i, Index )
        if ( Sim_HasBit( p->uPatCol, i ) )
            Extra_BitMatrixOr( pMat, i, p->uPatRow );
    // add two dimensions
-    for ( i = 0; i < p->nInputs; i++ )
+    Vec_IntForEachEntry( vSupport, i, Index )
        if ( Sim_HasBit( p->uPatRow, i ) )
            Extra_BitMatrixOr( pMat, i, p->uPatCol );
    // generate vectors B1 and B2
    for ( w = 0; w < p->nSimWords; w++ )
    {
-        p->uPatCol[w] = pSuppInfo[w] & ~pPat[w] &  pSimInfo[w];
-        p->uPatRow[w] = pSuppInfo[w] & ~pPat[w] & ~pSimInfo[w];
+        p->uPatCol[w] = pSupport[w] & ~pPat[w] &  pSimInfo[w];
+        p->uPatRow[w] = pSupport[w] & ~pPat[w] & ~pSimInfo[w];
    }
    // add two dimensions
-    for ( i = 0; i < p->nInputs; i++ )
+    Vec_IntForEachEntry( vSupport, i, Index )
        if ( Sim_HasBit( p->uPatCol, i ) )
            Extra_BitMatrixOr( pMat, i, p->uPatRow );
    // add two dimensions
-    for ( i = 0; i < p->nInputs; i++ )
+    Vec_IntForEachEntry( vSupport, i, Index )
        if ( Sim_HasBit( p->uPatRow, i ) )
            Extra_BitMatrixOr( pMat, i, p->uPatCol );
 }
--- a/src/opt/sim/simSymStr.c
+++ b/src/opt/sim/simSymStr.c
@ -37,7 +37,7 @@ static int   Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, V
 static int   Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap );
 static void  Sim_SymmsPrint( Vec_Int_t * vSymms );
 static void  Sim_SymmsTrans( Vec_Int_t * vSymms );
-static void  Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms );
+static void  Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport );
 static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );

 ////////////////////////////////////////////////////////////////////////
@ -55,7 +55,7 @@ static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
  SeeAlso     []

 ***********************************************************************/
-void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
+void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun )
 {
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pTemp;
@ -84,7 +84,7 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
        pTemp = Abc_ObjFanin0(pTemp);
        if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) )
            continue;
-        Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp) );
+        Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) );
    }
    // clean the intermediate results
    Sim_UtilInfoFree( pNtk->vSupps );
@ -92,7 +92,8 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
    Abc_NtkForEachCi( pNtk, pTemp, i )
        Vec_IntFree( SIM_READ_SYMMS(pTemp) );
    Vec_PtrForEachEntry( vNodes, pTemp, i )
-        Vec_IntFree( SIM_READ_SYMMS(pTemp) );
+        if ( !Abc_NodeIsConst(pTemp) )
+            Vec_IntFree( SIM_READ_SYMMS(pTemp) );
    Vec_PtrFree( vNodes );
    free( pMap );
 }
@ -429,7 +430,7 @@ void Sim_SymmsTrans( Vec_Int_t * vSymms )
  SeeAlso     []

 ***********************************************************************/
-void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms )
+void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport )
 {
    int i, Ind1, Ind2, nInputs;
    unsigned uSymm;
@ -443,6 +444,10 @@ void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms )
        uSymm = (unsigned)vSymms->pArray[i];
        Ind1 = (uSymm & 0xffff);
        Ind2 = (uSymm >> 16);
+        // skip variables that are not in the true support
+        assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) );
+        if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) )
+            continue;
        Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 );
        Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 );
    }
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@ -436,20 +436,82 @@ int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCou
  SeeAlso     []

 ***********************************************************************/
-int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters )
+int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
 {
-    Extra_BitMat_t * vMat;
-    int Counter, nPairs, i;
-    Counter = 0;
-    Vec_PtrForEachEntry( vMatrs, vMat, i )
-    {
-        nPairs = Extra_BitMatrixCountOnesUpper( vMat );
-        Vec_IntWriteEntry( vCounters, i, nPairs );
-        Counter += nPairs;
-    }
+    int i, k, Index1, Index2;
+    int Counter = 0;
+//    int Counter2;
+    Vec_IntForEachEntry( vSupport, i, Index1 )
+    Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 )
+        Counter += Extra_BitMatrixLookup1( pMat, i, k );
+//    Counter2 = Extra_BitMatrixCountOnesUpper(pMat);
+//    assert( Counter == Counter2 );
    return Counter;
 }

+/**Function*************************************************************
+
+  Synopsis    [Counts the number of entries in the array of matrices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilCountPairsAll( Sym_Man_t * p )
+{
+    int nPairsTotal, nPairsSym, nPairsNonSym, i, clk;
+clk = clock();
+    p->nPairsSymm    = 0;
+    p->nPairsNonSymm = 0;
+    for ( i = 0; i < p->nOutputs; i++ )
+    {
+        nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
+        nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
+        nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
+        assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
+        if ( nPairsTotal == nPairsSym + nPairsNonSym )
+        {
+            p->nPairsSymm    += nPairsSym;
+            p->nPairsNonSymm += nPairsNonSym;
+            continue;
+        }
+        nPairsSym    = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrSymms,   i), Vec_VecEntry(p->vSupports, i) );
+        nPairsNonSym = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrNonSymms,i), Vec_VecEntry(p->vSupports, i) );
+        assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
+        Vec_IntWriteEntry( p->vPairsSym,    i, nPairsSym );
+        Vec_IntWriteEntry( p->vPairsNonSym, i, nPairsNonSym );
+        p->nPairsSymm    += nPairsSym;
+        p->nPairsNonSymm += nPairsNonSym;
+//        printf( "%d ", nPairsTotal - nPairsSym - nPairsNonSym );
+    }
+//printf( "\n" );
+    p->nPairsRem = p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm;
+p->timeCount += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p )
+{
+    int i;
+    for ( i = 0; i < p->nOutputs; i++ )
+        if ( !Extra_BitMatrixIsDisjoint( Vec_PtrEntry(p->vMatrSymms,i), Vec_PtrEntry(p->vMatrNonSymms,i) ) )
+            return 0;
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@ -28,8 +28,9 @@ struct CSAT_ManagerStruct_t
 {
    // information about the problem
    stmm_table *          tName2Node;    // the hash table mapping names to nodes
+    stmm_table *          tNode2Name;    // the hash table mapping nodes to names
    Abc_Ntk_t *           pNtk;          // the starting ABC network
-    Abc_Ntk_t *           pTarget;       // the AIG of the target
+    Abc_Ntk_t *           pTarget;       // the AIG representing the target
    char *                pDumpFileName; // the name of the file to dump the target network
    // solving parameters
    int                   mode;          // 0 = baseline;  1 = resource-aware fraiging
@ -44,6 +45,7 @@ struct CSAT_ManagerStruct_t

 static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars );
 static void CSAT_TargetResFree( CSAT_Target_ResultT * p );
+static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode );

 // some external procedures
 extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
@ -72,8 +74,9 @@ CSAT_Manager CSAT_InitManager()
    mng->pNtk = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_SOP );
    mng->pNtk->pName = util_strsav("csat_network");
    mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
-    mng->vNodes  = Vec_PtrAlloc( 100 );
-    mng->vValues = Vec_IntAlloc( 100 );
+    mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
+    mng->vNodes     = Vec_PtrAlloc( 100 );
+    mng->vValues    = Vec_IntAlloc( 100 );
    return mng;
 }

@ -90,6 +93,7 @@ CSAT_Manager CSAT_InitManager()
 ***********************************************************************/
 void CSAT_QuitManager( CSAT_Manager mng )
 {
+    if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
    if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
    if ( mng->pNtk )       Abc_NtkDelete( mng->pNtk );
    if ( mng->pTarget )    Abc_NtkDelete( mng->pTarget );
@ -151,7 +155,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
            { printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
        // create the PI
        pObj = Abc_NtkCreatePi( mng->pNtk );
-        pObj->pNext = (Abc_Obj_t *)name;
+        stmm_insert( mng->tNode2Name, (char *)pObj, name );
        break;
    case CSAT_CONST:
    case CSAT_BAND:
@ -234,7 +238,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
            { printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
        // create the PO
        pObj = Abc_NtkCreatePo( mng->pNtk );
-        pObj->pNext = (Abc_Obj_t *)name;
+        stmm_insert( mng->tNode2Name, (char *)pObj, name );
        // connect to the PO fanin
        if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) )
            { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
@ -270,13 +274,13 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
    // this procedure also finalizes construction of the ABC network
    Abc_NtkFixNonDrivenNets( pNtk );
    Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext );
+        Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) );
    Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext );
+        Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) );
    assert( Abc_NtkLatchNum(pNtk) == 0 );

    // make sure everything is okay with the network structure
-    if ( !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheckRead( pNtk ) )
    {
        printf( "CSAT_Check_Integrity: The internal network check has failed.\n" );
        return 0;
@ -520,7 +524,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
        // create the array of PI names and values
        for ( i = 0; i < mng->pResult->no_sig; i++ )
        {
-            mng->pResult->names[i] = (char *)Abc_NtkCi(mng->pNtk, i)->pNext; // returns the same string that was given
+            mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
            mng->pResult->values[i] = pModel[i];
        }
    }
@ -623,6 +627,27 @@ void CSAT_TargetResFree( CSAT_Target_ResultT * p )
    free( p );
 }

+/**Function*************************************************************
+
+  Synopsis    [Dumps the target AIG into the BENCH file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode )
+{
+    char * pName = NULL;
+    if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) )
+    {
+        assert( 0 );
+    }
+    return pName;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@ -36,6 +36,7 @@ typedef struct Fraig_NodeStruct_t_        Fraig_Node_t;
 typedef struct Fraig_NodeVecStruct_t_     Fraig_NodeVec_t;
 typedef struct Fraig_HashTableStruct_t_   Fraig_HashTable_t;
 typedef struct Fraig_ParamsStruct_t_      Fraig_Params_t;
+typedef struct Fraig_PatternsStruct_t_    Fraig_Patterns_t;

 struct Fraig_ParamsStruct_t_
 {
@ -99,6 +100,9 @@ extern int                 Fraig_ManReadDoSparse( Fraig_Man_t * p );
 extern int                 Fraig_ManReadChoicing( Fraig_Man_t * p );      
 extern int                 Fraig_ManReadVerbose( Fraig_Man_t * p );       
 extern int *               Fraig_ManReadModel( Fraig_Man_t * p );
+extern int                 Fraig_ManReadPatternNumRandom( Fraig_Man_t * p );
+extern int                 Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p );
+extern int                 Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p );

 extern void                Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );        
 extern void                Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );      
@ -124,6 +128,8 @@ extern int                 Fraig_NodeReadNumRefs( Fraig_Node_t * p );
 extern int                 Fraig_NodeReadNumFanouts( Fraig_Node_t * p );                
 extern int                 Fraig_NodeReadSimInv( Fraig_Node_t * p );                    
 extern int                 Fraig_NodeReadNumOnes( Fraig_Node_t * p );
+extern unsigned *          Fraig_NodeReadPatternsRandom( Fraig_Node_t * p );
+extern unsigned *          Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p );

 extern void                Fraig_NodeSetData0( Fraig_Node_t * p, Fraig_Node_t * pData );
 extern void                Fraig_NodeSetData1( Fraig_Node_t * p, Fraig_Node_t * pData );
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@ -1,6 +1,6 @@
 /**CFile****************************************************************

-  FileName    [fraigAccess.c]
+  FileName    [fraigApi.c]

  PackageName [FRAIG: Functionally reduced AND-INV graphs.]

@ -58,6 +58,12 @@ int               Fraig_ManReadDoSparse( Fraig_Man_t * p )                    {
 int               Fraig_ManReadChoicing( Fraig_Man_t * p )                    { return p->fChoicing;  }
 int               Fraig_ManReadVerbose( Fraig_Man_t * p )                     { return p->fVerbose;   }
 int *             Fraig_ManReadModel( Fraig_Man_t * p )                       { return p->pModel;     }
+// returns the number of patterns used for random simulation (this number is fixed for the FRAIG run)
+int               Fraig_ManReadPatternNumRandom( Fraig_Man_t * p )            { return p->nWordsRand * 32;  }
+// returns the number of dynamic patterns accumulated at runtime (include SAT solver counter-examples and distance-1 patterns derived from them)
+int               Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p )           { return p->iWordStart * 32;  }
+// returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns)
+int               Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p )   { return p->iPatsPerm;        }

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

@ -104,6 +110,12 @@ int             Fraig_NodeReadNumRefs( Fraig_Node_t * p )                 { retu
 int             Fraig_NodeReadNumFanouts( Fraig_Node_t * p )              { return p->nFanouts;  }
 int             Fraig_NodeReadSimInv( Fraig_Node_t * p )                  { return p->fInv;      }
 int             Fraig_NodeReadNumOnes( Fraig_Node_t * p )                 { return p->nOnes;     }
+// returns the pointer to the random simulation patterns (their number is returned by Fraig_ManReadPatternNumRandom)
+// memory pointed to by this and the following procedure is maintained by the FRAIG package and exists as long as the package runs
+unsigned *      Fraig_NodeReadPatternsRandom( Fraig_Node_t * p )          { return p->puSimR;    }
+// returns the pointer to the dynamic simulation patterns (their number is returned by Fraig_ManReadPatternNumDynamic or Fraig_ManReadPatternNumDynamicFiltered)
+// if the number of patterns is not evenly divisible by 32, the patterns beyond the given number contain garbage
+unsigned *      Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p )         { return p->puSimD;    }

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

--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@ -1,6 +1,6 @@
 /**CFile****************************************************************

-  FileName    [fraigAnd.c]
+  FileName    [fraigCanon.c]

  PackageName [FRAIG: Functionally reduced AND-INV graphs.]

--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@ -259,8 +259,6 @@ struct Fraig_NodeStruct_t_
    Fraig_Node_t *        pRepr;         // the canonical functional representative of the node

    // simulation data
-//    Fraig_Sims_t *        pSimsR;        // the random simulation info
-//    Fraig_Sims_t *        pSimsD;        // the systematic simulation info
    unsigned              uHashR;        // the hash value for random information
    unsigned              uHashD;        // the hash value for dynamic information 
    unsigned *            puSimR;        // the simulation information (random)
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@ -53,7 +53,8 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
    pParams->fChoicing  =  0;                     // enables recording structural choices
    pParams->fTryProve  =  1;                     // tries to solve the final miter
    pParams->fVerbose   =  0;                     // the verbosiness flag
-    pParams->fVerboseP  =  0;
+    pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
+    pParams->fInternal  =  0;                     // the flag indicates the internal run 
 }

 /**Function*************************************************************
--- a/src/sat/fraig/fraigNode.c
+++ b/src/sat/fraig/fraigNode.c
@ -113,6 +113,10 @@ clk = clock();
    {
        // generate the simulation info
        pNode->puSimR[i] = FRAIG_RANDOM_UNSIGNED;
+        // for reasons that take very long to explain, it makes sense to have (0000000...) 
+        // pattern in the set (this helps if we need to return the counter-examples)
+        if ( i == 0 )
+            pNode->puSimR[i] <<= 1;
        // compute the hash key
        pNode->uHashR ^= pNode->puSimR[i] * s_FraigPrimes[i];
    }
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@ -355,7 +355,7 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
            return 0;
        // check the simulation info
        for ( i = 0; i < iWordLast; i++ )
-            if (  pNode1->puSimR[i] !=  pNode2->puSimR[i] )
+            if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
                return 0;
    }
    else
@ -365,7 +365,7 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
            return 0;
        // check the simulation info
        for ( i = 0; i < iWordLast; i++ )
-            if (  pNode1->puSimD[i] !=  pNode2->puSimD[i] )
+            if ( pNode1->puSimD[i] != pNode2->puSimD[i] )
                return 0;
    }
    return 1;