• [^] # Re: Solution en Haskell

    Posté par . En réponse au message Advent of Code 2023, jour 24. Évalué à 2. Dernière modification le 24 décembre 2023 à 12:26.

    Petite erreur de ma part, ce n'est pas un système d'équations linéaires mais quadratiques.
    Mais bon, ça n'empêche pas à Z3 de le résoudre.

    Comme annoncé, j'ai écrit des petites fonctions utilitaires pour Z3.
    Ca donne ça. C'est plus lisible qu'avant (si on a un peu l'habitude de la syntaxe d'Haskell.

    script :: [Hailstone] -> Z3 (Maybe [Integer])
script hailstones = do
 px <- mkFreshRealVar "px"
 py <- mkFreshRealVar "py"
 pz <- mkFreshRealVar "pz"
 vx <- mkFreshRealVar "vy"
 vy <- mkFreshRealVar "vy"
 vz <- mkFreshRealVar "vz"
 forM_ (zip [(0::Int)..] hailstones) \(i, Hailstone (V3 pxi pyi pzi) (V3 vxi vyi vzi)) -> do
 ti <- mkFreshRealVar ("t" <> show i)
 assert =<< px +& ti *& vx ==& pxi +& ti *& vxi
 assert =<< py +& ti *& vy ==& pyi +& ti *& vyi
 assert =<< pz +& ti *& vz ==& pzi +& ti *& vzi
 getIntResults [px,py,pz]