From ce3f8cb1d11b7b39fa48f809baa1419e9984fe8c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 1 Nov 2012 02:53:09 -0700 Subject: [PATCH] Improvements to the truth table computations. --- lib/pthreadVC2.dll | Bin 0 -> 86070 bytes src/base/abci/abcNpn.c | 4 +- src/misc/util/utilTruth.h | 187 +++++++++--------- src/opt/dau/dauCanon.c | 390 ++++++++++++++++++++++++++++++++++---- 4 files changed, 453 insertions(+), 128 deletions(-) create mode 100644 lib/pthreadVC2.dll diff --git a/lib/pthreadVC2.dll b/lib/pthreadVC2.dll new file mode 100644 index 0000000000000000000000000000000000000000..93f562baa916c6a5aac9aa753069399e081b17ce GIT binary patch literal 86070 zcmeEv4O~=J`u_z-9d&d@1w$o8gR;$X-hhFbVekdS6a_~HUjjl!0Tl>le97>of!f=R za(CNyw{5qqZMU{=RD^*&w0-CJSThU4sHO)aVi9#kK=aXm;Tb(^~{$RB#)T*^a$?pA+Ju_6*2GC zNsCI$YT~M@D_2(+uZvqzTv1W!j$2+5SM8~YE31f`wZIv-u5x9`6~l)QjhBlayEmbw z;J&$n5*$x27M9@ogQqftA{Kw8P>SCto}Ml&#_uQhW(!xb=LIa^!m<^m^lorXb22z? zUc?~ovuOhEq`xEFh)Kf`#~s1*)l%H4H}I=NXlKtlc8_O*2mL9(Tuy|P4{?z!1)1nQ zy0BmANBxUyDUCu|p z0e|TnHzVLNd>e*97y@Akgdq@yKo|mH2!tUJhCmnsVF-jFa0UpxLVvC6jU3l{&9%7P zd_OL~y9bxazrG~ zeIp_cm%|U>vf)>_OuinM0<3jgH~t!z8p^k2EH14LxWv z9XH_e2-W%6&A2r4xa@)Gqt!kGm&LWXIH|h7#tOZ)jH-5Y9xfkF!{w&Ca7p|jE;}~i za@mu(xF~gZ1un5v@_Sg(w?4WRmjWzbTMy7()0Mc4ph}LVir3L)S~M=@_u}%27njCj zT%L^YlCCtRMr377Y%(R=9K2D)TX#b;iP%WDL>C6H0H#!tZI1#0vi)Q*Hd;_}9w zxLBRI92|qoZi2?0)Pz4%vwlnkoFd>HD8a@1GhD8q@1`ul}zf(vl@J-wDlHE4v; zruDK*artyHF4s`oY}AColy9;Fmsjg>*+@l={y8pb7vl1l?YQh6jmxwj;j)zKypPa~ z`yDP1*5lGaE&7TozLx5@nz}oZ@UNEYVxi(qf57DyN}V$nmv^Xs)2LQUsi=L_82wUQ ztlMzuh~qeh+2KnV0{>GG$P_y4NTSEN>jE;?q9- zVdz8rsMNFVf}j*70gXeu2j}>rb(14>XlK(|)Zcpyl~%jTIlLB!*XkQRSLNW(7adE5 zw9DY+Jzee?8E9Pr_32!?q%FEfJgW_&g^W&=HKg3<@DEvg>r;zHU0QfBGmrJ!1 zJevH5Eoy#HbEbx1(VWR7&&?!u<&+NB_UM4ND7jV|p(o_)8?|*W;5EKV5=%yast`6>Ys&>e6 zreL;zoD~%=^P}{+!neQt!mM}|Fl?m2;W}))E&hdV2U04%X!7~q7A}8h5{+-~UUhwkXYdO&uG+@=-t~6+_(7hL zt`}(g#TR`T?|b*EOda(;KJf_N_spWQ@cucyc@%GI>%a_h0xLzXsJ0I59arDs9_K!OInxm- z@72;zqx5q(`(f=XDlAy$Cv|Lu2KU$Z{p<%b*h6k70ak+N*C+ah^Wbu z2nFq;^8)Td8EoeYA4adDXvWA9vQ&az$Wimz?Lw9Y(-)t2g3s=hFj|NvShyC7_o1=P znNc(-y!+EZg+%KkxZN8CLX?0REXS93Ldfm{HVN%6etL{Ax&?SZkNb)K?on}BZfll1 zR>l^(eO@9^GrrOc1B^m714kj z$S>Bl4dO4P0musBFQhbIG#hKP;%5noG~)y12ITk-Hq45*7kD1{1^!HpI1JV>tG>?_)8MKSYT9dFS9z29QUd`vIczttv6e2m{ zN=^NXe3r&NfS(@4&(JidGs+^|f<+ofDQZg5@i)-3sga>%f8Uqsb&-&x6SCCxZ=r-M z)%7ppCs!xvTq)O6S)M`sP4p}1Qm)5BnLX35kQF85piY!qBfT3%SbUAf+Ft0PNHAqI z=9c&Y)L(trc$g~9-}N2ZICG9(=#kH87vK2`J;IvnOSJf-buJtI&MJy{`+zQ|d?R;Jf^-ME9DBQA*KD#A;*y}vI^+j7yZh2(G z7F9V{&gJuie9>ma01vXHANgq(o&cw^z@h9?3x)ond>TU;5pU1n3pKn;)128ol%yUvE^*cu66lVgYt~C( zV;s-01AJ!uKL@+fLf(;uE>Vq=(FRk8sj+P$tC-Tt;cUvt6|1EjLdFqcu10X`tgm^7 zSl{pr^vzVY4Q|djK~zMjJ>m7~JY&JFHY}au6hCTX^DPl48`{~nnFdat8Z?5xi4A=W zq7g!-Di>%afkGHl&MhQxK&6H7X^OYDUA1*GrnZK~C~yZAxL@rOZ^Vs|cPxJfpLfic zceHJSklmRpE@!dQw@Z|)SJBO0jZ-}KIo`=o(=4`)zAg>v`e|K=_NbkriQdjQhIC@^ z5B|gFQ+V9|=*|D{=|umXu6#icmOAPgB3j^4(cwjWOriIHZ&?#Ya=y6s7~tDN;63E| zP?(TEm!BZM(8@5R{!pz(n6EDPVR*&Ri-o4f03NbG_62kyt8%h9hz{A_uf%de-EO{uT&_&!Qc~q< zH(Mw^ffV6{mwqvzW%NtdZ>}4^Rb@TCKKiob!hS~Tiwbw0hR9+WFs;ed2*jbAvt928 zw=dV3CtOa1*CkQne86>RGb#bda&4FR-lY-32y%-sNG2lrJeUfJBFkh1wT|(2M!JU+ zsZ-M++)Hg-6tBZ9JEY_KZ73|lJS}e{0|ZUfBF5X8 zz7Ul^fD#ly$-lwyIM-)C`11WtSQOBN0HF15!eyu)*kHF-ZpwUBuGAElnyt(Ta~RU9 z+wM_TI{noTE7u+^49*W>1MpA<29a~+ygv?k{V7cmYoxcuN}#)M+d8o^+ymKOBx!Sa`h2f)xG zL?$*5XwwW)zn}RG(H?Y>N|+Z<4D>iABZ!h^1jI(Fg>(%c0gyLGP~F)_dV;?fe5gE> zHG-9;RBw>pEUHu)u zukQEzf*Mdz3%N18u1DTb_(?gvBIh2PrGS_qDBvT_(_^R;n|A5x+84Zt_^Vy{^@p@| zw2%UF$JG0@b=z>?y)=>~H|~`vn+Et$*4rw9Yl}2B@>^7VTEiB|`Ev64OfZUSyvvDE zpD^A5JZ5~3kf~{y9|c0@JE}wu;!U9RP5ENi-`F&U1+9$1m=0+CENj9Ijjw>oECfCW z_h0Zc=-JwMjjR6ieD_s?hXhA?4TZYq45}mN6u02(LMO&ez0YH8$c)Mn*9OFl?5-6} zOpwh8^C5W5b&5$+Lxg7D!?6ThLe#c@dcxLQ*l>WzG@sTI-=bQ?3~1|U%_VG6H)N_^ ze8vgB7Eo1}ADLAy$U0wyFfjr{LzlxF{HRQCvnF*H((8SRenztq zrIjh>V1Z*qhP~?_x~v9$ydNWw&|nm`#QSZ8TUGy-XCQ{=Na^zdMFhW3!umX!SE}#G zcUyv%t)ibx@~>L+{7bE2w9cy3w7v9g^xt^X8JkRd{}f=srY=1enDYG1S->G|TPe?_qu(%O*h{dGr=R7|4zyDu1KB^A)IX*i75*{CH z{y+p4fOVWZ*<;!Xejkq~nJ@S-8|{J~15Nrd)`gv=;! z=KyWJ8ux7exSd*@X$Ez)Hfifbc{Y%y0eO1J7hB%*`SLNRh_B;DnHDh40;UDsSxgJE zeB)m`Eo@@At!C2#X8XWtAp)&I!-;oh^MK4={m0J-+mF2hX}?Q&JiZ0LBzk~w39~({ z60um|Fy%oMp=z#+e-_=DlgjCG5v@WrR{Puc(z^l77#iK*{B~w}mL=reEwtzJ?jVU4 z7Cys-*E+UuL$xB@{W1b$gck5CBw-IBsyYKBa3ky15Is&EO?}*7d;3c#c_p+H*tP|+ z@r*MB*8}cs6wNh|uv>R~21A%hyFkxFUa9Q-vt6JL07i%P>wXFGG)?~fni(?VEBg0q zz#+<l@i@E*;(Gx&;g-lJjr6_bQ)E(8a>8|}cT1U%6Y&v4?{*pi$Cv(^th!&3lg&*0~Y zY(fIi(XbiJ@Qc*;nHG%c`o`yov(?tmBBD3bOiXYJyN$B$(>7dzTLMoD^6+b-@|$Ne z?pOTsEfm01J*bQhKYeq@#|6;0-qKqM+v9`fss9RW|HV5DPK>_A1=2U6MulPDiB$^} z1SG!S9*K5)R-?s;Dy?#GI=SJ#=q|AO`Qn#vQemX@)p9nIH7 z2~HbuP=~Pz6d&FOTnAjQQxRt8ix03;RDrK6q?P^lH@^Pc(*Mio<7yx|Mpo|`@qE!o zEaj!02M?B9g-uRO__P}mYS$x3fM2u>bHt@U9Fh&6L4^MshGA-1GSVNuPZ<~;X>0%vV@U*NSwct}_k^}-a)0tG_zGTvB(jg&Y= z8HY)nttaJ7H2L^5HB>;GFh7q^=DfjotF~POA z+pewqGiGREkhNJ`_Ym$dAhdN$aTCx)A&K`K5w_?WGIfynioboCu{L?fKqQ>fO2#v{ zp-}G>-vG3vRSa#GUO@t_9!nUf7>#$GvXDzu8K7}Npaae|$8zMp5C z;P3Hz-+KaN>r7R)p-ANvSJQ{uCFWoSM9$t6&NJC5{uu>GZz9R}UNa}X?|)ZFcFyOM z#U1i@I%;kC4S7dPs~+Wa3&l;;tl8=uaTRNyORQnpAo#-&V%72Wtcj3)#N-pEM>Q8KnR9|w6oBYuM>Pt>>xj&kzFEJnlsxNg2r`>Ak zB)0AV-ZA;RV1oP|I`*M8n2z>#_`rEnW-f8SNB5KY-{AQk|4D3xn)X4A@$mkdCGf z+IkV`IdJ6>;8;(Pj!UCwq%eqmCyO7{Ht>bX_`Xy89ZDf2@wu^MLI@T3c>y>*2CcBZ zp}l1fRTo+{qlEix^$Jc9ma%dnq|fMTTh^=mf zXlJNoq`#6eC{n3sV7UVj?-bu}W{rWa9fNfs87b&$eTP~=7Au_#o2d^u@sCtThPMO) zn0C-0LNy!aYjVXO$sd)Xb$nhs&=DU{+B(cBs-;mPbfz$}a~Lv=qFv$+7f^b zCb5}}dSMDb1NE9El?4(T6HL1N<+|g|4U6LA7D7Z8gN8$L~ zFUJ%h%vVhpcJuR9G;un#^pkfx5k1y?`aGQ0E*OQ z8!DpmK$c>}0rDUKHn5>HUyXJ6i*7rrI3iD+_dM$uf-YHz#6THzl+Y=$G6P=c=c`*E zMm45qNyY&4VSU<4Jh3%XwPlYy3MG6hVEA-9Fh{|s*}}xUx%@=2^*OokdyPW$>~LX( zjJj+hY zENm-beDNoSgG78~E?S6z{b&;!F7scqp;~Z%obPAWzY#g287jh|`gi*=HdyQ8{{TRv zqfH(8(6wCW@CuXELZCw)4+IjI)gxlhYKJYQnAQWznKY)Ad7d))RvNYPdV#2I!4HWeGx$#1F z6qpt3YcyGD>#w9FCf3GWo*A^sFoyOH$SrE( zX3^DL! zVtC1JwcBKFDg*5C`!Gk4X#Z?Y=7^K+&tk5$r^Vc&_^TF*Gf{i6U5j(X6x^W!7LsvE z7IOqp+zv&r%fc;cAW^jKdub#!Vd&7-C80c~bB67+;?>>BScdr@LaYzY_xS&Jmj^hg zw;v;R$NS9yXWnxd%^a3L`?NP&K{9;t4VGn`PMrP}S-cQjC?}jn_|0f12Mm8n4dAQ= z@-(#Bh=&NqrOsU_PThrmCB?G>;2snNNYy)E{PUmD$C*$<(_we5{!zpUg;2B6Kobot zvbJsqV!BZ==Il|CUn8qS?CS>$naw89XpxL#VE40f#peJMtN>;$6d%JKl2Jtk3)z5& zV*oWq6`3m)3Hw4q@2wutdlfASg5DTGl*wm4S=!}*2q@}_&}fFg9&A8rgt=<)6JI=u z`qb!M;zU%Zc_xFNOWcH5VJ1P3WL_0QjaqPOKtdp-buVCGgUM^m@%vDQum`1#Lm!|m zS4nLlGqfmt6Yb1eD85Yn10&WPakrF9Zn2U}U{jJ)dpF0+b)QRhpNG2Vpcyby^tWJP&hh)i0z#GEm1o^Gf-29t zOBJ&6!CfX!1LStLK>i~niV|TQUz!e6Ow{w3^c?AXLx`pv3w;N7zJp&GKbTHvkKrQt zGL~?x8yTLn?Ok*2REa484s}q}Uw+ zZ+TaYf=k$bfNfVBsfqN)BuQTsOC=gL-Pkltcv(>s8A*E;!VKa@l=2n3rt_gSy7URg z)3MFasPc$z^&r9x83Dd4e1qSYTod@E^_bd#l%oJd4J@gxFF|u8OI813D9sVia10%w zFyntck!QL8$@X93F=NzXxvs7I6>*apSn+7)<>IXiP)ivE0&a#k7y} z$Rl9q^04P8KKd{rm9BX(&C~+mmwf~l8{}k%fp|Y++4f08-eIy|P<-n=jd<#rAQv=h zC0=nsgY5wHh;_HN?j^j?kS8`|i?F-pvsw9lv|jlLTuTKQnfv|Rkjp6+@Bc_>M@UlZ z8#2%!ct>D9Y0jG~BGS($r!=xn+xO<5CU`ua?`JmNLi-=`z=u!R1(BpVB=4o1|M@jo zUw)>{uz_h|R<~!gCmBQbB(UBm?L2TXYT->L6clg#Bls3t?lOZ6wmf0WUB-jKkTk|1+*@8xYdngPC%O{%g2qGWWcFgy4?-{S#u z7TJ4}QY6iCBwVK5T-n`IFZ04)->3KM8*63x+`aAK;(ELkT;H9PBR~KjoG#&qtiSm= z>4`{-V!uzO3xzBl3`Y6kflA zKf{bMa9BZB!p_p*l@A&B6%Niq5i z_HZPS6W@A(h?Zmz_W~l$D53jLu!oC-`;rh;>v6OLxC!BD93+^r*klElcOle#z&-(T z?oo>5tc_%7l3vujc#_=da6kkt z>$&&uqa@npWXlc)9Xw#qg5dN$%ooAq=X^f{El3{}@>Fqq7i)IFWD%l0uAbUeJ@hxP z_#G=iXb(`7qGcI*i<-#1MdgY^`^<9+dB}BCuJ|c%1{mI}9N_uDU_~r>+2^0J&lNsI zkMc~P!`55Tjx1=xmLxgs8BGcla5)0qNcfPL0;DTwa`iI8ht3m5)^ns1$?FS+eMJRL z^*(6>NZuQQp@##-4HRap$UdL+An6}l#Ii3`X{N*Q&5VNE#^+*DlwTTb>Y(D4lFywV zVf=Rtd9TBh`VuEn!dO=fUWJ5+5g#TAFR7Wqg*{K7g z8?w9PKFsu|Ttptfq8swMSkFNs>Q4z!CfUZ+G->97EX)I^UoLzedSyb3?7)*R=#PA@xG*Zsjb_Gt`feh&#%>i6ZCmw zX@r7KW)}yKU#Nd9>L1eM*D5rJ##+WPYAka89ZkZ#udV->+NNxjr7KW8ra-Yh0E))~ zpxE9GMP`n^RnuCJl0@e{Z2J8cbJj))WRfZRf!_YUx{c7!=qqg$wnfLIR8*f@3cqx* zOe!mHVoB0nsFi!AJOBujJ?r2TW{CB5&%hq;zC0&LBGjR+e~Ow7f03Ki5uO-fIyrW5 z>$3Ris$Dvy$m=v59T&^g2#ek7Li$_Y|f0z?{!h#ex$4X?l3B^z%PGzpEVXqG(Zb zKY9e1g3b@+UxL?@SD@bRC3>&F{>%MK&|Gh7gbKw4!Vp|Zq6{yW*A4N08@W}*=cy_mw zO4II`uVv;SP>maEjQ;2VHST=zm;UHJC!{Xuw))56M7}_cIfaD3zd+UG3CcZ^ z9FsG8C5v{)FxTX4x(XrOU5$xINF?tPJqv(L)Yr2BiV0D`#ZQfY(0n~#b@r6=Ce+k&-T(s*nHL} zaqiYxI3sZ`4xH53hACY4DoanoNs3;g>95`|F+MAs7K?H&Z8`|T`xdp3N3VYqASRCt08q#91DTW?@! z3mv>(t|Pa*@J_Jn$f<~g>&T2_-JTk1J^e;TF~5-`E;~+|dqbXQ z3OukrCKHYV4Y(;67##_hwe=MsXstRTcD*>tPFWHShrC@fxW+qO;=Z4uX*5bi20B5d0i5GlIY`m$%TcPmJd z4lBxZem3*v!{*IhM2D38|1@qLCRi?rf&=Yr;1($%G2A-fYZWLZq+8O2MMw$8tv7Hq z6XDj80NgqPPB{R#9zqtvt)pj&TR<%MHpBSaFL>HX2TVdR&&XCSkSmafVB##2W-(zF zlVvH8$vzPP;ssE)g7`++VEbRAm*=}ZjQ(QQA^&(njLgA#{{hQ8wbpwaD9yMhPrfn= zB)SH?VN?;D;xbjFm|l#JTdQq&lFFDHmD_qJZcsjrlI}^)Pd?;*ERa8$e2jrpK9CHO z1Ph&@K_D88d}N;>ERkG#j}Y>igNVEn%v4K!;U`2vaI654kUjLFGihyJXhzvRTzS8Z zk4RdZbSGD5iO(O^{oYaL@$JaCyE#GU$ApXV;GI^XyjT%Lr#J=Pzz z#_nsivFyhoR~xhZ(E)5kzIeGm`m9zPY>WsKF^Lzb|7kw8{%U2=Y3u%oS++<@bki9ix}otSkCd?i0`ww|`D?1iE z%Rv*Y>fGnv?>YLtXM;wPY;`vwfaU`oCB|U9@G;Wz* zs_9UU`07o-XlCg^!clTzlBE%_oellS*6UG(IQ?dZ@=S}wU31pldq`7>7*gWE;Sa-5 zro^@%CvEGt_>j}(HBv5mM^a)5FkU5n?gpw^rkQz*L*?Or?gzcxDCCQ;@vKg)mTazz7foHr{4xy}#*b$~?oGU&nMFSL2o=^*mHEo+kJKmAjFz$-)27xH7TZXe5 zNHmXHKQWY1hg-@-im1f)OsDRXJ>ezdo^9;jOw|ekz{p~1W&u($zfHxXcPfA=}gKArS zM}uZtL)1%TN#hRk0EYh5`6sS!kOZSH{HAJwO0r3u+P2`df()oHb-2FTiT1jMg~qrxM3Sg=($f0TiwaXBMrzA zc#2Y>^uZouF?_$ONDv(0UaQ!g@dWs!36a$xg*lw{K#_>-6tImNH@LqADD@PpCG%3 zGL^g5>xc(rCk6f&921x-p;pLa0w*YG%F%TJiz&ZK+JDk9fx_iw?d{FueuMI_+J1_-H!umJVX0U&!{MoKyNZZs9E?k&HJ=Z^J{*y=1fD zJ7{eZE+h+&dpq&ynZPVLng`OuMjcH0eQ!4pq>LE2T$^SmRYntWFa4Cl?J0^h`R*kn z5Nor0RB08J>pOTaxx8b>BPn*e^-QuhHxHz{b`1GV}_m$vQ`8kuahK$ayWqlQ;^ zZQYmX9C_)W2r$lcl#6`I>Xvxy%d?pR7G?9vq6|2vt;4C~p)AVYJ+Fq1i-HXsVPIA6 zRSc}I#vSIl0F$!N##L~51=qSiM}^sx1W=x@k9(HLh$bQ zNCfx`X($JnP@xv%0!^s!3==Ar0b_=ZyP^VX(=r+#2ib-hT*{Kcp`V-n&%W3(&x@axE7osghIr`<#m%?_lE)E)C0XwV8{y%I6u^g* z?M?~I-#0xIh7)B+tyC8sFues0%-i+|d(P0mxi01jO4(Ou&hePysLCA=4VE}!R?1=D zzvy|im8`IcofM|Su>lxZmFIAvAF2I?BwzO)8P6&*KXL{vRI&9?;j? zrGtI_ejYKo$a;T`epNC>@2@}jGXITO-!#luoovZv=ix-5hd5Dp9XY!hiYq>;XjAv@ zFM=$cC(`Iq&UiwM#tHuw?lEwa1_cT%K-hjEHVApcGCFxe<35bf#!SORW;_1!)T<#w@#lInkcdyDNzAxWM z3P$)UdE~*4oLn=i2At(J!&~CV5B)(aRacg~C_nwdv%hqL7l{f?hhR(aIc;<%5d9!Y zLEU)VVXshI_Zr%|eG99EwtgUDUE(;Y>a?j!2N1CHa0XG!CI2pN95h;ZEo&w@A|rnv zWE1+`Bl%2&SIbRD-%XMqTOM1K}#z>F!p&isC08)cXy^xO(e+8(* zYFWIEFhl4RZ)U&nKP_o%>Dn^$#rHQ+T8sD=ehF1OpQG+;n<`^0+k?hJ&ubx-`meU`eRP}T zL+uURk^WIePvYg*N%}^{hW54qxqmmU!fJdN`A-|f^o*K>WEuB8n_c2$1sy##m?fF7 zD2*LknOi-%Yz#yqT^R#fm$-C;e+l6|R8XJo&LyTmLYi z>=HLhxI={VH;8DcfJd>F1XD~`D(JV5a*5Bn{eY3mU_Qo5fv5G2TeRpF8B5_U2^=9@ zVl-}$6&>D zk$x|AN`9U=43RR-s8=qo3Dql@Is5LFoZh|iAuEM?1yg2xF1n_pTKbHJyxB=zbJX+} zb12ta!|BX88bG}AF=`2>dZ&2!8rG<`m@GaMP5@Oo;!B7jUSSVQA;;CjB(l&4 zc|B+PD(_cgPfa=$@=;R!8bEy2{d8w1j)TViEM?rkC-^-cFK1nLb~q-fp^wK-^!Cj% zV>X+8%G5!Al|7x+Ws+KYK>2C@@&gWpcZ!$zqXRa_oubYk9YBG4+Jlb1RLfRKU zqdR4sRw$`a1s@1c#~5auVD6N)^+PcT2~-{Ug)t7U-4+dVm2Gi&`z1?g7>M|H7qDX+ zuq_^7(ZCF%w?YT03nxupqv5CPTJJ!q;(ByHwsBzGpsgcohkmwl&eFhPA_jOWm5k4^ zooQy!A$|5Dd^V)D!%yi2X&*bFmM2gtwzxhT2!nJ52JNAhXxbsF?xjSdSasB)B(b(i zX}EjC`Drv+b!4Da3_01VV|*wp$UjP1Xs;Q~oURdaCA*IIVAnC79pm0fY`5TnUUQ&= z_guzf&6Rnq{01BhBL12hq0C~SYwOr3XXBXE!k~>LY}Q=%jf>w5#aoHZdJB1Es}J`m zr`ROFqUe!3#YdzV5ESOcK|VTF(K73vk-jUv`)_|gP#=dlnxCl9X^f-cad#$;rmjMw z%V)#UNYu>%*XY}~%GB)#>_g2NYG4VzbE>+s4}*in{_g}(xqNZDKRSTQ<%>V?NB2qP z)Y|$v7`*}7KYf|M`Kes6`J120%|u~zS{qTh&+)5h|HvDHbJj3a#%y>2Z8>8DzP5{W zTc80sSJz688^mYU5+*YpIQMnZ5GF02*LkK*D{1lcPRHDin1okX%_J%1sZ_IDSG*On>WIflA3T_YSI z$l^3&^yXgb&Cdy7ibkUsG5rwbv$W=zKsrn=@gXX`ceiGTQZpD1)I(mWW99yrd-b!@ z{(E&?zF2{5#6n`haXqy}A+Ew~NPavEnEE?b6$_v(&4@Bq74TIun^qO+@Y<9kUM>|N zw9`SlBgF~wqf(AIoazA?9hvS8WL9+kZ#2(lE(iS23Om<}fd9AC-+y)ei9ZK93VlBP zta!B~QP%sV62bM8-;ZbKGf&uV`NG$@*E0sOB$6ND?TlPMM3Pm(D+=p0e@W7u+edj* z*m=#9x2Lf3#>wT45->A-b=@#;r*`WgFnb}&?4!I1tbQ?a{d8C|(Rt7qvbvyyr2BY3 zG<>8|hGElKIb5F4f-l#=CiYQYpY@6Ar#{Xg2W?luJ+ySRAH1-h`Di~_yzi&=6sf;7 zYHudb%jh5Nt+(R_ouw|^rNOCE~W#DsIAaLHMDfv$E(^VM165r-A(}7koLY@j5H0`v@+USXPGP%5X@k&NV zz|R$+I!@j*RUF+Tsz5o|Uis~2&(3+h77Txn4#$JckMQ$Cu z>nm#AFl^bgQ*z)A$J(jA`DX;64ke2gPeEC>ZtUSZHPw`bA49);mB@> z03nDI*wK+XP3KMBG<>DS>%6PCmp>aESSoxi|EWX*@c=^ z<^Jl2Lhv~n@{wBy?IPGi#ff^*-$VYUGb{-%ujl*Jz32A6a^9E?E*^o#)^@kiRnC=i z=uT`zNQfOLZ@{*DzZfVvI*x=RYpNu#2MPfs*rEa?Mk+NY-xVx@z!8AlxDBp<@N-}F z0r!0N^$GZFaQVT{iqfP))q>N}G_{L%-$pZ5S8leYNNV?W@ln`VhV*>>Xg2nHCYNi1 zcjiX3UAdmQ_%z6i;Q~@DVwjJ4#WNuXoPuv_4wl0jrnv>*9iEHx#d2wExL)YtvZH5l z)E7m(UI9UHd-{8Z*2vm;jjR6ieCVhaz!J+nkF8lhEAFO!4zHD~o!}DfMQrr4lZpJ5 zfH?Gk4@7pR8nu_*5+LtLIWH;m2Ip$^_;-`i9l$|tL!78DD-gAl9;Olts zcIw<;z`j7*Ad~eydm>nW?F&wq+nX7xE2@fm zNewD0l*X(KfI;932WGK@sfM9-PH}{k8RSM63;{`>ky;X5zy6-tc*$p5H?vVgR0jAH z=S|~4)95G{bb_Sd300Co`Ql9lERWxvSFi68J&{yt=%igC2EzYbv08cyLtG0lsiag* z3a@o&m3WLgOLooY_MB1S^(?*6D+;dQt|G1C3bR;&8)y}8V&8>Ybs?S!o`*a!(wTHJ$s>tBP@Fa`8aAu)#n%}K zC})Rf1=Q~1ys4ZgE?=A=y&nQO*nWp8e?D&#zgZ@Iq@&jAWP1{HE?tiJ5#EK%>0I$O zy1{ushgd%7^}0vP$fFOahlD>=Y=8K2zSF(OXdaA}P=+?*1xqg6fUyM<7>^h+Np4^x zB-L0$mTFpg!kfogyU05lqyT49lRis>9w4f?g~|l8gEb(NT!QUryC~FJkwI6=D7!Vw zhZNr1Il!}kX$zgAg8EfQPg^RhqbK49h?9=D&;|Ko0-jNi7@!1TGZh1JBKb(`CVixv z3FrDc8INL`z&Pod(d(;cGN{&%1&bAI^m+(N2m{(je+yS@vEW5t0olYyp)(X{_WC3; z!R!_BXKD9}iB0&TVFQGfUrGH(+VE(|wbURwt}o6drY&Kp8xp_Kq=_y%&t$BWss2!H zGHMtF6pvlVj)T(g0-ggy=y->C@hfD*SwDHXVmpABgRe~y#l=)Up%=dFzCij;FVHEd zA0y2J=NrGj@A91JdTg}_CPu>R(0C#wjh<;aAm4uC4d0z}Rr$~vc`2V|VEaac^3(Z2 z;;!x(;bG%Wb%)O*9}^j5v;(*Fvy90I0g1XaHNFRz4h^f+uPrB06(V}YH?N{JK~wvEtA;r9)&@sz`-oBH7;>w9)p2W zrygvL1KTA?2CzV9RlG&kEIQl%lFDr6D}&lYEysk1sup;%?Y1=v`h%HSfd#o)K1si6k{3@vS9su2wH@%wv6?HD&l-(paAm% z$ZX%9hsakkxqyc$-`nzrdyt8b_jJUTvD7#G29@Lj9X-U@$-b%HHXXu~waGL1 zc~TN=8;E0G7OSje!KM?wfMPv(n1%%^o|zfIQR9Bf@K!TYoJmJVROK*{6b9Mq_&yHKG@u_*0aY!GJl- z{bZIqD$5h&-4Fh3*8)bXS+Q93Q=0;tbgu1T`=heIG#VfGl2Qii;$P6+g^K=%L+R+Z zyIrL{o7-O}cY8jQb|W384)n8izcOI_9oY*I{**vKXzTug_$+Om$bRZO@B<$;=w+ru z(k1V)f><&{)RL6tn;fN*J+@ar_D2Wo$K{JJ`=k5Zj|=qYCbjCjd01eZaXJ-?TE!RhQF6B;NzjKwYLm>S%1GKIy=uzzNodpA@02B7frPA6Bfu#Oxt>#;vYY?| zE$NdGOk`IRJ@iQ~rz$cf%=cTc8MR%qrRh6+7viV^mYz%k8ts8;>F9aWbtj|Qr5(~BZX7Yf0kp|>4J=J zLTSR~Gel8+1|;5O0BO=sV+hkr3Y2j08qi35;aV39K(Rg94~bacXo`1#Vd#b@6A zW7-BjPaPqFpPBqn7u*1PE1ON$cjUQc!a_&Nu~SRV==DF)3BX$@nnY0IJ9CJzC`Xob z`~UxLN0uy=t4*^oEZm@t&u{}?<75|?Z_j{kK0I8W?U5x^S0YnzTmhp(_L zyU+@vQpg2>MinfBh;vvGV^sBNP5e$C#+D4B$JW5Egy z6!K$uS{B6QomZCPF>R! z?V{BaZz#l$+dJqG@W1>ZPppfbIxB5b&>|0%!qmt^RzQ1)k}NBl$D!J@;-Q|dhH$~h z>!n08ec`|qL?|91%$rHd`hau+{BGgL)v!jLCr-;^WCKbD^fRn!Cy_LWN;YSb?A zHP)ZBMFTh1Z1)DMRBYWm>5mVwbwg(__aqqowYR@?wiZ{;@*upmp4Qe)C2p$2jXh5C zOywWdXFQ9Du?dx$)^`c6G@`NRNvr}S*0SH)GfAx#=N{eM(tCiJq{2pbvie%l*^cLP zb3>&J>dC?|OeKnca;DVfS}6Wa>R&df_sNbzsz}%XUQ=?k16Uc(0al)PnLxw=$As+?=P=JcrL7|kH0#&eI&wpmQmK+ALL6pV_Xk8Y%!UEt zS_$z;HH&tg8ZxJl6faI(gm~cwiXxfAKKH1UjVfs0rmHc1pJ+pjXKwca3czVZ41R{m zJWTMwy-~%NM$shkDh_eRvA)xzc=+Hi)d{yyi4?1*SRK#4U^;|4$L5H$XRzVK>SdMg zt$+1gKn)VKB*)H;7g$Wi$E9vtYiS98+L$5u4f3IRVP2%qvM<> zKVmx?>XR$uqXy94hWg}31KwVSq`>#{T~3&wV(uE&SQ|B)=<&&xlka<5IN%RCV`5S& zB`u~qjgT~ESR-f|w1wz>(_1IMVjtAu_wBanxTh2em342nz4@0nKYO!f*dfmeq_?9| zvBCko7jyE{0dH21up-|Eb@gCOmb^G$CF`xkfypM3vhi}!tQSz!@s?MpboAh4HR z8`Oq={De-bbfh#M?`|P#RFX1dj$HA{{2mAznMxmTS8hl1cYK zC?R$V#RiFybr{_5i471ZX*iz$xZiy#3AEwD)okpGx zDrNxGA&}_^MKpQ_Ov=!BYc;TrR?1ehvhgyGbi@*=0G0D4>>`NSsm4B!#^;X5zWpB% zwWO((8e7T|-0>QbHtJ|Em9mI0qh6#Wxa4F@R+BH`VZ7i=prxcQfmlOdf{w*RN%8C& z%dT{?r!OI%U8k@svHiXT;@x}+#4rHc+11A4iA?(vXkzds&_v-&Fte+LU1=HXOIXCN zGz5JK^Vsz&cGa`1id{K&?P4W&vMcRP_!8RLmAt$763Cs4FM-Zv@+FY-7mP}FB^4lF zf`*l##x-yxh3~@<2tyzYfiMKZ5C}sc41q8N!Vm~UAPj*p1i}yqL*U;J0SGO^e_;rO zArOW@7y@Akgdq@yKo|mH2!tUJhCmns|56BiHcem_?W9kWqNu_z;W6AVMw}DjkGMa8xL+dNi|4!X`z=By zf*Q{cAblOeqqzSw!UYJ6@Z5}0hCBs$j={Yiza#Mb3c`DcpM&Q-{4Pa!2=@c=dnPyor#3@G{bVjj$hK0K%1syBztZAhaQT zgJ%I@7s5{wb|B;+ekj5vxW55mIo{ibkc9iY5Z*%CT0HyktHSdF1RL(>BkpVbUXSp5 zgm>|L4Z>L5--KTyexJqf{Rns9or4IM;rj`)jke=+W(@cRk+nd{)VF$k9-%tly=uodB# z2#+AVjPMDD5rh{JK0r8*pzY+iD-dQQtU~Z0+>Edj;W30} zgbxtf5r)9)djf(LAs=BC!UlvJ5N<=*iLeXdHH425xNp(l2yqA|gmeTKLK(t!2)7~p z9^nOqzaVrVjQ$7u7hx7cF~SyvpCdeq@B+d?gwGJTE{+?Ikc6-Rp%h^Y!fgnDLU+c^dtKkc&`-a4W(e5#B)f7~yLK zjSu~Ukc2P?ArGMlVGY7YgzX47A^Zg4K7_{*UO;#Wfktd3H-J-d1Gz!mU{1{q;f8X< zI1M+P8^LKg9XFC2#f|2oxM;W>x`2z}#&YAh@mwr-Avb}W$i;D!xXIi_Ts)V+UCdnq zyU%i~;JKDU@#!Y$>NaaVB#Tp?G)UCkA9 z%efWYO0I-k#jS?tn=-DPTf?p8)^QbFC0E5=!&P%t?$YX#;+3wM#w%8?U8_9KEUs8l zvbK2n+LA?O>q=JU7niwvCk4h96}#QlMJr2c+|`wvl&n(Z>Js6(i(TMyQEiI zSw(3{b(y(UWqKWs<^s%T^~u6Ys*&j{$95iYh+@q%q`wEV;%L(3p~q0ho&F;PWdy)zu{x0fPh4AyANFt4dasttwmLFB@?i zOh$W7XbbqiNVO)BhkGnfcA8!^lqAh z34MPm#JK1#5Q#lLRpD7zR8?KMqNJv#vbrX)?m&ia%2vIBz|jl-a&(Vc%5l{zdjL?5 zWu0(_qz%;}->Tl!$2--VLcbBzee%~s<_+1a(hEwr2KQV*YKW#QJrw*_P089-ew;)< zNW`k={N|7D(Mc2=Vr(Kh#Mq?R;IUa#RaVif^H^k$`m>lG9l&DTK_i4k20_@3Nj!-9 zQeUqCC0JcjB+-NFK=j&BR$($Ks7Lc8=K8+VB|6qSojzN%3N+ADUD5-4rQ#)O)Mx2( za$w;gVMU;1MI{?olvKIPDl3X=N~+hFVSIr0ucQG%IjSnFidL*GDX#Dksbw*qno@rh z>lIc^Rdrb<_>@gW>xwsWp`t+*{n6~kv$mvKj#BzJAZk-t$=a1%P02cZtFoqq-6=B} z#iHu#i`ROj1lG3{3tj-9!A(^qra|QfG4xqDKhbaXkJ&gdRJT~@J%y~g5* z$qoO7ArOW@7y@Akgdq@yKo|mH2!tUJhCmnsVF-jF5Qab)0$~V*ArOW@7y`W@K>937 zP!j2x{zyM4E-FGd1%XB2lItn)l;lAMJ3VJ+#>S#d$TV3}Q2ZR)bfv$Z@hpnNVYwL# zGZtSlYu-E-F{i>^!uAc&C&jaE*5eL6j+vyWU+ycQ~29Jh}v zDydj0sW6pngylj6RF&N2>#9t!{yJsy(oth+JD)u^Q>zoJgkm$^9sD zom|#$xuWGItII07OUrh;W-eUBw7WTNL=mYHVbQ#f`xRGIyt3RwT30K});}gq^z*!h;(|Od|0tkj<^`F!PDbhCh&b;+4Ab*>P_4$3Z7)kDr*v^Am5&dc~I|` z^8r`Bj97s0E3oVgfTbJzHcQ3({KFRr|KZLsBzc2*C5C}sc41q8N!Vm~U zAPj-;1OcqO@qSFNb!PNr?X(^W5DsS-)-U8SzUZ^2hUAMcrA=^epf;bvc| zKyB6n=Ebm`#=?iSw7W$vSZTvI0efcw>Qx4KQoHCK<=gbs_q!Fa505}8mB>?toE2z! z_t#)MkJu8##sQ+0fI&5&P$ECA0z5Y09fEHh;;D>v$WwtjxKU0V-X++TBb{JJe_LRK z9sx*~pr%wy`f?TWN_8(~xq8RN!G?V%tk~n^-cU-EzFL8|=>6sRwj1S9|HMH8kb-{; zzGp)9{Vuu+3NCPQ62IpucRuISy@&W38c)u@d)} z<3A4fgyE|JPwK0<9$$z<85%-Q4)|ahsS`S+PYCURgv;N)sjWxnH%%-zlV4Gk| zuuZj@Y^k>0w%2SQ**>$KvJJKmw~w+(;m7)9gWYhIp~i5F;Woo>43S2SG0GTc zywqqiZa4nKc!zPP@qXhY#y=a67~73s8~R3A(jg)lP#B7jF$P9b(X!B zS1j*aKCygZ`Pvc#DDf$sDVtK?v{~(M+6&Ttmi9L4{QxcAvDkJ;aNHpME`5{!W&J_@ zhx$+TlMPc)^Vxd6WM1PWS(KpG8dRvo2yXoyUc$wKW={7+-QE=eAsMHEJ!R% zT%UM-;?0RaOZ-jZgNb_*Urzi>;?cy<6Hg>+lP*i@Od60pEO|`w#N>;UmnWAd*CyYX zyd(McCYpJ!$dK+-$QR}nTy}*z6t)Eyg zv0ZMPVVh^mvn{jL*>1D_!giPKKHC$v=WXfsZ2J=X3VVfpv;BJeFYNc&AGSYZ-)n!_ z{;54OO_LU#c1fB!ZB|-Yn#XaSYzt~_jq#7~|^9^~1BEydX^(O)I*9`9%h8PzbXPUN}er0;iblCK< z=}Xf|(*W}j^JsI7d4l-`^FH(7#I(eXi4P>c3ix#;j!!ZsWhXh4Rwe0@S0~?^{C~+B zj2(xi$Wmgdx4dL|2e|R2B_d@=iZ*3z%ET0F%Jh_B*3s4^jGYF+;k4C&*56}$$@X{K zx3+Qi#r9XzzDm2yvBa_6!8`upzyg{n=3lDM)i2RIjW-zIHSRH8V4h^Y)SP5?n6EVN zFyC%|(ENn?dGlWL=jK!9$V7GGh{P)rlM>e?Zc03ycs%ifq=`vcNsE&Tl2#;@CDkN7 znDkY$+A_uxZ<&g^rdwvCKYwp|-SUCuZw($p(bZK+qLE=(;*U6r~n^-rnqroNy0N$QuWU#Ff<9cUeC9c#6qW$D&gRzdJJRa|4heBe>ZiShMS|!ADSZ)rzDyaQxdOCT$p%u;wr%B*~Hfp zTM{FZMkb9(icOlF^pm7tCEb(sSkf~|FDAVXia0bmIeB(+cCs^hNpewgN%ETHXOrJf zJ_H*1WpYQd(PFV=Tkvv)Y`?WVWt(iDVxJEh=(Y3q zU)#U6tI~$2jZI5Po0jHDyD{ySw4bKknRZ{=gK6)i9ZhRZ`!en8G@WCtBi(T&U{~Z= z4z9s8J{sV0n@)RMVZF| zqc)qjng3$`o4L(=63z^V0#;Wgu1G9Tye9G5#BGTWB|ZlVasW{KFi}kWHqirEeVqJR z@(@d$#cG*uSz*~}xguq2%8yg-Ot~-Rk(B3Bno|aVGQ_4{l==hU&9c;*)KjT9S&vvZ zfkGa#AGNpJyX=F~GSlXz6{oF9bEjRKc5m8aX}i*%PurVzFzv&%ILB2qmbbxwDDdD? zy+NO&U#-7h|3m$+^#9NgG>kBeGhA%Y8#WuZ8*T^ne8BK0LyJK)d~P^y_{K2SIN7)u zRJ7c<-niAs8(%TLW&A(mSH^GQtnpG)iYd)B%XFpbDpQH68m-%%crfuu;=rU4N%NDo zCe!ldsD?stCvu?NEiCJ-%b+@(I`ik{E>oLrToz_!U73RcIwz0N2+Z3D8mTXJ2 zWq=YoZA&p?+_r0N+c94L1X}pCZI7+l_NwhY+hN<^Y^}D>Z5_4Wy zj3Lf&sUguY-7weSHT=|Yr{P}1?+q^+-Zbnry#m_)wP~u^jM={2TyGZ4zchE6rzbiS zmnIe`mL~or@y^6ki330rQj!)WElnyEsbo@t$Htpx9L!s@k6 zwBKug(EhspU3*4aecCf=ucp0+I{VV*Itm=C9oJ%R`p7|*y%Y6?17H2cz~Z%fkN#Wz z2w?9VLy2L(;iO>-xRw3JF{W6P!DMAvc^`O^DD!l4iTNAzJW#FG7>Bnf{yOo4#7Rlp zz@1#0d{uIe2rB1faur9Y=56bde>mL|h8E2bhD+2C(VfWdy)0}Aq zm^U}1U7r@=7~+`fFgmgwL>$^twM+Cz0Jo8b3jntrhDQObqlV86KEqX@6P3oz#v6@4 zGQMv-W;~7&6aji`F|9IHnKpsu{>b!8)7z#`KyQzmzBP@-4E4*zd%<1)0CUgP=p@8c%N?Ml_gNmaJa1{Xyq|J1WoT+^ z>R@Y}^@rBGtiJ;X@r-qkHPWWGU1+<+_Wx#JV+QnFJ~+=b*h~i2GpB7X+uXBxZu8D& zx-GNaLty#%#qO^ii@lP)hP|G>iM;4@R{Ko!%v1kfb|fI5toqw zF#XE_%Nh+MJtGq%DnFuncs; i++ ) { - extern void Abc_TtConfactorTest( word * pTruth, int nVars, int i ); + extern void Abc_TtCofactorTest( word * pTruth, int nVars, int i ); if ( fVerbose ) printf( "%7d : ", i ); - Abc_TtConfactorTest( p->pFuncs[i], p->nVars, i ); + Abc_TtCofactorTest( p->pFuncs[i], p->nVars, i ); if ( fVerbose ) Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" ); } diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 443ff0613..236c0d625 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -943,43 +943,43 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar word * pMasks = PPMasks[iVar][jVar]; int shift = (1 << jVar) - (1 << iVar); pTruth[0] = (pTruth[0] & pMasks[0]) | ((pTruth[0] & pMasks[1]) << shift) | ((pTruth[0] & pMasks[2]) >> shift); + return; } - else + if ( jVar <= 5 ) { - if ( jVar <= 5 ) - { - word * pMasks = PPMasks[iVar][jVar]; - int nWords = Abc_TtWordNum(nVars); - int w, shift = (1 << jVar) - (1 << iVar); - for ( w = 0; w < nWords; w++ ) - pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift); - } - else if ( iVar <= 5 && jVar > 5 ) - { - word low2High, high2Low; - word * pLimit = pTruth + Abc_TtWordNum(nVars); - int j, jStep = Abc_TtWordNum(jVar); - int shift = 1 << iVar; - for ( ; pTruth < pLimit; pTruth += 2*jStep ) - for ( j = 0; j < jStep; j++ ) - { - low2High = (pTruth[j] & s_Truths6[iVar]) >> shift; - high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar]; - pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low; - pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High; - } - } - else - { - word * pLimit = pTruth + Abc_TtWordNum(nVars); - int i, iStep = Abc_TtWordNum(iVar); - int j, jStep = Abc_TtWordNum(jVar); - for ( ; pTruth < pLimit; pTruth += 2*jStep ) - for ( i = 0; i < jStep; i += 2*iStep ) - for ( j = 0; j < iStep; j++ ) - ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] ); - } + word * pMasks = PPMasks[iVar][jVar]; + int nWords = Abc_TtWordNum(nVars); + int w, shift = (1 << jVar) - (1 << iVar); + for ( w = 0; w < nWords; w++ ) + pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift); + return; } + if ( iVar <= 5 && jVar > 5 ) + { + word low2High, high2Low; + word * pLimit = pTruth + Abc_TtWordNum(nVars); + int j, jStep = Abc_TtWordNum(jVar); + int shift = 1 << iVar; + for ( ; pTruth < pLimit; pTruth += 2*jStep ) + for ( j = 0; j < jStep; j++ ) + { + low2High = (pTruth[j] & s_Truths6[iVar]) >> shift; + high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar]; + pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low; + pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High; + } + return; + } + { + word * pLimit = pTruth + Abc_TtWordNum(nVars); + int i, iStep = Abc_TtWordNum(iVar); + int j, jStep = Abc_TtWordNum(jVar); + for ( ; pTruth < pLimit; pTruth += 2*jStep ) + for ( i = 0; i < jStep; i += 2*iStep ) + for ( j = 0; j < iStep; j++ ) + ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] ); + return; + } } /**Function************************************************************* @@ -1037,16 +1037,18 @@ static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore { word Temp; int i, k, Counter, nWords; - memset( pStore, 0, sizeof(int) * nVars ); if ( nVars <= 6 ) { for ( i = 0; i < nVars; i++ ) if ( pTruth[0] & s_Truths6Neg[i] ) pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] ); + else + pStore[i] = 0; return; } assert( nVars > 6 ); nWords = Abc_TtWordNum( nVars ); + memset( pStore, 0, sizeof(int) * nVars ); for ( k = 0; k < nWords; k++ ) { // count 1's for the first six variables @@ -1110,16 +1112,21 @@ static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pS SeeAlso [] ***********************************************************************/ -static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm ) +static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut ) { extern int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore ); - int pStore[16]; -// int pStore2[16]; + int fOldSwap = 0; + int pStoreIn[17]; + int * pStore = pStoreOut ? pStoreOut : pStoreIn; +// int pStore2[17]; int nWords = Abc_TtWordNum( nVars ); - int i, k, BestK, Temp, nOnes;//, nSwaps = 0;//, fChange; + int i, Temp, nOnes;//, fChange;//, nSwaps = 0;//; + int k, BestK; unsigned uCanonPhase = 0; assert( nVars <= 16 ); + for ( i = 0; i < nVars; i++ ) + pCanonPerm[i] = i; // normalize polarity nOnes = Abc_TtCountOnesInTruth( pTruth, nVars ); if ( nOnes > nWords * 32 ) @@ -1130,6 +1137,7 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC } // normalize phase Abc_TtCountOnesInCofs( pTruth, nVars, pStore ); + pStore[nVars] = nOnes; // Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore ); // Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore2 ); @@ -1144,62 +1152,71 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC uCanonPhase |= (1 << i); pStore[i] = nOnes - pStore[i]; } -/* - do { - fChange = 0; - for ( i = 0; i < nVars-1; i++ ) + + if ( fOldSwap ) + { + int fChange; + do { + fChange = 0; + for ( i = 0; i < nVars-1; i++ ) + { + // if ( pStore[i] <= pStore[i+1] ) + if ( pStore[i] >= pStore[i+1] ) + continue; + + Temp = pCanonPerm[i]; + pCanonPerm[i] = pCanonPerm[i+1]; + pCanonPerm[i+1] = Temp; + + Temp = pStore[i]; + pStore[i] = pStore[i+1]; + pStore[i+1] = Temp; + + if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) ) + { + uCanonPhase ^= (1 << i); + uCanonPhase ^= (1 << (i+1)); + } + Abc_TtSwapAdjacent( pTruth, nWords, i ); + fChange = 1; + // nSwaps++; + } + } while ( fChange ); + } + else + { + for ( i = 0; i < nVars - 1; i++ ) { - if ( pStore[i] <= pStore[i+1] ) - continue; + BestK = i + 1; + for ( k = i + 2; k < nVars; k++ ) + // if ( pStore[BestK] > pStore[k] ) + if ( pStore[BestK] < pStore[k] ) + BestK = k; + // if ( pStore[i] <= pStore[BestK] ) + if ( pStore[i] >= pStore[BestK] ) + continue; Temp = pCanonPerm[i]; - pCanonPerm[i] = pCanonPerm[i+1]; - pCanonPerm[i+1] = Temp; - + pCanonPerm[i] = pCanonPerm[BestK]; + pCanonPerm[BestK] = Temp; + Temp = pStore[i]; - pStore[i] = pStore[i+1]; - pStore[i+1] = Temp; - - if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) ) + pStore[i] = pStore[BestK]; + pStore[BestK] = Temp; + + if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) ) { uCanonPhase ^= (1 << i); - uCanonPhase ^= (1 << (i+1)); + uCanonPhase ^= (1 << BestK); } - Abc_TtSwapAdjacent( pTruth, nWords, i ); - fChange = 1; -// nSwaps++; + Abc_TtSwapVars( pTruth, nVars, i, BestK ); + // nSwaps++; } - } while ( fChange ); -*/ - - for ( i = 0; i < nVars - 1; i++ ) - { - BestK = i + 1; - for ( k = i + 2; k < nVars; k++ ) - if ( pStore[BestK] > pStore[k] ) - BestK = k; - if ( pStore[BestK] >= pStore[i] ) - continue; - - Temp = pCanonPerm[i]; - pCanonPerm[i] = pCanonPerm[BestK]; - pCanonPerm[BestK] = Temp; - - Temp = pStore[i]; - pStore[i] = pStore[BestK]; - pStore[BestK] = Temp; - - if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) ) - { - uCanonPhase ^= (1 << i); - uCanonPhase ^= (1 << BestK); - } - Abc_TtSwapVars( pTruth, nVars, i, BestK ); -// nSwaps++; } -/* - printf( "%d ", nSwaps ); + +// printf( "%d ", nSwaps ); +/* printf( "Minterms: " ); for ( i = 0; i < nVars; i++ ) printf( "%d ", pStore[i] ); diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c index 3ad447157..b66b276b7 100644 --- a/src/opt/dau/dauCanon.c +++ b/src/opt/dau/dauCanon.c @@ -70,7 +70,7 @@ void Abc_TtReverseBypes() SeeAlso [] ***********************************************************************/ -void Abc_TtConfactorTest7( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest7( word * pTruth, int nVars, int N ) { word Cof[4][1024]; int i, nWords = Abc_TtWordNum( nVars ); @@ -125,7 +125,7 @@ void Abc_TtConfactorTest7( word * pTruth, int nVars, int N ) */ } } -void Abc_TtConfactorTest2( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest2( word * pTruth, int nVars, int N ) { // word Cof[4][1024]; int i, j, nWords = Abc_TtWordNum( nVars ); @@ -185,7 +185,7 @@ void Abc_TtConfactorTest2( word * pTruth, int nVars, int N ) */ } } -void Abc_TtConfactorTest3( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest3( word * pTruth, int nVars, int N ) { word Cof[4][1024]; int i, j, nWords = Abc_TtWordNum( nVars ); @@ -217,7 +217,7 @@ void Abc_TtConfactorTest3( word * pTruth, int nVars, int N ) } } -void Abc_TtConfactorTest4( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest4( word * pTruth, int nVars, int N ) { word Cof[4][1024]; int i, j, nWords = Abc_TtWordNum( nVars ); @@ -259,7 +259,7 @@ void Abc_TtConfactorTest4( word * pTruth, int nVars, int N ) } } -void Abc_TtConfactorTest6( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest6( word * pTruth, int nVars, int N ) { // word Cof[4][1024]; int i, nWords = Abc_TtWordNum( nVars ); @@ -304,12 +304,22 @@ void Abc_TtConfactorTest6( word * pTruth, int nVars, int N ) i = 0; } -int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars ) +int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly ) { static word pCopy[1024]; static word pBest[1024]; - int nWords = Abc_TtWordNum( nVars ); + if ( fSwapOnly ) + { + Abc_TtCopy( pCopy, pTruth, nWords, 0 ); + Abc_TtSwapAdjacent( pCopy, nWords, i ); + if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 ) + { + Abc_TtCopy( pTruth, pCopy, nWords, 0 ); + return 1; + } + return 0; + } // save two copies Abc_TtCopy( pCopy, pTruth, nWords, 0 ); @@ -335,7 +345,7 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars ) // PXY // 110 - Abc_TtSwapVars( pCopy, nVars, i, i+1 ); + Abc_TtSwapAdjacent( pCopy, nWords, i ); if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) Abc_TtCopy( pBest, pCopy, nWords, 0 ); @@ -359,76 +369,261 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars ) // PXY // 000 - Abc_TtSwapVars( pCopy, nVars, i, i+1 ); + Abc_TtSwapAdjacent( pCopy, nWords, i ); if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) Abc_TtCopy( pBest, pCopy, nWords, 0 ); assert( Abc_TtEqual( pTruth, pCopy, nWords ) ); if ( Abc_TtEqual( pTruth, pBest, nWords ) ) return 0; + assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 ); Abc_TtCopy( pTruth, pBest, nWords, 0 ); return 1; } -int Abc_TtConfactorPerm( word * pTruth, int i, int nVars ) +int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, char * pCanonPerm, unsigned * puCanonPhase, int fSwapOnly ) { - int nWords = Abc_TtWordNum( nVars ); + static word pCopy1[1024]; int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23; + unsigned uPhaseInit = *puCanonPhase; int RetValue = 0; - fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 ); - fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 ); - if ( fComp23 >= 1 ) // Cof2 >= Cof3 + + if ( fSwapOnly ) { - if ( fComp01 >= 1 ) // Cof0 >= Cof1 + fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); + if ( fComp12 < 0 ) // Cof1 < Cof2 + { + Abc_TtSwapAdjacent( pTruth, nWords, i ); + RetValue = 1; + + if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) ) + { + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); + } + return RetValue; + } + + Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); + + fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 ); + fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 ); + if ( fComp23 >= 0 ) // Cof2 >= Cof3 + { + if ( fComp01 >= 0 ) // Cof0 >= Cof1 { fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 ); - if ( fComp13 < 1 ) // Cof1 < Cof3 ) - Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1; + if ( fComp13 < 0 ) // Cof1 < Cof3 + { + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << (i+1)); + RetValue = 1; + } + else if ( fComp13 == 0 ) // Cof1 == Cof3 + { + fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 ); + if ( fComp02 < 0 ) + { + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << (i+1)); + RetValue = 1; + } + } + // else Cof1 > Cof3 -- do nothing } else // Cof0 < Cof1 { fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 ); - if ( fComp03 < 1 ) // Cof0 < Cof3 ) + if ( fComp03 < 0 ) // Cof0 < Cof3 { Abc_TtFlip( pTruth, nWords, i ); - Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1; + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + RetValue = 1; } - else // Cof0 >= Cof3 + else // Cof0 >= Cof3 { - if ( fComp23 == 0 ) - Abc_TtFlip( pTruth, nWords, i ), RetValue = 1; + if ( fComp23 == 0 ) // can flip Cof0 and Cof1 + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + RetValue = 1; + } } } } else // Cof2 < Cof3 { - if ( fComp01 >= 1 ) // Cof0 >= Cof1 + if ( fComp01 >= 0 ) // Cof0 >= Cof1 { fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); - if ( fComp12 < 1 ) // Cof1 < Cof2 ) - Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1; + if ( fComp12 > 0 ) // Cof1 > Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + } + else if ( fComp12 == 0 ) // Cof1 == Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + else // Cof1 < Cof2 + { + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << (i+1)); + if ( fComp01 == 0 ) + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + } + } } else // Cof0 < Cof1 { fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 ); - if ( fComp02 == -1 ) // Cof0 < Cof2 ) + if ( fComp02 == -1 ) // Cof0 < Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); Abc_TtFlip( pTruth, nWords, i + 1 ); - Abc_TtFlip( pTruth, nWords, i ), RetValue = 1; + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + else if ( fComp02 == 0 ) // Cof0 == Cof2 + { + fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 ); + if ( fComp13 >= 0 ) // Cof1 >= Cof3 + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + } + else // Cof1 < Cof3 + { + Abc_TtFlip( pTruth, nWords, i ); + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + } + else // Cof0 > Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + } } + RetValue = 1; } - // perform final swap if needed fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); - if ( fComp12 == 1 ) // Cof1 > Cof2 - Abc_TtSwapVars( pTruth, nVars, i, i+1 ), RetValue = 1; + if ( fComp12 < 0 ) // Cof1 < Cof2 + { + Abc_TtSwapAdjacent( pTruth, nWords, i ); + RetValue = 1; + + if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) ) + { + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); + } + + if ( RetValue == 1 ) + { + if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse + { + Abc_TtCopy( pTruth, pCopy1, nWords, 0 ); + // undo the flips + *puCanonPhase = uPhaseInit; + // undo the swap + if ( fComp12 < 0 ) // Cof1 < Cof2 + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); + RetValue = 0; + } + } return RetValue; } -void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) + +void Abc_TtCofactorTest__( word * pTruth, int nVars, int N ) +{ + char pCanonPerm[16]; + unsigned uCanonPhase; + static word pCopy1[1024]; + static word pCopy2[1024]; + int i, nWords = Abc_TtWordNum( nVars ); + static int Counter = 0; + +// pTruth[0] = (s_Truths6[0] & s_Truths6[1]) | s_Truths6[2]; +// nVars = 3; + +/* + printf( "\n" ); + Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); + Abc_TtPrintBinary( pTruth, nVars ); + printf( "\n" ); +*/ + +// for ( i = nVars - 2; i >= 0; i-- ) + for ( i = 3; i < nVars - 1; i++ ) + { +/* + word Cof0s = Abc_Tt6Cof0( pTruth[0], i+1 ); + word Cof1s = Abc_Tt6Cof1( pTruth[0], i+1 ); + + word Cof0 = Abc_Tt6Cof0( Cof0s, i ); + word Cof1 = Abc_Tt6Cof1( Cof0s, i ); + word Cof2 = Abc_Tt6Cof0( Cof1s, i ); + word Cof3 = Abc_Tt6Cof1( Cof1s, i ); + + Abc_TtPrintBinary( &Cof0, 6 ); + Abc_TtPrintBinary( &Cof1, 6 ); + Abc_TtPrintBinary( &Cof2, 6 ); + Abc_TtPrintBinary( &Cof3, 6 ); + + printf( "01 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 1) ); + printf( "02 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 2) ); + printf( "03 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 3) ); + printf( "12 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 2) ); + printf( "13 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 3) ); + printf( "23 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 2, 3) ); + + if ( i == 0 && N == 74 ) + { + int s = 0; + continue; + } +*/ + Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); + Abc_TtCofactorPermNaive( pCopy1, i, nWords, 0 ); + + Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); + Abc_TtCofactorPerm( pCopy2, i, nWords, pCanonPerm, &uCanonPhase, 0 ); + +// assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); + if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) ) + Counter++; + + } + if ( Counter % 1000 == 0 ) + printf( "%d ", Counter ); + +} + + + +void Abc_TtCofactorTest8( word * pTruth, int nVars, int N ) { int fVerbose = 0; int i; + int nWords = Abc_TtWordNum( nVars ); if ( fVerbose ) printf( "\n " ), Abc_TtPrintHex( pTruth, nVars ); @@ -437,7 +632,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) printf( "Round 1\n" ); for ( i = nVars - 2; i >= 0; i-- ) { - if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) + if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) { if ( fVerbose ) printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); @@ -448,7 +643,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) printf( "Round 2\n" ); for ( i = 0; i < nVars - 1; i++ ) { - if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) + if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) { if ( fVerbose ) printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); @@ -461,7 +656,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) printf( "Round 3\n" ); for ( i = nVars - 2; i >= 0; i-- ) { - if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) + if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) { if ( fVerbose ) printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); @@ -472,7 +667,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) printf( "Round 4\n" ); for ( i = 0; i < nVars - 1; i++ ) { - if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) + if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) { if ( fVerbose ) printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); @@ -481,7 +676,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) i = 0; } -void Abc_TtConfactorTest10( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest10( word * pTruth, int nVars, int N ) { static word pCopy1[1024]; static word pCopy2[1024]; @@ -505,24 +700,137 @@ void Abc_TtConfactorTest10( word * pTruth, int nVars, int N ) } -void Abc_TtConfactorTest( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest111( word * pTruth, int nVars, int N ) { char pCanonPerm[32]; -// static word pCopy1[1024]; + static word pCopy1[1024]; static word pCopy2[1024]; int nWords = Abc_TtWordNum( nVars ); // Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); -// Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); + Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); // Kit_TruthSemiCanonicize_Yasha( pCopy1, nVars, pCanonPerm ); // Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" ); Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); - Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm ); + Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm, NULL ); // Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" ); -// assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); + assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); +} + + + + +void Abc_TtCofactorMinimize( word * pTruth, int nVars, int N ) +{ + char pCanonPerm[16]; + unsigned uCanonPhase; + int i, fVerbose = 0; + int nWords = Abc_TtWordNum( nVars ); + + if ( fVerbose ) + printf( "\n " ), Abc_TtPrintHex( pTruth, nVars ); + + if ( fVerbose ) + printf( "Round 1\n" ); + for ( i = nVars - 2; i >= 0; i-- ) + { + if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) ) + { + if ( fVerbose ) + printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); + } + } + + if ( fVerbose ) + printf( "Round 2\n" ); + for ( i = 0; i < nVars - 1; i++ ) + { + if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) ) + { + if ( fVerbose ) + printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); + } + } +} + + +void Abc_TtCofactorVerify( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase ) +{ + int i, k, nWords = Abc_TtWordNum( nVars ); + if ( (uCanonPhase >> nVars) & 1 ) + Abc_TtNot( pTruth, nWords ); + for ( i = 0; i < nVars; i++ ) + if ( (uCanonPhase >> i) & 1 ) + Abc_TtFlip( pTruth, nWords, i ); + for ( i = 0; i < nVars; i++ ) + { + for ( k = i; k < nVars; k++ ) + if ( pCanonPerm[k] == i ) + break; + assert( k < nVars ); + if ( i == k ) + continue; + Abc_TtSwapVars( pTruth, nVars, i, k ); + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] ); + } +} + +//#define CANON_VERIFY + +void Abc_TtCofactorTest( word * pTruth, int nVars, int N ) +{ + int pStoreIn[17]; + char pCanonPerm[16]; + unsigned uCanonPhase; + int i, nWords = Abc_TtWordNum( nVars ); + +#ifdef CANON_VERIFY + char pCanonPermCopy[16]; + static word pCopy1[1024]; + static word pCopy2[1024]; + Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); +#endif + + uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn ); + + for ( i = nVars - 2; i >= 0; i-- ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); +// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); + + for ( i = 1; i < nVars - 1; i++ ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); +// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); + + for ( i = nVars - 3; i >= 0; i-- ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); +// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); + + for ( i = 1; i < nVars - 1; i++ ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); +// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); + +#ifdef CANON_VERIFY + Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); + memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars ); + Abc_TtCofactorVerify( pCopy2, nVars, pCanonPermCopy, uCanonPhase ); + if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) ) + printf( "Canonical form verification failed!\n" ); +#endif +/* + if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) ) + { + Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" ); + i = 0; + } +*/ }