mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity
15525 commits 23 branches 48 tags 156 MiB
Commit graph

15525 commits

Author SHA1 Message Date
Nikolaj Bjorner db5252a81b add dummy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-29 11:31:39 -07:00
Nikolaj Bjorner 16413b4f9a 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 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 2021-07-26 13:47:21 -07:00
Nikolaj Bjorner 5652d2a157 2021-07-25 11:59:42 -07:00
Nikolaj Bjorner b638405e42 simplify 
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 ...)) () 2021-07-25 09:51:48 -07:00
Nikolaj Bjorner 2fa156eaf4 2021-07-25 09:36:45 -07:00
Nikolaj Bjorner 10145366b2 
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 2021-07-22 18:31:37 -07:00
Nikolaj Bjorner 848a8ebb98 2021-07-22 13:35:54 -07:00
Nikolaj Bjorner 2589f2bad4 2021-07-22 12:07:11 -07:00
Nikolaj Bjorner 76427cd281 2021-07-22 11:33:47 -07:00
Nikolaj Bjorner 9a5c0f2312 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 2021-07-21 09:08:55 -07:00
Nikolaj Bjorner 005d35f9c9 2021-07-21 07:39:39 -07:00
Nikolaj Bjorner ca8f914dd8 2021-07-21 07:22:05 -07:00
Nikolaj Bjorner e5e7c510d5 2021-07-21 07:14:54 -07:00
Nikolaj Bjorner 8a4b292f3e 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 2021-07-20 15:29:24 -07:00
Nikolaj Bjorner 134562162a 2021-07-20 13:50:21 -07:00
Nikolaj Bjorner 614cb26489 2021-07-20 11:44:57 -07:00
Nikolaj Bjorner 89ed19a719 2021-07-20 11:20:16 -07:00
Nikolaj Bjorner b84b5d091e 2021-07-20 08:02:21 -07:00
Nikolaj Bjorner f90795c42f 2021-07-20 07:58:21 -07:00
Nikolaj Bjorner 49bd3ad159 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 2021-07-19 16:09:13 -07:00
Nikolaj Bjorner a8b433e6ac 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-19 15:58:10 -07:00
Nikolaj Bjorner a64867942d designate quantifier axioms as auxiliary 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-19 15:35:18 -07:00
Nikolaj Bjorner 4388ab2e3e 
more gracefully handle non-implemented theories
 2021-07-19 13:50:20 -07:00
Nikolaj Bjorner 0a34eef470 2021-07-19 13:41:02 -07:00
Nikolaj Bjorner b0a22105d6 na 2021-07-19 13:28:20 -07:00
Nikolaj Bjorner 188a478214 
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 extend definition of ground to be variable free 2021-07-19 11:38:04 -07:00
Nikolaj Bjorner 3156ca5e77 - 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 normalize clause 2021-07-19 09:08:51 -07:00
Nikolaj Bjorner 7d915eb295 - 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 
https://github.com/Z3Prover/z3/issues/5417#issuecomment-882050602
 2021-07-18 10:44:30 -07:00
Nikolaj Bjorner 750c06e258 2021-07-18 10:21:42 -07:00
Nikolaj Bjorner 284d599788 
https://github.com/Z3Prover/z3/issues/5323#issuecomment-866503616
 2021-07-18 05:14:14 -07:00
Nikolaj Bjorner cde3eac7be 2021-07-18 13:45:21 +02:00
Nikolaj Bjorner ce1c8ee9e3 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-18 12:32:27 +02:00
Nikolaj Bjorner e0cb24867f Merge branch 'master' of https://github.com/z3prover/z3 2021-07-18 12:31:23 +02:00
Nikolaj Bjorner f239aeb4d4 add consequences forcing character values to be digits 2021-07-18 12:30:56 +02:00