From 5486d5ef9ea1ddedae0fb273efe9521d28af2e49 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 20 Jun 2017 14:09:50 -0700 Subject: [PATCH 1/1] add notes --- design/notes.dot | 7 +++++++ design/notes.pdf | Bin 0 -> 13301 bytes design/notes.txt | 49 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 56 insertions(+) create mode 100644 design/notes.dot create mode 100644 design/notes.pdf diff --git a/design/notes.dot b/design/notes.dot new file mode 100644 index 0000000..713fa6e --- /dev/null +++ b/design/notes.dot @@ -0,0 +1,7 @@ +digraph "Passes" { +TreeConstruction->TreeRewriting; +TreeRewriting->EncodingSelection; +EncodingSelection->Encoding; +Encoding->SATOptimization; +SATOptimization->CNFSATConversion; +} \ No newline at end of file diff --git a/design/notes.pdf b/design/notes.pdf new file mode 100644 index 0000000000000000000000000000000000000000..c9e46f7fb9f2afef6c47e5d596f049d909fdb063 GIT binary patch literal 13301 zcma)j1yG&K(rs`J7F;*(vVn~S*WfO}HMqMI+#xswm*8%}Ex5b86C}99gXEn1pL_5B z>bF!xm1+|7;PFR#4$N+*TuRSWehi3sW0j%}S;JLX0j8aBc#ttR`))zpiTj)6$2^$$$8ydm$^1|CY*cs_r!n>rVB@CP40}*>qyx`mT@g)=5 zGA}CR-~$LJ7%t@8=A^2qiK)qWE-q=k-JQgl>BBxg8X9R7@xonUh_aF?-weH z26;OdfF!X<)d98LQMI$S7f(5KE&`q3JZf(qSE~}bqv#k~@6gfuCDYZmkq37)u@Z@P z+^&FE(JSmheKlCevmT3I!aPFwc3zG*cMb*I{R^}D{TsVyDuyVmI}&9pZ}gKn%orYI zMVPk8I&OUAQPQbZ(kP+n+2NhXCvA^8S&YccRNzGPrl6CNW@)ZGZVM~+T~q!o2`Nq0 zHcTBHrie2QmzZW_1zTcX11IjOOKW&Me#jTm%aqt9^5K+>efN3! z@+~`L?AM5(fxS!GxTyG*tP25O-r%Z0L4pMtmnLgB_8Y~6g4rp7@5zna?3IL&Sf3&@ov145BC&pF26oQ5L+CrI^3#FLZ7JAbTnXCR_H+- z>4PSB)YHbS*jSF%duxcNS0%rma45^QY}zDHXl3ruBJFPFNCdl#uyVU&x{v2dhs-w6 zs>UB|^sb+rAAKup&o0%%_fJJzgik7$z^L#%vWiVQYk@*CpE)OhDf@{NaoKv#X25GM zgKe%3jI0qHat^A8GtR-OaHjO|d*8K~=CmR40EK12%nWa2W%w7HUVgpu@RfY8-!Jsz zU;(}MzqXkF#nRur6mfA7Q*?OYB!HXy6?l0V^_X5707fAJ01&`vp!f3m!qk_JKc9@E z)>aPxu>M5PL=Oaj{$~1%(aYpl}0SO5b zsMufH|8dZ9{A*eN+d=m_&7Tty2mrExINAQ~=xcF<^FUW_JmJhQYAm`wkU5box+YK4 zj**$z9}}k$r-bZ8OW-GgM#F@P(?iWEpgN!mb~F0bm_^FG8R`ayn$%;vP7{nk<1Ctr zlV~eCe#&Y1>6pM_1u^%$wFoKr`gWzM?b^L?0L>32w97+j{>; z>?~oPI3DvEdX4jZ_OfS;ICoTq=1|zP&gN^NRs|Pk?GdR9d=Ax`Yc|68Av$~^wi~<% zYLG&QOh?}c_4D3Ql4V%;r_>Q?qQT*{wtnf|Ub_NL_JmDYA*FZ;yyieAZtYJ6HakR8 zvwT-r1<0e&dQRb*6}#X=Mk3e2(xJ1|l=FVqC{^!H$P7`ng@b*d1Q8X}7QRQFbAfEV z=YL{SRwm#?gWIPH6jMp+3fJI{XakB+CjtN&6Y%`Qe9sM zH;eng3-vQQ5JzBho0yfSHQWZ=jGSecT-s_`~bv2PQHNNOOGVkv?3zHYIy`r;MU4d1i z#WgJEn5Q~X>D@Y#c*PP~UP~EY*c9Hy)PcJXOc@o?TP^udPGeS!uV0J5{WNFSbEvGH zil9>1+;ccRbD*ApR*p8Qugt`{ywR51)TXwxUDSA5Ea`^5U|uAbFt7BG<0*;vZu~B? zwn2ZhnGJl%-zS!2Q%3=zaJc|cW+}pp^s0PK#Y_c{kzHrdYOQSCf^|uE$z;KVxARiQGftD%={qR-8k1=& zjW0Egx6aCH%787-&v(&`D9x%=vV`w>2D~94IeAiqhjSi>8{|2DW*N3wB2L&FkG9Fj zn=JxV_ELj^Fa*T0-c?8{ITK_I{+d{o@KaxQ{h!e0cl zx*mT|EwS>TVpYt{JlqtjShpq1rZ0myY!$CbXEW-DXo{;9dhsHZ%}mp9z*sJ?HPr;;S%& zHyWb7%H#k;D{^w*8OtM5>rEm^%M5G2l`x!!2B{GV zstn+FLX&R|sP*kf)BDr23O5g63sOJ{SI$9l>a%Cp@*~4A!7zV?9m~e7gs<+0y(lat zev%rV8=qzJyt)+Xwzkpfn$U7Cov$!(k6sEI3^n%lthoVmN^M7;rMofAbvaCQLy~ z>iRNFlh{pxU5{9nPrY{h89SN`vmUr=y>HOCvaI!i-!c+HdV)yV#C~9cgW35XjoXbC z0@%=^O6aL`Y{c=VK?dSj(?$mq(<))N;4QR;w9&Z=Z;@n1%myf^2OY*?Fsr7zK`c8v zKN+q2u-w0~2A@-a?hbxj>0>?h<(0HxXP^=g3qGWn3FI}qr{~jfA5H5wEB;_eEILJd zxM;3LH9wj=9iiC(mq4rW@Q7;`I1*7Vz*WqyM~v4)2r;W(*iOM%czf_Rg&tQqPO_os z>20771l1Z556rC#n7c?zdFM{m^VdBGR|0Sov%P(C-VZwqc-C=91$35`>V^z&$!)=BXWGX-#EL$LK|LG|cif#yl!KNk8_c~N z&r{52`Kq$6phx;>ElPCHKw9(TEtf%*S1a*NI{83mB>W$-GoZ5MNp&D8RozOX?r>eO zgw}(#pQGe1NOOtP^)WKbofP`5Bg(P-`_w@)H>|U)Tm66upEO>5l6kufK_z$P*m;T; zbtTtnu*#({4>D7`1!18)>NQ!y`@Yl0&77VtHm}29z`nB+A^()#z!m#BZD&>@2uR%_ zl{}^b+UgAEe)nOukK*1zLN=>|8qgH+jN;kcqBV7q{H3FMg&%d;mGrc_nItsaH`VEd zj`r~1v(hgeBd8C&$5k;*{1Oo7D_YuB zE1pyCguW8E5)hy^fg-TAFM>`S*+d3?*C%Z2?{ZFTkXk%saPJ!~j+2rKLeDHuX+Dsc z!B8Q;jE@)4MxG^D$l&L|K@=xR36>;*r#i$l^%jp-jvkj6mnwbpc0{~j2wqgjXG|&h zYTa%N8HLa0GhKT7o6L@Tu*VO=V6|@rvCA$8`uKwcusyRx=}hgC8;$89De0V?MB>}KbdmG?(O)0APBRLFdfB#fCO57m(2~;in+^1Nr5i5XVkh#I z4pT5jKp-npi~7m-Mpm@p82)O8c3Ixls0Pd$hIgn zDAaZ~ciKhR`5oY%gD@Tas~6NTtZPw=OT(2-aV&ACdY6s9mvrY{#j3RF#>xpsk0QjB zAwx@0btLg{en#zy>>%f`MFy8h`hJsYRXz}0F+Lm=J%aFMKu#M|&@GCMY!HzVAwrmy zl^8|bLq?Qtb;YAq&ho9qeLv{_9kq9()!bLOsymxb+-u*%Dh^o#@cf*XU-56+PBvjyEB0nNuYoT0*5x0r1me@k^fVK4+ zK$KNBS}bZ2ex98y12`iKFtB0E1$>qjju-Ppeuv3TbbjaOf*%lrR{RFaP-%(VQ^_}i zoN&Dj+D9>-c_vLPsCFs<_dV(Ufqlwdzot=1B~T@K(cxo@LWaWEVgvUDE&P5&Oadt_ z#hfL#p3I^aH18$-s0l8CL`QQqs}eUYh+Ueae)y|ivI@AV0`NzX=Elj>)>wZnm`5>> zlUtd)r>37ZQF)%9GUj#G;qS1q>K7lIzwYImrDA+}bK;mn;^oOC*HLZOHi`vmTxM`? z-?f8UQ<1%Cf`Ire{dxTj0j$ZuK&nNjFn3BY%fY6mRmN%nj&*d3xemEoCDvicV|N9v{hB!Vjqq7%Av<480S}?6xp5mtkIw zo;?xgUER_`Z|RH0Kb?%7MDj)uA&;8S5mGJ8)Rq&ymx%OVK#HunISL_pU#GcT8Pa%g z#%4sdVt@8ojKIKKR++}vFqpbbeYOBzqE4dwhI%KXK&t?(q(DQ+f+`+loc7V$Pd3Yt zlOTUrY9MYH>r%^T!9pQWJPCdhCnk%zCcAOwi-b|cY24(t!!(!FCpl#NL{Lg@s(xhU z!bb$2jZ;q1jM1NA`DVpwV;x(L$+c`kObSsB;T_W`I~cywX)LxshVos)U52oJB^9Ju zsI((E%zTMqR4(j^?VgVw#G+h@#xlE-z4Es)Q8=ru6*9J*0P`I3p5kMztBWJzTGSb6 zVbt(!0Gi9tRN6>*L~bJ!MVj-~nXu9Lu`L$zID9~$hx)^NJ)F1H=>=zGr;WnO zQ<$3dQ9q=+%**7<1{~#@cn#mMecVfxvH-0YILT43^e2mc}etZnXriHEH zInZ95(BTfTo=8&Z-tbb7HVhVZ>{e;-aBp8Z5I!ICaL~k0omiN6a{p;**_4L(PLFwj zO-!TClHAetar0ZR6@AyX?`>}-RQE|b^n*=lRxWYZ|?UI87s^r9D^lX+KMzO-Z zt>pb%q^LA<>5t0~x5R@r9~T9q{6Bn9piSYW(AwRXWUULLH-dUVkWYNiK{=|SkYJf0 zMpq-!m~`hB+uL&|CNST=T6x{WpKAyg6FmgvNFm-|$_)kX2UAF~Qj;!goJqgU*QXgDOZHJoD7)kmUokYKrZzcY26s{j3Sh9t~EoO z`Eb8b?$^*!8|G&ugwU{|(@ncm_pt_25%Oo!r^-lwXGG20FefvWfHAr1W20^TjvUp7 zSY+OZPI^V~qg!#@9D!iS`-GGMMOFGcMQ`O@PECw8a-)$%Rd$!=M%6bQH8L zv=(O?BQfW3d(S+(%Qrr8@9)S+(ij~z7rGeUWo?!Z4_#%rCTQYM8O|y?mzr$~b|cq0 zG?8`>g%^ir6@SA@79I5E>F)jPf3~aurKTT;BWOG2!;7xEOyo*)rm__=FiIn9Wq6FBu}gh@74K_#Y%&a*#o{%&m<1{@*Mri>>s0re3?zk43}&|4ZRCTPVv^) zDyn%gHSt#g#j#$r-BYY%J>S8`+)^z~;DcJsh|*XCMQEYF;t}*2ogu5P!Nb{YQAj5x zKIR*FhSPu=vv3T`bvwZ2B4Ju{BD=aA;@|R-+m)9zx@c)_fwu)U)^e`qK&I|#4 zoD)V?^y=3KpBbrmSaX#<0iJ$-;VU`ppA^jkF^JK^24s6u=HZ=(HzK^e1%M)p7!^R5KY! z+|@FNG;-e9+mFRKqnRT#qh-HJ)~oR+U8>0F&8`jRpgh6AS}r#84SPYEvbD1H^aJrP z*XW~-J0%{0Y?aE6MWuREb{IaT7A(V`@JSf8wXWG8s1vS)3@BNNBH`QnyF6>wG4&c{jHd zEBShR43y|JW)Yz09QlN7pip@=GPtj_pL@n**_fJqs`IV!Yt!mD`Mt>{$57f?(eZcR z0xPOyE+s$B+zu@`p3P6YY=i?d&o2Q+=w+T1NMCwkMc&ZyP@znjHoz+*M~cSLh>$P) zHA82K3C4TKI57)2tW+vEjgTQEzS(gOXGY128GtAra?8>ZT_>7x(5&`8)k^EXzZ#Mn z@iunuMb+vXR{l|3#MkO^+@oYR-T&r2NiT>pdUnSVax4=3$B1vpFm%*%q$%a4zpwK_t&EoNb^zQ3VOZK66{LF` zuDt|uzMK+nR*phmDDJv+Kw4EnTx#ODUXw^(rX}GJv4UwWhD}s~e5f|LnCk^s=y^R= z2>kvpRDWAaiy#t-Ey;AJx!xWNv|Bs09@`I*F8wW*9J?^kpO#A`ef0ol#@?L@N~!s>tJ@}okC?T{eYQX{nM6JQQz6Ud#g!6{*~!+9tTlSPwRLf*?I z!kL_oseXrE^4aj9*@p*_yZDy`gKW58x8FUGA)SCa-1~MUY|ej}vGs99vbzn_`+A}+ zCe6k6lpeoV%Y~whs#Vzo%(=Dhx&4cN*3HtFb=9a1w==VS2E_qvYsQI8RxY}$Y3iTN z*9%0j$4I=Gyf{x>LxsLlE@shg+&+sCbG@gQ>Z*5s{Mp0Gj~Z>m2GJ2h`J$!SNst-A z-!^>(a`Znm#G0Q~%Ouc+6irTZQ6PWt2`*YVvmr6%Alp1WZK(xKER%cM-F#AtnHk^N ziP=2iRu@{eWtsy=4b3Bwf~^J%-eZCz7Kuh!50R8?tem-mp=g%E!sXkQ8akH|2s`A4 zT4G;^#c!_JJcDs6OLCJwjStw@RoD8Y`2+t`(#$~^rX|na?&GC=WtpSnctz`xY7jgO zrV?hnfh_HrVu8@4zKsDKN4b)P)#cRl>D@p z^{h*9$GLyxQ259YsuvocR+0e7c*C-6Px1!wj2KliquTB!oMTvw9WaY13m5}lE zQMf)R;%ZKk2hmQxrLk#hwG3q;mD#s=$KrVEGx=jI?%;~T+%XoQc6k`S-yl97 zT%;j5ZRQO~{!Z(~EyJ}5#r<*0DcCXDa8PT*_KQQP+<7%pBONz+f1kR;Cxs_$RtL9& zRf>*k`{Wq?Xyq;kxN7Ol8hfvUxw=RZg%T{jI+^D5a)YW(`pdYoT%9Uyy?XGQn?(?3j2Iba7>a#TU}K9zH&0P1eOmM9K#pq4Qm|mOkem#`DnW1<~p5RmSwLX{y^{A(G$c zjVi`C!iyF{CRO4{-pon3npdhe4zLIm*&aeVt?-a;Ij23oKgE*OSt+`lbm4W(I6BNK zJF+;9QYo@LFnX4!*dHr9_0G4-x%!NRA&)QS*z= zHLCr+#3&JYP0w?BM?6zwL4CR3K6wipbko6^357-j{T&@(E2SMcnPIjV9gT=v@qGSZQ13y7s-@eeXfJgHAG^GxZc&X2qhVQ*A`` zBtFe1XZ~yf$#x&L4O`x<VxT@Xiu%;ek>C$`aaz*!V2jIJPaBnd zne85#&+E<-PZiz=sace1^B?EqV`3i$=h2=!$#FLKm!Nc#CDTzf&yWUX(EN0qs3Zp# z-GuUKSC+!DOD^uk*n9L@# z?~@zzc`_eOLy{LG4YHj93?cTYPqR-z5&0y>Yu;=TQ00?Er-_J$5>&`OrXDL4SN3FU zyN7k&R80y+R@1i8pZWnvY3#w-1Xc%Hmv_uPcS1h#;kEM<{tOh? zy|1hMcz%~3rXyO)VYhPi=y-ousp`A1qft;SA$pRgRkr7vqpG=BLigw`f^xXLImNIA zvsA-Wg7lT;AiN>*>*y%^Q2kZI{Xn99;#ndtLoI`|PG0kXo#XAN?N5UVXE0+Ba|4yB z3dtZ}xQ>tXbnkoBw2v8#<1r&E?>#(l0<@s_S%jkv;w2D(n7`&BVoSG6GQJZxd7rWI z1)Be?eafn4D<-}_9ZQl%w#CP8%@VVft4x}2Gw6GEZGoanyhUZjmg zH3y;>8cGNcSOOXA6jUcdz2lT7xQ(y`qKe~_F3bz?d&FTX>!RrGZEqy&33$S_ec9PE zr^o6c9$~kfiQK#%Fbax=WOKmppsBy$fwHx+w~;Q|Z}cu;@6bGXTFoD5+gXe*%``>+rUs4f|n~_+Qs`Sw-gXWqS8QKQQxh z9pkRD^CH>b%k!AUFA@pzi8hVN=B8!lpvd^1GQn7p@F}yD5tI}1K|EgagHRo_!qy{{ z_qgWzANOG05IQND%pqsj37es=~xUNDAdSdF0A~S-pzPJl{nxv!kFBU zxnXt|?6jlIh9G;z~pLxMN~_SgiF68bqlZGzDFcBYAd zfWJIbr|aV*R0Npw=^VWITo7N6HyP|3cXUzrSaoU3ysNQbui&R7Q++lpBF1$5Hiw7w z)B2w0_lM~KOcNpj9N0@HF_x5oolM>ubQ90yAtK~V9ur0`*qZmBdHIQQfJ%_&g-9je zR6I~yp`X!-dU}7Y!V+_%>W)y&OF0R02uFT-7w2cEh*}h?{$W}2C^tR#+T z(ohH~-TQbIGEt_59p(H`0tuphxZW1f)j@B)n$q>x!; z^%M;;ghItIMk^C5N2`c3Q8Q25+S3^x=mqflTDFMx+?a8;4jsR8M`uH4eX6*CbR| zY5w>G`xjymbl`q;TQv(q{G*>7&_$rTy#l6)t98+Mjs@U+?opo)%fomp%hRnOd+H%O ziYNEopbux5+&)t<{=hc|HO0ioTeeJdmCEH}_y226;!+q36 zAT(HChrFft-H!xC8lxO?=Z#rG-sd3s#kHPowhy_4M_owXt)6qoql1=86`nTxHrFL9 zSIv_@kHS=uHtWcry1V*Txk{p>n;BYmKbKXz>m9pn!<#;B0<0QmR zSelr9A8x%*OE0MHZi+SdaHKHYE-_j$v3j7>>bU)841f5Tz&1G2=~=hc8r$(Ya!#a4 zGgy_dMvJc>L6{TUI;8%?K3VzEox)wvSINsZj@*QMf+vDpt?JQ9C`p#v{C4Ib9?327 zhl&|DYIT*UI)=g^t6x96Dh4sS2I@YSdO$RTh9F(rjDOC;A`S4l9W;Ub-ho0hxAHj2 zkC2g5cVSI3`mp4_R~7rjEw{J>pYnN`R;;Nro9_Wj%v0F`WB6a@^h5|(0tIW(XlRpHNTF zF_xL}uAYek@E9_gI>`fCZ!29*zVKdy*lg@>^CJ+pE?kb&j6)%e zPiBtgln0(a@{H?9U=+aO9DUi~x8-lz^cZZ&2;&TGzA)|+aUvymqzq*`mrD^XfF@+z z79AAFoF}&SuOr*abE0il1aox!m5wn%a|b^KVJT3+7?h8C5En|<>`htpIUnJmWK8UU zHtUS*f~>6FIwoMt)9f8j#1q!HSXUiln$W}iCG!EI0<$T?%k31IVfO{1gPFb7iD%!F z?KURF_$vr1GkS{y?KyG*ZhvvuN*x+)5!TN35McCmQh{pgd#s6I-FPT8QIBnPFyH#7O(!EXrJRO`usHchbY7~diNnj-8w`iw8| zKIGy<10Jlem;|Q-*4Byd14SqQ02s~3x1i#zPoSxiKwMmUUj_D|iVuXg6mhv9jR*43 z<5IHXVkE_r=;88mHPK+%eK}8EA2`z^jZbC~%1fr<7~gOtM`DtKsYWbuDZ0S%A+c3r zu9Ek%hj2w*)e|1U5FTj}9=#jPs(7Yh#TgiPW6JHn(8uwqWuR_de6PeKUJzQ@+1bI(k&Bt(ThCW>I$U zS1NTba;lWXvoTF$umscb=5Nz#la7juUapsJ^2D3+eAHA{Fri*+JC;SL9N^0GvBpc* zfa@P7wa>s*AG#4m&jTKsybDF6Zb91Kc7TxS-=F3nuh#*^gm;>&hO_b@_Ah+-7Rw(w zC?{y8$r-~7S9?inj|ERJk(!QOjl0cB9TCO4{B{_FG~OD49vWX14&VRajl|%vS2Q^F zrF3rSmj>d!kwd?LNHGNLDA;a#C|_h)b?ThX`(it+Qe8gbIU=;-Svu<>5?q8Zm7Q3^3@yDV?BP3T88t4v9Z$CdF$~4$%#> zk~31K_3v&UJt$AreGf>;)iAMe(@2U7N(+bmxPOV7^^MilQE)|Dd6JbFdNBtX7Q?<6 zl1M6~`}>$ZbyM(>9*YJ2SA8LiXnN!2k`NXiz_H5|p^hJnZ&1$)KNgKlk*kD_b{RZh?9bxeo*)H~!Y@ho^@vryX#6xVUP~h7EB@40v8+ZFGDdIeaJcO>0>v zrd}V+wAV&YM38GokCyMFztizm@oNGg7I&>$>@Dw|cN&i#G|f*Q(mRghpfzZR9nJ5r zS?eW->m}@KC0}35G%GZtW zHXIozS_VD?B)jg_dmG^fc_X#n^J0m~k@XxUP8FEiDSSz+qm)8Y4gW0XPvJEPtKIWc=eH`j+@yXeVe0 zIhlx=&(N#y1z4YE6ty4GeQUa0FbG{Re~;~@-V}G2QeWvXFU8*INW;@+89n^JC|Q3e z_pd@Qb29y{E(N}dNB<#QpZ5*uaeoIGRAsIc(7wxH{l#GC+I<1na zrI9_og0-cd)xQix^(;*-Tme+S`>6lG7JA0^0M>t*2>#Kg(lax$0O(nnIRHR*CME!o znH~6-MpfKF&%)F|z{=Rd2*C8)O~BsZRpZJI`qO+}*lU}f`7c07&*p=XsjXY@W%d03@!N}P3MP~exDuEX{vC;2Ty~2aoUAVi{11!?_)_Hmz&M#- z$n|d+@P(}ZH6D-&^xqgW`wI{M-51FEvQPgL1HGpHKkPU-Ue2=rz&M#+QuOZ_Gw{D+ zdpS8?`0<~19Bls>&%sXb<=n9QeKAMT)XnHMf3KWXu(p2L6R&mn!@F0Wzv$Ed-f8v@ WdUg)KGY(|t1hT@DlZ(iT!v7y3Yar7A literal 0 HcmV?d00001 diff --git a/design/notes.txt b/design/notes.txt index ce399c3..4219c89 100644 --- a/design/notes.txt +++ b/design/notes.txt @@ -9,3 +9,52 @@ future? (5) Could simplify output of functions... Maybe several outputs have same effect... + + +Work/Passes: + +(1) TreeConstruction --- need backwards links... +BooleanVar/ElementVar should be able to query all of its uses. Should +go all the way up... + +(2) Naive Encoding Pass --- add an encoding to every Element/Function... + +(3) Encoder Pass --- implement encodings into constraint objects... + +(4) Test... Make sure the thing works... + +Next basic implementation phase: +(1) Extend Naive Encoder Pass to test other encodings +(2) Build more clever function encodings strategies (e.g., equals, add, etc)... +(3) Test + +Actual research: + +(1) TreeRewriting --- probably should do Equivalent Subexpression +Elimination (Don't have the same expression appear twice, instead +simply link to it again). Possibly good to do in TreeConstruction... +This could be lower priority as it isn't really essential to make +things work. Should also probably be switchable on/off... + +(2) Advanced TreeRewriting --- can rewrite functions/predicates to +eliminate unused entries or to eliminate effectively identical +outputs... e.g., consider a function f() that can output the values +1,3, 5, 7, and its output is only ever compared to 3... We could +rewrite the values 1, 5, and 7 to be the same value. + +(3) Advanced Encoding Strategies + a) encoding alignment --- making binary index encodings over +different sets work together + + b) Implement K-Map for function encoding + +(4) Implement search framework --- probably simulated annealing over a +population of strategies... search framework should probably be able +to turn on/off nearly any optimization we have... + +(5) Implement backend translation strategies....do optimizations and +implement other simplifcation strategies + +(6) Convert SATCheck to use Constraint Compiler...not sure about order... + +(7) Profile system.... -- 2.34.1