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

2573 commits

Author SHA1 Message Date
Nuno Lopes
c250209a3f
Update api_ast.cpp 2024-12-16 12:12:24 +00: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
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
Yuantian Ding
4be4067f75
Typescript high-level api for Sets (#7471) 2024-12-05 07:00:11 -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
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
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
7c5ff7c623 moving compile time flags to setup for pyodide 2024-11-16 08:28:24 -08:00
Linus
d3009dabfc
Proposed fix for #7451 (#7452) 2024-11-13 09:11:40 -08:00
Nikolaj Bjorner
30ad22a4ef fix #7449 2024-11-11 15:45:18 -08:00
Audrey Dutcher
75e46778fa
Make build process work with pyodide (#7442) 2024-11-04 11:09:51 -08:00
Nikolaj Bjorner
92065462b4 use std::exception as base class to z3_exception 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-04 11:08:15 -08:00
Jonas Jongejan
604714ba40
js: Add pseudo-boolean high-level functions (#7426) 
* js: Add pseudo-boolean high-level functions

* Add check for arg length
 2024-11-02 12:34:15 -07:00
Nikolaj Bjorner
b0fef6429f
Add assert_and_track support to Optimize class in .NET binding (#7437) 
Related to #7436

#7436

---

For more details, open the [Copilot Workspace session](https://copilot-workspace.githubnext.com/Z3Prover/z3/issues/7436?shareId=XXXX-XXXX-XXXX-XXXX).
 2024-10-26 01:33:09 -07:00
Nikolaj Bjorner
8b657f27aa add shortcut to retrieve kind of application 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-22 13:05:58 -07:00
Nikolaj Bjorner
78d1139ba0 add shortcut to retrieve kind of application 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-22 13:04:41 -07:00
Nikolaj Bjorner
0ebea1c298 remove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-22 11:58:16 -07:00
Jonas Jongejan
45ef6d0109
js: Adding manual release methods (#7428) 
* js: Adding manual release methods

* Add unregister token

* Add pointer assertion

* Add missing line
 2024-10-22 09:15:49 -07:00
Nikolaj Bjorner
54d30f26f7 add _0 to platform tag for pypi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-10 15:52:10 -07:00
Nikolaj Bjorner
00f1f1b83d fix typo in setup.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-09 14:19:10 -07:00
Nikolaj Bjorner
fe71b75ffd remove : from setup.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-09 13:21:27 -07:00
Nikolaj Bjorner
48aa2f6988 setup python dist to remove internal build suffix for macos 2024-10-09 12:47:17 -07:00
Nikolaj Bjorner
8c39863019 fix typo in arch for setup.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 16:17:40 -07:00
Nikolaj Bjorner
4cefc513eb add sequoia to os versions #7407 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 16:05:53 -07:00
Nikolaj Bjorner
19f63cd6e3 add sequoia to os versions #7407 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 15:57:49 -07:00
Kevin Gibbons
77aa5280df
wasm: increase timeout in tests (#7401) 2024-09-25 18:33:14 +01:00
Kevin Gibbons
103c5ad71c
wasm: attempt to GC in tests (#7400) 2024-09-25 15:53:36 +01:00
Nikolaj Bjorner
2655301afc comment out simple proofs unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-24 23:01:12 +01:00
Páll Haraldsson
994056f347
C API now used by Julia. (#7387) 
See: https://github.com/ahumenberger/Z3.jl/releases/tag/v1.0.0
 2024-09-24 15:17:00 +01:00
Nikolaj Bjorner
716a815ce1 update lock file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-24 11:29:35 +01:00
Nikolaj Bjorner
5c583299f1 Remove unnecessary const qualifiers from comparison operator overloads in z3++.h 2024-09-23 13:38:07 +01:00
Nikolaj Bjorner
4b4a28239f Add const qualifiers to comparison operators and update iterator equality checks in various classes 2024-09-23 11:45:11 +01:00
Nikolaj Bjorner
0f896503a9 Add initial value setting API for solver and optimize contexts and update related function signatures 2024-09-18 16:18:47 +03:00
Nikolaj Bjorner
48712b4f60 Add initial value setting for variables in Z3 API, solver, and optimize modules 2024-09-18 16:13:15 +03:00
Nikolaj Bjorner
0ba306e7b3 y 2024-09-17 12:27:13 +03:00
Audrey Dutcher
0837e3b8e8
Fix nightly (#7365) 
- add some logic to setup.py to handle cross platform tagging correctly
  this adds a dependency on setuptools>=70
- rearrange the nightly CI to use these new builds correctly
 2024-09-03 16:11:42 -07:00
Nikolaj Bjorner
5360656440 fix expected 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-28 09:40:57 -07:00
Audrey Dutcher
e1f1d677ff
New python packaging and tests (#7356) 
* Simplify/modernize python packaging

* Modify azure CI to utilize new python packaging
 2024-08-27 17:12:31 -07:00
Philip Zucker
e7382d6ff9
Added "&lambda;" pretty printing to python (#7320) 2024-07-31 08:14:16 -07:00
Nikolaj Bjorner
374609bd46 kludge to address #7232, probably superseeded by planned revision to setup/pypi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-08 16:54:09 -07:00
Sergey Bronnikov
1da132005a
Fix a comment for Z3_solver_from_string (#7271) 
Z3_solver_from_string accepts a string buffer with solver
assertions, not a string buffer with filename.
 2024-07-02 07:09:33 -07:00
Nikolaj Bjorner
3bf2b3f741 fix #7260 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-19 15:37:20 -07:00
dependabot[bot]
758d886fac
Bump braces from 3.0.2 to 3.0.3 in /src/api/js (#7261) 
Bumps [braces](https://github.com/micromatch/braces) from 3.0.2 to 3.0.3.
- [Changelog](https://github.com/micromatch/braces/blob/master/CHANGELOG.md)
- [Commits](https://github.com/micromatch/braces/compare/3.0.2...3.0.3)

---
updated-dependencies:
- dependency-name: braces
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-06-19 15:29:38 -07:00