mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 19:51:22 +00:00
Code Activity
19834 commits 44 branches 51 tags 171 MiB
Commit graph

19834 commits

This branch
This branch
All branches
Author SHA1 Message Date
Copilot
abf92228a1
Merge 12d4ec7eda into ad2934f8cf 2025-07-27 09:20:22 +02:00
Nikolaj Bjorner
ad2934f8cf fix unsound len(substr) axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-26 15:38:25 -07:00
Nikolaj Bjorner
1f8b08108c #7739 optimization 
add simplification rule for at(x, offset) = ""

Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions.
The example highlights some opportunities for simplification, noteworthy at(..) = "".
The example is solved in both versions after adding this simplification.
 2025-07-26 14:02:34 -07:00
Nikolaj Bjorner
8e1a528796 ensure atomic constraints are processed by arithmetic solver 2025-07-26 12:52:48 -07:00
Nikolaj Bjorner
0528c86905 fix #7745 
axioms for len(substr(...)) escaped due to nested rewriting
 2025-07-26 12:30:42 -07:00
Nikolaj Bjorner
95be0cf9ba remove verbose output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-25 20:22:52 -07:00
Nikolaj Bjorner
e54928679f add option to selectively disable variable solving for only ground expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-25 19:15:20 -07:00
Nikolaj Bjorner
1a488bb67a indentation 2025-07-25 11:00:30 -07:00
Nikolaj Bjorner
01633f7ce2 respect smt configuration parameter in elim_unconstrained simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-24 16:22:08 -07:00
Nikolaj Bjorner
a6c51df144 ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-24 14:54:15 -07:00
Nikolaj Bjorner
a2f17420ff moving to active/passive division 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-23 15:22:16 -07:00
Nikolaj Bjorner
44cd38c9ff
Update msvc-static-build.yml 2025-07-23 10:32:56 -07:00
Nikolaj Bjorner
fc51067207 compile warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-21 16:20:08 -07:00
Nikolaj Bjorner
1d1a01c6cc update logging 2025-07-21 16:14:14 -07:00
Nikolaj Bjorner
dbcbc6c3ac revamp ac plugin and plugin propagation 2025-07-21 07:35:06 -07:00
Nikolaj Bjorner
b983524afc add diagnostics instrumentation to mam 2025-07-12 17:52:06 -07:00
Nikolaj Bjorner
383f4db14c update pretty printer to show lambdas 2025-07-12 17:51:37 -07:00
Nikolaj Bjorner
47a2376172 bugfix to ac-plugin 
use list for "shared" should be indices into an array of shared expressions, not the monomial index.
 2025-07-12 17:51:19 -07:00
