Thank you very much for the fast and precise answer, I'll study this ! Le jeu. 26 nov. 2020 à 22:24, Sorawee Porncharoenwase <[email protected]> a écrit : > > You are doing a recursion on a symbolic value, which is a common pitfall in > Rosette. > > See slide 81 and subsequent slides for more details. Slide 87 shows a > solution to this problem. > > > On Thu, Nov 26, 2020 at 1:12 PM Bertrand Augereau > <[email protected]> wrote: >> >> Hello everybody, >> >> not sure if this is the good place to ask about this but I couldn't >> find a good location so I'm asking for help here, after all it's >> strongly connected to Racket :) >> >> I'm trying to reverse-engineer some specific piece of hardware with >> the help of Rosette, to discover if it can help or not. In the long >> run I want it to help me find magic numbers for a specific routine to >> match captures of the hardware output (can't say more about this >> though). >> >> After dumbing down (a lot) my first tries, I'm having issues with this >> code running endlessly: >> #lang rosette/safe >> >> (define (zero-a x) 0) >> (define (zero-b x) >> (if (= x 0) 0 (zero-b (- x 1)))) >> >> (define-symbolic x integer?) >> (assert (>= x 0)) >> (assert (<= x 10)) >> >> (verify (assert (= (zero-a x) (zero-b x)))) >> >> I don't have a strong theoretical understanding of what Rosette can >> and cannot do, but I thought that by restraining the range with the >> asserts, at least I'd get a brute force search of the solution space, >> which should be fast. >> Does it make sense ? Can somebody explain me where is my misunderstanding ? >> >> Thank you folks, >> Bertrand >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Racket Users" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/racket-users/CAHV%3D05otPXjbrEaHWvJF-SeDSxz2-Mjq3p%3DSHR3HvuJRAJJ3-A%40mail.gmail.com.
-- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAHV%3D05rhby63VMWfP0RV-BL%3DsYSQAv%3DdoUfj%3DChC4fYjW16dkA%40mail.gmail.com.
