3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-05 20:35:41 +00:00
Commit graph

73 commits

Author SHA1 Message Date
Dan Liew
a3e0eae9ec Move CMakeLists.txt files (other than the one in the repository root)
and the cmake directory into a new directory ``contrib/cmake`` that
mirrors the directory structure of the root. This is a comprimise
between me and Christoph Wintersteiger that was suggested by Arie
Gurfinkel that allows the CMake build system to live in the Z3
repository but not impact the Z3 developers that want to avoid the CMake
build system. The build system will not work in its new location
and a bootstrap script will soon be provided that allows a developer
to copy the files back to their correct location.
2016-03-04 15:26:09 +00:00
Dan Liew
251527603d Implement a CMake build system.
This is a large rework of my first attempt at this (#459).

This implementation calls into the recently implemented python scripts
to generate the necessary generated ``.h`` and ``.cpp`` files but is
independent from Python building system otherwise.  Unlike the Python
build system, the generated files are emitted into the build tree to
avoid polluting the source tree. The build system is setup to refuse to
configure if it detects generated files in the source tree. If your
source tree is dirty you can run ``git clean -fx`` to clean your working
directory.

Currently the build succeeds on Linux using CMake 3.4.3 using
the "Unix Makefiles" generator with gcc or clang.

The following notable features are implemented:

* Building of the C and C++ examples and the ``test-z3`` executable.
  These are included from the ``all`` target so you have to tell the
  build system (e.g. make) to build them manually.

* Install (``make install``) and uninstall (``make uninstall``) of libz3
  and its header files. This supports ``DESTDIR`` out of the box because
  CMake supports it.

* An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library.

* Support for using/not using OpenMP (``USE_OPENMP``)

* Support for using/not using libgmp (``USE_LIB_GMP``)

* Setting the SOVERSION for libz3. I'm not sure if I'm setting the
* number correctly though. This is required by Linux distrubtions that
  wills ship libz3. This needs discussion.

The following notable features are currently not implemented
and are left for future work.

* Support for ARM.
* Support for the foci2 library.
* Support for creating/installing/uninstalling the dotnet, java, python and ml
  bindings.
* Full support for MSVC. Although I've tried to write the CMake code
  with MSVC in mind not all the correct flags are passed to it.
* Support for using the git hash.

This new build system has several advantages other the old build system.

* It is easier for outside contributors to contribute to Z3 when the
  build system is something more standard.
* Incremental builds work properly. With the old build system when
  new code is pulled down the old build directory would need to thrown
  out and a new fresh build had to be performed because the build system
  didn't know how to correctly rebuild the project (e.g. couldn't handle
  new sources being added/removed, compiler flags changing, generated
  files changing, etc...). This is a MASSIVE boost to productivity!
* We now have access rich array of features that CMake provides for
  building C/C++ projects. This means less time spent implementing
  custom build system logic in Python that is already supported by
  CMake.
