mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-21 01:24:43 +00:00
Code Activity
20341 commits 32 branches 53 tags 204 MiB
Commit graph

20341 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
ed5d9364d7 add trace tag for levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
a6a02ee0b1 pass nlsat::solver to levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ae6ae57f5f use new display functions 2026-01-14 07:45:13 -10:00
Lev Nachmanson
d8917ffe12 create free function display functions 2026-01-14 07:45:13 -10:00
Lev Nachmanson
e7193501d4 pass pmanager 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
cdc5272040 pass anum_manager to levelwise, crash on sign 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
7fca133f6f t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
23328e8226 more accurate init of the relation between polynomial properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
e5b9643b01 use std::map instead of std::unordered_map 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
8f066e1573 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
4ac0bf5007 define symbolic_interval 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
0ca9c2eb93 more scaffolding 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
3aba50f48d closer to the paper 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
bbd304e1a5 scaffolding 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
26ea9391a9 scaffoldin 2026-01-14 07:45:12 -10:00
Lev Nachmanson
2eecf2a3d4 t2 2026-01-14 07:45:12 -10:00
Lev Nachmanson
16d80a6f8d t1 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:12 -10:00
Lev Nachmanson
53c52a4f65 t0 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:12 -10:00
Lev Nachmanson
ece691285e 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-01-14 07:23:26 -10:00
Nuno Lopes
888d2fc480 copilot: don't use std::format and try using clang-tidy 2026-01-14 09:17:49 +00:00
Lev Nachmanson
d5e0216070 Revert "Merge pull request #8190 from Z3Prover/copilot/fix-std-format-usage" 
This reverts commit d9bdb6b83c, reversing
changes made to 8b188621a5.
 2026-01-13 18:18:07 -10:00
Copilot
3bf271bb42
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-01-13 18:57:10 -08:00
Lev Nachmanson
d9bdb6b83c
Merge pull request #8190 from Z3Prover/copilot/fix-std-format-usage 
Modernize string formatting from std::ostringstream to std::format
 2026-01-13 13:54:00 -10:00
copilot-swe-agent[bot]
0c2ea345fb Fix spacing in error message 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-01-13 21:36:14 +00:00
copilot-swe-agent[bot]
64957e2b0e 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-01-13 21:34:47 +00:00
copilot-swe-agent[bot]
99a40e79d4 Modernize ostringstream to std::format in ast.cpp and array_decl_plugin.cpp 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-01-13 21:29:51 +00:00
copilot-swe-agent[bot]
d274181c1f Initial plan 2026-01-13 21:07:21 +00:00
Nikolaj Bjorner
8b188621a5 coerce bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-13 11:45:57 -08:00
Nikolaj Bjorner
c78d5405d1 update iterator pattern 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-13 11:33:15 -08:00
Simon Jeanteur
deaced1711
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-01-13 10:53:17 -08:00
Copilot
7377d28c30
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-01-13 10:50:10 -08:00
Nikolaj Bjorner
a0bca2b71a
Add workflow_dispatch trigger to wip.yml 2026-01-13 10:49:33 -08:00
Nikolaj Bjorner
1806e8bb33
Update pyodide.yml 2026-01-13 10:48:34 -08:00
Copilot
635c7ea32e
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-01-13 09:35:57 -08:00
Nikolaj Bjorner
5d0be96fd1 update RCFNum 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-13 09:22:43 -08:00
Nikolaj Bjorner
c2cf11672a update python example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-13 09:17:01 -08:00
Nikolaj Bjorner
38d67b3c59 removing file to deal with build issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-13 09:15:14 -08:00
Nikolaj Bjorner
eca8e19231 remove debug output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-12 21:52:44 -08:00
Copilot
daefb4ddfd
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-01-12 21:27:33 -08:00
dependabot[bot]
bb6cd7cd0e
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-01-12 20:45:55 -08:00
dependabot[bot]
6023b4c406
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-01-12 20:45:41 -08:00
dependabot[bot]
df95e219b4
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-01-12 20:45:23 -08:00
dependabot[bot]
b9b1ae56f2
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-01-12 20:45:10 -08:00
dependabot[bot]
aeb7f7eb51
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-01-12 20:44:56 -08:00
Copilot
bd0eba812d
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-01-12 16:34:42 -08:00
Copilot
cfd40d2588
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-01-11 21:20:32 -08:00
Copilot
b5492e5cf9
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-01-11 21:20:07 -08:00
Copilot
15108bf36e
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-01-11 21:19:40 -08:00
Nikolaj Bjorner
130c210239 remove optional_benchmarks from CmakeLists 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-11 19:52:07 -08:00
Copilot
4d188f07e9
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-01-11 19:47:39 -08:00