mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
9047 commits 49 branches 53 tags 182 MiB
Commit graph

9047 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Murphy Berzish
b2388464e4 add re.all to theory_str 2017-08-09 22:03:26 -04:00
Murphy Berzish
84abdae5f7 fix indentation 2017-08-09 15:38:56 -04:00
Murphy Berzish
fce35fdb61 Revert "fix indentation and add support for re.allchar" 
This reverts commit cadde94017.
 2017-08-09 15:37:52 -04: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
Murphy Berzish
cadde94017 fix indentation and add support for re.allchar 2017-08-07 23:02:55 -04:00
Murphy Berzish
f4c0e0b28d fix regex bug in theory_str for empty string match. need to fix indents 2017-08-06 17:17:04 -04: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
Lev Nachmanson
95f86ae2c0 more efficient lar_solver::get_model 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-08-03 11:03:52 -07:00
Nikolaj Bjorner
5fdea2cb18 use rfind instead of index to avoid prefix clashes #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 10:19:07 -07:00
Lev Nachmanson
712619a9cf fix a but in adjusting term indices for implied_bounds 2017-08-03 10:09:00 -07:00
Nikolaj Bjorner
ffaaa1ff34 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-03 08:50:17 -07:00
Nikolaj Bjorner
8844112418 update header include generation to use relative paths #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 08:50:04 -07:00
Nikolaj Bjorner
06e48c89f2 Merge branch 'master' of https://github.com/z3prover/z3 2017-08-02 16:56:51 -07:00
Nikolaj Bjorner
4b3251dec1 update API functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-02 16:56:43 -07:00
Nikolaj Bjorner
d12a0133ce Merge pull request #1189 from delcypher/travis_ci_wait_longer_when_no_output 
[TravisCI] Try to make the LTO build more reliable.
 2017-08-02 08:47:09 -07:00
Dan Liew
c2f69ae9fb [TravisCI] Try to make the LTO build more reliable. 
TravisCI kills builds that don't show output for over 10 minutes [1].
This sometimes causes LTO builds to fail because gcc shows no output
during linking which can take many minutes to complete.

To workaround this we use the `travis_wait` command to allow at
most 45 minutes for the build to run. This command will force output
to appear at regular intervals.

The change is made in the top-level `.travis.yml` file rather than
the other scripts because I don't want to pollute them with TravisCI
specific details.

[1] https://docs.travis-ci.com/user/common-build-problems/#Build-times-out-because-no-output-was-received
 2017-08-02 11:58:47 +01:00
Nikolaj Bjorner
ce3fd22f3b use common idioms for factor-equivalence code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 21:07:20 -07:00
Nikolaj Bjorner
0a6759383a Merge pull request #1188 from agurfinkel/move_obj_equiv 
moved obj_equiv_class to ast
 2017-08-01 20:05:37 -07:00
Arie Gurfinkel
88a35119b9 moved obj_equiv_class to ast 2017-08-01 19:24:50 -04:00
Nikolaj Bjorner
4d07fa5db3 use ifdef instead of if for _TRACE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 12:46:38 -07:00
Nikolaj Bjorner
be8add44e9 instrument unit test to use reproducible random number generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 12:42:08 -07:00
Nikolaj Bjorner
22a2aae486 trying to fix build break on use of iterator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 11:47:55 -07:00
Nikolaj Bjorner
3214644e0d Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-01 10:51:52 -07:00
Nikolaj Bjorner
2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Christoph M. Wintersteiger
49d5131f83 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-01 18:33:59 +01:00
Christoph M. Wintersteiger
81a7f37acc Fixed LP tests 2017-08-01 18:33:47 +01:00
Christoph M. Wintersteiger
13c9a6faf7 Merge pull request #1185 from agurfinkel/spacer-nlg-fix 
Spacer nlg fix
 2017-08-01 17:23:23 +01:00
Christoph M. Wintersteiger
aefed78f1a Fixed ML API build again 2017-08-01 17:02:04 +01:00
Christoph M. Wintersteiger
ce01895ab3 Fixed ML API build. 2017-08-01 16:54:27 +01:00
Christoph M. Wintersteiger
4ff938f2c1 Fixed MPF fp.rem(0,0,0). Relates to #872. 2017-08-01 16:46:10 +01:00