* CMake supports many IDEs out of the box so it should be fairly
  straight forward to build Z3 with Visual Studio (once support for MSVC
  is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-03-04 15:26:09 +00:00
Christoph M. Wintersteiger
4e37821dde "canceled" -> Z3_CANCELED_MSG
Relates to #431
2016-02-04 13:52:43 +00:00
Nikolaj Bjorner
96d1066c6a reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 16:43:48 -08:00
Nikolaj Bjorner
baee4225a7 reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 16:21:24 -08:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Nikolaj Bjorner
c09ac5422b fix by anomaly detection, issue #118
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-06-02 10:42:03 -07:00
Leonardo de Moura
f6f59ad6bc Fix memory allocation problems in RCF module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-04-10 19:03:25 -07:00
Leonardo de Moura
3ae01cf619 Fix cygwin (with python 2.6) compilation problems.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-28 17:29:55 -08:00
Leonardo de Moura
4624919786 Improve html pretty printer for RCF package
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-27 11:24:23 -08:00
Leonardo de Moura
77f58269ed Add html pretty printing mode for RCF package
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-27 10:19:54 -08:00
Leonardo de Moura
5d938a5fe2 Fix bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-20 18:41:24 -08:00
Leonardo de Moura
3344151aca Replace # with x in the definition of algebraic elements
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-20 18:21:09 -08:00
Leonardo de Moura
bb386c0f18 Fix problem in inv_rf
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-16 11:19:11 -08:00
Leonardo de Moura
eea3384106 Add lazy normalization for algebraic extension values. Increase default max_precision to 128.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-15 16:35:36 -08:00
Leonardo de Moura
217c8375ce Add new rational function normalization procedure.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-15 14:34:34 -08:00
Leonardo de Moura
f0737bdf7f Replace expensive_eval_sign_at with version that does not generate rational numbers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-14 18:30:36 -08:00
Leonardo de Moura
799fe073db Add API for extracting numerator/denominator of RCF numerals. Add field to store the original isolating interval before refinement.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-14 18:29:08 -08:00
Leonardo de Moura
991a1528cd Cache isolating interval for better pretty printing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-14 12:17:15 -08:00
Leonardo de Moura
025cb2a2a8 Avoid wasteful memory allocation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-14 12:03:22 -08:00
Leonardo de Moura
38e0b4a20a Fix bug. Add is_denominator_one macro.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-14 11:55:52 -08:00
Leonardo de Moura
742f2b07dd Add support for compact string representation in the RCF API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-14 11:08:32 -08:00
Leonardo de Moura
6c35e08e43 Make sure we do not use denominators != 1 when encoding values of algebraic extensions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-14 10:43:18 -08:00
Leonardo de Moura
7312f49f88 Fix Visual Studio warnings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-13 09:06:07 -08:00
Leonardo de Moura
f747bde548 Add restore_interval for extensions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 21:59:41 -08:00
Leonardo de Moura
be2bf861c7 Use clean_denominators before root isolation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 20:43:17 -08:00
Leonardo de Moura
2b5883454c Add support for prem_gcd in square_free
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 19:49:50 -08:00
Leonardo de Moura
551d0b7de0 Fix bug in sprem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 19:44:05 -08:00
Leonardo de Moura
7711146d23 Add prem_gcd based on pseudo-remainder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 19:36:07 -08:00
Leonardo de Moura
13d5c3e07a Add normalize_int_coeffs to control the coefficient growth in Sturm sequences
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 18:01:29 -08:00
Leonardo de Moura
e6102a8260 Move clean_denominators code to the top
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 17:11:42 -08:00
Leonardo de Moura
1e362e6fec Add comments to mark sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 17:08:58 -08:00
Leonardo de Moura
a9fa232f11 Fix bug in compare
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 16:45:24 -08:00
Leonardo de Moura
ea9421bb38 Expose rcf module parameters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 16:40:45 -08:00
Leonardo de Moura
e6a35c6241 Add prem to avoid rational function values
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 16:27:56 -08:00
Leonardo de Moura
09d3686d58 Fix memory leak in realclosure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 15:54:07 -08:00
Leonardo de Moura
1d761ea9a5 Add clean_denominators procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 15:45:43 -08:00
Leonardo de Moura
d60f2db116 Remove select method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-12 09:46:00 -08:00
Leonardo de Moura
a03a6e9bf6 Add more tracing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-11 21:12:51 -08:00
Leonardo de Moura
5ce70eb521 Fix bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-11 17:55:03 -08:00
Leonardo de Moura
3cc072f3a7 Add bisect_isolate_roots
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-11 16:28:39 -08:00
Leonardo de Moura
5a9040a247 Replace is_real with depends_on_infinitesimals to avoid misunderstandings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-11 10:35:38 -08:00
Leonardo de Moura
0de6b4cc92 Complete the implementation of expensive_algebraic_poly_interval
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-11 10:11:03 -08:00
Leonardo de Moura
714167a378 Add more tracing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-10 18:36:47 -08:00
Leonardo de Moura
2f5c7c9ba9 Add determine_algebraic_sign
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-10 17:07:32 -08:00
Leonardo de Moura
619e597174 Add normalize_algebraic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-10 13:38:51 -08:00
Leonardo de Moura
191e503418 Fix bug. Improve nl_nz_sqf_isolate_roots
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-10 12:51:54 -08:00
Leonardo de Moura
71ab7759d1 Add root method (syntax sugar for isolate_roots)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-10 12:23:37 -08:00
Leonardo de Moura
1a7d39f9a0 Add refine_algebraic_interval
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-10 12:09:07 -08:00
Leonardo de Moura
4a0b431cf4 Add mk_algebraic method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-10 11:13:21 -08:00