mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity
11690 commits 24 branches 48 tags 158 MiB
Commit graph

29 commits

Author SHA1 Message Date
Nikolaj Bjorner
de6409f558 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-25 11:07:14 -08:00
Nikolaj Bjorner
5a68fc8c07 fix pdd_stack for gc on reduce, add unit test for linear_simplify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-25 11:05:59 -08:00
Nikolaj Bjorner
38f74297a9 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-23 15:30:06 -08:00
Nikolaj Bjorner
beb4c0f27b added notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-23 12:34:30 -08:00
Nikolaj Bjorner
77868f3d96 added notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-23 12:32:02 -08:00
Nikolaj Bjorner
25b98f497a adding level2var 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-22 11:51:04 -08:00
Nikolaj Bjorner
58be42d2a9 initial unit test for pdd_grobner 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-22 10:59:12 -08:00
Nikolaj Bjorner
feff6a2add fix build, add ZDD reference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-20 11:49:50 -08:00
Nikolaj Bjorner
1f9aff04df fix 2808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-20 11:29:08 -08:00
Nikolaj Bjorner
6ad55cc8f6 add tuned implementation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-19 15:26:55 -08:00
Nikolaj Bjorner
78b022491d comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-19 09:26:02 -08:00
Nikolaj Bjorner
1287572f4f add complexity throttle 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 14:31:31 -08:00
Nikolaj Bjorner
13e335f062 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 14:14:46 -08:00
Nikolaj Bjorner
98bfbc2d62 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 13:59:45 -08:00
Nikolaj Bjorner
469f618742 build dependencies, invariant annotation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 13:48:27 -08:00
Nikolaj Bjorner
5e0799225d adding pdd-grobner 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 12:03:13 -08:00
Nikolaj Bjorner
dd452e0ac1 eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 15:29:27 -07:00
Nikolaj Bjorner
f99384c6a3 fix nightly regression from solve-eqs context solver addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-27 04:17:43 -07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the 
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
 2017-06-12 11:59:00 +01:00
Johannes Kanig
9bfa73ee06 Take into account number of monomials for rlimit counting 
Should fix issue #611
 2016-06-08 11:17:26 +09:00
Nikolaj Bjorner
5e7db2e3e2 disable mk_array_eq as it breaks model evaluation/validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-18 08:29:24 -07:00
Nikolaj Bjorner
42726171b5 add limit checks in Grobner. Issue #599 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-15 11:34:48 -07:00
Nikolaj Bjorner
6b82b949cf Make Groebner basis computation interruptable. Exponsed in issue #269 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 11:39:59 -07:00
Nikolaj Bjorner
963981b3a6 fix memory alias bug and non-termination bug exposed by issue #184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-31 14:45:10 -07:00
Nikolaj Bjorner
7c9dd6b8a8 fix exception unsafety leading to double free, issues #184 and issue #175. Location and fix strategy suggested by Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-09 00:34:59 +02:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Leonardo de Moura
9e299b88c4 reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-23 21:53:34 -07:00