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
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
Bernhard Gleiss
4559092a0c
refactored variable names and added comments to min_cut-related methods for unsat-core-computation
2017-08-01 11:17:06 -04:00
Bernhard Gleiss
bc3d8580c9
fixed typo in optimized unsat core plugin code
2017-08-01 11:17:06 -04:00
Christoph M. Wintersteiger
79ab8a5a5a
Fixed cmake build
2017-08-01 16:16:17 +01:00
Christoph M. Wintersteiger
e315d063c5
renamed LP bound propagator to avoid linker name clashes
2017-08-01 16:07:51 +01:00
Christoph M. Wintersteiger
6bc5209e26
Fixed build problems with .vcxproj
2017-08-01 15:53:55 +01:00
Nikolaj Bjorner
72c478078e
adding cdecl directive to Z3_qe_lite to address build failure for Java bindings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 23:14:53 -07:00
Nikolaj Bjorner
1820ccd491
z3-qe-lite?
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 22:15:57 -07:00
Nikolaj Bjorner
b12882d94a
a few more spacer related warning messages
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 21:56:13 -07:00