mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-21 16:16:38 +00:00
Code Activity
19480 commits 23 branches 48 tags 157 MiB
Commit graph

19480 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath 555ac49023 shortcut 2023-12-01 15:23:48 +01:00
Jakob Rath 878d4a2fd0 Collect relevant entries 2023-12-01 15:18:57 +01:00
Jakob Rath 7987ac4475 check for full intervals 2023-12-01 15:14:16 +01:00
Jakob Rath a3bf994aa4 viable: store origin pvar in entry 2023-12-01 13:19:20 +01:00
Jakob Rath 828f74db73 slicing::explain_simple_overlap 2023-12-01 13:15:45 +01:00
Jakob Rath cf9b7bed0c imports 2023-11-29 16:03:47 +01:00
Jakob Rath e76c6b0fdc fix test 2023-11-29 15:04:23 +01:00
Jakob Rath 872459170f viable fallback with overlaps 2023-11-29 15:04:23 +01:00
Jakob Rath 27bc858509 univariate solver: support constraints on lower bits 2023-11-29 15:04:23 +01:00
Jakob Rath c29d04d431 fix compiler error (2) 2023-11-29 15:04:23 +01:00
Jakob Rath 923e4b4bd9 fix compile error 2023-11-29 15:04:23 +01:00
Jakob Rath 79d77bc690 exit conditions 2023-11-29 15:04:23 +01:00
Jakob Rath 590e9b0fb1 outer loop, to continue search after recursive call 2023-11-29 15:04:23 +01:00
Jakob Rath 5d3a5a94e8 update progress 2023-11-29 15:04:23 +01:00
Jakob Rath 179da49379 fix 2023-11-29 15:04:23 +01:00
Jakob Rath 0b98a76177 refinement 2023-11-29 15:04:23 +01:00
Jakob Rath 203df6babb fix recursion in case of large gap 2023-11-29 15:04:23 +01:00
Jakob Rath 39bee180de store bit-intervals that were used 2023-11-29 15:04:23 +01:00
Jakob Rath 3740e766f7 check bits for next_val 2023-11-29 15:04:23 +01:00
Jakob Rath 2a3c8d2b82 find_on_layer: refactor interval loop 2023-11-29 15:04:22 +01:00
Jakob Rath 91a47b262b find_on_layer: fixed bits refinement 2023-11-29 15:04:22 +01:00
Jakob Rath 6fa3af29c6 return entry from refine_bits 2023-11-29 15:04:22 +01:00
Jakob Rath 3b1836ea1e fixed bits tests 2023-11-29 15:04:22 +01:00
Jakob Rath bd48a63a07 Update extend_by_bits argument 2023-11-29 15:04:22 +01:00
Nikolaj Bjorner a805e1f27d fixes to AC plugin 2023-11-28 12:50:43 -08:00
Nikolaj Bjorner 14483dcd6e n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-20 16:15:30 -08:00
Nikolaj Bjorner 6a572543b4 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-20 15:54:00 -08:00
Nikolaj Bjorner cbefe74219 hastwo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-18 15:41:18 -08:00
Nikolaj Bjorner 7ad8c6a6ce na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-15 17:56:45 -08:00
Nikolaj Bjorner a76aca57f0 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-15 17:03:41 -08:00
Nikolaj Bjorner 108275dcd9 n/a 2023-11-15 15:00:02 -08:00
Nikolaj Bjorner bf5e6936c0 updated AC simplification 2023-11-15 11:01:51 -08:00
Nikolaj Bjorner d5315e2283 prepare for subsumption 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-14 10:56:01 -08:00
Nikolaj Bjorner 616d00409f updates to AC plugin, notes in BV plugin 2023-11-14 00:52:46 -08:00
Nikolaj Bjorner 54909f8755 use uint set to track superset of equations that are in simplified state 2023-11-13 01:15:37 -08:00
Nikolaj Bjorner 654dce3dc4 bug fixes 2023-11-12 17:35:42 -08:00
Nikolaj Bjorner 5c71824f2b adding unit test for arith_plugin 2023-11-12 16:48:10 -08:00
Nikolaj Bjorner 65a8c162f5 add E(T) functionality for bv and ac functions 
Add an option to register EUF modulo theories,
The current theory with a unit test is BV.
The arithmetic theory plugs into an AC completion. It is partially finished, pending setting up testing and implementing handling of shared terms.
 2023-11-12 15:39:56 -08:00
Jakob Rath 9ce47ab460 fix recursion 2023-11-10 10:57:02 +01:00
Jakob Rath 115a82cd82 Fix helper function viable::find_value 2023-11-10 10:54:31 +01:00
Jakob Rath 5a03d13913 viable::test3 2023-11-10 10:53:15 +01:00
Jakob Rath b7ee4b0d63 dtrim 2023-11-09 16:40:47 +01:00
Jakob Rath fc676e235f fix some bugs, add unit test 2023-11-09 15:03:14 +01:00
Jakob Rath d3d0a5f635 compile 2023-11-09 13:03:14 +01:00
Jakob Rath e45358d9be viable algorithm sketch 2023-11-09 11:33:13 +01:00
Jakob Rath e393c2fe9b r_interval, distance 2023-11-09 11:28:01 +01:00
Jakob Rath 4efb06c60b get comments out of the way 2023-11-07 16:20:45 +01:00
Jakob Rath be0e6c3267 viable plan 2023-11-07 13:17:15 +01:00
Jakob Rath f51b194017 remove overly strict assertion 2023-11-07 13:14:55 +01:00
Jakob Rath 3796a46b55 log 2023-11-06 15:58:07 +01:00