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
Nikolaj Bjorner
bcb61ee12c
v0 of edit distance repair
2024-12-05 14:14:27 -08:00
Yuantian Ding
4be4067f75
Typescript high-level api for Sets ( #7471 )
2024-12-05 07:00:11 -08:00
Nikolaj Bjorner
a17d4e68eb
bugfix to elim_uncnstr to ensure nodes are created. Prepare smt_internalizer to replay unit literals
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-04 15:32:15 -08:00
dependabot[bot]
6ea4110b30
Bump docker/build-push-action from 6.9.0 to 6.10.0 ( #7469 )
...
Bumps [docker/build-push-action](https://github.com/docker/build-push-action ) from 6.9.0 to 6.10.0.
- [Release notes](https://github.com/docker/build-push-action/releases )
- [Commits](https://github.com/docker/build-push-action/compare/v6.9.0...v6.10.0 )
---
updated-dependencies:
- dependency-name: docker/build-push-action
dependency-type: direct:production
update-type: version-update:semver-minor
...
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2024-12-02 15:39:49 -08:00
Nikolaj Bjorner
aec867586a
updates to equality solving search
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-02 13:41:18 -08:00
Nikolaj Bjorner
e6feb8423a
sls: fix bug where unsat remains empty after a literal is flipped. The new satisfiable subset should be checked
...
refined interface between solvers to expose fixed variables for tabu objectives
2024-12-01 18:35:56 -08:00
Nikolaj Bjorner
24c3cd38d1
add v0 of equality solver
2024-11-30 17:25:49 -08:00
Nikolaj Bjorner
05e053247d
add facility to solve for a linear term over API
2024-11-30 09:34:27 -08:00
Nikolaj Bjorner
d2411567b5
add projection with witnesses
...
expose model based projection with witness creation
2024-11-27 10:26:34 -08:00
Nikolaj Bjorner
b7b611d84b
inherit from std::exception
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-27 10:26:34 -08:00
Nuno Lopes
ab1be5c06e
internalize the reduce_args_tactic to reduce the number of heap allocations
2024-11-27 12:35:40 +00:00
Nuno Lopes
1ccfba6a91
remove unreachble code
2024-11-27 12:09:16 +00:00
Nikolaj Bjorner
1e62029413
use ztring
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-25 17:36:42 -08:00
Nikolaj Bjorner
fce377e1d7
add basic regex functions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-25 17:34:49 -08:00
Nikolaj Bjorner
b143a954c5
add notes and additional functions to sls-seq
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-25 13:46:16 -08:00
Nikolaj Bjorner
aed3279d7d
add missing new_value_eh when repaired up
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-24 19:57:40 -08:00
Nikolaj Bjorner
1e839e5ac2
add missing new_value_eh when repaired up
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-24 19:42:13 -08:00
Nikolaj Bjorner
7ed185aa9e
add comments
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-24 19:09:50 -08:00
Nikolaj Bjorner
4559b23caf
add local search functionality to sls_seq_plugin
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-24 11:24:17 -08:00
Nikolaj Bjorner
b4e768cfb0
adding plugin for local search strings
2024-11-22 13:56:03 -08:00
Nikolaj Bjorner
36725758eb
fix typos POLING -> POLLING in setup.py and remove unused CFLAGS
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-21 11:32:38 -08:00
Nikolaj Bjorner
71bad7159b
#7418 - circumvent use of timer threads to make WASM integration of z3 easier
...
The scoped_timer uses a std::therad. Spawning this thread fails in cases of WASM.
Instead of adapting builds and using async features at the level of WASM and the client, we expose a specialized version of z3 that doesn't use threads at all, neither for solvers nor for timers.
The tradeoff is that the periodic poll that checks for timeout directly queries the global clock each time.
We characterize it as based on polling.
2024-11-21 11:20:05 -08:00
Nikolaj Bjorner
94f0aff47f
remove the use-pthread
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-19 19:55:03 -08:00
Nikolaj Bjorner
76795a44e4
remove -pthread from options
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-19 19:50:47 -08:00
Nikolaj Bjorner
8965123c0d
fix type in setup.py
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-19 19:08:29 -08:00
Nikolaj Bjorner
10d9c81957
adapt for pyodide built
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-19 18:51:04 -08:00
Nikolaj Bjorner
012fc1b72b
more detailed tracing of where unmaterialized exceptions happen
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-19 18:15:50 -08:00
Nikolaj Bjorner
7de0c29f12
Update pyodide.yml
...
try using flags from js/scripts/build-wasm.ts
2024-11-19 12:58:08 -08:00
Nikolaj Bjorner
e855a50d9b
add exception handling to easier diagnose #7418
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-19 11:46:54 -08:00
Nikolaj Bjorner
5168a13efa
track exceptions in reason-unknown
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-19 09:29:23 -08:00
Nikolaj Bjorner
a8a50695c9
Update README.md
2024-11-18 13:29:06 -08:00
Nikolaj Bjorner
15f954ec3b
add picture of z3guide
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-18 13:21:35 -08:00
Nikolaj Bjorner
24dfc17920
Update README.md
2024-11-18 11:54:34 -08:00
Nikolaj Bjorner
4b72e517b7
SLS: log clause , allow more frequent export of SLS state to SMT
2024-11-17 20:13:02 -08:00
Nikolaj Bjorner
84447b7031
remove incremental mode from EUF, include statistics about restart vs propagation calls to sls
2024-11-17 16:58:18 -08:00
Nikolaj Bjorner
c7ea4964f2
bug fixes to sls
2024-11-17 13:07:38 -08:00
Nikolaj Bjorner
e380903d61
Update README.md
2024-11-16 19:20:04 -08:00
Nikolaj Bjorner
2310514e02
fix #7454
2024-11-16 18:20:06 -08:00
Nikolaj Bjorner
5fd1231ec0
incorporate ls during propagation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-16 15:28:28 -08:00