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)
On Mon, Jul 12, 2021 at 1:28 PM David Wonnacott <dwonn...@haverford.edu>
wrote:
> I'm hoping there are readers of this list who are familiar with Rosette
> <https://docs.racket-lang.org/rosette-guide/index.html?q=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
>
> --
> 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+unsubscr...@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
> <https://groups.google.com/d/msgid/racket-users/6d45e35e-dbef-43f9-bf5c-318c6f25f557n%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-users/CADcuegszRmCFaDS%2BpAaCXmap30_nQLYwei-LseQOQSGRGRvbDg%40mail.gmail.com.
