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

4442 commits

Author SHA1 Message Date
Christoph M. Wintersteiger 5510e0ddef Added finite-domain constant to Z3_decl_kind 2015-12-02 17:03:37 +00:00
Christoph M. Wintersteiger 5a43d8a469 Whitespace 2015-12-02 17:02:39 +00:00
Christoph M. Wintersteiger cbda38ee80 Added finite domain expressions and numerals to the .NET, Java, and Python APIs.
Relates to #318
2015-12-02 17:01:52 +00:00
Nikolaj Bjorner 6580f1daf3 expose main interpolation routines in C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-02 07:40:06 -08:00
Christoph M. Wintersteiger 9e756fb6db Warning fix for Comparable<T> in Java API 2015-12-02 14:42:36 +00:00
Christoph M. Wintersteiger 00ce124db3 Bugfix for Z3_is_numeral for finite-domain numerals.
Relates to #318
2015-12-02 14:41:46 +00:00
Christoph M. Wintersteiger 52bbd67cd3 Whitespace 2015-12-02 14:40:47 +00:00
Nikolaj Bjorner 216c1b2989 Merge pull request #349 from NikolajBjorner/master
add macro for converting std::vectors to pointers (leaking abstraction)
2015-12-01 18:36:16 -08:00
Nikolaj Bjorner 485ac9c39d add macro for converting std::vectors to pointers (leaking abstraction)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-01 16:35:03 -08:00
Nikolaj Bjorner 2916f14b40 Merge pull request #347 from NikolajBjorner/master
bind variables in queries generated from Horn tactic to enforce that …
2015-12-01 14:49:08 -08:00
Nikolaj Bjorner b3e8020c88 bind variables in queries generated from Horn tactic to enforce that rule formulas don't contain free variables. Issue #328
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-01 14:47:33 -08:00
Nikolaj Bjorner 388b4b6eb7 Merge pull request #346 from NikolajBjorner/master
bugfix for #343
2015-12-01 13:46:08 -08:00
Nikolaj Bjorner aa777bd5c6 Fix for #343. Optimizations introduced on 8-10-2015 were too agressive. Remove unreferened variable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-01 13:43:47 -08:00
Nikolaj Bjorner 9fa4bf2f8f Fix for #343. Optimizations introduced on 8-10-2015 were too agressive
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-01 13:41:57 -08:00
Nikolaj Bjorner f68c1d755f Merge pull request #344 from delcypher/fix_stray_uft8_bom
Fixed stray UTF-8 Byte order mark in ``InterpolationContext.cs``.
2015-12-01 05:21:00 +13:00
Dan Liew b0bc50a75c Fixed stray UTF-8 Byte order mark in `InterpolationContext.cs`.
Old versions of the mono compiler don't like it.
2015-11-30 15:02:02 +00:00
Nuno Lopes 5d289a8da5 fix leak in asserted_formulas::propagate_values() for proof generation mode
continuation of issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-11-29 10:49:52 +00:00
Dan Liew d2ba6f0ebf Provide a way to customise the install directories via environment
variables:

Z3_INSTALL_BIN_DIR - defaults to "bin"
Z3_INSTALL_LIB_DIR - defaults to "lib"
Z3_INSTALL_INCLUDE_DIR - defaults to "include"

This has two advantages

