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

3185 commits

Author SHA1 Message Date
Nikolaj Bjorner
ab66239c11 separate linear update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 18:13:16 -07:00
Nikolaj Bjorner
ebbcfafd81 include 5% reset probability 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 17:58:49 -07:00
Nikolaj Bjorner
32c3a5af67 include linear moves 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 17:56:34 -07:00
Nikolaj Bjorner
d6b89ba2d5 make reset updates recursive 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 14:16:34 -07:00
Nikolaj Bjorner
47b793a5e0 disable nested mul, use non-lookahead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:55:43 -07:00
Nikolaj Bjorner
059ccd67bb disable nested mul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:27:09 -07:00
Nikolaj Bjorner
c643672e9f perform lookahead update + nested mul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:25:48 -07:00
Nikolaj Bjorner
29aca5b1d6 flatten products 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:00:50 -07:00
Nikolaj Bjorner
87d556d37d delay factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 10:57:35 -07:00
Nikolaj Bjorner
67d3f3b110 localize impact of factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 10:14:59 -07:00
Nikolaj Bjorner
3c92119b1a disable tabu in fallback modes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 09:55:43 -07:00
Nikolaj Bjorner
11ed99089b remove restart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 09:32:04 -07:00
Nikolaj Bjorner
b2bc51e9ac fix bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 16:44:44 -07:00
Nikolaj Bjorner
0b8177c7d6 generalize factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 16:23:37 -07:00
Nikolaj Bjorner
69dd247cfc re-add tabu override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 09:25:34 -07:00
Nikolaj Bjorner
a2b8b724b2 fixes to semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 09:20:11 -07:00
Nikolaj Bjorner
3884fc7b11 add factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 05:05:10 -07:00
Nikolaj Bjorner
80e7f6d355 disable tabu when using reset moves 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 22:28:50 -07:00
Nikolaj Bjorner
42289c2f44 disable fail restart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 19:51:09 -07:00
Nikolaj Bjorner
988a46dbc4 fix division by 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 17:32:58 -07:00
Nikolaj Bjorner
f6dd6a38cd update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-20 11:51:52 -07:00
Nikolaj Bjorner
8b281b625e updates 2024-08-19 16:04:28 -07:00
Nikolaj Bjorner
de8faa231f fixes to ite and other 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-16 16:48:12 -07:00
Nikolaj Bjorner
98f4b5103e refactor basic plugin and clause generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-15 14:04:03 -07:00
Nikolaj Bjorner
438389771d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-14 16:20:24 -07:00
Nikolaj Bjorner
7d765ddb6b fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-14 15:55:30 -07:00
Nikolaj Bjorner
4978f5a9ac fixes 2024-08-13 21:38:38 -07:00
Nikolaj Bjorner
afef727b88 bug fixes 2024-08-13 14:50:17 -07:00
Nikolaj Bjorner
849385c6a1 bugfixes in sls-arith 2024-08-12 17:42:52 -07:00
Nikolaj Bjorner
8dac67d713 evolve sls arith 2024-08-06 15:07:29 -07:00
Nikolaj Bjorner
fce21981c6 fixes to sls 2024-07-27 03:29:54 +02:00
Nikolaj Bjorner
5e62984178 updates to repair logic, mainly arithmetic 2024-07-21 21:03:14 -07:00
Nikolaj Bjorner
5b0d49cd76 testing / debugging arithmetic 2024-07-19 11:31:43 -07:00
Nikolaj Bjorner
ae55d30961 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 22:26:18 -07:00
Nikolaj Bjorner
6bd2a39fb7 fixes and rename sls-cc to sls-euf-plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 21:45:30 -07:00
Nikolaj Bjorner
5767dfac49 fix build of unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 19:39:59 -07:00
Nikolaj Bjorner
c7f67f9a72 remove stale files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 17:17:39 -07:00
Nikolaj Bjorner
cc208394c3 remove shared attribute 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 14:46:55 -07:00
Nikolaj Bjorner
04ad63c732 fix unit test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 14:45:36 -07:00
Nikolaj Bjorner
428361b22e merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 14:45:03 -07:00
Nikolaj Bjorner
706e6291e3 fix compiler errors for gcc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 12:17:10 -07:00
Nikolaj Bjorner
5f4ca8c6fc use template<> syntax 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 11:11:37 -07:00
Nikolaj Bjorner
ff104c4b13 move definitions to cpp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 11:09:59 -07:00
Nikolaj Bjorner
5a9161ed7b use portable ptr-initializer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-15 11:00:33 -07:00
Nikolaj Bjorner
402fdf667d bv updates 2024-07-14 19:34:24 -07:00
Nikolaj Bjorner
1cd95e9db4 add sls-sms solver 2024-07-14 16:51:06 -07:00
Nikolaj Bjorner
586343ce64 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-14 15:38:56 -07:00
Nikolaj Bjorner
8357ac1cfc adding basic plugin 2024-07-09 19:47:58 -07:00
Nikolaj Bjorner
ef54feec3d porting bv-sls 2024-07-08 13:16:28 -07:00
Nikolaj Bjorner
e7104ebb93 move sat_ddfw to sls, initiate sls-bv-plugin 2024-07-06 20:14:44 -07:00