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

7808 commits

This branch
This branch
All branches
Author SHA1 Message Date
Murphy Berzish
a570149b57 finite overlap models with binary search 2017-01-17 14:49:57 -05:00
Christoph M. Wintersteiger
6d34899c46 Bugfix for macro finder. Fixes #832. 2017-01-17 15:44:03 +00:00
Christoph M. Wintersteiger
0fae048e3e Windows build fix. 2017-01-17 12:58:32 +00:00
Murphy Berzish
794e210958 finite model fix 2017-01-16 21:42:11 -05:00
Murphy Berzish
0af834421f finite model finding for other concat cases in theory_str 2017-01-16 18:24:47 -05:00
Murphy Berzish
e459617c39 experimental finite model finding WIP, first successful run 2017-01-16 18:04:03 -05:00
Murphy Berzish
4e2847dea4 Revert "scale theory-aware priority by bvar_inc" 
This reverts commit aa8bf2668f.
 2017-01-16 15:46:28 -05:00
Murphy Berzish
4b6582b8f3 Revert "experimental z3str2 search order" 
This reverts commit 0dfaa30ae8.
 2017-01-16 15:46:17 -05:00
Murphy Berzish
0dfaa30ae8 experimental z3str2 search order 2017-01-16 14:46:04 -05:00
Christoph M. Wintersteiger
625681f82f Updated cmake build 2017-01-16 15:59:16 +00:00
Christoph M. Wintersteiger
e472a8d4cf Enabled filenames in error messages during inclusion of files. 2017-01-16 15:46:58 +00:00
Christoph M. Wintersteiger
090a331d79 Added filenames to error messages for when we have more than one file. 2017-01-16 15:43:13 +00:00
Christoph M. Wintersteiger
00a50eea7f Added (include ...) SMT2 command. 2017-01-16 15:05:58 +00:00
Christoph M. Wintersteiger
6fe1682378 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-16 14:08:26 +00:00
Christoph M. Wintersteiger
24e4f19d76 build fix 2017-01-16 14:08:21 +00:00
Nikolaj Bjorner
dc543a7ee7 update macro_util logging to uniform format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 21:13:22 -08:00
Nikolaj Bjorner
c4c9de0838 fix memory leaks from cancellations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 20:09:27 -08:00
Nikolaj Bjorner
24eae3f6e0 fix crash with unary xor #870 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 12:06:56 -08:00
Nikolaj Bjorner
dd0d3d4510 use stirngs for env variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 11:59:09 -08:00
Nikolaj Bjorner
ee36662435 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-15 11:56:01 -08:00
Nikolaj Bjorner
7df803c131 Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 11:52:48 -08:00
Murphy Berzish
aa8bf2668f scale theory-aware priority by bvar_inc 2017-01-14 15:28:58 -05:00
Murphy Berzish
a9ec8666f0 add phase selection to theory-aware branching queue 2017-01-14 14:43:57 -05:00
Christoph M. Wintersteiger
340ba7780e Added MAKEJOBS env var to mk_unix_dist.py 2017-01-14 18:57:10 +00:00
Christoph M. Wintersteiger
b30f3a6dbd Separated win32/64 builds 2017-01-14 14:56:25 +00:00
Christoph M. Wintersteiger
d8e4966a11 Added win64 build badge 2017-01-14 14:18:37 +00:00
Nikolaj Bjorner
bc6b3007de remove unused features related to weighted check-sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-13 20:53:22 -08:00
Christoph M. Wintersteiger
37916fe7e9 Update README.md 2017-01-13 21:33:11 +00:00
Christoph M. Wintersteiger
43eb6cc022 CI trigger 2017-01-13 20:43:53 +00:00
Murphy Berzish
dd03632f3d Merge branch 'develop' of github.com:mtrberzi/z3 into develop 2017-01-13 12:57:50 -05:00
Murphy Berzish
f033a77fae modify theory-aware branching to manipulate activity instead of giving absolute priority 2017-01-13 12:57:48 -05:00
Murphy Berzish
677fcdcb41 concat overlap avoid in theory_str 2017-01-12 18:41:30 -05:00
Christoph M. Wintersteiger
f1a4a48491 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-12 12:49:35 +00:00
Christoph M. Wintersteiger
2458db30cf Corner-case fix for smt::solver::pop_core 2017-01-12 12:49:26 +00:00
Murphy Berzish
6576dabd58 add tracing info to theory_str cut var map 2017-01-12 00:20:34 -05:00
Nikolaj Bjorner
9e4142d599 Merge pull request #869 from danpere/fix/coreclr 
Fix .NET Core bindings
 2017-01-11 20:52:49 -08:00
Daniel Perelman
3370adcdff Mark void DummyContracts as Conditional to avoid compiling their arguments. 2017-01-11 17:02:26 -08:00
Daniel Perelman
f7ebe16046 Omit '.dll' from library name for DllImport. 2017-01-11 16:56:28 -08:00
Christoph M. Wintersteiger
650ea7b9cc Bugfix for smt.core.extend_patterns 2017-01-11 18:40:11 +00:00
Murphy Berzish
20a8ad9b21 correctly reserve entries in theory aware branching queue heap 2017-01-10 22:15:46 -05:00
Murphy Berzish
bc5af58734 additional theory-aware branches in theory_str 2017-01-10 20:08:35 -05:00
Murphy Berzish
1363f50e4f demonstration of theory-aware branching in theory_str, WIP 2017-01-10 19:50:46 -05:00
Christoph M. Wintersteiger
9f49905582 Formatting, whitespace, and Z3_API annotations. 2017-01-10 21:05:27 +00:00
Christoph M. Wintersteiger
d8d869822f Cleaned up #include<iostream> in api* objects. 2017-01-10 21:04:44 +00:00
Murphy Berzish
3459c1993e experimental theory-aware branching code 2017-01-10 15:38:33 -05:00
Christoph M. Wintersteiger
384468bc99 Added option to extend unsat cores with literals that (potentially) provide quantifier instances. 2017-01-10 20:22:20 +00:00
Christoph M. Wintersteiger
ba9d36605b Formatting, whitespace 2017-01-10 20:22:20 +00:00
Murphy Berzish
9004e1b23e disable length test/theory case split integration theory_str 2017-01-10 12:34:44 -05:00
Nikolaj Bjorner
dda1774fa1 update CMakeList to remove polynomial-factorization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-10 08:21:49 -08:00
Christoph M. Wintersteiger
8047f0d91a GCC compilation/keyword fix. Relates to #864 2017-01-10 14:06:56 +00:00