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

7833 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
0f1583309d Bugfix for fp.fma. One piece of puzzle #872. 2017-07-21 21:12:45 +01:00
Christoph M. Wintersteiger
faa19117e4 Fixed inconsistent state upon solver interruption. Partially fixes #951. 2017-07-21 17:42:48 +01:00
Christoph M. Wintersteiger
943dc8118a Improved collect-statistics tactic 2017-07-20 13:44:47 +01:00
Murphy Berzish
7ddb940f77 add e_internalized() check in theory_str::get_arith_value() 2017-07-19 10:15:38 -04:00
Murphy Berzish
69f0ed9b1f remove disabled code block in get_arith_value() 2017-07-18 13:13:12 -04:00
Murphy Berzish
c6707688ba improved get_arith_value() in theory_str 
Since the root of the eqc of an integer term should be a constant
if there is a constant in that eqc, we can ask for it directly
without either iterating over the entire eqc or
asking the arithmetic solver (and receiving potentially stale info).
 2017-07-18 13:11:03 -04:00
Christoph M. Wintersteiger
da34de340d Fixed bug in sat model converter. Fixes #1148. 2017-07-15 20:25:13 +01:00
Nikolaj Bjorner
8a57e081f7 Merge pull request #1138 from delcypher/cmake_serious_warnings 
Support serious warnings in CMake and TravisCI
 2017-07-14 11:14:35 +02:00
Christoph M. Wintersteiger
680f342247 Merge pull request #1145 from delcypher/fix_doc_typo 
Fix minor typo in C API documentation
 2017-07-12 15:47:44 +01:00
Christoph M. Wintersteiger
baedf41c6c Merge pull request #1144 from delcypher/fix_parse_bvsmod_i 
Fix typo that prevented uses of `bvsmod_i` being parsed.
 2017-07-12 15:47:24 +01:00
Dan Liew
5b511f12b3 Fix minor typo in C API documentation 2017-07-12 13:07:19 +01:00
Dan Liew
89c8f1722f Fix typo that prevented uses of bvsmod_i being parsed. 2017-07-12 12:53:10 +01:00
Christoph M. Wintersteiger
bf83b897a1 Merge pull request #1142 from jfeser/master 
Add get_num_scopes to python solver api.
 2017-07-11 21:29:50 +01:00
Jack Feser
0e45777104 add get_num_scopes to python solver api 2017-07-11 14:42:34 -04:00
Murphy Berzish
86e7f83e06 proper theory_arith integration in theory_str::get_arith_value() 2017-07-11 13:24:48 -04:00
Dan Liew
630863619b [TravisCI] Add Z3_WARNINGS_AS_ERRORS environment variable to 
control the `WARNINGS_AS_ERRORS` CMake option.
 2017-07-09 14:44:20 +01:00
Dan Liew
6e2ca69654 [CMake] Change the WARNINGS_AS_ERRORS option from BOOL to STRING 
to allow a new mode `SERIOUS_ONLY`.

Modes:

