mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity
19510 commits 22 branches 48 tags 156 MiB
Commit graph

19510 commits

This branch
This branch
All branches
Author SHA1 Message Date
Clemens Eisenhofer 9557e7cacf
Minor (#7540) 2025-01-31 08:22:30 -08:00
Nikolaj Bjorner 1ce6e66ac9 generalize logic detection to use sub-string matching 2025-01-30 16:34:54 -08:00
Nikolaj Bjorner eb825855fa increase the log level on callbacks with bit-indices that get set 2025-01-30 16:34:36 -08:00
Nikolaj Bjorner c9ac4d6f75 pre-flatten use list before iterating over m_unsat 
select_max_same_sign accesses the use-list which may cause it to be flattened.
 2025-01-30 16:34:17 -08:00
Nikolaj Bjorner e3566288a4 fixes based on benchmarking UFDTLIA/NIA/BV 2025-01-29 17:00:26 -08:00
Nikolaj Bjorner f1e0950069 fix several crashes exposed by QF_UFDTNIA benchmark sets 2025-01-29 16:23:38 -08:00
Nikolaj Bjorner bfe4673dac this check is not an invariant in the first place 
but nice to have.
 2025-01-29 16:23:18 -08:00
Nikolaj Bjorner 51357f6d06 Add selective filter on Ackerman axioms 2025-01-29 11:42:50 -08:00
Clemens Eisenhofer c2a0919f79
Removed no progress case in seq-sls (#7537) 2025-01-29 09:43:57 -08:00
Nikolaj Bjorner 6d3cfb63da add eval1 functionality for replace_all 2025-01-29 04:36:55 -08:00
Nikolaj Bjorner ab43d2dcf1 fix semantics of check-int64 div operation to align with smtlib semantics 2025-01-29 04:29:38 -08:00
Nikolaj Bjorner 30d72f79ac remove verbose output of overflow 2025-01-29 03:48:11 -08:00
Nikolaj Bjorner 3379155a63 add check for root literal assignment 2025-01-29 03:14:14 -08:00
Nikolaj Bjorner fe5d17d515 handle exception internally, avoid passing rationals to integer operations 2025-01-28 20:09:59 -08:00
Nikolaj Bjorner 5b175c1bcd fix crashes in sls_datatype 2025-01-28 19:24:32 -08:00
Nikolaj Bjorner fe713eb8e9 disable quadratic moves for non-integers as sqrt isn't currently defined for rationals 2025-01-28 16:53:12 -08:00
Nikolaj Bjorner d8430810fe fix mixup between sync and sls managed variables 2025-01-28 16:35:50 -08:00
Nikolaj Bjorner fa605454fb fix crash reported by Nikhil on F* due to unhandled exception while using the rewriter during search 2025-01-28 16:27:28 -08:00
Nikolaj Bjorner 5c2a9d9936 fix pickup of new constraints 2025-01-28 15:04:13 -08:00
Nikolaj Bjorner 1676378be9 skip last power 2025-01-28 15:03:01 -08:00
Nikolaj Bjorner 8a7d971264 Update sls_bv_lookahead.h 2025-01-28 15:02:45 -08:00
Nikolaj Bjorner 2ebc647079 skip update stack items that are not Bool/bv 2025-01-28 15:02:33 -08:00
Nikolaj Bjorner 632e2b56e4 fix initialization of mod terms 2025-01-28 15:01:50 -08:00
Nikolaj Bjorner fd5f5feb40 add cmake option to turn on asan 2025-01-28 15:01:31 -08:00
Nikolaj Bjorner a8279dd9d5 reset kv map consistently with egraph 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 17:09:38 -08:00
Nikolaj Bjorner 57a5474ab4 revert flat default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 16:56:12 -08:00
Nikolaj Bjorner 72ae161307 compress store array before model-eval rewriter sees it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 16:55:07 -08:00
Nikolaj Bjorner fe1622b592 sls fixes for ABV. Axiomatization required as saturation can produce conflicts by congruence closure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 15:16:13 -08:00
Jonáš Fiala 2050fc3b35
Preserve fingerprint in trace (#7534) 2025-01-27 13:09:48 -08:00
Can Cebeci 2d8f024680
Mark fixed_eq literals as relevant (#7533) 2025-01-27 11:10:46 -08:00
Nikolaj Bjorner 63f9fdaf3e fix build 2025-01-27 10:52:21 -08:00
Nikolaj Bjorner 15ee879602 fix #7532 2025-01-27 10:51:12 -08:00
Nikolaj Bjorner b6e7b80704 updates to handle bugs exposed by qf-abv for local search 
- ctx.is_true(e) - changed to work with expressions that are not literals, but come from top-level assertions
- set fixed in sls_bv_fixed to work with non-zero low order bits
- array plugin to deal with cases where e-graph is inconsistent after a merge.
 2025-01-27 10:35:29 -08:00
Nikolaj Bjorner 7ffed8613a fix bug with handling theory symbols of bit-vector type. Happens for data-type accessors. Reported by Clemens Eisenhofer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 08:22:33 -08:00
Nikolaj Bjorner 09e84e0448 fix crash when accessing bool-info vars, reported by Clemens Eisenhofer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 07:28:20 -08:00
Hari Govind V K f574950237
fix #7521 (#7531) 2025-01-26 17:52:06 -08:00
Nikolaj Bjorner 5634dc5875 fix model construction bug: ignore non-relevant expressions when building model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-26 17:50:15 -08:00
Nikolaj Bjorner d3bf25ce85 throttle value smt -> sls 2025-01-26 14:16:43 -08:00
Nikolaj Bjorner d4100fc472 fixes to update propagation. 
rename update and update_args_value to
update_checked
update_unchecked

ensure upward propagation so that local values are consistent when entering lookahead solvers.
 2025-01-26 12:55:03 -08:00
Nikolaj Bjorner 04d0e9492b set log level of revert repair down to 3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-26 11:56:59 -08:00
Nikolaj Bjorner 55fc57b5c7 relax out of range restrictions to handle large intervals 2025-01-26 11:24:26 -08:00
Nikolaj Bjorner 4f2272dbb2 increase log level for 'set value failed' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-25 23:43:53 -08:00
Nikolaj Bjorner 7fb6497ce1 fix return value when in external mode bool-flip 
return null_bool_var instead of false (= 0).
 2025-01-25 22:57:58 -08:00
Nikolaj Bjorner d4f2de734b add smt_params dependency to sls in cmakelists 2025-01-25 22:38:32 -08:00
Nikolaj Bjorner 12e8082d86 consolidate functionality 2025-01-25 22:34:58 -08:00
Nikolaj Bjorner a7010574c8 align use_list with number of variables during flatten, push clause and bool_vars_of addition into clause and atom creation time. 2025-01-25 20:47:57 -08:00
Nikolaj Bjorner 7fc59b65ad add recursive updates to lookahead 2025-01-25 16:10:00 -08:00
Nikolaj Bjorner 57cb988461 fix gcc build 2025-01-25 15:51:58 -08:00
Nikolaj Bjorner 60fb53ad34 fix debug build 2025-01-25 15:50:07 -08:00
Nikolaj Bjorner ecc302bdc8 fix trace build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-25 11:38:58 -08:00