mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity
19052 commits 23 branches 48 tags 156 MiB
Commit graph

19052 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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