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

84 commits

Author SHA1 Message Date
Christoph M. Wintersteiger 9a757ffffe Result ordering fix for qprofdiff 2017-04-07 18:12:33 +01:00
Christoph M. Wintersteiger 23f4a0c332 Build fix for qprofdiff 2017-04-07 18:12:26 +01:00
Christoph M. Wintersteiger f3c990d356 Fixes for qprofdiff 2017-04-07 18:12:16 +01:00
Christoph M. Wintersteiger d390885757 Added utility to compare quantifier instantiation profiles generated via smt.qi.profile=true 2017-04-06 18:37:29 +01:00
Dan Liew 28493622c2 [CMake] On Windows when building the examples copy the Z3 library 
into the directory of the example executable so that it works "out
of the box".
 2017-03-13 12:37:29 +00:00
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 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
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
Christoph M. Wintersteiger c5fe591dbc Merge pull request #739 from angr/fix/soname_version 
Set soname version correctly in cmake build
 2017-02-04 20:39:50 +00:00
Christoph M. Wintersteiger c56edc63d2 Merge pull request #882 from dwoos/sine-filter 
Add basic Sine Qua Non filtering
 2017-02-04 20:24:09 +00:00
Nikolaj Bjorner 37ee4c95c3 adding parallel threads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 02:09:08 -08:00
Doug Woos a9d61d48ae Add basic Sine Qua Non filtering 2017-01-27 11:22:39 -08:00
Christoph M. Wintersteiger 625681f82f Updated cmake build 2017-01-16 15:59:16 +00:00
Nikolaj Bjorner bc6b3007de remove unused features related to weighted check-sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-13 20:53:22 -08:00
Nikolaj Bjorner dda1774fa1 update CMakeList to remove polynomial-factorization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-10 08:21:49 -08:00
Nikolaj Bjorner 331658f208 remove polynomial factorization as suggested by issue #852 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-09 21:30:54 -08:00
Andrew Dutcher 657b0de2fc cmake build: set SOVERSION to include the minor version number 2016-12-11 08:27:35 -08:00
Andrew Dutcher aca3d0545c Set soname version correctly in cmake build 2016-12-11 08:22:24 -08:00
Nikolaj Bjorner ea601dd403 fix and coallesce clique functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 03:55:48 -08:00
Nikolaj Bjorner 51a4085910 check for logic in solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-04 15:19:11 +00:00
Nikolaj Bjorner fa1a0aa7ba remove buggy and unused equivalence relation plugin. Github issue #770 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-31 22:59:56 +01:00
Nikolaj Bjorner 461e88e34c additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-25 20:32:13 -07:00
Nikolaj Bjorner 3778048eb4 add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:31:59 -07:00
Nikolaj Bjorner d060359f01 add fd solver for finite domain queries 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-18 22:34:34 -04:00
Dan Liew 289e51f455 [CMake] Fix building the Java bindings. 
This was broken due to 495ef0f055
and a914822346 adding and removing
source files without updating the CMake build.
 2016-10-17 18:30:49 +01:00
Dan Liew 462d3e8e8b [CMake] Unbreak building the .NET bindings. 
7fefe40f21 broke building the .NET
bindings by renaming the signing key without updating the CMake build.
 2016-10-17 18:19:31 +01:00
Dan Liew 03071db3ed [CMake] Fix building the examples when libz3 is built as a static library. 2016-10-17 18:19:31 +01:00
Dan Liew 4ef55505e7 [CMake] Fix #763 reported by @jirislaby. 
`INTERFACE` was the not appropriate usage requirement to use. However
it only caused a problem when USE_LIB_GMP was enabled. With `INTERFACE`
`-lgmp` was not specified on the link line so `libz3.so` did not have a
reference to the library and linking against `libz3.so` by clients
would fail with missing references to symbols in `libgmp`.
 2016-10-17 18:19:25 +01:00
Christoph M. Wintersteiger 12c47348bc Merge pull request #761 from delcypher/bv2fpa_unbreak_cmake_build 
Unbreak the CMake build broken by 009af4455d
 2016-10-17 11:47:01 +01:00
Nikolaj Bjorner aec59e4ff7 add consequence finding to inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-16 15:43:28 -04:00
Dan Liew b2381acceb Unbreak the CMake build broken by 009af4455d 
The commit added an additional source file and dependency but the
corresponding changes weren't added to the CMake build.
 2016-10-15 21:42:20 +01:00
Nikolaj Bjorner cf56da8482 add z3test to cmakelists.txt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 16:33:30 -07:00
Nikolaj Bjorner 14668b4d44 Merge pull request #735 from angr/new-build 
New packaging for and ability to distribute python bindings
 2016-09-21 15:55:22 -07:00
Andrew Dutcher f451363a8f use copy instead of create_symlink when not on unix 2016-09-21 15:15:21 -07:00
Nikolaj Bjorner 7f29674842 add option to bypass compression of unbound tails, issue #738 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-16 14:56:10 -07:00
Andrew Dutcher 9e498536b6 Fix cmake build to work with the new system 2016-09-15 02:19:20 -07:00
Andrew Dutcher 0bbd172af3 First steps to a sane python build 2016-09-14 01:37:04 -07:00
Nikolaj Bjorner 8221a09659 fast path for antecedent extraction in smt_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 16:49:19 -07:00
Nikolaj Bjorner 083939ab0e add tactic to eliminate enumeration sorts in favor of bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-23 14:11:21 -07:00
Nikolaj Bjorner 9ed2c846a9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-21 18:19:10 -07:00
Nikolaj Bjorner 3581f6de42 remove stale SLS option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-21 18:18:42 -07:00
Nikolaj Bjorner 16e3a91bdf fix issues reported by Geoff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-21 07:56:21 -07:00
Nikolaj Bjorner 1073e161c7 remove deprecated max-sat solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 19:08:23 -07:00
Nikolaj Bjorner f3d657ebd1 add tptp5 example to cmake, adding output SZS directives for Geoff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-15 12:09:23 -07:00
Nikolaj Bjorner 16ad33bf39 add collection of statistics #652 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-13 18:17:49 -07:00
Nikolaj Bjorner 9f5a117443 move mus to solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-10 16:24:14 -07:00
Nikolaj Bjorner 6aa6102891 factor out model-based-opt code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-27 15:08:10 -07:00
Nikolaj Bjorner 68c7d64d00 adding model-based opt facility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-27 11:18:20 -07:00