mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Code Activity
15528 commits 23 branches 48 tags 156 MiB
Commit graph

15528 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner 49b94a0090 #5417 extend definition of ground to be variable free 2021-07-19 11:38:04 -07:00
Nikolaj Bjorner 3156ca5e77 #5417 - delay propagation from callbacks from mam 
mam assumes the egraph isn't updated during callbacks.
 2021-07-19 11:10:48 -07:00
Nikolaj Bjorner 776f270b64 #5417 normalize clause 2021-07-19 09:08:51 -07:00
Nikolaj Bjorner 7d915eb295 #5417 - revise q_eval based on bug based on non-chronological dependencies with post-hoc explain function 2021-07-19 07:40:46 -07:00
Nikolaj Bjorner e8bc9f3469 #5417 
https://github.com/Z3Prover/z3/issues/5417#issuecomment-882050602
 2021-07-18 10:44:30 -07:00
Nikolaj Bjorner 750c06e258 #5417 2021-07-18 10:21:42 -07:00
Nikolaj Bjorner 284d599788 #5323 
https://github.com/Z3Prover/z3/issues/5323#issuecomment-866503616
 2021-07-18 05:14:14 -07:00
Nikolaj Bjorner cde3eac7be #5323 2021-07-18 13:45:21 +02:00