From 3c25decf65704916943b0569e6d0608072550a89 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 28 Aug 2005 08:01:00 -0700
Subject: [PATCH] Version abc50828

---
 abc.dsp                    |  12 +
 abc.opt                    | Bin 52736 -> 53760 bytes
 abc.plg                    | 579 +---------------------------------
 src/base/abc/abc.c         |   5 +
 src/base/abc/abc.h         |   5 +
 src/base/abc/abcAig.c      |   4 +
 src/base/abc/abcCheck.c    |   7 +-
 src/base/abc/abcCreate.c   |  59 +++-
 src/base/abc/abcFraig.c    |   5 +-
 src/base/abc/abcNetlist.c  |  13 +-
 src/base/abc/abcSop.c      |  98 ++++--
 src/base/abc/abcStrash.c   |   1 -
 src/base/cmd/cmd.c         |   2 +-
 src/base/main/main.c       |   2 +-
 src/csat_apis.h            | 125 --------
 src/opt/rwr/rwr.h          |   1 -
 src/opt/rwr/rwrMan.c       |  21 --
 src/sat/csat/csat_apis.c   | 630 +++++++++++++++++++++++++++++++++++++
 src/sat/csat/csat_apis.h   | 174 ++++++++++
 src/sat/fraig/fraig.h      |   2 +
 src/sat/fraig/fraigApi.c   |   1 +
 src/sat/fraig/fraigFeed.c  |  41 +++
 src/sat/fraig/fraigInt.h   |   3 +
 src/sat/fraig/fraigMan.c   |   1 +
 src/sat/fraig/fraigSat.c   |  25 ++
 src/sat/fraig/fraigTable.c |  37 +++
 26 files changed, 1102 insertions(+), 751 deletions(-)
 delete mode 100644 src/csat_apis.h
 create mode 100644 src/sat/csat/csat_apis.c
 create mode 100644 src/sat/csat/csat_apis.h

diff --git a/abc.dsp b/abc.dsp
index da023c2a3..65c1eb1a7 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1036,6 +1036,18 @@ SOURCE=.\src\sat\sim\simUnate.c
 SOURCE=.\src\sat\sim\simUtils.c
 # End Source File
 # End Group
+# Begin Group "csat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\csat\csat_apis.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\csat\csat_apis.h
+# End Source File
+# End Group
 # End Group
 # Begin Group "opt"
 
