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

17153 commits

Author SHA1 Message Date
Copilot
c58ef30944 Add sequence higher-order functions to Java API (#8226) 
* Initial plan

* Add four sequence operations to Java API (SeqMap, SeqMapi, SeqFoldl, SeqFoldli)

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

* Fix checkContextMatch call and add test for sequence operations

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

* Add 4-parameter checkContextMatch overload for consistency

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:33 -08:00
Copilot
509cd8d36e Add benchmark export to C# and TypeScript APIs (#8228) 
* Initial plan

* Add benchmark export functionality to C# and TypeScript APIs

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

* Fix TypeScript build error: remove redundant array length parameter

The Z3 TypeScript wrapper auto-generates array length parameters from the array itself, so passing assumptions.length explicitly causes a parameter count mismatch. Removed the redundant parameter.

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:33 -08:00
Copilot
2304da0fa2 Add advanced sequence operations to C# API (#8227) 
* Initial plan

* Add advanced sequence operations to C# API

- Add MkSeqMap: Map function over sequence
- Add MkSeqMapi: Map function over sequence with index
- Add MkSeqFoldLeft: Fold left operation on sequence
- Add MkSeqFoldLeftI: Fold left with index on sequence

These functions match Python's SeqMap, SeqMapI, SeqFoldLeft, and SeqFoldLeftI and provide feature parity with other language 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:33 -08:00
copilot-swe-agent[bot]
0115b7cadc Fix segfault in dioph_eq.cpp by adding bounds check 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:32 -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
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
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
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
Nikolaj Bjorner
f39497c8e7 fix #8195 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.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
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
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
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-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
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
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
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
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
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
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
Copilot
4f4fbe7f14 Add missing API methods across language bindings (#8150) 
* Initial plan

* Add API coherence improvements for C#, Python, C++, and TypeScript

- C#: Add SubstituteFuns method to Expr class
- Python: Add update method to ExprRef class
- C++: Add update method to expr class
- TypeScript: Add complete Statistics API with Statistics interface, StatisticsEntry interface, StatisticsImpl class, and statistics() methods for Solver, Optimize, and Fixedpoint

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

* Add Z3_stats import and Statistics types to TypeScript bindings

- Add Z3_stats to imports in types.ts and high-level.ts
- Add Statistics and StatisticsEntry to type imports in high-level.ts
- Fixes missing type references identified in code review

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:08 -08:00
Copilot
f7b196e8f0 Add [[nodiscard]] to AST factory functions and modernize iterator loops (#8143) 
* Initial plan

* Add [[nodiscard]] to AST factory functions and modernize iterator loops

- Added [[nodiscard]] attribute to key factory functions in ast.h:
  - All mk_app() variants for creating application nodes
  - All mk_func_decl() variants for creating function declarations
  - All mk_const() variants for creating constants
  - All mk_sort() variants for creating sorts
  - mk_var() for creating variables
  - mk_quantifier(), mk_forall(), mk_exists(), mk_lambda() for quantifiers
  - mk_label(), mk_pattern() and related functions

- Converted iterator loops to range-based for loops in:
  - src/util/region.cpp: pop_scope()
  - src/util/dec_ref_util.h: dec_ref_key_values(), dec_ref_keys(), dec_ref_values()
  - src/util/mpf.h: dispose()
  - src/util/numeral_buffer.h: reset()

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

* Modernize additional iterator loops to range-based for loops

- Converted iterator loops to range-based for loops in:
  - src/api/api_ast_map.cpp: Z3_ast_map_keys() and Z3_ast_map_to_string()
  - src/api/c++/z3++.h: optimize copy constructor and add() method
  - src/opt/wmax.cpp: mk_assumptions()

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

* Revert changes to z3++.h for C++ version compatibility

Revert the range-based for loop changes in src/api/c++/z3++.h to maintain
compatibility with older C++ versions that users may rely on. The C++ API
wrapper must support down-level C++ standards for backward compatibility.

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

* Trigger CI build

[skip ci] is not used to ensure CI runs

---------

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:08 -08:00
Copilot
ce62db18a4 Add Simplifier, Params, and ParamDescrs APIs to TypeScript bindings (#8146) 
* Initial plan

* Add Simplifier, Params, and ParamDescrs APIs to TypeScript bindings

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

* Add Tactic.usingParams and comprehensive documentation for new APIs

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 implementation summary documentation

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

* Fix test by using valid parameter for solve-eqs simplifier

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

* Delete IMPLEMENTATION_SUMMARY.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
d867eb3cd8 Add Goal, ApplyResult, and Tactic APIs to TypeScript bindings (#8141) 
* Initial plan

* Add Goal, ApplyResult, and enhanced Tactic/Probe APIs to TypeScript bindings

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

* Fix async tactic.apply and add comprehensive tests for new APIs

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

* Address code review feedback: fix proxy handler, factory method, and type improvements

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

* Add API examples documentation and format code with Prettier

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

* Fix merge conflict in test file - complete truncated tactic test

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

* Add test case for tactic.apply method

missing bracket,

* Change tactic from 'simplify' to 'smt'

* Delete src/api/js/TACTICS_API_EXAMPLES.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:07 -08:00
Nikolaj Bjorner
767f7eeace fix #8116 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:07 -08:00
Copilot
3a5cf48289 Add Floating-Point and String/Sequence APIs to TypeScript bindings (#8135) 
* Initial plan

* Add FP and String/Seq type definitions to TypeScript bindings

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

* Implement FP and String/Seq in TypeScript high-level bindings

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

* Add comprehensive tests for FP and String/Seq APIs

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

* Fix build errors: Add isFP to test scope and use eqIdentity for Sort comparison

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

* Fix code formatting with Prettier for WASM build

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

* Fix FPNum.value() to use Z3_get_numeral_double instead of parsing string

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

* Simplify length check for empty sequence

Refactor length check for empty sequence in tests.

---------

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:07 -08:00
Copilot
1dc59727c2 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-02-18 20:57:07 -08:00
Copilot
aff4a61eb3 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-02-18 20:57:07 -08:00
Nikolaj Bjorner
617fb60176 Update high-level.test.ts 2026-02-18 20:57:07 -08:00
Copilot
6b3adcf259 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-02-18 20:57:07 -08:00
Copilot
5bf49cbd5a 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-02-18 20:57:07 -08:00