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

6270 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner 99b7c26e9f exposing regular expression features to address issue #831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 13:05:02 +01:00
Nikolaj Bjorner 8e6600c6be add python API for newly exposed regex constructors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 09:09:03 +01:00
Nikolaj Bjorner 976fadf771 add missing complement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:21:57 +01:00
Nikolaj Bjorner 0473d2ef56 add regular expression features to C# API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:17:13 +01:00
Nikolaj Bjorner a82b5e21fe add regular expression operations to C and C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:11:36 +01:00
Nikolaj Bjorner 4e25bffab6 add range constructor to .NET API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-08 18:33:02 +01:00
Nikolaj Bjorner feb801564b adding range to C API. Issue #831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-08 18:28:27 +01:00
Christoph M. Wintersteiger dc0d29a00c Bugfix for model construction. Fixes #828. 2016-12-08 16:14:54 +00:00
Wensheng Tang 99d10d1224 Fixed utf-8 version string handling for python2. Resolved #787 2016-12-08 15:09:59 +08:00
Christoph M. Wintersteiger f1a704484b Re-added context creation locks in the Java API. Relates to #819. 2016-12-01 23:16:15 +00:00
Nuno Lopes dedae29300 add a few more statics to avoid symbol clashes 2016-12-01 17:37:07 +00:00
Nuno Lopes e697d3e810 remove 2 outdated comments 2016-12-01 14:10:31 +00:00
Nuno Lopes 42b26c63e5 make a few functions static 2016-12-01 14:01:20 +00:00
Nikolaj Bjorner 7ebc660b6d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-30 09:52:15 -08:00
Nikolaj Bjorner 024082a45f adding preferred sat, currently disabled, to wmax. Fixing issue #815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-30 09:52:05 -08:00
Nikolaj Bjorner d9227b95ea blast distinct in incremental BV solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-29 15:45:23 -08:00
Nuno Lopes 4b4365470d mam compiler: move reset of matched_exprs cache next to code reset 2016-11-28 15:40:25 +00:00
Nuno Lopes 2babd192b8 small optimization in compilation of multi-patterns 
also make the path faster for single patterns
 2016-11-28 14:43:47 +00:00