mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Code Activity
5198 commits 23 branches 48 tags 156 MiB
Commit graph

5198 commits

This branch
This branch
All branches
Author SHA1 Message Date
Dan Liew 49c92e4bd7 [CMake] Add a note about the name of the Z3 Java `.jar` file. 2016-04-18 15:33:19 +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 48550732bf [CMake] Add a few notes on finding the Java installation. 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
Dan Liew 3042f0f964 Fix inconsistent emission of Java enumeration files. The ordering of emitted 
enum values is not consistent between python 2 or 3. The root cause
of the problem was a dictionary's keys being iterated over which has
no defined order.

This has been fixed by iterating over the dictionary's items and
ordering by values.  We could order by key rather than the values but
seeing as these represent an enum, ordering by value makes more sense.
 2016-04-17 19:03:17 +01:00
Dan Liew b3713e7496 Refactor `mk_z3consts_java() code into mk_z3consts_java_internal()` 
and move that into ``mk_genfile_common.py``. Then adapt ``mk_util.py`` and
``mk_consts_files.py`` to call into the code at its new location.

The purpose of this change is to have Python code common to the Python
and CMake build systems separate from Python code that is only used for
the Python build system.
 2016-04-17 19:03:17 +01:00
Christoph M. Wintersteiger 14e1e247a4 Revert "nmake->make, little error" 
This reverts commit 8287f7ba82.
 2016-04-17 11:35:27 +01:00
Nikolaj Bjorner 7a317a4f07 Merge pull request #566 from xavdel/patch-1 
nmake->make, little error
 2016-04-16 17:46:04 -07:00
Xavier DELPIERRE 8287f7ba82 nmake->make, little error 2016-04-17 02:39:35 +02:00
Nikolaj Bjorner 0094b36636 fix bounds check to fix segfault reported in issue #565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 12:25:29 -07:00
Nikolaj Bjorner 1c8e0918d8 move to std::vector in replayer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 10:08:29 -07:00
Nikolaj Bjorner d383fd851a move vector<std::string to std::vector<std::string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 09:34:27 -07:00
Nikolaj Bjorner 4ebf392da7 Fixes #564: use std::vector on std::strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 09:26:13 -07:00
Nikolaj Bjorner 0f93853a4c remove labels from evaluation result 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-12 13:17:10 -07:00
Nikolaj Bjorner aa7b5d80fe extract array terms for evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-12 09:41:50 -07:00
Nikolaj Bjorner 2033719c14 fix optimization pre-processing reported by Gereon Kremer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-09 20:58:57 -07:00
Nikolaj Bjorner 6e57015a12 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-09 16:51:42 -07:00
Nikolaj Bjorner cc6f72aba7 fix handing of ite conditions that have to be included in projection, thanks to bug report by Zak 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-10 01:48:35 +02:00
Christoph M. Wintersteiger 16e487b32a Bugfix for ackermann helper 2016-04-08 17:20:09 +01:00
Christoph M. Wintersteiger bd0bd08ecf add is_considered_uninterpreted checks into acker_helper 2016-04-08 16:58:11 +01:00
Christoph M. Wintersteiger 0597b579b1 Bugfixes for bvarray2uf conversion. 2016-04-07 19:10:31 +01:00
Christoph M. Wintersteiger 5971c20653 Bugfixes for bv_trailing. 2016-04-07 13:08:17 +01:00
Christoph M. Wintersteiger 3a532c08a6 Bugfix for func_interp else-case compression 2016-04-06 19:24:08 +01:00
Christoph M. Wintersteiger e662427060 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 15:39:37 +01:00
Christoph M. Wintersteiger e527aca296 Bugfix for unspecified else-case in func_interps. 2016-04-06 15:39:32 +01:00
Nuno Lopes e2b7ad246a bv_trailing: fix compiler warning + use of ast_manager 2016-04-06 15:34:31 +01:00
Christoph M. Wintersteiger 7534b53bae Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 14:51:25 +01:00
Christoph M. Wintersteiger 86ca224460 Merge pull request #554 from MikolasJanota/trailing 
Trailing
 2016-04-06 14:25:58 +01:00
Mikolas Janota 7ad9dec6c2 Adding cpp files for bv_trailing to CMakeLists. 2016-04-06 11:04:17 +01:00
Mikolas Janota dbffc15b98 Improvements in caching of bv_trailing. 2016-04-06 11:04:15 +01:00
mikolas 9ba5bbfd33 Re-factoring and comments in bv_trailing. 2016-04-06 11:04:13 +01:00
Mikolas Janota 248feace34 fixing the behavior in bv_trailing 2016-04-06 11:04:11 +01:00
mikolas fced47386e More work on trailing 0 analysis. 2016-04-06 11:04:09 +01:00
mikolas ddb6ae4eab More work on trailing 0 analysis. 2016-04-06 11:04:07 +01:00
mikolas 78cb1e3c7b More work on trailing 0 analysis. 2016-04-06 11:04:05 +01:00
mikolas c7f1746321 Starting to work on trailing 0 analysis. 2016-04-06 11:04:03 +01:00
Nikolaj Bjorner 493b86eca7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-05 22:27:11 +02:00
Nikolaj Bjorner b97d694e5e undo model evaluation to BR_FULL pending regression in assertion violation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-05 22:26:57 +02:00
Christoph M. Wintersteiger efd923b826 Merge pull request #552 from MikolasJanota/bug_fix 
Avoiding adding spurious +0 in poly_rewriter::cancel_monomials.
 2016-04-05 19:06:19 +01:00
mikolas 05ce886afe Avoiding adding spurious +0 in poly_rewriter::cancel_monomials. 2016-04-05 17:26:48 +01:00
Nikolaj Bjorner c454b81b2c special case branching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-05 11:57:49 +02:00
Nikolaj Bjorner ed1a5797fb check that a clause was not removed to fix issue #551 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-04 20:15:49 +02:00
Nikolaj Bjorner ec5a4ba63d add documentation comment for evaluation, Issue #536 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-04 12:59:18 +02:00
Nikolaj Bjorner 9667185af0 issue #549, replace BoolVal by False, otherwise creates regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-03 12:53:50 +02:00
Nikolaj Bjorner 11e8f06272 issue #549, replace False by BoolVal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-03 12:52:15 +02:00
Nikolaj Bjorner 33e7640645 disable mb branching pending unit test analysis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-03 10:53:37 +02:00
Nikolaj Bjorner 03336ab9f2 add evaluation of array equalities to model evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-02 15:07:01 +02:00