* Initial plan
* Update Z3_mk_datatype_sort API to accept array of parameters
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update language bindings for parametric datatype sort API
- Python: Updated DatatypeSort() to accept optional params list
- OCaml: Added mk_sort_ref_p/mk_sort_ref_ps for parametric datatypes
- .NET: Added MkDatatypeSortRef() methods with optional params
- Java: Added mkDatatypeSortRef() methods with optional params
- All changes maintain backward compatibility
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix .NET build error - rename params to parameters
The 'params' keyword is reserved in C#, causing compilation errors.
Renamed parameter from 'params' to 'parameters' in MkDatatypeSortRef methods.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add unit test for parametric datatypes
Added test_parametric_datatype.cpp to demonstrate polymorphic datatypes.
The test creates two concrete instantiations of a generic pair concept:
- pair_int_real with fields (first:Int, second:Real)
- pair_real_int with fields (first:Real, second:Int)
Then verifies that accessors work correctly and type checking is enforced.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Implement polymorphic type variables support for parametric datatypes
- Modified datatype_decl_plugin to allow type variables as parameters
- Updated mk_datatype_decl to extract type variables from field sorts
- Type variables are collected in order of first appearance
- Revised unit test to use Z3_mk_type_variable for polymorphic datatypes
- Test creates pair datatype with type variables alpha and beta
- Successfully instantiates with concrete types (pair Int Real) and (pair Real Int)
- Verifies accessor types match and equality terms are well-typed
- All tests pass
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add Z3_mk_polymorphic_datatype API and refactor datatype creation
- Added new API Z3_mk_polymorphic_datatype to z3_api.h
- Renamed static mk_datatype_decl to api_datatype_decl in api_datatype.cpp
- Modified api_datatype_decl to accept explicit type parameters
- Updated all callers to use renamed function
- Added test_polymorphic_datatype_api demonstrating new API usage
- Both tests pass successfully
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Remove type variable collection logic from constructors
Removed the logic for collecting type variables from field sorts based on constructors.
* Update comments on parameter handling in api_datatype.cpp
Clarify usage of parameters in API documentation.
* Fix OCaml build error - use list instead of array for mk_datatype_sort
Changed mk_sort_ref to pass empty list [] instead of empty array [||].
Changed mk_sort_ref_p to pass params list directly instead of converting to array.
Z3native.mk_datatype_sort expects a list, not an array.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add polymorphic datatype example to C++ examples
Added polymorphic_datatype_example() demonstrating:
- Creating type variables alpha and beta with Z3_mk_type_variable
- Defining parametric Pair datatype with fields of type alpha and beta
- Instantiating with concrete types (Pair Int Real) and (Pair Real Int)
- Getting constructors and accessors from instantiated datatypes
- Creating constants and expressions using the polymorphic types
- Verifying type correctness with equality (= (first p1) (second p2))
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>
* Add comprehensive API special relations tests
- Implement tests for all 5 special relations API functions:
* Z3_mk_linear_order - Linear order relation
* Z3_mk_partial_order - Partial order relation
* Z3_mk_piecewise_linear_order - Piecewise linear order relation
* Z3_mk_tree_order - Tree order relation
* Z3_mk_transitive_closure - Transitive closure of a relation
- Test coverage achieved: 100% (5/5 lines) in src/api/api_special_relations.cpp
- Added comprehensive test cases covering:
* Basic functionality with different sorts
* Different index parameters
* Expression creation and integration
* Edge cases and variations
🤖 Generated with Claude Code
* staged files
* remove files
---------
Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
* Add comprehensive API polynomial subresultants tests
- Add tests for Z3_polynomial_subresultants function in api_polynomial.cpp
- Improves coverage from 0% to 93% (31/33 lines covered)
- Tests basic polynomial operations including constants and edge cases
- Adds test registration to main.cpp and CMakeLists.txt
* staged files
* remove files
---------
Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Added comprehensive test coverage for Z3's pseudo-boolean constraint API functions, improving coverage from 0% to 100% for src/api/api_pb.cpp.
- Created comprehensive test suite in src/test/api_pb.cpp
- Added test registration in src/test/main.cpp and src/test/CMakeLists.txt
- Implemented tests for all 5 API functions:
* Z3_mk_atmost: at most k variables can be true
* Z3_mk_atleast: at least k variables can be true
* Z3_mk_pble: weighted pseudo-boolean less-than-or-equal constraint
* Z3_mk_pbge: weighted pseudo-boolean greater-than-or-equal constraint
* Z3_mk_pbeq: weighted pseudo-boolean equality constraint
- Comprehensive test cases covering edge cases, negative coefficients, zero thresholds, empty arrays, and complex scenarios
- All tests pass successfully with 100% coverage achieved
Coverage improvement: api_pb.cpp went from 0% (0/64 lines) to 100% (64/64 lines)
Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This addresses issue #1163 by removing the #ifdef _WINDOWS guard from
src/test/hashtable.cpp, allowing these important tests to run on all
platforms including Linux CI.
Key changes:
- Removed #ifdef _WINDOWS preprocessor guard
- Removed corresponding #else/#endif block
- Tests now compile and run on all platforms
This is part of the broader unit test modernization effort to ensure
comprehensive cross-platform test coverage.
Co-authored-by: Daily Backlog Burner <github-actions[bot]@users.noreply.github.com>
* Daily Test Coverage Improver: Add comprehensive API Datalog tests
This commit adds comprehensive test coverage for Z3's Datalog/fixedpoint API functions, improving coverage from 0% to 17% (84/486 lines) in src/api/api_datalog.cpp.
Key improvements:
- Tests for Z3_mk_finite_domain_sort and Z3_get_finite_domain_sort_size
- Tests for Z3_mk_fixedpoint, reference counting, and basic operations
- Coverage for string conversion, statistics, and reason unknown functions
- Comprehensive error handling and edge case testing
🤖 Generated with [Claude Code](https://claude.ai/code)
Co-Authored-By: Claude <noreply@anthropic.com>
* staged files
* remove files
---------
Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
* Initial plan
* Add comprehensive test coverage for math/lp and math/polynomial modules
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Finalize test coverage improvements with corrected implementations
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix compilation errors in test files
- Fix algebraic_numbers.cpp: Simplified tests to use basic algebraic operations without polynomial manager dependencies
- Fix polynomial_factorization.cpp: Corrected upolynomial::factors usage and API calls
- Fix nla_intervals.cpp: Changed 'solver' to 'nla::core' and fixed lar_solver constructor
- Fix monomial_bounds.cpp: Updated class names and method calls to match current NLA API
These changes address the scoped_numeral compilation errors and other API mismatches identified in the build.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix monomial bounds test assertions to use consistent values
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>
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros
* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md
* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled
* trace: improve trace tag handling system with hierarchical tagging
- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
(class names and descriptions to be refined in a future update)
* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals
* trace : add cstring header
* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py
* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.
* trace : Add TODO comment for future implementation of tag_class activation
* trace : Disable code related to tag_class until implementation is ready (#7663).