`ON` - All warnings are treated as errors (same as before)
`OFF` - Warnings are not treated as errors (same as before)
`SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors.

Upgrade code is included to upgrade old CMake cache's to use the new
type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The
user's previous setting is preserved when doing this.

Very few warnings are treated as errors for now. Developers can
add more later as they see fit.
 2017-07-09 14:34:30 +01:00
Nikolaj Bjorner
2b0106c199 doc fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-09 11:26:27 +02:00
Nikolaj Bjorner
2af08a378d avoid complaining about division by 0 as unhandled in theory-lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-08 18:21:47 -07:00
Nikolaj Bjorner
5714f830b0 fix check for finite sorts #1122 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-08 13:37:24 -07:00
Nikolaj Bjorner
ea331ebfbe revert update to #1134 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 08:29:16 -07:00
Nikolaj Bjorner
d06e48a361 detect overlapping signatures #1134 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 08:13:14 -07:00
Nikolaj Bjorner
98391883ca Merge branch 'master' of https://github.com/z3prover/z3 2017-07-07 07:45:00 -07:00
Nikolaj Bjorner
49cf3f8008 update documentation according to #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 07:44:55 -07:00
Christoph M. Wintersteiger
4b895abec7 Merge pull request #1136 from danpere/guard-cf 
Add flag to mk_make.py to optionally enable Control Flow Guard
 2017-07-07 11:48:52 +01:00
Daniel Perelman
d57494395c Add --guardcf flag to mk_make.py to optionally enable Control Flow Guard. 2017-07-06 16:59:20 -07:00
Nikolaj Bjorner
465ed7d068 adding doc #1132 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-05 10:21:57 -07:00
Nikolaj Bjorner
5357864dbe Merge pull request #1131 from mtrberzi/fix-warnings-2 
fix theory_str warnings: rename get_value() to get_arith_value()
 2017-07-05 10:03:41 -07:00
Murphy Berzish
b14364a117 fix theory_str warnings: rename get_value() to get_arith_value() 2017-07-05 11:06:40 -04:00
Nikolaj Bjorner
41803ec1cf fix trace/debug build for unreferenced variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 19:55:38 -07:00
Nikolaj Bjorner
cba9a160d3 deal with warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 19:42:22 -07:00
Nikolaj Bjorner
5b8e3ae198 Merge pull request #1129 from mtrberzi/fix-warnings 
clean up warnings in theory_str
 2017-07-04 19:41:43 -07:00
Nikolaj Bjorner
bd92797663 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 15:25:59 -07:00
Nikolaj Bjorner
d66db280a8 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:43:32 -07:00
Nikolaj Bjorner
a1306eaab6 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:17:37 -07:00
Nikolaj Bjorner
253870c6d7 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:08:23 -07:00
Murphy Berzish
03fe3d74f8 clean up warnings in theory_str 2017-07-04 13:28:18 -04:00
Nikolaj Bjorner
47f194e4c9 icon update, take 4 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 17:06:38 -07:00
Nikolaj Bjorner
cc4cc8e4fb icon update, take 3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 17:05:31 -07:00
Nikolaj Bjorner
416d955cfb icon update, take 2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 17:03:41 -07:00
Nikolaj Bjorner
934dd0db4a revert icon update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 17:00:48 -07:00
Nikolaj Bjorner
031d7e1b59 use iterators, update build icon for osx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 16:58:40 -07:00
Nikolaj Bjorner
c66ec9d3f6 Merge branch 'master' of https://github.com/z3prover/z3 2017-07-01 11:48:31 -07:00
Nikolaj Bjorner
08524a2d90 cleanup for warning message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 11:47:17 -07:00
Nikolaj Bjorner
27ad1813b7 Merge pull request #1126 from delcypher/travis_ci_initial_implementation 
[TravisCI] Implement TravisCI build and testing infrastructure for Linux
 2017-07-01 11:17:47 -07:00
Dan Liew
8310fed528 [TravisCI] Implement TravisCI build and testing infrastructure for Linux 
The Linux builds rely on Docker (using Ubuntu 16.04LTS and Ubuntu
14.04LTS) to build and test Z3 so that builds are easily reproducible.

A build status button has been added to `README.md` so that it is
easy to see the current build status.

More documentation can be found in `contrib/ci/README.md`.

This implementation currently tests 13 different configurations. If
build times become too long we can remove some of them.

Although it would be nice to test macOS builds that requires
significantly more work so I have left this as future work.
 2017-07-01 11:51:30 +01:00
Nikolaj Bjorner
be4b0ffe69 fix unsoundness bug instroduced when fixing #1125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-30 19:36:38 -07:00
Nikolaj Bjorner
c44c8284bd use worklist algorithm to avoid stack overflow #1125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-30 18:10:36 -07:00
Christoph M. Wintersteiger
1f29cebd4d Fixed backwards compatibility problem in maxsat example 2017-06-28 14:44:41 +00:00
Christoph M. Wintersteiger
1a59123819 Fixed x86/x64 issues in theory_str 2017-06-28 12:49:10 +01:00