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.
