You are doing a recursion on a symbolic value, which is a common pitfall in Rosette.
See slide 81 <https://courses.cs.washington.edu/courses/cse507/19au/doc/L01.pdf> 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/CADcuegvopDTOWr2V4xf7gWPMVMiNSJbabiE5r48aYycg6iqRoQ%40mail.gmail.com.
