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

19050 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath 0a8879b505 also normalize or_op 2024-05-06 13:26:17 +02:00
Jakob Rath c7a80eaf5d port additional simplification from polysat branch 2024-05-06 13:16:10 +02:00
Jakob Rath 7a3349eeae disable assertions for now 2024-05-03 10:03:03 +02:00
Jakob Rath f8c593edf9 remove unused ckind_t::smul_fl_t 2024-04-23 14:38:33 +02:00
Jakob Rath 69ea52407f refactor, update comment 2024-04-15 11:18:42 +02:00
Jakob Rath 06e5595e87 revert for now 2024-04-12 14:35:12 +02:00
Jakob Rath 183f96b481 explain_hole_overlap wip 2024-04-11 11:26:07 +02:00
Jakob Rath 138c90d52b explain_overlap, notes on case ebw < abw 2024-04-11 11:19:49 +02:00
Jakob Rath adea39b92e dbg output 2024-04-11 11:12:49 +02:00
Jakob Rath 020a4d5d04 r_interval::contains 2024-04-11 11:11:02 +02:00
Jakob Rath 3f3b052933 move modification to the front 2024-04-04 10:28:08 +02:00
Jakob Rath 2b89767d1f ensure smaller layers are visited first 2024-04-03 18:25:18 +02:00
Jakob Rath 18eeb48b34 invalidated reference 2024-04-03 17:58:35 +02:00
Jakob Rath b808dece15 always restart find_overlap at smallest size 2024-04-03 17:38:43 +02:00
Jakob Rath 583c40de1f check 2024-04-03 16:42:17 +02:00
Jakob Rath 4a51139bc8 fix marking for redundancy 2024-04-03 16:41:21 +02:00
Jakob Rath 017ae78c81 enable removal of redundant explanations 2024-04-03 15:38:33 +02:00
Jakob Rath c5b02f8360 simplify side conditions on reduced intervals 2024-04-03 15:38:33 +02:00
Jakob Rath d19de4b1d3 fixed_bits notes 2024-04-03 15:38:33 +02:00
Jakob Rath 60422d2071 separate terminology (suffix vs. overlap) 2024-04-02 16:34:49 +02:00
Jakob Rath 17131983fe use loop instead of goto 2024-04-02 16:31:51 +02:00
Jakob Rath 88be5e6611 check hole_len 2024-04-02 16:28:45 +02:00
Jakob Rath 47f28c6857 find_overlap should stay on lower bit-width to find conflicts 2024-04-02 16:27:29 +02:00
Jakob Rath f127d12e4c remove redundant intervals (disabled for now) 2024-04-02 15:10:12 +02:00
Nikolaj Bjorner b07cb3dc54 use C++23 conventions in buffer.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-30 16:26:19 -07:00
Jakob Rath 287d772ff6 WIP: add missing conditions on size of "holes" 
when combining intervals of different bit widths
 2024-03-28 16:48:35 +01:00
Jakob Rath 0d3e88fd31 display_explain 2024-03-28 16:38:41 +01:00
Jakob Rath a7c84da44d Fix monomials::parity 2024-03-27 10:49:02 +01:00
Jakob Rath e22c86acb6 fixed_slice display 2024-03-25 14:34:06 +01:00
Jakob Rath 8a23523f20 fix crash on EBxzQox7raUO.smt2 2024-03-25 13:20:24 +01:00
Nikolaj Bjorner ac6554eb92 set C++ version to 20 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-21 10:59:31 -07:00
Nikolaj Bjorner 182979771f disable verbose 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-21 10:41:31 -07:00
Jakob Rath 934b2ad5ef update target selection to what was intended 2024-03-21 13:53:26 +01:00
Jakob Rath 342db52558 fix 2024-03-21 12:03:52 +01:00
Jakob Rath acd05686e4 relevant level should be based on what's to appear in the lemma 2024-03-21 11:05:55 +01:00
Jakob Rath 7d1a57b6e9 remove commented code 2024-03-20 15:38:42 +01:00
Jakob Rath 7922ee3e82 debug output 2024-03-20 15:37:34 +01:00
Jakob Rath fd9c931168 skip entry for origin variable 2024-03-20 15:37:03 +01:00
Jakob Rath 23ca9d9fc5 select targets, try generic/specific version of projection 2024-03-20 15:26:33 +01:00
Jakob Rath de809932eb refactor, minor fixes 2024-03-20 14:33:30 +01:00
Jakob Rath ef6b5f82d1 relax level constraint 2024-03-20 13:39:16 +01:00
Jakob Rath 91a9feb5a8 warnings 2024-03-20 12:16:24 +01:00
Jakob Rath f47fbdd714 Move interval projection out of viable 2024-03-20 12:11:14 +01:00
Jakob Rath 5339a2f70f Don't access solver_interface directly 2024-03-20 10:16:40 +01:00
Jakob Rath a34bb99db3 Use variable from violated interval as origin 2024-03-20 10:15:25 +01:00
Jakob Rath 3a11350142 Move helper functions 2024-03-20 10:10:27 +01:00
Nikolaj Bjorner 6eeb022048 fix encoding for sdiv exposed by zQkAOXjEDwgm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-19 16:00:09 -07:00
Nikolaj Bjorner ffe7b46e74 unsigned cast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-19 15:02:42 -07:00
Jakob Rath f5eb457bee fix propagate_from_containing_slice dependency 2024-03-19 16:13:28 +01:00
Jakob Rath 489a1495d2 dep 2024-03-19 14:23:44 +01:00