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

937 commits

Author SHA1 Message Date
Nikolaj Bjorner
ee07008fb9 import files from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:04:46 -08:00
Nikolaj Bjorner
e954f59052 ensure that solver objects have timeout/rlimit/ctrl-c exposed as possible parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 13:50:17 -08:00
Bruce Mitchener
d757c342d5 Define NO_Z3_DEBUGGER for emscripten builds. 2019-01-07 23:13:09 +07:00
Nikolaj Bjorner
2486971094
Merge pull request #2065 from waywardmonkeys/improve-ios-support 
Define NO_Z3_DEBUGGER for iOS builds.
 2019-01-06 18:56:03 -08:00
Bruce Mitchener
7e1ce2a16c Define NO_Z3_DEBUGGER for iOS builds. 
This is defined because we can't call `system` (via `invoke_gdb`)
on iOS and related platforms.
 2019-01-06 12:16:33 +07:00
Bruce Mitchener
a06bc49710 Let str_hashtable store const char*. 
This removes some boilerplate const casting.
 2019-01-06 12:15:31 +07:00
Bruce Mitchener
877df0f1cc If NO_Z3_DEBUGGER, also drop defining invoke_gdb. 2018-12-27 09:21:45 -05:00
Bruce Mitchener
51a947b73d Change how 64 bit builds are detected. 
Instead of doing this at configure time, we look at the actual
compile time status. This also avoids hardcoding checks based on
what CPU architecture is present, which doesn't work when Z3 is
being built on non-x86_64 platforms.
 2018-12-09 16:16:20 +07:00
Bruce Mitchener
4bc1b0b8c8 Fix typos. 2018-12-05 21:07:34 +07:00
Nikolaj Bjorner
030f458017 add vs2013 specific def for thread local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-03 09:15:30 -08:00
Nikolaj Bjorner
9849644f15
Merge pull request #2005 from waywardmonkeys/remove-macos-ifdef 
Remove undef max/min on macOS.
 2018-12-03 07:18:41 -08:00
Bruce Mitchener
a0264c08a8 Windows builds need immintrin.h 
Fixes issue #2006.
 2018-12-03 22:15:14 +07:00
Bruce Mitchener
742efd5104 Remove undef max/min on macOS. 
This is no longer needed.
 2018-12-03 12:32:45 +07:00
Nikolaj Bjorner
8fc75f59b0
Merge pull request #2003 from waywardmonkeys/use-thread_local-storage-specifier 
Use C++11 thread_local for portability.
 2018-12-02 12:32:01 -05:00
Nikolaj Bjorner
cadf4ff914
Merge pull request #2002 from waywardmonkeys/remove-thread-local-macro 
Remove unused THREAD_LOCAL macro.
 2018-12-02 12:31:43 -05:00
Nikolaj Bjorner
74bc461e6b
Merge pull request #1999 from waywardmonkeys/fix-typo 
Fix typo.
 2018-12-02 12:31:19 -05:00
Bruce Mitchener
a332eb10bc Use C++11 thread_local for portability. 
This should work on all supported compilers rather than using
__declspec(thread) and __thread.
 2018-12-02 22:10:37 +07:00
Bruce Mitchener
a0a940f938 Remove unused THREAD_LOCAL macro. 2018-12-02 13:58:31 +07:00
Bruce Mitchener
150fe881ce Fix typo. 2018-12-01 21:06:16 +07:00
Bruce Mitchener
a3ece29628 Remove include of immintrin.h. 
This file doesn't appear to be used and isn't available on all
platforms.
 2018-12-01 20:39:03 +07:00
Nikolaj Bjorner
f2de15a665
Merge pull request #1982 from waywardmonkeys/avoid-const-params-in-decls 
Avoid const params in decls.
 2018-11-28 09:08:03 -08:00
Bruce Mitchener
2016f48dc9 Avoid const params in decls. 
Const-qualification of parameters only has an effect in function
definitions.
 2018-11-28 19:07:33 +07:00
Bruce Mitchener
b83d6d77c9 Use nullptr rather than 0/NULL. 2018-11-28 14:57:01 +07:00
Bruce Mitchener
e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07:00
Nikolaj Bjorner
8e83d04e02 this->size() 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-25 14:22:22 -08:00
Nikolaj Bjorner
16be5b0e7d fix #1816 - m_parent_selects gets updated while accessing an interator, fix is to rely on the size of the vector for iteration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-25 14:04:17 -08:00
Nikolaj Bjorner
7b2590c026 fix is-unit test in seq rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-21 17:08:33 -08:00
Nikolaj Bjorner
0c1408b30e fixing #1948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-21 13:48:48 -08:00
Lev Nachmanson
67ea2a2c88 test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-11-20 09:52:43 -08:00
Nikolaj Bjorner
04d709dae1 build errors on shrink 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-19 09:42:10 -08:00
Nikolaj Bjorner
5eefa9c34b fix combinator signatures 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-19 08:42:18 -08:00
Nikolaj Bjorner
b8ac3e6ce4 Merge branch 'master' of https://github.com/z3prover/z3 2018-11-19 00:48:40 -08:00
Nikolaj Bjorner
529e62e01e remove unsound rewrite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-19 00:48:33 -08:00
Nikolaj Bjorner
102d23f780 Merge branch 'master' of https://github.com/z3prover/z3 2018-11-18 10:40:14 -08:00
Nikolaj Bjorner
a9e6d83c6e std::cout -> out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-18 10:40:08 -08:00
Nikolaj Bjorner
6ef2557e2a investigate #1946 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-18 09:34:33 -08:00
Nikolaj Bjorner
a775d1f518 newline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-31 14:40:13 -05:00
Nikolaj Bjorner
fac114872f Merge branch 'master' of https://github.com/z3prover/z3 into csp 2018-10-22 07:25:39 -07:00
Nikolaj Bjorner
536c2b6ce5 bypass warning size_t/unsigned 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-21 13:15:14 -07:00
Nikolaj Bjorner
ccca063e54 Merge branch 'master' of https://github.com/Z3Prover/z3 into csp 2018-10-21 12:26:53 -07:00
Bruce Mitchener
7e35ce275a Remove unused warning_displayer. 2018-10-21 20:30:07 +07:00
Bruce Mitchener
a73cf590db Remove disable_error_msg_prefix. 
This wasn't used or actually implemented to do anything.
 2018-10-21 20:29:01 +07:00
Bruce Mitchener
129353542c Improve format2ostream. 
Instead of looping to find a big enough buffer, we can call the
correct function to calculate it, remembering to add an extra
character for NUL termination.

We also correctly do a va_copy of the args to avoid crashes on
some platforms.
 2018-10-21 20:22:21 +07:00
Bruce Mitchener
21cf218a9f Remove commented out string2ostream. 2018-10-21 20:12:53 +07:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Nikolaj Bjorner
28a5a515a8 fix #1889 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-18 09:20:12 -07:00
Nikolaj Bjorner
c7d0d4e191 add c-cube's recursive function theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-17 04:56:58 -07:00
Michał Janiszewski
844f400a62 Remove superfluous const from returned types 2018-10-16 19:30:48 +02:00
Nikolaj Bjorner
e9d615e309 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 15:16:22 -07:00
Lev
99339798ee fix the value oflar_solver.m_status during pop() 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-10-04 19:43:01 -07:00