mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity
19044 commits 23 branches 48 tags 157 MiB
Commit graph

16026 commits

Author SHA1 Message Date
Dmitri
1166c5b666
Support BitVectors in the TypeScript Optimize API 
This is just a change in type declarations to allow calling minimize/maximize with BitVectors.
 2024-12-17 13:37:47 +02:00
Nuno Lopes
6f24123f0c reduce hash table lookups in expr_abstract in half 2024-12-16 11:00:55 +00: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
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
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
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
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
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
Nikolaj Bjorner
750dd68a14 enable par_then and par_or even if single threaded - fall back to sequential mode 2024-11-16 12:29:22 -08:00
Nikolaj Bjorner
f64d077d2a fix re-entrancy bug during flip in arith_base 2024-11-16 12:29:03 -08:00
Nikolaj Bjorner
b929996941 update to set single threaded 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-16 09:11:44 -08:00
Nikolaj Bjorner
f39198d9a8 move build-env setting to correct place 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-16 08:32:47 -08:00
Nikolaj Bjorner
197951cad4 fixes to sls 2024-11-16 08:28:24 -08:00
Nikolaj Bjorner
7c5ff7c623 moving compile time flags to setup for pyodide 2024-11-16 08:28:24 -08:00
Nikolaj Bjorner
ccbe6c33ae fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-15 09:29:30 -08:00