Thank you very much for the fast and precise answer, I'll study this ! Le jeu. 26 nov. 2020 à 22:24, Sorawee Porncharoenwase <sorawee.pw...@gmail.com> 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 > <bertrand.auger...@gmail.com> 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 racket-users+unsubscr...@googlegroups.com. >> 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 racket-users+unsubscr...@googlegroups.com. 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.
