Nikolaj Bjorner
d8fafd8731
Update euf_ac_plugin.cpp
...
include reduction rules in forward simplification
2025-08-03 14:17:00 -07:00
Nuno Lopes
f23b053fb9
remove a bunch of string copies
2025-08-03 10:41:38 +01:00
Nuno Lopes
97aa46add3
remove default constructor
2025-08-03 09:52:53 +01:00
Nikolaj Bjorner
89cc9bd333
disable pre-processing during cubing
2025-07-31 20:58:58 -07:00
Nikolaj Bjorner
2d876d5af1
allow for internalize implies
2025-07-31 20:48:15 -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
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
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
