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

57 commits

Author SHA1 Message Date
Dan Liew 462d3e8e8b [CMake] Unbreak building the .NET bindings.
7fefe40f21 broke building the .NET
bindings by renaming the signing key without updating the CMake build.
2016-10-17 18:19:31 +01:00
Dan Liew 03071db3ed [CMake] Fix building the examples when libz3 is built as a static library. 2016-10-17 18:19:31 +01:00
Dan Liew 4ef55505e7 [CMake] Fix #763 reported by @jirislaby.
`INTERFACE` was the not appropriate usage requirement to use. However
it only caused a problem when USE_LIB_GMP was enabled. With `INTERFACE`
`-lgmp` was not specified on the link line so `libz3.so` did not have a
reference to the library and linking against `libz3.so` by clients
would fail with missing references to symbols in `libgmp`.
2016-10-17 18:19:25 +01:00
Christoph M. Wintersteiger 12c47348bc Merge pull request #761 from delcypher/bv2fpa_unbreak_cmake_build
Unbreak the CMake build broken by 009af4455d
2016-10-17 11:47:01 +01:00
Nikolaj Bjorner aec59e4ff7 add consequence finding to inc-sat-solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-10-16 15:43:28 -04:00
Dan Liew b2381acceb Unbreak the CMake build broken by 009af4455d
The commit added an additional source file and dependency but the
corresponding changes weren't added to the CMake build.
2016-10-15 21:42:20 +01:00
Nikolaj Bjorner cf56da8482 add z3test to cmakelists.txt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-09-21 16:33:30 -07:00
Nikolaj Bjorner 14668b4d44 Merge pull request #735 from angr/new-build
New packaging for and ability to distribute python bindings
2016-09-21 15:55:22 -07:00
Andrew Dutcher f451363a8f use copy instead of create_symlink when not on unix 2016-09-21 15:15:21 -07:00
Nikolaj Bjorner 7f29674842 add option to bypass compression of unbound tails, issue #738
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-09-16 14:56:10 -07:00
Andrew Dutcher 9e498536b6 Fix cmake build to work with the new system 2016-09-15 02:19:20 -07:00
Andrew Dutcher 0bbd172af3 First steps to a sane python build 2016-09-14 01:37:04 -07:00
Nikolaj Bjorner 8221a09659 fast path for antecedent extraction in smt_context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-28 16:49:19 -07:00
Nikolaj Bjorner 083939ab0e add tactic to eliminate enumeration sorts in favor of bit-vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-23 14:11:21 -07:00
Nikolaj Bjorner 9ed2c846a9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-21 18:19:10 -07:00
Nikolaj Bjorner 3581f6de42 remove stale SLS option
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-21 18:18:42 -07:00
Nikolaj Bjorner 16e3a91bdf fix issues reported by Geoff
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-21 07:56:21 -07:00
Nikolaj Bjorner 1073e161c7 remove deprecated max-sat solvers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-20 19:08:23 -07:00
Nikolaj Bjorner f3d657ebd1 add tptp5 example to cmake, adding output SZS directives for Geoff
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-15 12:09:23 -07:00
Nikolaj Bjorner 16ad33bf39 add collection of statistics #652
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-13 18:17:49 -07:00
Nikolaj Bjorner 9f5a117443 move mus to solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-10 16:24:14 -07:00
Nikolaj Bjorner 6aa6102891 factor out model-based-opt code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-27 15:08:10 -07:00
Nikolaj Bjorner 68c7d64d00 adding model-based opt facility
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-27 11:18:20 -07:00
Christoph M. Wintersteiger fb86b01a8b Merge pull request #576 from delcypher/cmake_fix_windows_install
[CMake] Fix install of libz3.dll on Windows
2016-04-26 21:08:24 +01:00
Christoph M. Wintersteiger e24c6c14e0 Merge pull request #568 from delcypher/cmake_java_bindings
Teach CMake to build and install the Java bindings
2016-04-26 21:05:26 +01:00
Dan Liew fd7b8fe1ab [CMake] On Windows fix the `install` target so that it installs
``libz3.dll``.

