3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-25 13:36:53 +00:00
Commit graph

20236 commits

Author SHA1 Message Date
Nikolaj Bjorner
cb5fb390bc fix #8102
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-23 09:44:22 -08:00
Ilana Shapiro
eb56ac48b0
Some changes to improve LIA performance (#8101)
* add user params

* inprocessing flag

* playing around with clause sharing with some arith constraints (complicated version commented out)

* collect shared clauses inside share units after pop to base level (might help NIA)

* dont collect clauses twice

* dont pop to base level when sharing units, manual filter

* clean up code

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
2025-12-22 17:47:36 +00:00
Nikolaj Bjorner
97acdb85a2 remove flight test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-21 14:40:43 -08:00
Nikolaj Bjorner
0c8a219fc4 next flight test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-21 13:36:57 -08:00
Nikolaj Bjorner
a0554b154a update to macos-latest
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-21 12:17:09 -08:00
Nikolaj Bjorner
880cf0129b naming convention
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-21 12:14:13 -08:00
Nikolaj Bjorner
feda43a2ac indent
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-21 12:13:02 -08:00
Nikolaj Bjorner
db46a1195b flight test copilot generated slop?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-21 11:56:19 -08:00
Nikolaj Bjorner
ed5312fbe4 fix #8097 2025-12-21 10:02:47 -08:00
Nikolaj Bjorner
5ceb312f41
Update docs.yml 2025-12-20 18:59:42 +00:00
Copilot
06658a1fd7
Fix docs.yml workflow: specify working directory for npm commands (#8098)
* Initial plan

* Fix docs.yml build by adding working-directory to npm steps

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-12-20 02:03:54 +00:00
Nikolaj Bjorner
ca62133a56 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-19 14:13:14 -08:00
Nikolaj Bjorner
6584084d6a set build directory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-19 13:49:24 -08:00
Nikolaj Bjorner
1220352767 make build directory configurable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-19 13:46:21 -08:00
Nikolaj Bjorner
baded7fa5a
Refactor documentation workflow to simplify installation
Remove redundant command for installing Python package.
2025-12-19 21:14:20 +00:00
Nikolaj Bjorner
8f73a29136
Fix Z3BUILD environment variable in docs workflow 2025-12-19 20:54:03 +00:00
Nikolaj Bjorner
38a0cc1ef9 set build be configurable by env
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-19 12:51:36 -08:00
Nikolaj Bjorner
abd8b51ece fix build dir
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-18 20:46:42 -08:00
Nikolaj Bjorner
2f6f5ff227 try adding wasm as separate step
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-18 20:10:26 -08:00
Nikolaj Bjorner
792434e45f
Update docs.yml 2025-12-19 03:52:55 +00:00
Nikolaj Bjorner
5e22b82b61
Modify docs.yml to generate JS documentation
Updated documentation generation script to include JavaScript output.
2025-12-19 03:21:47 +00:00
Nikolaj Bjorner
f901646e08 enable js
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-18 19:12:53 -08:00
Nikolaj Bjorner
909e41ce9c include paramters
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-18 17:32:57 -08:00
Nikolaj Bjorner
1cccbfdcf3 updated with env ocaml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-18 14:00:50 -08:00
Nikolaj Bjorner
89e5e294fc update doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-18 13:39:45 -08:00
Copilot
f291908e58
Fix docs.yml workflow: update actions to v4 (#8095)
* Initial plan

* Fix docs.yml workflow: update GitHub Actions to valid versions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-12-18 21:33:09 +00:00
Nikolaj Bjorner
382d184ee2 docs with ml bindings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-18 13:08:23 -08:00
Nikolaj Bjorner
897724964c fix indentation 2025-12-18 13:03:47 -08:00
Nikolaj Bjorner
3469dda936
Modify docs.yml for deployment settings
Updated the GitHub Actions workflow for documentation deployment, changing the publish directory and removing the push trigger.
2025-12-18 20:51:36 +00:00
Nikolaj Bjorner
7ec6c09a14
Update publish directory for documentation deployment 2025-12-18 20:27:29 +00:00
Nikolaj Bjorner
7e9dea9bc7
Update docs.yml 2025-12-18 20:27:01 +00:00
Copilot
2a3f874883
Deploy docs to z3prover.github.io organization pages (#8094)
* Initial plan

* Deploy docs to z3prover.github.io organization pages

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-12-18 19:39:04 +00:00
Nikolaj Bjorner
04d9504cc3
Simplify CI workflow by removing emscripten steps
Removed unnecessary steps for emscripten setup and TypeScript/WASM build in the CI workflow.
2025-12-17 20:28:16 +00:00
Nikolaj Bjorner
9ffc7e4b80
Add working directory for wasm build step 2025-12-17 19:39:30 +00:00
Nikolaj Bjorner
a912bfe05d
Update docs.yml 2025-12-17 18:12:39 +00:00
Nikolaj Bjorner
470d660cee
Update docs.yml 2025-12-17 18:09:34 +00:00
Copilot
fc72855e55
Fix docs.yml workflow: resolve WASM/native library conflict in documentation generation (#8093)
* Initial plan

* Fix docs.yml: Build native Z3 Python bindings before WASM to avoid library conflicts

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-12-17 17:18:33 +00:00
Nikolaj Bjorner
9933500365 use new arithmetic solver for AUFLIA, fixes #8090
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-16 16:09:37 -08:00
Nikolaj Bjorner
60926e0347 fix #8092
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-16 15:49:49 -08:00
Copilot
9a09b10cea
Fix docs.yml workflow: remove conflicting native build step (#8091)
* Initial plan

* Fix docs.yml workflow to properly build and deploy documentation

- Remove `no-install: true` from setup-emsdk step to properly install emscripten
- Remove `working-directory: src/api/js` from setup-emsdk step (not needed)
- Remove manual emsdk install/activate/source commands from Build wasm step
- Remove redundant native Z3 build step that conflicted with wasm build
- Simplify Generate Documentation step by removing redundant source command

The main issue was that the native Z3 build was creating a Makefile in the build/
directory before the wasm build ran. The wasm build script then saw the Makefile
existed and skipped the emconfigure step, but the native Makefile doesn't have a
libz3.a target, causing the build to fail. Removing the native build allows the
wasm build to properly configure its own build with emscripten.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-12-16 23:14:55 +00:00
Nikolaj Bjorner
8cc1d12555 merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-16 14:15:05 -08:00
h-vetinari
429771e5b7
BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088)
* Add CMake option to build only Python bindings without rebuilding libz3

Introduce Z3_BUILD_LIBZ3_CORE option (default ON) to control whether libz3 is built.
When set to OFF with Z3_BUILD_PYTHON_BINDINGS=ON, only Python bindings are built
using a pre-installed libz3 library. This is useful for package managers like
conda-forge to avoid rebuilding libz3 for each Python version.

Changes:
- Add Z3_BUILD_LIBZ3_CORE option in src/CMakeLists.txt
- When OFF, find and use pre-installed libz3 as imported target
- Update Python bindings CMakeLists.txt to handle both built and imported libz3
- Add documentation in README-CMake.md with usage examples

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix CMake export issues when building only Python bindings

Conditionally export Z3_EXPORTED_TARGETS only when Z3_BUILD_LIBZ3_CORE=ON
to avoid errors when building Python bindings without building libz3.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Disable executable and test builds when not building libz3 core

When Z3_BUILD_LIBZ3_CORE=OFF, automatically disable Z3_BUILD_EXECUTABLE
and Z3_BUILD_TEST_EXECUTABLES to avoid build/install errors.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* only build src/ folder if Z3_BUILD_LIBZ3_CORE is TRUE

* move z3 python bindings to main CMake

* move more logic to main CMakeLists.txt

* move Z3_API_HEADER_FILES_TO_SCAN to main CMakeLists.txt

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-12-16 17:50:37 +00:00
Nikolaj Bjorner
9f7e304ee8
Update docs.yml 2025-12-16 17:36:42 +00:00
Nikolaj Bjorner
818afaf4b5
Add defaults for job run working directory 2025-12-16 17:16:21 +00:00
Nikolaj Bjorner
b82287dc25
Update docs.yml 2025-12-16 16:49:05 +00:00
Nikolaj Bjorner
6b6e1e017b
Update docs.yml 2025-12-16 15:31:18 +00:00
Nikolaj Bjorner
8407bfc8a3 build the ts bindings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-15 20:02:21 -08:00
Nikolaj Bjorner
d7f6f0d2a7 build the ts bindings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-12-15 20:01:28 -08:00
dependabot[bot]
7cbd4423ee
Bump actions/upload-artifact from 5 to 6 (#8083)
Bumps [actions/upload-artifact](https://github.com/actions/upload-artifact) from 5 to 6.
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](https://github.com/actions/upload-artifact/compare/v5...v6)

---
updated-dependencies:
- dependency-name: actions/upload-artifact
  dependency-version: '6'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2025-12-16 03:42:10 +00:00
Copilot
8cda0fc69d
Build native Z3 for x64 before generating docs (#8086)
* Initial plan

* Build Z3 for ubuntu x64 and invoke JS build scripts in docs workflow

- Modified docs.yml to build Z3 natively for ubuntu-latest x64 before documentation generation
- Removed default working directory to allow explicit working-directory per step
- Added step to build Z3 using python scripts/mk_make.py
- Kept emscripten setup as required for wasm build
- Modified mk_api_doc.py to invoke npm run build:ts and npm run build:wasm as described in src/api/js/README.md
- mk_api_doc.py now runs the full build process (TypeScript + wasm) before generating documentation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Source emsdk environment before generating documentation

- Added source command to ensure emscripten tools are in PATH when mk_api_doc.py runs npm scripts
- This ensures emcc and other emscripten tools are available for npm run build:wasm

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Revert changes to mk_api_doc.py

- Removed npm run build:ts and npm run build:wasm calls from mk_api_doc.py
- Reverted to only calling npm run docs as before

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-12-16 03:41:27 +00:00