<dh_work>
there are two things you can do with one of those and a Z3.Model.model (returned when you ask Z3 to solve), and both throw
<oni-on-ion>
hmm, not sure. just started to do some C ffi stuff myself with ocaml
<dh_work>
I wonder if the problem is thta I'm feeding z3 wrong inputs
<oni-on-ion>
possibly; ocaml type inference is super smart
keep_learning has joined #ocaml
<dh_work>
that wouldn't be the mechanism
<dh_work>
I found an old stackoverflow post about this but it doesn't apply to current z3
<dh_work>
companion_cube: do you know what's going on here?
<dh_work>
the simplest case of the intractable object I'm getting back prints from z3 as: (define-fun I0pp0_regarray () (Array Int (_ BitVec 32)) (lambda ((x!1 Int)) #x00000000))
<dh_work>
the func_decl thinks it's an uninterpreted function (its get_decl_kind is OP_UNINTERPRETED)
<dh_work>
nothing is working and I'm about to give up :(
<dh_work>
feeding more complicated constraints so it's not a constant function doesn't help, eithe.r
andrewlitteken has joined #ocaml
<dh_work>
oh charming
<dh_work>
I rearranged some stuff to try to pass in different constraints, and that bought me:
<dh_work>
Fatal error: exception Z3.Error("domain sort Int and parameter sort Int do not match")
* dh_work
gives up
oni-on-ion has quit [Read error: Connection reset by peer]
mfp has quit [Ping timeout: 244 seconds]
oni-on-ion has joined #ocaml
al-damiri has quit [Quit: Connection closed for inactivity]
oni-on-ion has quit [Ping timeout: 246 seconds]
oni-on-ion has joined #ocaml
ziyourenxiang has joined #ocaml
ale64bit has joined #ocaml
oni-on-ion has quit [Remote host closed the connection]
oni-on-ion has joined #ocaml
<dh_work>
(figured out the type mismatch, z3's reporting the wrong error)
oni-on-ion has quit [Remote host closed the connection]
pera has joined #ocaml
ale64bit has quit [Ping timeout: 245 seconds]
AnAverageHuman has joined #ocaml
oni-on-ion has joined #ocaml
oni-on-ion has quit [Remote host closed the connection]
gravicappa has joined #ocaml
<companion_cube>
dh_work: do you use only one context?
<companion_cube>
dh_work: also you can print stuff, it's probably a lambda
Guest76995 has quit [Ping timeout: 246 seconds]
AnAverageHuman has quit [Ping timeout: 256 seconds]
rcmerci has joined #ocaml
pera has quit [Quit: leaving]
dmiles has quit [Ping timeout: 258 seconds]
ygrek has quit [Ping timeout: 246 seconds]
rcmerci has left #ocaml ["ERC (IRC client for Emacs 26.1)"]
gareppa has joined #ocaml
gareppa has quit [Client Quit]
mal``` has quit [Quit: Leaving]
_whitelogger has joined #ocaml
freyr69 has joined #ocaml
Birdface has joined #ocaml
Haudegen has joined #ocaml
_whitelogger has joined #ocaml
_whitelogger has joined #ocaml
_whitelogger has joined #ocaml
_whitelogger has joined #ocaml
andrewlitteken has quit [Quit: Connection closed for inactivity]
Birdface has joined #ocaml
madroach has quit [Ping timeout: 264 seconds]
madroach has joined #ocaml
KeyJoo has joined #ocaml
dhil has joined #ocaml
johnelse has joined #ocaml
Serpent7776 has joined #ocaml
johnelse has quit [Ping timeout: 250 seconds]
johnelse has joined #ocaml
mfp has joined #ocaml
johnelse has quit [Read error: Connection reset by peer]
johnelse has joined #ocaml
zolk3ri has joined #ocaml
johnelse has quit [Quit: leaving]
Birdface has quit [Ping timeout: 250 seconds]
Birdface has joined #ocaml
silver has joined #ocaml
johnelse has joined #ocaml
johnelse has quit [Quit: Lost terminal]
johnelse has joined #ocaml
tane has joined #ocaml
eskatrem has joined #ocaml
zolk3ri has quit [Remote host closed the connection]
johnelse has quit [Quit: leaving]
Haudegen has quit [Remote host closed the connection]
johnelse has joined #ocaml
jao has joined #ocaml
jao is now known as Guest36354
weird_error has quit [Quit: weird_error]
Birdface has quit [Remote host closed the connection]
Birdface has joined #ocaml
zolk3ri has joined #ocaml
keep_learning_M has quit [Quit: This computer has gone to sleep]
keep_learning_M has joined #ocaml
JimmyRcom has quit [Ping timeout: 258 seconds]
<eskatrem>
Hi, what's the best REPL for ocaml on emacs? ocaml or utop?
Guest36354 has quit [Ping timeout: 246 seconds]
Birdface has quit [Ping timeout: 268 seconds]
freyr69 has quit [Remote host closed the connection]
<vsiles>
anything is better than ocaml REPL :D
<vsiles>
`rlwrap ocaml` is my minimal setting when I don't have utop
KeyJoo has quit [Remote host closed the connection]
<flux[m]>
it was about "on emacs" and I seem to remember utop in emacs has some benefits compared to standard ocaml, of course you need to have some mode to accompany it
Haudegen has joined #ocaml
<eskatrem>
never heard of rlwrap ocaml
<eskatrem>
flux[m]: what mode did you add?
<flux[m]>
I don't remember, it's been a while I've used it
<flux[m]>
if I needed to look for it, I guess I would google for utop emacs or look at ELPA :)
<eskatrem>
yeah but I mean, what functionalities did you add?
<eskatrem>
oh, I installed the package utop from ELPA and now the REPL has auto complete!
mengu has joined #ocaml
mengu has quit [Read error: Connection reset by peer]
mengu has joined #ocaml
ygrek has joined #ocaml
al-damiri has joined #ocaml
nikivi has quit [Quit: ZNC is awesome]
nikivi has joined #ocaml
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 246 seconds]
dimitarvp has joined #ocaml
dimitarvp has quit [Client Quit]
jao has joined #ocaml
malina has joined #ocaml
metreo has joined #ocaml
eskatrem has quit [Read error: No route to host]
malina has quit [Ping timeout: 246 seconds]
FreeBirdLjj has joined #ocaml
ale64bit has joined #ocaml
silver has quit [Read error: Connection reset by peer]
silver has joined #ocaml
dhil has quit [Ping timeout: 246 seconds]
malina has joined #ocaml
ale64bit has quit [Ping timeout: 258 seconds]
dhil has joined #ocaml
Haudegen has quit [Remote host closed the connection]
dmiles has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
<dh_work>
companion_cube: yes, it's a lambda, looks like this: (define-fun arr_1 () (Array Int (_ BitVec 32)) (lambda ((x!1 Int)) #x00000000))
<dh_work>
knowing this does not appear to offer any further leverage though :(
<companion_cube>
use Quantifier to extract the body
<companion_cube>
it's a bit tricky
<dh_work>
lambdas are quantifiers?
<dh_work>
I suppose that makes a certain amount of sense
<companion_cube>
yes, they've been added after the fact ^^'
FreeBirdLjj has quit [Ping timeout: 244 seconds]
<dh_work>
although what I've got is a func_decl and I don't see a way to get a quantifier from it
<companion_cube>
ah but then if you have a func decl the func decl API should be enough?
<companion_cube>
(can't remember, you probably have `body` somewhere)
<vsiles>
flux[m]: sorry I always filter "emacs" when I read it
<dh_work>
no, there's no body apparently
<dh_work>
what comes back from the solver is a Z3.Model.model; you can get a list of FuncDecl.func_decl from that
<dh_work>
then for each you're supposed to get the interpretation, which is either an Expr.expr or a FuncInterp.func_interp
<dh_work>
depending on whether it's a constant or a function respectively
<dh_work>
both these throw though
<dh_work>
so all I've got is a FuncDecl.func_decl
<companion_cube>
is ppx_deriving_protobuf production-ready?
Birdface has joined #ocaml
<companion_cube>
(alternatively, is ppx_protocol_conv + msgpck prod-ready)
Birdface has quit [Ping timeout: 264 seconds]
<dh_work>
ah, _if_ I have the original array expression I can use Model.eval to get the lambda value back, and then that's an expression so I can get the quantifier body
<dh_work>
unfortunately in my real code (not the example) that will be a gigantic pain
<companion_cube>
in any case you really should have a separate function to extract this kind of shit from the models
<dh_work>
well sure
<Drup>
(or use z3_overlay :3)
<companion_cube>
does z3_overlay provide a comprehensive API to extract models?
<companion_cube>
(it's not even on opam, Drup, come on)
<companion_cube>
"just use $unreleased-lib"…
<Drup>
it's not ? :O
<companion_cube>
`opam search z3` doesn't return anything like that
<Drup>
oh shit, I forgot to release it
<companion_cube>
:D
<Drup>
ah, no I didn't!
<Drup>
ah, yes, I did, it's pinned locally
<Drup>
dammit.
<companion_cube>
is there online docs?
<companion_cube>
have you tested the model extraction features on recent releases of z3?
<companion_cube>
(cause they've changed their model generation)
<Drup>
I have not
<Drup>
but it all go through the official API
<Drup>
the only magic is on the ocaml side, via GADTs
ziyourenxiang has quit [Ping timeout: 250 seconds]
<companion_cube>
so it doesn't provide anything convenient to extract functions from models
<Drup>
I haven't played with functions, no.
<companion_cube>
so it's not relevant to the problem ;)
<Drup>
But I don't see the difficulty
<companion_cube>
(functions and arrays, actually, these are the same)
<Drup>
arrays work.
<companion_cube>
have you tried to extract an array from a model on a recent version of z3? 🙄
<companion_cube>
(hint: it's going to be a lambda)
<Drup>
it doesn't matter much, I circumvent the question: I wrap it as `fun v -> get_value model (Z3.get a v)`
<companion_cube>
-_-
<companion_cube>
that's only good for concrete evaluation, not if you want to do symbolic things with the model
<Drup>
what, you would prefer I extract the model and write an SMT-model interpreter in OCaml ? It's pointless, Z3 is very good at interpreting SMT models
<companion_cube>
well it's a valid API, it's just much more limited in what you can do with it
<Drup>
You want a shalow embeding, right
mengu has quit [Quit: Leaving...]
JimmyRcom has joined #ocaml
<dh_work>
what I am doing doesn't necessarily require a symbolic model but it does require being able to feed the model back to a subsequent z3 invocation
<dh_work>
anyway I have something that works, it's just disgusting
<dh_work>
I suppose I should deploy this for now and file a bug upstream
Haudegen has joined #ocaml
AtumT has joined #ocaml
<companion_cube>
:D
dhil has quit [Ping timeout: 268 seconds]
Jesin has quit [Quit: Leaving]
Anarchos has joined #ocaml
Jesin has joined #ocaml
<Anarchos>
how to get the list of all the ocaml compilers version in opam ?
<Drup>
Anarchos: the list of the official released versions ?
<Anarchos>
Drup yes
<Anarchos>
i try to find the latest version without afl and immutable strings.
<Drup>
opam list --no-switch --all-version ocaml-base-compiler
<Anarchos>
afl is not supported on my platform due to lack of sys/shm.h and immutable strings are not compatible with dypgen
<Drup>
Why does it matter for afl ? It's just instrumentation, it doesn't add additional deps
<Anarchos>
afl needs <sys/shm.h> to compile, which my platform does not have.
ygrek has quit [Ping timeout: 245 seconds]
malina has quit [Remote host closed the connection]
<dh_work>
if you don't need to run afl, just give it a fake one
<Anarchos>
dh_work a fake sys/shm.h ?
<dh_work>
yeah
<dh_work>
should be straightforward
<dh_work>
or patch ocaml to test for whether shm.h exists and not build afl if not
<dh_work>
also should be straightforward
<dh_work>
they might even take it upstream, you never know
kakadu has quit [Remote host closed the connection]
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
gravicappa has quit [Ping timeout: 255 seconds]
Jesin has quit [Quit: Leaving]
Jesin has joined #ocaml
zolk3ri has quit [Remote host closed the connection]
Haudegen has quit [Remote host closed the connection]
kakadu has joined #ocaml
metreo has quit [Quit: Leaving.]
ygrek has joined #ocaml
jmiven has quit [Quit: co'o]
Haudegen has joined #ocaml
DomTorr has quit [Read error: Connection reset by peer]
jbrown has quit [Ping timeout: 240 seconds]
jmiven has joined #ocaml
DomTorr has joined #ocaml
jbrown has joined #ocaml
nopf_ has quit [Quit: leaving]
ygrek has quit [Ping timeout: 255 seconds]
Serpent7776 has quit [Quit: leaving]
unyu has quit [Quit: ERC (IRC client for Emacs 26.2)]
unyu has joined #ocaml
ygrek has joined #ocaml
tane has quit [Quit: Leaving]
eskatrem has joined #ocaml
kakadu has quit [Remote host closed the connection]
AnAverageHuman has joined #ocaml
eskatrem` has joined #ocaml
eskatrem has quit [Ping timeout: 250 seconds]
weird_error has joined #ocaml
AnAverageHuman has quit [Ping timeout: 256 seconds]
klntsky has quit [Ping timeout: 256 seconds]
klntsky has joined #ocaml
Haudegen has quit [Remote host closed the connection]