I've left a comment about the installation of ``libz3.lib``. I'm not
sure if we want that installed or not.
2016-04-26 11:49:46 +01:00
Dan Liew 626e0736d2 [CMake] Implement installation of ".NET" bindings on Windows.
We don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead we just copy into
installation directory.

There are several reasons for this:

* We can't install the Z3_DOTNET_ASSEMBLY_DLL into the gac in a portable
  way like we can with mono (i.e. the ``-root`` flag).
* It isn't best practice to use ``gacutil.exe``
  on Windows to install into the GAC, see
  https://msdn.microsoft.com/en-us/library/yf1d93sz(v=vs.110).aspx .

Taking this approach should be sufficient because we can now do
something like this

```
mkdir build
cmake -G Ninja -DCMAKE_INSTALL_PREFIX=<some_path> ../
ninja
mkdir <some_path>
ninja install
```

and then put the contents of <some_path> into a zip file which creates a redistributable zip file for Windows.
2016-04-26 11:24:16 +01:00
Dan Liew 7213280d9b [CMake] Emit a warning when configuring to build the `.NET` bindings under
a multi-configuration generator (e.g. Visual Studio).

The warning concerns different generated files clobbering each other.
Unfortunately there isn't a clean way to fix this right now. See
http://public.kitware.com/pipermail/cmake/2016-March/063101.html
2016-04-26 08:56:46 +01:00
Dan Liew 7cedf79b38 [CMake] When building the ".NET" bindings emit `Microsoft.Z3.dll`
and ``Microsoft.Z3.xml`` to the root build directory rather than
``<root_build_directory>/src/api/dotnet``.

This fixes #573 which makes the behaviour consistent with the Python
build system.
2016-04-26 08:56:25 +01:00
Dan Liew c6965d5cb2 [CMake] Try to fix the Windows build when building the Java bindings.
On Windows the ``z3java`` target is not a ``LIBRARY`` target so just
drop the ``LIBRARY`` keyword here.
2016-04-18 14:07:09 +01:00
Dan Liew a56a53e72d [CMake] Fix installation location of `com.microsoft.z3.jar` when
using CMake 2.8.12.2. It seems ``install_jar()`` in the version of
``UseJava.cmake`` shipped with that version of CMake doesn't handle
the ``DESTINATION`` argument correctly and treats that as the
installation location so CMake would install to
``/usr/local/DESTINATION`` rather than ``/usr/locale/share``.
2016-04-18 12:07:18 +01:00
Dan Liew a1e8311844 [CMake] Add version to `com.microsoft.z3.jar`. On Linux systems
the ``.jar`` file is created as ``com.microsoft.z3-4.4.2.0.jar``
and a symlink named ``com.microsoft.z3.jar`` is created which points
to it in the build and install directory.
2016-04-18 11:39:56 +01:00
Dan Liew 8f69728703 [CMake] Change default install location for `com.microsoft.z3.jar`.
It seems ``.jar`` files are typically installed into
``/usr/share/java``.
2016-04-18 11:39:56 +01:00
Dan Liew 022039535a [CMake] Implement support for building and installing the Java bindings.
I'm not entirely happy with some parts of the implementation

* The default locations for installing ``com.microsoft.z3.jar`` and ``libz3java.so``
  aren't correct.  CMake cache variables have been provided that allow the user to change
  where these get installed.

