mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 08:18:55 +00:00
Code Activity
20276 commits 70 branches 53 tags 203 MiB
Commit graph

20276 commits

This branch
This branch
All branches
Author SHA1 Message Date
Copilot
05994345cb
Add agentic workflow for C++ coding conventions and modernization analysis (#8140) 
* Initial plan

* Add code conventions analyzer 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-10 12:28:31 -08:00
Copilot
6d14d2e3b8
Add missing API methods: Java substituteFuns, TypeScript Fixedpoint and substitution APIs (#8138) 
* Initial plan

* Add substituteFuns to Java and substitute methods to TypeScript

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

* Add Fixedpoint (Datalog) API to TypeScript bindings

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

* Improve error message in Java substituteFuns method

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

* Fix TypeScript build error: use .ptr instead of .decl for FuncDecl

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

* Fix TypeScript build errors: handle optional symbols and pointer null checks

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-10 12:04:50 -08:00
Copilot
495e1f44ba
Add missing array API functions and fix BitVec method typos (#8132) 
* Initial plan

* Add missing API functions: array_default, array_ext, and fix BitVec typos

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

* Add documentation for new array API functions

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

* Fix WebAssembly build: Add default() method to LambdaImpl

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-09 11:26:27 -08:00
Nikolaj Bjorner
3881b6845b
Update high-level.test.ts 2026-01-09 09:34:10 -08:00
Copilot
02972ffab3
Add solver introspection APIs to Java bindings (getUnits, getNonUnits, getTrail) (#8130) 
* Initial plan

* Add getUnits(), getNonUnits(), and getTrail() methods to Java Solver API

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

* Add SolverIntrospectionExample and update Java examples README

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

* Revert changes in examples/java directory, keep only Solver.java API changes

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-09 09:04:56 -08:00
Copilot
c324f41eb0
Add TypeScript API parity: Solver introspection, congruence closure, and Model sort universe methods (#8129) 
* Initial plan

* Add TypeScript API parity: Solver and Model introspection methods

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

* Format code and add API parity demo example

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

* Add comprehensive API parity documentation

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

* Fix Context usage in tests and demo - use api.Context('main')

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

* Delete src/api/js/API_PARITY.md

* Delete src/api/js/examples/high-level/api-parity-demo.ts

---------

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-09 09:03:53 -08:00
Copilot
bac004047b
[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-01-08 21:10:27 -08:00
Nikolaj Bjorner
926359140b
Remove duplicate unsatCore method in types.ts 
Removed duplicate unsatCore method declaration.
 2026-01-08 20:56:12 -08:00
Copilot
22061a7452
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-01-08 20:07:16 -08:00
Nikolaj Bjorner
1d3bdd6e43 remove stale actions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-08 20:01:35 -08:00
Nikolaj Bjorner
26fd6caf27 remove stale actions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-08 20:01:00 -08:00
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