3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Commit graph

5085 commits

Author SHA1 Message Date
Dan Liew
140b3de3aa Make warnings that are emitted when installing Python bindings outside
the install prefix on OSX less aggressive by not stating that this might
lead to a broken install (even though it might!).

Also emit a similar warning during the configuration step.

This partially addresses #361
2015-12-12 19:30:24 +00:00
Nikolaj Bjorner
32be23fdaa fix index into reversed contains semantics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 19:30:24 +00:00
Nikolaj Bjorner
267a1e962c moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 19:30:24 +00:00
Nikolaj Bjorner
d4a90d7ec3 moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 19:30:24 +00:00
Nikolaj Bjorner
a9723fb6c7 reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 19:30:23 +00:00
Nikolaj Bjorner
9769322690 reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 19:30:23 +00:00
Nikolaj Bjorner
e08bfb62f8 moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 19:30:23 +00:00
Nikolaj Bjorner
589626b738 moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 19:30:23 +00:00
Nikolaj Bjorner
f2f9578c0a cleanup cancelation logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 19:30:22 +00:00
Christoph M. Wintersteiger
325d516825 ocaml build fix 2015-12-12 19:30:22 +00:00
Christoph M. Wintersteiger
02f7ae4a4d updated ocaml build and installation 2015-12-12 19:30:22 +00:00
Nikolaj Bjorner
3ff7283f94 Merge pull request #373 from NikolajBjorner/master
revamp cancellation logic
2015-12-12 10:34:13 -08:00
Nikolaj Bjorner
2ecbe26be1 ensure limit children are safe for race conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 10:24:19 -08:00
Nikolaj Bjorner
54ac71cada ensure limit children are safe for race conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 10:23:56 -08:00
Nikolaj Bjorner
4132fc2d91 ensure limit children are safe for race conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 10:18:51 -08:00
Nikolaj Bjorner
f8a804ba56 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-12 09:44:20 -08:00
Nikolaj Bjorner
2a051719d8 cleanup deprecated critical sections, fix cancellation for par_or_else tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 09:43:00 -08:00
Christoph M. Wintersteiger
bb55744fc0 Merge pull request #374 from delcypher/less_agressive_out_of_install_prefix_warnings
Make warnings when installing Python bindings on OSX that are outside the install prefix less aggressive
2015-12-12 16:01:19 +00:00
Dan Liew
f9687e780a Link to the release notes in `README.md` 2015-12-12 11:50:38 +00:00
Dan Liew
b4dd5d3d08 Rewrite intro text in `README.md`. 2015-12-12 11:46:02 +00:00
Dan Liew
560810ee67 Fix command line indent in `README.md` 2015-12-12 11:33:32 +00:00
Dan Liew
2947893e10 Partially document the Z3 bindings in `README.md` 2015-12-12 11:32:33 +00:00
Dan Liew
2bd9bbafe4 Re-organise the discussion of Clang, it is not a second class citizen
and so doesn't deserve to be stuck at the end of the README. It also
**does** support OpenMP!
2015-12-12 10:31:12 +00:00
Dan Liew
f09fa3c87b Recent changes to the build system mean that setting a custom
``--prefix=`` is likely to disable installing the Python bindings so
the old instructions aren't helpful. Reword them and mention using
``DESTDIR``.
2015-12-12 10:22:56 +00:00
Dan Liew
08610ae243 Correct incorrect information on what `PREFIX is in README.md`.
It isn't always the root of the Python install.
2015-12-12 10:06:10 +00:00
Dan Liew
68247aa58f Convert README to markdown 2015-12-12 10:01:27 +00:00
Dan Liew
948df47027 Make warnings that are emitted when installing Python bindings outside
the install prefix on OSX less aggressive by not stating that this might
lead to a broken install (even though it might!).

Also emit a similar warning during the configuration step.

This partially addresses #361
2015-12-12 09:34:50 +00:00
Nikolaj Bjorner
c97db1722d fix index into reversed contains semantics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 22:00:01 -08:00
Nikolaj Bjorner
9c597e9eea Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-11 17:47:03 -08:00
Nikolaj Bjorner
521271e559 moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 17:46:22 -08:00
Nikolaj Bjorner
1aea9722cb moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 16:56:23 -08:00
Nikolaj Bjorner
96d1066c6a reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 16:43:48 -08:00
Nikolaj Bjorner
baee4225a7 reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 16:21:24 -08:00
Nikolaj Bjorner
981f8226fe moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 13:36:47 -08:00
Nikolaj Bjorner
32b6b2da44 moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 13:13:11 -08:00
Nikolaj Bjorner
61dbb6168e cleanup cancelation logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 12:35:35 -08:00
Christoph M. Wintersteiger
f164f17190 ocaml build fix 2015-12-11 20:01:55 +00:00
Christoph M. Wintersteiger
50f17e403c updated ocaml build and installation 2015-12-11 19:56:23 +00:00
Nuno Lopes
39ca5480d7 ensure that formula is skolemized in the smt solver when using MBQI
Reviewed by Nikolaj

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-12-11 18:18:09 +00:00
Nuno Lopes
ef06da8c2c fix build with gcc 2015-12-11 18:14:14 +00:00
Christoph M. Wintersteiger
3388e1e628 Removed superfluous file. 2015-12-11 18:00:38 +00:00
Christoph M. Wintersteiger
8fef9e57c5 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-11 17:52:12 +00:00
Nikolaj Bjorner
4e155887b2 consolidate cancellation to context check_cancel_flag instead of calling in set_cancel()
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 09:51:43 -08:00
Christoph M. Wintersteiger
ea353d77e9 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-11 17:48:50 +00:00
Christoph M. Wintersteiger
12ee1d342c Improved argument validation in FP API.
Fixes #372
2015-12-11 17:48:40 +00:00
Nikolaj Bjorner
ee4ed1749a add cancel checks in model finder, patch by Sarah Winkler
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 09:09:25 -08:00
Nikolaj Bjorner
aa415f3d58 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-11 08:37:55 -08:00
Nikolaj Bjorner
85b9bb3cc6 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 08:37:47 -08:00
Christoph M. Wintersteiger
b25f517a89 Bugfix for C++ API.
Fixes #371.
2015-12-11 14:03:41 +00:00
Christoph M. Wintersteiger
cc8e685f45 whitespace 2015-12-11 14:03:24 +00:00