mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
16217 commits 23 branches 48 tags 157 MiB
Commit graph

16217 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
bc2e6ce037 Update release.yml for Azure Pipelines 2021-07-10 22:42:02 +02:00
Nikolaj Bjorner
66fc980154 add helper axioms for int2bv #5396 2021-07-10 17:13:16 +02:00
Nikolaj Bjorner
34885562e0 try without #!/bin/env python #5397 2021-07-10 15:20:56 +02:00
Nikolaj Bjorner
0f8d2d1d51 fix #5399 2021-07-10 14:47:51 +02:00
Nikolaj Bjorner
2973d3bdc1 fix #5392 2021-07-07 23:43:30 +02:00
Nikolaj Bjorner
897cbf347b fix #5381 2021-07-07 16:51:06 +02:00
Nikolaj Bjorner
29c6d42380 is-char is overloaded #5389 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-07 08:20:31 +02:00
Nikolaj Bjorner
4f184b6aa9 fix #5376 2021-07-06 19:20:35 +02:00
Nikolaj Bjorner
c2595b9bc8 #5379 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-06 18:58:27 +02:00
Nikolaj Bjorner
af5b2a4179 #5376 2021-07-06 16:44:44 +02:00
Nikolaj Bjorner
ca05c66847 #5376 2021-07-06 14:20:23 +02:00
Marc Mosko
8a33391708
Expose optimize.assertAndTrack to Java (#5387) 
Co-authored-by: Marc Mosko <mmosko@parc.com>
 2021-07-06 01:22:00 -07:00
Gabriel Radanne
0c7625cd26
Remove size argument in OCaml's Z3.mk_re_intersect (#5383) 
* Remove size argument in OCaml's `Z3.mk_re_intersect`

Passing the size as argument is unnecessary in OCaml, and that argument is abridged in all similar `Seq` functions. This applies the same pattern.

* Enable the ocaml documentation in Seq.

Turn all the comments into proper documentation comments.
 2021-07-06 01:21:04 -07:00
Nikolaj Bjorner
bdcfba1324 use sort* not ast* #5386 2021-07-06 10:19:17 +02:00
Nikolaj Bjorner
2a8d00d815 fix #5378 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-06 00:04:16 +02:00
Nikolaj Bjorner
e5aa02b8f5 fix #5382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-05 19:30:03 +02:00
Nikolaj Bjorner
7255a2afd1 fix #5379 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-05 18:43:11 +02:00
Nikolaj Bjorner
d5ff672aaa generalize co-factor to handle cubes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-05 14:10:09 +02:00
Nikolaj Bjorner
04ce8ca5ef u256, separate viable_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-04 23:47:12 -07:00
Nikolaj Bjorner
aeec3bb6df viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-04 10:20:01 -07:00
Nikolaj Bjorner
c0e885931c na 2021-07-03 15:44:25 -07:00
Nikolaj Bjorner
e19a7f71aa u256 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-03 11:31:23 -07:00
Nikolaj Bjorner
ff717a9db1 test / fix wrap-around for mod-interval 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-03 10:49:22 -07:00
Nikolaj Bjorner
1355ea432a na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-03 09:42:25 -07:00
Nikolaj Bjorner
ac0945d617 add memory header 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-03 09:38:08 -07:00
Nikolaj Bjorner
4a94d13c4d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-03 09:34:53 -07:00
Nikolaj Bjorner
c3ac079272 include path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-03 09:15:21 -07:00
Nikolaj Bjorner
674e030456 include paths, separate test for mod_interval 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-03 09:09:54 -07:00
Nikolaj Bjorner
7b31a4e6d1 missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-03 08:52:50 -07:00
Nikolaj Bjorner
1ed1e416b7 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 16:34:33 -07:00
Nikolaj Bjorner
babb90832c initial u256 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 16:24:23 -07:00
Nikolaj Bjorner
c053c7f1c8 virtual 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 13:30:15 -07:00
Nikolaj Bjorner
cc4354ffd5 warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 13:27:00 -07:00
Nikolaj Bjorner
c54b9305b5 viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 11:26:17 -07:00
Nikolaj Bjorner
0fc9d7ad0d viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 11:26:05 -07:00
Nikolaj Bjorner
0520180846 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 03:49:23 -07:00
Nikolaj Bjorner
5bd900a7e1 fix include dependencies for tbv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 03:36:17 -07:00
Nikolaj Bjorner
9e69e1614e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 03:33:51 -07:00
Nikolaj Bjorner
788de7d614 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-02 02:48:45 -07:00
Nikolaj Bjorner
05bcf0bed7 test sup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-01 10:33:25 -07:00
Nikolaj Bjorner
5edc939b85 inf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 21:29:28 -07:00
Nikolaj Bjorner
7d5a1acb61 test sup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 21:12:00 -07:00
Nikolaj Bjorner
6eae7d71db sketch computation for sup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 20:07:10 -07:00
Nikolaj Bjorner
b9f6fc5130 debug buidl 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 13:55:57 -07:00
Nikolaj Bjorner
5549301335 remove unreachable code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 09:13:13 -07:00
Nikolaj Bjorner
b019477378 add cofactoring functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 09:11:42 -07:00
Nikolaj Bjorner
1defbc8aa4 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-06-30 01:05:42 -04:00
Nikolaj Bjorner
a374e739f1 prepare for tuned viable sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-30 01:05:34 -04:00
Jakob Rath
3436b52c4a
Polysat: refactor constraints (#5372) 
* Refactor: remove sign and dep from constraint

* fix some bugs

* improve log messages

* Add missing premises to lemma

* Rename getter in an attempt to fix linux build
 2021-06-25 11:04:25 -07:00
Nikolaj Bjorner
a0b0c1f428 with a fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-23 17:50:33 -07:00