From 696844ea23ece1e4251ec0a624bf24a9d3a85d71 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 20 Aug 2010 10:46:56 +0000
Subject: [PATCH] started to rewrite the CADE07 formulas as FunCheck functions.
So far they all work :)
---
lib/z3.jar | Bin 148167 -> 148414 bytes
src/funcheck/CodeExtraction.scala | 24 +++++++++-
src/funcheck/Extractors.scala | 14 ++++++
src/purescala/PrettyPrinter.scala | 7 ++-
src/purescala/Trees.scala | 8 +++-
vmcai2011-testcases/CADE07.scala | 72 ++++++++++++++++++++++++++++++
6 files changed, 120 insertions(+), 5 deletions(-)
create mode 100644 vmcai2011-testcases/CADE07.scala
diff --git a/lib/z3.jar b/lib/z3.jar
index 37ffb232df24c3b5aa8e35181a736edf576ed751..e40a8c348760944735605957c8a5d45f5dada7db 100644
GIT binary patch
delta 6716
zcmX@!%DJzdlQ+PdnMH(wgMowLQ-sJwUMpr0<#m?%d4$MjDaP+iV1@{b4kL&$*_rhz
zm<~`9*=)~d%L(Sx^FIX9o0A2mf>mw)Ey&8q{5nEpGqZ3j3z*R@-oOrGOm<ixvsp`C
znHj{{9H4X<!Vput!vq%jsxhAp%$Tlk1(uo|9cMB5ygtun3FEV@AeqSlN-~q{Q`k0h
zS*n5cOukSiv)SKz4@5agHvc@^W&``RVj$(4AB3I*>)X6BdO2AA=IFRnV8-Nir)8$|
z*E8~L4oDP$=#F0@v$;Mc2khp__4{Nd%L{XC7Rr1C_RZwV2{MzpA8}1rFk<4G+*Qf5
z**N<W#3YcdDtQt0eTQwU-&=k!uX|p8e(%4p-}Cn~JMe@sIfbpCw*9K*+6Lk4&pf`Z
zm~oxEd1~&`1p*8BdyE)2IW*k9=H2$|jKTxodP||Le=eS#n37v6#H{638ESjr!>=#<
zKDl&?O}P|jl09YXCAnR1E6-|Zu^&`y@fO^$vORQZfZ_x0*si#9?^oB~K9*83nPKvk
z@(B~I*G|3Svvo%J>1?liPc-6A#VMa|lzx5S>F!-^Ij3Yg{1!AmTqq}1@xg)lkYvB<
znQIgFZK}Rhq;;&ma=xLVcqz|$&D66#^~V}-2lu+J-Qw)P)w<qk);dr14GG4Ze+xcY
zl_ax8c!l$v`t1TQ_-kA4f8}Jlpjq$0ULu&WyYE;?id6T5&9~w_4OgW;d3W@J_VdRq
zax9Z`PH?Whp!Oh~#aZ8Rnb)zMxBjwJWu3lVwXne`vr02+jnp!;^oGt=VK)r@lLY#!
zytFfqnV1D@%qc!3aD=7fkin@qORch-i6YKZnwhVPB)m$#JK<mb$qgO;50-V>`Zd(n
zFA`a`YO3+m77HIP1BPIhsH}*mStl=aWtl9r57u6N^^%mIg+t%DJ^ylik0)KV6^-6$
zIAzzGYd5XZeu<<orYSV`=DskM@|)2bXZ$yp$#**c;ZO6r&GR=M++f|X$6~|mMfyS?
zt}L1^lKlJQ+oDMKm($kml$q9cnknUhp4zUc^XKZVPMtld#kFUi=i0>nW$QT)SzSw*
z+phD(M{n=5jrDE|EVq2vs4aI+F)3r=wEz1WroUzkn{T>!!(NU%7XFLh&3Z0k`~8X(
z|LzHA<t4LP1J?BN^i1&kvmj$yxJH-!=`ALFTY2SkT#iV13f!J|+R|R*rUtt<8{agI
zOVREeM?aJ}N7M^@HZ7g)@^QkN{`dK7zkS~odFra&G3`#3M5&5N{wKC=t-S3Qe9`*P
z(M8%B%QG4`n7kGcW;%NE-~>tecVgj_c#e8qK6cq^R<4@O>EBFSTz)TIK6Bg2yN5%U
z86VggV=|vhL&nuSW9{Oo+ZCmT@>|q}@(x{QRP~q<eY2vf?&jl!wE7MQ^`}-!zmBj7
zE5}_lPmJ>X;%V|yWOt_K9g$iI?RRUtwAVB*k6zl^pmZbC{QuS9>&+AYgr!H!c`Ul=
z99zowzY(SfvNy`jlKSv@(u}Ht?sA`iO&aFGdG-JI%#*zwY&ox>^h!bCv?Ding*C>m
z;ulCO*iydzLUhjVndgo*#{}io@70{ha58;XK)SsD9TDST{ffz(_Va&aR-85K(`VsR
zb+?yH>-8@T*)+F<Pfs;Sc1pFTL{yx-Wk~U#g>#pt=;^I1S+}68P~~O!`(;w@vxSyq
z_f1{0^XXc{T1zFiAfD5^HD`(+)_!BYMyB|FN4mIhob~J_;vFZ-Tsfj^r@Z8Hjjlf~
z-+oh>?RU}EYZENjE_#?d&0F<uz?t8@{97YltFCU(>OFtZ%&tN%$C}Cdz=EUda{s%p
z&VH{Gb!v}qM(Srx=hI1ZnCDnrdzizUthq(Dw!Ufqd)bP4&dK+qKkQ-3e<J#0-)}jK
zXRHQa`o$)3yGy@gIg)d5<Hl{`xxx)!ukr}}s_*<6vFQ960f+2&4+P)4Jz;6mFLcs#
z<h+pFSRNfxeZJ#w*O81Z?mKkP)cF2q_&u@ri@f;e7?zE{rv18q@Idj48s3Y&!4fOw
zts6W4Z8s=j+FsYF;^&v}j<rLg^tt7h1<%iM>c}`-B|WUE=6NXopoVv5@4w)P%Fo7k
zc3=N47yGh)dhPrB5i0x-PqN;X3lRvgl+Myv@O4qH+wI<#<c#GP&qbX&7dPeM_A3ro
zm6vb$nD|sqraj@aj!AJ@!90)OhCh^;k86bg*39|)rSZ!e)!O!@eb1e$`nT?G%aXI{
ztv_<h^Puw<lWu3ZdcK&tmi_0o7yMxk@Mh=ucPnbf7FGs^j{+PF42b#+Q~@!ToMB>q
z6CtwsLRlBMsGfe`l2K-|zctt9=E}!lk;(BZKmzQWdupyhY5`D%(%8@kkzIFMc6xz2
zBll*j=18!}=4q{*kP2dBwA7@NqMI*vP6bOqjOKpCy?H{<Gq6dUD<>S`2iHOl3*;es
zKs8L=l6w&8_!ajcu5(!ZNf4~gbgw(4uBqRrQy(2H?Jj0#YizstB5NwkBwY~&WtGL;
z3fwLVLTc8^27+RToML#6mGwFtdMql`5qK>vd;2HlPn&*k$*(-wT&`^qTIsQAcKg~>
z{kLviR-Sn@;@+v|Ut4zV|99@E-+a5zuj}i62r^vy(9^K_(yJ}}+27B)^&W8lz4^QK
z*~3q7B_{u>|8pTjg5^i>YTt%6f(zVkZ;5-j$HBoW$8_y2@9qNuACt^dlY@V6{`oG8
zkMX$a>XbPO&mWXJJiY3<_3D9I_ILSGXOmep-ZMnymfZ<7T`T<9q)42(<LJeO6Y^yh
zuSJ{8-Wv3LNmO>eWT@Du2U`#4Cr@`MWM&OyljqrVz~5h5qM}|W?2QtCbg$dn3r5jr
zLzb3J>yGDlSe^6qjzVLz>^|26-}l*YHhENis($-r%7MKR8~s^!-hZRXB5$22;TEvy
z>m3{Q2k%d}-*)>gv7PzvOv4LF+~#E;CPgGw-8}hi`ko5ozNO!tl@-FzJYJSqdduTU
z|Iy!f7E9aQ)$tc7c-XrspnmuEc`xQq`=?Uqu|Y=Vu0r$Vi@t(8uDWiu_C0O0a_N_A
zr*B;>yL{xyas%<(OAm=PCVXU8c;a)oho?MoT0=YQH7mn2X-D_0*my{yU{Sw+;Df7t
z*9zANybtd9_|NKB!rcuFk!sBTg2LR!*ZTFpMSr@qwD{ojo_FOr&(b0<a&~OpT;F#w
zAyi0vpTRzpAl@41mA$XH_uP)DxzB6E!BZtKZ)RkdGc#giF6X`p3lE5GJjT;~^;C8H
z$Fq@ZyRMqeKCUDAF}vfPmXh77?~m^8a;j6XukG8N$Sh~%m^x)+#v@(bhrGwGas8F@
zs9{g;U3;|rPC#R>I$J+?AD44tppZmu_2>GnR@$$x+@71aGik+^U#C{h6@C{!@r0z1
zn#|J*EoqtOv$W6V<jb5{V<TZP>w;<Dr+*I)g%s?2wY<<(*;}%cC7olTT&UiPhpA5N
zPi=iKw|v@ceJv}?V)ccc;ZF?;cU1U0s$MyGKZ^hECz&Pk>r~X9+b$026LJlEBsF(|
z<0IMBiu$X|v-R{td;DH1C~Nz7MEPY;F@Ca1>dZca*OTo+C;gld8Nhq;p!dbkq5A&r
zoj$4iPw{_ttW**`6`QfDOif_!i<&7erVn34nteK9JS|w`YiPjy$yGJ0PWh)VQ5Ac>
zw@;|&v&Nitm$!&<>+UhoKeX%N7xitXt_xeb0$V>zOzG0B-?GZ(==qC_{0sY6Y>HAz
ziWA>AL$3Ivf7p%<Q9Ir)k@{48S#qC=Ufa%xo=Pn39rNt&Yj7H`67b?Z^-+0l$M-D8
zhZjQ(!u4ZbEU|J(3G6tP(rjVIH1T=o-k(*I#9H<&dt$I&u=m38<FEPUrhXIi6S*pK
zV#l&q&8>=)&R;pZCcC`8Dq>=6{UejsiX9hDJXuv<ym03J<g@C|-la$NgRe|~zIguI
zD!1eQ^4&)tGfs^D_F_f;<WG9blQMQ6jy``)sc%Eyx|SyYtItwYPfhln_J2or$oF*X
zz>B{QU)k3^`OvIqD%vydTW9Xs_nhCXo#{3E%w5Zl@v5I(ot(7G=BrBhU2WI;Ln+pc
z-?i9FCVjXhxb*U$ihc9W>rFp-uH{(nZWAM`aMRMIYu*RgO%1)YYE!|&AKXfu+WnQG
zwKu;!Kc{{3=+(m9sD<hEYhKU#QW9Xdy1g@C9jnsr*T1J+KcaZ}#Ur(nqU+utw&s*c
z-|ef+ORBy;>+H1D4fFbV9bejU{8lWPzlEjV-{ELn00Wc1;}J<S_CIfa-&lTe+mETv
zr#G(4j(%gDVS4S##Zwi0)vA4Qf6SYvEm+$5KH)|5oCNCwfm_6HzG!C%GI$|m_2`0?
zV3qa68s^38bASDRs48*X@Pg|>i5jMa^C29M>#n%D7pNVcJMXt!f3cut@}c=Z_a6*N
zTK{AH>Uyn%EpOlO`otY7ITZKrl~B_EhBJAe#Q#|TwfcG5|AZ-n<c~L6zZkeuoLsj|
z_CBJ-Xg4|Uh&<!&$$dxc8967PJE9Qaetcj1-Tn7DoVOhIxbakO2bXe!J;NpM=8pe2
zdTf~(pC5VlAi$2{e2naucjf%`zn_2ju^&{QU1JizQqIP}V8)GJo!K2-3a&XOZ;Y1O
zbaFMg+S$DB^dg90<pj;?brwwQo14#DL8_et_jJHgo8LdQ05iaqoxCvnX5XjYCZHN;
zvfWX??Jp%6^}(H_=^M-#Wu|jkG4XGAlV{}O0IPWaP-c6+I-?PU7aixk{kcBlF>p6+
z`vx;chz;BCTQZh`-7|UJX-GF|fi)B7_I4Y_EfAXnlw`I?IWTVG1RMGw)MC547vn34
zmim1%+XH+VuR>IUoKzOb=n3X+KNP|^4a@>}$o#F@x7S55vOq)*+>@Q|Yt6(t{emqM
z+xCsojM`vFZoi+*_!n&Q_WNm!CJ?nC8~w5vf3Sn?k6$6XJ*|jQ5UdK~?R^$ZoYMpB
znb@{3En&O}(FE!P)-7S*KBt25GeqhAG)9^2>#7-@APPW%!(Y$%1;UG8A+uenneif6
zDX6D9eO)yp+jfaIMhO;BGi17P7o%!@X^3~Qw7bB&c{eX^a`Nb@@Qh#z6Wb^!;cAoQ
z(6(x7QpW}+wiJ#fG3!Ki(hNN!qL#|+{$%lt{mG;`MW<VxCmAi&YTpwx)wwQ2Yp>8U
znKxIaElaQ3_51fP!(YGW$Jeno=;$a^m}i~+wQg&Md?d$Q>&eI5D)(&6mYd1(=g3Os
z2lYlxyP{WHT?=Mkxcy6x(dAv|-}s2#x+TM8eM9xMl9T(<vc9vEf9&Rvd+mAICQIRq
zs#p6n^|WUv*4Uj|6UMhTR(<*%#{jOawoJTJ-mKbs$!1-|*G-XynLpwWE7)oM=v06C
z?rILxn$;KHGV^t@2{lQvD0pm~!#sPzF7N-PXSe40)GNu=Om1GiX5!mrk=tV*aF@*U
z5UX9_*e?BR7XOuRdR+z=`eO3KWPjf{^(5PW?cU#^w*wPr6uet6a+>4erT-F7YZf^B
zGz;$VOSLkPX3zVT_rp=YwZ46dU+&?Rx39W~JahSEx-VCkRp3G4$|W5?XXgea_E=?@
z&H0o%qvBDP?LDdbG8v<|9h`aR^KQFLJ*G4zqAq&*<k?d)k}P+=Z04NtDTsMl=l8bk
zt%<@9F06jD_OG&5;j^p0S4(D<c5CTr&9@3;{&=VPmdddSoX1+zjGoPm`{-Bxt$K&n
zR@2W1T~cocPpguvEKU_TYt54?mTdL?$4;GBYR_#FY~&+4pL|=pC#HV&p7onDf=<7h
zb8^MDxwU)d+Un_ixg&9ZW`<X+k+XTpHDSJ47Pm{@-dyzHWn^YT<+5#3#`6l!B+u(l
zx)bnC?%YxPS5oIZ6W6X4wqI{CZP&Tu%dfDeYZ_bJpOQFRu+UI{liQ<PXBPg|F-t5v
zF=L&mq*%pyomG)>4-_Y@5UG$^s!`vwXw&}PFQZqvS^tckd$eTfb?rr^cT+Y_ZWm5w
zmUnAOcTSEy7AsPAX1j>Mnf<0(y{@gAHS4Y%tl&sp9yR5sfN)jHYpb@UGp<#AwvZ5r
zbv<pbVj|7!t9HFb^H2n@_uAswlA9zFgTCM8s*$nQ{C2$ghN=zkm95sRSKQ>Dc=RfJ
z{pGD!OLcE6-uNTFxk$In|HJt-Q{mswzIFc%X0E*QSxF}E_R=Lk8=aW<-JAEucX#6D
zYQt4mXC+&et@S$Zzis#ZS5?0!t}K{+%+8^?$$+1W<!-z8e_O}$X`V*kD<_)VVRsLj
zFjw3v^XtWxKHGYpc>L1uSoXi+fcb^_|74l;7pQ-&XR6x&Pb}nVb-<5I?I7{Ba-Ueb
zB$sX7|CYOUOY^ln2B(tuNqlh%Hv1e-1n%khWci=(SkUdI_WJ${r*JQ^`~QlkElBt6
z^mKuroR6YkPA`$M^4<TZ*Xd`XP?`qMHjgjCQVy9F9#t=2t4b<$8dP!0sJ;vmU0J-N
zu<GTlXYZfQZ^(Pny3&s)cCA~(%PZ$6{C(K9v;P`r(gm~lof?JZSwDEHg3ZsL$owI5
z@ApTqi7u->lv8}SO?Q2jSDBpsd|Sumc3pqA?H)zuTko(Qm;80sEa6=|sL}{xTE^(f
z!oU#7#(>%fnhYxV{`E38Fo6c?wl_{-{Lc+$HP2zZ0Uod09ygCs0nD1-IG^z^^M?qL
z?Trf<ojX8dfzyv`Fj;^ZOqxu~KpLm7)?{)3Gu~-3If5BRT2Mxr7LyZLWVaTRJ(%$q
zCgrHjR0=A3r|;Be3IsEFb(q$G8GCe?e83EDT_z_mBS4oa2+UZj%j5`VywrtiPt;>d
z0gIf_gDU3LXL19Jgy};?X6rLWf<?aTGX;PdUItKI8x5E|!6JVRn3jSWOAVP^z>GJB
zOkNzXBSdUL9m?r;MohL~;W{HGKXBoF-Uw=sgfWvlSSrbw$r;R8VGNb}Xbd&p)`ZC$
zEY)oSb;3Ops4fjtCNHp5sVUUoM@*sSaG5bVgY611V{!$nnPJ8h!U=K|xK%Lys~MA>
zB8WR%##q>lnStRB8v}z212Ql;$}oMR6_d&I1C~r&)1R6%34`?;HZ9^Soj%coNtEfv
ziOCx~6~IzpJARupNi!`tJ$dhGh3OU+Og!=+3v3SEuTtP=VBoP~V30>PpTTu{vIUbK
zSW(xLjET>f7#NnYGB8M^DB3iAg9Vco*!a5^OwvpbA5Q-FP=30kB@>SV$oRf1MlISV
z3=F%<7#Ji_bjm!Pd>~q6dZZ<j5LkPjC6hE$ujF(?M<&hb34x4a(@$A434^5`STad7
z@=pI_$)pJml+3ufvTPg-4F7o<7-Uflbya7a&TqmbF+I+TNeJu!<*FASm$ET1WbiRC
zSfZ$%rVqD^XZlGKs55R^F-bEoGGm;6z>HB^JHVTfNrVA1a1Qd$XXfRd`b-QA+AItV
zGAO29oNi~$qz!g%jy01svzHCy<o^%FrZ2E&5(PVY`)%2%9!>^^{Q?XO;wV}T92lqj
zIWS60e`n3a12*BWHIp<GqZh<|&Nk3sh_qpnW>)hBJ56MIw++<A3v8IAnWO?CiW34E
zWv9Q;heqy;Q|{Bkm>C$}vM?}+qS(1*x}GhQ3OI5r^$XJ<GchpCW@TWIL{a2Bz0j6P
z1MH$XwoKAY<<Zmat(n9@%`hRb)}Yp<_PdxE7`#}~WB1~8Mmr{TuvTq5CTZr2X^fKt
z7RXFbwS#)5+Kx$@i6aZ*YQHQ-_USXtp{`C^G}ZbwBLhPe6S}F^(?7#Zm9=M*X3i;L
zoP6P)D5yCHanPDcS2Hd#F)*}a_$7OKqdn9wYwVe%8C#~GuxBy^JMa(4sHb&|)6W|)
zNlZ6#V1k%+`=rIPRZI*FcbU<h@nd?j1JrZ94ouRFFQ%__U{aHR6Cq-YTt17S1g7fr
zcMeR-;56xcGe|t1iGjhKg@Hj2MbU;nP=MHgi_`)~CTZsEiHy@HPGA(~M^1^)BSfZe
zaAcBZ%AGs?tRs^aSotrIa*z3p)AQyrN?|B>bYhZb%3d%%&WTA5RPs-+cLJHdka7CN
d1&ktM0p6@^AcurAgfsk<WMEjY$;80G007=C{Fnd$
delta 6499
zcmdnj&Uw6*lQ+PdnMH(wgMouVxkGp&uN5<h@;b{b)ge6nU<jkgW<AEoOd#H75f&Xr
z5M#14>r*ftpd_-{p3RmM%&F&p2%<M93ruBXmh2GT{9BNfky)Wbcr&wbD+`#>E#ANm
zVoY{eATvGAl!<?{rMw6;NMv(>(qRZgOzjR6Smdk5d^Rv+y1o@yYI1a(#pLt)Jewtq
z&$5DKCI=|VOs-F1oBm#(iEXohr2<&v<O^jooBgf#K=go=<eg{RY+%1u45VlCgV1we
z&6_tyF9)mN936KG%$U6Pw9ItAdPbhj0f_<--SI1AHrJ=*fL%YiexJ-_d0~#}=Zu)x
zHcMpQ0efz8<pi1O|16ofHp^zefEW{?Br`qAn2BeyL7q=N-{$IX_ln=W|8wsByy~B?
z-`}reZ;)8Q(y}H_H-B|;6eIh(vlHJ08m<>-)4uKHsOTUsk;;_P$gq9wbe^v>9S_X@
zSEQ2lbMb8DlegZeu!Zz|T2<BX@axOkr=3E&8cX+PT+_&2YFl#q^Q^!Sz9wgm=}HN~
z{HwhdIvo(-C9-$U{qXwjy(d4YF{-V6ub^BWrM+@ymf`wo*Qe|`8MtT4Ubkt?=GPi8
zmzVP1oMI_3*Ma%4v#rU82aRkk#&X#+)+*MfeqHi3r04%9yW}LlR}%ArPtBV7uZMa2
za;fg9%=QKmuJ~4y*vWng2h-BNE1w8GYLTHH&~EWxPw|5MFOL1Mg;^E^*EjIJP`Xei
z+q?3FiP*vPt$QaWg`7Tdw|imux8s~P9BMZw2uCgSJ+PjmEw0IDYESXj-<)5rEZhFo
zi81xkm!K^Xrarmn7=%ODZb*K2L?Q3%l(0)ZnK{b>ES|S0c5n)`CQjK~6!K=%VU0Eo
zcJ@`82d*67rTF*%q(s5_2YiLA=P>-PchL+9)lNUfSvW%^fngcPmMa@hU7fU0^lFAv
z{j#vI)k{rf3L0eQR{p&?tMBNlYOQTW$r`1RYd2S(`J#D(>5K!D^z94TCUXq9_on^2
z%`!_bzwN25c>cYV=EQP_%EAP5*Lal&D_!+9k9~W5`{|~>OS-Ye7COAsSx+2@^(omp
zZ*G0*l-bRpA{DliqYlgY#tXNUt~qGMA9-SCOx4-k|2+=H84r`)ZRR*1x!|Pxzm}2z
zI`bO4Y`4T}!5xM3-0qrw*Q|QC(p0WYakjnD6|RL5(vlL2bALEq)L9=OVm~c2QzlE=
z?nXz4;UtA^w$qF20yYKmh4IMf1TNX$C(!lqW!r{&wMi`A=ADleBjxYkk9zyQbn}$e
zwLRfNo`+06sLY>`oBes)++~Z(e{{QsU+}xgl$d!<QH`Z*a<ihb-5uR^Dw17Om-Q|$
zHM#9mG3`5RM&~zgf8*TAyW3a$q&F1r%&-#;u;|LW5aqsg+s9W)b{YOEcUqP+drdId
zzUkwaKbwvpJX0^w=y$5r<x3~0n%ka5`G>YldNDcUl4jZEpdFgO48rb2i-t$A`)~K+
zW^~<fIq%=<<?Gm$f37{Z!Q!}f%3R(P?|yI0YPg<cYhwD~xvJsU2V(DMEJz8=TXyH)
zze-!{Wy_0f9==-faFI^u=F+uHyF=s^&OFF?pSN)PjWXl8z3e-e+^Me$R$`oV-elo9
zyLme_)0V}3P)n_sf5h%&V*2#C`jo%hJawh#KU$GuEhrn~wZux}dyv7FJ$6Map8asP
z_C6UC6Z100QS`CLCGq>drhR6r9@k~GJ&R9AC;uvP;aMUvtvuLBzb*VmeuU+-eS+up
z)b^B_dFl&HeA^|k?U%-7(XMUvefE5t-Fdz}&04Ei9OZiWvd(m`T?=PCm)6hPc+ESE
z|Ekpd=G;9WY;KgXlr=bZhui$?zB>E6PShzI-;C7HTF$4F<}lCsvF`9isbfJI*1!I-
z)Ze%MVAFnV-}VQUtoKf6f2jR#TX2Ru;f1`eiuk_V9YO+|S?~95-I_6*Va@uq2^Z@9
z&zu&jO>1L_DrW7kFjrC+sOe-b;`C~e<KA<7(XDE?H{mL7i)|03CO*sl#eSndXUYE^
z5>J&nu5Q2bpO0;x^YiSEyg7$F{@&p9`Le&YQFzB!Zk56Ureb}EBP*=WFJ!eX_e*#v
zaY>N-`R!zm{S42uPvm@=f9TZg`48{y-S_>4SN;As)&GwvRdV?2z4*4Eso~Vk59$lP
zF3NSg-P@9!vHaq>s8i?Sraat!#o?;*@(mvopUTznAAA;>@hs=D&BSlXA6(h`0@r;D
zzVYiN^UFx@Uwq!O=UczXWtZ|^y;C7oe<aHDpz{`!?)5fyd~@nr&Oa9o_{SLF&CcQV
z)4_ZTD+9wv0S*QRL<I+`j2KJKfQ#wP7s|T8jOq6*8D%E>TXSu0u6zs@nH;|YB*4D8
zr{)?nsL}vcDbr7yFbQm)*iZ*ivi7v>X8q<AFlY0$R!&G2u`ya|^8XW})AyS)v2VW7
z*$0*eTL7vfxHnJec?LFcbLE61{2-GzJ1mfgXa!X@bxZC+q~llI18d#vu=<lASe@x!
zcSwCxzfY(BZm{%qQTy`p_v^ysHMA$>EM$mOl&odg<iMhocqz8AbAy1`qr(X~=ebn&
ztefDlCTO;w^-twbm+Zdk>Q@$6ADns8d6F6b+>`QGU+&bNnWR&0Bz3pA{QdiX=YGzu
zes?qe|L4Q~3=`VYS>{X)TV5NnJKrpe#qQSpz4tTa^se(sU#@@N?siz=!2GCOrj%X=
z(_72Fay@5dx|Fy&^J-iaOIw%tW=-kYx8|QMzyD02AZD}IG0q~sIQEdZxgpWKG35__
zExTyr*6@jM!PT_evZ0r)4E>bL4I3h4WVwD`6HMCcx;aw2)Nj?+Z_@%(75U?C|1m4$
z6fqAFNd0h7f&0&wEsc%!$CHlgecEs};|ibd=BqxTS?N1}d}Y{jD(oDukj0H>(JVFZ
zPfu3pSfalFx}QJioo><JE)#yAo#*snqi|ayi)z&Qv&BsR_SNjj+0tKVd11aJv+lNn
zM0Wm8)n(J?=G33;Hh&yZWpBb%bkrtKDr|YL%fE;{=Ph>~ynOZ(3#0fv4et7_)vr4L
zWxn(mYG*m^c!}4@Lh`OiV{~lD?#o-wOpfx(-@8UO*WA~qj;nZMtX7U7hnPKs(>aqf
zCkn*VI4dF&)(Ria2|Lp*rQO4*{_BSbYuwrd+2dRv?OG+?uV2i6jhA~us!@Ts;YNex
zzdw@ptLn#EiPxNaQFlBoZ<^@bh6wBW*Al#8sv941KlWC>dcb<htrhzYY(9JR``rW0
z2Nrz)n56vp@U%|R+tVI!OLDzYy*49pV^n3n@jc7cp&M_deV(DJT*rH{w!5SM)!vHj
z>n6yb@Sp!S??ywrPk>~q&a4VA?~104Tb=f^3Ee*!k(~We);uKPcIUyz-0rOlH)wG7
z?6a-^88vrm>8rP1+hYtvqH0sGp5y$!+T#fir*L19%~amL;<HoJwwd##g~{>A_`Z;G
zudFXf)Ut^GdU?m9iA#H2nv7cl`nANbd@x$r{Au2@OsAhWWwT99=Y+nvv$|-8Ma-V%
z3xr-h$Y0x@SIKvYKU`??=Xrrz?wv~7g}r_k6h8JD)$e(A*>w7JEw|+*6DCeochOyL
zdP=e=k~b}W##hhzS|@8x=&Wda@?hzUpR1-XU+l7MQ~cBRp9^dzay`{E3AGmP@GG(N
zS~RQRi;i^V6Uoz>Q+{c!IPYm|7y5L$@g<?|&vEXY$0|kqu4hJdw~EEh5Kp{Y@Jsmi
ztVID%M^_xG<ncOMFA^2H=+X0xi_3SoheYZM8LsD!_vzpHLtQ&2LibKt5bw{OFL~mn
z#1G&3pd#4h?BYK^e@csFD92K^r#~k89jV^h@F7EM#%giBk|0@yO&Tt#n;d1N8&7;b
za<9hLliMjSxM;@p4!0MNAAe=<_p0Vr@5<szi3$FC@Q}dC^jB%uw$@wQt~s&JzHpY4
zO-x2g(be5MFPyo*@!8~sOLsk*uKDWp=ZojdY!^RX-hcGb$A%NS)g@Q9dsa>lHr#Ue
z;o9_ULH7vvaHoUIvx+wfJw2&*y8e#qs^6REuE_YCn05cCXQFTMB+)bP=bFgf|I9wy
zx$$eWPi*kxw#iSf8XCsVtD3a>-PC%e#7%P#6i;Qg@~n8-aVfLTCjNZ-^wTNnPLH?6
zN=eRLJ!@CcwQ`O5r?fIdBX<P+VV&4A_4uAu`*MC2KcD*M(W@P1YcFiJzgFs7Wu-Cy
z>R}g+>r4~xeyu%~{b)jBNujXS&ey6H(Pq1Q^N!n?Z`_-GHtn=gg#Yoj1tt0|wSv3C
zqw1T~7bNLxFf=Y#c*HZCx$ax-o68x|e@-oY8gYHA?l;LTQrWLEQt!0y6>`_N>s_Fl
zk@?74;+L5E4ZZ@Ax6^aJI5TKUlyJ%xX3XW-JJ(}h<HhS{fB%0F>Uk{jVo?H*9pi>{
zt(HRDti{R}lOOt>uU&k6XU81Fhv)y?Pte*J{^$Bt?O=mM>uTo7(+%csh_5f@+*t3B
zX8x1g&TqfpzfZzNybf%3ySwZfm}UkD)=&02qQq!5IroS><Lb%1N9-B-CZ9c`5D<NQ
zU;Ewt_c@%m9QL^JRBi{CazZ@ACGX}A|D0objSa;~#RVGj4e9Ins-Ev||NpnR;!ixN
zUK9Evv$2AWfx(QM0j*lIJ-QTJbxhtEEw%aoiPezmW9{ih5YfsBnwzW7JA&&RP;IvP
z_B}`!XY;#<77!(%N>5&xeR_Zu6WivXr>-WTdS|ljQNQgkBpLO=eWu9{tEIM^$TLcF
zfaTsjl-ZuA&S(VTMaMaBf2PlP4BTl0shsZX%gD9;vKb=>*n;i%EE&td&H{I|Kz*j|
zwKj}<!IGe^-1bNZ#!Z}HlOKdyY<Kfwd<9WnzfWenzc1reh)R%)N&^`^!MyDULl~!l
zS>W!Ozcu^z+6YD#h{%O9ne7Xr8Lc7ii(etL{Z}&ML$I0CCss4cO!u*865lSE&d3N+
z53<!ai}44fj~c&1cKT0yCZ6quMU1RqO(0KAzIl&(`@9my>kuuVK4IMw_UXM2Ozhhi
zRWQB*E8IS@nlTQd02D@i^^9L2y!aI|(=!~Ic(>~{Gadme1$$hujZqHV3Yc!x#i&}J
z8yuJ~<t{Mq=HACO>}@g$(i=9`isv+Y_8izK(thlcWAbS}wXKd@+<F%^&$(RuaKpnD
zQQxOO5&yE3f9;iJLGr7<E#?0i82X$~YG;{TSy}nF-)Z}9-mLw9{(U`zgWxuSDaR6Q
z-bDQ_JMYA?ZF{d<arPC{YPF^-vKH&UuI(0BA6uU<UX#CYZ|vNP(;SSivvR(<aTMRY
z)%vqH^2N+^vk!HjYrR@}dZ$@afb5=S8z#<r8}YSpe=_gvwBz0)`vm)qycF6SniZOv
z99v%8%@H~?Num17o2~~O-#2gl@2+wG-t$|E9S3Y#4=tD^@LhX$$-UjZpZtAR8B}d&
zIB%(tb6V!sy!uxwzetu}C}`jIxow^5?A?yDD>}tY-19y&YZSY`a`#a5IJjteX=mP7
z;oBSU+P1iSdy)KoUUuO16aQ}>P&*#b6uL^OdP;U{f@BG+$&UU5`gawX<R;#0JDz_-
zC3UA+r|Fh+)gg%w_X{5{Iquv&rF-uCnCzAt{0~kGy*lA?%=KnUz0QW<@Uo`QjCw0S
zb^hFR#gf}3bZt{jjQ_%)Jqx2;Vjnjeg!7wDE|xRg7r#P(>iM-@RhNE-B)yyybHyU~
z@~6m;uQw;{-z9$gM%MIWtCkr#8=HuEyZPRct*+Rn|LM=Vtc1@WAGGGh6s}2VU7vVN
zAZ~xvq@PJ;OV@N=JE{3H_{hHcRhc!fCvJHzClcg;JnK@LN=%KGSnr!hkGX$G>CZG?
zweDm)&uW`(-9Zz>E1S|pR@pSKiimZ7xaT&Pti?-(`gMk}!jHOU$YrTr){mbmrz4}^
z+1Pd_t@pXct*RFaN}E1B&tA1r-=NWc<=GcHjYj+X6!qit<{T6LsxN=Gu=&v$y?VDJ
zvZir{L4xy+e09qD{ih<<){?_Gvx~dyxU-ALygu3M@1k|9Q!XnT%cMV;wa&KS#o1Mp
z=l$F}YmX17T)^bLZpt=G1i$X%`<w2UEy$FjddoEPd`8^a|GY2%#4p&>`txkO!j_r;
zg{PDY)N)Vyz|8T-{gA;7#n*<7JGfJxtH*TIJIWl0KRdBMPDDk)^6Ub^W63A#Zj?{>
z*J)OvJjJO@GHlt0!z<4`cy>6RbN?sll)8OWqrVid7n+bDU&Nlsd+qP%1@cY5r&jr}
zNypt)nz^UGXTs8n(g&aI2Nj@?Lqi?}GBYqdVL>ZEZ5iNT^6OCD?O*#C8<;@DSlcTm
zGXCcVv#RDY-T)76Z4aH#r~qb7uUNqNm)W^ZczeY{M&}OD*xB@bnoJg8#!pSAWuPIk
z>5H_O9KejHT1<{$hNd=@k*m$*1Qyw(&14T|d;v*Gb_h?m&|xYCm4?$d=r9F>87#U?
zYru@nx=cP`29q9>6PV$y#}ou+%+X_V1T!A!LA6KdGo^q<_Ul6xvluYBfkk``pdynD
zm?FU<?+lm%zzj!2sIC=;OrBtoFNRD@!HhXZOfF!?V<RRn4uuY3TTp*%x~VafEm*kJ
zn8^>!IA#pBhu?(BofE7uHZX15^n+$hqSH%Em^8qu=9@rOy)c2=WMazX4VG#$g}Uad
zDU&-`MBa?a3(Uwdg9gEFGbU%S2%|Za;cm|43Kr=%X9@vZ3$8b(zcFXB1B>fgFiA5R
z9-XeJ%OpBI-U90E`5@7oCnj&~RG5Cpf=O5&<ls$DdEQ1cGce3#VPKGhClL^1;dDMr
zCS9<3c9u-iOm62VC!SZFUSr9`0~YKC32weO`P@C(=@#ZpJYeGrukPFSfr)|P04oE7
zEXWi%el-1qC6f+Vr@R%DG?VO8kn==9)v*v*>qO7{hJ36H4BT7{3@&hOAV%NxMk}UZ
zMUZp(#q+OxU}s=h!OOrP1(JhfK6%FJTJnt2(*>-d4wScMl4f+9Zfy;<Hp`kxnrXWJ
zbU|At&FLGgndHEZxd>9Vc=}swCQUG3(uPTz>5}F24R%c8(|v8A!Q}sc&-Yo(3=HP1
z=)vSYz1{{IOzUl!q!|sTpSEFA1N+F)x|HE069WSSD+7Zb+@T-_({uq_XsiU-GD$P4
zPtUPs(og{TkbUBXRt;tbhC(*<V2}=kJDq2Gy#*83^v||T!eB>p+A&EpZw+Cbeldhm
zY`U!-Gz5I?n4}r~rf1kOX@DK{=AGMXK@J9n_q+@Y(ja%hamDoYc1&7ev+jV*x|GZ~
z{arGn<a93+Xv|iNH?=%xVqn<H%D|um*9T%;nr>&$WC(Wr*YAJZud_2STo*w1F=rOU
z@xED%?9=z#Lmha|o=KX~X8J38CUvj_-(ND>yq%eWVG1jH^yW@CaDc{8j02N2W6tyn
z2WW_0xLMyN$jrb{h2gT+>gfv|nS`fbc3_ePo6j>b^v(%p28P8L$@AHCen)6Jv2$dS
zX8bul$`R_Q_y-5selRmIXtOaeh=V)~$1kTZaD>J+a=|MCR{&zDO@Hdhqzn#PZYL&b
zrk%ZzkT__?B&;CWA#A%WO=;61ZUzQraRvq<kPbL5nJ~S@iAg~bq{?aYtveGL85r`J
z7#L*WDnN{~IgHc0<}%7oZ!l-#0TtxaKZ5KDoHw1%nMqv>q?tcS_}C!^28Q<x3=9Gw
zJ#btypOK-;SU(^?Gp}U&1ScjD1?M(l+q^Q{d(0gS3<3KX8HC|#L5z|G(<eJKsj}_R
H03~byhdvJG
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index b60cab38f..c6caa595e 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -422,7 +422,29 @@ trait CodeExtraction extends Extractors {
throw ImpureCodeEncounteredException(tree)
}
}
- }
+ }
+ case ExSetContains(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => ElementOfSet(rr, rl)
+ case _ => {
+ if(!silent) unit.error(tree.pos, ".contains on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ }
+ case ExSetSubset(t1,t2) => {
+ val rl = rec(t1)
+ val rr = rec(t2)
+ rl.getType match {
+ case s @ SetType(_) => SubsetOf(rl, rr)
+ case _ => {
+ if(!silent) unit.error(tree.pos, "Subset on non set expression.")
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ }
case ExSetMinus(t1,t2) => {
val rl = rec(t1)
val rr = rec(t2)
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 62f4b0dae..110efa675 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -409,6 +409,20 @@ trait Extractors {
case _ => None
}
}
+
+ object ExSetContains {
+ def unapply(tree: Apply) : Option[(Tree,Tree)] = tree match {
+ case Apply(Select(lhs, n), List(rhs)) if (n.toString == "contains") => Some((lhs,rhs))
+ case _ => None
+ }
+ }
+
+ object ExSetSubset {
+ def unapply(tree: Apply) : Option[(Tree,Tree)] = tree match {
+ case Apply(Select(lhs, n), List(rhs)) if (n.toString == "subsetOf") => Some((lhs,rhs))
+ case _ => None
+ }
+ }
object ExSetMinus {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index 11daf5eba..4b8207562 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -73,7 +73,6 @@ object PrettyPrinter {
case And(exprs) => ppNary(sb, exprs, "(", " \u2227 ", ")", lvl) // \land
case Or(exprs) => ppNary(sb, exprs, "(", " \u2228 ", ")", lvl) // \lor
case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ", lvl) // \neq
- case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg
case Iff(l,r) => ppBinary(sb, l, r, " <=> ", lvl)
case Implies(l,r) => ppBinary(sb, l, r, " ==> ", lvl)
case UMinus(expr) => ppUnary(sb, expr, "-(", ")", lvl)
@@ -106,6 +105,10 @@ object PrettyPrinter {
case FiniteMultiset(rs) => ppNary(sb, rs, "{|", ", ", "|}", lvl)
case EmptySet(_) => sb.append("\u2205") // Ø
case EmptyMultiset(_) => sb.append("\u2205") // Ø
+ case Not(ElementOfSet(s,e)) => ppBinary(sb, s, e, " \u2209 ", lvl) // \notin
+ case ElementOfSet(s,e) => ppBinary(sb, s, e, " \u2208 ", lvl) // \in
+ case SubsetOf(l,r) => ppBinary(sb, l, r, " \u2286 ", lvl) // \subseteq
+ case Not(SubsetOf(l,r)) => ppBinary(sb, l, r, " \u2288 ", lvl) // \notsubseteq
case SetMin(s) => pp(s, sb, lvl).append(".min")
case SetMax(s) => pp(s, sb, lvl).append(".max")
case SetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl) // \cup
@@ -181,7 +184,7 @@ object PrettyPrinter {
}
case ResultVariable() => sb.append("#res")
-
+ case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg
case _ => sb.append("Expr?")
}
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 66fa89e42..cafc43db5 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -249,11 +249,15 @@ object Trees {
/* Set expressions */
case class EmptySet(baseType: TypeTree) extends Expr with Terminal
case class FiniteSet(elements: Seq[Expr]) extends Expr
- case class ElementOfSet(element: Expr, set: Expr) extends Expr
+ case class ElementOfSet(element: Expr, set: Expr) extends Expr with FixedType {
+ val fixedType = BooleanType
+ }
case class SetCardinality(set: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
- case class SubsetOf(set1: Expr, set2: Expr) extends Expr
+ case class SubsetOf(set1: Expr, set2: Expr) extends Expr with FixedType {
+ val fixedType = BooleanType
+ }
case class SetIntersection(set1: Expr, set2: Expr) extends Expr
case class SetUnion(set1: Expr, set2: Expr) extends Expr
case class SetDifference(set1: Expr, set2: Expr) extends Expr
diff --git a/vmcai2011-testcases/CADE07.scala b/vmcai2011-testcases/CADE07.scala
new file mode 100644
index 000000000..1453c4534
--- /dev/null
+++ b/vmcai2011-testcases/CADE07.scala
@@ -0,0 +1,72 @@
+import scala.collection.immutable.Set
+
+object CADE07 {
+ def vc1(listContent: Set[Int]) : Boolean = {
+ (listContent.size == 0) == (listContent == Set.empty[Int])
+ } ensuring(_ == true)
+
+ def vc2(x: Int, listContent: Set[Int]) : Set[Int] = {
+ require(!listContent.contains(x))
+ listContent ++ Set(x)
+ } // ensuring(_.size == listContent.size + 1)
+
+ def vc2r(x: Set[Int], listContent: Set[Int]) : Set[Int] = {
+ require(x.size == 1 && !x.subsetOf(listContent))
+ listContent ++ x
+ } ensuring(_.size == listContent.size + 1)
+
+ def vc2a(listRoot: Int, list: Set[Int], x: Int, listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
+ require(
+ list.contains(listRoot)
+ && !listContent.contains(x)
+ && listContent.subsetOf(objectAlloc)
+ && objct.contains(x)
+ && objectAlloc.contains(x))
+
+ listContent ++ Set(x)
+ } // ensuring(_.size == listContent.size + 1)
+
+ def vc2ar(listRoot: Set[Int], list: Set[Int], x: Set[Int], listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
+ require(
+ listRoot.size == 1
+ && listRoot.subsetOf(list)
+ && x.size == 1
+ && !x.subsetOf(listContent)
+ && listContent.subsetOf(objectAlloc)
+ && x.subsetOf(objct)
+ && x.subsetOf(objectAlloc))
+
+ listContent ++ x
+ } ensuring(_.size == listContent.size + 1)
+
+ def vc2b(listRoot: Int, list: Set[Int], x: Int, listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
+ require(
+ list.contains(listRoot)
+ && listContent.subsetOf(objectAlloc)
+ && objct.contains(x)
+ && objectAlloc.contains(x))
+
+ listContent ++ Set(x)
+ } ensuring(_.size == listContent.size + 1)
+
+ def vc2br(listRoot: Set[Int], list: Set[Int], x: Set[Int], listContent: Set[Int], objectAlloc: Set[Int], objct: Set[Int]) : Set[Int] = {
+ require(
+ listRoot.size == 1
+ && listRoot.subsetOf(list)
+ && x.size == 1
+ && listContent.subsetOf(objectAlloc)
+ && x.subsetOf(objct)
+ && x.subsetOf(objectAlloc))
+
+ listContent ++ x
+ } ensuring(_.size == listContent.size + 1)
+
+ def vc3(x: Int, listContent: Set[Int]) : Set[Int] = {
+ listContent ++ Set(x)
+ } //ensuring(_.size <= listContent.size + 1)
+
+ def vc3r(x: Set[Int], listContent: Set[Int]) : Set[Int] = {
+ require(x.size == 1)
+ listContent ++ x
+ } ensuring(_.size <= listContent.size + 1)
+}
--
GitLab