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

20366 commits

This branch
This branch
All branches
Author SHA1 Message Date
Copilot
17541fc4fd [WIP] Fix build warning fixer to access daily build logs (#8133) 
* Initial plan

* Update build-warning-fixer with correct tool usage and examples

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

* Add specific workflow targets to build-warning-fixer

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:06 -08:00
Nikolaj Bjorner
8fddcd7d89 Remove duplicate unsatCore method in types.ts 
Removed duplicate unsatCore method declaration.
 2026-02-18 20:57:06 -08:00
Copilot
2e7c7f47bb Remove GITHUB_READ_ONLY flag blocking Actions log retrieval in build-warning-fixer (#8128) 
* Initial plan

* Remove GITHUB_READ_ONLY=1 flag to allow log retrieval in build-warning-fixer

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:06 -08:00
Nikolaj Bjorner
d8a6007385 remove stale actions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:06 -08:00
Nikolaj Bjorner
50365e653b remove stale actions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:06 -08:00
Nikolaj Bjorner
c76deffb9a Delete .github/workflows/codeql-analysis.yml 2026-02-18 20:57:06 -08:00
Copilot
c9528cc74e 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-02-18 20:57:06 -08:00
Copilot
b524f63957 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-02-18 20:57:06 -08:00
Copilot
3be56ff27b 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-02-18 20:57:05 -08:00
Copilot
d8fe997368 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-02-18 20:57:05 -08:00
Copilot
7fc54c86d9 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-02-18 20:57:05 -08:00
Copilot
c02a20aa5a 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-02-18 20:57:05 -08:00
Copilot
caff1debd3 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-02-18 20:57:05 -08:00
Nikolaj Bjorner
6fca8d0940 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-02-18 20:57:05 -08:00
Nikolaj Bjorner
ba3f4ef1e8 update aw to current version 2026-02-18 20:57:05 -08:00
Nikolaj Bjorner
4ef799ada4 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-02-18 20:57:05 -08:00
Nikolaj Bjorner
768755b6f5 increase timeout on windows build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:05 -08:00
Nikolaj Bjorner
d15de65851 Fix link formatting for AIX build settings 2026-02-18 20:57:05 -08:00
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