The round-trip property already fails to hold, because there are multiple kinds of hashes, and they are not equal. (equal? (string->jsexpr (jsexpr->string (hash 'a 1))) (hash 'a 1)) Allowing strings would make the equal? situation worse, though, and it would introduce new kinds of questionable/bad jsexprs, like (hash "a" 1 'a 2) and (hasheq "a" 1 (string #\a) 2).

Is there any Z3 bindings for Racket? I found some packages on the Internet, but I don’t know which one should I use.

@chansey97 #lang rosette has z3 bindings https://emina.github.io/rosette/\|https://emina.github.io/rosette/ https://docs.racket-lang.org/rosette-guide/sec_solvers-and-solutions.html#%28part._.Z3%29\|https://docs.racket-lang.org/rosette-guide/sec_solvers-and-solutions.html#%28part._.Z3%29

Thanks @spdegabrielle. But can rosette/solver/smt/z3 be used as a general z3 API interface (e.g. z3py)? Or it is just be used for rosette by itself? For example, (List Int) in Z3 is a solvable type, but not in rosette. (solvable? list?) ; => #f, I even don't know how to define a recur solvable type in rosette. BTW, the docs doesn’t tell me how to use rosette/solver/smt/z3 as a SMT solver directly.

Add some background information:

I am comparing traditional Logic Programming (e.g minikanren/Prolog) vs Satisfiability Modulo Theories (e.g. z3). Although using different theoretical frameworks, they are very similar (Consider CLP(X) vs DPLL(T)).

For one direction, we seemly can use an SMT solver as minikan’s backend for constraint logic programing. In fact, someone has already done this work, see https://github.com/namin/clpsmt-miniKanren

For another direction, I think an excellent SMT solver can do constraint logical programming efficiently (to some extent). But there are very few materials about this on the internet. So I have to tried it by myself.

My first attempt is executing a program backwards. For example, implements minikanren’s appendo relation in z3. In fact, I have succeeded in smt2 language. The problem is that smt2 cannot get all the satisfying models automatically. We must use some API binding. This is why I want a z3 API binding in Racket.

PS. I have tried z3py, but failed. The z3py’s docs is very brief and difficult to read, especially about “how to define a recursive function”. Frankly, I posted a https://stackoverflow.com/questions/68450731/converting-appendo-relation-from-smt2-to-python\|question in StackOverflow, but no one has answered so far.

Notice that smt2 is a s-expr language. So I think its API binding should be compatible well with Racket. Or more easily, we can construct smt2 commands in Racket and send them to z3 process. But I hope some framework code (or lib) can do this out of box.

Does anyone know of other languages that use Racket’s separate phases of execution model?

Here’s a good one: https://github.com/philnguyen/z3-rkt\|https://github.com/philnguyen/z3-rkt

Maybe Sweet.js? I not 100% sure though - maybe they only have phase 0 and 1.

According to this blog post, there are infinite many phases. https://medium.com/@disnet/sweetening-syntactic-abstractions-e615ab87f2dd

And Tim Disney writes they are using the Racket approach.

Looks interesting, thanks!

I think rust’s approach effectively implements phases too

That’s interesting, I’d never thought of it that way, but yeah I guess it does?

A Rust procedural macro is compiled into a library, which is then used by the compiler to expend code that uses that macro :thinking_face:

Maybe you could look at how rosette does it and create your own standalone z3 library for racket?

{scribble again, sorry} The online docs still give red-underlined tags despite having for-labelled the relevant libraries (as can be seen https://github.com/Metaxal/text-block/blob/main/scribblings/combiners.scrbl#L3\|here), and raco setup --check-pkg-deps reporting no issue. Strangely, the issue doesn’t appear when generating the docs on my laptop.

I think, you need to add racket/base too.

That would be strange, since these symbols are exported by the libs listed above

I’ll try though

exact-nonnegative-integer? is in racket/base

Huh, right indeed…

@spdegabrielle Yes, that is what I originally wanted to do, but rosette’s source code is a bit hard to read (lacking z3 wrapper’s unit test). I just found clpsmt-miniKanren has z3-driver.rkt and z3-tests.rkt, which seems what I want. I’m reading her code :wink:.

When I scribble-run the page alone on my laptop, these tags are always in red though, even with for-label racket/base . And if I raco setup then raco docs all links are good. That makes it a little complicated to debug. Is there a simple way to do it to see how it would render on http://docs.racket-lang.org\|docs.racket-lang.org?

I use this to invoke scribble. raco scribble +m --htmls --dest htmls --redirect-main <http://docs.racket-lang.org> manual-sketching.scrbl &amp;&amp; open htmls/manual-sketching/index.html

I think, that handles the red tags at least. I did see a difference between raco setup and raco scribble when racket/gui was instantiated (but that seems to be a "don’t do that-situation).

Thanks a bunch @soegaard2

I still had to run raco setup to remove the red links though

I usually just start the z3 process and send s-expressions

Here a tiny example https://gist.github.com/shhyou/ce02ba69a2ecc7f89a7f704eb8e1f8b2

I think, I picked it up here on Slack.

Thanks. @shu—hung Can it run in windows? It tells me ; error writing to stream port Sorry I am not familiar with system programming in Racket.

Yes it can. You need to provide the full, absolute path to z3.exe in https://gist.github.com/shhyou/ce02ba69a2ecc7f89a7f704eb8e1f8b2#file-solver-rkt-L9

SMTLIB is an S-expression language so I do think directly launching the process and interact with it is the most straightforward way

using the API binding, however, is going through FFI and C etc

@shu—hung I run the module test, it gives a error: > solve: cannot parse model ((define-fun x () Int 10)) > input: ((declare-const x Int) (assert (= (* x 2) (+ x 10))))

What is the convention with respect to syntax-track-origin? (when should it be used)

Hmm, I’m using Z3 4.8.7. What version of z3 are you using?

z3–4.8.12

Do you know if Z3’s syntax changed since then? Looks like the code is expecting the output (model (define-fun x () Int 1) ) from the solver but there’s no model around the output.

@shu—hung I switched to z3-4.4.1 , it works. Thanks!

Okay. Basically, this is what solve is doing: 1. send the given S-expressions to Z3 2. send (check-sat) (L45) 3. get an S-expression from the solver. if the output is sat, (L47-L50) 4. send (get-model) to the solver (L51) 5. get an S-expression from the solver. expect the output to have the form `(model (define-fun ,vars () ,typs ,vals) ...)

@shu—hung Yes. The syntax has changed. In z3–4.4.1, there is a model at the top of the s-exp. In z3–4.8.12, no model at the top.

Okay! So that’s the problem

Moreover, the code isn’t doing much in parsing the output from the solver. For example, it does not handle ite, functions (and hence no arrays), etc

One most visible part is probably the missing handling for let

@shu—hung What do you mean by “missing handling for let”? Sorry I am new to z3.

The output of Z3 can contain let expressions. I forgot the concrete syntax in SMTLIB2, but it’s documented in the SMTLIB2 language

So you might want to handle it

> Moreover, the code isn’t doing much in parsing the output from the solver. For example, it does not handle ite, functions (and hence no arrays), etc > One most visible part is probably the missing handling for let That’s not a big problem:grinning:. I can fine-tune the code by myself or comparing with z3-driver.rkt in clpsmt-miniKanren (which use a similar approach). Thanks.

I found the relevant decoding code in Rosette EDIT: https://github.com/emina/rosette/blob/master/rosette/solver/smt/dec.rkt#L135

Out of curiosity. Is there a way to force DrRacket to do a GC? I currently have a DrRacket instance running for a while. I closed all the tabs at the some point, but DrRacket is using 1.6G

Thanks.

You can call (collect-garbage) or click the recycle icon

BTW, the FFI approach is very difficult to use (e.g. z3py’s docs is too brief:thinking_face:).

Thanks @camoy. I will try it.

Is it possible to monkey patch a struct (e.g. add a gen:stream or gen:custom-write to it post-hoc)?

But since it does not support parameterized sort, it may not be able to implement List Int type (see background information in the thread below).

no, that’s not possible

I would probably create a wrapper struct with the property

I remember reading something about being able to forward parts of the struct, but I could be making that up? i.e., the wrapper should be able to automatically create wrapper field-accessors &c.?

Maybe that was some kind of struct inheritance/extension I saw, idk anymore

yeah, that sounds familiar. a wrapper is fine, just wondered if there was a method of doing it

you could use struct inheritance as well, the substruct could implement the properties

I’m using racket/engine , and I’m having issues with the main thread being blocked after exiting on a timeout. I know there are issues with mutable hash tables using equal? and eq? comparisons. Are there any other data structures with this issue? For instance, the main thread will be blocked if I try to print the value of a box used in the engine, but that seems wrong. Additionally, if I create another thread (not in engine) that simply prints the stack trace of the main thread every so often, the main thread will start executing again. Unfortunately, I have no small example for this, so I’m describing this issue in broad strokes. Any help is appreciated.

To recreate this issue: Checkout: https://github.com/bksaiki/herbie/tree/thread-safe Run: make install (requires cargo) racket src/herbie.rkt report --threads 1 --timeout 5 bench/hamming graphs

Is there a nice, built-in (list? stream?) -> (stream? list?) function?

Doing what?

I have a list of streams and want to convert it into a single stream that returns a list of values each iteration

I can write something, but if a function already existed (that I’m not seeing), I’d rather use that :wink:

Not sure, haven’t used streams in a while.

sadly stream-map doesn’t take multiple streams

I don’t think there’s a built-in function, but we can write one: https://stackoverflow.com/questions/59232050/varadic-zip-in-racket/59232230#59232230

Is it possible that the error message for a contract violation does not correctly describe the actual contract? I received the following error: licensing-search: contract violation expected: string? given: #f in: an element of the 6th argument of (->* (connection? string? Date? (listof hash?) (listof string?) string?) (#:case-key-set set-mutable? #:fuzzy-address-search? boolean? #:limit exact-positive-integer?) any) contract from: (function licensing-search) blaming: /home/deploy/crcracket/ncaoc/acis/licensing-search.rkt (assuming the contract is correct) but the code is: (define/contract (licensing-search conn api-username reference dob names driver-licenses last4ssn #:limit [ limit 100 ] #:fuzzy-address-search? [ fuzzy-address-search? #f ] #:case-key-set [ case-key-set (mutable-set) ]) (->* (connection? string? string? date? (listof hash?) (listof string?) string?) (#:limit exact-positive-integer? #:fuzzy-address-search? boolean? #:case-key-set set-mutable?) any) The error message is missing the 3rd argument i.e. the second string?, so this makes me wonder if the “6th argument” part of the error is accurate.

The fact that it says “in an element of” seems to imply a list, so it does seem to be the actual 6th argument vs. the 6th argument in the error message.

Ah, this is nicer than what I cobbled together. Thanks!

That seems like it would be a bug, but I just tried to replicate it with this code and I got “7th”: #lang racket (require racket/date) (define (connection? x) #t) (define/contract (licensing-search conn api-username reference dob names driver-licenses last4ssn #:limit [ limit 100 ] #:fuzzy-address-search? [ fuzzy-address-search? #f ] #:case-key-set [ case-key-set (mutable-set) ]) (->* (connection? string? string? date? (listof hash?) (listof string?) string?) (#:limit exact-positive-integer? #:fuzzy-address-search? boolean? #:case-key-set set-mutable?) any) (void)) (licensing-search #f "x" "x" (current-date) null null 'x)

Strange. The code hasn’t changed since Oct 2020, so it’s unlikely to be an out of date compilation.

I saw it’s used when you want to forge a new identifier based on an existing identifier.

In fancy-app, it turns (+ _ 1 _ 2) to (lambda (x1 x2) (+ x1 1 x2 2)).

In the above example, you want to create two new identifiers “x1” and “x2", but you also want x1 to inherit whatever the first _ has, and x2 to inherit whatever the second _ has.

https://github.com/samth/fancy-app/blob/master/main.rkt#L18

I took your example, slightly modified, and I got the correct error message: licensing-search: contract violation expected: string? given: #f in: an element of the 6th argument of (->* (connection? string? string? date? (listof hash?) (listof string?) string?) (#:case-key-set set-mutable? #:fuzzy-address-search? boolean? #:limit exact-positive-integer?) any) I’ve viewing the error via journalctl on Ubuntu Linux, so I’m wondering if the line containing the 3rd argument just didn’t get logged properly? Regardless, I think I can count on it being the 6th arg which is all I need. Thanks @samth

I used: #lang racket (require racket/date) (define (connection? x) #t) (define/contract (licensing-search conn api-username reference dob names driver-licenses last4ssn #:limit [ limit 100 ] #:fuzzy-address-search? [ fuzzy-address-search? #f ] #:case-key-set [ case-key-set (mutable-set) ]) (->* (connection? string? string? date? (listof hash?) (listof string?) string?) (#:limit exact-positive-integer? #:fuzzy-address-search? boolean? #:case-key-set set-mutable?) any) (void)) (licensing-search #f "x" "x" (current-date) '() '(#f) "1234")

This is on Racket v7.3 for what it’s worth.

I get the same (correct) error message for both 7.3 and HEAD

https://stackoverflow.com/questions/46596353/systemd-dropping-random-pieces-of-stdout might be related :(

Maybe not - I ran the full journalctl output and I don’t see any suppressed messages for today even though there are some suppressed messages last month.

Thanks for the example!

@badkins I notice it’s Date? in your first error message but date? in the define/contract. I don’t know the significance but wonder if that discrepancy might be a clue? Maybe the error message comes from another contract for another function, somehow??

One wild guess: That package added an optional argument, and your server is running an older version than the newer one you and Sam are looking at locally??

(By “that package” I guess I mean /home/deploy/crcracket/ncaoc/acis/licensing-search.rkt; I don’t know if it’s a package.)

Nim ( https://nim-lang.org ) has at least macros at compile time in addition to runtime execution. You can execute most of the code at compile time you could execute at runtime.

Thanks Greg. I just had another error, and the contract error has the same issue of the missing string?. That would be far too coincidental to be a logging issue with a missing log line. I’ve grep’d the code for licensing-search, and I only see one definition in my entire source tree, and that definition hasn’t changed since Oct 2020. But your catch of Date? vs. date? is an interesting one!! I’ll have to keep digging…

@samth crazy question, but I’ve grep’d my codebase and found zero occurrences of Date? - can you think of a possible explanation for the contract error to capitalize date? to Date? - I know it’s nuts, but I had to ask :)

That’s very weird

It’s blaming the right function at the right line of the right file, so this is so odd.

I’m able to reproduce the issue with 'Date? by (require gregor) , instead of (require racket/date) - but I expect that’s a red herring.

Although I’m mildly curious why that happens :)

@jaz do you happen to know why a Racket contract error would capitalize a gregor date? to ’Date? ? I doubt it’s related to my current problem, but any additional understanding of what’s going on with the contract system could be useful.

Does removing the compiled/ directories and performing full-system recompilation (raco setup ) help? do you have the old code before Oct 2020?

Currently being handled… All good

@badkins I do, indeed: https://github.com/97jaz/gregor/issues/18

And, in fact, I did find a way around this in datetime.

Is it possible to update the sqlite DLLs shipped with Racket? The version that ships wit Racket is 3.22.0, which is 3 years old. In particular this version contains a bug where a COMMIT might report success even though it failed (this bug was introduced in 3.17.0 and fixed in 3.32.2).

This is the bug that was fixed: https://www.sqlite.org/src/info/810dc8038872e212 And this is the release log for SQLite: https://sqlite.org/changes.html

I think someone had a package that packaged updated SQLite binaries, but I forget who it was

I think it is @popa.bogdanp: https://github.com/Bogdanp/racket-libsqlite3, however, is there a reason why this needs to be a separate package while Racked ships with a very old version?

I agree that this should be fixed; just mentioning an alternative solution at the moment

If I understand the process correctly, it would be just a matter of taking the prebuilt binaries from that package and adding them to https://github.com/racket/libs

If this is all that it is involved, and @popa.bogdanp is OK with using the binaries he built, I would be happy to do this and submit a pull request for this.

I think there’s code somewhere for the build process but I can’t find it now, so a PR seems fine

the (hash "a" 1 'a 2) case is particularly bad

since at least with the other kinds of round-tripping, it’s fairly easy to guess what the result will be

round-tripping (hash "a" 1 'a 2) could validly produce any of the following four results: • (hash "a" 1) • (hash 'a 2) • (hash "a" 2) • (hash 'a 1) …and I don’t really see any “logical” best choice

in the case of key collisions, throwing an exception would be the best choice IMO

One possibility is to define jsexpr? as:

jsexpr? = ... \| (hash/c symbol? jsexpr?) \| (hash/c string? jsexpr?)

Then you can’t mix symbol? and string? within one hash, but can mix them across hashes

It still won’t fix the equal? issue, but at least the (hash "a" 1 'a 2) problem won’t occur

You can use transposing in Rebellion to do that

Rhombus should “fix” this issue though

(in-transduced streams (transposing #:into into-list)) will give you a lazy (sequence/c list?)

It’s not quite a (stream/c list?) though

Oh wait, transposing requires that all of the sequences have the same length. Does that matter for your case?

if we’re talking about how to deal with this problem in Rhombus, I’m half-tempted to suggest just getting rid of symbols and mutable strings

> If this is all that it is involved, and @popa.bogdanp is OK with using the binaries he built, I would be happy to do this and submit a pull request for this. Feel free! @alexharsanyi

Heads-up, though, that my version of the Windows libs are built on Windows Server 2016 so it’s possible (likely?) that they won’t work on Windows versions older than Windows 10 so that might be a problem with just copying them into racket-libs. I don’t know what the minimum supported Windows version is, but I assume it’s older than Windows 10.

I checked both the x86 and x64 sqlite DLLs for windows and they only link against kernel32.dll, so I think they would work fine on older windows versions, except perhaps Windows XP. However, I have no way of testing this…

Looks interesting too, thanks a lot!

Is there something in the standard library or a third-party package which is like https://docs.racket-lang.org/reference/pairs.html?q=cartesian#%28def._%28%28lib._racket%2Flist..rkt%29._cartesian-product%29%29\|cartesian-product , but yields the inner lists (or maybe vectors for faster random access) lazily? Outside the standard library, I found https://docs.racket-lang.org/for-helpers/index.html?q=in-nested#%28form._%28%28lib._for-helpers%2Fextra..rkt%29._in-nested%29%29\|in-nested , but from the syntax it seems to assume that the number of sequences is known at compile time.

I like the language a lot, but all in all I seem to have even more fun with Racket. :smile:

Fair enough :D seems to be a lot of people’s experience, that they always go back to their Lisp of choice. I’m still a newbie in this space, but maybe that’ll be me in the future haha

good question, an in-cartesian-product function would be a good thing to add to racket/sequence

I learned and used Nim before Racket, but after getting used a bit to the latter I’m now enjoying it more than Nim. But I still like programming in Nim when Racket isn’t a good fit.

Note that Nim is an imperative language. There are some FP-like features (say, higher-order functions and anonymous functions), but the data structures usually used, say, in the standard library, are all mutable.

Here’s one possible implementation

(require racket/generator) (define (product . xss) (in-generator (let loop ([xss xss] [acc '()]) (cond [(null? xss) (yield (reverse acc))] [else (for ([x (in-list (first xss))]) (loop (rest xss) (cons x acc)))]))))

I saw there’s https://docs.racket-lang.org/reference/sequences.html?q=in-parallel#%28def._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._in-parallel%29%29\|in-parallel which would suggest in-nested for the new function, although it would conflict with the for-helpers package. :wink:

This version is a bit more efficient, but the ordering is not consistent with cartesian-product. It still enumerates correctly though, just with different ordering

(define (product . xss) (in-generator (let loop ([xss (reverse xss)] [acc '()]) (cond [(null? xss) (yield acc)] [else (for ([x (in-list (first xss))]) (loop (rest xss) (cons x acc)))]))))

That was quick! :slightly_smiling_face: I want this in the standard library, both. :smile:

For the first version I checked that you can use it with sequences in general if you remove the in-list call.