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

20451 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
ddb0a2f7e8 Initial plan 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
bd7caa2802 Update nightly.yml 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
021d24d0cb Update C++ compiler version in cross-build workflow 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
a0dca6b570 Change container image from ubuntu:jammy to ubuntu:noble 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
f63a4236c3 Update GCC version in cross-build workflow 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
b0c655d2cf Update nightly.yml 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
3f48780224 Update nightly.yml 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
fd1ef7f7b0 Add workflow_dispatch trigger to android-build.yml 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
2d814446a5 Update cross-build.yml 2026-02-18 20:57:31 -08:00
Copilot
de825be4c7 Replace fall-through comments with Z3_fallthrough macro (#8219) 
* Initial plan

* Fix switch fall-through warnings with Z3_fallthrough attribute

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:31 -08:00
Copilot
c8d6b3161f Update cross-build workflow to GCC 12 for C++20 support (#8220) 
* Initial plan

* Update cross-build workflow to use g++-12 for C++20 support

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:31 -08:00
Copilot
11970f9203 Fix 13 compiler warnings: sign-comparison and unused parameters (#8215) 
* Initial plan

* Fix 13 compiler warnings: sign-comparison and unused parameters

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:31 -08:00
Copilot
ac097f1d74 Fix artifact extraction patterns in nightly Python packaging job (#8217) 
* Initial plan

* Fix unzip patterns in Python packaging job

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:31 -08:00
Ilana Shapiro
6f41e9fc29 Fix UNKNOWN bug in search tree about inconsistent end state (#8214) 
* restore more aggressive pruning in search tree

* restore where we close children to be correct

* add core strengthening check

* fix recursion bug

* less strict core propagation

* old search tree version

* restore search tree patch

* remove flag

* debugging inconsistent end state with search, some changes need to be made in search tree, only backtrack should be closing nodes, I think the bug is when we do find_highest_attach for nonchronological backjumping, you might get to a point where the sibling is closed, so then we need to resolve further up the tree

* clean up code, fix deadlock

* delete test files

* clean up

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
 2026-02-18 20:57:31 -08:00
Copilot
1d304d0300 Fix nightly build failures in ARM64 and Python packaging jobs (#8213) 
* Initial plan

* Fix nightly build workflow failures for ARM64 and Python packaging

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:31 -08:00
Nuno Lopes
b1b582d3e8 bot: restore std::format 2026-02-18 20:57:31 -08:00
Copilot
2bcc366d32 [WIP] Update nightly.yml to fix build error with macOS runner (#8209) 
* Initial plan

* Fix macos-13 runner retirement: update to macos-14

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:30 -08:00
Copilot
5986ca33ef Fix checkout action GLIBC incompatibility in manylinux and macOS builds (#8207) 
* Initial plan

* Fix checkout action compatibility with manylinux containers and macOS

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:30 -08:00
Copilot
71d26fd233 Reapply PR #8190: Replace std::ostringstream with C++20 std::format (#8204) 
* Initial plan

* Reapply PR #8190: Replace std::ostringstream with C++20 std::format

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:30 -08:00
Copilot
a71cabf8c7 Migrate nightly builds from Azure DevOps to GitHub Actions (#8206) 
* Initial plan

* Add GitHub Actions workflow for nightly builds

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

* Fix Windows builds to use --zip flag instead of manual archiving

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:30 -08:00
Nikolaj Bjorner
f39497c8e7 fix #8195 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:30 -08:00
Copilot
d43b6d2684 Change code-conventions-analyzer workflow discussion category to "Agentic Workflows" (#8203) 
* Initial plan

* Update code-conventions-analyzer discussion category to "Agentic Workflows"

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:30 -08:00
Copilot
5d78c82f01 Update api-coherence-checker workflow to use "Agentic Workflows" discussion category (#8202) 
* Initial plan

* Update api-coherence-checker to use "Agentic Workflows" discussion category

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:30 -08:00
Nikolaj Bjorner
aa6fddf944 simplify contains check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:30 -08:00
Ilana Shapiro
f5fc7eb173 Add core strengthening and non-chronological backtracking to parallel search tree (#8193) 
* restore more aggressive pruning in search tree

* restore where we close children to be correct

* add core strengthening check

* fix recursion bug

* less strict core propagation

* old search tree version

* restore search tree patch

* remove flag

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
 2026-02-18 20:57:30 -08:00
Copilot
8a4f5f56fc Fix api-coherence workflow to verify and filter resolved issues (#8201) 
* Initial plan

* Update api-coherence workflow to verify and filter resolved issues

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:30 -08:00
Copilot
317dd92105 Standardize for-loop increments to prefix form (++i) (#8199) 
* Initial plan

* Convert postfix to prefix increment in for loops

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

* Fix member variable increment conversion bug

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

* Update API generator to produce prefix increments

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:29 -08:00
Copilot
851b8ea31c Replace manual pair unpacking with structured bindings (#8197) 
* Initial plan

* Apply structured bindings to enode_bool_pair usage

Replace manual unpacking of pairs with C++17 structured bindings in:
- src/ast/euf/euf_egraph.cpp
- src/smt/smt_internalizer.cpp
- src/smt/smt_context.cpp (2 locations)

This improves code readability and reduces boilerplate code.

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:27 -08:00
Copilot
a5a2a37495 Replace remaining NULL with nullptr (#8198) 
* Initial plan

* Replace NULL with nullptr in spacer_context.cpp

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:27 -08:00
Copilot
1ee3e17c31 Update ARM GCC toolchain to 13.3 for C++20 std::format support (#8196) 
* Initial plan

* Update ARM GCC toolchain from 11.2 to 13.3 for C++20 std::format support

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:23 -08:00
Nikolaj Bjorner
3dd466d4f1 remove RCF example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:14 -08:00
Nuno Lopes
3dd21d481b fix build 2026-02-18 20:57:14 -08:00
Copilot
a3c10c68a7 Remove redundant overridden default destructors (#8191) 
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:13 -08:00
Lev Nachmanson
8266de787c throw an algebraic exception on a failure of m_limit.inc() instead of returning sign_zero 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:13 -08:00
Nuno Lopes
a3440f1567 copilot: don't use std::format and try using clang-tidy 2026-02-18 20:57:13 -08:00
Lev Nachmanson
accb7393cd Revert "Merge pull request #8190 from Z3Prover/copilot/fix-std-format-usage" 
This reverts commit d9bdb6b83c, reversing
changes made to 8b188621a5.
 2026-02-18 20:57:13 -08:00
Copilot
aab029f404 Enhance Code Conventions Analyzer for empty constructors and non-virtual destructors (#8192) 
* Initial plan

* Enhance Code Conventions Analyzer for empty constructors and non-virtual destructors

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:13 -08:00
copilot-swe-agent[bot]
242ec13297 Fix spacing in error message 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-02-18 20:57:13 -08:00
copilot-swe-agent[bot]
494dc25ca5 Modernize more files to use std::format: bv_decl_plugin, dl_decl_plugin, datatype_decl_plugin, seq_decl_plugin 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-02-18 20:57:13 -08:00
copilot-swe-agent[bot]
794de8fa8b Modernize ostringstream to std::format in ast.cpp and array_decl_plugin.cpp 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-02-18 20:57:13 -08:00
copilot-swe-agent[bot]
b0d29c1e45 Initial plan 2026-02-18 20:57:13 -08:00
Nikolaj Bjorner
1a37a73172 coerce bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:13 -08:00
Nikolaj Bjorner
b3c1de6643 update iterator pattern 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:12 -08:00
Simon Jeanteur
9ca6580e38 Subterms Theory (#8115) 
* somewhaat failed attempt at declaring subterm predicate

I can't really figure out how to link the smt parser to the rest of the
machinenery, so I will stop here and try from the other side. I'll start
implmenting the logic and see if it brings me back to the parser.

* initial logic implmentation

Very primitive, but I don't like have that much work uncommitted.

* parser implementation

* more theory

* Working base

* subterm reflexivity

* a few optimization

Skip adding obvious equalities or disequality

* removed some optimisations

* better handling of backtracking

* stupid segfault

Add m_subterm to the trail

* Update src/smt/theory_datatype.h

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/ast/rewriter/datatype_rewriter.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/smt/theory_datatype.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/smt/theory_datatype.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/smt/theory_datatype.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* review

* forgot to update `iterate_subterm`'s signature

* fix iterator segfault

* Remove duplicate include statement

Removed duplicate include of 'theory_datatype.h'.

* Replace 'optional' with 'std::option' in datatype_decl_plugin.h

* Add is_subterm_predicate matcher to datatype_decl_plugin

* Change std::option to std::optional for m_subterm

* Update pdecl.h

* Change has_subterm to use has_value method

* Update pdecl.cpp

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
 2026-02-18 20:57:12 -08:00
Copilot
a6c1d32074 Replace empty destructors with = default for compiler optimization (#8189) 
* Initial plan

* Replace empty destructors with = default

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:12 -08:00
Nikolaj Bjorner
e29289ad97 Add workflow_dispatch trigger to wip.yml 2026-02-18 20:57:12 -08:00
Nikolaj Bjorner
9887f050eb Update pyodide.yml 2026-02-18 20:57:12 -08:00
Copilot
3c0c29d37a Extend code-conventions-analyzer workflow with Z3-specific C++ modernization patterns (#8187) 
* Initial plan

* Update code-conventions-analyzer workflow with modern C++ preferences

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:11 -08:00
Nikolaj Bjorner
a7c4967c97 update RCFNum 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:11 -08:00
Nikolaj Bjorner
6f0b349b46 update python example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:11 -08:00