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

11615 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
092c25d596 fix #2007 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 18:37:30 -08:00
Nikolaj Bjorner
b40c2b2926 fix #876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 14:11:00 -08:00
nilsbecker
6d2cf4f464 smt-like logging of theory specific meaning of constants 2018-12-10 22:49:08 +01:00
Nikolaj Bjorner
68ace83893 remove enable trace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 07:34:56 -08:00
Nikolaj Bjorner
f2a7bcaf5d remove prints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-09 14:38:45 -08:00
Nikolaj Bjorner
bb69aa88fb Merge branch 'master' of https://github.com/z3prover/z3 2018-12-09 12:56:26 -08:00
Nikolaj Bjorner
604e5dd0bb fixing #2030 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-09 12:56:21 -08:00
Nikolaj Bjorner
45bf7887e4
Merge pull request #2032 from waywardmonkeys/enable-dl-table-tests 
Enable dl_table tests on non-Windows/Cygwin.
 2018-12-09 20:01:21 +01:00
Bruce Mitchener
1b91694d9b Enable dl_table tests on non-Windows/Cygwin. 2018-12-09 21:02:06 +07: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
Nikolaj Bjorner
559f57470e fix #2031 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-09 08:21:48 +01:00
Nikolaj Bjorner
2ca83d0095 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-08 15:42:13 +01:00
Nikolaj Bjorner
38b5e6de56 fix #2019 - insufficient axioms for special cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-08 13:57:35 +01:00
Nikolaj Bjorner
f1d1e728ff
Merge pull request #2021 from waywardmonkeys/api-bool-reduction 
Simplify boolean code.
 2018-12-07 18:59:45 +00:00
Nikolaj Bjorner
a20e68facc throttel extract/ite rewriting to avoid perf-bug exposed in example from Lucas Cordeiro and Alessandro Trindade 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-07 17:54:49 +00:00
Bruce Mitchener
0231bc44bc Simplify boolean code. 
Now that the C API is using bool, this can be simplified.
 2018-12-07 22:06:51 +07:00
Nikolaj Bjorner
a9946685ca
Merge pull request #2024 from UniQP/caseLabels 
Fix enum type of case labels
 2018-12-06 07:43:01 -08:00
Nikolaj Bjorner
e1b1953ff1
Merge pull request #2025 from msoeken/nuget-release 
Changes to NuGet release script
 2018-12-06 07:41:52 -08:00
Mathias Soeken
9a0a1dd818 Changes to NuGet release script. 2018-12-06 16:19:03 +01:00
Sebastian Buchwald
5690dbcbfd Fix enum type of case labels 2018-12-06 00:08:29 +01:00
Nikolaj Bjorner
f2c263001c
Merge pull request #2020 from waywardmonkeys/fix-typos 
Fix typos.
 2018-12-05 13:16:23 -08:00
Bruce Mitchener
4bc1b0b8c8 Fix typos. 2018-12-05 21:07:34 +07:00
Nikolaj Bjorner
9635ddd8fc fix #2018 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-05 00:54:10 -08:00
Nikolaj Bjorner
dc77579707 delta faction to control double lookahead eagerness 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-04 23:41:03 -08:00
Nikolaj Bjorner
44b2c3ce6b
Merge pull request #2016 from Z3Prover/revert-2015-c++-api-use-nullptr 
Revert "Use nullptr, not 0 in the C++ API impl."
 2018-12-04 12:07:10 -08:00
Nikolaj Bjorner
3b54575340
Revert "Use nullptr, not 0 in the C++ API impl." 2018-12-04 12:06:44 -08:00
Nikolaj Bjorner
0223846b4f
Merge pull request #2015 from waywardmonkeys/c++-api-use-nullptr 
Use nullptr, not 0 in the C++ API impl.
 2018-12-04 10:18:23 -08:00
Nikolaj Bjorner
7aaacbfc62
Merge pull request #2014 from waywardmonkeys/simplify-boolean-returns 
Simplify some boolean returns.
 2018-12-04 10:17:53 -08:00
Nikolaj Bjorner
4b94ea112d
Merge pull request #2013 from waywardmonkeys/remove-get-manager 
Remove Z3_get_manager.
 2018-12-04 10:17:29 -08:00
Nikolaj Bjorner
3551d12168
Merge pull request #2011 from waywardmonkeys/missing-Z3_API 
Z3_fixedpoint_add_constraint: decl missing Z3_API.
 2018-12-04 10:17:12 -08:00
Nikolaj Bjorner
2372d1bdeb
Merge pull request #2012 from waywardmonkeys/doc-fixups 
Fix up more documentation formatting.
 2018-12-04 10:16:27 -08:00
Nikolaj Bjorner
a6d8818be4 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-04 10:14:42 -08:00
Nikolaj Bjorner
9e5aaf074e perf improvements for #1979 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-04 10:13:55 -08:00
Bruce Mitchener
924776eaa6 Use nullptr, not 0 in the C++ API impl. 2018-12-04 22:43:01 +07:00
Bruce Mitchener
5fa861fa95 Simplify some boolean returns. 2018-12-04 22:41:31 +07:00
Bruce Mitchener
374b80f37f Remove Z3_get_manager. 
This was publicly exported from the shared library, but it isn't
in any header files and isn't used anywhere in the repository.
 2018-12-04 21:38:33 +07:00
Bruce Mitchener
15e1a5ee86 Fix up more documentation formatting. 2018-12-04 20:20:21 +07:00
Bruce Mitchener
6c21d3d9e8 Z3_fixedpoint_add_constraint: decl missing Z3_API. 2018-12-04 12:24:42 +07:00
Nikolaj Bjorner
e15a39f463
Merge pull request #2010 from waywardmonkeys/doc-markup-z3-l-consts 
Mark up Z3_L_TRUE and friends correctly in the docs.
 2018-12-03 19:01:05 -08:00
Bruce Mitchener
42d2a46826 Mark up Z3_L_TRUE and friends correctly in the docs. 2018-12-04 09:12:12 +07:00
Nils Becker
0870760eb5 logging meaning of theory specific constants 2018-12-03 22:41:59 +01:00
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
Nikolaj Bjorner
8638c2c8a4
Merge pull request #2008 from waywardmonkeys/add-immintrin.h-on-windows 
Windows builds need immintrin.h
 2018-12-03 07:17:53 -08:00
Bruce Mitchener
a0264c08a8 Windows builds need immintrin.h 
Fixes issue #2006.
 2018-12-03 22:15:14 +07:00
nilsbecker
988e8afc2e support for logging congruence closure equality explanations when commutativity is used 2018-12-03 13:50:48 +01:00