From 2b6055040b929422586918cdc5d3e94fcd3fc398 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 5 Apr 2025 14:43:30 -0700 Subject: [PATCH] update agentz3 sample based on hugging face training/test data https://huggingface.co/datasets/CardinalOperations/IndustryOR/blob/main/IndustryOR.json --- genaisrc/agentz3.genai.mts | 44 +++++++++++++++++++++++++++++++++++++ genaisrc/agentz3.genai.ts | 12 ---------- genaisrc/genaiscript.d.ts | Bin 136603 -> 157111 bytes genaisrc/tsconfig.json | 4 +++- 4 files changed, 47 insertions(+), 13 deletions(-) create mode 100644 genaisrc/agentz3.genai.mts delete mode 100644 genaisrc/agentz3.genai.ts diff --git a/genaisrc/agentz3.genai.mts b/genaisrc/agentz3.genai.mts new file mode 100644 index 000000000..62714d5b0 --- /dev/null +++ b/genaisrc/agentz3.genai.mts @@ -0,0 +1,44 @@ +script({ + tools: ["agent_z3"], +}) + +$`Solve the following problems using Z3: + +The Zhang family has 6 children: Harry, Hermione, Ron, Fred, George, and Ginny. +The cost of taking Harry is $1200, Hermione is $1650, Ron is $750, Fred is $800, +George is $800, and Ginny is $1500. Which children should the couple take to minimize +the total cost of taking the children? They can take up to four children on the upcoming trip. + +Ginny is the youngest, so the Zhang family will definitely take her. + +If the couple takes Harry, they will not take Fred because Harry does not get along with him. + +If the couple takes Harry, they will not take George because Harry does not get along with him. + +If they take George, they must also take Fred. + +If they take George, they must also take Hermione. + +Even though it will cost them a lot of money, the Zhang family has decided to take at least three children. + +The SMTLIB2 formula must not contain forall or exists. +Use the Z3 command "minimize" to instruct the solver to minimize the cost of taking the children. +use the Z3 command "(check-sat)" to check if the formula is satisfiable. +` + + +/* + + +Twenty golfers wish to play in foursomes for 5 days. Is it possible for each golfer to play no more + than once with any other golfer? + +Use SMTLIB2 to formulate the problem as a quantifier free formula over linear integer arithmetic, +also known as QF_LIA. + +For every golfer and for every day assign a slot. +The golfers are numbered from 1 to 20 and the days are numbered from 1 to 5. +Express the problem as a set of integer variables, where each variable represents a golfer's slot on a given day. +The variables should be named as follows: golfer_1_day_1, golfer_1_day_2, ..., golfer_20_day_5. + +*/ \ No newline at end of file diff --git a/genaisrc/agentz3.genai.ts b/genaisrc/agentz3.genai.ts deleted file mode 100644 index 8520d9426..000000000 --- a/genaisrc/agentz3.genai.ts +++ /dev/null @@ -1,12 +0,0 @@ -script({ - tools: ["agent_z3"], -}) - -$`Solve the following problems using Z3: - -Twenty golfers wish to play in foursomes for 5 days. Is it possible for each golfer to play no more - than once with any other golfer? - -Use SMTLIB2 to formulate the problem as a quantifier free formula over linear integer arithmetic, -also known as QF_LIA. The formula should produce an assignemnt to the twenty golfers for the 5 days of foursomes. The SMTLIB2 formula must not contain forall or exists. -` \ No newline at end of file diff --git a/genaisrc/genaiscript.d.ts b/genaisrc/genaiscript.d.ts index ae37c093763adf970a598b87ed3ae0f6e086b463..16f49c2ea2046cc4a3a22a1dfeb90a96e746e5dd 100644 GIT binary patch delta 17567 zcmc&+4R9S-b)IX>wxrmOY|FB2%kf%{qi08YvTVnR6S^uw zcAs|l=_j^%N$C%zp#)#b($Y3inwBAfBz>i(h5m#x&{BTtwvzyDDS^N+gpy={feaJq zch23rZ=a+%VTJ)_V!ge4@44rmd;ZT^-urO<<$rB>;I_IQH>GzxKJbMl3k#W|{QD&> zaz%Y!esRg71^4Wf`T9E>ZD-gW8_s&>n0&B)VtLjbcHCgtnl9!|+xg3eZ;J()V&$pE zyBDqcvMk|#K`x|7gbLA>Omp7eU zOoYjNz97GI!%=zk#s+D1tdzs4#fue%f{$X zHtKaRbgY#Rq!!E3w)L`{T0sk<-)r=g_omkApMRTbi+)!AD|Ja!KELe`#e4`??(VEC zl^@u%L;lZun!@KVh&p-8o;SVwhhlN%+j~3_Ha{+!_8cBKX84vjX?aG*b;j&m$uk4n zb<)O(amxr?H}4x$c0O;6T88bMwK9Q~#gD+1D{fs|2CEJ6V*j>Y<8b^iz>pf5K;7H6 z@n2(`L3=UV%--sNnHe_#OJkxpobt?K5&KQq!MI^MYH>OO*WCz^1}*C+R;=|Z*>|4p|Ot2?e^wf8m3iNTi2N8j+##<1v$x~5WK z`Pe*bfQPe|=gUXGvqq%lr@ymFe&d-IdGC{r@~7Wf68&yz0u=*mIsiSKQeo8cWdHa^ zd2C`yWg^?!EHAui>7ooyYsseJb>Z6k#kKMyKWeC4n%*qr_hJ)rn<@P6HC`LO<4LjkraP^G@G`7v+YfLUW75o*EW`DTQZZ{1(srOI zM^Mz5C;w!4O*v-;N4=9gDW!-BIx5he@pH7G*GO$O_VpRZJhx!`*4|Tn)hXD}#!jw> z!=~`iYnAuDCvA0|=Z+c5wF8qzFPpmxlmej)6 z#{?tIcksx;W2Wa@8lxL(-oF0up{u-oS)3{xfBRk`H~#jLP2f+u--7E|#+aSQ6$dW! z$dv1y^NVIiKJks_J%$MZ?J8K9HpA0sO&&}_9L38NR@)#!_}`Rg2i6?~ExdTU*do9C z>y6=s?~9hogKw>?YlEm;-k6!OjDc}8fGh=&HJlpsSczy$g&YRwe`(+taLGqn#kMH(qRnnR=NG4;G+1jPs1MO}~drUOv3* zU&Z>~1JDmpV5V{M_#wR`Poa|&_m7&swR@LgIT<%g`int(Rn_kQrjP<8ZVi!qb+jR(<@u%GH7u643Vh0>_H*vRnaM+J4?a1 z>vcj{aDlcDE#zCqhyprN%cQg(ccI?3&oONMj^VOp0m&S*0O5@Ij@aGK*rP?$3DTqp zCvo+PxeDOKJod)a0$W_jawL~V)*c(P$YruYWmw)|%Ca1m9RMR(RT9u{gk5;!SD?by zwTfjchz=*9f@_G^JezoA+JC{MBarhGj^4~A8zBj*!?_56vbqG#W4I5`@{4XeO9g0C zdm#jHn3fLP*>FXxXjx6Cj!sN)2M8>)P4mG)ef6}8H%y0Z&xsUisa<0wCqqtw#=(MA z)6EcYD_gs(p37RNd;%)M^m3&FE{ZjAbQD~_hDnY~r(yavB7>duCSW~M`$^@Y_#tf^ zadGt#UG(&<3+92>ZkYKgvpiD;OSaU`GAwKdU!`EqB!Q0OFr|#`5IcbWFmwGJH=-EDayqAQs7wUs_2wR8DFXy1}$DpaP2gOsC;G`59wG6MVz~-}t3s(eQzO! z6YPfI1tP8)i#gw~-Jp75*kc||71^mK&oX`2A+b?@Q`mb^+)&l(ClRT|yh(;_j#e*W zhSuucukK0@k~2gX`tw>!+G~Cur#Exe{i|V+yMGB*vJ5YibxPtQjD5_`ir;H|kHmO_ z{E5+iE$`9IBwn3>w$h{3E#)Kk-?bzfmaE>rS^usadb_(wZoRZ>?U0pMfp+91WXTnP zTk6UE?_49l{?h8@?HRXd=iMO9Gb)c<`h7vyx6{vfb}@kGI$Fx*;1cIu`okz0k-wiE z&Gj0CG~p1xtn7c+{%e}yej~i~jUg-JS-~LeLne?{-qRL7|KDO!<=qe7AmqAFE?YYL zb>(yK`|g6}%t9wT)A7lA$#>qmw({CP8(bJZenPC-S+EO{-G~sN0rG6w7wtYdQ_UF5?bxUNNGGz<6>A9$NQ`oX1@5B)`9p%|5GAO0%-eevNZ@b4!cc@qD=>%(ux zzx9u9k$XP!c`;h4fApUgE;>n$Yxu$y#4GMIOVU{cD~N|+x31T|LFClJ6R4pU&65)k zt(DF*^=Gn1HcF4Y>?**_6?m}$%$-fMRJpWf^QItRVt7GdZjzqwaqkBDG zawu6)44CGX*L-yOVmbY%P1ix%90U*K{P5Lshy*of!XpXB!-*HfI(heR)u-^X_Mp5D zqbZuFRdlBzANbxD`NroOn>nWK?e0#e(;%;c7xo+#&D|%xd<`gglx}{KgIz?5DT;+L zMT6YRj-<3c{tvTr4sD!I=z2{j;aS2v8vDwoHbrFc zz{OWUxAL*C{A@AdZKNjy7_*`j9AtbV3|V zgYy_F*N6NxB!##&Htb-oti?Vqh6~}9-C|vM@y|tDgUTy_4Z>%42tziFH}=ft3?>nf zR}4b(q84Q}KZJ)T#C3xTKGJD~iGIaNwFKAD>WIZ^IE=<|6nWpZYvlg>SIfcYT9`+^ z^xX0tl(NMEUt><1L&`?Dqm<2s*pjZIDCDMEX%8PC6`PkKuz-5tYd?J^ywW4qK<2(w z9z=vnIiu)2nemcy4zp-@fPTZBAZ!pwvFgGrrG$9Y%w}!Q!`6(BL21;=Lg3auyZP*4 zL>L$>C#d0AQ_*N*&_+(BDr-q>EXp$mUP;*`EY^=Txu^Ib`hY6&rEg@6&yiux6d#+^ zTeK4}9SRWp*BlUohY)Jj(gFy~oryu7NxF8;Nzn8NB?}(^Ioy z-q}&}tmdlIhv!d;_FZ(${%m$Wz_=s@6+aRL%RBOa{&Pe4z$vlpW?DT+H*C!Z0C%qd z;Kv*Qu@9yQO{6om>`k#fm{3$#&AZSSJwWOi#O=8%^_8i&P68)!m}!J^!;pMrN; z{MPD|(3mi$42gN2bg3FUjS$ugI-y^(X8;4|4;GK13$gljmhM7T3T{S1cG$muiHngC(jYaGa1lodJZ^?RN}KmKg-%}CZ6!IaCZ*j<=)oV+!rod!jtg5e=e8vff( zv1JW{s=zu%Cb?SezykTTXV%WD-mGSeSI^-wN;vYqE2|sq92n9XFnw8ksd*KvSRQ%Z zIMU{vbI16Si|S--w<|lIe|Bj--S$x=C*;IStK^24o|E^!R3|_5&TDrbHmB`EsgQ8T zqKparZrB{s#wKSGyEwN&1P%Kq#A>Mg=@aa~-BHTtiEyA+LaScnvQTCFPqQsyIWLy& zRi-h}DRa_$2@T0yQUd@C6GN2mC~XYW>%`*Af7mR3u#xIg&BuUXFk=)^Iimz5n-BSu zAFh{=W*3Fd&0@_ebt|9|TMafE^8H_JzVzbqYbHv_XR#0A6GfI0A;&F~9A%#gy)=3{ zMA`Q6-~zEeT-7R?!v}VYy2}sl5+7a`-g2F2T2AtzIG!jRm(lu97W1wN`GFi1EH8&d z8T%1Rn&U+g-zc899mJ_|DJ(pHyV$oqA-hA!@xzT%BFS6UtoHeJ_;^7|FZHca4x6PK?b@)n&>cTc{nvOoBRO+_W1@i_LqW zlZH)uSRoLB>EB1gM*l%XaD;XZs$?s0we7r<(yX;W+QWMWL{|QIcT?wqcw=J{{sGA8 z+xKYoq3EW@hwOXgm50`?KZ@G1hqN|~Jv)j<6?M7imJQ-acqI^R`v$1$X`rY8chAMG zfJLZyNQpvv0Wx{0yVRh~Z-%f!`NQF}1L9NizaP4G^Fgxi1O^nWS;4n-1bm@ZT>iwM z_~+|4M9z7&>gyC$!M8No-WR^j7XNrlwd#Z_c0Z!8V2JD516;{g0SlNbE^$ZW=ffxJ z7PPKl9KcO%G2p`b^8Np^Rz9}7IsEf6(buH&4H|SP&WbhH@ggOVN_`$J*uma-PU@`K zC>p~%&x#+&cWztXL!p9c>kbL+8IM|gol~e^6j77$z24{++8e{e=fw3d6GeyiIdShc zGOaiD?3l)X45bHc7t{1l;_2o+^e*hqi`@&13zx_8;#A%0)I2VDAfJCnTX@feI1#S% zgekU$=RMK2h))@Q&=c)#v|a5fs5PT22z(&>SxhG<7LMeONBgp3%Vtq z5_MEHVskv{+Ngg*v^keu4b4r&`EJyl5V^F7wv&92HU@Rdo=UV)3Lx;idPq;<fngj%)#x9JhC{4KRwX&+fR+X`q!R(8(g6am=mtS@m)ljH@oj`*>+N%0lV29BDy< zxvhlMFftNRen_chD|;dl0--Wo715y_z$T88^rskMvY`}C7~3_>Je)RE@Dk>d5Xrdt zQo)HviKwX7%~`4@%~?A-1Ks70jrkVW)ycxdgp3aYH5Dx^d$W#koEP;cWKXd-!kwO$r0rYdO#iP(pK#svufjBd|$^?R;FHQ@O5J27Y9i zvaf}W^7kI@GrGG~@rvA-EUJ32pk$|&SkoC4rdXFmT%Cpv1CN$47z$=^Q~M&<4k|Bx zqi~C`E>jDKqDbPV`^lLmD0(@x66fQ1OkICk6FZv92qialAA^e zP9Igxj8*21VrV>@Pr`B-!|O--63I}{%9Zk_2fL4~9rF8B9(L6U*doxOfHd89I+l#A zoAJ}04{^v@)7^RaHhvI2Z1z{qzz>|(q~s~&B$P*-V0>WQ&SysqGn283;B6gdsiTsi zh%SP$L=<>1FktNyjViI^6lyWYeLwN3^9Dju5K{GSYKj{@3@KjsHW=t$d)s4JJS5v0tO@kB+Wp9qBJ}olDy9x z3^96j^uSt~vIWqugybvX7*R9|BdUnoQ1m##~lhm zU2M{8=r>A%O?`7p*P!2J{`;gIYGy`P9v>rm#txA+sd0!}bH^iv5{G^2cEYkRR+pi6 zXN+-oYL4#Xre!~Hi_x1&*mKpLnNWe6t5hIOvu`JowmTNmRim!Q?gumt{Z+fh1XjI? zWz~BSc$U=#4kz(JVK~p_JR}DZxH4a-4az+k$oAWL;#sI$0}82IsZAzeOb%Y3Bt|1E z{cX5X(=W2K$1ppA(UCID3tHw#mXP2ml#uHHbR|lvplFVQs$`LUW%3AB92*{6(t|$& zIFTb_XH!TCCR}qi&NK!JkeAFPuzmDgj-_%KPWBhuK6_O(d!AulGV2u?ZJM6&BqD}L z74#?~-YahtEh`nd=8RtpQqCD{)*5uqn^lpnn)9MeP7UFri)yx?q9KjOEX-j?4|5u` zFqxQvOCeg4AK*CIi<+#Y21wq<>=O#*%hiDmd`yAE$`3g=R%ktz)mOe@*L8!EU-UDN0~jJr$;3oC2Vxsx#%)2Qt-AkTffY#GD!A{(@X?bP!yg&KV_YW zo#$dfZ-{8vd@e!2tdptoym-;8mtBX*FON{7wmwNTp!9-b1h;@h7CrhYN+lq7ptq;N zKJ2O0Zg}pBSoS*Rp+rz}ob%u+?dpNOG=U@EUI(D$L84hNW5tS$CRZ;+Uis^`GGdnT z$gZj40qi}p8_-`_+t0X2UBb?xpGyOUQ$Iq?cF>`Eg&(&!A-1ICJl?j$zj9^@Zpm*) zi=FCj*O(Aow9mlvXP_hbl~7-4aEfoGR2Z^#M3xt|tR*Zp5u#?Kq1+)%mYX_SDGf$3 zbeyR=iv(Ge&Z1md{Iil730U^3|s(5<-*Ew2mVk_ z750YU!0QmVz3-!9KDO3B5h0M znR?_GxMmQt+b#9c$GkTOPHOk9at!~@|+Cd8&KNZvybvo;#rOGtjw zoA?$ubRxdsRXqv~r~{>{B0YMM5;O_dAkmpdWNw3vLaQ1#vQbp1n=z1C<#Dc|a7k*c z%jZ;xYM`b>UfQ_bLbQS=ZPj*!Y#sXN;dal!1C4rwsZ}3{!H@ELqdTM`%a)@f4ad0N zRqkTwFk@DR0S+ zG(>li8bzQCatFvTP}r0;#!&PM;x;XYa(1MFx;dzAm{oQ3`5gP*4BhBBJz#qoQU~~U zF;Zc=CmXR7$1zZ3YEBt-Wu4!vJ?R#pt6YAR9uOYG<3p~@NOf%K*h-%dl9JWgZ$S0Y zC{I+>JH?0OqILmEAsh>zEa|iFS6RpKeFd@j$kfzS+9?*!`e}5hb>mB?b4cZPGiyZi zl}DY5ualjsP6JJ0*bqzy7whyHNEVX$+3>!iXx>R1BHKhN9H^>JNz&k`v%sg#*1(O% zgbqg0$M9qXsT{7z~Fi$BR`* zX86C~6Kl$BM^y6RS0Mo9SOVrS@-IaIC=5idi)8UvA^_!B0)90D5QYVD?U`50_lmbt zT80v)H=$2!6)nsd_^f5`ozZus+69XJsv1Vc+dEt752&x}Pc`iI#KRon+xKVC+V^iNj{=S&A zC8UK&qrh}`Sk7bzLh-1PC9f4kRKrI{C*=5mGf7`~hL2tmi!Rr{UEH^{pV3dGF9!yX zk#ciT)TVrHBK(WZwt7niZA^|z$nX9G@xDDRD9av4^C)GKk85oR&tw0<8u`)T)f0IGX`sAaB!|;Fcr8_l)=<{;oy{pRAPq4M$g6bGB zs<{nve{=!|3liU656u7R^)aX+&_vHW)B(|fC3zavJPM95Up>5AyFiRR!b%(*fh;OBtg|guYo+@Wytrx*sMO@ zt*h7D$fy5zbt{odLrEp>NbWCphF|=&Sh6L<*FqT$q`VjnZJHE|AyO#1;p5*I%~Z*+ zCNY2pOHlZUZ;OU9w`mw4KjjxlMgkX=!w4Y5hC9I_1l&g6v38e&{(3$ICY|q26OtG6 zQq^}Vvummkn&469o5Z=P?sU?z(e#a8QLrO_R}jmjCLOOzhQGAz*GdJ`=^}!vqz`Nt z&!gn4LMdS5J#6iy$O%LeAUi6SnvD8MR-2CqA19Z`*`c<$J&0 zDj(=wbi67D@rkP57L!dYC;h%g66Roa`po5y{}8vX>{6b@ufgxA#sOfP+5x>hJn>C2 zh?wj0+rBBxwc)=nT(Gf@Jb7sj-w?LdEm$ER9In6owV#SFH*TfIvnajF{W{3&p=lYu Xq(upGgIX%l)`x#DKi06|*=znEtCP7q delta 1531 zcmZ`(YfKbZ6wVoT+2^P{mX`{bExuOX5g#k^2x4PRk)+lXBidniU|09$%peehReZ!^ zqQ(=r8W(MgO+;HGy^%5L0}Wbjq^qVrnwrK`+ds95p;6O6ww-~+)U^FEbH4k1=boE$ z?mb7nZaH?we5le;QdU?zSQ9g$%N)S7=7q>v8d<01dtg4>n+f<}3S%dy-UPNM>E{G& zbNs;8r`kqXQ6c;a;aA4;A!@#eRgpll!{1L?;4jnF>LEC#FExFC- zmm{Ji$dcPDHVdr*h3zjG0Q_ZMGHWV2V#mz#UHEuuH9J_o2NbxIV0QFIR|Eio5^OeL)HsLh^uJa>crf6Zc;C4Imlx9Dms|YrQ(g( zjrh^_a{O#(7Td666j)uCmBZnk7WU2Vr~yOo&%x{aZ1nzGaL^6eoE1OV&mZot{y!mw zJ?S@TAiyTC~KDlUT^J>UU0bjV;ZC>;?I3s0tFb$=z^ z9L>b;exlh7#`=Rs)-$jdnCDET4I3JgdP}tg?+wicJiT!mE4}a=XId^cuM7$;xT9-2 zlHo0^_VeWltZR5*f+3=aUV5tt9OxXm%0(3Xb>xz6KDm5XH@mKEx9cus+jw>I@Y1zZ zBwyeDFVe)at{zWd=SL5~%vM=w5#>rZsqqO)O*j|{i28NDJx*gqY&X>7NUWX}-ry7Q z`V}5m-yLS9_Xds3^y89LJUbRecu~aY@3%k)7#lO=mrsxAn0nrUBxKKyV%4)0Sc+}W zb2-wfDJ5*|`HMu1{56f8_>)*@*J4Pg4@_XvQLZ}83`quh%mF;@SeHgCYamhOm%`H=?0&?n_VqBx+X8-Bag(|8$g&E0 zBAd&y>kp_kB8!qno;LKJ^cq`@f6 zGU!X{{uW5;8lOm%c#mogPV{cZpL)`$uL10ICJz>zdTJ_dio%+d+K{GeF^E4zWYH52 zd1ZPj7aRsLy zJSj8_O@a6X)22|UqkU2cg|`ZmSbuykvCkh2ijvb>VYT{0iYPS;9+A8i5w)ml)p6i} znj5v7d2#~IS=EQ9;hdd5`VMj|dSzur8(dg&EtAf^4Ke)U0P?xQr{#RPWSrF{^r~fqQ8C8xSoJ%K!iX diff --git a/genaisrc/tsconfig.json b/genaisrc/tsconfig.json index 69cb864bd..c2d89175a 100644 --- a/genaisrc/tsconfig.json +++ b/genaisrc/tsconfig.json @@ -11,7 +11,9 @@ "allowJs": true, "skipLibCheck": true, "noEmit": true, - "allowImportingTsExtensions": true + "allowImportingTsExtensions": true, + "verbatimModuleSyntax": true, + "resolveJsonModule": true }, "include": [ "*.mjs",