* The name of ``libz3java.so``. It doesn't conform to the Debian
  packaging guidelines (https://www.debian.org/doc/packaging-manuals/java-policy/x126.html)
  and I have not provided an option to change this.

* The fact that ``SONAME`` and ``VERSION`` are not set on ``libz3java.so``.

These issues should be addressed once we know the correct way to handle
installation.
2016-04-18 11:39:20 +01:00
Mikolas Janota 7ad9dec6c2 Adding cpp files for bv_trailing to CMakeLists. 2016-04-06 11:04:17 +01:00
Dan Liew cc12b1ebce [CMake] The bug in mono that causes the `gacutil` utility to crash if
the assembly was compiled with ``/platform:x64`` has now been reported
so update the comments to reflect this.
2016-03-28 23:10:23 +01:00
Dan Liew 20d3bf4d0c [CMake] Implement support for building the .NET bindings.
When using Mono support for installing/uninstalling the bindings
is also implemented. For Windows install/uninstall is not implemented
because the python build system does not implement it and Microsoft's
documentation (https://msdn.microsoft.com/en-us/library/dkkx7f79.aspx)
says that the gacutil should only be used for development and not for
production.

For now a warning is just emitted if ``INSTALL_DOTNET_BINDINGS``
is enabled and the .NET toolchain is native Windows. Someone with
better knowledge of how to correctly install assemblies under Windows
should implement this or remove this message.

A notable difference from the Python build system is the
``/linkresource:`` flag is not passed to the C# compiler. This means
a user of the .NET bindings will have to copy the Z3 library (i.e.
``libz3.dll``) to their application directory manually. The reason
for this difference is that using this flag requires the working
directory to be the directory containing the Z3 library (i.e.
``libz3.dll``) but setting this up with multi-configuration generators
doesn't currently seem possible.
2016-03-27 15:04:04 +01:00
Christoph M. Wintersteiger fe201013e0 Merge pull request #521 from delcypher/cmake_python_custom_install_location
[CMake] Add CMAKE_INSTALL_PYTHON_PKG_DIR option to control where python
2016-03-20 00:57:31 +00:00
Nikolaj Bjorner 67dc5ce2b5 fix cmake issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 15:51:31 -07:00
Nikolaj Bjorner 20bbdfe31a moving remaining qsat functionality over
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 15:35:26 -07:00
Nikolaj Bjorner 296addf246 add new files to cmakelists
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 12:44:44 -07:00
Dan Liew 8746cc4a14 [CMake] Add CMAKE_INSTALL_PYTHON_PKG_DIR option to control where python
bindings are installed.
2016-03-18 22:18:51 +00:00
Christoph M. Wintersteiger 80d8a6a660 Merge pull request #498 from delcypher/genfile_refactor
Refactor generated file code out of ``mk_util.py`` and into ``mk_genfile_common.py``
2016-03-11 18:44:01 +00:00
Christoph M. Wintersteiger 9095d7db44 Merge pull request #504 from delcypher/cmake_custom_install_dirs
[CMake] Provide a way to customise the install directories
2016-03-10 12:39:11 +00:00
Nikolaj Bjorner 843e95cddc updating CMakeLists file, hope it works :-)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-09 15:56:23 -08:00
Dan Liew 04ca873abb [CMake] Provide a way to customise the install directories used for
executables, include files and libraries. We use
``GNUInstallDirs.cmake`` which ships with CMake to do the difficult work
of setting a sensible default and setting up CMake cache variables.
These can be overriden when running CMake by setting the
``CMAKE_INSTALL_BINDIR``, ``CMAKE_INSTALL_INCLUDEDIR`` and
``CMAKE_INSTALL_LIBDIR`` cache variables.
2016-03-09 14:22:27 +00:00
Dan Liew e12875ddb5 [CMake] Mirror the additional NDEBUG define for non debug builds recently added
by 03a8ef2795 . This relates to #463

Also leave a note regarding ``compiler_flags_override.cmake`` its
value is a bit dubious now that the compiler flags are almost the CMake
defaults.
2016-03-09 11:46:46 +00:00
Dan Liew 98244ac9a9 [CMake] Remove global "generated file" dependency on `mk_util.py`.
Most file generation scripts don't depend on it anymore.

The exceptions are uses of ``update_api.py``. An explicit dependency
has been added here and a ``FIXME`` has been left to indicate that this
should be removed once ``update_api.py`` is completly independent of
``mk_util.py``.
2016-03-09 11:22:49 +00:00
Dan Liew a2e3788a20 [CMake] Refactor the dependency on `scripts/mk_util.py` into
a list ``Z3_GENERATED_FILE_EXTRA_DEPENDENCIES`` that is used by
the ``add_custom_command()`` declarations. This will let
us easily change the common dependencies for generating build files in
the future.
2016-03-09 11:22:48 +00:00
Dan Liew 114f09cf4c Add missing source file declarations to CMake build that were
added by 70f13ced33
2016-03-07 15:00:22 +00:00