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

6153 commits

This branch
This branch
All branches
Author SHA1 Message Date
Dan Liew ac85c68ccb [CMake] Fix examples linking against libz3 when it is built as a 
static library on Linux.
 2017-03-13 11:53:33 +00:00
Dan Liew b20bf5169a [CMake] Fix typo handling OpenMP flags. 2017-03-13 11:53:33 +00:00
Dan Liew db5520c71d [CMake] Build c_example, cpp_example and z3_tptp5 as external 
projects.

This works by giving each example it's own CMake build system and
then consuming Z3 via the Z3 CMake config package from the build
tree.
 2017-03-13 11:53:33 +00:00
Dan Liew d9617841e0 [CMake] Python examples should only be copied over if python bindings 
are being built.
 2017-03-13 11:53:33 +00:00
Dan Liew 73614abf37 [CMake] Implement generation of Z3Config.cmake and Z3Target.cmake 
file for the build and install tree.

These files allow users of CMake to use Z3 via a CMake config package.
Clients can do `find_package(Z3 CONFIG)` to get use the package from
their projects.

When generating the files for the install tree we try to generate
the files so that they are relocatable so that it shouldn't matter
if the installed files aren't in the CMAKE_INSTALL_PREFIX when
a user consumes them. As long as the relative locations of the files
aren't changed things should still work.

A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been
added so that the install location of the Z3 CMake package files can be
controlled.

This addresses #915 .
 2017-03-13 11:53:27 +00:00
Nikolaj Bjorner e2933350b2 Merge pull request #937 from delcypher/cmake_git_version 
[CMake] Support including Git hash and description into the build.
 2017-03-12 23:36:21 +01:00
Dan Liew 2cb4223979 [CMake] Support including Git hash and description into the build. 
CMake will automatically pick up changes in git's HEAD so that
the necessary code is rebuilt when the build system is invoked.

Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been
added that enable/disable including the git hash and the output of `git
describe` respectively. By default if the source tree is a git
repository both options are on, otherwise they are false by default.

To support the `Z3GITHASH` macro a different implementation is used from
the old build system. In that build system the define is passed on the
command line. This would not work well for CMake because CMake
conservatively (and correctly) rebuilds *everything* if the flags given
to the compiler change. This would result in the entire project being
rebuilt everytime git's `HEAD` changed.  Instead in this implementation
a CMake specific version of `version.h.in` (named `version.h.cmake.in`)
is added that uses the `#cmakedefine` feature of CMake's
`configure_file()` command to define `Z3GITHASH` if it is available and
not define it otherwise. This way only object files that depend on
`version.h` get re-built rather than the whole project.

It is unfortunate that the build systems now have different `version.h`
file templates. However they are very simple and I don't want to
modify how templates are handled in the python/Makefile build system.
 2017-03-12 22:11:59 +00:00
Nikolaj Bjorner 1f4f4514bf Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-12 09:40:58 +01:00
Nikolaj Bjorner 8bec1e25a8 move restore relevancy until after literals have been replayed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-12 08:32:06 +01:00
Nikolaj Bjorner 7272d3f480 Merge pull request #936 from jamesbornholt/z3py-with 
z3py: With tactical should not try to use context as a parameter
 2017-03-12 08:25:53 +01:00
James Bornholt 559c5e5ae6 z3py: With tactical should not try to use context as a parameter 2017-03-11 16:09:25 -08:00
Nikolaj Bjorner 228111511c fixing build break, addressing #935 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-11 18:41:36 +01:00
Nikolaj Bjorner 509f7409ba adding fixedpoint object to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-10 23:01:43 +01:00
Nikolaj Bjorner 338193548b fixing build break, adding fixedpoint object to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-10 22:52:55 +01:00
Nikolaj Bjorner fbf81c88a2 remove print breaking build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 11:13:38 +01:00
Nikolaj Bjorner abdd982cea Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-08 21:41:43 -08:00
Nikolaj Bjorner 854bb2197f include recursive functions to models. Issue #898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-08 21:41:24 -08:00
Nikolaj Bjorner 7b727fc725 remove scratch notes from readme 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 06:37:56 +01:00
Nikolaj Bjorner 6f68355fbc Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-08 21:33:43 -08:00
Nikolaj Bjorner e34996fa9d add notes to README based on feedback in #916 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 06:00:34 +01:00
Nikolaj Bjorner 29969648ba check that formulas are in lira before invoking qsat. Issue #919 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 05:52:46 +01:00
Nikolaj Bjorner fcda4cee9f ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 05:29:56 +01:00
Nikolaj Bjorner 829519b837 fix bug for bit-vector optimization. Issue #928 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-08 10:19:35 +01:00
Nikolaj Bjorner b9d9e8ef06 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-08 10:10:50 +01:00
Nikolaj Bjorner 202ac0d1ee Merge branch 'master' of https://github.com/Z3Prover/z3 
:wi
 2017-03-08 10:08:54 +01:00
