OCaml bindings status and compilation

Dec 14, 2013 at 3:33 AM
What is the current status of OCaml bindings? And how can I build the same? I downloaded v4.3.1 and could found how to build OCaml bindings.
Coordinator
Dec 16, 2013 at 12:26 PM
The current status is that there are two different ocaml bindings: First, the old ones (pre-4.0, but should still work) are in src/api/ml which also contains build instructions and second, completely new ones in the branch called ml-ng that are integrated with the new build system and they can be built by adding --ml to the call to python scripts/mk_make.py. The idea is that the ml-ng branch gets integrated with the next major release and there may be some smaller changes made to it before it is released, but the overall structure will most likely stay as it is now.
Apr 14, 2014 at 10:49 PM
Edited Apr 15, 2014 at 9:50 AM
I struggled today to make the binding link correctly with ocamlfind and opam. Here are my remarks

1) first, ml-ng is broken now because someone merged a bug from unstable but not the fix that came a few days later

2) Having z3native.c and z3native.ml is a terrible idea. Please change the name to z3native_stub.c or something else.

3) I have put together very simple _oasis and opam files that allow to build ocaml-z3 separately and to use it with ocamlfind (which is essential if you want this ocaml binding to be actually used) and with opam. I'm not sure if I can distribute them (I'm quite oblivious to those licensing issues, to be honest), but I will happily provide them if you are interested.

Thanks a lot for this new binding, I will start using it and report more remarks as I work with it.

Edit : also, the old binding doesn't work anymore, at least for me.
Coordinator
Apr 15, 2014 at 6:03 PM
Thanks a lot for your feedback! Figuring out ocamlfind had been on my list for a long time. I've now added make targets for ocamlfind installation. Installation should be fairly easy now:
python scripts/mk_make.py --ml
cd build
make
sudo make ocamlfind_install
(the last is also part of make install; on Windows ocamlfind_install is available even though intall isn't).

I've also updated examples/ml/README to show a typical call using ocamlfind. On my OSX machine this does not complain and it produces a binary, but that binary doesn't seem to do anything. I'll have to look at again that at some later point.

Thanks for pointing out that the ml-ng branch wasn't up to date with unstable, this has now been fixed.

The current Z3 license doesn't allow redistribution, so you shouldn't submit your own packages. We have also decided against publishing managed packages ourselves because there are simply too many package repositories that we would have to support. But if there is a way to publish a package that on the user's demand downloads (and perhaps compiles) Z3 then that should be fine (this is also how it's done for Oracle Java on many systems).

Josh Berdine has recently submitted a fix to his copy of the old ML bindings in his fork (see here), perhaps that fixes your problem with them too?

Could you elaborate on your 2)? z3native.c contains the implementation of the functions in z3native.ml/mli, so I don't see why that is a terrible name.
Apr 15, 2014 at 8:00 PM
What I did is that I extracted the source of the binding and used a regular ocaml build system (oasis + ocamlbuild) to compile them. z3native.c will produce a .o and z3native.ml will produce ... a .o, which will erase the previous one. Hence lot's of function are undefined, and it fails. The usual solution is to append "_stub" to the C file name.

About opam, it's a source package manager, so it should be possible to fetch and build the ml part, but considering that it builds also the C part, and link against it, I'm not sure it's such a good idea. However, "packaging" something that uses ocamlfind is very simple : you just need to have an "opam" file with the build instructions and the installation to the correct prefix (given by opam). opam is quite useful even with "local" packages so I will let you investigate it a little bit and see by yourself.

Anyway, thanks for the ocamlfind target ! :)

I started to work with the binding (and manage to get some simple examples to work). My first impressions:
1) There is no way, except using unsafe functions in Z3native, to retrieve the value of a numeral. Could you add one ? It seems there is an issue with machine size int, could it be possible to use Num/Big_int for this ? I could print and parse it back, but it's not very nice.
2) The binding in general is very unsafe, I'm writing an AST in ocaml with back and forth transformation functions, so that it's easier and safer to manipulate from ocaml. We could take the opportunity that we are in ocaml to make the binding much much safer.
3) There are some inconsistencies in the binding (some is_* functions are in Expr instead of Boolean, but some are in Arithmetic, this kind of stuff)


What is the best way for me to provide patches ? Fork + Pull request ?
Coordinator
Apr 16, 2014 at 1:32 PM
Awesome, thanks for all the feedback!

