Rosette variable definitions from an s-expression (I'm new to Rosette)

[David Wonnacott]

I'm hoping there are readers of this list who are familiar with Rosette, or could at least suggest a better place for me to ask such questions.

I'm trying to use Rosette for some symbolic code simplification, and I'd like to be able to hand it various expressions that involve sets of variables (with types) and sets of assumptions that I extract from s-expressions with other Racket code.

So, while I could do this:

  #lang rosette/safe
  (define-symbolic i j integer?)
  (verify (assert (> i j)))

or even this:

  #lang rosette/safe
  (define-symbolic i j integer?)
  (define query (> i j))
  (verify (assert query))

and have it provide a counter-example model, e.g., i=j=0, I can't do this simplified version of what I'm aiming at:

  #lang rosette/safe
  (define (verify-me query)
    (define-symbolic (symbolics query) integer?)
    (verify (assert query)))
  (verify-me '(> i j))

Possibly I could do something unpleasant with macros to resolve this, though I suspect I'd need to convert a lot of other code into macros; possibly I could create a collection of fresh symbolics, and then replace the things I want to treat as symbolic in "query" with some kind of map. But, it didn't seems to me that I was asking for a really unusual usage case, so I'm hoping there's a more "normal" way to do this, i.e., to extract all names not it (make-base-namespace) from an s-expression and then make symbolics for some/all of them as if with define-symbolic.

Perhaps this is easy, or perhaps this is just not something one could do with Rosette, or perhaps something in between?

Dave W

[Sorawee Porncharoenwase]

The recommended way is to write an interpreter to interpret your s-exp. E.g.,

#lang rosette

(define vars (make-hash))

(define (lookup v)
  (hash-ref! vars v
             (λ ()
               (define-symbolic* a-var integer?)
               a-var)))

(define (interp e)
  (match e
    [(? symbol? e) (lookup e)]
    [`(> ,a ,b) (> (interp a) (interp b))]))

(define (verify-me e)
  (verify (assert (interp e))))

(define a-sol (verify-me '(> i j)))

a-sol

(evaluate (interp 'i) a-sol)

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/6d45e35e-dbef-43f9-bf5c-318c6f25f557n%40googlegroups.com.