mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
10271 commits 23 branches 48 tags 157 MiB
Commit graph

930 commits

Author SHA1 Message Date
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
Nikolaj Bjorner 69f35a2970
Merge branch 'master' into intel-compiler 2018-10-02 11:54:52 -07:00
Bruce Mitchener a76397d3b8 Refer to macOS rather than Mac OS / OSX. 2018-10-02 17:38:09 +07:00
Nikolaj Bjorner 7082d85115
Merge pull request #1860 from waywardmonkeys/modernize-use-override 
Use 'override' where possible.
 2018-10-01 20:43:56 -07:00
Bruce Mitchener 373b691709 Use 'override' where possible. 2018-10-02 10:26:38 +07:00
Nikolaj Bjorner 5eb24d3118 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-01 20:22:10 -07:00
Nikolaj Bjorner 3c7e7a7ffd
Merge pull request #1852 from janisozaur/unused-const 
Drop unused CV-qualifiers from scalar return values
 2018-10-01 20:10:21 -07:00
Nikolaj Bjorner 4bc6720af7
Merge pull request #1853 from janisozaur/solve-ax-eq-b 
Add missing template instantion for lar_core_solver::m_r_solver
 2018-10-01 20:09:50 -07:00