diff --git a/abc.opt b/abc.opt
index e644011b4b500e99014cc80035b7b50b63dd3b0d..b387ed94ce8356b446fc0cd28e8c9476c520ca16 100644
GIT binary patch
literal 53760
zcmeHQeT*B&b)UTt=}upk^=0`h*;tOvlTOm{^kK=dCGmJXi8ha9NS<`EbfJ0V-W@G|
znM+Ei7<T0VEsWGj-82n^^q;gz(*#Kh2dGg2g#iPG4J9oaCx8>D2m-f>0mo<^$ABBx
zA98<hW|uqU&QfQ`uG?l;dbhhXZ{B<JW@bsg_vY<0Ke+Pwzx?hs|H?X!1FV-_dS{R=
zlgc$*6Yyg#L;XAN(6xQ0YZUp%{~-;$4Ow-JTQ8sw&<~(7Uk(@m3<6dFRsv|8SL3_}
za0LKUfL#e#2Uri-0N4m1ysL2D47eI_4d7b9b%5&u9|3$6KzNfl-vHPGxDoJiz)gUg
z0Rg}eU@L%dhjHEx*a6rH7y$$Uqkvt2-GDuSy#T`Bhx2~Gt$<GeZUfv7H~=^ZI0Og*
z#sGvrj&lSs0XPge0*C_c0Ne?P0SJ#Ef$JpTlYkT;4afkd07n7G0MmfufV%)E0Mu><
z=T8B$fV%-Xz$_pSC;$w=9AF+m_#gC<VpaTWFdaRw;9O^C!FlP&Cd?RH#-7VGJ9KSo
z<?Y{oN~3<+sK>y)&Q39t)u4+!`maNm4O}<4E^Iunv(9?>Jf*oya(Lm%<y=mhtT@KN
zy~@sjzk#cFf2?Ia8m%1-uvGr5h>gWRf>AG`ucU?da;yP=TCc>Lj-}ApL`W8Y4dX|$
z_vU8vo5Q!B%+~7FdyIU;Jc$B=9R;&S2+2qwU&@(gwvsCwLo2ovjJaaP(8nX;SSS_A
zCSsAy@nj?x9qW!3j~&m34j)cM4u>+Ku~;OqsGyY$eR3+YYgAR245iYM>|`hzaJNe)
zmOwn2N+ctx%<*h`Dw#~AGD2JhG2kUbha=JPbk`n%UM3RGWGABWP%Ilx#M7D7R5+s$
z4}FfJ^0**3tk;T#Vf{4!TcOLjQf}UK3t~6RrXuOYR4S}gnF}d8uF_sQl8T06UHg;H
zgfh`Em<eIKa`nPhGd~)Q9LrLZsdT_><Qh$LLfzwI@$oEXRXQCwRw;yO(#4f?j_@#w
zk(3*GSWnc8^Ipv{RuK%<<YXugH4W?Lr^D59Iaevj+K<r`jbz8CFs#vdCX$*6LHE^J
zS{+=dVZG4ImH4I8E<&;=;&DugXd<4)bj<`x)x3?T->;Xmi(9rhMW4{;>P4ec(D~}p
zr`zgU%Z$jjOY**wZuRf|qdE<Zq5r8wIFe3hV~KFvyc^bw1*6gs4-?&3Y#8;59-5fW
zj^nYQFR7KIo9Rq89S<d=@ySSh3UjY0jbn5&8H=DiBh(j3r4p%Vd?L|4ko97*kghiC
zdFja}wLBgVO-94gvKiKAbEc8yL)P&?Y-<)yMKFinZ9_au6%B=wawX1hST7ChXM%uH
z$b$1Mop%9t1NH#+0&W59bLOTaT8l$AGTkQK`^_X1qfdo47R7=&Wg7L&*_uJi8ms6`
zqGU`K&Af-C?$4EBy-}hk=9!~LeKL1XwQgM&E7iJ+i0iQjy|j-X2&D51MmZ-nk4H1k
z!WRppv0zwB-&w#;izQ9l)+`^7Oz7ccy_z>nGe%E{+nniiKw2K3XifCwR4St1u8*_|
zJZF98NHndVt`-X|R4U0jcc~YTuHj#UG#sDR26~U{jrv*rz7|F}lnEbc8#iMJ53hW#
zkzdfIa(%0g3a1^OsM+`0mOnd*uYP~K9NADT7LfUeBa3;X)+kmhUhJ3Nq{Wq*NSw#;
z2^hz-JT^5M=U+G$hpcCGHX9F*W$mghTNd?O^;&bbRLtuFUDAj6JZRB?4xRC|Im9!m
zM9hPQsO#Xt3tdbcGD<F!9vmjK9n>dXltoh|Rp*l~fe#T67B*6n<8-jIE3>@T#k;+l
zGf)T;!N*NJO`o`8O=RPV@d!QVl@hhE1#%0wO|lkJC&>;GJ@LF`oruQp*{BrEs%n!%
zlyxwbXehKXnLex}Pvvd2QP4ryZmOV~7`ubM=+bxZ&ZS^gwb2%39poh%3J&<T6jD!9
zQPW1B7j=+#2&kyz8@*C`JhzkWdZCg|(spYP%KSHlN;gD{SGG%Ul`6QjD0y(AUnR<Z
z(6=rAo5kH3YNKG)BBfx356z>|u$q%y*VZMgu!D__%73!CpML3R{7z+OcttyXpmq|s
zTdU;fUkNjbL~JaSijJ$9bl|k}Yp?8N-CoPdE2Nl8;u~!wI~7&(7qzHtW87-f!Ln8E
z#Vi!2FWU+0*)ptGn&pnqtQLmN@WRjEAZq~Aw4R=G+JIKh>A8F@i{D($vXQM+8(Hx~
zzn}-QliBHgd+~LrR?p3M#|y=hM?y=&oJ>uRjEpP^HJJ<#t+@M}gFW=ch2SFoedak0
z_KO}Jx2<FPTMo|E+SS@)+ub;iPOfRud6GTJwk0*PdFm}9xOfIQWcnbO#=i$%=ymZL
z_}uCiot@fF?cAuFS3r{IE%p|B@NGAp#jg(bkR6F&owiO(z3IkT0FK@F>$K~%OFP`W
z9+h|vYJ=K&g**>^){*&5_9lDk7B`(2A9iq_WzVu#A0|Dt>-lvFXTP>zdts-W&I07I
z`}Hz=nH{~=-LG>J&JWoS*&n^?#yQk<=-i;)pqYxkpO^aeG<%wTKIoPwAdS~!>@oIb
z1<s;G=K{OH*1hGH=MiZv4rm9o8x=UohBICVwS(F(o^#VVB;ov+{g{1GF;|aByq;oD
zvGWT3d}EKJpDo%J?V?IQlAZ^!)_)6mNTQFp?0)0MY;&Gl|7OknGVT;0<21oEX5b@O
z5$kYmAH%dlaF8Lg6OUI|e{4K5)^@|Yi25%9XyPmdkJw)h4=DVhu@pSQC7Qnd@3?RO
z^X-4{$zbW*|HhBU6=u8+!xO&wSe_JxbxyLg3|mH0-~PvKhQ9reoNvDU&$s{4JP<}k
z-~Q*@|Aa}|HsW=f>3sX2(hB3-{{jljm29}{oJe+^ZAId~58wW$&|<sIu2YY`{m-}m
zk+Fd>-~K1eJ-+?VZL|C!?SBI>vQ5VBi1o1k#zN5?ZMOx6Oa$hfoXpjZ7L7AI^0nF~
zGRfiSBV-kB+-RJs)=v>`kZjd$hj0J$<Ny5lzxQNL^W*=x-A9TVY#GiFfZ@mg`SE`U
z1@z<pEL*Z4|L4d5*?t8(%1|9xg(&#;;1d*dgq;wINA!*y>F&q>sX`AGCIKmSuhSmj
z$N%~9e<E1WW5Kl|{8W*Ke*B-<lO~>cVm12le|%SgZpEzo@qd;<!jJzG;ZT13pWEK{
z`xO7D+JAivJCZ91sH1(+mpg92{$s?=zN`JmA0wjH{^KZi(MPcxK8IcK`O7g=)MNj3
zi}zCZKW`&Cl$-#E&0pNT`@bvR1OHoyjm1CAO6a?Ze@CHp0~*(nJK$aE|6TV#O#ChV
z_aeBH_I?lYeQjjs?Y}LONF9*>u0*}q`ec}*++8v-Q7jow^Xren2yE7Jc|*S$t#7_n
z59-#=@_;!sNCfB5z+5GEUFy`@?4#Hy62@YVs~rpO>+ZB=!8?TV<3Hh|_4j{c<E6j<
z+u4Ok!9)K3Z-4(cx3ByAzgupFsK5WaJ^mP`EZyJ#ZJPFPX=`hETMU%H|J%Je*fA3O
z`@borfN%fxawj<3w>u5vqNZ)B@uCh_g+oALcjsZAD!Zv4|LMnniap|O6Rg94+%eTU
zYQ3hkAOG2Xr??;gNyZpI{*&Sg3H<m^w>|oUjQ_m*C9&1{N;1i9*N+t|yGC`s{d+l?
z-+1!J0Y-VMDDRycYrWhqWt0q<@F?z6J4YL+c?9S=T=1>o|K7hWn~9_|C#m?QenOxf
z<1hBF7RAKSSme#$<h7_|ZkCrNPegy!?@3#5CMs`Iwp)HI8`zLekEO8ddnF5Ja`kzm
z5p5V{RqqJjEfkenMA~ec8nWkd?H#UHn>7oA8#<LWWc^fD^bc$pzvEbMzFg>1-BYY~
zsqHK0ij^+)7K_<}nnho}=}}`fG-~RGR&}{i@5a2AtD8m_gx-SLm3-ak)^|$=vx;1%
ziUH{@pYEpip1FpynV@RZ&Z&|5a;8U(XxLZoUf(}g&lTsp@b5K?<u28I`ODB3Gpkxt
zi{Cr9nCn6v)y;0z^)uZ@y*J-fb8XXXIj0`AzPZ|bH`$h<Va@2uzua}j^qbA@?d_pA
z?(L$3zA|zfs_S8Ht9R=`kJ(K<ea%L(q$VuJ^t9o@msiU=UUkIC6^y#@!*n6JCS{ma
z%9D9n%-({5QQN@6<3<hXO^r(aY`9u!;1Oiht;e7&fVj3}*4p;M`}rTOs7^osqiuim
z^FJnH9lu9mWoxC8R2V<(AkI$1iXZ<Ojr;i@Mcf>D0`0BiiYX-JZtR>ze*Q-%YO_-}
zWL@<0KYH26{QQrZh@bz_&;RJ}|Mu;FA4dMi&#(u%JuUFUV9z4nWHbF~CuikP*iYCO
z{>7cM@|EgqS|99P1UG6oYXAH-{=O(3x2@y+!Bwr?smBn}IHt%$`uf4QxrLAfcoqL<
z75PIS0v)O+cme<ZMv>R@^}}mgIYysh&#><*aC8ah2kZwdaKSC}X5<DXqa?wd_;<G=
zSLr^9&X3rS*!O?pw%4BD+^5+xU#VTG{ZxVT%AHRB*|pkQ?e0sxuKcqv-r?k*J;V;N
z$G5o0;>9Blo$s;lvEz#InwEHN&^Blb3Y^!$%a(bgwo$wG???|lI#kg*HcND#XV0_S
z_PP5WkZ^v^e$KKAoFfv>&)Cn{fFg%)Qqpt3*0248VoVn#oE6#%?cXpfJ9GFxA9Zwi
z7v98GR^;%#DD{1ZwnHl@a_^ph+sTJ}y>`9!&c}P{9cc6lH05y|Z~l5ou`Vu1V|o-Z
zzYi$p{5K?Czhu8;M-^-5oYeQ%*lX--3Y>=|I+xfb_NW5Kw*TM5$n=ac*E-DC8spaL
z9?S;9pc&XthWb3Metxw;R|6;u73W1Ug$IWkja+^~+^@iWc)`dcEd=4NrrT<%l&hJB
z(;!?oat-UAsD+yiQAs!BbEb4-7Q_wFoyb*+RdGvU#S<_IN|j_fl`5MROK_q&vDg$<
zbQ7&KcJPi6%^1Dq!l^_43vsgwb=YJ)1|NqgAmqs+a%4ES^iC5?RzgQUj8f6GdP3;Q
zdJ(L+9!O0oBVVnY7Wbr=lrfjfH>wsv>JdsTdIG;vEm+)%e#$sghX8^AbtIjW)Rs2x
z6*X(9#<(|SG>T;lnP{gMsz~c$k6*fK^^+K-VVN|g@k^gE45>O(EEg-5YDtc%3Wm>C
z8j+rYZBmdXYIspgaqg_RCnpBE`rxgg+0<tbA6@VvSYE8QhGU>uO~EuNTCNs1V=yLK
zlC82zO2s*WViiORcEL)4kt|u$;tFw30+p&(2f)M;cTKT+j8rOd0bfxhv*9J-io=%|
zwD@pu3-u3H=wd|(CoXv(S5oOj9g{^=t)Tm8rDzS_pt!Z>Bu6F*t%=YJ9}PXMd*ROz
z=UjspD0elGYPnB=E`;-duE<Nk&oK1!HZYF!He^Jn3d>r~abOnb3ms=6UO!!lg^sIG
zttg5IaWmm8D%`aOj;frITY)>N1H!OQES7T<yP#%Wi)F~mLltY}SMuA#tp~&ke&1rY
zir?}95Ttrd<6i0|x4lz0`?;x|ItQCNow)IwcNSK1-dUWjF5(K073ZeKX8<+HM%}5w
zDsgU(+5|eR>3Cyir`g<jSs+QNax<!3j6lYA4?J$k8|d5r{r5kq-+JcffAI4^*uFGB
z|AXswMXgshi6B1T{_orW+moP>&A!9G)`}ihct%<#ey`|a-~R90|5bCt&;RPj|I$}_
zKmM2h5`!N6_+Ph8^@EK6_3i(B`SCx#{a^T5eEUDygL-slW-#{u)&39582U;^B_8@7
zE}0XhLb_C)7486X0{QlT-~JDOfN%dd#(euf8-OL>xBqjO8Jq#W{olR2$=Vd*$N%Fc
z%GpY1+HyTKF`dObp+iVRq|?r@ykVNLYCc!Gjc01)Ee_~TqH`xxk01Z9Tlq))_<ukC
z-`W%-+#4;6zV#-6Y|EyvGP|{~ef$664l}nO|6eNRb>IFU&)V;JQ!OC7u03ByBy}_z
zj&w{Y8<of?Tql0~zaRfUGUCVo`|<yN{Qrj$|38kL!?Uc(=JC&9b=l;(r0aFa|4dml
z2DuH9LenmP#0lj(fj5pU(|PbOgL{QFkO%qQ9UHJSfbu@u$5L9KBqS^U@>1|Ghhy`m
z^W|_qi2C1!{|aQ?A!7y^dd1P%i=q35!?&KyTG^Y;lZfU$Y1Z>6DMFS1*^wW<U*9nr
z+~1ALP7f-S@|lwaSsp*mY3&Pkqcyq&T6Xv{k=wnSXWaJc;8H~6q0vNZ?=IfWYat&D
z=Z6L<r$N11+8(wA9zf}8yL1de(WmShM0%dvIG$_d8fR;UK3Oz#rQ&?0Y*dirL8u=K
z>4~+WJXr+vqs3||*C<wzu|-rOtIZRuqZK`wo5vf!>-B2guDKpH>!YQTF`p~x(Tdrq
zH}i7Khf%*VRIlgG>SNVrrC{oj#k^q@3?x($v_A)oO%tVRu7TV?m1?~VLJ6e4$W>Y>
zp9jhY3#E7(<_UfFtbUhKN7fZV<4+ufXvJ7W6uXY7*Ji2JyGMX<m7ox<oJQvhf`=^X
zp8{u%z)74o>T{*)8JqqWP<5rKN@HumDV^^quxtMewO5GRDP)^yYk3vw2IEzI(kNH!
zXYCdrN9pExwSxHjMzPY&&6c26=%psha}$u(+tQ8~&05tg%JpAF{U(G58}mq>F|O3h
zp95vBjndhvFHw7J2{?`X=krEEHF|FYWsT@@XX`y0ro?zGrpK!deS(J8?%Wt^uBI9a
zDKA3TpXPH(pU8nx3+n+^eq!xpwa`S@T_pYhmFu~Es?e+}>IX<JTQx^8Q%VMA0)LF;
z&GPeCO&0U@s#%?D=;3YK+?plaKDLPs)T~#AuBc(nVo$+|(V4*-?dqtYqQ4f$c85N~
zx$<<HvaxJGP~%hiL~#bijZ+^D<QH;ved|zd`+?IjWEVkvw%I}&nYqTUKb@(bGAeS_
zvKrs$u}pAVPSij{tE~bli%D>1Ye1|gJv5uoCT8!+HnLlX0)arYVq*0gg&{6saOhLP
zq3Z%}ToR1BFtpRFk~2mB9Le_Y9i184%jG6kF8-XRN3-kg?vgq>dK{eD(5fYw&`S#5
zU+)we4XbRq)ppr2+6og~%ld00DPz9B7R29y8Yi5NFQajZ6~(E#-BVIL*da}_>U42r
z=BgT$iBdk&<_>94QNEH0LzHl}c9tf{8QN8Iqa$bIlpx7B+a!yv;ToA~Ljrk@!G~Ew
z;uB|iZ5->)sIRVJWKju@;by(BR?byKuSc&%uSriUn#l!xOqnM}W>(h3<tVN<1ss8d
zHtFF$v?UOjELO9$R{;|mPh!j%dlrBV$H7doW^Lyfjm!*fr0EyNYR0}I^F%XKZ#EW!
zGn-Iq%VC#6h~>43245muYmE`bT<Msr*ib<;wXcSYtB4QwHl3(ps}+cIM%#ijZB(FV
zTmHr=zSW60s?fywsB*wZ7Ds}!yZ7zdKLXik8QbSzFJxTSq$kpdI0e@QgZp-m?%B0x
zzkZWGvN(Zbur`N}jo^tOmN#ZXKM6O&{{~mpcpZ9;{{yw8Q7@m^H6sRV*R`w<ovE}f
zS4ns=KzxN08i_w_i;rzM=p|{fZNS9z;A2rc%csnMHDyv_USQs%&FJ!4tT=nvsPxxp
z%sJvVo3!)Lz!d0wXkcE8r-t`ja4lGxK7zYFe>b+~l2}oE(F|G7HZILN_as}xMNgCp
z=pK{;ij7mjLHf(bxSfNj<$uvxe77+hL80~CJ?tbta{iG&_3;t`9_87Y0K?D!+#ZVW
z=YRGJ26oancg`U{|FiIOkYPF*Ivi0hH2?j7{`>zT>2x9`X2-BzX_kk?i<|6s7P#L3
zM_<F~7-oCfv0uC6-d_Lf!B%dC&Dv(|*S}$1_q|WEX|@Gl?7Quar+xSr6np;f{^npS
z2f;PkHQJbJ&;M5)oQv!t`;3ClGm}m(gR8Zxwa2!*V`?Azth1m0N%kb$mc(9E#&oU>
z>rdcYgROiJ)UO8=xdR>r4sGEi*s1N*&MEfTpO<*O#ol5MzU|iY=I^`#ON_9AuG7|O
zDMb!~7aw+HzD~PNyQI*M{O-CzZBRR}kmnIehhFdhdtKu7EPIx{3L`>iOyr@4)A#+_
ze(eQCE`x`@?#!Q;*~{#xBB#bzAdlU5ulVnaaVN*e4cZNwspxwE`8({fc$z)UJ|A?C
zyPV(TG4>eyvI2*4m)LYJunTP6Tki3abC(>@4rn(jaOB)22epIRFP?MLp_pTvmzVul
z&L{E|dy1WZ)lEnCA8gUKXcrawS-@Pi^*o>rXunm+Bj+XY%K!3>J%c@DGbHfJ|03ru
z@yh>_l;)3D{uepFiC6xYb5g&&^1mEvI(_%b|3Y#0wgJT}|I2xamskE5IhTr8{uen<
zidX&@%G+Yg<CXt~@|)Q6$1DGfoZrMN|BD>o>=pk_xl3$bUin|-95G(`U*x<bUin`r
z$B;c&z4E`vd4Ig}zfi6jTZdlxU*vo%Uin`xNV!ygm;5gapkvG9mH%a*lpn_{|BIZ@
z$SeN~i#g-vmH%a}g!2x2hh6$I|9sbv;CYMBaJC*G9|d-nee*An0i7Mv<?@SCzsQ#~
zsK9wn!dYMoEb;X|7o9~3r-=7pUZbE>`_&u#2Pf(A9{f8zthwl%lW<CS$L3uMoJS;_
zGCWYhBW^lhk#H*TP`xtS<Kp$Ggj0n-Ye*sU6B161)!62XZXG@&;oQsaWw$BlJTKwU
zTSI3QIDzlHrrC3>0iRk~(f7bhjt)<=(=1eW_lrq5XYgjyKUVPC_qPtOMYd?qAJ4o<
zH0LwOz18_$;uZAEezv^9-e8fxcjL%8p&n<CvuFNuJ^L%|c<&#wf!^maUnz&#A<T&*
zfO7yk1}?4cIfQcza1KDnz_%}H2XP()oCEwmAImTj{p`@PNBjEN`8Gv_cfxK@>rAI_
zx4&esu-H%Odk5Y3v$xr5?VtVw->=5#et>-!<MG?u?fO;h`^X(v+D+fTsQwE4zSzZ{
zTW8m=XNTBf7Tk#Y2GwuGthgDdNOR8*`z-F@tlhy~j<T~*B<#8AzFoWb?cKY7-}v_3
z`y*r9gTe5`_OXfGd$*5_ghC@DyTifJ$msp_`$inZ!1kBEg^OPSHld7QB|dOw0lgox
zChmnS@W}DQK3li!8n-6w#98l)E=W%VAG37P^C9cvWyms!LAy~p<B}iOx^)2~zDT$A
zz9_?H^cy^xJ_UtnAF?tYhd|#0tdY*Pj90mp!JXFciz4VrNpOobE3hBV=F89j)6a_k
z!i=~cgR&Le?XxY=2Dc)1EZlV8XecszOK8{l_TViOd+?kXAK4z72#(QnVkEqOWMcn#
zWUuv{0Ac=Hyz@CRjdB8dPTbtbnD77d{eQysOnxAEQhfg(yj;HjuW`!v|6%WwZFBbh
zf4=_@aXC7@UP5|@gkm#*@BeGdB&E`j@BgzG6HTYq?h%EmR4-`lbSrn_wC`t$hmc({
zlSst)%V9hBwY1lIxwQTFzm{`)E?>*y1EE<qvXyEhD|YS`^gwnp>*s$GzguMgjhFv#
zLGs&q`Tt~pq?i9s_I-N!|72gIm;X=p5qkOmWS^6l|4;Vcc=`Wi|BaXbPxiBV`Tt}e
zp_l(p_Mv+D|70Jkm;X=pZ+ZFuWFM-R|Ig3=B>d}M{y*6d<mLa9{Uu)hKR^GIpa03r
R|0nxLe;5DX|F-u({5OyFS+4*9

literal 52736
zcmeHQTXWo2at1jhMN${bk}P?BStIh=CM}8LP?BRgiehqxwCRu{mqSS#i(D=Sb4bFR
z0bl^bOHy&1ROKnR&28WFoT^mv5B!p<ROKQ03C`PQE3bJ<?K)rg0WdQ-hhxe~+3T$X
zsX0J*pZf(keY*Sn`@cQ=`QQE13;$siuKQNW`o$Mx)<_qA0QUrZowq>$;tRUZe(4@4
zbA5|y;OEGzjdm*mh5*9=YV%WoQNS2r9B>*y?R*x$=K#+D&;_h#0T%!l0ha*J0f_Gk
zexC<?2k-*mMZimdmjT}eyaFJ;W&B<RybAap;5ESOfHwdWfJwlc0OGxl-y47_z)iq3
zpbVG++ydMN+yT4=ApW=Udl&Ey;5PvG0KW;i5BM#>yMS519Dw+%_?-tV0Nw+<4_E|z
z0Qhad5`g#!R&c)x_&#6_Py?(39s(W#9s_;=_#ME9fF}S7w~5~$0=57@0yuy=zy&k_
z0ziCU*R^H^_?K8VO77z~vW}30lV6w7W3s#seo3&;#$KHH<G=ss0V-d{`WUH4)}9qx
zA?m_K`EAr?g8PK)BI7&m*R}?^pHknYd>qHujpuw)XT>##)C21P=?mOF{dL|N9H6l?
z061y-XDFF8{du&yhq6*Fe3k1Q(x>rCY14I*I4%=Yn*IRVkMdq}>hANEcQ&@dDELUY
zNxT6B!Bis-iD7(dV@))L6N`=3zPl36Hg~4tdQ?Qu1wm8AuSTAqsOVY{X|N9yuNfDZ
zx040OO@c^4>tc2q4bdoY#zAvm6oa>7Cz*8<Z{JIf3j9Q>G@W)VjwL)2u7<WOS{m$1
z)DY1J8p8M6qOD6}O*q9OP?l<3jM>oBL?vmJAkxJriHpIp;cCK(++8hMZ6xGGE&X=n
zcspv=7+rDvz%NA3gar`V#ZDk8LTN<CFFV?Z)Ou&`2SKA)9gIi6X=w>HN1K~<r{2`^
zQ*YH3Os${TYpHn$QcaPN?Jz7vOW31g=K}Jf?<B>n5n4Bl4%>xDw-4KuNT?A2|Gsd-
zs>)92nu=cXVx{5^+sjT8d50?Zs^b+0BU022W}w$ZqwN+;2z(9mk*i6x=J`8nV;#01
zh7Gl#(Lpr7?-X)K$irg&1G(hYRZg{0!Ko_>(3;-jwi7i5LW*doSZJU%9U9o0__&ZU
zAa#9~&`~=n4)pDCr&tGs(o80d*7g|USBJ91YC9uH`r!|PTGNy;x|1?T5q@1Wm<fGM
zNsr5oI%Zo=7^<%gM(U<C$*!rjl%T7(l%&*Lj@RW@61BA_NoxH`ysic%Wld}s-@1~3
zspyz0&~-2wM$;fEAri$-oe|VtDJjR7U(;Tm@`m#Q^_|r6f`zuPyuQ6a_uBOWT@GSR
ztuSuZFTS`L{hm7YF#d7mDYLgYOd^L8oof{1>X1B48=A>AXVCS}oVegA6J$=qn>2`u
z-$Na$7Z>X-r>#c8P9)-DH_GW$yGmD5UK?@JD!%31u)P&0PEw4S@QFJ1G0i(oujLir
z4Lc$U!Xh$slHFMM@e@1SVymTm&c#U-JNt#%HW7!Rqcl7w{Hpv&+#Kh(EM82u8?;(r
zwVR$V?5p+IZ8>{lN*oINU3`C6S1J#e=RYZLI8DcIc^gYBmD!~lp4UYy+*qrv&Q$N*
zol08a)lQ7{C^(3P?fKh*y-f`}H8p;3_tyQDb`rJ|`?2RYf`fZEff>g|lr<5zn@KEj
z^pQ`=->|1`5k)~X5l>#X%XjPpC-RYFJdWSH8Ajqhe(FKvh<<mIR`dS2+io<dpB8F^
z&@xpG;loCw610`&0EGdGhNaTVlJs5_w2SZLG}K}o979?1ieHOqkY%+Wr<7H7RgzNH
zL=Y7RWJ;=0*V303A8ks1mL<|uod}Bww32AfiM`^W16o%hp%cYI^8#XgEpgnvLM9t=
zL!BRitn3OM?^578#pVXL`UL|drh{Uxfn8VM0Fltl(Lid-0W6~BUf#R<1fk|_7Y8?C
z51eAd0J|=fd55r(<Hy^|6a~sd-&1BEtb+@c35;5qKvsel8bEpR5y4L!rHgV1&2km|
z?YbtGDps({G6#_mK2{dZAap*~<$|79mS&mf?dZN}c)h3@s*G1ZL9p~vM+2?hl!YZB
z%`#8Ql*}@(OOl2~+Sj$rE0OeXgvI_OekS+<<fA_Z_5$v+>pF=5agnI8$j5~APsT^$
z*nWKf0{Tw?Bsx6_A0_`~d|-hv_+)&<OK}?cUnWyD^1lt9(A8<0(dNa#UkaF}jr^~B
z(*sL9^=)tDfB9Y!iwoNceLfYJbwtuiu!x|_uL!G?UJ+g+Zep~N|8?!!vD8vmgHp_9
z<bRL~8u_2sH1a>WBr)<oBmYY^9*q2tzy2V-GxEQ#H>#2Ubt;2bNxD5JCg{KONMU5b
zsCo1XvPmjv)I2g>Go$8_FQp(A{Qp<;7=;LKdFg|tL2EeK_2QZD_UHi4#)*hFmYwjC
zCl03EFuY6xJ6uD=tmAzkl7k@HBi?eV51PpnWk~tg$p1)>65B3D|Ig_EnT;XRD#lE&
zQ<^gyL*LBC&;|+6G#l`Y*6Fb^LD6DMu}1z!dW2d{TPb~0H79etuI?mJ`&BJTs{B;q
zjr@--7>xd((f><jJ4XM{=>JK9uhIX@R^1Tv8U4SGY|H5Xb$x@fJWthfH1fanePZ<g
z(u$x3oiX#urc_ApR7DX&ezRs?I{WL#ut@fyZbx>}Uv^!E{W19pkk-d1vp@bdiZr!9
zUW66>BCO#ZSizGG{L@~rzs}P>sr~acN`#yf;L6gMPf!1M{41pY>y%8Ie#L5{>@og5
zLahtbxDDR{PgVa<UH%HCpVof~s-I;0JqBavI3_Xg@V)t!wfo(FPlIl|L>IBdtC&%;
zDCz`%`7wmRap<_hegmQ3c*ic=sbx9LNyaEb(&3NK)Pi;dCJG%7)v-3C%#>ixF}R(S
zARis(_eu$7J0)mUl`vpRSjY~MSYbr2Xop&`<QQffqtd=`yEEQNM`DZ55?jc6YU7Ty
zjs3SYIX8v@#xS7sPB;3WM*q{ue<94(xU`UOB#qQOCFtrcB`K2g9B<^ms_w9?9M$*=
zDx5`=JY)ae5oF|+*z~<ssHmJ~^goUMr?LO;acyPvKaKvUvHzCSqLKe*Yavo!RX;(D
z{5Pu~BmeE%Hu)u$|NiJ_(h&OM>|6yNU>+|%xHV(1%`eT**5*$^6erz3j#?FX-5|e^
zI=+h}&O=zwr?9g1N%wQ$Q!=q;EznPK!^Y$PH9WGlK3`kkAoS0MiGgg&e>!|tqA5u@
zqao`5Fcmk}v)u_)MZLZArO{KQ|2ceY+%jdE3Z+2T$mpe7ZEg*A;is+2x&!ZP$zmc}
zy3!H5nyIcxdgPh|@Sw}}#|~T4WLVg#rH}+vOBf!#RQ=#_$!#_IkO#e>4|S*oZzFx^
zX%h8@K8Ydv5b6`W1ot)l$Z%TIhdj(qYWgsgurJ+@jD6ZZ<g{#%Eo+%d@Qb1)$Z(KH
z_n~HSJ9?%e2jb*D!G}oD+J`Qs;C&cMc<b~br`dxPUCUJ3K6JE%G#qyF`jH`+??=YW
z*N2=Yfd##mi6#A7iVT=;0`%c1K_<|LJj`C$`Z35+7mJVkF!3gYp3duPJ&9u;jQds3
zP#c!heL~ZgM<24RB>DFYB)4$CCihzUggFQAU|qX1eK<=EfmXX@RjMKsena@~QR>i0
zMCmlwodJ2D+cVG}j#h(_2&(=fVRhPzgg5rz9T|@ljj8n~@wyt66l4Ew?7!LRq>=v_
z`Ja*h8Tp^_|Cs4+8U4>LL57k4W%4Z}|I2)W;j7ZP`OjyIZ<Cw<Us!)Q=vYDN{PSaj
zqo2Pzm=%InRa$d3CMe1ZDORVdKqRxw+mMT_ic)hqURQULsI5IoGRwSlGRE3XwMhWd
zxcTp|=8?(&KVmIl$m|CSqU!;RCDnrvi?eDjeuqg&?~;pGzT2g{QQ&619f>CO;MoMu
z#&_lOIG&|F5r;ZUk3qBPgg9M^F%%%3ZTOjDqoI;NRB<*%=OJ!%;>F;A&JWW_y>|h#
zO&5_~(OpD3^C6FB0f*t_4~uX}&jq2pF7YuVIc*sZ#QEV2Xv>}tckF4tiFq04H$;+7
zj}M%dNb^eU@Q2Z)lW{ma(WQ+$KT@gJgd6z#l1%jiDU3YmiaDr6ESKrx_vu6<ex~@>
z!~q{5!3e6h8oUW~9&juSKb#|q_;^k5X$g#?xNExs+<Ii~SAz$8exQuia0Er%)qb@D
zA-c$rxZ!93$xiur=tH+HYj290rn63Lk3{5cAIWFhz#umw*r_1z!$Vo~(G54jDKE&I
zV>I>2$N4%dALbxvOmlW7#WcO`G%pe{-^dWBC1SOic8h1^Gi9h5qy<1Co$Q|T0zQ+Y
zD;1<GQQgTfrs8+fWkjA1@3c_)AfbkXch0}O<uaZo>_UXjB1z-)ya*@r@^MT)rhSr`
z<@<r-DPezx_O4h@o`0Q$1}JYcP}TB&0^OwQ^UUM52t%s$92PGS4nyx}BBYXZ=E1~C
zSs%u)%n#qmfeswaw49MKJn#(5PosFs8;(e8bch*~#_`lu04a2*Bu=sTT{5Njau_n6
z&Qjs<r}>f3P?7QRbDr24e&hy_{3VF%sgx|2r(&iC0zg6DPGw}lIu{labS^A@W&az+
z9j2AeL!J&%R+Feh!6@lGJjx;{NZN5?W>KWxIV_NJsoP@IZ!dxw<{mh1a&ApZ(~bO}
z`md4y8~H!4MKR43zIT8zABNegF4yrj`oH-$r1Ae?{6EMIALIWan<tF_ho0>pBmXz@
zfAy3*-Uy*@e#L*QYUoc+U5%SRa=k@fAvC9f18t7^&8A;y%za(wKN<NybxJ8rFAQXf
zG-jTW?(8F3Ihu8MN>C4Z%n0U~-)xxYtFdqJm|sZ7ARQy2605yen(;!jQELWu684j{
z$;kiRWh4K`et?nxi#a3zw@Aou<o~>7hRpyY|2O*oU29|cjbr?OMCQY=t5<aPE(?-^
zHhhB1P0L=wFT;mnVKJ0vX&K(uj-$awbSDyV@u0^%EbRv?hpQ{+u*XTORY<`N+gows
zC?~KJKJl=J-dleSCvlokP$-@T4~tIheixXH{NKp`jr_kbfQ<j=9w%=icnH;;;=Bff
z;lf-3jApZWAKGp$*ftlZDR8Iel4>-SU|*RjiN9Uf#8UP4Jt&3swjsC)9|w_2SR$1)
zW|zC>us*H@#?7N~^O%`7m}9<s2h*?YG2d1A9Ijh!YX|>?6_Ld6sjds~|2&KkV}O(T
zUw%L-yhML2s|qjEF4Auyb>B+h2l?r)OJBkN@&+Z5`agcU)b!k$@9UG6Umwd?$Npc^
zAIJHBqy<TWUU?NuG5LGfd(H%eTzDgnT<n>6KL43=um8S1HB-LZFP59f#6m8gHz-N~
z>yL9>Z<qVUHFJWvGWBJO?)L4ssc?FY$`?U_2>jhKdKE`O^F}30dKB2R8Fmip&3hRI
zI-8$9SH&VDISPf16%ke&JAO;}@Z=yX5<}v%^Rupt#gP5T3z|;i1@OBfiSSMH+1W+k
zUUhbaJs(8@+-FG2%b;9bY&OM?)3g`;IEmVBcgQ~l{khpFa*ph|pzSwed;ZYH0jdIS
zQDh8%29C=M&A>_Qs_=uTg@{(L%yj&m<<G%#DP`dg2fKb`e<&h&$&hjUMTcS07l+VC
zhgYAt-ONk(V=!EiF)aG~D11Yv(Vf-51kX9ivw}~V?PhS0#s60zJu68y7zymzY#WeK
z{~FY1B=sSDO7w)h0@~Pvz?LTJS%}wwef~k<Lz6!7{I*kXqFPZeVRwFB2h+tYw^c6=
zgV^h){|)Guq3A1i;37kQP!;RtZ^3dtV<{HuClnq#+xzgWxg#37*84eF&dCxNL*E%d
zm#8i+*$;xmUZAGU3O5JJcZfpD;U4PxceyXw3l0*>xjwO4pPgS08f_F^iQ*4Hyoj~A
zD;n)cLm#DlWmWS&dP-BEC-8*e#;wn<EPHMg#KCrASFT-CYnFJ2tjpGDm>&K)9%A&t
zI^fC7=2%Gf89oTZA#G_75zn*xHIjVXxF2#?e&THco$S3b;qE$-{pMtN<Np4V=L=|B
z$2rsV<_j5pe?8a}em7|(WRr~%nc69e4RH*FXAo7INO|+k2|1qZ*}A*6QvYZx*?Mzw
zVq&80#~8h$G08bBPyVnx`O<{SOBtggOx`?>$cdtSot)i$Yi4uuEzUP3rKHbs9uw^4
zthiJig%X!HFXdFq6G};H_!m1!k)*g&Y1om+WYkhVZw-gjYhq_OEaUHJ$Pw2bj8MBQ
zdGaT?acoX8MI$$>L8pk*n^!_qCa~Pn@l;o%0)Lt!Mpi08ctjoKfb3(w*U4wHC!=Ju
znN=@uuIbGlCPdF1+{|4}+;L8YRg60koej~lAR@&|I~odGjxS3+^CC)3^)%jI-Ng$h
zelopzI+V9Fe4kb#`pv5o6U$z(MWzPm#h8B4O|qs(+%)S`_ei^Hv0<h+C!eD}SHTd5
zSy23>y&hr1yS#ZB*evl3hm=o+3#{rf^k$e$YdT1wgTfwyy5~@cn=6zKwkDs1u#`gN
zoY1xMW=|}r+${ge9$PALAfI~6E813`KAbMsZ@+!(?lkg7V>kOPmypMiHcdm*@~3>E
zTz>oZ%$-|z?%J>0(}xSV#=>p9E6PvG7}IF}VanVz|1F;hnTAs1|7f@>qSljJo3e#&
zy=V=gFn-S%?aI9D<2<a1jk13|%Ra1VP)cgSo(7YBg4-fI;(juk_LDW)8PM4gX694~
zBg*%LKO9n<Gvl=^>ds7oE>N5)(3#~_aeQA;Mk#e4nR?b~pUeA_97a4+CesOxb8|uM
zWal{RE6oOqhe|<=$zFMk{&E}lrXZ>O7lp+KO`Mcvt=}HBHt?SLSDxx~DXsDUV*I}t
z|1UiXz{dZx@&EiQD*xqE=xad}-%mB+L@=!Fm3)~afJkYXJ~4D^kW66P;oe#^y5aI2
z3bk(I8>UMY0CHqaZ-KtIYBE5`Z}x0Ja|FE64VM~CEUziP7#up%UN<SqFzc#bMoKWc
z;kof?m*0Zk7f8Mu`v!Hx3k{xU$*2H9FzM_UswWYLA!MfoEGGP_G!e7-6Z#*ln<d9e
zN<V%7zXwJ?zcv`uKk9lt^j7gPv|P*T7<#H@)l0>Ge-QyKt6o$`%Sy#3G@5(S9WAR~
ze5z&Di|o>}>LtX^w%BTkVqPFBr7G^_&8oN;n^rL)E$ff0C#A^pOaJ&MuMHj!l&q~#
zo?8&}CKK&jLDyk}+_7&s4eXmtxmU-pYWKHtzL-Cb`!mv4GJi?WV!vkJOW^9JU%WYc
zdc^3{Fq6gM$@n42`BKgimi<g(M~gNb=ra3%s06AEv;UW1)5+}r<@=&$|Ih6Inf*Vr
z|7Z69%>EyC4$b~wsx6wYTJn|2F>6_4|Kac0ZqR~aLc?xC!^OT@kKLBDC+N&G`(3O<
zsw<U;%k!U<H=L&9x4ey|mCEc=4bSVM6>hB6R%fbr?oK7G@ai}_Oof__U5|o;SlFJw
z9oXA+u<z8=_`Tg*_gC6U*iPtNwnlJp?<O$gxQHUvxnhZf<{c-0!=APUX`@ZVlV<<V
z?EjhbA2LS`#{W~7jEc9mR4W%o>zt)90h&aC;`&@tpuSp=nK5475RqueG<x4Ij3!MU
p9Ucmqigh3ds43o<7_Ad$GeNU!!+7KWi99-)J-)61@~ztA`(LxN2*m&Z

diff --git a/abc.plg b/abc.plg
index 844bfe4e2..1e02d8fb7 100644
--- a/abc.plg
+++ b/abc.plg
@@ -6,284 +6,13 @@
 --------------------Configuration: abc - Win32 Release--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2D56.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F49.tmp" with contents
 [
 /nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\opt\cut" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c 
-"C:\_projects\abc\src\base\abc\abc.c"
-"C:\_projects\abc\src\base\abc\abcAig.c"
-"C:\_projects\abc\src\base\abc\abcAttach.c"
-"C:\_projects\abc\src\base\abc\abcBalance.c"
-"C:\_projects\abc\src\base\abc\abcCheck.c"
-"C:\_projects\abc\src\base\abc\abcCollapse.c"
-"C:\_projects\abc\src\base\abc\abcCreate.c"
-"C:\_projects\abc\src\base\abc\abcCut.c"
-"C:\_projects\abc\src\base\abc\abcDfs.c"
-"C:\_projects\abc\src\base\abc\abcDsd.c"
-"C:\_projects\abc\src\base\abc\abcFanio.c"
-"C:\_projects\abc\src\base\abc\abcFpga.c"
-"C:\_projects\abc\src\base\abc\abcFraig.c"
-"C:\_projects\abc\src\base\abc\abcFunc.c"
-"C:\_projects\abc\src\base\abc\abcFxu.c"
-"C:\_projects\abc\src\base\abc\abcLatch.c"
-"C:\_projects\abc\src\base\abc\abcMap.c"
-"C:\_projects\abc\src\base\abc\abcMinBase.c"
-"C:\_projects\abc\src\base\abc\abcMiter.c"
-"C:\_projects\abc\src\base\abc\abcNames.c"
-"C:\_projects\abc\src\base\abc\abcNetlist.c"
-"C:\_projects\abc\src\base\abc\abcPrint.c"
-"C:\_projects\abc\src\base\abc\abcReconv.c"
-"C:\_projects\abc\src\base\abc\abcRefactor.c"
-"C:\_projects\abc\src\base\abc\abcRefs.c"
-"C:\_projects\abc\src\base\abc\abcRenode.c"
-"C:\_projects\abc\src\base\abc\abcRewrite.c"
-"C:\_projects\abc\src\base\abc\abcSat.c"
-"C:\_projects\abc\src\base\abc\abcSeq.c"
-"C:\_projects\abc\src\base\abc\abcSeqRetime.c"
-"C:\_projects\abc\src\base\abc\abcShow.c"
-"C:\_projects\abc\src\base\abc\abcSop.c"
-"C:\_projects\abc\src\base\abc\abcStrash.c"
-"C:\_projects\abc\src\base\abc\abcSweep.c"
-"C:\_projects\abc\src\base\abc\abcTiming.c"
-"C:\_projects\abc\src\base\abc\abcUnreach.c"
-"C:\_projects\abc\src\base\abc\abcUtil.c"
-"C:\_projects\abc\src\base\abc\abcVerify.c"
 "C:\_projects\abc\src\base\cmd\cmd.c"
-"C:\_projects\abc\src\base\cmd\cmdAlias.c"
-"C:\_projects\abc\src\base\cmd\cmdApi.c"
-"C:\_projects\abc\src\base\cmd\cmdFlag.c"
-"C:\_projects\abc\src\base\cmd\cmdHist.c"
-"C:\_projects\abc\src\base\cmd\cmdUtils.c"
-"C:\_projects\abc\src\base\io\io.c"
-"C:\_projects\abc\src\base\io\ioRead.c"
-"C:\_projects\abc\src\base\io\ioReadBench.c"
-"C:\_projects\abc\src\base\io\ioReadBlif.c"
-"C:\_projects\abc\src\base\io\ioReadEdif.c"
-"C:\_projects\abc\src\base\io\ioReadPla.c"
-"C:\_projects\abc\src\base\io\ioReadVerilog.c"
-"C:\_projects\abc\src\base\io\ioUtil.c"
-"C:\_projects\abc\src\base\io\ioWriteBench.c"
-"C:\_projects\abc\src\base\io\ioWriteBlif.c"
-"C:\_projects\abc\src\base\io\ioWriteCnf.c"
-"C:\_projects\abc\src\base\io\ioWritePla.c"
-"C:\_projects\abc\src\base\main\main.c"
-"C:\_projects\abc\src\base\main\mainFrame.c"
-"C:\_projects\abc\src\base\main\mainInit.c"
-"C:\_projects\abc\src\base\main\mainUtils.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddAbs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddApply.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddFind.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddInv.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddIte.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddNeg.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddWalsh.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAndAbs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAnneal.c"
-"C:\_projects\abc\src\bdd\cudd\cuddApa.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAPI.c"
-"C:\_projects\abc\src\bdd\cudd\cuddApprox.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBddAbs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBddCorr.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBddIte.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBridge.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCache.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCheck.c"
-"C:\_projects\abc\src\bdd\cudd\cuddClip.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCof.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCompose.c"
-"C:\_projects\abc\src\bdd\cudd\cuddDecomp.c"
-"C:\_projects\abc\src\bdd\cudd\cuddEssent.c"
-"C:\_projects\abc\src\bdd\cudd\cuddExact.c"
-"C:\_projects\abc\src\bdd\cudd\cuddExport.c"
-"C:\_projects\abc\src\bdd\cudd\cuddGenCof.c"
-"C:\_projects\abc\src\bdd\cudd\cuddGenetic.c"
-"C:\_projects\abc\src\bdd\cudd\cuddGroup.c"
-"C:\_projects\abc\src\bdd\cudd\cuddHarwell.c"
-"C:\_projects\abc\src\bdd\cudd\cuddInit.c"
-"C:\_projects\abc\src\bdd\cudd\cuddInteract.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLCache.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLevelQ.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLinear.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLiteral.c"
-"C:\_projects\abc\src\bdd\cudd\cuddMatMult.c"
-"C:\_projects\abc\src\bdd\cudd\cuddPriority.c"
-"C:\_projects\abc\src\bdd\cudd\cuddRead.c"
-"C:\_projects\abc\src\bdd\cudd\cuddRef.c"
-"C:\_projects\abc\src\bdd\cudd\cuddReorder.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSat.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSign.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSolve.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSplit.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSubsetHB.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSubsetSP.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSymmetry.c"
-"C:\_projects\abc\src\bdd\cudd\cuddTable.c"
-"C:\_projects\abc\src\bdd\cudd\cuddUtil.c"
-"C:\_projects\abc\src\bdd\cudd\cuddWindow.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddCount.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddFuncs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddGroup.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddIsop.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddLin.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddMisc.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddPort.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddReord.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddSetop.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddSymm.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddUtil.c"
-"C:\_projects\abc\src\bdd\epd\epd.c"
-"C:\_projects\abc\src\bdd\mtr\mtrBasic.c"
-"C:\_projects\abc\src\bdd\mtr\mtrGroup.c"
-"C:\_projects\abc\src\bdd\parse\parseCore.c"
-"C:\_projects\abc\src\bdd\parse\parseStack.c"
-"C:\_projects\abc\src\bdd\dsd\dsdApi.c"
-"C:\_projects\abc\src\bdd\dsd\dsdCheck.c"
-"C:\_projects\abc\src\bdd\dsd\dsdLocal.c"
-"C:\_projects\abc\src\bdd\dsd\dsdMan.c"
-"C:\_projects\abc\src\bdd\dsd\dsdProc.c"
-"C:\_projects\abc\src\bdd\dsd\dsdTree.c"
-"C:\_projects\abc\src\bdd\reo\reoApi.c"
-"C:\_projects\abc\src\bdd\reo\reoCore.c"
-"C:\_projects\abc\src\bdd\reo\reoProfile.c"
-"C:\_projects\abc\src\bdd\reo\reoSift.c"
-"C:\_projects\abc\src\bdd\reo\reoSwap.c"
-"C:\_projects\abc\src\bdd\reo\reoTest.c"
-"C:\_projects\abc\src\bdd\reo\reoTransfer.c"
-"C:\_projects\abc\src\bdd\reo\reoUnits.c"
-"C:\_projects\abc\src\sop\mvc\mvc.c"
-"C:\_projects\abc\src\sop\mvc\mvcApi.c"
-"C:\_projects\abc\src\sop\mvc\mvcCompare.c"
-"C:\_projects\abc\src\sop\mvc\mvcContain.c"
-"C:\_projects\abc\src\sop\mvc\mvcCover.c"
-"C:\_projects\abc\src\sop\mvc\mvcCube.c"
-"C:\_projects\abc\src\sop\mvc\mvcDivide.c"
-"C:\_projects\abc\src\sop\mvc\mvcDivisor.c"
-"C:\_projects\abc\src\sop\mvc\mvcList.c"
-"C:\_projects\abc\src\sop\mvc\mvcLits.c"
-"C:\_projects\abc\src\sop\mvc\mvcMan.c"
-"C:\_projects\abc\src\sop\mvc\mvcOpAlg.c"
-"C:\_projects\abc\src\sop\mvc\mvcOpBool.c"
-"C:\_projects\abc\src\sop\mvc\mvcPrint.c"
-"C:\_projects\abc\src\sop\mvc\mvcSort.c"
-"C:\_projects\abc\src\sop\mvc\mvcUtils.c"
-"C:\_projects\abc\src\sop\ft\ftFactor.c"
-"C:\_projects\abc\src\sop\ft\ftPrint.c"
-"C:\_projects\abc\src\sat\asat\added.c"
-"C:\_projects\abc\src\sat\asat\solver.c"
-"C:\_projects\abc\src\sat\msat\msatActivity.c"
-"C:\_projects\abc\src\sat\msat\msatClause.c"
-"C:\_projects\abc\src\sat\msat\msatClauseVec.c"
-"C:\_projects\abc\src\sat\msat\msatMem.c"
-"C:\_projects\abc\src\sat\msat\msatOrderJ.c"
-"C:\_projects\abc\src\sat\msat\msatQueue.c"
-"C:\_projects\abc\src\sat\msat\msatRead.c"
-"C:\_projects\abc\src\sat\msat\msatSolverApi.c"
-"C:\_projects\abc\src\sat\msat\msatSolverCore.c"
-"C:\_projects\abc\src\sat\msat\msatSolverIo.c"
-"C:\_projects\abc\src\sat\msat\msatSolverSearch.c"
-"C:\_projects\abc\src\sat\msat\msatSort.c"
-"C:\_projects\abc\src\sat\msat\msatVec.c"
-"C:\_projects\abc\src\sat\fraig\fraigApi.c"
-"C:\_projects\abc\src\sat\fraig\fraigCanon.c"
-"C:\_projects\abc\src\sat\fraig\fraigFanout.c"
-"C:\_projects\abc\src\sat\fraig\fraigFeed.c"
-"C:\_projects\abc\src\sat\fraig\fraigMan.c"
-"C:\_projects\abc\src\sat\fraig\fraigMem.c"
-"C:\_projects\abc\src\sat\fraig\fraigNode.c"
-"C:\_projects\abc\src\sat\fraig\fraigPrime.c"
-"C:\_projects\abc\src\sat\fraig\fraigSat.c"
-"C:\_projects\abc\src\sat\fraig\fraigTable.c"
-"C:\_projects\abc\src\sat\fraig\fraigUtil.c"
-"C:\_projects\abc\src\sat\fraig\fraigVec.c"
-"C:\_projects\abc\src\sat\sim\simMan.c"
-"C:\_projects\abc\src\sat\sim\simSat.c"
-"C:\_projects\abc\src\sat\sim\simSupp.c"
-"C:\_projects\abc\src\sat\sim\simSym.c"
-"C:\_projects\abc\src\sat\sim\simUnate.c"
-"C:\_projects\abc\src\sat\sim\simUtils.c"
-"C:\_projects\abc\src\opt\fxu\fxu.c"
-"C:\_projects\abc\src\opt\fxu\fxuCreate.c"
-"C:\_projects\abc\src\opt\fxu\fxuHeapD.c"
-"C:\_projects\abc\src\opt\fxu\fxuHeapS.c"
-"C:\_projects\abc\src\opt\fxu\fxuList.c"
-"C:\_projects\abc\src\opt\fxu\fxuMatrix.c"
-"C:\_projects\abc\src\opt\fxu\fxuPair.c"
-"C:\_projects\abc\src\opt\fxu\fxuPrint.c"
-"C:\_projects\abc\src\opt\fxu\fxuReduce.c"
-"C:\_projects\abc\src\opt\fxu\fxuSelect.c"
-"C:\_projects\abc\src\opt\fxu\fxuSingle.c"
-"C:\_projects\abc\src\opt\fxu\fxuUpdate.c"
-"C:\_projects\abc\src\opt\rwr\rwrEva.c"
-"C:\_projects\abc\src\opt\rwr\rwrExp.c"
-"C:\_projects\abc\src\opt\rwr\rwrLib.c"
-"C:\_projects\abc\src\opt\rwr\rwrMan.c"
-"C:\_projects\abc\src\opt\rwr\rwrPrint.c"
-"C:\_projects\abc\src\opt\rwr\rwrUtil.c"
-"C:\_projects\abc\src\opt\cut\cutMan.c"
-"C:\_projects\abc\src\opt\cut\cutMerge.c"
-"C:\_projects\abc\src\opt\cut\cutNode.c"
-"C:\_projects\abc\src\opt\cut\cutSeq.c"
-"C:\_projects\abc\src\opt\cut\cutTable.c"
-"C:\_projects\abc\src\opt\cut\cutTruth.c"
-"C:\_projects\abc\src\map\fpga\fpga.c"
-"C:\_projects\abc\src\map\fpga\fpgaCore.c"
-"C:\_projects\abc\src\map\fpga\fpgaCreate.c"
-"C:\_projects\abc\src\map\fpga\fpgaCut.c"
-"C:\_projects\abc\src\map\fpga\fpgaCutUtils.c"
-"C:\_projects\abc\src\map\fpga\fpgaFanout.c"
-"C:\_projects\abc\src\map\fpga\fpgaLib.c"
-"C:\_projects\abc\src\map\fpga\fpgaMatch.c"
-"C:\_projects\abc\src\map\fpga\fpgaTime.c"
-"C:\_projects\abc\src\map\fpga\fpgaTruth.c"
-"C:\_projects\abc\src\map\fpga\fpgaUtils.c"
-"C:\_projects\abc\src\map\fpga\fpgaVec.c"
-"C:\_projects\abc\src\map\mapper\mapper.c"
-"C:\_projects\abc\src\map\mapper\mapperCanon.c"
-"C:\_projects\abc\src\map\mapper\mapperCore.c"
-"C:\_projects\abc\src\map\mapper\mapperCreate.c"
-"C:\_projects\abc\src\map\mapper\mapperCut.c"
-"C:\_projects\abc\src\map\mapper\mapperCutUtils.c"
-"C:\_projects\abc\src\map\mapper\mapperFanout.c"
-"C:\_projects\abc\src\map\mapper\mapperLib.c"
-"C:\_projects\abc\src\map\mapper\mapperMatch.c"
-"C:\_projects\abc\src\map\mapper\mapperRefs.c"
-"C:\_projects\abc\src\map\mapper\mapperSuper.c"
-"C:\_projects\abc\src\map\mapper\mapperTable.c"
-"C:\_projects\abc\src\map\mapper\mapperTime.c"
-"C:\_projects\abc\src\map\mapper\mapperTree.c"
-"C:\_projects\abc\src\map\mapper\mapperTruth.c"
-"C:\_projects\abc\src\map\mapper\mapperUtils.c"
-"C:\_projects\abc\src\map\mapper\mapperVec.c"
-"C:\_projects\abc\src\map\mio\mio.c"
-"C:\_projects\abc\src\map\mio\mioApi.c"
-"C:\_projects\abc\src\map\mio\mioFunc.c"
-"C:\_projects\abc\src\map\mio\mioRead.c"
-"C:\_projects\abc\src\map\mio\mioUtils.c"
-"C:\_projects\abc\src\map\super\super.c"
-"C:\_projects\abc\src\map\super\superAnd.c"
-"C:\_projects\abc\src\map\super\superGate.c"
-"C:\_projects\abc\src\map\super\superWrite.c"
-"C:\_projects\abc\src\misc\extra\extraUtilBdd.c"
-"C:\_projects\abc\src\misc\extra\extraUtilBitMatrix.c"
-"C:\_projects\abc\src\misc\extra\extraUtilCanon.c"
-"C:\_projects\abc\src\misc\extra\extraUtilFile.c"
-"C:\_projects\abc\src\misc\extra\extraUtilMemory.c"
-"C:\_projects\abc\src\misc\extra\extraUtilMisc.c"
-"C:\_projects\abc\src\misc\extra\extraUtilProgress.c"
-"C:\_projects\abc\src\misc\extra\extraUtilReader.c"
-"C:\_projects\abc\src\misc\st\st.c"
-"C:\_projects\abc\src\misc\st\stmm.c"
-"C:\_projects\abc\src\misc\util\cpu_stats.c"
-"C:\_projects\abc\src\misc\util\cpu_time.c"
-"C:\_projects\abc\src\misc\util\datalimit.c"
-"C:\_projects\abc\src\misc\util\getopt.c"
-"C:\_projects\abc\src\misc\util\pathsearch.c"
-"C:\_projects\abc\src\misc\util\safe_mem.c"
-"C:\_projects\abc\src\misc\util\strsav.c"
-"C:\_projects\abc\src\misc\util\texpand.c"
-"C:\_projects\abc\src\opt\rwr\rwrDec.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2D56.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2D57.tmp" with contents
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F49.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F4A.tmp" with contents
 [
 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:no /pdb:"Release/abc.pdb" /machine:I386 /out:"_TEST/abc.exe" 
 .\Release\abc.obj
@@ -477,6 +206,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\simSym.obj
 .\Release\simUnate.obj
 .\Release\simUtils.obj
+.\Release\csat_apis.obj
 .\Release\fxu.obj
 .\Release\fxuCreate.obj
 .\Release\fxuHeapD.obj
@@ -489,6 +219,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\fxuSelect.obj
 .\Release\fxuSingle.obj
 .\Release\fxuUpdate.obj
+.\Release\rwrDec.obj
 .\Release\rwrEva.obj
 .\Release\rwrExp.obj
 .\Release\rwrLib.obj
@@ -557,300 +288,13 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\safe_mem.obj
 .\Release\strsav.obj
 .\Release\texpand.obj
-.\Release\rwrDec.obj
 ]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2D57.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F4A.tmp"
 <h3>Output Window</h3>
 Compiling...
-abc.c
-abcAig.c
-abcAttach.c
-abcBalance.c
-abcCheck.c
-abcCollapse.c
-abcCreate.c
-abcCut.c
-abcDfs.c
-abcDsd.c
-abcFanio.c
-abcFpga.c
-abcFraig.c
-abcFunc.c
-abcFxu.c
-abcLatch.c
-abcMap.c
-abcMinBase.c
-abcMiter.c
-abcNames.c
-abcNetlist.c
-abcPrint.c
-abcReconv.c
-abcRefactor.c
-abcRefs.c
-abcRenode.c
-abcRewrite.c
-abcSat.c
-abcSeq.c
-abcSeqRetime.c
-abcShow.c
-abcSop.c
-abcStrash.c
-abcSweep.c
-abcTiming.c
-abcUnreach.c
-abcUtil.c
-abcVerify.c
 cmd.c
-cmdAlias.c
-cmdApi.c
-cmdFlag.c
-cmdHist.c
-cmdUtils.c
-io.c
-ioRead.c
-ioReadBench.c
-ioReadBlif.c
-ioReadEdif.c
-ioReadPla.c
-ioReadVerilog.c
-ioUtil.c
-ioWriteBench.c
-ioWriteBlif.c
-ioWriteCnf.c
-ioWritePla.c
-main.c
-mainFrame.c
-mainInit.c
-mainUtils.c
-cuddAddAbs.c
-cuddAddApply.c
-cuddAddFind.c
-cuddAddInv.c
-cuddAddIte.c
-cuddAddNeg.c
-cuddAddWalsh.c
-cuddAndAbs.c
-cuddAnneal.c
-cuddApa.c
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(181) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(213) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(530) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(588) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data
-cuddAPI.c
-cuddApprox.c
-cuddBddAbs.c
-cuddBddCorr.c
-cuddBddIte.c
-cuddBridge.c
-cuddCache.c
-C:\_projects\abc\src\bdd\cudd\cuddCache.c(902) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddCheck.c
-cuddClip.c
-cuddCof.c
-cuddCompose.c
-cuddDecomp.c
-cuddEssent.c
-cuddExact.c
-cuddExport.c
-cuddGenCof.c
-cuddGenetic.c
-cuddGroup.c
-C:\_projects\abc\src\bdd\cudd\cuddGroup.c(2062) : warning C4018: '<=' : signed/unsigned mismatch
-cuddHarwell.c
-cuddInit.c
-cuddInteract.c
-cuddLCache.c
-C:\_projects\abc\src\bdd\cudd\cuddLCache.c(1387) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddLevelQ.c
-cuddLinear.c
-cuddLiteral.c
-cuddMatMult.c
-cuddPriority.c
-cuddRead.c
-cuddRef.c
-cuddReorder.c
-C:\_projects\abc\src\bdd\cudd\cuddReorder.c(395) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddSat.c
-C:\_projects\abc\src\bdd\cudd\cuddReorder.c(2016) : warning C4700: local variable 'minLevel' used without having been initialized
-C:\_projects\abc\src\bdd\cudd\cuddReorder.c(2020) : warning C4700: local variable 'maxLevel' used without having been initialized
-cuddSign.c
-cuddSolve.c
-cuddSplit.c
-cuddSubsetHB.c
-cuddSubsetSP.c
-cuddSymmetry.c
-cuddTable.c
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(1822) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(1927) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(2235) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(2303) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(2358) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddUtil.c
-cuddWindow.c
-cuddZddCount.c
-cuddZddFuncs.c
-cuddZddGroup.c
-cuddZddIsop.c
-cuddZddLin.c
-cuddZddMisc.c
-cuddZddPort.c
-cuddZddReord.c
-cuddZddSetop.c
-cuddZddSymm.c
-cuddZddUtil.c
-epd.c
-mtrBasic.c
-mtrGroup.c
-parseCore.c
-parseStack.c
-dsdApi.c
-dsdCheck.c
-dsdLocal.c
-dsdMan.c
-dsdProc.c
-dsdTree.c
-reoApi.c
-reoCore.c
-reoProfile.c
-reoSift.c
-reoSwap.c
-reoTest.c
-reoTransfer.c
-reoUnits.c
-mvc.c
-mvcApi.c
-mvcCompare.c
-mvcContain.c
-mvcCover.c
-mvcCube.c
-mvcDivide.c
-mvcDivisor.c
-mvcList.c
-mvcLits.c
-mvcMan.c
-mvcOpAlg.c
-mvcOpBool.c
-mvcPrint.c
-mvcSort.c
-mvcUtils.c
-ftFactor.c
-ftPrint.c
-added.c
-solver.c
-msatActivity.c
-msatClause.c
-msatClauseVec.c
-msatMem.c
-msatOrderJ.c
-msatQueue.c
-msatRead.c
-msatSolverApi.c
-msatSolverCore.c
-msatSolverIo.c
-msatSolverSearch.c
-msatSort.c
-msatVec.c
-fraigApi.c
-fraigCanon.c
-fraigFanout.c
-fraigFeed.c
-fraigMan.c
-fraigMem.c
-fraigNode.c
-fraigPrime.c
-fraigSat.c
-fraigTable.c
-fraigUtil.c
-fraigVec.c
-simMan.c
-simSat.c
-simSupp.c
-simSym.c
-simUnate.c
-simUtils.c
-fxu.c
-fxuCreate.c
-fxuHeapD.c
-fxuHeapS.c
-fxuList.c
-fxuMatrix.c
-fxuPair.c
-fxuPrint.c
-fxuReduce.c
-fxuSelect.c
-fxuSingle.c
-fxuUpdate.c
-rwrEva.c
-rwrExp.c
-rwrLib.c
-rwrMan.c
-rwrPrint.c
-rwrUtil.c
-cutMan.c
-cutMerge.c
-cutNode.c
-cutSeq.c
-cutTable.c
-cutTruth.c
-fpga.c
-fpgaCore.c
-fpgaCreate.c
-fpgaCut.c
-fpgaCutUtils.c
-fpgaFanout.c
-fpgaLib.c
-fpgaMatch.c
-fpgaTime.c
-fpgaTruth.c
-fpgaUtils.c
-fpgaVec.c
-mapper.c
-mapperCanon.c
-mapperCore.c
-mapperCreate.c
-mapperCut.c
-mapperCutUtils.c
-mapperFanout.c
-mapperLib.c
-mapperMatch.c
-mapperRefs.c
-mapperSuper.c
-mapperTable.c
-mapperTime.c
-mapperTree.c
-mapperTruth.c
-mapperUtils.c
-mapperVec.c
-mio.c
-mioApi.c
-mioFunc.c
-mioRead.c
-mioUtils.c
-super.c
-superAnd.c
-superGate.c
-superWrite.c
-extraUtilBdd.c
-extraUtilBitMatrix.c
-extraUtilCanon.c
-extraUtilFile.c
-extraUtilMemory.c
-extraUtilMisc.c
-extraUtilProgress.c
-extraUtilReader.c
-st.c
-stmm.c
-cpu_stats.c
-cpu_time.c
-datalimit.c
-getopt.c
-pathsearch.c
-safe_mem.c
-strsav.c
-texpand.c
-rwrDec.c
 Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2D59.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F4C.tmp" with contents
 [
 /nologo /o"Release/abc.bsc" 
 .\Release\abc.sbr
@@ -1044,6 +488,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2D59.tmp" with cont
 .\Release\simSym.sbr
 .\Release\simUnate.sbr
 .\Release\simUtils.sbr
+.\Release\csat_apis.sbr
 .\Release\fxu.sbr
 .\Release\fxuCreate.sbr
 .\Release\fxuHeapD.sbr
@@ -1056,6 +501,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2D59.tmp" with cont
 .\Release\fxuSelect.sbr
 .\Release\fxuSingle.sbr
 .\Release\fxuUpdate.sbr
+.\Release\rwrDec.sbr
 .\Release\rwrEva.sbr
 .\Release\rwrExp.sbr
 .\Release\rwrLib.sbr
@@ -1123,16 +569,15 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2D59.tmp" with cont
 .\Release\pathsearch.sbr
 .\Release\safe_mem.sbr
 .\Release\strsav.sbr
-.\Release\texpand.sbr
-.\Release\rwrDec.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2D59.tmp"
+.\Release\texpand.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP2F4C.tmp"
 Creating browse info file...
 <h3>Output Window</h3>
 
 
 
 <h3>Results</h3>
-abc.exe - 0 error(s), 15 warning(s)
+abc.exe - 0 error(s), 0 warning(s)
 </pre>
 </body>
 </html>
diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index c2b739b5b..f8871ba9b 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -1065,6 +1065,11 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
+        return 1;
+    }
 
     // modify the current network
     Abc_NtkCleanup( pNtk, 0 );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 200d25012..2366aa10e 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -406,6 +406,7 @@ extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
 extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis );
+extern Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
 extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
@@ -532,10 +533,13 @@ extern void               Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
+extern char *             Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
+extern char *             Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
 extern char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
+extern char *             Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
 extern char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
@@ -559,6 +563,7 @@ extern void               Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_In
 extern void               Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
 /*=== abcStrash.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
+extern Abc_Obj_t *        Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 extern Abc_Obj_t *        Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm );
 extern int                Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index d42fdac0a..2200bea15 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -172,6 +172,10 @@ Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew )
         Abc_ObjSetFaninL0( pObj->pCopy, Abc_ObjFaninL0(pObj) );
         Abc_ObjSetFaninL1( pObj->pCopy, Abc_ObjFaninL1(pObj) );
     }
+    // relink the choice nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( pObj->pData )
+            pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
     Vec_PtrFree( vNodes );
     // relink the CO nodes
     Abc_NtkForEachCo( pMan->pNtkAig, pObj, i )
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index ee77cd027..e8b00271e 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -361,7 +361,8 @@ bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
 bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanin, * pFanout;
-    int i, k, Value = 1;
+    int i, Value = 1;
+//    int k;
 
     // check the network
     if ( pObj->pNtk != pNtk )
@@ -395,7 +396,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
             Value = 0;
         }
     }
-
+/*
     // make sure fanins are not duplicated
     for ( i = 0; i < pObj->vFanins.nSize; i++ )
         for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
@@ -417,7 +418,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                 printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
             }
-
+*/
     return Value;
 }
 
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index 9f192979f..7de9ea3e3 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -333,7 +333,64 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
     Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
 
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the network composed of one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFinal, * pOther, * pNodePo;
+    int i;
+
+    assert( Abc_NtkIsLogic(pNtk) );
+    
+    // start the network
+    Abc_NtkCleanCopy( pNtk );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkNew->pName = util_strsav(pNtk->pName);
+
+    // collect the nodes in the TFI of the output
+    vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)vRoots->pArray, vRoots->nSize );
+    // create the PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    }
+    // copy the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = Abc_NodeStrash( pNtkNew->pManFunc, pObj );
+    Vec_PtrFree( vNodes );
+
+    // add the PO
+    pFinal = Abc_AigConst1( pNtkNew->pManFunc );
+    Vec_PtrForEachEntry( vRoots, pObj, i )
+    {
+        pOther = pObj->pCopy;
+        if ( Vec_IntEntry(vValues, i) == 0 )
+            pOther = Abc_ObjNot(pOther);
+        pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther );
+    }
+
+    // add the PO corresponding to this output
+    pNodePo = Abc_NtkCreatePo( pNtkNew );
+    Abc_ObjAddFanin( pNodePo, pFinal );
+    Abc_NtkLogicStoreName( pNodePo, "miter" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
     return pNtkNew;
 }
 
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index c0eb1c0ad..724c38777 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -89,7 +89,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     ProgressBar * pProgress;
     Fraig_Node_t * pNodeFraig;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pConst1;
+    Abc_Obj_t * pNode, * pConst1, * pReset;
     int i;
 
     assert( Abc_NtkIsAig(pNtk) );
@@ -102,6 +102,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
     pConst1 = Abc_AigConst1( pNtk->pManFunc );
+    pReset  = Abc_AigReset( pNtk->pManFunc );
 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
@@ -111,6 +112,8 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( pNode == pConst1 )
             pNodeFraig = Fraig_ManReadConst1(pMan);
+        else if ( pNode == pReset )
+            continue;
         else
             pNodeFraig = Fraig_NodeAnd( pMan, 
                 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index bfa418427..8e10b3916 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -254,23 +254,26 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
         if ( !Abc_NodeIsAigChoice(pObj) )
             continue;
         // create an OR gate
-        pNodeNew = Abc_NtkCreateNode(pNtk);
+        pNodeNew = Abc_NtkCreateNode(pNtkNew);
         // add fanins
         Vec_IntClear( pNtk->vIntTemp );
-        for ( k = 0, pFanin = pObj; pFanin; pFanin = pFanin->pData, k++ )
+        for ( pFanin = pObj; pFanin; pFanin = pFanin->pData )
         {
             Vec_IntPush( pNtk->vIntTemp, (int)(pObj->fPhase != pFanin->fPhase) );
             Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
         }
         // create the logic function
-        pNodeNew->pData = Abc_SopCreateOr( pNtk->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
+        pNodeNew->pData = Abc_SopCreateOrMultiCube( pNtkNew->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
         // set the new node
-        pObj->pCopy = pNodeNew;
+        pObj->pCopy->pCopy = pNodeNew;
     }
     // connect the internal nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_ObjForEachFanin( pObj, pFanin, k )
-            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+            if ( pFanin->pCopy->pCopy )
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
+            else
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     // connect the COs
     Abc_NtkFinalize( pNtk, pNtkNew );
     // fix the problem with complemented and duplicated CO edges
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index b6972d583..28e92889f 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -92,7 +92,39 @@ char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the constant 1 cover with 0 variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan )
+{
+    return Abc_SopRegister( pMan, " 1\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the constant 1 cover with 0 variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan )
+{
+    return Abc_SopRegister( pMan, " 0\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AND2 cover.]
 
   Description []
                
@@ -115,7 +147,7 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input AND cover.]
 
   Description []
                
@@ -136,7 +168,7 @@ char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input NAND cover.]
 
   Description []
                
@@ -158,7 +190,7 @@ char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input OR cover.]
 
   Description []
                
@@ -180,7 +212,32 @@ char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input OR cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
+{
+    char * pSop, * pCube;
+    int i;
+    pSop = Abc_SopStart( pMan, nVars, nVars );
+    i = 0;
+    Abc_SopForEachCube( pSop, nVars, pCube )
+    {
+        pCube[i] = '1' - (pfCompl? pfCompl[i] : 0);
+        i++;
+    }
+    return pSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the multi-input NOR cover.]
 
   Description []
                
@@ -201,7 +258,7 @@ char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input XOR cover.]
 
   Description []
                
@@ -218,7 +275,7 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the multi-input XNOR cover.]
 
   Description []
                
@@ -235,7 +292,7 @@ char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the inv cover.]
 
   Description []
                
@@ -251,7 +308,7 @@ char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Starts the buf cover.]
 
   Description []
                
@@ -367,18 +424,11 @@ int Abc_SopGetPhase( char * pSop )
 int Abc_SopGetIthCareLit( char * pSop, int i )
 {
     char * pCube;
-    int nVars, c;
+    int nVars;
     nVars = Abc_SopGetVarNum( pSop );
-    for ( c = 0; ; c++ )
-    {
-        // get the cube
-        pCube = pSop + c * (nVars + 3);
-        if ( *pCube == 0 )
-            break;
-        // get the literal
+    Abc_SopForEachCube( pSop, nVars, pCube )
         if ( pCube[i] != '-' )
             return pCube[i] - '0';
-    }
     return -1;
 }
 
@@ -520,6 +570,8 @@ bool Abc_SopIsAndType( char * pSop )
     for ( pCur = pSop; *pCur != ' '; pCur++ )
         if ( *pCur == '-' )
             return 0;
+    if ( pCur[1] != '1' )
+        return 0;
     return 1;
 }
 
@@ -537,14 +589,12 @@ bool Abc_SopIsAndType( char * pSop )
 bool Abc_SopIsOrType( char * pSop )
 {
     char * pCube, * pCur;
-    int nVars, nLits, c;
+    int nVars, nLits;
     nVars = Abc_SopGetVarNum( pSop );
-    for ( c = 0; ; c++ )
+    if ( nVars != Abc_SopGetCubeNum(pSop) )
+        return 0;
+    Abc_SopForEachCube( pSop, nVars, pCube )
     {
-        // get the cube
-        pCube = pSop + c * (nVars + 3);
-        if ( *pCube == 0 )
-            break;
         // count the number of literals in the cube
         nLits = 0;
         for ( pCur = pCube; *pCur != ' '; pCur++ )
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index 961e6c5f9..bf97c5bf2 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -28,7 +28,6 @@
 
 // static functions
 static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
-static Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 static Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
 static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
 
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index aa15c0af0..255791a70 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -335,7 +335,7 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
     int i, num;
     int size;
     int c;
-    num = 30;
+    num = 50;
 
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
diff --git a/src/base/main/main.c b/src/base/main/main.c
index ed1e929d3..a3fd979a1 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -209,7 +209,7 @@ int main( int argc, char * argv[] )
                 break;
         }
     }
-    
+     
     // if the memory should be freed, quit packages
     if ( fStatus == -2 ) 
     {
diff --git a/src/csat_apis.h b/src/csat_apis.h
deleted file mode 100644
index 0b0091679..000000000
--- a/src/csat_apis.h
+++ /dev/null
@@ -1,125 +0,0 @@
-//These are the APIs, enums and data structures that we use 
-//and expect from our use of CSAT.
-
-enum GateType
-{
-// GateType defines the gate type that can be added to circuit by
-// CSAT_AddGate();
-enum GateType
-{
-CSAT_CONST = 0,  // constant gate
-CSAT_BPI,    // boolean PI
-CSAT_BPPI,   // bit level PSEUDO PRIMARY INPUT
-CSAT_BAND,   // bit level AND
-CSAT_BNAND,  // bit level NAND
-CSAT_BOR,    // bit level OR
-CSAT_BNOR,   // bit level NOR
-CSAT_BXOR,   // bit level XOR
-CSAT_BXNOR,  // bit level XNOR
-CSAT_BINV,   // bit level INVERTER
-CSAT_BBUF,   // bit level BUFFER
-CSAT_BPPO,   // bit level PSEUDO PRIMARY OUTPUT
-CSAT_BPO,    // boolean PO
-};
-#endif
-
-//CSAT_StatusT defines the return value by CSAT_Solve();
-#ifndef _CSAT_STATUS_
-#define _CSAT_STATUS_
-enum CSAT_StatusT 
-{
-UNDETERMINED = 0,
-UNSATISFIABLE,
-SATISFIABLE,
-TIME_OUT,
-FRAME_OUT,
-NO_TARGET,
-ABORTED,
-SEQ_SATISFIABLE        
-};
-#endif
-
-
-// CSAT_OptionT defines the solver option about learning
-// which is used by CSAT_SetSolveOption();
-#ifndef _CSAT_OPTION_
-#define _CSAT_OPTION_
-enum CSAT_OptionT
-{
-BASE_LINE = 0,
-IMPLICT_LEARNING, //default
-EXPLICT_LEARNING
-};
-#endif
-
-#ifndef _CSAT_Target_Result
-#define _CSAT_Target_Result
-typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
-/*
-struct _CSAT_Target_ResultT
-{
-enum CSAT_StatusT status; //solve status of the target
-int num_dec;    //num of decisions to solve the target
-int num_imp;    //num of implications to solve the target
-int num_cftg;    //num of conflict gates learned 
-int num_cfts;    //num of conflict signals in conflict gates
-double time;    //time(in second) used to solver the target
-int no_sig;        // if "status" is SATISFIABLE, "no_sig" is the number of 
-                // primary inputs, if the "status" is TIME_OUT, "no_sig" is the
-                // number of constant signals found.
-char** names;    // if the "status" is SATISFIABLE, "names" is the name array of
-                // primary inputs, "values" is the value array of primary 
-                // inputs that satisfy the target. 
-                // if the "status" is TIME_OUT, "names" is the name array of
-                // constant signals found (signals at the root of decision 
-                // tree),"values" is the value array of constant signals found.
-int* values;
-};
-*/
-
-// create a new manager
-CSAT_Manager CSAT_InitManager(void);
-
-// set solver options for learning
-void CSAT_SetSolveOption(CSAT_Manager mng,enum CSAT_OptionT option);
-
-// add a gate to the circuit
-// the meaning of the parameters are:
-// type: the type of the gate to be added
-// name: the name of the gate to be added, name should be unique in a circuit.
-// nofi: number of fanins of the gate to be added;
-// fanins: the name array of fanins of the gate to be added
-int CSAT_AddGate(CSAT_Manager mng,
-            enum GateType type,
-            char* name,
-            int nofi,
-            char** fanins,
-            int dc_attr=0);
-
-// check if there are gates that are not used by any primary ouput.
-// if no such gates exist, return 1 else return 0;
-int CSAT_Check_Integrity(CSAT_Manager mng);
-
-// set time limit for solving a target.
-// runtime: time limit (in second).
-void CSAT_SetTimeLimit(CSAT_Manager mng ,int runtime);
-void CSAT_SetLearnLimit   (CSAT_Manager mng ,int num);
-void CSAT_SetSolveBacktrackLimit   (CSAT_Manager mng ,int num);
-void CSAT_SetLearnBacktrackLimit   (CSAT_Manager mng ,int num);
-void CSAT_EnableDump(CSAT_Manager mng ,char* dump_file);
-// the meaning of the parameters are:
-// nog: number of gates that are in the targets
-// names: name array of gates
-// values: value array of the corresponding gates given in "names" to be
-// solved. the relation of them is AND.
-int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
-// initialize the solver internal data structure.
-void CSAT_SolveInit(CSAT_Manager mng);
-void CSAT_AnalyzeTargets(CSAT_Manager mng);
-// solve the targets added by CSAT_AddTarget()
-enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng);
-// get the solve status of a target
-// TargetID: the target id returned by  CSAT_AddTarget().
-CSAT_Target_ResultT*
-CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
-void CSAT_Dump_Bench_File(CSAT_Manager mng);
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 6e127b278..1c291b331 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -125,7 +125,6 @@ extern void              Rwr_ManIncTravId( Rwr_Man_t * p );
 extern Rwr_Man_t *       Rwr_ManStart( bool fPrecompute );
 extern void              Rwr_ManStop( Rwr_Man_t * p );
 extern void              Rwr_ManPrintStats( Rwr_Man_t * p );
-extern void              Rwr_ManPrepareNetwork( Rwr_Man_t * p, Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *       Rwr_ManReadFanins( Rwr_Man_t * p );
 extern Vec_Int_t *       Rwr_ManReadDecs( Rwr_Man_t * p );
 extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 71db4b20c..d4772812b 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -162,27 +162,6 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
 */
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Assigns elementary cuts to the PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Rwr_ManPrepareNetwork( Rwr_Man_t * p, Abc_Ntk_t * pNtk )
-{
-    // save the fanout counters for all internal nodes
-//    p->vFanNums = Rwt_NtkFanoutCounters( pNtk );
-    // precompute the required times for all internal nodes
-//    p->vReqTimes = Abc_NtkGetRequiredLevels( pNtk );
-    // start the cut computation
-//    Rwr_NtkStartCuts( p, pNtk );
-}
-
 /**Function*************************************************************
 
   Synopsis    [Stops the resynthesis manager.]
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
new file mode 100644
index 000000000..eddd7270c
--- /dev/null
+++ b/src/sat/csat/csat_apis.c
@@ -0,0 +1,630 @@
+/**CFile****************************************************************
+
+  FileName    [csat_apis.h]
+
+  PackageName [Interface to CSAT.]
+
+  Synopsis    [APIs, enums, and data structures expected from the use of CSAT.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 28, 2005]
+
+  Revision    [$Id: csat_apis.h,v 1.00 2005/08/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+#include "csat_apis.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct CSAT_ManagerStruct_t
+{
+    // information about the problem
+    stmm_table *          tName2Node;    // the hash table mapping names to nodes
+    Abc_Ntk_t *           pNtk;          // the starting ABC network
+    Abc_Ntk_t *           pTarget;       // the AIG of the target
+    char *                pDumpFileName; // the name of the file to dump the target network
+    // solving parameters
+    int                   mode;          // 0 = baseline;  1 = resource-aware fraiging
+    Fraig_Params_t        Params;        // the set of parameters to call FRAIG package
+    // information about the target 
+    int                   nog;           // the numbers of gates in the target
+    Vec_Ptr_t *           vNodes;        // the gates in the target
+    Vec_Int_t *           vValues;       // the values of gate's outputs in the target
+    // solution
+    CSAT_Target_ResultT * pResult;       // the result of solving the target
+};
+
+static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars );
+static void CSAT_TargetResFree( CSAT_Target_ResultT * p );
+
+// some external procedures
+extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
+extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+CSAT_Manager CSAT_InitManager()
+{
+    CSAT_Manager_t * mng;
+    mng = ALLOC( CSAT_Manager_t, 1 );
+    memset( mng, 0, sizeof(CSAT_Manager_t) );
+    mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC_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 );
+    return mng;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_QuitManager( CSAT_Manager mng )
+{
+    if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
+    if ( mng->pNtk )       Abc_NtkDelete( mng->pNtk );
+    if ( mng->pTarget )    Abc_NtkDelete( mng->pTarget );
+    if ( mng->vNodes )     Vec_PtrFree( mng->vNodes );
+    if ( mng->vValues )    Vec_IntFree( mng->vValues );
+    FREE( mng->pDumpFileName );
+    free( mng );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets solver options for learning.]
+
+  Description [0 = baseline; 1 = resource-aware solving.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option )
+{
+    mng->mode = option;
+    if ( option == 0 )
+        printf( "CSAT_SetSolveOption: Setting baseline solving mode.\n" );
+    else if ( option == 1 )
+        printf( "CSAT_SetSolveOption: Setting resource-aware solving mode.\n" );
+    else
+        printf( "CSAT_SetSolveOption: Unknown option.\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds a gate to the circuit.]
+
+  Description [The meaning of the parameters are:
+    type: the type of the gate to be added
+    name: the name of the gate to be added, name should be unique in a circuit.
+    nofi: number of fanins of the gate to be added;
+    fanins: the name array of fanins of the gate to be added.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr )
+{
+    Abc_Obj_t * pObj, * pFanin;
+    char * pSop;
+    int i;
+
+    switch( type )
+    {
+    case CSAT_BPI:
+    case CSAT_BPPI:
+        if ( nofi != 0 )
+            { 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;
+        break;
+    case CSAT_CONST:
+    case CSAT_BAND:
+    case CSAT_BNAND:
+    case CSAT_BOR:
+    case CSAT_BNOR:
+    case CSAT_BXOR:
+    case CSAT_BXNOR:
+    case CSAT_BINV:
+    case CSAT_BBUF:
+        // create the node
+        pObj = Abc_NtkCreateNode( mng->pNtk );
+        // create the fanins
+        for ( i = 0; i < nofi; i++ )
+        {
+            if ( !stmm_lookup( mng->tName2Node, fanins[i], (char **)&pFanin ) )
+                { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; }
+            Abc_ObjAddFanin( pObj, pFanin );
+        }
+        // create the node function
+        switch( type )
+        {
+            case CSAT_CONST:
+                if ( nofi != 0 )
+                    { printf( "CSAT_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc );
+                break;
+            case CSAT_BAND:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BNAND:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BOR:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL );
+                break;
+            case CSAT_BNOR:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BXOR:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
+                if ( nofi > 2 )
+                    { printf( "CSAT_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateXor( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BXNOR:
+                if ( nofi < 1 )
+                    { printf( "CSAT_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
+                if ( nofi > 2 )
+                    { printf( "CSAT_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
+                pSop = Abc_SopCreateNxor( mng->pNtk->pManFunc, nofi );
+                break;
+            case CSAT_BINV:
+                if ( nofi != 1 )
+                    { printf( "CSAT_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+                pSop = Abc_SopCreateInv( mng->pNtk->pManFunc );
+                break;
+            case CSAT_BBUF:
+                if ( nofi != 1 )
+                    { printf( "CSAT_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+                pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc );
+                break;
+            default :
+                break;
+        }
+        Abc_ObjSetData( pObj, pSop );
+        break;
+    case CSAT_BPPO:
+    case CSAT_BPO:
+        if ( nofi != 1 )
+            { 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;
+        // 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; }
+        Abc_ObjAddFanin( pObj, pFanin );
+        break;
+    default:
+        printf( "CSAT_AddGate: Unknown gate type.\n" );
+        break;
+    }
+    if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) )
+        { printf( "CSAT_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks integraty of the manager.]
+
+  Description [Checks if there are gates that are not used by any primary output.
+  If no such gates exist, return 1 else return 0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CSAT_Check_Integrity( CSAT_Manager mng )
+{
+    Abc_Ntk_t * pNtk = mng->pNtk;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // this procedure also finalizes construction of the ABC network
+    Abc_NtkFixNonDrivenNets( pNtk );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext );
+    assert( Abc_NtkLatchNum(pNtk) == 0 );
+
+    // make sure everything is okay with the network structure
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "CSAT_Check_Integrity: The internal network check has failed.\n" );
+        return 0;
+    }
+
+    // check that there is no dangling nodes
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFanoutNum(pObj) == 0 )
+        {
+            printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" );
+            return 0;
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets time limit for solving a target.]
+
+  Description [Runtime: time limit (in second).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime )
+{
+    printf( "CSAT_SetTimeLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetLearnLimit( CSAT_Manager mng, int num )
+{
+    printf( "CSAT_SetLearnLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num )
+{
+    printf( "CSAT_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num )
+{
+    printf( "CSAT_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the file name to dump the structurally hashed network used for solving.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_EnableDump( CSAT_Manager mng, char * dump_file )
+{
+    FREE( mng->pDumpFileName );
+    mng->pDumpFileName = util_strsav( dump_file );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds a new target to the manager.]
+
+  Description [The meaning of the parameters are:
+    nog: number of gates that are in the targets,
+    names: name array of gates,
+    values: value array of the corresponding gates given in "names" to be solved. 
+    The relation of them is AND.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    if ( nog < 1 )
+        { printf( "CSAT_AddTarget: The target has no gates.\n" ); return 0; }
+    // clear storage for the target
+    mng->nog = 0;
+    Vec_PtrClear( mng->vNodes );
+    Vec_IntClear( mng->vValues );
+    // save the target
+    for ( i = 0; i < nog; i++ )
+    {
+        if ( !stmm_lookup( mng->tName2Node, names[i], (char **)&pObj ) )
+            { printf( "CSAT_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; }
+        Vec_PtrPush( mng->vNodes, pObj );
+        if ( values[i] < 0 || values[i] > 1 )
+            { printf( "CSAT_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; }
+        Vec_IntPush( mng->vValues, values[i] );
+    }
+    mng->nog = nog;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Initialize the solver internal data structure.]
+
+  Description [Prepares the solver to work on one specific target
+  set by calling CSAT_AddTarget before.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_SolveInit( CSAT_Manager mng )
+{
+    Fraig_Params_t * pParams = &mng->Params;
+    int nWords1, nWords2, nWordsMin;
+
+    // check if the target is available
+    assert( mng->nog == Vec_PtrSize(mng->vNodes) );
+    if ( mng->nog == 0 )
+        { printf( "CSAT_SolveInit: Target is not specified by CSAT_AddTarget().\n" ); return; }
+
+    // free the previous target network if present
+    if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
+
+    // set the new target network
+    mng->pTarget = Abc_NtkCreateCone( mng->pNtk, mng->vNodes, mng->vValues );
+
+    // to determine the number of simulation patterns
+    // use the following strategy
+    // at least 64 words (32 words random and 32 words dynamic)
+    // no more than 256M for one circuit (128M + 128M)
+    nWords1 = 32;
+    nWords2 = (1<<27) / (Abc_NtkNodeNum(mng->pTarget) + Abc_NtkCiNum(mng->pTarget));
+    nWordsMin = ABC_MIN( nWords1, nWords2 );
+
+    // set parameters for fraiging
+    memset( pParams, 0, sizeof(Fraig_Params_t) );
+    pParams->nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
+    pParams->nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
+    pParams->nBTLimit   = 99;             // the max number of backtracks to perform at a node
+    pParams->fFuncRed   = mng->mode;      // performs only one level hashing
+    pParams->fFeedBack  = 1;              // enables solver feedback
+    pParams->fDist1Pats = 1;              // enables distance-1 patterns
+    pParams->fDoSparse  = 0;              // performs equiv tests for sparse functions 
+    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;              // the verbosiness flag for proof reporting
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Currently not implemented.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_AnalyzeTargets( CSAT_Manager mng )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves the targets added by CSAT_AddTarget().]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
+{
+    Fraig_Man_t * pMan;
+    int * pModel;
+    int RetValue, i;
+
+    // check if the target network is available
+    if ( mng->pTarget == NULL )
+        { printf( "CSAT_Solve: Target network is not derived by CSAT_SolveInit().\n" ); return UNDETERMINED; }
+
+    // transform the target into a fraig
+    pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); 
+    Fraig_ManProveMiter( pMan );
+
+    // analyze the result
+    mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
+    RetValue = Fraig_ManCheckMiter( pMan );
+    if ( RetValue == -1 )
+        mng->pResult->status = UNDETERMINED;
+    else if ( RetValue == 1 )
+        mng->pResult->status = UNSATISFIABLE;
+    else if ( RetValue == 0 )
+    {
+        mng->pResult->status = SATISFIABLE;
+        pModel = Fraig_ManReadModel( pMan );
+        assert( pModel != NULL );
+        // 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->values[i] = pModel[i];
+        }
+    }
+    else 
+        assert( 0 );
+
+    // delete the fraig manager
+    Fraig_ManFree( pMan );
+    // delete the target
+    Abc_NtkDelete( mng->pTarget );
+    mng->pTarget = NULL;
+    // return the status
+    return mng->pResult->status;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets the solve status of a target.]
+
+  Description [TargetID: the target id returned by CSAT_AddTarget().]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
+{
+    return mng->pResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dumps the target AIG into the BENCH file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_Dump_Bench_File( CSAT_Manager mng )
+{
+    Abc_Ntk_t * pNtkTemp;
+    char * pFileName;
+
+    // derive the netlist
+    pNtkTemp = Abc_NtkLogicToNetlistBench( mng->pTarget );
+    if ( pNtkTemp == NULL ) 
+        { printf( "CSAT_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
+    pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
+    Io_WriteBench( pNtkTemp, pFileName );
+    Abc_NtkDelete( pNtkTemp );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the target result.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars )
+{
+    CSAT_Target_ResultT * p;
+    p = ALLOC( CSAT_Target_ResultT, 1 );
+    memset( p, 0, sizeof(CSAT_Target_ResultT) );
+    p->no_sig = nVars;
+    p->names = ALLOC( char *, nVars );
+    p->values = ALLOC( int, nVars );
+    memset( p->names, 0, sizeof(char *) * nVars );
+    memset( p->values, 0, sizeof(int) * nVars );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the target result.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CSAT_TargetResFree( CSAT_Target_ResultT * p )
+{
+    if ( p == NULL )
+        return;
+    FREE( p->names );
+    FREE( p->values );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
new file mode 100644
index 000000000..124ca266e
--- /dev/null
+++ b/src/sat/csat/csat_apis.h
@@ -0,0 +1,174 @@
+/**CFile****************************************************************
+
+  FileName    [csat_apis.h]
+
+  PackageName [Interface to CSAT.]
+
+  Synopsis    [APIs, enums, and data structures expected from the use of CSAT.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 28, 2005]
+
+  Revision    [$Id: csat_apis.h,v 1.00 2005/08/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CSAT_APIS_H__
+#define __CSAT_APIS_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+typedef struct CSAT_ManagerStruct_t     CSAT_Manager_t;
+typedef struct CSAT_ManagerStruct_t *   CSAT_Manager;
+
+
+// GateType defines the gate type that can be added to circuit by
+// CSAT_AddGate();
+#ifndef _CSAT_GATE_TYPE_
+#define _CSAT_GATE_TYPE_
+enum GateType
+{
+    CSAT_CONST = 0,  // constant gate
+    CSAT_BPI,        // boolean PI
+    CSAT_BPPI,       // bit level PSEUDO PRIMARY INPUT
+    CSAT_BAND,       // bit level AND
+    CSAT_BNAND,      // bit level NAND
+    CSAT_BOR,        // bit level OR
+    CSAT_BNOR,       // bit level NOR
+    CSAT_BXOR,       // bit level XOR
+    CSAT_BXNOR,      // bit level XNOR
+    CSAT_BINV,       // bit level INVERTER
+    CSAT_BBUF,       // bit level BUFFER
+    CSAT_BPPO,       // bit level PSEUDO PRIMARY OUTPUT
+    CSAT_BPO         // boolean PO
+};
+#endif
+
+
+//CSAT_StatusT defines the return value by CSAT_Solve();
+#ifndef _CSAT_STATUS_
+#define _CSAT_STATUS_
+enum CSAT_StatusT 
+{
+    UNDETERMINED = 0,
+    UNSATISFIABLE,
+    SATISFIABLE,
+    TIME_OUT,
+    FRAME_OUT,
+    NO_TARGET,
+    ABORTED,
+    SEQ_SATISFIABLE     
+};
+#endif
+
+
+// CSAT_OptionT defines the solver option about learning
+// which is used by CSAT_SetSolveOption();
+#ifndef _CSAT_OPTION_
+#define _CSAT_OPTION_
+enum CSAT_OptionT
+{
+    BASE_LINE = 0,
+    IMPLICT_LEARNING, //default
+    EXPLICT_LEARNING
+};
+#endif
+
+
+#ifndef _CSAT_Target_Result
+#define _CSAT_Target_Result
+typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
+struct _CSAT_Target_ResultT
+{
+    enum CSAT_StatusT status; // solve status of the target
+    int num_dec;              // num of decisions to solve the target
+    int num_imp;              // num of implications to solve the target
+    int num_cftg;             // num of conflict gates learned 
+    int num_cfts;             // num of conflict signals in conflict gates
+    double time;              // time(in second) used to solve the target
+    int no_sig;               // if "status" is SATISFIABLE, "no_sig" is the number of 
+                              // primary inputs, if the "status" is TIME_OUT, "no_sig" is the
+                              // number of constant signals found.
+    char** names;             // if the "status" is SATISFIABLE, "names" is the name array of
+                              // primary inputs, "values" is the value array of primary 
+                              // inputs that satisfy the target. 
+                              // if the "status" is TIME_OUT, "names" is the name array of
+                              // constant signals found (signals at the root of decision 
+                              // tree), "values" is the value array of constant signals found.
+    int* values;
+};
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// create a new manager
+extern CSAT_Manager          CSAT_InitManager(void);
+
+// set solver options for learning
+extern void                  CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option);
+
+// add a gate to the circuit
+// the meaning of the parameters are:
+// type: the type of the gate to be added
+// name: the name of the gate to be added, name should be unique in a circuit.
+// nofi: number of fanins of the gate to be added;
+// fanins: the name array of fanins of the gate to be added
+extern int                   CSAT_AddGate(CSAT_Manager mng,
+                                      enum GateType type,
+                                      char* name,
+                                      int nofi,
+                                      char** fanins,
+                                      int dc_attr);
+
+// check if there are gates that are not used by any primary ouput.
+// if no such gates exist, return 1 else return 0;
+extern int                   CSAT_Check_Integrity(CSAT_Manager mng);
+
+// set time limit for solving a target.
+// runtime: time limit (in second).
+extern void                  CSAT_SetTimeLimit(CSAT_Manager mng, int runtime);
+extern void                  CSAT_SetLearnLimit(CSAT_Manager mng, int num);
+extern void                  CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num);
+extern void                  CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num);
+extern void                  CSAT_EnableDump(CSAT_Manager mng, char* dump_file);
+
+// the meaning of the parameters are:
+// nog: number of gates that are in the targets
+// names: name array of gates
+// values: value array of the corresponding gates given in "names" to be
+// solved. the relation of them is AND.
+extern int                   CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
+
+// initialize the solver internal data structure.
+extern void                  CSAT_SolveInit(CSAT_Manager mng);
+extern void                  CSAT_AnalyzeTargets(CSAT_Manager mng);
+
+// solve the targets added by CSAT_AddTarget()
+extern enum CSAT_StatusT     CSAT_Solve(CSAT_Manager mng);
+
+// get the solve status of a target
+// TargetID: the target id returned by  CSAT_AddTarget().
+extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
+extern void                  CSAT_Dump_Bench_File(CSAT_Manager mng);
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 53a46584e..946ed56bb 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -97,6 +97,7 @@ extern int                 Fraig_ManReadFeedBack( Fraig_Man_t * p );
 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 void                Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );        
 extern void                Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );      
@@ -157,6 +158,7 @@ extern int                 Fraig_CountLevels( Fraig_Man_t * pMan );
 extern int                 Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
 extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
 extern void                Fraig_ManProveMiter( Fraig_Man_t * p );
+extern int                 Fraig_ManCheckMiter( Fraig_Man_t * p );
 
 /*=== fraigVec.c ===============================================================*/
 extern Fraig_NodeVec_t *   Fraig_NodeVecAlloc( int nCap );
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index d60c71683..0194f3b4f 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -57,6 +57,7 @@ int               Fraig_ManReadFeedBack( Fraig_Man_t * p )                    {
 int               Fraig_ManReadDoSparse( Fraig_Man_t * p )                    { return p->fDoSparse;  }
 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;     }
 
 /**Function*************************************************************
 
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 0a950aba2..b46f6c41f 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -765,6 +765,47 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
     p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Doubles the size of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode )
+{
+    int * pModel = NULL;
+    int iPattern;
+    int i;
+
+    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsDyna, 0 );
+    if ( iPattern >= 0 )
+    {
+        pModel = ALLOC( int, p->vInputs->nSize );
+        memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
+        for ( i = 0; i < p->vInputs->nSize; i++ )
+            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) )
+                pModel[i] = 1;
+        return pModel;
+    }
+    iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsRand, 1 );
+    if ( iPattern >= 0 )
+    {
+        pModel = ALLOC( int, p->vInputs->nSize );
+        memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
+        for ( i = 0; i < p->vInputs->nSize; i++ )
+            if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) )
+                pModel[i] = 1;
+        return pModel;
+    }
+    return pModel;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 1139bdc09..5f8b3496f 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -178,6 +178,7 @@ struct Fraig_ManStruct_t_
     Msat_Solver_t *       pSat;          // the SAT solver
     Msat_IntVec_t *       vProj;         // the temporary array of projection vars 
     int                   nSatNums;      // the counter of SAT variables
+    int *                 pModel;        // the assignment, which satisfies the miter
     // these arrays belong to the solver
     Msat_IntVec_t *       vVarsInt;      // the temporary array of variables
     Msat_ClauseVec_t *    vAdjacents;    // the temporary storage for connectivity
@@ -378,6 +379,7 @@ extern void                Fraig_FeedBackInit( Fraig_Man_t * p );
 extern void                Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 extern void                Fraig_FeedBackTest( Fraig_Man_t * p );
 extern int                 Fraig_FeedBackCompress( Fraig_Man_t * p );
+extern int *               Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
 /*=== fraigMem.c =============================================================*/
 extern Fraig_MemFixed_t *  Fraig_MemFixedStart( int nEntrySize );
 extern void                Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose );
@@ -404,6 +406,7 @@ extern Fraig_Node_t *      Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_No
 extern void                Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 extern int                 Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
 extern int                 Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
+extern int                 Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
 extern void                Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
 extern void                Fraig_TablePrintStatsS( Fraig_Man_t * pMan );
 extern void                Fraig_TablePrintStatsF( Fraig_Man_t * pMan );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index d41f5d0bf..657163403 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -171,6 +171,7 @@ void Fraig_ManFree( Fraig_Man_t * p )
     if ( p->vProj )      Msat_IntVecFree( p->vProj );
     if ( p->vCones )     Fraig_NodeVecFree( p->vCones );
     if ( p->vPatsReal )  Msat_IntVecFree( p->vPatsReal );
+    if ( p->pModel )     free( p->pModel );
 
     Fraig_MemFixedStop( p->mmNodes, 0 );
     Fraig_MemFixedStop( p->mmSims, 0 );
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index ba22cfad5..13c09a9e6 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -109,6 +109,31 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the miter is unsat; 0 if sat; -1 if undecided.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManCheckMiter( Fraig_Man_t * p )
+{
+    if ( p->vOutputs->pArray[0] == Fraig_Not(p->pConst1) )
+        return 1;
+    // save the counter example
+    FREE( p->pModel );
+    p->pModel = Fraig_ManSaveCounterExample( p, Fraig_Regular(p->vOutputs->pArray[0]) );
+    // if the model is not found, return undecided
+    if ( p->pModel == NULL )
+        return -1;
+    return 0;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Checks whether two nodes are functinally equivalent.]
diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
index 5318c41e3..4dc6afdcc 100644
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@@ -371,6 +371,43 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Find the number of the different pattern.]
+
+  Description [Returns -1 if there is no such pattern]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand )
+{
+    int i, v;
+    assert( !Fraig_IsComplement(pNode1) );
+    assert( !Fraig_IsComplement(pNode2) );
+    if ( fUseRand )
+    {
+        // check the simulation info
+        for ( i = 0; i < iWordLast; i++ )
+            if ( pNode1->puSimR[i] !=  pNode2->puSimR[i] )
+                for ( v = 0; v < 32; v++ )
+                    if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
+                        return i * 32 + v;
+    }
+    else
+    {
+        // check the simulation info
+        for ( i = 0; i < iWordLast; i++ )
+            if ( pNode1->puSimD[i] !=  pNode2->puSimD[i] )
+                for ( v = 0; v < 32; v++ )
+                    if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
+                        return i * 32 + v;
+    }
+    return -1;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Compares two pieces of simulation info.]