Absolutely, your reason for renaming z3native.c is totally valid and I've renamed it to z3native_stubs.c now.

I've also added get_big_int and get_ratio to get "standard" ocaml objects from integers and reals/rationals. There's really no better or more efficient way than converting to string and back at the moment, so that's what these implementations do (they also do that in other APIs).

Can you elaborate on 2) ? What exactly constitutes unsafety here? We had plans to provide a more higher level API (like the Python and .NET APIs), but finally we decided against that because of performance considerations. The current level of abstraction is a bit of a compromise, but it provides all necessary things without the most inconvenient things (e.g., reference counting is abstracted away) at reasonable performance.
I'm sure some users would still like a higher level API though, if you would like to work on something like that it's definitely a most welcome contribution! Note that because of licensing issues we have to keep the master/unstable/pure branches free of external contributions. However, we do have a `contrib' branch too. Leo described the release and contribution process in a blog post some time ago: External contributions

Re 3): Agreed, those have been moved now.
Apr 16, 2014 at 3:06 PM
Edited Apr 16, 2014 at 3:08 PM
Thanks for the quick answers and fixes!

For 2) Sorry for the lack of clarity. Typically, I could write :
Boolean.not ctx (Arithmetic.Integer.mk_numeral_i 3)
which, I presume, is going to fail horribly at runtime (I didn't even bother to try). It is possible to statically guarantee such operations in ocaml without any performance sacrifices, you just need to introduce, for example, an abstract type t in the module Boolean and make the function Boolean.not of type context -> Boolean.t -> Boolean.t
Just this, applied to all kind of terms, would make the binding safer and clearer.
To handle polymorphism/subtyping, as used in Arithmetic.add (which works over Real and Integers), one could use phantom types with polymorphic variants, for exemple in the Arithmetic module :
type 'a t (* = Expr.expr but kept abstract in the .mli *)
mk_mod : context -> [< `Int ] t -> [> `Int ] t
mk_add : context -> ([< `Int | `Real ] as 'a) t list -> 'a t
(this technique is called phantom types, because the type is never associated to a value, it's just here to encode informations)
I hope I'm clear enough. I will give some examples when I find my higher level api satisfying.


A few questions about the API/Z3. Sorry, I'm not very familiar with z3 to begin with.
What is going to happen if I assert non-boolean formules, "assert(x+3)" for example.
What is the point of sorts, as they are in the API right now ? Why would I need to create a new Boolean sort, for example ?
What can be inside a value in a model exactly ? Can I get back a model were one of the variable (or one of the branch of a function) is not a literal ?
Speaking of models, are all "constant" considered functions with a zero arity, regarding "Model.get_*_decls" ?

A new quick note : <return> tags are not interpreted by ocamldoc, and should be replaced by @return (no s at the end). Same goes for <c> tags (replace with brackets).
Coordinator
Apr 16, 2014 at 4:57 PM
Yes, this is what I meant by "compromise". In other APIs (e.g., Python, .NET) we have special types like BoolRef and BitVecRef that allow us to make track what kind of expression is being used, but in the case of Ocaml we decided not to do that for performance reasons: basically every time a pointer is returned from the underlying C-API, we have to do a number of additional API calls to figure out what kind of pointer that is to then be able to cast it to the correct OCaml-type.
At the moment, you're right, nothing stops you from constructing bogus expressions that result in exceptions being thrown at runtime; in your example of (not 3) that is exactly what will happen.

Some answers to your questions:
assert(x+3) will throw a Z3_exception
Sorts are needed because they can be user-defined (e.g., datatypes); the basic sorts are included in that just for consistency.
What exactly a model value is depends on the theory you are using, integers and reals are straightforward, but for arrays for example the model is a function that maps indices to values. Theoretically you can also get a model where one variable is not assigned any value (if it's an actual don't-care). The Model.eval function takes a Boolean option called `completion', if that is set, then such models will be completed with default values.
Yes, every "const" is a function of zero arity; it's a "constant function" conceptually. In the case of models, the function get_const_decls provides a list of all constant functions that have a model value, and the function get_func_decls provides a list of all non-zero arity functions that have a model assigned. In the ML API there is also the get_decls function which provides a list of all decls, including zero and non-zero arity ones.

Thanks for catching the documentation bugs, those are now fixed!
Apr 17, 2014 at 12:13 AM
I got the following error with Integer.get_big_int ; Fatal error: exception Failure("invalid digit") The term should be "- 3" ... :/

I start getting the hang of it (or at least, the basic part), so thanks a lot for the help.

Starting tomorrow, I will play a bit with the opt branch, as I will need that too. Z3native.ml is auto-generated so I will just add some wrapper for the new functions. Hopefully it should be enough.
Coordinator
Apr 17, 2014 at 2:08 PM
Sorry about that, that was simply a bug which is now fixed! Apparently ocaml doesn't like spaces in those strings.
May 27, 2014 at 10:30 AM
Hello,

I'm using the newer OCaml bindings and I get a segmentation fault. The fault is random, if I print more to STDOUT the crash is not observed.

Following is the backtrace.

#0 0x00007ffff74e2484 in ast_table::erase(ast*) () from libz3.so
#1 0x00007ffff74e42ef in ast_manager::delete_node(ast*) () from libz3.so
#2 0x00007ffff6b9bdc8 in Z3_substitute () from libz3.so
#3 0x00000000004e34b5 in n_substitute ()
#4 0x00000000005dc5ec in caml_c_call ()
...

What could be the reason? Please give me some pointers on how to debug it more.

Manjeet

--
Manjeet Dahiya
http://manjeetdahiya.com


Coordinator
May 29, 2014 at 2:44 PM
Thanks for the report Manjeet. Do you have any more information than the backtrace? From the trace it looks like the call to substitute was given an invalid expression, either as part of the substitutions or as the expression to substitute things in (probably the latter).

Are you using timeouts? The current timeout handling procedures are known to create problems on some systems (see here).

What do you mean by random? Does it always happen on the same problems, but not all of them, or does it sometimes happen on the exactly same problem?
May 30, 2014 at 3:15 AM
Are you using timeouts? The current timeout handling procedures are known to create problems on some systems (see here).
No.
What do you mean by random? Does it always happen on the same problems, but not all of them, or does it sometimes happen on the exactly same problem?
With random, I mean that the crash is observed when fewer print statements are used. If I print more information the crash is not observed. Also in gdb, I have run the program many times to produce the crash. I'm unable to isolate the problem on which the crash is observed because as soon as I start logging the crash goes away.

I tried to google the problem and found the following page. Is it possible that Z3-ocaml-bindings may suffer from the same bug?
Coordinator
May 30, 2014 at 12:09 PM
It seems unlikely to me that this is caused by a stack overflow. I would rather think that something is going wrong with the reference counting or that somehow a bogus pointer into unallocated memory makes it into the expression that you're trying to substitute things in. Is there any way I could take a closer look at your application?
Jun 2, 2014 at 7:39 PM
Please give me sometime we are restructuring.

Just a quick out of topic question: I have two arrays a1 and a2. I want an expression for equivalence of these arrays. What function should be used? Will Boolean.mk_eq work? Because earlier in STP we could not do like this.
Coordinator
Jun 3, 2014 at 10:49 AM
Yes, mk_eq should work just fine. Take a look at the arrays section in the guide: Z3 Guide, Arrays. This is in SMT2 syntax, but you can see how equality and disequality constraints are generated using normal equality.
Coordinator
Jun 3, 2014 at 11:15 AM
We don't have a good Ocaml example program yet, but looking at the .NET example might be useful, e.g., ArrayExample2 shows how to use equality.
Jun 3, 2014 at 11:44 AM
I forgot to mention but I did this : https://github.com/drup/ocaml-z3

It's a (small for now, as I'm adding features when I need them) type safe overlay for z3, without any performance cost. There is a small example here : https://github.com/Drup/ocaml-z3/blob/master/test/simple.ml
It's designed so that's it's possible to still use the unsafe API for unimplemented parts (by using a downcast or Symbol.trustme).
Jun 10, 2014 at 12:04 PM
I get different result from ocaml and equivalent smt2 file (with z3 executable). I have posted the details here:


