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

6138 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner 20790c46ee bail out on failure to properly project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 04:23:07 +01:00
Nikolaj Bjorner 32c63ce4cd address other warnings per input from delcypher 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 17:23:59 +01:00
Nikolaj Bjorner 6594c3a046 add virtual destructor to intermediary class in case this helps for #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 13:58:39 +01:00
Nikolaj Bjorner dea3b8ddf7 address warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 13:14:36 +01:00
Nikolaj Bjorner 8e078cf9e2 address #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 07:52:00 +01:00
Nikolaj Bjorner fe10f2d244 address #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 07:51:16 +01:00
Nikolaj Bjorner 0ef14ffa08 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 23:18:02 +01:00
Nikolaj Bjorner e092232f67 add virtual destructors, fix operator code for API methods complement and intersection per note by Loris d'Antoni 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 23:17:52 +01:00
Christoph M. Wintersteiger 649d474686 Build fix for C++ example 2016-12-09 19:09:47 +00:00
Christoph M. Wintersteiger 4c664f1c05 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 15:03:36 +00:00
Christoph M. Wintersteiger 16b32ecf12 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.

(+reversed accidental debug code commit).
 2016-12-09 15:03:31 +00:00
Nikolaj Bjorner a17e957362 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 15:32:26 +01:00
Nikolaj Bjorner acba529bce fix bug in encoding of axioms for indexof. Issue #806 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 15:32:15 +01:00
Christoph M. Wintersteiger 56b1a8b086 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.
 2016-12-09 13:43:05 +00:00
Christoph M. Wintersteiger 9df5c31485 Whitespace 2016-12-09 13:40:46 +00:00
Nikolaj Bjorner 0ab2067b69 produce error message for cores with optimization. Issue #825 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 13:15:40 +01:00