copilot-swe-agent[bot]
12d4ec7eda Complete datatype implementation with full Context integration and tests 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-07-12 08:09:48 +00:00
copilot-swe-agent[bot]
46f7b5edc8 Implement core datatype functionality with TypeScript compilation success 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-07-12 08:05:57 +00:00
copilot-swe-agent[bot]
695ab0c298 Complete datatype type definitions with working TypeScript compilation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-07-12 07:57:09 +00:00
copilot-swe-agent[bot]
fd9d9a3323 Add datatype type definitions to types.ts (work in progress) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-07-12 07:53:44 +00:00
copilot-swe-agent[bot]
1a03669f95 Initial plan 2025-07-12 07:32:03 +00:00
Nikolaj Bjorner
fd5455422e fix #7725 - proofs are only possible if context was created with proofs enabled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-12 09:14:23 +02:00
LeeYoungJoon
e575919657
debug : Add support for selecting LLDB via invoke on macOS (#7726) 2025-07-12 09:02:09 +02:00
Nikolaj Bjorner
0995928f6e wip - throttle AC completion, enable congruences over bound bodies 
- AC completion which is exposed as an option to the new congruence closure core used roots of E-Graph which gets ordering of monomials out of sync.
- Added injective function handling to AC completion
- Move to model where all equations, also unit to unit are in completion
- throw in first level bound bodies into the E-graph to enable canonization on them.
 2025-07-11 12:48:27 +02:00
Nikolaj Bjorner
35b1d09425 working on ho-matcher 2025-07-08 04:50:43 +02:00
Nikolaj Bjorner
195f3c9110 update build dependencies 2025-07-07 16:50:35 +02:00
Nikolaj Bjorner
0c5b0c3724 turn on ho-matcher for completion 2025-07-07 14:08:51 +02:00
Nikolaj Bjorner
1b3c3c2716 initial pattern abstraction and move matching to src 2025-07-06 00:53:46 -07:00
Nikolaj Bjorner
2d1a42d53f fixes to ho-matcher 2025-07-05 16:24:45 -07:00
Nikolaj Bjorner
3ccf7a695b make concurrent collect_statistics in a timeout thread safe 2025-07-04 18:58:29 -07:00
Nikolaj Bjorner
951554e883 ho matcher draft 
Draft implementation of higher-order matcher.
No specific tuning at this point.
 2025-07-04 18:01:47 -07:00
Nikolaj Bjorner
0ee1ee54bd Update azure-pipelines.yml for Azure Pipelines 
remove build steps for python packaging
 2025-07-04 14:25:53 -07:00
Lev Nachmanson
d2990e2f68 use usize to suppress the data loss warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-07-02 14:42:55 -07:00
Nikolaj Bjorner
f544dd4ab2 deal with warnings 
@levnach - there are some additional warnings.
You could revert the change to std_vector or use usize() that I added to vector.h. Look at build logs from the pipelines or actions or figure out how to add a continuous AI script to fixup build warnings (I tried a few times earlier on but the features available to do this were not for laymen).
 2025-07-02 10:59:56 -07:00
Nikolaj Bjorner
bb100a40d5 c is non-null 2025-07-02 10:57:54 -07:00
Copilot
75678fc2c2
Fix O(n²) performance issue in CLI datatype declaration processing (#7712) 
* Initial plan

* Implement batch initialization fix for O(n²) datatype performance issue

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix the real O(n²) bottleneck with lazy hash table for constructor name lookups

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Optimize get_constructor_by_name: use func_decl* parameter, add linear search optimization for small datatypes, and ensure non-null postcondition

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-07-02 09:54:36 -07:00
LeeYoungJoon
53c48f7226
trace : Sort and reorder trace tags by tag_class and tag_name (#7714) 2025-07-02 09:53:35 -07:00
Nikolaj Bjorner
0218fb75a2 fixup pipleline to support testing packaging 2025-07-02 07:59:23 -07:00
LeeYoungJoon
0928a1fdf0
trace : Classify tag_names unique to smt_internalize.cpp (#7713) 2025-07-01 21:30:07 -07:00
Nikolaj Bjorner
8de80e666b #7710 
partial fix
 2025-07-01 14:23:23 -07:00
Nikolaj Bjorner
97193b4a1d call into collect_statistics in case of -T interrupt 2025-07-01 14:15:15 -07:00
Nikolaj Bjorner
a28f55a3bc log scope level of lemma 2025-07-01 14:14:30 -07:00
Nikolaj Bjorner
bfed237a6c expose scope level 2025-07-01 14:14:16 -07:00
Nikolaj Bjorner
bc96e9e9ae Add python packaging to main pipeline to check updates to sdist 2025-06-30 09:22:01 -07:00
Nikolaj Bjorner
725c0933ad use usize to work around mess with static_cast<unsigned> insertions when looping over small vectors 2025-06-30 09:04:47 -07:00
Nikolaj Bjorner
a73e244db4 nits 2025-06-30 08:37:39 -07:00
Nikolaj Bjorner
661ccb3702
Revert "Fix source installation to create dist-info directory for package dis…" (#7704) 
This reverts commit ad0afbb792.
 2025-06-29 09:11:32 -07:00
Nikolaj Bjorner
b1259fb6ce Update nightly.yaml for Azure Pipelines 2025-06-28 16:11:16 -07:00