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

19127 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 487a544274 remove test code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-29 21:05:41 -07:00
Nikolaj Bjorner fd66d2f26c better equality solver for bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-29 21:02:57 -07:00
Jakob Rath 16fb86b636 separate scope 2024-05-15 11:36:06 +02:00
Jakob Rath 865822651c patch to deal with prefix wrap-around 2024-05-15 11:34:51 +02:00
Jakob Rath 343d693929 reduce output 2024-05-15 10:15:25 +02:00
Jakob Rath f4d5bd5cd1 fix fixed-prefix constraint again 2024-05-15 09:50:59 +02:00
Jakob Rath 8d4c4ac475 fix intblast sign_ext 2024-05-14 21:36:17 +02:00
Jakob Rath a4f14fa29f fix prefix constraint 2024-05-14 19:33:32 +02:00
Jakob Rath 1f686126a3 guard against stale explain_kind 2024-05-14 19:16:31 +02:00
Jakob Rath 962edfd03c set proper explain_kind in case of full interval 2024-05-14 19:13:34 +02:00
Jakob Rath 47d93037f7 fix prefix 2024-05-14 18:54:29 +02:00
Jakob Rath 705d94d883 reduce output 2024-05-14 16:44:44 +02:00
Jakob Rath ec0224912b enable 2024-05-14 16:37:40 +02:00
Jakob Rath 5b8c6a98c2 fix? 2024-05-14 16:34:31 +02:00
Jakob Rath 38745512c0 first attempt at new explain_overlap 2024-05-14 16:22:57 +02:00
Jakob Rath 764ccebcbf Add constraints::fixed 2024-05-14 15:03:30 +02:00
Jakob Rath cc799bbfc1 fix sign_extend 2024-05-14 10:57:25 +02:00
Jakob Rath b640ea775a begin updated viable-conflict 
copy explain_overlap
 2024-05-14 10:40:26 +02:00
Jakob Rath 1292fb2adb extra px < qx axioms 2024-05-13 22:46:49 +02:00
Jakob Rath d28441bd8f Add additional ashr axiom 2024-05-13 15:21:17 +02:00
Jakob Rath fb5a40a6fd fix sle 2024-05-13 15:14:49 +02:00
Jakob Rath 94955e3fae Merge remote-tracking branch 'origin/master' into poly 2024-05-11 23:30:53 +02:00
Jakob Rath a3c85d3a60 subsumption hotfix 2024-05-11 17:54:59 +02:00
Jakob Rath 2494ffacaf print validation num_check 2024-05-11 14:23:54 +02:00
Jakob Rath c3ffbf05db fix bv type error in projection check 2024-05-11 14:16:18 +02:00
Jakob Rath d335b6b035 add missing include 2024-05-11 12:44:57 +02:00
Jakob Rath f904c08116 enable the saturation rules 2024-05-10 14:59:19 +02:00
Nikolaj Bjorner efc893263a add abs function to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-05-09 20:54:39 -07:00
Nikolaj Bjorner b120745078 add C++ bindings for sequence operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-05-09 20:20:05 -07:00
Nikolaj Bjorner c7529d0b25 expose fold as well 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-05-09 14:56:18 -07:00
Nikolaj Bjorner fc6c4c98e2 initial warppers for seq-map/seq-fold 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-05-09 14:52:49 -07:00
Nikolaj Bjorner f9176fb4b7
Update README.md 2024-05-07 11:39:52 -07:00
Jakob Rath 7925ef731f relax eq_resolve conditions 
fixes Example 1
 2024-05-06 15:24:00 +02:00
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
Nikolaj Bjorner 8f4ffc7caf add logging for first conflict 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-05-01 20:50:52 -07:00
Nikolaj Bjorner 2f02278227 add virtual destructor to z3::object class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-05-01 16:35:25 -07:00
Nikolaj Bjorner 19eb7225ea add virtual destructor to z3::object class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-05-01 16:20:05 -07:00
Nikolaj Bjorner 231a985bf9 add virtual destructor to z3::object class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-05-01 16:17:06 -07:00
Nikolaj Bjorner 04c55c34e5 fix unsoundness bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-05-01 14:45:15 -07:00
Nikolaj Bjorner 869643a551 fix memory leak 2024-05-01 10:07:37 -07:00
Nikolaj Bjorner 1ef4354080 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-04-30 17:52:00 -07:00
Nikolaj Bjorner aa1a596394 add doc-string 2024-04-30 17:05:40 -07:00
Nikolaj Bjorner 29e724f787 add gc to lemmas, convert bounds constraints to lemmas, add simplification pre-processing beyond equality extraction 2024-04-30 17:05:21 -07:00
Nikolaj Bjorner b0222cbdaa temper warning messages from uninitalized pointers 2024-04-30 17:00:49 -07:00
Nikolaj Bjorner 4c070f9e76 add extra fields to nlsat-clause 2024-04-30 17:00:05 -07:00
Nikolaj Bjorner 39dc8861ee expose comparisons with polynomials, incremental way to extract variables 2024-04-30 16:59:50 -07:00
Nikolaj Bjorner bc577b93ae refine precision before taking closest integral value. 2024-04-30 16:58:22 -07:00
Nikolaj Bjorner 2ad9f220f2 add logging 2024-04-30 16:57:59 -07:00