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 <[email protected]>
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 [email protected].
> 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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-users/CADcuegszRmCFaDS%2BpAaCXmap30_nQLYwei-LseQOQSGRGRvbDg%40mail.gmail.com.
