mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
10414 commits 49 branches 53 tags 182 MiB
Commit graph

8619 commits

Author SHA1 Message Date
Nikolaj Bjorner
ea0d253308 fix const-char test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-03 11:56:20 -08: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
226497e530 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-03 08:45:28 -08:00
Nikolaj Bjorner
2aa7ccc4a9 hide bit-vector dependencies under seq_util 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-03 08:45:17 -08:00
Nikolaj Bjorner
f1b1886eec
Merge pull request #2004 from waywardmonkeys/remove-nl-purify-tactic 
Remove unused nl_purify_tactic.cpp
 2018-12-03 07:18:56 -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
f40eed99f7 Remove unused nl_purify_tactic.cpp 
This file wasn't built and won't compile as the header for it
is missing.

Most of the related code was removed in df6b1a707e.
 2018-12-02 23:49:49 +07: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
Bruce Mitchener
2faf5ef995 Remove unused iPos. 
This was incremented, but never actually used, so remove it.
 2018-11-30 23:13:22 +07:00
Bruce Mitchener
c51caad5ad Remove duplicate initialization of a sort variable. 2018-11-30 23:12:55 +07:00
Bruce Mitchener
bcfa8045fa Sink some values into loops. 
This removes some dead stores that happen prior to the loop and
ensure that no one is looking at the values outside of the
loop.
 2018-11-30 23:12:21 +07:00
Nikolaj Bjorner
1cfd14fd74
Merge pull request #1995 from waywardmonkeys/fix-typos 
Fix typos.
 2018-11-30 07:45:24 -08:00
Nikolaj Bjorner
dbfeeb8b1c fix #1994 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-30 07:43:42 -08:00
Bruce Mitchener
3149d7f7a4 Fix typos. 2018-11-30 22:19:30 +07:00
Nikolaj Bjorner
57318bab5b Merge branch 'master' of https://github.com/z3prover/z3 2018-11-29 21:04:49 -08:00
Nikolaj Bjorner
3db73e442c reset max unfolding literal on backtrack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-29 21:04:43 -08:00
Nikolaj Bjorner
b0d5b242f1
Merge pull request #1991 from waywardmonkeys/fix-java-api-swap-params 
Fix java api swap params
 2018-11-29 20:53:08 -08:00
Bruce Mitchener
afc9de960c Improve JavaDoc. 2018-11-30 08:42:28 +07:00
Bruce Mitchener
38ca9ddfeb Swapped significand and exponent in call to Context.mkFPNumeral. 
Fixes #973.
 2018-11-30 08:42:01 +07:00
Bruce Mitchener
6567698199 Fix initialization order on theory_seq. 2018-11-30 08:10:49 +07:00
Nikolaj Bjorner
1d4d95aea2 fix #1989 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-29 16:10:02 -08:00
Nikolaj Bjorner
67f22d8d65 improving performance for length constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-29 11:32:52 -08:00
Nikolaj Bjorner
e96f9de70b perf #1988 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-29 06:02:32 -08:00
Nikolaj Bjorner
8248ec879e fix qsat destructor memory allocation #1948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-28 15:35:46 -08:00
Nikolaj Bjorner
45dd820b6c Merge branch 'master' of https://github.com/z3prover/z3 2018-11-28 13:50:40 -08:00
Nikolaj Bjorner
5dc1337476 fix #1984 - already fixed in private branch, but wasn't propagated to master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-28 13:49:53 -08:00
Nikolaj Bjorner
3fe9b76fe5
Merge pull request #1986 from mtrberzi/issue1908 
Z3str3: correct str.replace semantics
 2018-11-28 13:15:39 -08:00
Murphy Berzish
e76e501216 Z3str3: correct str.replace semantics 2018-11-28 14:42:19 -05: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
Nikolaj Bjorner
ee5ae8fb5e
Merge pull request #1983 from waywardmonkeys/missing-ref 
mk_coeffs_without was inadvertently copying src.
 2018-11-28 09:07:15 -08:00
Nikolaj Bjorner
a78380901e
Merge pull request #1976 from waywardmonkeys/use-nullptr-more 
Use nullptr rather than 0/NULL.
 2018-11-28 09:06:40 -08:00
Bruce Mitchener
a3281a02db mk_coeffs_without was inadvertently copying src. 
Pass it via ref.
 2018-11-28 20:12:47 +07: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
090f14e7bc Fix a couple of typos. 2018-11-28 14:58:04 +07:00
Bruce Mitchener
b83d6d77c9 Use nullptr rather than 0/NULL. 2018-11-28 14:57:01 +07:00
Nikolaj Bjorner
c5f280ae6e
Merge pull request #1969 from Bronsa/master 
Catch and print exceptions in Z3_mk_config
 2018-11-27 10:43:43 -08:00
Nikolaj Bjorner
5df29daa35
Merge pull request #1972 from waywardmonkeys/use-vector-empty 
Prefer using empty rather than size comparisons.
 2018-11-27 10:39:34 -08:00
Nikolaj Bjorner
7b68d3d893
Merge pull request #1973 from waywardmonkeys/modernize-use-override 
Use 'override' in new code.
 2018-11-27 10:37:35 -08:00
Nikolaj Bjorner
4bbf90c57f
Merge pull request #1974 from waywardmonkeys/fix-ocaml-typo 
Fix typo in OCaml API docs.
 2018-11-27 10:37:24 -08:00
Nikolaj Bjorner
2b34e4f738 fix #1968 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-27 10:36:03 -08:00
Bruce Mitchener
7fb0106ead Fix typo in OCaml API docs. 2018-11-27 22:14:41 +07:00
Bruce Mitchener
64ac929301 Use 'override' in new code. 2018-11-27 22:07:14 +07:00