Please advise.


--
Manjeet Dahiya
http://manjeetdahiya.com


Jun 17, 2014 at 9:11 AM
Edited Jun 18, 2014 at 5:52 AM
I tried with C API too. It gets stuck like ML API. I think, I'm not choosing a correct solver. How can I know the solver or tactic is being used in Z3 executable?
Jun 18, 2014 at 5:52 AM
I tried with C API too. It gets stuck like ML API. I think, I'm not choosing a correct solver. How can I know the solver or tactic is being used in Z3 executable?
Coordinator
Jun 23, 2014 at 4:37 PM
This has been answered on stackoverflow now.
Aug 14, 2014 at 1:35 AM
@wintersteiger : would it be possible to add a configure option allowing compilation using a system installed z3 ?
Coordinator
Aug 14, 2014 at 11:53 AM
At the moment, the ocamlfind_install target installs a copy of libz3.dll/.so/.dylib into the ocamlfind directory, so when Z3 is built, a call to make install will install the correct version into ocamlfind as well. This is perhaps unnecessary, because at runtime it should use the first libz3.dll/.so/.dylib that it finds in PATH/LD_LIBRARY_PATH/DYLD_LIBRARY_PATH I think.

What would be the benefit of hardcoding a particular path during the build?
Aug 14, 2014 at 4:42 PM
Actually, after closer inspection, what I though was a linking issue may not be.

