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

20480 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
f832d5c4d9 removing file to deal with build issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:11 -08:00
Nikolaj Bjorner
0bdf266bb4 remove debug output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:11 -08:00
Copilot
2581cd4abd Fix unused parameter warnings in empty override functions by omitting parameter names (#8174) 
* Initial plan

* Fix unused parameter warnings in empty override functions

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

* Omit parameter names in empty override functions instead of casting to void

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
dependabot[bot]
50bf3221ea Bump actions/setup-dotnet from 4.3.1 to 5.0.1 (#8175) 
Bumps [actions/setup-dotnet](https://github.com/actions/setup-dotnet) from 4.3.1 to 5.0.1.
- [Release notes](https://github.com/actions/setup-dotnet/releases)
- [Commits](67a3573c9a...2016bd2012)

---
updated-dependencies:
- dependency-name: actions/setup-dotnet
  dependency-version: 5.0.1
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:57:11 -08:00
dependabot[bot]
cc77bce3ed Bump actions/download-artifact from 6.0.0 to 7.0.0 (#8176) 
Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 6.0.0 to 7.0.0.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](https://github.com/actions/download-artifact/compare/v6...v7)

---
updated-dependencies:
- dependency-name: actions/download-artifact
  dependency-version: 7.0.0
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:57:11 -08:00
dependabot[bot]
87cc6a4490 Bump actions/setup-java from 4.8.0 to 5.1.0 (#8177) 
Bumps [actions/setup-java](https://github.com/actions/setup-java) from 4.8.0 to 5.1.0.
- [Release notes](https://github.com/actions/setup-java/releases)
- [Commits](c1e323688f...f2beeb24e1)

---
updated-dependencies:
- dependency-name: actions/setup-java
  dependency-version: 5.1.0
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:57:11 -08:00
dependabot[bot]
29228ca475 Bump actions/checkout from 4.2.2 to 6.0.1 (#8178) 
Bumps [actions/checkout](https://github.com/actions/checkout) from 4.2.2 to 6.0.1.
- [Release notes](https://github.com/actions/checkout/releases)
- [Commits](https://github.com/actions/checkout/compare/v4.2.2...v6.0.1)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: 6.0.1
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:57:11 -08:00
dependabot[bot]
e208e2f2c1 Bump astral-sh/setup-uv from 5.4.2 to 7.2.0 (#8179) 
Bumps [astral-sh/setup-uv](https://github.com/astral-sh/setup-uv) from 5.4.2 to 7.2.0.
- [Release notes](https://github.com/astral-sh/setup-uv/releases)
- [Commits](d4b2f3b6ec...61cb8a9741)

---
updated-dependencies:
- dependency-name: astral-sh/setup-uv
  dependency-version: 7.2.0
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:57:10 -08:00
Copilot
3a0e3ca24a Add RCF (Real Closed Field) bindings to C++, Java, C#, and TypeScript (#8171) 
* Initial plan

* Add RCF (Real Closed Field) bindings to C++ API

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

* Add RCF (Real Closed Field) bindings to Java API

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

* Add RCF (Real Closed Field) bindings to C# (.NET) API

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

* Add RCF (Real Closed Field) example for TypeScript/JavaScript API

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

* Add comprehensive RCF implementation summary documentation

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:10 -08:00
Copilot
7bb05374a4 Add set_ast_print_mode() to Python, C#, and TypeScript bindings (#8166) 
* Initial plan

* Add set_ast_print_mode to Python and PrintMode getter to C#

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

* Add setPrintMode to TypeScript Context API

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:10 -08:00
Copilot
aaec2e032e Modernize C++ patterns: range-based for loops and nullptr (#8167) 
* Initial plan

* Replace NULL with nullptr in test files

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

* Convert iterator loops to range-based for loops (part 1)

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

* Convert iterator loops to range-based for loops (part 2)

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

* Fix compilation errors in iterator loop conversions

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:10 -08:00
Copilot
f08f97b555 Update API coherence checker to include OCaml bindings and remove Julia (#8168) 
* Initial plan

* Update API coherence checker to include OCaml bindings and remove Julia

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:10 -08:00
Nikolaj Bjorner
2e9da416f6 remove optional_benchmarks from CmakeLists 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:09 -08:00
Copilot
0cc16b63c2 Replace custom util/optional with std::optional (#8162) 
* Initial plan

* Replace optional with std::optional in source files

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

* Fix array_map contains() and remove optional_benchmark test

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

* Address code review feedback - simplify array_map and test

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:09 -08:00
Copilot
c92fe7ced9 Change Code Conventions Analyzer to output to Discussions instead of Issues (#8163) 
* Initial plan

* Change Code Conventions Analyzer to use Discussions instead of 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:09 -08:00
Copilot
6d5f050ed1 Convert internal class enums to enum class for type safety (#8158) 
* Initial plan

* Convert plain enums to enum class in EUF module

- Convert eq_status in euf::ac_plugin to enum class
- Convert undo_kind in euf::ac_plugin to enum class
- Convert undo_t in euf::arith_plugin to enum class
- Convert to_merge_t in euf::egraph to enum class
- Update all usage sites to use scoped enum syntax

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

* Convert more plain enums to enum class

- Convert state enum in substitution class
- Convert instruction enum in generic_model_converter class
- Convert eq_type enum in bit2int class
- Update all usage sites to use scoped enum syntax

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:09 -08:00
Copilot
d68837693c Adopt C++17 structured bindings for map/pair iteration (#8159) 
* Initial plan

* Adopt structured bindings for map iteration

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

* Fix DEBUG_CODE macro issue with structured bindings

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:09 -08:00
Nikolaj Bjorner
f15b0b2a56 cross-compile do_not_optimize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:09 -08:00
Copilot
932e6c04f6 Add std::optional vs custom optional performance benchmark (#8160) 
* Initial plan

* Complete optional benchmark implementation

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

* Add comprehensive benchmark results documentation

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

* Address code review feedback - improve benchmark portability and remove redundant volatile

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

* Final refinement: fix inline assembly constraint for const reference

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

* Delete OPTIONAL_BENCHMARK_RESULTS.md

---------

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:08 -08:00
Copilot
7abdc3f0d8 Add missing API functions to C++, Java, C#, and TypeScript bindings (#8152) 
* Initial plan

* Add missing API functions to C++, Java, C#, and TypeScript bindings

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

* Fix TypeScript type errors in new API functions

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

* Address code review comments and add documentation

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

* Fix TypeScript async issue in polynomialSubresultants

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

* Delete API_COHERENCE_FIXES.md

---------

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:08 -08:00
Nikolaj Bjorner
b4dcd8b34e remove ci-doctor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:08 -08:00