mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00
Code Activity
20265 commits 71 branches 53 tags 203 MiB
Commit graph

20265 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
0decb25420
Delete .github/workflows/codeql-analysis.yml 2026-01-08 19:59:08 -08:00
Copilot
f690afa6b1
Add AtMost, AtLeast, unsatCore, and reasonUnknown to JS/TS API (#8118) 
* Initial plan

* Add AtMost, AtLeast, checkAssumptions, and unsatCore methods to JS/TS API

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

* Format code with prettier

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

* Add comprehensive documentation for Solver.check, checkAssumptions, and unsatCore methods

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

* Remove redundant checkAssumptions method, use check() for assumptions

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

* Enable unsat_core tracking in test to fix 'unknown' result

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

* Add reasonUnknown() method and use it in test to debug unknown results

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>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-08 19:53:08 -08:00
Copilot
bc4f587acc
Add missing C# API functions for solver introspection and congruence closure (#8126) 
* Initial plan

* Add missing C# API functions for NonUnits, Trail, and Congruence methods

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

* Fix formatting: remove extra blank lines in new properties

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-01-08 18:46:47 -08:00
Copilot
7a35caa60a
Fix memory lifetime bug in async array parameter handling for JS API (#8125) 
* Initial plan

* Fix async array parameter handling in JS API wrappers

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

* Add test for solver.check() with assumptions

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

* Address code review feedback: add null checks and improve readability

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

* Add unsatCore() method to Solver class

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-01-08 18:43:58 -08:00
Copilot
dc2d2e2edf
Add missing C++ API methods for congruence closure and model sort universe (#8124) 
* Initial plan

* Add missing C++ API functions for congruence closure and model sort universe

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

* Add error checking and context validation to new API methods

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

* Add documentation for get_sort precondition

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

* Delete examples/c++/test_missing_apis.cpp

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-08 15:16:55 -08:00
Copilot
936952dd00
Enable workflow log access for build-warning-fixer agent (#8123) 
* Initial plan

* Enable agentic-workflows MCP server for workflow log access

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-01-08 15:06:57 -08:00
Copilot
8e59c4938a
Upgrade agentic workflows to gh-aw v0.36.0 (#8122) 
* Initial plan

* Upgrade agentic workflows to gh-aw v0.36.0

- Applied automatic codemods (timeout_minutes → timeout-minutes, command → slash_command)
- Fixed pr-fix.md: push-to-pr-branch → push-to-pull-request-branch
- Updated include paths from agentics/shared/ to shared/
- Migrated @include syntax to {{#import}} syntax
- Moved shared workflow files to standard .github/workflows/shared/ location
- Ran gh aw init to refresh agent files and instructions
- All 8 workflows compile successfully

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-01-08 11:50:35 -08:00
Nikolaj Bjorner
c107ba22b3 Merge branch 'master' of https://github.com/Z3Prover/z3 2026-01-08 18:46:41 +00:00
Nikolaj Bjorner
69bc608a18 Add GitHub Actions workflow for automatic build warning detection and fixing 
This workflow analyzes build warnings from CI runs of the Z3 theorem prover codebase. It extracts compiler warnings, creates fixes for straightforward issues, and generates pull requests with the changes. The process is designed to be conservative, ensuring that only safe and minimal changes are made to the codebase.
 2026-01-08 18:45:57 +00:00
Copilot
a7a18b8309
Add agentic workflow for multi-language API coherence checking (#8119) 
* Initial plan

* Add API coherence checker agentic workflow

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-01-08 10:31:23 -08:00
Nikolaj Bjorner
c7cee3227d update aw to current version 2026-01-08 18:15:03 +00:00
Nikolaj Bjorner
ccc2a34444 fix #8109 
default behavior is conservative: if the body of a recursive function contains uninterpreted variables they are not rewritten.
Model evaluation will bind values to uninterpreted variables so the filter should not apply here.
 2026-01-07 10:56:50 -08:00
Nikolaj Bjorner
fbf65c5d76 increase timeout on windows build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-05 09:09:57 -08:00
Nikolaj Bjorner
5c8886dd00
Fix link formatting for AIX build settings 2026-01-05 07:29:51 -08:00
Nikolaj Bjorner
29b616bac6
Update README.md 2026-01-05 07:29:00 -08:00
Simon Sobisch
c390afa279
AIX compat (#8113) 
* fix name conflict for struct proc

* aix compat
 2026-01-05 07:23:05 -08:00
bu99ed
ff7d0fb501
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-01-03 15:26:40 -08:00
Nikolaj Bjorner
5dc812728e refine maxresw option 2026-01-02 16:23:51 -08:00
Lev Nachmanson
623b32239c 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-01-02 11:56:35 -10:00
Lev Nachmanson
918722d2f6 add a check in entry_invariant() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-02 10:54:36 -10:00
Nikolaj Bjorner
5c4a3128c4 update wcnf front-end and add new wcnf strategy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-01 17:50:42 -08:00
Lev Nachmanson
17dffc67c9 catch a conflict with a fractional sum of fixed variables in a term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-30 16:09:35 -10:00
Lev Nachmanson
58462938fa cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-30 16:09:35 -10:00
Nikolaj Bjorner
cc94930e00 fix #8105 2025-12-30 11:30:22 -08:00
Nikolaj Bjorner
ec4246463f fix #8045 2025-12-28 10:41:27 -08:00
Nikolaj Bjorner
e4cdbe0035 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
 2025-12-26 12:04:57 -08:00
Nikolaj Bjorner
c12425c86f fix #8099 (again) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-12-25 14:16:54 -08:00
Lev Nachmanson
ce2405aab6 assert entry_invariant only when all changes are done 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-25 11:33:32 -10:00
Nikolaj Bjorner
f26facaf8f fix #8076 
remove unsound "optimization" for correction sets. It misses feasible solutions
 2025-12-25 12:44:08 -08:00
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