choose* ing from list of unknown length

[freemin7]

I want to build a program in SSA form and angelic execution. I want to make sure it is SSA by manually maintaining a list what variables can be selected at a particular point in time, which depends on previous choices.

However i fail to make that work even in a simple case:

#lang rosette/safe

(require rosette/lib/synthax rosette/solver/smt/boolector rosette/solver/smt/z3)
(require rosette/lib/angelic racket/list)

(current-bitwidth #f)
(define-symbolic y integer?)

(solve (begin (assert (eq? 16 y))
            (assert (eq? 12  (apply choose* (range y  ))))
            ))

(synthesize #:forall (list) #:guarantee
            (assert (eq? 12  (apply choose* (range y )))))

I tried several solver combinations with no success. Using choose results in a bad syntax error. From the documentation it is not clear whether the n in the description must not depend on a variable. I see no good justification why it is impossible in principle to do this.

[sorawee]

The issue is with (range y), as range is not lifted (i.e., it doesn't appear as a supported operation in this page). Our symbolic error tracer could be used to reveal the problem in your program.

Fundamentally, even if (range y) doesn't error, it would instead loop infinitely, because range works by recursively constructing elements, but since y is a symbolic value, this recursion will only create more symbolic values, with no termination. We explained this phenomenon in this section.

Instead, you can do something like this.

#lang rosette

(define-symbolic y x integer?)

(solve
 (begin
   (assert (eq? 16 y))
   (assert (eq? 12 x))
   (assert (<= 0 x (sub1 y)))))

[sorawee]

Let me close this now, but if you have any follow-up question, feel free to reach out.