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

8025 commits

This branch
This branch
All branches
Author SHA1 Message Date
Dan Liew
ba8bff76ae [TravisCI] Modify Debug configuration that I forgot to change with 
`RUN_UNIT_TESTS=BUILD_ONLY`.
 2017-10-06 15:52:01 +01:00
Nuno Lopes
9aa6386be9 fix debug build 2017-10-06 15:27:16 +01:00
Nikolaj Bjorner
e13d839e7c Merge branch 'master' of https://github.com/z3prover/z3 2017-10-06 13:43:11 +01:00
Nikolaj Bjorner
2634be01aa adding backwards pass 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 13:43:01 +01:00
Christoph M. Wintersteiger
50042ab638 removed unused variables 2017-10-06 13:00:09 +01:00
Dan Liew
0be28b66fe [TravisCI] Update out of date README.md file. 2017-10-06 12:57:46 +01:00
Dan Liew
2519719d3f Fix typo 2017-10-06 12:57:46 +01:00
Dan Liew
d47aea3987 [TravisCI] Workaround slow unit test execution for Debug builds. 
Unit tests execute very slowly in Debug (i.e. unoptimized) builds.  This
causes TravisCI to terminate the job due to no console output being
seen.

To workaround this for the debug builds the tests are just compiled
but not executed. To implement this the `RUN_UNIT_TESTS` environment
variable now can take on the values `BUILD_ONLY`, `BUILD_AND_RUN`,
and `SKIP` rather than `0` or `1`.
 2017-10-06 12:57:42 +01:00
Christoph M. Wintersteiger
3edf147213 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-06 12:33:57 +01:00
Christoph M. Wintersteiger
690b17fc25 Removed Ubuntu x86 VSTS/CI build (not supported by VSTS anymore). 2017-10-06 12:33:47 +01:00
Nikolaj Bjorner
755ca46df6 adding bv_bounds tactic dominator style 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 12:15:41 +01:00
Nikolaj Bjorner
cb548404bc bail out dominators after log number of steps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 12:08:37 +01:00
Nikolaj Bjorner
6df628edc7 pin elements in expr2depth 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 11:45:29 +01:00
Nikolaj Bjorner
eac659f748 deal with empty set of post-orders 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 11:34:14 +01:00
Nikolaj Bjorner
f59cf2452d #1284 build problems 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-05 22:20:31 +01:00
Nuno Lopes
6eb442f06c Merge branch 'master' of github.com:Z3Prover/z3 2017-10-05 18:10:27 +01:00
Nuno Lopes
6268ff1fa1 dom_simplify improvements with Nikolaj 2017-10-05 18:10:20 +01:00
Christoph M. Wintersteiger
d38e15eae7 Merge pull request #1281 from levnach/dev 
add cancellation checks
 2017-10-05 16:29:46 +02:00
Dan Liew
0633d5819f [TravisCI] Fix bug. PYTHON_EXECUTABLE should not be in common 
defaults. The location is dependent on the implementation.

This triggered a build failure on TravisCI because the location
of the default Python binary is different to what is in the Docker
container.
 2017-10-05 15:09:16 +01:00
Dan Liew
eb975a49d6 [TravisCI] Fix bug where Z3_BUILD_TYPE was not being passed as 
a Docker build argument.

Also update an out of date comment.
 2017-10-05 14:56:31 +01:00
Dan Liew
53fc6ac11b [TravisCI] Refactor as many CI default options as possible so that 
the Docker and "TravisCI macOS" builds share most of the same defaults
by sourcing the `ci_defaults.sh` file.
 2017-10-05 14:56:15 +01:00
Nuno Lopes
110d558ee4 dom_simplify_tactic: micro opt 2017-10-05 08:53:12 +01:00
Lev Nachmanson
fd3d785a5b add this-> 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-10-04 14:49:45 -07:00
Lev Nachmanson
2828126b72 add cancellation checks 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-10-03 10:20:49 -07:00
Nikolaj Bjorner
f1eb53761a Merge pull request #1280 from TheRealNebus/master 
update to _get_args to convert arguments from AstVector to a python list
 2017-10-02 09:26:16 -07:00
Miguel Angelo Da Terra Neves
6c7a82edce update to _get_args to convert arguments from AstVector to a python list 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-10-02 09:20:59 -07:00
Nikolaj Bjorner
e0e2397566 missing setup datatypes for QF_DT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-01 19:40:30 -07:00
Nikolaj Bjorner
05428314be fix #1276 related crashes for re-sumption after cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-01 15:13:43 -07:00
Nikolaj Bjorner
bec60f763b add diagnostics to DDNF and fix #1268 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-30 12:35:36 -07:00
Nikolaj Bjorner
04b11d9721 Merge branch 'master' of https://github.com/z3prover/z3 2017-09-30 10:15:52 -07:00
Nikolaj Bjorner
8ff8c6433b fix #1277 fix #1278 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-30 10:15:27 -07:00
Christoph M. Wintersteiger
bba005154c Merge pull request #1271 from ulidtko/master 
Fix Python API docs done with `make api_docs`
 2017-09-27 15:12:34 +01:00
Christoph M. Wintersteiger
34e6e62ae1 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-09-27 14:23:13 +01:00
Christoph M. Wintersteiger
9a464dded4 Removed -std=c++11 from OCaml stubs build command. Fixes #1263. 2017-09-27 14:22:59 +01:00
Max ulidtko
ce6e26043a fix Python API doxygen (make api_docs) 2017-09-27 14:07:18 +03:00
Max ulidtko
f07b89df86 fix pydoc part of make api_docs 2017-09-27 14:07:02 +03:00
Christoph M. Wintersteiger
4ad3f1f4ea Merge pull request #1270 from kenmcmil/issue1269 
fixing issue [1269]
 2017-09-27 11:25:19 +01:00
Nikolaj Bjorner
2229a2fc1b model validation update take 2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-26 08:43:31 -07:00
Nikolaj Bjorner
6450ee33c5 disregard model validation when source expression contains uninterpreted theory functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-26 08:25:48 -07:00
Ken McMillan
c8a67abdd7 fixing issue [1269] 2017-09-25 14:33:20 -07:00
Murphy Berzish
ec7ea8a763 redo length testing with concrete length, linear search only 2017-09-25 15:21:59 -04:00
Nikolaj Bjorner
f179d49f4f check for eof, based on testing garbled repro from #1267 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-24 10:58:39 -07:00
Nikolaj Bjorner
9cd974e334 remove display 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-24 09:40:35 -07:00
Nikolaj Bjorner
7a15de374a fix #1266 by bypassing topological ordering on theory symbols 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-24 09:19:51 -07:00
Nikolaj Bjorner
2751cbc270 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-23 22:36:36 -05:00
Nikolaj Bjorner
95ee4c94f1 remove utf fixes #1265 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-23 11:37:55 -05:00
Murphy Berzish
317e2b1898 take shortcuts during length testing when length is known from integer theory 2017-09-22 12:32:13 -04:00
Murphy Berzish
b2af690c6d enable binary search for theory_str 2017-09-22 12:31:46 -04:00
Nikolaj Bjorner
cd24535e51 add newline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-22 09:54:56 -05:00
Nikolaj Bjorner
cab4e4b461 add feature to display benchmark in format seen by SAT solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-21 18:32:46 -05:00