Confusing synthesizer behavior (choosing integers vs. forms)

[jefftrull]

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:

#lang rosette/safe

(define-symbolic A B C integer?)
(struct state (A B C) #:transparent)

; sketch
(define (mover s)
  (synthesized s #:depth 1))

; checker
; implements B = A
(define (check-mover impl s)
  (let ((result (impl s)))
    (assert (= (state-A result) (state-A s)))
    (assert (= (state-B result) (state-A s)))
    (assert (= (state-C result) (state-C 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))

(require rosette/lib/synthax)
(define-grammar (synthesized s)
  [expr
   (choose
    s
    ((uop) (expr)))]
  [uop
    ; PROBLEM AREA
   (lambda (s)
     ; perform a move from A, B, or C to A, B, or C determined by two integers
     (let* ((srcno (??))
            (dstno (??))
            (src (if (= srcno 0) (state-A s) (if (= srcno 1) (state-B s) (state-C s)))))
       ; restrict values
       (assert (and (>= dstno 0) (< dstno 3)
                    (>= srcno 0) (< srcno 3)))
       (state (if (= dstno 0) src (state-A s))
              (if (= dstno 1) src (state-B s))
              (if (= dstno 2) src (state-C s)))))
   )])

(define sol
  (synthesize
   #:forall (list A B C)
   #:guarantee (check-mover mover (state A B C))))

(if (sat? sol) (print-forms sol) (print "UNSAT"))

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 and dstno I replace the code labeled PROBLEM AREA (the lambda) with a (choose... form that lists two possible implementations, it picks the correct one, and uop does not appear in the result:

   (choose
    (lambda (s)
      (state (state-A s) (state-B s) (state-A s)))  ; C = A
    (lambda (s)
      (state (state-A s) (state-A s) (state-C s)))  ; B = A
   )

Thanks for your help. I am excited to be getting started with Rosette.

[sorawee]

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)

[jefftrull]

Quite right! Thanks for noticing that. Updated accordingly (same result)

[sorawee]

I have a working code on my laptop, but the battery ran out... I'll post it when I get back home.

[sorawee]

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"))

[jefftrull]

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?

[jefftrull]

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?