3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Commit graph

1220 commits

Author SHA1 Message Date
Nikolaj Bjorner 3616688d6b update pipeline
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-10 17:26:47 -07:00
Nikolaj Bjorner 9cb47188ea Update release.yml for Azure Pipelines 2020-09-10 15:41:12 -07:00
Nikolaj Bjorner 79734f26ae move to python3 for release.yml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-10 11:51:28 -07:00
Nikolaj Bjorner 6e7a80b68e change version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-10 10:59:06 -07:00
Nikolaj Bjorner c481570257 disable pip in trial release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-10 10:16:57 -07:00
Nikolaj Bjorner fe43f8df8f na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-03 08:11:43 -07:00
Nikolaj Bjorner 35e3d8425c move fpa
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-29 11:16:21 -07:00
Nikolaj Bjorner b9cbb08858 shuffle dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-29 09:51:39 -07:00
Nikolaj Bjorner 86c11b9349 order
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-28 13:05:25 -07:00
Nikolaj Bjorner b03d1c8053 deps
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-28 13:01:49 -07:00
Nikolaj Bjorner 0440cfeea7 add smt params dependency
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-28 12:59:22 -07:00
Nikolaj Bjorner 4244ce4aad adding ack/model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-28 12:55:47 -07:00
Sergey Vladimirov 7f0b5bc129
Allow to skip System.loadLibrary() calls from Java Native class (#4667) 2020-08-28 07:30:26 -07:00
Nikolaj Bjorner 4ab35a9bb5 euf model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-26 15:55:20 -07:00
Nikolaj Bjorner c21a2fcf9f sat solver setup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-26 09:40:42 -07:00
Nikolaj Bjorner ecd3315a74 add sat-euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-25 12:16:57 -07:00
Nikolaj Bjorner 3dedc13481 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-24 02:00:37 -07:00
Nikolaj Bjorner 65e6d942ac euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-24 01:55:13 -07:00
Nikolaj Bjorner 96f10b8c1c user propagator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-22 19:01:04 -07:00
Nikolaj Bjorner 2d5b749745 extend solver callbacks with methods
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-21 19:24:59 -07:00
Nikolaj Bjorner 080be7a2af merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-21 12:14:28 -07:00
Nikolaj Bjorner 4857d60c99 user propagator over the API 2020-08-18 21:53:02 -07:00
Nikolaj Bjorner e591b321bb set guard/cf and dynamic base in release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-17 08:21:44 -07:00
Nikolaj Bjorner 4d586c2c13 remove stale references to gac/csc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-26 12:03:03 -07:00
Nikolaj Bjorner f17ead21f9 fix #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-21 10:11:39 -07:00
Nikolaj Bjorner e8b5abe63e revert - copy over xml in mk-dist mode #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 11:17:29 -07:00
Nikolaj Bjorner a7b71239ae copy over xml in mk-dist mode #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 10:22:57 -07:00
Nikolaj Bjorner 9bc5552ca2 add vcrunime pattern to distribution directive #4542
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-25 08:56:13 -07:00
Nikolaj Bjorner 274323b818 fix reset order for #4533
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-19 16:07:45 -07:00
Nuno Lopes 07e5b228a2 try to fix nightly build by moving to python3. python2 isn't supported anymore by setuptools 2020-05-31 11:40:13 +01:00
Ivan Gotovchits 24a9ca3226
fixes numerous issues in OCaml bindings building process (#4468)
It now works both in dynamic and static mode and the compiled
libraries can be used by all linkers in the OCaml system, without
any specificy instructions other than specifying the dependency on
the z3 library.

Using the libraries
===================

Compiling binaries
------------------

The libraries can be linked statically with both ocamlc and ocamlopt
compilers, e.g.,

```
ocamlfind ocamlc -thread -package z3 -linkpkg run.ml -o run
```
or
```
ocamlfind ocamlopt -thread -package z3 -linkpkg run.ml -o run
```

When bindings compiled with the `--staticlib` the produced binary will
not have any dependencies on z3
```
$ ldd ./run
        linux-vdso.so.1 (0x00007fff9c9ed000)
        libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb56f09c000)
        libgmp.so.10 => /usr/lib/x86_64-linux-gnu/libgmp.so.10 (0x00007fb56ee1b000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fb56ebfc000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb56e85e000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb56e65a000)
        libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb56e442000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb56e051000)
        /lib64/ld-linux-x86-64.so.2 (0x00007fb570de9000)
```

The bytecode version will have a depedency on z3 and other external
libraries (packed as dlls and usually installed in opam switch):
```
$ ocamlobjinfo run | grep 'Used DLL' -A5
Used DLLs:
        dllz3ml
        dllzarith
        dllthreads
        dllunix
```

But it is possible to compile a portable self-contained version of the
bytecode executable using the `-custom` switch:

```
ocamlfind ocamlc -custom -thread -package z3 -linkpkg run.ml -o run
```

The build binary is now quite large but doesn't have any external
dependencies (modulo the system dependencies):
```
$ du -h run
27M     run
$ ocamlobjinfo run | grep 'Used DLL' | wc -l
0
$ ldd run
        linux-vdso.so.1 (0x00007ffee42c2000)
        libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fdbdc415000)
        libgmp.so.10 => /usr/lib/x86_64-linux-gnu/libgmp.so.10 (0x00007fdbdc194000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fdbdbf75000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fdbdbbd7000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fdbdb9d3000)
        libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fdbdb7bb000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fdbdb3ca000)
        /lib64/ld-linux-x86-64.so.2 (0x00007fdbde026000)
```

Loading in toplevel
-------------------

It is also possible to use the built libraries in toplevel and use
them in ocaml scripts, e.g.,
```
$ ocaml
        OCaml version 4.09.0

 # #use "topfind";;
 - : unit = ()
 Findlib has been successfully loaded. Additional directives:
  #require "package";;      to load a package
  #list;;                   to list the available packages
  #camlp4o;;                to load camlp4 (standard syntax)
  #camlp4r;;                to load camlp4 (revised syntax)
  #predicates "p,q,...";;   to set these predicates
  Topfind.reset();;         to force that packages will be reloaded
  #thread;;                 to enable threads

- : unit = ()
 # #require "z3";;
 /home/ivg/.opam/4.09.0/lib/zarith: added to search path
 /home/ivg/.opam/4.09.0/lib/zarith/zarith.cma: loaded
 /home/ivg/.opam/4.09.0/lib/z3: added to search path
 /home/ivg/.opam/4.09.0/lib/z3/z3ml.cma: loaded
 #
```

To use z3 in a script mode add the following preamble to a file with
OCaml code:
```
  #!/usr/bin/env ocaml
  #use "topfind";;
  #require "z3";;

  (* your OCaml code *)
```

Then it is possible to run it as `./script` (provided that the code is
in a file named `script` and permissions are set with `chmod a+x
script`).

Of course, such scripts will depend on ocaml installation that shall
have z3 dependencies installed.

Using Dynlink
-------------

The built z3ml.cmxs file is a self-contained shared library that
doesn't have any depndencies on z3 (the z3 code is included in it) and
could be loaded with `Dynlink.loadfile` in runtime.

Installation
============

I did not touch the installation part in this PR, as I was using opam
and installed artifacts as simple as:
```
ocamlfind install z3 build/api/ml/* build/libz3-static.a
```

assuming that the following configuration and building process
```
python2.7 scripts/mk_make.py --ml --staticlib
make -C build
```

Though the default installation script in the make file shall work.

Dynamic Library mode
====================

The dynamic library mode is also supported provided that libz3.so is
installed in a search path of the dynamic loader (or the location is
added via the LD_LIBRARY_PATH) or stored in rpaths of the built
binary.

Build Artifacts
===============

In the static mode (--staticlib), the following files are built and
installed:

- `{z3,z3enums,z3native}.{cmi,cmo,cmx,o,mli}`: the three compilation
units (modules) that comprise Z3 bindings. The `*.mli` files are not
necessary but are installed for the user convenience and documentation
purposes. The *.cmi files enables access to the unit
definitions. Finally, `*.cmo` contain the bytecode and `*.cmx, *.o`
contain the native code. Files with the code are necessary for cross-module
optimization but are not strictly needed as the code is also
duplicated in the libraries.

- libz3-static.a (OR libz3.so if built not in the staticlib mode)
contains the machine code of the Z3 library;

- z3ml.{a,cma,cmxa,cmxs} - the OCaml code for the bindings. File
z3ml.a and z3ml.cmxa are static libraries with OCaml native code,
which will be included in the final binary when ocamlopt is used. The
z3 library code itself is not included in those three artifacts, but
the instructions where to find it are. The same is truce for `z3ml.a`
which includes the bytecode of the bindings as well as instructions
how to link the final product. Finally, `z3ml.cmxs` is a standalone
shared library that could be loaded in runtime use
`Dynlink.loadfile` (which used dlopen on posix machines underneath the
hood).

- libz3ml.a is the archived machine code for `z3native_stubs.c`, which
is made by ocamlmklib: `ar rcs api/ml/libz3ml.a
api/ml/z3native_stubs.o` it is needed to build statically linked
binaries and libraries that use z3 bindings.

- dllz3ml.so is the shared object that contains `z3native_stubs.o` as
well as correct ldd entries for C++ and Z3 libraries to enable proper
static and dynamic linking. The file is built with ocamlmklib on posix
systems as
```
gcc -shared -o api/ml/dllz3ml.so api/ml/z3native_stubs.o -L. -lz3-static -lstdc++
```

It is used by `ocaml`, `ocamlrun`, and `ocamlc` to link z3 and c++
code into the OCaml runtime and enables usage of z3 bindings in
non-custom runtimes (default runtimes).

The `dllz3ml.so` is usually installed in the stubs library in opam
installation (`$(opam config var lib)/stublibs`), it is done
automatically by `ocamlfind` so no special treatment is needed.

Technical Details
=================

The patch itself is rather small. First of all, we have to use
`-l<lib>` instead of `-cclib -l<lib>` in ocamlmklib since the latter
will pass the options only to the ocaml{c,opt} linker and will not
use the passed libraries when shared and non-shared versions of the
bindings are built (libz3ml.a and dllz3ml.so). They were both missing
either z3 code itself and ldd entries for stdc++ (and z3 if built not
in --staticlib mode).

Having stdc++ entry streamlines the compilation process and makes
dynamic loading more resistant to the inclusion order.

Finally, we had to add `-L.` to make sure that the built artifacts are
correctly found by gcc.

I specifically left the cygwin part of the code intact as I have no
idea what the original author meant by this, neither do I use or
tested this patch in the cygwin or mingw environemt. I think that this
code is rather outdated and shouldn't really work. E.g., in the
--staticlib mode adding z3linkdep (which is libz3-static.a) as an
argument to `ocamlmklib` will yield the following broken archive
```
ar rcs api/ml/libz3ml.a libz3-static.a api/ml/z3native_stubs.o
```
and it is not allowed (or supported) to have .a in archives (though it
doesn't really hurt as most of the systems will just ignore it).

But otherwise, cygwin, mingw shall behave as they did (the only change
that affects them is `-L.` which I believe should be benign).
2020-05-27 09:21:14 -07:00
Nikolaj Bjorner b3366bae5a remove test-examples from MacOS build, re-add maxsat example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-19 13:52:44 -07:00
Nikolaj Bjorner 5fe0eeda63 disable regressions in ST mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-19 09:37:06 -07:00
Nikolaj Bjorner fcd2bc605c try to make template parsing work
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:17:36 -07:00
Nikolaj Bjorner 323a752bbf disable maxsat. for a mysterious reason it started failing on a single macos build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:16:32 -07:00
Lev Nachmanson d3c00ca2c3 change mode to executable to some py files
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-05-16 14:12:16 -07:00
Nuno Lopes 0313cf6d4c restore exec bit on configure & scripts/*.sh 2020-05-16 20:07:36 +01:00
Lev Nachmanson 08940cff8f comment out the call to nra_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-05-15 11:26:40 -07:00
Nikolaj Bjorner 17b8db95c1 inc version
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-08 15:05:01 -07:00
Nikolaj Bjorner ee522e1668 update comment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-08 15:03:52 -07:00
Nikolaj Bjorner ad55a1f1c6 Update release.yml for Azure Pipelines
disable pypi republish for 4.8
2020-05-08 14:12:38 -07:00
Nikolaj Bjorner 42e6cbce3d publish also ubuntu build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-08 14:10:23 -07:00
Nikolaj Bjorner 9a44ed854b enable pip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-08 12:34:07 -07:00
Nikolaj Bjorner 2804b40edb disable nuget publish for now
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-08 12:32:57 -07:00
Andrew Helwer b42ea38028
Automatically push release pipeline packages to nuget.org (#4249) 2020-05-07 17:31:27 -07:00
Nikolaj Bjorner 611c14844d fix #3194, remove euclidean solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-08 16:05:13 +01:00
Phillip Schanely a20d4fa362 Use the latin-1 codec instead of ascii in Python bindings.
The latin-1 codec maps byte values 0-255 to unicode codepoints 0-255.
The ascii codec only maps the lower half of that range.
2020-03-05 21:52:22 -08:00
Nikolaj Bjorner 5a357f9998 fixup build of example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-02-27 14:34:44 -08:00
Nikolaj Bjorner 80c98dfb1f avoid const in ml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-02-27 10:40:10 -08:00
Nikolaj Bjorner a65efb682b avoid const in ml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-02-27 10:40:10 -08:00