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

4941 commits

Author SHA1 Message Date
Nikolaj Bjorner 962979b09c rework sat.mus to use restart count for bounded minimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-26 13:28:40 -08:00
Nikolaj Bjorner 7386e2f3e9 add warning for scearios of #876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:29:30 -08:00
Nikolaj Bjorner 6e6c5935d7 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-25 18:09:37 -08:00
Nikolaj Bjorner 777091e653 fix part 1 of #875 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:09:27 -08:00
Nikolaj Bjorner 4782e19086 fix bug in sat-simplifier decreasing heap values of variables that are not in the heap 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 16:21:51 -08:00
Nikolaj Bjorner 60783e5696 fix regression for z3num 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 13:26:58 -08:00
Nikolaj Bjorner 4ec4abd7e3 fix test for int-value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-23 13:31:43 -08:00
Christoph M. Wintersteiger adf8072eaa Added option to limit the distance of unsat core extension through patterns. 2017-01-21 12:28:37 +00:00
Nikolaj Bjorner 1bfd09e16b Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-19 19:31:24 -08:00
Nikolaj Bjorner e23509797a access parameters from Python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-19 19:28:20 -08:00
Christoph M. Wintersteiger 5c1ffe13d1 x64 build fix for .NET 3.5 API 2017-01-18 13:06:28 +00:00
Christoph M. Wintersteiger 81c3a7dabd Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-18 12:32:10 +00:00
Christoph M. Wintersteiger a334020f2c Added .NET 3.5 solution/project files 2017-01-18 12:32:02 +00:00
Nikolaj Bjorner 16552d32cb Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-17 14:19:32 -08:00
Nikolaj Bjorner 0aa912371b Another fix for #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 14:19:24 -08:00
Nikolaj Bjorner 735998c386 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-17 13:41:25 -08:00
Nikolaj Bjorner 873d975c77 fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 13:41:15 -08:00
Christoph M. Wintersteiger 6d34899c46 Bugfix for macro finder. Fixes #832. 2017-01-17 15:44:03 +00:00
Christoph M. Wintersteiger e472a8d4cf Enabled filenames in error messages during inclusion of files. 2017-01-16 15:46:58 +00:00
Christoph M. Wintersteiger 090a331d79 Added filenames to error messages for when we have more than one file. 2017-01-16 15:43:13 +00:00
Christoph M. Wintersteiger 00a50eea7f Added (include ...) SMT2 command. 2017-01-16 15:05:58 +00:00
Nikolaj Bjorner dc543a7ee7 update macro_util logging to uniform format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 21:13:22 -08:00
Nikolaj Bjorner c4c9de0838 fix memory leaks from cancellations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 20:09:27 -08:00
Nikolaj Bjorner 24eae3f6e0 fix crash with unary xor #870 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 12:06:56 -08:00
Nikolaj Bjorner ee36662435 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-15 11:56:01 -08:00
Nikolaj Bjorner 7df803c131 Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 11:52:48 -08: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
Christoph M. Wintersteiger f1a4a48491 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-12 12:49:35 +00:00
Christoph M. Wintersteiger 2458db30cf Corner-case fix for smt::solver::pop_core 2017-01-12 12:49:26 +00:00
Daniel Perelman 3370adcdff Mark void DummyContracts as Conditional to avoid compiling their arguments. 2017-01-11 17:02:26 -08:00
Christoph M. Wintersteiger 650ea7b9cc Bugfix for smt.core.extend_patterns 2017-01-11 18:40:11 +00:00
Christoph M. Wintersteiger 9f49905582 Formatting, whitespace, and Z3_API annotations. 2017-01-10 21:05:27 +00:00
Christoph M. Wintersteiger d8d869822f Cleaned up #include<iostream> in api* objects. 2017-01-10 21:04:44 +00:00
Christoph M. Wintersteiger 384468bc99 Added option to extend unsat cores with literals that (potentially) provide quantifier instances. 2017-01-10 20:22:20 +00:00
Christoph M. Wintersteiger ba9d36605b Formatting, whitespace 2017-01-10 20:22:20 +00: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
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
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
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
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 189d449cff fix generation of wcnf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-18 14:49:45 -08: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
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
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 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
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