3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-04 15:03:57 +00:00
Commit graph

20038 commits

Author SHA1 Message Date
Nikolaj Bjorner
c8bdbd2dc4 remove directory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-10-03 11:58:57 -07:00
Nikolaj Bjorner
e137aaa249 add user propagators to opt_solver 2025-10-02 19:44:22 -07:00
Nikolaj Bjorner
0e6b3a922a Add commands for forcing preferences during search
Add commands:

(prefer <formula>)
- will instruct case split queue to assign formula to true.
- prefer commands added within a scope are forgotten after leaving the scope.

(reset-preferences)
- resets asserted preferences. Has to be invoked at base level.

This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2
2025-10-02 10:47:10 -07:00
Nikolaj Bjorner
5d8fcaa3ee update clang format 2025-10-02 10:39:37 -07:00
Nikolaj Bjorner
72c89e1a4e fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-30 15:58:48 -07:00
Nikolaj Bjorner
0881a71ed2 update format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-30 15:42:01 -07:00
Nikolaj Bjorner
65c9a18c3a fix #7956
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-30 15:41:49 -07:00
Ruijie Fang
339f0cd5f9
Correctly distinguish between Lambda and Quantifier in Z3 Java API (#7955)
* Distinguish between Quantifier and Lambda in AST.java

* Distinguish betwee Lambda and Quantifier in Expr.java

* Make things compile
2025-09-30 09:55:14 -07:00
Nikolaj Bjorner
253a7245d0 add analysis
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-28 13:05:04 +03:00
Nikolaj Bjorner
b5f79da76a add analysis
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-28 13:03:31 +03:00
Nikolaj Bjorner
ae55b6fa1e add analysis
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-28 13:02:05 +03:00
Nikolaj Bjorner
bda98d8da4 fix #7948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-28 12:52:20 +03:00
Nikolaj Bjorner
b7eb21efed fix #7948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-28 12:52:19 +03:00
Wael Boutglay
391880b6fc
Add missing ::z3::sdiv to z3++.h (#7947) 2025-09-25 22:04:15 +03:00
Nikolaj Bjorner
6173a0d025 propagate value initialization to atoms 2025-09-24 11:01:24 +03:00
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
5d91294e90 update workflows 2025-09-19 03:31:56 +01:00
Nikolaj Bjorner
59bd1cf4a0 updated clang format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-18 15:13:20 -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
635d3b7017
Add .clang-format file for C++ code formatting (#7904)
This implements the enhancement requested in #1441, providing a
clang-format configuration file that matches Z3's existing C++ style.

Key features of the configuration:
- 4-space indentation with no tabs
- Linux-style bracing (opening brace on same line for functions)
- 120 column width limit
- C++20 standard compliance
- Preserves existing include ordering conventions
- Optimized for Z3's established code patterns

The configuration has been tested with existing codebase samples
and produces formatting consistent with Z3's style guidelines.

Closes #1441

🤖 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:22:27 -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
7cb491dd6a update compiled workflows 2025-09-17 23:49:55 +01:00
Don Syme
d989bcaebe update compiled workflows 2025-09-17 23:47:16 +01:00
Don Syme
f300dfc425 recompile improvers 2025-09-17 16:41:49 +01:00
Don Syme
2d0b9e6972 recompile improvers 2025-09-17 15:50:33 +01:00
Don Syme
aabdb407d1 latest improvers 2025-09-17 13:49:00 +01:00
Don Syme
2364ea42ba update improvers 2025-09-17 13:19:24 +01:00
Don Syme
7268136bb6 update workflows 2025-09-17 11:33:24 +01:00
Don Syme
db8206d265 improve improvers 2025-09-17 11:03:23 +01:00
Don Syme
5b70f75d89 allow burner to create PRs 2025-09-17 02:41:38 +01:00
Don Syme
81da4be228 backlog burner 2025-09-17 02:20:48 +01:00
Don Syme
ba4c9238c0 add daily backlog burner 2025-09-17 02:03:48 +01:00