mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 15:04:42 +00:00
Code Activity
20348 commits 45 branches 58 tags 178 MiB
Commit graph

20348 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
12ca9f0e5d Update README.md 2026-02-18 20:57:05 -08:00
Simon Sobisch
b2db2c8b23 AIX compat (#8113) 
* fix name conflict for struct proc

* aix compat
 2026-02-18 20:57:04 -08:00
bu99ed
cea0f7c427 set source & target version java compile flags in cmake build to match the python/make build for consistent bytecode generation (#8112) 
Co-authored-by: bu99ed <bu99ed@localhost>
 2026-02-18 20:57:04 -08:00
Nikolaj Bjorner
b5578ec74e refine maxresw option 2026-02-18 20:57:04 -08:00
Lev Nachmanson
482ece11a8 when deleting the last row from m_e_matrix go over fresh variables defined for this row and mark the rows depending on them as changed 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Lev Nachmanson
a49d2b2067 add a check in entry_invariant() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Nikolaj Bjorner
51ac976877 update wcnf front-end and add new wcnf strategy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:04 -08:00
Lev Nachmanson
0da98c1378 catch a conflict with a fractional sum of fixed variables in a term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Lev Nachmanson
cf287e6a64 cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Nikolaj Bjorner
8b683787d4 fix #8105 2026-02-18 20:57:04 -08:00
Nikolaj Bjorner
d0add7e3d8 fix #8045 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
7151c5ac6e fixes to finite domain arrays 
- relevancy could be off and array solver doesn't compensate, #7544
- enforce equalities across store for small domain axioms #8065
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
c495cf42b6 fix #8099 (again) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:03 -08:00
Lev Nachmanson
5279c7993d assert entry_invariant only when all changes are done 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
d9612d356f fix #8076 
remove unsound "optimization" for correction sets. It misses feasible solutions
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
170febe538 fix #8102 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:03 -08:00
Ilana Shapiro
6d61efa6b8 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>
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
5016eb9592 remove flight test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
5ce0d597d2 next flight test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
a6c9bf9b77 update to macos-latest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
b9f09babbe naming convention 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
84a4f0220d indent 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
c9808254dd flight test copilot generated slop? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
e2df7d3d32 fix #8097 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
76fbd62037 Update docs.yml 2026-02-18 20:57:02 -08:00
Copilot
00b3b1e698 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>
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
f8beeab517 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
3089fb0932 set build directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
a5aef2c4d0 make build directory configurable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
9c23119f43 Refactor documentation workflow to simplify installation 
Remove redundant command for installing Python package.
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
0efa27ba83 Fix Z3BUILD environment variable in docs workflow 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
7eab06be7e set build be configurable by env 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
279a379a1e fix build dir 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:02 -08:00
Nikolaj Bjorner
1b76944c7d try adding wasm as separate step 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
a01bd575c9 Update docs.yml 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
9aede918bd Modify docs.yml to generate JS documentation 
Updated documentation generation script to include JavaScript output.
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
50bca45237 enable js 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
17f8594756 include paramters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
cfdd3208c6 updated with env ocaml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
f81fe09ddb update doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:01 -08:00
Copilot
24eb0efbc0 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>
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
a2a4bb44c0 docs with ml bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
5be3c6b4e8 fix indentation 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
1f14f7542b Modify docs.yml for deployment settings 
Updated the GitHub Actions workflow for documentation deployment, changing the publish directory and removing the push trigger.
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
a60bd113dc Update publish directory for documentation deployment 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
71c20690e3 Update docs.yml 2026-02-18 20:57:01 -08:00
Copilot
604d04c8b3 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>
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
6367736a4a Simplify CI workflow by removing emscripten steps 
Removed unnecessary steps for emscripten setup and TypeScript/WASM build in the CI workflow.
 2026-02-18 20:57:01 -08:00
Nikolaj Bjorner
0f990b0c11 Add working directory for wasm build step 2026-02-18 20:57:00 -08:00
Nikolaj Bjorner
da2c4dde69 Update docs.yml 2026-02-18 20:57:00 -08:00