3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 21:49:29 +00:00
Commit graph

16846 commits

Author SHA1 Message Date
Nikolaj Bjorner
eae4de075b fix latent bug in factorization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-23 10:47:24 +03:00
Nikolaj Bjorner
04ddade2dd remove stale comment 2025-09-22 04:43:41 +03:00
Nikolaj Bjorner
f5c28a0b76 household cleanup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-22 03:58:04 +03:00
Nikolaj Bjorner
e26f7b900c fix unsound axiom for lower-bounding 2025-09-21 19:24:13 +03:00
Nikolaj Bjorner
dcdae5a61c add smt debug output for nla_core 2025-09-21 19:24:13 +03:00
Nikolaj Bjorner
ce53e06e29
Par (#7945)
* port parallel

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* update smt-parallel

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* cleanup

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* neat

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* configuration parameter renaming

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* config parameters

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-21 10:11:04 +03:00
Nikolaj Bjorner
2b5b985492 fix divergence regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-20 02:18:44 -07:00
Nikolaj Bjorner
9876e85a45 turn on max of sums transformation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-20 00:55:37 -07:00
Nikolaj Bjorner
3256d1cc8b fix bug in unit test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-20 00:44:49 -07:00
Nikolaj Bjorner
0e8648c7d7 fix compile of lp.cpp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-20 00:33:23 -07:00
Nikolaj Bjorner
a8ae52bfbf fix missing call change to cross-nested. Prepare for lower-bound and upper-bound cardinality constraints 2025-09-19 18:57:50 -07:00
Nikolaj Bjorner
2517b5a40a port improvements from ilana branch to master regarding nla
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-19 12:28:31 -07:00
Don Syme
b17df988ed
Daily Test Coverage Improver: Add comprehensive API special relations tests (#7925)
* 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>
2025-09-18 09:20:14 -07:00
Don Syme
3fa34952f0
Daily Backlog Burner: Fix bad .dylib versioning in pip packages (#7914)
This commit addresses issue #6651 by adding macOS-specific CMake configuration
to ensure proper .dylib versioning in pip packages.

Problem:
- .dylib files distributed in pip packages showed version 0.0.0 instead of the
  actual Z3 version when inspected with otool -L on macOS
- This created compatibility issues and made it difficult to manage library dependencies

Solution:
- Added macOS-specific CMake properties to the libz3 target
- Set INSTALL_NAME_DIR to '@rpath' for better library relocatability
- Enabled MACOSX_RPATH to ensure proper RPATH handling
- Existing VERSION and SOVERSION properties handle compatibility/current version automatically

The fix ensures that macOS .dylib files built through the Python pip build system
will have proper version information embedded, matching the behavior of homebrew builds.

Closes #6651

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-authored-by: Daily Backlog Burner <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
2025-09-18 08:55:56 -07:00
Lev Nachmanson
c43cb18e63 better rewriting
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-18 08:08:32 -07:00
Lev Nachmanson
37904b9e85 fix the parameter evaluation order
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-18 07:52:13 -07:00
Don Syme
cda0a922b9
Daily Test Coverage Improver: Add comprehensive API polynomial tests (#7905)
* 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>
2025-09-17 20:47:22 -07:00
Don Syme
82ab6741a0
Daily Test Coverage Improver: Add comprehensive API pseudo-boolean constraint tests (#7898)
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>
2025-09-17 20:45:43 -07:00
Don Syme
222c64fa6f
Remove Windows-only guard from hashtable unit tests (#7901)
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>
2025-09-17 20:23:01 -07:00
Don Syme
1b058f23e9
Daily Backlog Burner: Add include directory for easier Z3 integration (#7907)
This change addresses issue #1664 by implementing an include directory that
consolidates all Z3 API headers in one convenient location for developers.

## Implementation

- Creates `build/include/` directory during CMake configuration
- Copies all Z3 API headers (z3*.h) and C++ API header (z3++.h) to include directory
- Updates libz3 target to expose the include directory via target_include_directories
- Uses CMake custom target with POST_BUILD commands for automatic header copying

## Benefits

- **Developer Experience**: Single include directory eliminates need to specify multiple paths
- **Build Integration**: Works seamlessly with existing CMake build system
- **API Completeness**: Includes both C API and C++ API headers
- **Automatic Updates**: Headers are copied automatically during build process

## Usage

Developers can now:
- Use `-I build/include` for manual compilation
- Benefit from automatic include path setup when using Z3 via CMake find_package()
- Access all Z3 API headers from a single, predictable location

This follows the standard C/C++ project convention of having a dedicated include
directory, making Z3 easier to integrate into external projects.

Closes #1664

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-authored-by: Daily Backlog Burner <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
2025-09-17 20:21:56 -07:00
Don Syme
4e1a9d1ef7
Daily Test Coverage Improver: Add comprehensive API Datalog tests (#7921)
* 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>
2025-09-17 20:07:24 -07:00
Don Syme
ee083a2e6c
Daily Test Coverage Improver: Add comprehensive API AST map tests (#7890)
* Add comprehensive tests for AST map API functions

Improved test coverage from 0% to 84% for src/api/api_ast_map.cpp by adding comprehensive tests for:
- Basic map operations (creation, insertion, lookup, size)
- Map manipulation (overwrite values, erase entries, reset)
- Reference counting (inc_ref/dec_ref)
- String representation (to_string function)

This contributes 94 newly covered lines to overall project test coverage.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

* staged files

* Delete coverage-steps.log

* Delete coverage-summary.txt

* Delete coverage.html

* Delete z3.log

---------

Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-16 17:26:07 -07:00
Lev Nachmanson
9b88aaf134 determine parameter evaluation order
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-16 16:32:46 -07:00
Don Syme
44d2bba3e5
Add comprehensive tests for API algebraic number functions (#7888)
- Created new test file api_algebraic.cpp with tests for all algebraic API functions
- Tests cover basic operations (add, sub, mul, div, power, root)
- Tests cover comparison operations (lt, le, gt, ge, eq, neq)
- Tests cover sign detection (is_zero, is_pos, is_neg, sign)
- Tests cover algebraic value detection (is_value)
- Added comprehensive test cases for rational numbers and fractions
- Updated main.cpp and CMakeLists.txt to include the new test module

Coverage improvements:
- src/api/api_algebraic.cpp: 0% -> 52% (136/258 lines covered)
- Overall project coverage: ~47% (gained 71 covered lines)

Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
2025-09-16 15:32:23 -07:00
Nikolaj Bjorner
6752be7263
Remove unused variable in polynomial.cpp
Removed unused variable 'sz2' in polynomial multiplication.
2025-09-15 10:43:09 -07:00
Nikolaj Bjorner
b0bc41457f
Update polynomial.cpp 2025-09-15 10:41:56 -07:00
Nikolaj Bjorner
7efcda2674 Update polynomial.cpp 2025-09-15 09:46:29 -07:00
Nikolaj Bjorner
f4a87d4f61 shelve experiment with a variant of geobuckets
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-15 09:46:29 -07:00
Copilot
41491d79be
Add comprehensive test coverage for math/lp and math/polynomial modules (#7877)
* 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>
2025-09-14 14:57:21 -07:00
Nikolaj Bjorner
6e767795db set status to unknown 2025-09-14 13:43:10 -07:00
Nikolaj Bjorner
928a2e7cf2 update python doc tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-14 10:56:26 -07:00
Nikolaj Bjorner
0d0dd0315a evaluate unhandled arithmetic operators based on an initialized model #7876
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-14 06:45:36 -07:00
Nikolaj Bjorner
3c897b450f add rewrite rules for update-field under accessors and recognizers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-14 06:14:42 -07:00
Nikolaj Bjorner
84bf34266b put back shortcut for square test. Remove assumption in unit test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-14 05:00:47 -07:00
Nikolaj Bjorner
8158a500d4 remove shortcut as it breaks current contract
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-14 04:49:27 -07:00
Nikolaj Bjorner
573c2cb8f7 micro tuning perfect square test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-13 20:10:43 -07:00
Nuno Lopes
c350ddf990 remove a few useless dynamic casts 2025-09-13 21:06:55 +01:00
Nikolaj Bjorner
3a409e0673 #7861
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-11 15:05:11 -07:00
Nikolaj Bjorner
8440623f6d initialize table with power of 2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-11 11:47:25 -07:00
Copilot
294f0578b0
Fix Java API mkString to properly handle Unicode surrogate pairs (#7865)
* Initial plan

* Fix Java API mkString to properly handle surrogate pairs

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>
2025-09-11 11:13:31 -07:00
Nikolaj Bjorner
9196a3c369 fix #7861
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-11 10:20:58 -07:00
Nikolaj Bjorner
7566cc744d display assumptions used 2025-09-11 10:20:55 -07:00
Copilot
b2acbaa0c9
Fix .NET performance issues by reducing multiple enumerations in constraint methods (#7854)
* Initial plan

* Fix .NET performance issues by reducing multiple enumerations in constraint methods

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

* Refactor MkApp and related methods for null checks

* Update null checks for MkApp method arguments

* Fix assertion condition for MkApp method

---------

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>
2025-09-07 16:43:13 -07:00
Nikolaj Bjorner
a7eed2a9f3 remove flush_smc after m_solver.get_model #7855
the SAT model converter is applied by m_solver.get_model()
Calling m_sat_mc->flush_smc causes the SAT model converter to be inherited within m_sat_mc and then the model converter gets applied again. This time breaking the model.
flush_smc is reserved for incremental use:
2025-09-07 16:42:21 -07:00
Nikolaj Bjorner
d701702735 remove model converter operator on expr_ref& 2025-09-07 16:42:20 -07:00
Copilot
90e610eb23
Fix performance issue in MkAnd(IEnumerable) and eliminate code duplication (#7851)
* Initial plan

* Fix performance issue in MkAnd(IEnumerable<BoolExpr>) method

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

* Refactor IEnumerable methods to call params array variants

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>
2025-09-06 19:50:38 -07:00
Nikolaj Bjorner
866393a842 update defaults for new grobner featuers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-05 14:34:03 -07:00
Nikolaj Bjorner
d7718623a4 handle case where all variables are bounded
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-04 12:58:03 -07:00
Nikolaj Bjorner
98a9a34f2b add option to reduce pseudo-linear monomials
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-04 11:04:12 -07:00
Nikolaj Bjorner
e0c315bc3e filter pseudo-linear monomials 2025-09-03 17:51:12 -07:00