Nikolaj Bjorner
4eeb98d294
Merge branch 'ilana' into parallel-solving
2025-07-28 19:53:51 -07:00
Ilana Shapiro
f607a704ec
Merge branch 'Z3Prover:master' into parallel-solving
2025-07-28 16:45:45 -07:00
Ilana Shapiro
36fbee3a2d
add top-k fixed-sized min-heap priority queue for top scoring literals
2025-07-27 18:12:07 -07:00
Nikolaj Bjorner
f77123c13c
enable passive, add check for bloom up-to-date
2025-07-27 17:18:23 -07:00
Nikolaj Bjorner
67695b4cd6
updates to ac-plugin
...
fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop.
2025-07-27 13:38:37 -07:00
Nikolaj Bjorner
07613942da
Add parameter validation for selected API functions
2025-07-27 13:38:37 -07:00
Nikolaj Bjorner
e3139d4e03
#7750
...
add pre-processing simplification
2025-07-27 13:38:36 -07:00
humnrdble
eb24488c3e
FreshConst is_sort ( #7748 )
2025-07-27 03:19:43 -07:00
Nikolaj Bjorner
a9b4e35938
Update PARALLEL_PROJECT_NOTES.md
2025-07-26 17:44:29 -07:00
Nikolaj Bjorner
9d0a2ae355
Update PARALLEL_PROJECT_NOTES.md
2025-07-26 17:40:43 -07: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
27c1ffc7fb
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 20:17:19 -07:00
Nikolaj Bjorner
4c229d057d
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 20:16:12 -07:00
Nikolaj Bjorner
c3da87ca12
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 20:15:29 -07:00
Nikolaj Bjorner
964363504c
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 20:13:06 -07:00
Nikolaj Bjorner
f6ec7f5381
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 20:03:52 -07:00
Nikolaj Bjorner
82b4c3ea23
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 20:02:37 -07:00
Nikolaj Bjorner
e1eb3ace3c
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 19:35:51 -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
f2ff0adc79
more notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-07-25 15:52:46 -07:00
Nikolaj Bjorner
9bba708f9b
fix compilation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-07-25 15:36:46 -07:00
Ilana Shapiro
65504953f7
add bash files for test runs
2025-07-25 15:34:26 -07:00
Nikolaj Bjorner
f6fc5045d2
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 15:12:13 -07:00
Nikolaj Bjorner
202807b317
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 15:09:03 -07:00
Nikolaj Bjorner
e732354259
Update PARALLEL_PROJECT_NOTES.md
2025-07-25 15:00:32 -07:00
Nikolaj Bjorner
138ac63dd0
added notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-07-25 11:23:05 -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
Ilana Shapiro
4b87458ce2
Merge remote-tracking branch 'upstream/ilana' into parallel-solving
2025-07-24 11:52:21 -07:00
Ilana Shapiro
563906dcdb
Merge branch 'Z3Prover:master' into parallel-solving
2025-07-24 11:48:01 -07:00
Nikolaj Bjorner
ac857aaf72
add score access and reset
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-07-23 15:32:49 -07:00
Ilana Shapiro
20b9690b01
very basic setup ( #7741 )
2025-07-23 15:26:02 -07:00
Ilana Shapiro
41b5c64c80
very basic setup
2025-07-23 15:24:12 -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
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
