mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
6204 commits 23 branches 48 tags 157 MiB
Commit graph

6204 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Christoph M. Wintersteiger
8047f0d91a GCC compilation/keyword fix. Relates to #864 2017-01-10 14:06:56 +00:00
Christoph M. Wintersteiger
8f95ee01e1 Removed polynomial factorization test cases. Relates to #852 and fixes #865. 2017-01-10 14:02:59 +00: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
Nikolaj Bjorner
8d09b6e4a8 add at-least and pbge to API, fix for issue #864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-09 21:23:00 -08:00
Nikolaj Bjorner
c69a86e647 fix bug in antecedent collection for consequence finding: once an antecedent is set, it should not be cleared 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-06 19:34:50 -05:00
Nikolaj Bjorner
e9edcdc6e6 moderate exception behavior for issue #861 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-05 16:09:16 -05:00
Christoph M. Wintersteiger
447c97a783 Merge pull request #797 from delcypher/refactor_ocaml_generated_files 
Refactor OCaml generated file generation in preparation for CMake support
 2017-01-05 12:39:06 +01:00
Nikolaj Bjorner
f443bfed87 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-04 19:05:52 -08:00
Nikolaj Bjorner
ddf4bc548f allow disabling exceptions from C++. Issue #861 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-04 19:04:43 -08:00
Nikolaj Bjorner
ae9a3bfc24 add operator for issue #860 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-04 09:14:09 -08:00
Christoph M. Wintersteiger
cb75a55095 Fixed initialization order warning. 2017-01-03 13:41:08 +00:00
Nikolaj Bjorner
74d3de01b3 enable incremental consequence finding with restart timeout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-02 10:07:02 -08:00
Nikolaj Bjorner
a4d5c4a00a make get_consequence call skip check-sat if a model is already there 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-30 18:05:19 -08:00
Nikolaj Bjorner
8dde60f634 initialize watch in assign_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-26 10:18:55 -08:00
Nikolaj Bjorner
aaf6e67ec8 add restart.max parameter to control cancellation based on restart count 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:43:47 -08:00
Nikolaj Bjorner
2bd29548da improve parser error message over API, streamline names of statistics for arithmetic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:27:56 -08:00
Nikolaj Bjorner
c44dd01292 fix missing else reported in #855 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 20:56:14 -08:00
Nikolaj Bjorner
46df31babf Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-22 20:54:14 -08:00
Nikolaj Bjorner
1787fa8296 remove redundant disjunction in compilation of at-most-1 constraints, log mutexes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 20:54:09 -08:00
Nikolaj Bjorner
a444a33c30 updated encodings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 17:45:21 -08:00
Andrew Dutcher
1eec0799ca Add -fpic to armv7/armv8 build 2016-12-22 14:26:41 -08:00
Nikolaj Bjorner
f52baf1e17 fix build again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:48:43 -08:00
Nikolaj Bjorner
4bcf1bf2f6 fix debug build, unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:44:49 -08:00
Nikolaj Bjorner
df492e200f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:04:02 -08:00
Nikolaj Bjorner
8d18fd075e remove sources for unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 09:54:45 -08:00
Nikolaj Bjorner
7378362e81 Merge pull request #853 from delcypher/scoped_timer_linux_perf_fix 
Fix issue with bd1f07f864
 2016-12-21 09:13:00 -08:00
Dan Liew
b5aa6d5eb5 Fix issue with bd1f07f864 pointed out by 
@nunolopes .

If `pthread_cond_signal()` is called while `m_mutex` is held then the
timing thread might be woken up twice due to waking up from
`pthread_cond_timeout()` (due to being signaled) but then being forced
to sleep again because the thread calling `~imp()` is still holding
`m_mutex` (which the timing thread needs to acquire).
 2016-12-19 22:36:42 +00:00
Dan Liew
2e74a2c54e Refactor update_api.mk_ml() so that the source and output directories 
can be different. This feature will be needed by the CMake build system
to build the OCaml bindings.
 2016-12-19 21:05:17 +00:00
Dan Liew
76bbecf4fe Refactor mk_z3consts_ml() code into mk_z3consts_ml_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-12-19 21:05:17 +00:00
Dan Liew
0e03fe9bf2 Fix inconsistent emission of OCaml 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-12-19 21:05:16 +00:00
Christoph M. Wintersteiger
251d1ec031 Fix for parallel builds of the OCaml API. Relates to #797. 2016-12-19 16:58:25 +00:00
Christoph M. Wintersteiger
2c32e30fed Build fix for static binaries + shared examples 2016-12-19 16:47:28 +00:00
Nikolaj Bjorner
0c6c104f9a Merge pull request #841 from delcypher/scope_timer_spurious_wakes 
Make `scoped_timer` robust to spurious wakes under Linux.
 2016-12-19 08:22:03 -08:00
Nikolaj Bjorner
08f95bedf7 Merge pull request #849 from ColdHeat/master 
Making z3 python look in its installation directory for the z3 lib
 2016-12-18 15:47:01 -08:00
Nikolaj Bjorner
189d449cff fix generation of wcnf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-18 14:49:45 -08:00
Kevin Chung
e16577ff61 Making z3 python look in its installation directory for the z3 lib 2016-12-18 17:27:55 -05:00
Nikolaj Bjorner
5083b1adee Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-17 16:03:02 -08:00
Nikolaj Bjorner
5cb21924ad ensure that FD logic understands pb from command context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-17 16:02:54 -08:00
Christoph M. Wintersteiger
6ce903b1d6 Style, whitespace. 2016-12-16 20:04:29 +00:00
Christoph M. Wintersteiger
a1a662b23f Build fix for C/C++ example programs. 2016-12-16 04:51:07 -08:00
Nikolaj Bjorner
c1480b4389 handle model generation from issue #748. Deal with warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-12 00:40:52 +01:00
Dan Liew
bd1f07f864 Fix implementation of scoped_timer under Linux where it was 
incorrectly assumed that `pthread_cond_timedwait()` would exit
due to a condition variable being signaled or a timeout occuring.

According to the documentation `pthread_cond_timedwait()` might
spuriously wake so we introduce a new variable `m_signal_sent` (that is
guarded by an existing mutex) that is used as the variable to check that
the thread wake was not spurious.

This is intended to partially fix #839 .
 2016-12-11 23:12:36 +00: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
7cc093eee0 Add rewrite rule for property encoded in #812 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 11:05:12 +01:00
Nikolaj Bjorner
2307a7ffa7 fix bug in handling of repeated soft constraints. #815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 10:19:57 +01:00
Nikolaj Bjorner
0765eea486 add suggestions from #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 05:45:40 +01:00
Nikolaj Bjorner
70bb92d016 remove nested booleans during pre-processing. issue #837 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 05:16:31 +01:00
Nikolaj Bjorner
ff46a925a2 bail out on failure to properly project. issue #837 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 04:25:05 +01:00