CEisenhofer
c1c6276ae2
Trying different update generation function
2024-12-27 18:11:48 +01:00
CEisenhofer
1cd5e22d66
One check was missing
2024-12-27 14:54:27 +01:00
CEisenhofer
9d7ce8e779
Removed debug code
2024-12-27 14:29:41 +01:00
CEisenhofer
2a0c1dce18
Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping
2024-12-27 13:54:29 +01:00
Nikolaj Bjorner
5eb71c3be6
integrate lookahead v1 into repair loop
...
this ports some functionality from lookahead solver for qfbv-sls into sls-smt.
2024-12-26 17:49:30 -08:00
Nikolaj Bjorner
c58171478f
remove dead code
2024-12-26 13:48:55 -08:00
Nikolaj Bjorner
d3a6521185
rely on is_sat fallback for failed repair-up, add separate file for WIP on lookahead.
2024-12-26 13:06:28 -08:00
Nikolaj Bjorner
13dcfd26dd
remove debug out
2024-12-25 15:23:47 -08:00
Nikolaj Bjorner
c9cae77304
update regex membership to be slightly better tuned
2024-12-25 10:56:16 -08:00
Nikolaj Bjorner
f4ed432244
try a basic heuristic that finds some string that belongs to re.
2024-12-25 10:10:59 -08:00
Nikolaj Bjorner
09825edcd8
remove compute depth in favor of already existing get_depth
2024-12-23 18:49:54 -08:00
Nikolaj Bjorner
e332904fb2
cosmetic updates
2024-12-23 18:49:38 -08:00
Nikolaj Bjorner
85d3041a80
avoid platform non-reproducibility due to argument evaluation ordering
2024-12-23 17:13:51 -08:00
Nikolaj Bjorner
23c4728d68
remove some platform specific behavior
2024-12-23 16:28:10 -08:00
Nikolaj Bjorner
554191885e
remove platform dependent print
2024-12-23 16:13:36 -08:00
Nikolaj Bjorner
4f4cafbc98
start update with expr-inverter to handle PB
2024-12-22 18:17:42 -08:00
Nikolaj Bjorner
b592ce4707
reserve space in heap to avoid debug check in elim_unconstrained
2024-12-22 18:17:40 -08:00
Nuno Lopes
97c70ba501
remove some uneeded constructors
2024-12-22 15:06:58 +00:00
Nikolaj Bjorner
fb5bbb8074
read laziness parameter modulo relvancy to avoid race conditions with setting relevancy = 0
2024-12-22 14:07:29 +01:00
Nikolaj Bjorner
a214dc32e8
add some comments, fix nyis
2024-12-22 13:52:19 +01:00
Nikolaj Bjorner
65b678dd42
use bail_out instead of early return to ensure marks are cleared
2024-12-22 06:14:38 +01:00
Nikolaj Bjorner
78ce6c1c6c
revert relevancy override
2024-12-21 18:10:10 +01:00
Nikolaj Bjorner
3b2315d771
remove verbose output
2024-12-21 15:52:57 +01:00
Nikolaj Bjorner
578804acf4
fix #7460
2024-12-21 14:42:23 +01:00
Nikolaj Bjorner
2044fb460d
fix #7490
2024-12-21 14:32:02 +01:00
Nikolaj Bjorner
8dec84110b
add lia2card tactic as default #7483
2024-12-21 13:11:22 +01:00
Nikolaj Bjorner
4f7b6c794e
always copy Microsoft.Z3.xml into package directory #7482
2024-12-21 13:10:05 +01:00
Nikolaj Bjorner
07b1ee5dcc
mask regression on fpa by not auto-setting relevancy=0
2024-12-21 12:41:04 +01:00
Nikolaj Bjorner
da6a5facca
revert change to setup_context that delays it until there are assertions
2024-12-21 11:53:46 +01:00
Nikolaj Bjorner
db9f45dfec
set relevancy = 0 in auto-config mode when there are bit-vectors and no quantifiers, #7484
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-20 18:10:46 +01:00
Nikolaj Bjorner
114cae50a5
update gcm script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-20 17:27:21 +01:00
Nikolaj Bjorner
87f7a20e14
Add (updated and general) solve_for functionality for arithmetic, add congruence_explain to API to retrieve explanation for why two terms are congruent Tweak handling of smt.qi.max_instantations
...
Add API solve_for(vars).
It takes a list of variables and returns a triangular solved form for the variables.
Currently for arithmetic. The solved form is a list with elements of the form (var, term, guard).
Variables solved in the tail of the list do not occur before in the list.
For example it can return a solution [(x, z, True), (y, x + z, True)] because first x was solved to be z,
then y was solved to be x + z which is the same as 2z.
Add congruent_explain that retuns an explanation for congruent terms.
Terms congruent in the final state after calling SimpleSolver().check() can be queried for
an explanation, i.e., a list of literals that collectively entail the equality under congruence closure.
The literals are asserted in the final state of search.
Adjust smt_context cancellation for the smt.qi.max_instantiations parameter.
It gets checked when qi-queue elements are consumed.
Prior it was checked on insertion time, which didn't allow for processing as many
instantations as there were in the queue. Moreover, it would not cancel the solver.
So it would keep adding instantations to the queue when it was full / depleted the
configuration limit.
2024-12-19 23:27:57 +01:00
Nuno Lopes
e4ab2944fe
Optimize expr_safe_replace for quantifiers when all source patterns are vars ( #7481 )
...
* Update expr_safe_replace.cpp
* Update expr_safe_replace.cpp
* Update expr_safe_replace.cpp
2024-12-19 23:05:13 +01:00
Nuno Lopes
c33bc2c8be
expr_abstract: save 1 hashtable lookup per app argument
...
when we already know that the app is missing one arg to rewrite
2024-12-18 09:50:50 +00:00
Nuno Lopes
2f5c0a6985
remove 2 unneeded lambda captures
2024-12-17 16:02:24 +00:00
Nuno Lopes
6f24123f0c
reduce hash table lookups in expr_abstract in half
2024-12-16 11:00:55 +00:00
Nikolaj Bjorner
a6e59ea45e
fix build flags for release.yaml
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-16 04:41:29 +01:00
Nikolaj Bjorner
a97ad76bb6
publish pypi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-15 13:00:50 -08:00
Nikolaj Bjorner
200ef236da
Update RELEASE_NOTES.md
2024-12-15 06:01:44 -08:00
Nikolaj Bjorner
e40972b7f7
Update release.yml
...
disable publish to pypi during release dry-runs
2024-12-15 05:55:48 -08:00
Nikolaj Bjorner
b529a58b91
add unit test for incremental equation edit distance with repair
2024-12-15 05:53:28 -08:00
Nikolaj Bjorner
31ee56c1ca
wip - incremental edit distance algorithm
2024-12-13 09:30:49 -08:00
Nikolaj Bjorner
538f74d64c
extract stats with finalize for parallel mode
2024-12-13 09:30:49 -08:00
Oskar Haarklou Veileborg
b4295620b3
Add __enter__ and __exit__ methods on Optimize class ( #7477 )
...
This enables the use of the with statement for the Optimize class to
concisely call push() and pop(). This works similarly to the Solver
class.
2024-12-13 09:19:04 -08:00
Nikolaj Bjorner
1e5c59a06f
add repair step for str.replace
2024-12-12 09:15:36 -08:00
Nikolaj Bjorner
e8c2360043
fix #7461
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-09 16:57:17 -08:00
Nikolaj Bjorner
8f5658b77d
add another baseline heuristic for string equalities, add cases for array axioms.
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-09 15:55:19 -08:00
Kevin Gibbons
e5f8327483
Update emscripten ( #7473 )
...
* fixes for newer emscripten thread handling behavior
* fix return type for async wrapper functions
* update prettier
* update typescript and fix errors
* update emscripten version in CI
* update js readme about tests
2024-12-06 18:11:14 -08:00
Nikolaj Bjorner
4fbf54afd0
fixes to regex membership and edit updates
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-06 09:50:30 -08:00
Nikolaj Bjorner
1ab0962d43
partial fix to make computed term integer well-formed for solve_for functionality
2024-12-05 17:10:52 -08:00