* We no longer hard code strings like "bin" all over the place
* Packagers can easily control where things get installed.
2015-11-28 19:11:03 +00:00
Dan Liew d205b176e8 Bug fix for `MakeRuleCmd.create_relative_symbolic_link()`.
create_relative_symbolic_link(out, '/usr/lib64/libz3.so',
'/usr/lib/python3.5/site-package/libz3.so') would create an incorrect relative
path because it would consider ``/usr/lib`` to a be a path prefix of
``/usr/lib64``.
2015-11-28 19:03:05 +00:00
Dan Liew f1d4f36ddf Refactor the use of `$(DESTDIR)$(PREFIX) in MakeRuleCmd`
class so that it is exposed via a public method (``install_root()``)
so that is can be used externally. Also refactor the existing methods
to use it.
2015-11-28 19:03:05 +00:00
Dan Liew 32c4384d48 Fix dead comment and expand on the reasons for making a symbolic link
slightly.
2015-11-28 19:03:05 +00:00
Dan Liew 684318149b Remove dead code that I accidently left behind. 2015-11-28 19:03:05 +00:00
Dan Liew 6984070b3a Fix typo (missing argument) that I missed that didn't fire because
I did not test on Windows.
2015-11-28 19:03:05 +00:00
Dan Liew d6fa0583ab Fix bug in `ExeComponent.mk_uninstall()` in the build system
which would try to uninstall components that were never installed.

This bug would cause the following line to be emitted in the
``Makefile`` under the ``uninstall`` rule even though there was
no corresponding rule to install the file under the ``install`` rule.

```
@rm -f $(DESTDIR)$(PREFIX)/bin/test-z3$(EXE_EXT)
```
2015-11-28 19:03:05 +00:00
Dan Liew 041c02feb7 Finish addressing @wintersteiger comments on `$(DESTDIR)` being
duplicated in too many places by refactoring the installation and
removal of the Python bindings to use the ``MakeRuleCmd`` class.

In order to make this change:

* ``PYTHON_PACKAGE_DIR`` no longer contains the text ``$(PREFIX)``
* ``PYTHON_PACKAGE_DIR`` **MUST BE** inside the installation prefix
2015-11-28 19:03:05 +00:00
Dan Liew 23cf7e86a9 Start to address @wintersteiger 's comments aboug `$(DESTDIR)` being
duplicated in too many places and being worried that someone might
forget to use it when installing additional components.

To acheive this the new ``MakeRuleCmd`` class provides
several class methods to generate commonly needed commands used in
make file rules.

Most of the build system has been changed to use these helper methods
apart from stuff related to the Python bindings. This can't be changed
until we fix how PYTHON_PACKAGE_DIR is handled. Right it not guaranteed
to live under the install prefix but this is a requirement when using
the ``MakeRuleCmd`` methods.
2015-11-28 19:03:05 +00:00
Dan Liew 53f0addb6b Avoid making a copy of libz3 on non Windows platforms for the
Python bindings (provided they both exist within the same install
prefix) by creating a relative symbolic link. This saves
space when packaging Z3.
2015-11-28 19:03:05 +00:00
Dan Liew e8822b1806 Add a note about using DESTDIR when building Z3 completes. 2015-11-28 19:03:05 +00:00
Dan Liew 4c11037d70 Fix setting the path to the Python package directory.
There were several problems with the existing implementation.

* When specifying ``--prefix`` the implementation would assume the
  path was ``$(PREFIX)/lib/python-<VERSION>/dist-packages``. This
  is incorrect. ``dist-packages`` is Debian (and its derivatives,
  i.e Ubuntu) specific and won't work on other Linux distributions
  such as Arch Linux.

* When generating the ``Makefile``, ``$(PREFIX)`` was only emitted
  during the Python installation when ``--prefix`` was passed on
  the command line. When ``--prefix`` was not passed the absolute
  path to the Python package directory was emitted. This is not
  very consistent.

This patch checks that the detected Python package directory lives
under the install prefix and emits an error if it does not as this
indicates that the installation will be broken. If the Python package
directory does live under the install prefix it replaces that prefix
with the ``$(PREFIX)`` variable when emitting the ``Makefile`` for
consistency with the other install commands.

If a user really wants to install to a particular Python package
directory they can force it with the newly added ``--pypkgdir=``
flag.
2015-11-28 19:03:05 +00:00
Dan Liew b285ce7cee Partially fix not being able to do a staged install (using `DESTDIR`)
when installing the Python bindings.

