diff --git a/advent-of-code-2023.csproj b/advent-of-code-2023.csproj index c50afe0..6ad3f80 100644 --- a/advent-of-code-2023.csproj +++ b/advent-of-code-2023.csproj @@ -75,6 +75,8 @@ + + @@ -89,4 +91,8 @@ + + + + diff --git a/inputs/24.txt b/inputs/24.txt new file mode 100644 index 0000000..f9e9e05 --- /dev/null +++ b/inputs/24.txt @@ -0,0 +1,300 @@ +385803404726014, 386664184220541, 365612177547870 @ -192, -149, -36 +67771006464582, 193910554798739, 21517103663672 @ 280, 136, 426 +334054450538558, 356919582763697, 188448277532212 @ 84, -25, -48 +312676332944619, 337964672568504, 98227917525187 @ -35, -48, 372 +262053228716736, 348276320363511, 253216606954466 @ 37, -86, 31 +333526091894424, 327836481184227, 164687124486536 @ -65, 10, 196 +136308365945474, 334381606808383, 125587682445786 @ 158, -78, 267 +323717230671270, 328009829437175, 337115590656098 @ -108, -69, -33 +291700494449310, 337446891146933, 403527094306834 @ -89, -94, -36 +213920672175570, 65552798424640, 292480960528288 @ -8, 190, 81 +290980325848551, 318625443662390, 251065702879428 @ 73, 38, -87 +356219743903424, 372738065198325, 173629044789054 @ -91, -167, 45 +335569387143705, 220611972353945, 227370838301783 @ -123, 93, 118 +378989155122831, 373893551581799, 490516490184776 @ -183, -133, -179 +316964152354417, 377191852958393, 518250352298454 @ -97, -139, -301 +269488686042498, 302755736242613, 265930073075472 @ 40, 17, -15 +559034149216678, 519679436133677, 532650491704570 @ -390, -301, -211 +199481489198585, 29551954045775, 151234141438259 @ 111, 443, 232 +289629941437250, 268620305703325, 221264962397498 @ -7, 87, 85 +275358066553404, 274068078596243, 240507508125410 @ 37, 90, 31 +276827079064164, 101633616581386, 186011557695457 @ -26, 300, 176 +297663782856030, 402738199321925, 248211515653058 @ -71, -175, 93 +214575905428670, 285484598087669, 365634404691522 @ -9, -40, 5 +109561933588174, 237133241090922, 359706372666613 @ 92, 6, 18 +204240989840562, 334494358985081, 304086354165818 @ 30, -85, 43 +321555343478910, 357901758547385, 179203142613938 @ -24, -90, 147 +197324045077571, 308437347447096, 289742356642898 @ 135, -18, -17 +330975278295456, 345099029477697, 232960502418240 @ -53, -45, -40 +244758240275994, 148270370569025, 341619712434766 @ -11, 158, -16 +275658599167282, 139017182984065, 117542199700234 @ -25, 238, 285 +306387523207370, 360386737589534, 239496726901865 @ 56, -94, -98 +357978580614954, 356129825909997, 225719435454654 @ -146, -83, -15 +223671617009415, 329633075621279, 185533024675454 @ -29, -89, 195 +328411184086263, 388776342220522, 226872420062246 @ 139, -300, -389 +261336027047322, 256924147052505, 490381349202074 @ -23, 28, -239 +259930234799528, 371376965446663, 398040751251448 @ 129, -134, -462 +309284828898720, 323783526933825, 183744555090348 @ -23, -9, 152 +402330549565980, 498319351820615, 224808408030698 @ -203, -256, 155 +260202009982316, 216765106205019, 391896653167292 @ -55, 34, -26 +218982781599390, 67441612502790, 343883169644443 @ -20, 174, 36 +141849861082606, 232846248045093, 298748171766178 @ 54, 7, 83 +295185614280178, 182720577600545, 349236005990226 @ -27, 248, -165 +353023837337862, 362911500852077, 178701730402454 @ -18, -41, -94 +336507751402422, 441255078475877, 200229369315490 @ -71, -379, 71 +407581083289150, 362016498148165, 484015244537058 @ -267, -111, -537 +359880934389328, 226140351047332, 261590777229804 @ -150, 474, -219 +347056408084827, 283233021180721, 257388407347698 @ -23, 621, -657 +340294299033135, 285814062952309, 301398631300820 @ -89, 145, -251 +343359441017486, 357125315534487, 232880222781344 @ -100, -89, -23 +276206766363022, 349761305163973, 268152110657634 @ 45, -81, -45 +218499461041551, 258580353794663, 67849322645429 @ 17, 11, 334 +320248703670408, 295949247586567, 523439851127110 @ -101, -20, -315 +157580579887306, 153170757185349, 338622077484314 @ 80, 129, 7 +307640117451810, 410639435468045, 191294064358058 @ 89, -317, 65 +279333655319378, 268697691571573, 321070678033174 @ -10, 57, -79 +101435702073642, 337593450996443, 217618781821226 @ 162, -88, 147 +281338616293444, 205173494417713, 405155680382762 @ -81, 39, -29 +305661112743537, 420943144739793, 32241092006606 @ 97, -363, 787 +133047406299795, 332977572633730, 325570110580388 @ 73, -90, 49 +261489653779791, 355604852293248, 416249793033393 @ 73, -96, -382 +297873526074638, 237609011571077, 306287788749922 @ -61, 80, -13 +75576223796421, 167271768716129, 326600796406246 @ 127, 77, 51 +368252371944453, 343681121537330, 318054747911234 @ -177, -62, -193 +257149017625896, 403190872971397, 229440103526506 @ 34, -191, 87 +298005527228420, 281558791324245, 185293403577978 @ 45, 153, 131 +231602837664582, 101831236085297, 248521570744193 @ -28, 149, 128 +21252359315130, 21059531300255, 296125502732428 @ 184, 227, 81 +326602929473897, 340345994409110, 167594701873270 @ 9, 8, 171 +206330983367810, 272938599374485, 395597149200268 @ 6, -23, -36 +351549447904744, 318374618742317, 161108832503782 @ 27, 701, 149 +358111963088490, 352897661018525, 224279296470638 @ -129, -17, -242 +212305971866400, 216719158308705, 163041168183408 @ 70, 109, 213 +122577883308246, 176570270577385, 328470128003018 @ 130, 108, 13 +154379461786055, 156233048283330, 348097559718843 @ 53, 94, 24 +356118881302399, 188357412111249, 432270259923649 @ -145, 357, -516 +312634097133068, 451625774431512, 240165746735963 @ -46, -320, 28 +322897425919563, 280361425482827, 266947247491067 @ -103, 7, 56 +247585462288306, 310054234293952, 206044866280632 @ 168, 42, 81 +332607322558998, 305073031807001, 198798422489378 @ 10, 236, -17 +346536342417746, 386729620079641, 174268720304075 @ -48, -251, 100 +263876827856802, 427231721855813, 419953205489726 @ -55, -191, -66 +230753367061233, 325785277680899, 222305688880290 @ -35, -85, 159 +327146814427546, 297764481490689, 323003800135077 @ -16, 165, -460 +217482538469814, 202660948344989, 454198049536778 @ -22, 35, -67 +296199290528334, 245132082060181, 177066898565634 @ -92, 6, 201 +408872309569249, 350194185909070, 399144319536734 @ -225, -102, -101 +204142977649481, 217263391762093, 334611894084506 @ 29, 57, 7 +156704074837923, 232660472512901, 150915372815002 @ 127, 65, 231 +262327739537240, 314643700556177, 301997229498712 @ -19, -49, 14 +278164973199595, 438588939449196, 556014086873722 @ -9, -254, -505 +188464600595613, 357554529643547, 237970497821327 @ 113, -109, 94 +357893786525068, 385127898943489, 211678676681904 @ -145, -185, 26 +253118981308590, 88305653891225, 387537254229338 @ 20, 342, -163 +224753255269584, 428122393179597, 196648126327102 @ -5, -195, 177 +257844812203428, 474271472239727, 253608788201084 @ -63, -228, 130 +373522691552600, 249243808996561, 385902748709550 @ -199, 279, -555 +270491902410066, 294828689638902, 226582983241252 @ 40, 36, 69 +350568288964932, 325542602065395, 250512969350620 @ -113, 48, -156 +299879234623062, 149609032430601, 316083749535490 @ -56, 247, -49 +355759022426610, 399693237586045, 184148731797008 @ -134, -251, 112 +332275347951406, 155290138306308, 396310198678714 @ -132, 94, -25 +235090558147606, 118090735142509, 477784936530930 @ -22, 151, -133 +344536162610454, 333902401000940, 137203812026846 @ -60, 68, 331 +229764703931928, 286687790172347, 319014212319227 @ 34, -5, -18 +185589808729674, 323861854502775, 238965459280866 @ 112, -57, 95 +320329244342052, 380820007422950, 218743038252635 @ 34, -182, -64 +246323943658186, 319621711816065, 151311573960653 @ 168, 13, 238 +339899765593806, 351164577547109, 188639419559426 @ 12, 7, -19 +358958708239014, 356233140374949, 167650617335746 @ -101, 61, 59 +301296072448918, 336944897376310, 236672437707952 @ 20, -32, -15 +308813680617720, 323852727492110, 226410292584878 @ -30, -16, 51 +270764004306455, 548897325139115, 272911011482208 @ -13, -421, 33 +416810836165746, 406270086757761, 366948146706072 @ -230, -173, -36 +340338210994969, 323659246867766, 308886653932197 @ -117, -34, -90 +294782196886326, 314641921331837, 119889635452098 @ 97, 80, 363 +239345735629865, 213305416050295, 316553531846293 @ 35, 123, -34 +250544640362382, 299394738294149, 389706947690642 @ 24, -11, -166 +172163857890230, 220701506103165, 147168783541098 @ 282, 219, 245 +353149672821376, 473828597637297, 202528453563016 @ -127, -513, 54 +334761798631230, 238063182603797, 397425700070642 @ -134, 11, -31 +231294599142882, 266453629608965, 323083388744138 @ 42, 33, -37 +330626140721340, 219970028603525, 154730675449814 @ -129, 33, 225 +294742744027950, 251237230248770, 382666022989453 @ -68, 38, -94 +395640117641435, 271609279927070, 404013260156423 @ -199, -22, -44 +84145249222510, 202868062374993, 236124926340014 @ 236, 111, 109 +1147480396461, 328680810927084, 131081474315112 @ 205, -86, 249 +244578437707646, 181216989480941, 222406715810762 @ -18, 104, 142 +174303061990920, 200995288271765, 403466453112628 @ 25, 41, -24 +154000694867609, 147888010807127, 192734316982710 @ 137, 191, 171 +359313433797054, 444410665275881, 233762006860118 @ -136, -670, -332 +170571375161550, 252160944152645, 323932174944098 @ 34, -7, 51 +301382407091205, 218691969485375, 230168407528178 @ -43, 167, 79 +13025967189744, 119198576824901, 219020178573794 @ 195, 129, 159 +299848790911604, 299268300504307, 233302584702507 @ 78, 139, -70 +296888874680574, 316408018949579, 202311509285726 @ 100, 82, 41 +308456279989635, 307944306411035, 216077983664093 @ 21, 79, 22 +280711194242082, 352651376961857, 217109177418680 @ 110, -73, 22 +317256339757982, 192641114167013, 549053473440466 @ -103, 107, -298 +325989811826545, 171275237613355, 169425821040108 @ -19, 643, 173 +344941366910185, 255664705016710, 283718958985976 @ -139, 28, 49 +333251554537668, 365970089150282, 191866673285414 @ 50, -106, -29 +136968447517980, 400178308236315, 164869428513653 @ 82, -161, 214 +373682252861358, 401209311098893, 461257166168554 @ -176, -164, -126 +110827505798240, 287103948755763, 234916989725528 @ 126, -33, 133 +181498722876475, 265800912276387, 400841712935079 @ 51, -5, -66 +282115148812350, 293536077022345, 291225145069398 @ -8, 18, -36 +238252128186552, 188195777557738, 34996867375215 @ 22, 142, 404 +300014726902704, 178330721552265, 355195683167534 @ -101, 63, 25 +336744885426510, 350145796378565, 197103013221602 @ 111, 68, -198 +277501417377102, 470547254553125, 251637352470722 @ -8, -312, 50 +325225573544340, 231333623404767, 532183304522428 @ -119, 36, -222 +252511759947316, 317700280746416, 278149919520943 @ 50, -28, -12 +352890165412422, 336553287210569, 165267666249632 @ -76, 149, 149 +231348934600938, 254366523311037, 321747568814130 @ 34, 45, -25 +99287769103293, 128363597102876, 358183613415347 @ 107, 120, 16 +310579399159782, 357874859020073, 168900411964496 @ -40, -101, 194 +304053648301086, 309756584336021, 273944390963354 @ -102, -65, 100 +227639566933102, 256269293168281, 393834857944522 @ -28, -14, -15 +364056728028564, 328107026665253, 194844842320688 @ -165, -79, 178 +117354187118730, 124060602692789, 280020403532510 @ 81, 117, 100 +367011027830526, 250974647820149, 234309930017042 @ -171, 90, 80 +499904695450707, 478096080039786, 400757439302230 @ -323, -254, -61 +258040640626680, 312821058997749, 253745803620360 @ 46, -15, 29 +342350112377290, 337453812074005, 216597774328568 @ -42, 57, -128 +272589395905592, 362308351555047, 281416220790402 @ -13, -116, 15 +254277242373293, 486631552262484, 490219334751415 @ 59, -368, -460 +161464040078175, 177414221021094, 279559359116066 @ 151, 172, 31 +271812745641950, 327994886405985, 240547308085498 @ 180, 27, -93 +245547729072884, 250274242326647, 472465189929400 @ 77, 116, -424 +160017509685689, 386811739271505, 16060707315447 @ 63, -147, 380 +371408674786340, 368262083877290, 389270226210888 @ -202, -124, -855 +360848133478764, 335103859842419, 182536368199064 @ -146, 131, 25 +251415280525654, 265943852903625, 330163268299966 @ -12, 13, -13 +321378846481318, 269457275174747, 173946518956310 @ 24, 320, 145 +11609655378627, 86538947451740, 95867546502558 @ 415, 338, 323 +286476102094380, 372895613985005, 250761758718563 @ -10, -135, 34 +330249873564054, 376664151566117, 210874209509762 @ 142, -199, -281 +499914264357868, 460785966374769, 495870771492540 @ -411, -293, -390 +287025888751506, 315531236758649, 300662204953754 @ -17, -24, -55 +223296940143084, 310054592958761, 322315758351584 @ 107, -13, -98 +326888619499966, 284689293726849, 218896669238574 @ -48, 142, 24 +136239981548592, 400278990524767, 193497573497578 @ 82, -161, 183 +210561337637436, 225291686049970, 397870532857904 @ 22, 48, -71 +321848340476710, 305217776298849, 281081004739732 @ -64, 27, -78 +336438868463707, 348440111731678, 161679514523864 @ 57, 42, 181 +202575747710135, 258762689214605, 347513749995954 @ 11, -7, 15 +238409058372980, 313541653919600, 525712129016558 @ -22, -64, -197 +343106497521703, 370478769013508, 189320588944772 @ 105, -148, -215 +278653216285502, 139407367317109, 176975843111351 @ -52, 177, 196 +339643481027335, 337940842063855, 318841836094623 @ -129, -81, -18 +272356973044620, 286712261570935, 200719417926296 @ 46, 63, 121 +302906543748560, 302070911420845, 336766303991058 @ -81, -35, -25 +279222457335950, 312050730496005, 102341745970018 @ 158, 91, 431 +328547437601940, 333036626051585, 170617947872498 @ 93, 139, 119 +166638972882204, 250217091134834, 264006464658458 @ 202, 94, 23 +331862432860233, 336017505125100, 266490747895086 @ -83, -42, -61 +348882493761512, 399114947259306, 166868462711687 @ -118, -224, 190 +230880012567652, 152141032227571, 169979553304102 @ 93, 294, 197 +358671515142894, 359947272094261, 166634558141522 @ -122, -44, 130 +289647550517313, 414969996099002, 295461046245800 @ -57, -194, 21 +307575296006526, 303123297926029, 349977687288050 @ -38, 22, -215 +198786071327086, 292232694474279, 222993048305210 @ 44, -30, 139 +159215452463678, 221120051631181, 323115866538978 @ 32, 15, 63 +204534524932740, 62143454981063, 202682901675275 @ 46, 279, 162 +343359996629860, 364940274724195, 397134152420168 @ -114, -117, -383 +304932388434574, 180020546020549, 559488775282050 @ -106, 61, -178 +344622367429566, 271420746735293, 221794988056370 @ -46, 492, -191 +339707915865138, 433810942794301, 245552005360652 @ -122, -243, 64 +270252908062274, 293297964646059, 354986279299102 @ -30, -18, -63 +282085465044174, 152586385812549, 257148919074762 @ -68, 129, 104 +338794761942670, 475878171239173, 345229924058658 @ -54, -609, -627 +362956160157885, 356717926656095, 206778734147333 @ -161, 19, -378 +364219281383314, 383339262542702, 188489546365184 @ -168, -184, 97 +115985308065173, 419174535304638, 407917045548223 @ 77, -176, -22 +312753822248310, 291068067221525, 276958509886238 @ -94, -19, 56 +331612953739722, 341064297287381, 310812615029474 @ 13, 29, -641 +287465373724936, 319985803709435, 234870510667634 @ 45, 8, 7 +172212516198570, 289414744474577, 507608710608818 @ 21, -50, -117 +309215269980450, 281323554498441, 375557559571768 @ -74, 19, -142 +345237241565322, 439789038980931, 317319012156084 @ -146, -198, 62 +136236608164242, 204408369714737, 146875047362282 @ 163, 110, 237 +347149919610198, 355890620027765, 156303109326674 @ -53, -37, 225 +316087982604084, 292935285798693, 286260137414128 @ -35, 81, -132 +286688628133875, 213343995914435, 355792292221283 @ -43, 119, -92 +348242123716546, 372698104033365, 175629601536716 @ -6, -167, 22 +214427509021692, 231441141824881, 289710620646632 @ 178, 189, -83 +296728342720366, 500554200874617, 531845107148234 @ -12, -428, -635 +189530777124854, 336891148766333, 428264214534178 @ 15, -94, -57 +346805416215694, 304141377162341, 215670420933634 @ -66, 260, -130 +122846468064180, 240393315048620, 273299109906698 @ 182, 58, 55 +245431668678792, 158857280796983, 313221035815784 @ 30, 219, -35 +249150807637086, 236979316821965, 98713323753410 @ -30, 28, 291 +361137978353174, 281507210536999, 344843742655434 @ -160, 42, -141 +206554425526542, 225228566865989, 366127275139298 @ -7, 17, 13 +263100540524910, 327775089854501, 185350182259010 @ 111, -14, 144 +259570749464581, 240022292669580, 259176203591873 @ 33, 118, 28 +318617855203545, 473799498745136, 203304516316088 @ -59, -374, 113 +344991269514359, 384609075054521, 175814200859719 @ 17, -283, 32 +294149490465512, 336888681466399, 214461568604558 @ 15, -44, 73 +268217034231045, 246342332854445, 315317044433315 @ -9, 73, -36 +326670925035519, 332864273810972, 216177568193195 @ -15, 20, -20 +331326531537705, 397247514831405, 354957752366778 @ -119, -167, -57 +291070468901155, 303205932797500, 274215786828898 @ -7, 16, -33 +138151674503660, 98067558875400, 288521213148108 @ 126, 222, 53 +365208521217536, 512041671699004, 231661683223733 @ -166, -270, 148 +356211081141222, 372214614835685, 153452665853450 @ -37, -187, 280 +323765442571726, 345632817800261, 182778811713890 @ -42, -55, 142 +254709505868332, 317989160069186, 252775492763325 @ 162, 26, -66 +353111062175862, 372020836587373, 176974127522570 @ -5, -176, -98 +227044590569750, 213039856604975, 351877513853748 @ -12, 47, 5 +199710109883440, 93411462486105, 274387189002473 @ 90, 301, 40 +154846141458601, 308672678971386, 462714529941148 @ 47, -66, -87 +283162731133017, 278511724283134, 122344762985860 @ 37, 100, 309 +278452443212631, 269128033327091, 368778544617365 @ -23, 39, -130 +116850894919422, 230400566950229, 165050987749346 @ 302, 135, 207 +260697705868248, 331507689359744, 230934509869239 @ 58, -46, 62 +345883734794082, 404319736386014, 165508639034243 @ -96, -266, 188 +338518007127116, 197895428534989, 333026065429020 @ -82, 441, -363 +501219359367120, 412285025575991, 553543190879582 @ -374, -193, -381 +315802188788550, 335952206092989, 221378550288190 @ 46, 19, -64 +318355888692006, 379462736241893, 346108974688070 @ -62, -151, -208 +258432198353802, 116363585901746, 279158788196090 @ 48, 384, -25 +331495566132405, 329696949720270, 262637093449293 @ -71, -12, -88 +225128317377718, 98339882122589, 405612346982306 @ 9, 212, -89 +339590953497350, 387529697719375, 418409016132703 @ -60, -209, -930 +188156378042670, 144991106399203, 54479747459418 @ 76, 180, 363 +189508861409856, 220025770701113, 300342334256882 @ 39, 47, 55 +355470936519087, 377588730568583, 186025958729126 @ -123, -173, 67 +357617990656670, 278931805125261, 301898192453698 @ -154, 34, -37 +213886629816471, 247221744883994, 187412927602760 @ 117, 102, 165 +296374173800760, 169384218125771, 83441210687864 @ 111, 694, 524 +236639955898698, 151938093144053, 194945971221898 @ 67, 269, 153 +288917518632726, 492724869524685, 228500513113072 @ -8, -387, 72 +295727746197582, 360474744238229, 503124831753782 @ -68, -115, -270 +282189594610170, 282491392005509, 436551439705984 @ -74, -31, -88 +314954230601466, 420548190234857, 214580005953260 @ 64, -371, -51 +357847064816890, 337336638576149, 184267494146994 @ -109, 197, -61 +348706752056672, 275377145397879, 169020924918062 @ -73, 460, 145 +214663556424384, 302115053921987, 548387355035240 @ -15, -60, -170 +137816123354705, 68881532714919, 90822718496989 @ 141, 279, 312 +248891797596266, 313785440491389, 60802879347282 @ 89, -5, 435 +469165669056299, 304541996543790, 499226179275000 @ -271, -62, -123 +265821000515835, 161895492455969, 181634450597243 @ 11, 245, 178 +356285242983476, 347728362889153, 158843970135404 @ -81, 127, 196 +324775129764550, 347016718050565, 202162951243018 @ 159, 57, -160 +235138827258360, 84780944337545, 375637426198508 @ 19, 279, -90 +207155653686690, 268708428643649, 269113419224924 @ 216, 117, -51 +328903202326354, 314642642432431, 231385235953726 @ -42, 66, -43 +351348584362654, 328210234088285, 183423860793722 @ -46, 278, -44 +133923271127655, 15946363179440, 218432342211833 @ 77, 244, 158 +261067422616210, 294587005892105, 54887803745498 @ 71, 44, 457 +331821353676594, 422141575447479, 299518708308799 @ 40, -473, -706 +369931379292600, 277109566356635, 291555687461348 @ -207, 460, -640 +271201570580361, 319931769006502, 233949945157639 @ 37, -20, 54 +219929906219867, 351074327917355, 267765680025459 @ 77, -97, 36 +292339075455432, 199741793871233, 285373325473232 @ -71, 95, 54 +346900087043760, 288681201410123, 253127416209530 @ -114, 119, -73 +347544901928734, 345957012938925, 155174759798780 @ 68, 213, 244 +241918384900110, 396704843204545, 178323238720558 @ 76, -182, 180 +305784694247844, 291026924781121, 547325893026114 @ -77, -9, -369 \ No newline at end of file diff --git a/inputs/24a.txt b/inputs/24a.txt new file mode 100644 index 0000000..cbe1492 --- /dev/null +++ b/inputs/24a.txt @@ -0,0 +1,5 @@ +19, 13, 30 @ -2, 1, -2 +18, 19, 22 @ -1, -1, -2 +20, 25, 34 @ -2, -2, -4 +12, 31, 28 @ -1, -2, -1 +20, 19, 15 @ 1, -5, -3 \ No newline at end of file diff --git a/src/24.cs b/src/24.cs new file mode 100644 index 0000000..2b9db3e --- /dev/null +++ b/src/24.cs @@ -0,0 +1,132 @@ +using System.Numerics; +using aoc2023.Util; +using Microsoft.Z3; + +namespace aoc2023; + +internal class Day24 : Day +{ + class path + { + public readonly ivec3 startPos; + public readonly ivec3 velocity; + + public readonly BigInteger a; + public readonly BigInteger b; + public readonly BigInteger c; + + public path(ivec3 p, ivec3 v) + { + startPos = p; + velocity = v; + + a = velocity.y; + b = -velocity.x; + c = velocity.y * startPos.x - velocity.x * startPos.y; + } + + public override string ToString() => $"{startPos} @ {velocity}"; + } + + private readonly List hailstones = []; + internal override void Parse() + { + var lines = Parsing.ReadAllLines($"{GetDay()}"); + foreach (var line in lines) + { + var split = line.Split(" @ ").Select(x => x.Replace(" ", "")).ToList(); + path p = new(ivec3.Parse(split[0]), ivec3.Parse(split[1])); + hailstones.Add(p); + } + } + + internal override string Part1() + { + BigInteger lowerBound = 200000000000000; + BigInteger upperBound = 400000000000000; + long total = 0; + for (int i = 0; i < hailstones.Count; i++) + { + for (int j = 0; j < i; j++) + { + var (a1, b1, c1) = (hailstones[i].a, hailstones[i].b, hailstones[i].c); + var (a2, b2, c2) = (hailstones[j].a, hailstones[j].b, hailstones[j].c); + if (a1 * b2 == b1 * a2) + { + continue; + } + + var x = (c1 * b2 - c2 * b1) / (a1 * b2 - a2 * b1); + var y = (c2 * a1 - c1 * a2) / (a1 * b2 - a2 * b1); + if (x < lowerBound || x > upperBound || y < lowerBound || y > upperBound) + { + continue; + } + + if ((x - hailstones[i].startPos.x) * hailstones[i].velocity.x >= 0 && (y - hailstones[i].startPos.y) * hailstones[i].velocity.y >= 0 && + (x - hailstones[j].startPos.x) * hailstones[j].velocity.x >= 0 && (y - hailstones[j].startPos.y) * hailstones[j].velocity.y >= 0) + { + total++; + } + } + } + + return $"Intersections: <+white>{total}"; + } + + internal override string Part2() + { + var ctx = new Context(); + var solver = ctx.MkSolver(); + + // Coordinates of the stone + var x = ctx.MkIntConst("x"); + var y = ctx.MkIntConst("y"); + var z = ctx.MkIntConst("z"); + + // Velocity of the stone + var vx = ctx.MkIntConst("vx"); + var vy = ctx.MkIntConst("vy"); + var vz = ctx.MkIntConst("vz"); + + // For each iteration, we will add 3 new equations and one new condition to the solver. + // We want to find 9 variables (x, y, z, vx, vy, vz, t0, t1, t2) that satisfy all the equations, so a system of 9 equations is enough. + for (var i = 0; i < 3; i++) + { + var t = ctx.MkIntConst($"t{i}"); // time for the stone to reach the hail + var hail = hailstones[i]; + + var px = ctx.MkInt(hail.startPos.x); + var py = ctx.MkInt(hail.startPos.y); + var pz = ctx.MkInt(hail.startPos.z); + + var pvx = ctx.MkInt(hail.velocity.x); + var pvy = ctx.MkInt(hail.velocity.y); + var pvz = ctx.MkInt(hail.velocity.z); + + var xLeft = ctx.MkAdd(x, ctx.MkMul(t, vx)); // x + t * vx + var yLeft = ctx.MkAdd(y, ctx.MkMul(t, vy)); // y + t * vy + var zLeft = ctx.MkAdd(z, ctx.MkMul(t, vz)); // z + t * vz + + var xRight = ctx.MkAdd(px, ctx.MkMul(t, pvx)); // px + t * pvx + var yRight = ctx.MkAdd(py, ctx.MkMul(t, pvy)); // py + t * pvy + var zRight = ctx.MkAdd(pz, ctx.MkMul(t, pvz)); // pz + t * pvz + + solver.Add(t >= 0); // time should always be positive - we don't want solutions for negative time + solver.Add(ctx.MkEq(xLeft, xRight)); // x + t * vx = px + t * pvx + solver.Add(ctx.MkEq(yLeft, yRight)); // y + t * vy = py + t * pvy + solver.Add(ctx.MkEq(zLeft, zRight)); // z + t * vz = pz + t * pvz + } + + solver.Check(); + var model = solver.Model; + + var rx = model.Eval(x); + var ry = model.Eval(y); + var rz = model.Eval(z); + + long result = long.Parse(rx.ToString()) + long.Parse(ry.ToString()) + long.Parse(rz.ToString()); + + return $"Added coordinates of rock-throwing position: <+white>{result}"; + } +}