Open jefftrull opened 7 months ago
Just curious: the value of src
is the top-level symbolic variable A, B, or C. Should that be (state-A s), state-B, or state-C instead?
(I don't know what you want to do, so it could be that what you have is really what you want already... but in case you are modeling register assignment based on the previous state, what you currently have doesn't make sense to me)
Quite right! Thanks for noticing that. Updated accordingly (same result)
I have a working code on my laptop, but the battery ran out... I'll post it when I get back home.
It's long ago that I read define-grammar
, but if I remember correctly, the "top level" of each clause should be stuff like (choose ...)
or (??)
.
In any case, here's a repaired code that synthesizes swap
#lang rosette/safe
(require rosette/lib/synthax)
(define-symbolic A B C integer?)
(struct state (A B C) #:transparent)
; sketch
(define (mover s)
(synthesized s #:depth 3))
; checker
; implements B = A
(define (check-mover impl s)
(define result (impl s))
(assert (= (state-B result) (state-A s)))
(assert (= (state-A result) (state-B s))))
; an example that passes check-mover
(define (moveBtoA s)
(state (state-A s) (state-A s) (state-C s)))
#;
(check-mover moveBtoA (state 11 12 13))
(define (do-move s srcno dstno)
; restrict values
(assert (and (>= dstno 0) (< dstno 3)
(>= srcno 0) (< srcno 3)))
(define src
(case srcno
[(0) (state-A s)]
[(1) (state-B s)]
[(2) (state-C s)]))
; perform a move from A, B, or C to A, B, or C determined by two integers
(state (if (= dstno 0) src (state-A s))
(if (= dstno 1) src (state-B s))
(if (= dstno 2) src (state-C s))))
(define-grammar (synthesized s)
[expr
(choose
s
(do-move (expr) (??) (??)))])
(define sol
(synthesize
#:forall (list A B C)
#:guarantee (check-mover mover (state A B C))))
(if (sat? sol) (print-forms sol) (print "UNSAT"))
Thank you so much for your quick response and for providing a solution. I'm still not certain what rule I should apply in the future to avoid this mistake, though. Can you explain in more detail what was wrong with my original code? I have other working examples where the (??)
and (choose...
structures appear at various levels in the grammar without a problem, and I can't tell what rule the code in this issue violates.
Also, is there a reason for the result? It's very odd that Rosette should provide a "sat" result and then supply a form that has the name of a grammar rule in it. How can that work?
I found a small change to my original code that makes it work:
; PROBLEM AREA
(let ((srcno (??))
(dstno (??)))
; restrict values
(assert (and (>= dstno 0) (< dstno 3)
(>= srcno 0) (< srcno 3)))
(lambda (s)
; perform a move from A, B, or C to A, B, or C determined by two integers
(let ((src (if (= srcno 0) (state-A s)
(if (= srcno 1) (state-B s) (state-C s)))))
(state (if (= dstno 0) src (state-A s))
(if (= dstno 1) src (state-B s))
(if (= dstno 2) src (state-C s)))))
Here the (??)
structures are pulled outside of the lambda. I understand that these forms may produce a different symbolic value each time they are evaluated. Could that cause a problem?
I am trying to synthesize choices of integers as well as forms inside a grammar, by using both the
??
and(choose ...
forms. I haven't been able to do it successfully yet. Below is a small test case. I am trying to map a struct consisting of three integers to another one where one of the integers has been copied to another. For example, I might specify that(A B C)
should become(A B B)
for all possible A, B, and C. The results are very strange. But first, the code:The result is quite peculiar:
(define (mover s) ((uop) s))
uop
is a label inside the grammar. What is it doing as part of the synthesized function? Did I do something wrong?If instead of asking the synthesizer to choose values for
srcno
anddstno
I replace the code labeled PROBLEM AREA (the lambda) with a(choose...
form that lists two possible implementations, it picks the correct one, anduop
does not appear in the result:Thanks for your help. I am excited to be getting started with Rosette.