3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Commit graph

5544 commits

Author SHA1 Message Date
martin-neuhaeusser
28f9c61d76 Include *.cmx files during installation of OCaml bindings.
The *.cmx files are now installed using ocamlfind. They contain information from the
compiler that can be used during optimization (the upcoming OCaml 4.03.0 issues
warning 58 if those files are missing from a package).
2016-03-28 17:08:22 +02:00
Dan Liew
c52c999393 [CMake] Document the `PYTHON_EXECUTABLE` CMake cache variable.
User's can use this to pick a different version of Python to use
for the build.
2016-03-27 15:04:22 +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
Dan Liew
6a2a8e06d7 [CMake] Declare uninstall rule before the components so that they
can add dependencies to the rule for their own custom uninstall
logic.
2016-03-26 17:59:11 +00:00
Dan Liew
23ac66ef42 Fix inconsistent emission of `Enumerations.cs`. 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-03-26 17:59:11 +00:00
Dan Liew
d3f87e44a2 Refactor `mk_z3consts_dotnet() code into mk_z3consts_dotnet_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-03-26 17:59:11 +00:00
Nikolaj Bjorner
0870b4a5a0 add length coherence check for length = 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-25 17:17:34 -07:00
Nikolaj Bjorner
f34a54fea0 fix stats collection over exceptions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-24 17:08:13 -07:00
Nikolaj Bjorner
808855ce6b add internalization for auxiliary division functions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-24 16:20:42 -07:00
Nikolaj Bjorner
709a5d9524 fix bug: & -> &&
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-24 16:09:12 -07:00
Nikolaj Bjorner
b30b8008b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-24 08:48:52 -07:00
Nikolaj Bjorner
29845d037b fix build break on seq evaluation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-24 08:48:42 -07:00
Nuno Lopes
83e34638e6 add support to build with MSVC /Gr (fastcall mode for x86)
not enabled by default nor exposed at the moment
2016-03-24 15:39:18 +00:00
Nikolaj Bjorner
89fad8913f fix issue #535
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-24 08:16:54 -07:00
Nikolaj Bjorner
05a784fa9e fix issue #535
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-24 08:16:19 -07:00
Nikolaj Bjorner
fe4f3e7772 fix regressions exposed in QF_LIA: manager got initialized early and Euclidean solver is not safe even with some throttle
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-23 20:38:18 -07:00
Nikolaj Bjorner
87989dd93e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-23 17:25:23 -07:00
Nikolaj Bjorner
45fdb95f53 fix performance for model construction, recognize concats of values as a value for pre-processing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-23 17:23:57 -07:00
Nikolaj Bjorner
8a4624e21f Merge pull request #531 from seahorn/qearrays
extend model with the value of a fresh variable
2016-03-23 16:54:16 -07:00
Arie Gurfinkel
4e7b6b6586 proposed fix to compare 2016-03-23 19:20:57 -04:00
Arie Gurfinkel
ee125b4fe3 extend model with the value of a fresh variable 2016-03-23 19:07:50 -04:00
Nikolaj Bjorner
96f113afee Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-23 10:19:25 -07:00
Nikolaj Bjorner
ec681d7565 some of Arie's fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-23 10:19:16 -07:00
Christoph M. Wintersteiger
7e02c8f82a Merge pull request #528 from EinNarr/master
Clean up README
2016-03-23 16:50:51 +00:00
Bohao Zhang
749e1a1fb1 Clean up README
mentioning C++ and Java.
2016-03-23 16:14:38 +01:00
Christoph M. Wintersteiger
5af5549a56 Merge pull request #527 from tabe/examples-typo
Fix typo in examples/*/README
2016-03-23 12:41:14 +00:00
Takeshi Abe
5c2969c0f0 Fix typo 2016-03-23 12:51:41 +09:00
Nikolaj Bjorner
fd6fe87c5d enable qe-lite for UFNIA benchmarks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-22 15:41:21 -07:00
Christoph M. Wintersteiger
4badc52dc3 Merge pull request #526 from bpowers/_build
build: allow overriding of 'ar' in mk_config
2016-03-22 15:05:55 +00:00
Christoph M. Wintersteiger
8bcac82658 Merge branch 'master' of https://github.com/Z3Prover/z3
# Conflicts:
#	CMakeLists.txt
2016-03-22 15:04:48 +00:00
Christoph M. Wintersteiger
38fc49a05d Merge branch 'delcypher-cmake_fix_enable_tracing_in_debug_mode' 2016-03-22 15:02:40 +00:00
Bobby Powers
7bb085a565 build: allow overriding of 'ar' in mk_config
This will still use 'ar' if AR isn't set in the environment, but lets
us override the default archive tool at configure time.

Just like CC and CXX, this doesn't apply to a ./configure for Windows.
2016-03-22 10:47:51 -04:00
Nikolaj Bjorner
72ec6dc8e1 remove debug code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-21 16:58:48 -07:00
Nikolaj Bjorner
5e737641b7 remove qe-lite pass in quant_tatics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-21 16:57:30 -07:00
Nikolaj Bjorner
701f32471e hardening model checker code against cancellations'
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-21 15:04:20 -07:00
Dan Liew
d3afdc957b [CMake] Fix issue #522
Previously tracing could be disabled and was not enabled by default in a
debug build. This isn't desirable but I had avoided fixing it because
enabling tracing in debug mode would be confusing because
``ENABLE_TRACING`` could be set to off but tracing would be enabled
anyway.

I have resolved this by renaming the option from ``ENABLE_TRACING`` to
``ENABLE_TRACING_FOR_NON_DEBUG``. The semantics of the optiona are now
that it will enable tracing in non-debug builds. I have also added code
to ensure that tracing is always enabled in debug builds.

Whilst I was here I also fixed how ``option()`` was being used. The
default value and comment were in the wrong order.
2016-03-21 19:37:33 +00:00
Nikolaj Bjorner
3dc2028925 adding min/max
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-21 09:20:57 -07:00
Nikolaj Bjorner
680c28d083 remove nnf conversion which breaks NRA property
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-20 16:34:04 -07:00
Nikolaj Bjorner
1a5449c3d4 enable new NRA solver for nra benchmarks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-20 12:35:29 -07:00
Nikolaj Bjorner
73e29c6ee6 fix regression warning on invalid case split strategy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-20 10:20:43 -07:00
Nikolaj Bjorner
92b5aac12a adjusting new tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-20 10:13:23 -07:00
Nikolaj Bjorner
b66fc4e355 Merge pull request #523 from delcypher/fix_no_kind_namespace
Fix gcc build broken by f175f864ec.
2016-03-20 10:12:14 -07:00
Dan Liew
971fd59fbb Fix gcc build broken by f175f864ec.
C++ enums (unless they are class enums) don't define their own
namespace.
2016-03-20 10:18:59 +00:00
Nikolaj Bjorner
f0bdcbb3db expose qsat tactic to default tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 18:40:59 -07: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
Nikolaj Bjorner
d614fedde2 more merges with qsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 12:41:41 -07:00
Nikolaj Bjorner
76d637626a include more qsat features
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 12:30:24 -07:00