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

15886 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
31267e6ab8 #5429 2021-07-30 14:55:59 -07:00
Nikolaj Bjorner
f3f83d0445 #5429 2021-07-30 13:43:02 -07:00
Nikolaj Bjorner
5ca8628e0d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 13:42:54 -07:00
Nikolaj Bjorner
38250fc304 re-move #5442 2021-07-29 15:33:30 -07:00
Nikolaj Bjorner
b8a437bd8a #5429 
relevancy propagation applies to quantifier unfolding.
 2021-07-29 15:05:06 -07:00
Nikolaj Bjorner
211a6c8752 rename 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-29 11:32:20 -07:00
Nikolaj Bjorner
d0686671c5 Merge branch 'master' of https://github.com/z3prover/z3 2021-07-29 11:31:45 -07:00
Nikolaj Bjorner
db5252a81b add dummy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-29 11:31:39 -07:00
0152la
72d3074a44
Add Ubuntu CMake Coverage CI step (#5442) 
Adds an extra step to CI jobs which executes the Z3 test suite with
coverage enabled, and additionally executed coverage-enhancing tests
added to z3test.
 2021-07-29 11:29:49 -07:00
Nikolaj Bjorner
703659a3a8 fix #5439 2021-07-28 17:16:17 -07:00
Kiwamu Okabe
81b8f397b3
Need -thread option to compile OCaml example (#5440) 
I can compile the OCaml example with `-thread` option at Linux.

```
$ ocaml --version
The OCaml toplevel, version 4.05.0
```
 2021-07-28 16:57:26 -07:00
Nikolaj Bjorner
442d1d28ea #5429 2021-07-27 19:11:16 -07:00
Nikolaj Bjorner
16413b4f9a #5429 2021-07-27 17:18:22 -07:00
Nikolaj Bjorner
79296d8dfc proviso for different life-time of objects allocated in arguments. 2021-07-27 09:09:21 -07:00
Nikolaj Bjorner
5964b26ca2 err 2021-07-27 09:07:34 -07:00
Nikolaj Bjorner
7cb4932ae8 fix #5435 2021-07-27 09:04:29 -07:00
Nikolaj Bjorner
2f49094d49 change debug output 2021-07-26 19:36:16 -07:00
Nikolaj Bjorner
7e705c4854 fix #5430 2021-07-26 13:47:21 -07:00
Nikolaj Bjorner
5652d2a157 #5429 #5431 2021-07-25 11:59:42 -07:00
Nikolaj Bjorner
b638405e42 simplify #5431 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-25 09:57:38 -07:00
Margus Veanes
4fd1e6d32c
added derivative support for (str.to_re (str.from_int ...)) (#5431) 2021-07-25 09:51:48 -07:00
Nikolaj Bjorner
2fa156eaf4 #5429 2021-07-25 09:36:45 -07:00
Nikolaj Bjorner
10145366b2 #5425 
Add an alternative to unit-subsume-simplify
It is called solver-subsumption
It does a little more than unit-subsume-simplify and also uses a different decomposition algorithm for clauses.
It removes redundant constraints and simplifies clauses in a single pass.
A possible use of this tactic is in isolation where the maximal number of conflicts
(smt.conflicts_max, sat.conflicts_max) are bounded. For simpler formulas full solver calls may be still feasible.
 2021-07-23 21:02:25 -07:00
Nikolaj Bjorner
32beb91efa sat.euf add missing function 2021-07-22 19:17:17 -07:00
Nikolaj Bjorner
800fef6653 fix #5424 2021-07-22 18:31:37 -07:00
Nikolaj Bjorner
848a8ebb98 #5427 2021-07-22 13:35:54 -07:00
Nikolaj Bjorner
2589f2bad4 #5427 2021-07-22 12:07:11 -07:00
Nikolaj Bjorner
76427cd281 #5427 2021-07-22 11:33:47 -07:00
Nikolaj Bjorner
9a5c0f2312 #5427 2021-07-22 09:38:05 -07:00
Nikolaj Bjorner
39c3f34a30 remove unused dependency 2021-07-21 09:25:08 -07:00
Nikolaj Bjorner
644bd82ac7 #5422 2021-07-21 09:08:55 -07:00
Nikolaj Bjorner
005d35f9c9 #5422 2021-07-21 07:39:39 -07:00
Nikolaj Bjorner
ca8f914dd8 #5422 2021-07-21 07:22:05 -07:00
Nikolaj Bjorner
e5e7c510d5 #5422 2021-07-21 07:14:54 -07:00
Nikolaj Bjorner
8a4b292f3e #5422 2021-07-21 06:25:30 -07:00
Nikolaj Bjorner
0ba518b0c0 avoid perf abyss for macros 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-20 20:07:06 -07:00
Nikolaj Bjorner
574246ff7a #5420 2021-07-20 15:29:24 -07:00
Nikolaj Bjorner
134562162a #5420 2021-07-20 13:50:21 -07:00
Nikolaj Bjorner
614cb26489 #5420 2021-07-20 11:44:57 -07:00
Nikolaj Bjorner
89ed19a719 #5420 2021-07-20 11:20:16 -07:00
Nikolaj Bjorner
b84b5d091e #5420 2021-07-20 08:02:21 -07:00
Nikolaj Bjorner
f90795c42f #5420 2021-07-20 07:58:21 -07:00
Nikolaj Bjorner
49bd3ad159 #5417 again, refining root clauses above search level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-19 16:56:10 -07:00
Nikolaj Bjorner
7af2309fae #5331 2021-07-19 16:09:13 -07:00
Nikolaj Bjorner
a8b433e6ac #5331 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-19 15:58:10 -07:00
Nikolaj Bjorner
a64867942d #5417 designate quantifier axioms as auxiliary 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-19 15:35:18 -07:00
Nikolaj Bjorner
4388ab2e3e #5417 
more gracefully handle non-implemented theories
 2021-07-19 13:50:20 -07:00
Nikolaj Bjorner
0a34eef470 #5417 2021-07-19 13:41:02 -07:00
Nikolaj Bjorner
b0a22105d6 na 2021-07-19 13:28:20 -07:00
Nikolaj Bjorner
188a478214 #5417 
strict inequality (over reals) require solving for least-upper/greatest-lower bounds that may coincide with non-strict inequalities (be epsilon stronger). Instead of using the coefficient 'a' to turn the inequality into an equality, add the slack value as a constant.
 2021-07-19 13:19:03 -07:00