Nikolaj Bjorner ec86cd8357 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-08 10:07:40 +01:00
Nikolaj Bjorner 41e6fafc58 fix bug for bit-vector optimization. Issue #919 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-08 10:07:31 +01:00
Christoph M. Wintersteiger b57764800c Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-07 18:10:31 +00:00
Christoph M. Wintersteiger 8f14cfadd2 Tabs, whitespace 2017-03-07 18:10:03 +00:00
Nikolaj Bjorner 91eddecd6e Merge pull request #927 from mtrberzi/zstring-patch 
Add boolean operators and stream<< to zstring
 2017-03-04 12:29:52 -08:00
Murphy Berzish ad0766898c add boolean operators to zstring and fix ostream 2017-03-04 15:20:57 -05:00
Christoph M. Wintersteiger c1d0e200c7 Merge pull request #925 from delcypher/cmake_validate_build_type 
[CMake] Validate CMAKE_BUILD_TYPE
 2017-03-03 13:52:27 +00:00
Dan Liew cac0283e7d [CMake] For single configuration generators only allow 
`CMAKE_BUILD_TYPE` to be one of the pre-defined build configurations
that we support.
 2017-03-02 21:18:54 +00:00
Christoph M. Wintersteiger 075a56ef02 Merge pull request #924 from cheshire/fix_jni_string_leak 
Free allocated char arrays in JNI API
 2017-03-01 18:32:54 +00:00
Christoph M. Wintersteiger b22c83ea66 Merge pull request #923 from mlr-msft/master 
Fixed bug in `mk_make.py --build=`...
 2017-03-01 18:29:40 +00:00
George Karpenkov dbdb0307db Free allocated char arrays in JNI API 
Fixes #886
 2017-03-01 15:22:15 +01:00
Michael Lowell Roberts 3415672f31 fixed bug where mk_make.py --build=... would fail to handle absolute paths correctly. 2017-02-28 08:24:35 -08:00
Nikolaj Bjorner 4792229c2b Merge pull request #922 from mtrberzi/regex-unroll 
add _re.unroll internal operator to seq_decl_plugin
 2017-02-27 18:37:37 -08:00
Nikolaj Bjorner f8a3a46d44 Merge pull request #921 from cheshire/obj_value_as_vector_java 
Obj value as vector java
 2017-02-27 09:53:23 -08:00
George Karpenkov be1e9918f0 Class Optimize#Handle should be static, 
as it already includes an explicit reference to the Optimize class.
 2017-02-27 18:49:02 +01:00
George Karpenkov b3be83e7c5 Sane indentation + removing extra spaces for Optimize.java 2017-02-27 18:48:44 +01:00
George Karpenkov d6c79facc7 Java API for getting the objective value as a triple 
See #911 for the motivation,
and e02160c674 for the relevant change
in C API.
 2017-02-27 18:42:44 +01:00
Nikolaj Bjorner 899843b7cd fix unhandled finite domain sort rewrite case. Issue #918 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-26 17:20:54 -08:00
Nikolaj Bjorner 996c0f0666 fix type on exception message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-25 16:14:50 -08:00
Nikolaj Bjorner c7591e3c99 remove unreferenced label 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-24 11:13:08 -08:00
Nikolaj Bjorner 183ee7e37d expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-24 11:10:18 -08:00
Nikolaj Bjorner e02160c674 expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-24 11:07:40 -08:00
Nikolaj Bjorner 8437cb7132 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-24 07:54:25 -08:00
Murphy Berzish 0ebd93c8b5 add _re.unroll internal operator to seq_decl_plugin 2017-02-23 20:57:19 -05:00
Nikolaj Bjorner e744d0f271 Merge pull request #910 from mtrberzi/octal-escape 
Add C-style octal escape sequences to seq_decl_plugin
 2017-02-23 16:02:21 -08:00