mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity
7207 commits 23 branches 48 tags 156 MiB
Commit graph

7207 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner e1d08e9526 remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 20:41:29 -07:00
Nikolaj Bjorner a3ccdaf318 Merge branch 'master' of https://github.com/z3prover/z3 2017-08-17 20:28:56 -07:00
Nikolaj Bjorner ff47c8632b remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 20:28:49 -07:00
Nikolaj Bjorner 7861cfcef2 Merge pull request #1216 from delcypher/cmake_simpler_include_paths 
Simpler include paths (fixes #534)
 2017-08-17 15:59:23 -07:00
Christoph M. Wintersteiger abd599f48e Fixed ref-counting bug in smt_model_checker. Fixes #1212. 2017-08-17 19:29:53 +01:00
Christoph M. Wintersteiger 320c81e497 Whitespace 2017-08-17 19:18:14 +01:00
Dan Liew 920c596c23 [CMake] Clean up setting include paths. 
Now that all include paths are relative to the `src/` trees (
one in source tree and one in the build tree) we can simplify
what the CMake build does significantly.

While I'm here I also removed some dead code that wasn't doing
anything useful.
 2017-08-17 18:26:58 +01:00
Dan Liew a2d7b43554 Update header includes to be relative to src/ directory. 2017-08-17 18:26:53 +01:00
Christoph M. Wintersteiger 3487b368d1 Added diagnostic output for pattern inference. 2017-08-17 17:27:06 +01:00
Christoph M. Wintersteiger 1620796bd1 Whitespace 2017-08-17 17:25:04 +01:00
Christoph M. Wintersteiger b2d590e0c9 Bugfix for MAM. Fixes #1213. Partially addresses #1212. 2017-08-17 16:00:59 +01:00
Christoph M. Wintersteiger 96d0781c9d Whitespace 2017-08-17 11:39:06 +01:00
Nikolaj Bjorner 43c2ccb29a add missing functions to serialize optimize benchmarks for Java #1215 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-16 16:38:48 -07:00
Nikolaj Bjorner 4b759fd865 add missing functions to serialize optimize benchmarks for Java #1215 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-16 16:18:19 -07:00
Nikolaj Bjorner 97e263299d add logic 'SAT' as an alternative name to QF_FD some solverFor(SAT) works too. #1152 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-15 01:35:28 -07:00
Nikolaj Bjorner 25752dc169 enable QF_UF mode use same parameters whether with or without static featues, #1141, revert some breaking changes that should not have been part of commit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-15 01:20:30 -07:00
Nikolaj Bjorner 1690febffd enable QF_UF mode use same parameters whether with or without static featues, #1141 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-15 00:26:05 -07:00
Nuno Lopes 4b00bc636b revert the patch to remove no-strict-aliasing 
VS 2012 doesnt support C++11 unions..
 2017-08-14 23:00:59 +01:00
Nuno Lopes 197aefd111 fix crash introduced in my previous commit 2017-08-14 22:22:48 +01:00
Nikolaj Bjorner dc4dbdf51e Merge branch 'master' of https://github.com/z3prover/z3 2017-08-14 12:52:41 -07:00
Nikolaj Bjorner 086ea7867e another stab at #989 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-14 12:52:25 -07:00
Christoph M. Wintersteiger 75c3e2d67e Merge pull request #1208 from delcypher/travis_ci_temp_disable_macos 
[TravisCI] Temporarily disable the macOS build configuration.
 2017-08-14 21:25:48 +02:00
Nuno Lopes 000796c25c micro-optimization in tactics' cleanup(): avoid dealloc+alloc traffic 2017-08-14 20:12:00 +01:00
Nuno Lopes 632c2d8ebf use static_assert in COMPILE_TIME_ASSERT 2017-08-14 20:10:17 +01:00
Nuno Lopes 2473c69679 Drop no-strict-aliasing and fix 2 places where it was violated 2017-08-14 20:09:49 +01:00
Dan Liew 9dc332ae9d [TravisCI] Temporarily disable the macOS build configuration. 
@wintersteiger is concerned there might be legal issues using
TravisCI's macOS infrastructure.

For context see:

https://github.com/Z3Prover/z3/pull/1207#issuecomment-322200998
 2017-08-14 17:35:51 +01:00
Nikolaj Bjorner 07bc19b489 add documentation to string rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-14 07:19:04 -07:00
Nikolaj Bjorner a39b0b201a another fix to str.to.int/int.to.str semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:27:34 -07:00
Nikolaj Bjorner fb17362dff fix string rewriting according to definition. Relates to examples in #1202 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:21:38 -07:00
Nikolaj Bjorner ead704f52f handle undefined constant cases for int.to.str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:13:10 -07:00
Nikolaj Bjorner 893bcbb585 revert unsound change in integer extraction from expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 14:39:37 -07:00
Nikolaj Bjorner b6cc24faf3 deal with absence of integer congruence root by querying arithmetic theory directly, #1202 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 14:24:56 -07:00
Nikolaj Bjorner 00742566fb address inconsistent states encountered when cancelling, #1197 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 13:40:30 -07:00
Nikolaj Bjorner 19bb55e396 recognize theory_i_arith to fix #1200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 10:22:36 -07:00
Nikolaj Bjorner 347ea50b93 fix for #1202 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 09:25:46 -07:00
Nikolaj Bjorner c4083c367a update handling of contains constraints taking string literals into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 19:14:55 -07:00
Nikolaj Bjorner c0bd40c00a Merge branch 'master' of https://github.com/z3prover/z3 2017-08-12 17:53:07 -07:00
Nikolaj Bjorner 50e9b371d9 inc version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 17:52:58 -07:00
Nikolaj Bjorner 516d8b034d Merge pull request #1207 from delcypher/travis_ci_macos 
[TravisCI] Enable macOS build
 2017-08-12 17:43:52 -07:00
Nikolaj Bjorner df18c3496a Merge pull request #1205 from delcypher/cmake_openmp_better_default 
[CMake] Change how the default value of `USE_OPENMP` is set.
 2017-08-12 17:43:39 -07:00
Nikolaj Bjorner 85cdfd885f address bug reported in #1196 and include additional ad-hoc rewrites to handle some string cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 17:41:18 -07:00
Nikolaj Bjorner f99048f3e7 rewrite to address some cases like #1203, updates to division handling in NRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 13:24:54 -07:00
Dan Liew 850c2ebc0c [TravisCI] Add scripts to build and test Z3 on macOS (OSX) and 
add a single configuration to TravisCI to test.

TravisCI is very slow at running macOS jobs so just have one
configuration for now.
 2017-08-12 19:14:06 +01:00
Dan Liew e88f33ba94 [TravisCI] Unbreak showing interactive log output for non-LTO 
builds.

c2f69ae9fb added the use of the
`travis_wait` command to all builds but this stops interactive
build output from showing in the TravisCI web interface. To limit
the scope of this change we only use it for LTO builds now.
 2017-08-12 19:14:06 +01:00
Dan Liew e898f515f7 [CMake] Change how the default value of USE_OPENMP is set. 
This change means if the user explicitly passes `-DUSE_OPENMP=ON` to
CMake during the first configure and the compiler does not support
OpenMP the configure will fail but if the user doesn't specify it the
build system will automatically enable/disable OpenMP support depending
on whether it is supported by the compiler.

This is an improvement on the previous behaviour because previously we
would just emit a warning if `-DUSE_OPENMP=ON` was passed and the
compiler didn't support OpenMP.
 2017-08-12 18:37:03 +01:00
Nikolaj Bjorner 7b47b0380e update Ackerman reduction for division to make Andre and Nathan happy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-10 23:43:21 +02:00
Nikolaj Bjorner 082936bca6 enable overloading resolution on define-fun declarations, fix #1199 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-08 09:21:06 +02:00
Nikolaj Bjorner 05c4ea82ce Merge pull request #1146 from levnach/dev 
fix get_model in lar_solver
 2017-08-03 14:01:29 -07:00
Nikolaj Bjorner 2f466b6585 Merge branch 'master' of https://github.com/z3prover/z3 2017-08-03 13:56:04 -07:00
Nikolaj Bjorner 91ee52e549 fix #1195 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 13:53:38 -07:00