Would it be possible to compile and install cmxs ? It would allow to use the Z3 bindings directly in the toplevel (and also to dynlink against Z3).
You will also need to add two lines in the META which look like that :
archive(byte, plugin) = "z3.cma"
archive(native, plugin) = "z3.cmxs"
A target to only compile the ocaml part and not have to recompile all the C++ would still be nice, though. :)
Coordinator
Aug 14, 2014 at 6:09 PM
Thanks for the suggestion! I added the cmxs, it should now be installed into ocamlfind automatically (it may require you to rerun scripts/mk_make.py to create a new and clean build directory).

The ml target (i.e., make ml) or ocamlfind_install should not need to rebuild the C++ parts of the code (i.e. libz3.dll/.so/.dylib) if they are already built and the sources are unmodified.
Aug 15, 2014 at 7:42 PM
Bytecode linking still doesn't work. The reason is that the .so you give to ocamlfind is not the .so of the stubs, but the .so of the whole library.

There are numerous tools (1, 2) to build OCaml libraries. OCaml is a bit complicated to build, especially C bindings, and it's very easy to get it wrong, as those bug reports have proven, please use one of the two tools I linked instead of rolling your own makefiles rules. If it's not possible, please read this.

Previously I just took all the ml api sources and copied them in my project, and this was enough to compile them. I can't do that anymore, because it's basically impossible to distribute to other people.

I would like to be able to use the z3 bindings in any condition, being bytecode, native code or in the toplevel. It worked with the small piece of _oasis file I linked, so I except it to work in the official packaging too. Thanks.
Coordinator
Dec 6, 2014 at 5:42 PM
I've given the ML API build a bit of a revamp. For me, all of the use cases work now (byte, native, and toploop via ocamlfind). We have to roll our own makefiles because everything needs to be integrated with the rest of the build, and it can't require any tools that don't come in standard packages. In fact, providing an ocamlfind_install make target is already a breach of our principles (we don't supply any other managed packages).

If you have some spare time, could you test this new build to see whether that package now works for all your use cases too? Thanls!
Dec 7, 2014 at 12:28 AM
It works with byte, native and the toplevel now. Thanks.
Feb 11, 2015 at 3:51 PM
The toplevel is broken again, here is the error message:
Cannot load required shared library dllz3ml.
Reason: /home/gabriel/.opam/4.02.1/lib/stublibs/dllz3ml.so: /home/gabriel/.opam/4.02.1/lib/stublibs/dllz3ml.so: undefined symbol: Z3_mk_fpa_lt.
Feb 11, 2015 at 4:06 PM
And same problem with native compilation. I guess the new C file for FP is not linked.
Coordinator
Feb 11, 2015 at 4:16 PM
Edited Feb 11, 2015 at 4:16 PM
Hmm, both work fine for me. Are you by any chance trying this on the ml-ng branch which doesn't exist anymore? This has been integrated into unstable last week along with the FP features. Also, when you re-run scripts\mk_make.py, it creates a stubs file in src/api/ml/z3native_stubs.c and this file should contain a definition for n_mk_fpa_lt which calls Z3_mk_fpa_lt. The latter is included in libz3.so/.dll.
Feb 11, 2015 at 4:38 PM
Yes, it was based on unstable. I'll check if it was not file from a previous installation later.