If ``DESTDIR`` is set the bindings will now be installed under this
path but ``$(PREFIX)`` only appears in the ``Makefile`` if ``--prefix``
was set which seems a little broken (we'll fix this soon).

The creation of the Python ``site-packages`` (and ``__pycache__`` for Python
3) directories has been moved to build time instead of configure time
because we don't know what ``DESTDIR`` will be set to at configure time.
2015-11-28 19:03:05 +00:00
Dan Liew 9489665ddc Partially fix not being able to do a staged package install of Z3 using the
DESTDIR make file variable (https://www.gnu.org/prep/standards/html_node/DESTDIR.html)
for ``install`` and ``uninstall`` targets.

Typically packagers build packages like so

```
$ ./configure --prefix=/usr/
$ make
$ make DESTDIR=/some/path/ install
```

Doing this installs the files into a directory ``/some/path`` but places
files inside that directory using the layout in ``--prefix`` (e.g.
``/some/path/usr/bin/z3``).  The ``/some/path`` directory can then be
packaged (e.g. tarballed) for later installation.

The ``DESTDIR`` is not set in the Makefile and thus is empty by default
which maintains the existing ``make install`` behaviour.

Unfortunately this situation isn't fixed for the Python bindings (and
possibly others) yet as more invasive changes are needed here. I'll fix
this in later commits.
2015-11-28 19:03:05 +00:00
Nuno Lopes d175c99542 fix ast leak in asserted_formulas::propagate_values()
Fixes issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-11-27 20:09:17 +00:00
Christoph M. Wintersteiger db2f973e3e Fixed initialization order in bvarray2uf_tactic 2015-11-27 15:34:06 +00:00
Nuno Lopes 2739930900 fix build with clang
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-11-27 12:13:44 +00:00
Christoph M. Wintersteiger 8eea6fd775 Bugfix for FPA float to float conversion.
Fixes #337
2015-11-24 17:21:40 +00:00
Christoph M. Wintersteiger 5e37cf9bbf Removed potentially unnecessary string decoding in Python API. 2015-11-23 18:41:31 +00:00
Christoph M. Wintersteiger 6aa5ec9f77 Eliminated unused variables 2015-11-23 13:12:05 +00:00
Nikolaj Bjorner 436a51d8f0 fix build of maxsat.c
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-22 22:10:22 -08:00
Christoph M. Wintersteiger 59c1944f92 Bugfix for FP casts (float to float conversion).
Fixes #331.
2015-11-22 14:49:04 +00:00
Nuno Lopes d9bafc3fba rewrite scoped_timer for linux
The previous version was racy and could lead to crashes.
The timer could be deleted before the callback was called, making it execute on already freed memory

This new version is similar to Mac's. It spawns its own thread and uses pthread_cond_wait.
Care is taken for small timeouts to avoid races in the thread creation and timer destruction.

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-11-22 11:40:52 +00:00
Nuno Lopes b26735a887 fix build with gcc
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-11-22 11:24:30 +00:00
Nikolaj Bjorner 3be279dc29 fix build break on maxsat.c example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-21 10:36:24 -08:00
Nikolaj Bjorner c1a6163bda disable aig tactic in inc_sat_solver (it can blow up the size of formulas significantly without sharing) and fix configuration update bug for optimization context exposed in example by Corina
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-20 14:34:31 -08:00
Nikolaj Bjorner 95fe9a3a68 Merge pull request #334 from NikolajBjorner/master
remove deprecated user-theory plugins and other unused functionality …
2015-11-20 11:47:05 -08:00
Nikolaj Bjorner 665af3d8b9 remove deprecated user-theory plugins and other unused functionality from API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-20 08:43:27 -08:00
Nikolaj Bjorner e96d93ee42 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-20 08:02:08 -08:00
Nikolaj Bjorner 995e112a18 fix examples
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-20 08:01:59 -08:00
Nikolaj Bjorner fd8fd40669 fix tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-20 08:00:01 -08:00
Christoph M. Wintersteiger d9beb9e15a Windows build fix 2015-11-20 09:57:05 +01:00
Christoph M. Wintersteiger 9175cf195d Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-19 23:27:24 +01:00