From cf8a17a6aeb3fc0ec722c1ecee552408d8e024bd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 11 Aug 2025 13:16:37 -0700 Subject: [PATCH 01/28] restore the square-free check Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 51 ++++++++++++++++++++++++++++++------- 1 file changed, 42 insertions(+), 9 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index eaa087999..83c5f31b6 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -618,22 +618,55 @@ namespace nlsat { } } - // For each p in ps add the leading coefficent to the projection, - void add_lc(polynomial_ref_vector &ps, var x) { +// The monomials have to be square free according to +//"An improved projection operation for cylindrical algebraic decomposition of three-dimensional space", by McCallum, Scott + + bool is_square_free(polynomial_ref_vector &ps, var x) { + polynomial_ref p(m_pm); + polynomial_ref lc_poly(m_pm); + polynomial_ref disc_poly(m_pm); + + for (unsigned i = 0; i < ps.size(); i++) { + p = ps.get(i); + unsigned k_deg = m_pm.degree(p, x); + if (k_deg == 0) + continue; + // p depends on x + disc_poly = discriminant(p, x); // Use global helper + if (sign(disc_poly) == 0) { // Discriminant is zero + TRACE(nlsat_explain, tout << "p is not square free:\n "; + display(tout, p); tout << "\ndiscriminant: "; display(tout, disc_poly) << "\n"; + m_solver.display_assignment(tout) << '\n'; + m_solver.display_var(tout << "x:", x) << '\n'; + ); + + return false; + } + } + return true; + } + + // If each p from ps is square-free then add the leading coefficents to the projection. + // Otherwise, add each coefficient of each p to the projection. + void add_lcs(polynomial_ref_vector &ps, var x) { polynomial_ref p(m_pm); polynomial_ref coeff(m_pm); - // Add coefficients based on well-orientedness + bool sqf = is_square_free(ps, x); + // Add the leading or all coeffs, depening on being square-free for (unsigned i = 0; i < ps.size(); i++) { p = ps.get(i); unsigned k_deg = m_pm.degree(p, x); if (k_deg == 0) continue; // p depends on x TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p) << "\n";); - coeff = m_pm.coeff(p, x, k_deg); - TRACE(nlsat_explain, tout << " coeff deg " << k_deg << ": "; display(tout, coeff) << "\n";); - insert_fresh_factors_in_todo(coeff); - + for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) { + coeff = m_pm.coeff(p, x, j_coeff_deg); + TRACE(nlsat_explain, tout << " coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";); + insert_fresh_factors_in_todo(coeff); + if (sqf) + break; + } } } @@ -1175,7 +1208,7 @@ namespace nlsat { TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; display(tout, ps); tout << "\n";); - add_lc(ps, x); + add_lcs(ps, x); psc_discriminant(ps, x); psc_resultant(ps, x); if (m_todo.empty()) @@ -1223,7 +1256,7 @@ namespace nlsat { } TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; display(tout, ps); tout << "\n";); - add_lc(ps, x); + add_lcs(ps, x); psc_discriminant(ps, x); psc_resultant(ps, x); From 6486d9290aaa608c1fc0065329f875f17bf9bdf5 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 12 Aug 2025 15:18:52 -0700 Subject: [PATCH 02/28] Add .github/copilot-instructions.md with comprehensive Z3 development guide (#7766) * Initial plan * Add comprehensive .github/copilot-instructions.md with validated build commands and timing Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Remove test_example binary file from repository 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> --- .github/copilot-instructions.md | 167 ++++++++++++++++++++++++++++++++ 1 file changed, 167 insertions(+) create mode 100644 .github/copilot-instructions.md diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md new file mode 100644 index 000000000..5420b2ad1 --- /dev/null +++ b/.github/copilot-instructions.md @@ -0,0 +1,167 @@ +# Z3 Theorem Prover Development Guide + +Always reference these instructions first and fallback to search or bash commands only when you encounter unexpected information that does not match the info here. + +## Working Effectively + +### Bootstrap and Build the Repository + +Z3 supports multiple build systems. **ALWAYS** use one of these validated approaches: + +#### Option 1: Python Build System (Recommended for most use cases) +- `python scripts/mk_make.py` -- takes 7 seconds to configure +- `cd build && make -j$(nproc)` -- takes 15 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes. + +#### Option 2: CMake Build System (Recommended for integration) +- Clean source tree first if you previously used Python build: `git clean -fx src/` +- `mkdir build && cd build` +- `cmake ..` -- takes 1 second to configure +- `make -j$(nproc)` -- takes 17 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes. + +#### Dependencies and Requirements +- Python 3.x (required for both build systems) +- C++20 capable compiler (g++ or clang++) +- GNU Make +- Git (for version information) + +### Test the Repository + +**Python Build System:** +- Build unit tests: `make test` -- takes 3.5 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes. +- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes. + +**CMake Build System:** +- Build unit tests: `make test-z3` -- takes 4 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes. +- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes. + +**Test basic Z3 functionality:** +```bash +./z3 --version +echo "(declare-const x Int)(assert (> x 0))(check-sat)(get-model)" | ./z3 -in +``` + +### Validation Scenarios + +**ALWAYS** test these scenarios after making changes: + +#### Basic SMT Solving +```bash +cd build +echo "(declare-const x Int) +(assert (> x 0)) +(check-sat) +(get-model)" | ./z3 -in +``` +Expected output: `sat` followed by a model showing `x = 1` or similar. + +#### Python Bindings +```bash +cd build/python +python3 -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())" +``` +Expected output: `Result: sat` and `Model: [x = 1]` or similar. + +#### Command Line Help +```bash +./z3 --help | head -10 +``` +Should display version and usage information. + +## Build System Details + +### Python Build System +- Configuration: `python scripts/mk_make.py` (7 seconds) +- Main build: `cd build && make -j$(nproc)` (15 minutes) +- Test build: `make test` (3.5 minutes) +- Generates build files in `build/` directory +- Creates Python bindings in `build/python/` +- **Warning**: Generates files in source tree that must be cleaned before using CMake + +### CMake Build System +- Clean first: `git clean -fx src/` (if switching from Python build) +- Configuration: `cmake ..` (1 second) +- Main build: `make -j$(nproc)` (17 minutes) +- **Advantages**: Clean build tree, no source pollution, better for integration +- **Recommended for**: IDE integration, package management, deployment + +### Critical Timing and Timeout Requirements + +**NEVER CANCEL these operations**: +- `make -j$(nproc)` builds: 15-17 minutes. **Set timeout to 30+ minutes minimum**. +- `make test` or `make test-z3` compilation: 3.5-4 minutes. **Set timeout to 10+ minutes**. +- Unit test execution: 16 seconds. **Set timeout to 5+ minutes**. + +**Always wait for completion**. Z3 is a complex theorem prover with extensive code generation and builds may appear to hang but are actually progressing. + +## Repository Structure + +### Key Directories +- `src/` - Main source code organized by components (ast, smt, sat, etc.) +- `examples/` - Language binding examples (C, C++, Python, Java, .NET, etc.) +- `scripts/` - Build scripts and utilities +- `.github/workflows/` - CI/CD pipeline definitions +- `cmake/` - CMake configuration files + +### Important Files +- `README.md` - Main documentation and build instructions +- `README-CMake.md` - Detailed CMake build documentation +- `configure` - Wrapper script around `scripts/mk_make.py` +- `CMakeLists.txt` - Main CMake configuration +- `scripts/mk_make.py` - Python build system entry point + +## Common Tasks and Validation + +### Pre-commit Validation +Before committing changes: +1. **Build successfully**: Use one of the validated build commands above +2. **Run unit tests**: `./test-z3 /a` must pass +3. **Test basic functionality**: Run validation scenarios above +4. **Test affected language bindings**: If modifying API, test relevant examples + +### Working with Language Bindings +- **Python**: Located in `build/python/`, test with validation scenario above +- **C/C++**: Examples in `examples/c/` and `examples/c++/` + - Compile C++ example: `g++ -I src/api -I src/api/c++ examples/c++/example.cpp -L build -lz3 -o test_example` + - Run with: `LD_LIBRARY_PATH=build ./test_example` +- **Java**: Build with `python scripts/mk_make.py --java`, examples in `examples/java/` +- **C#/.NET**: Build with `python scripts/mk_make.py --dotnet`, examples in `examples/dotnet/` + +### Performance Testing +For performance-sensitive changes: +- Build optimized: `python scripts/mk_make.py` (Release mode by default) +- Test with realistic SMT problems from `examples/SMT-LIB2/` +- Use Z3's built-in statistics: `z3 -st problem.smt2` + +## Common Issues and Solutions + +### Build System Conflicts +- **Error**: CMake complains about polluted source tree +- **Solution**: Run `git clean -fx src/` to remove Python build artifacts + +### Python Import Errors +- **Error**: `import z3` fails +- **Solution**: Ensure you're in `build/python/` directory or add it to `PYTHONPATH` + +### Missing Dependencies +- **Error**: Compiler not found or version too old +- **Solution**: Z3 requires C++20. Install g++ 10+ or clang++ 10+ + +### Long Build Times +- **Normal**: 15-17 minute builds are expected for Z3 +- **Never cancel**: Set timeouts appropriately and wait for completion +- **Optimization**: Use `make -j$(nproc)` for parallel compilation + +## Key Projects in Codebase + +Z3 is organized into several key components: + +- **Core SMT**: `src/smt/` - Main SMT solver engine +- **SAT Solver**: `src/sat/` - Underlying boolean satisfiability solver +- **Theories**: Various theory solvers (arithmetic, arrays, bit-vectors, etc.) +- **Abstract Syntax Trees**: `src/ast/` - Expression representation and manipulation +- **Tactics**: `src/tactic/` - Configurable solving strategies +- **API**: `src/api/` - Public C API and language bindings +- **Parsers**: SMT-LIB2, Dimacs, and other input format parsers +- **Model Generation**: Creating and manipulating satisfying assignments + +The architecture is modular with clean separation between the core solver, theory plugins, and user interfaces. \ No newline at end of file From d375d97576d45d2d51090ab06ce061713fde17be Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 12 Aug 2025 15:19:32 -0700 Subject: [PATCH 03/28] Bump actions/checkout from 4 to 5 (#7773) Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to 5. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](https://github.com/actions/checkout/compare/v4...v5) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: '5' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/Windows.yml | 2 +- .github/workflows/android-build.yml | 2 +- .github/workflows/cross-build.yml | 2 +- .github/workflows/labeller.yml | 2 +- .github/workflows/msvc-static-build-clang-cl.yml | 2 +- .github/workflows/msvc-static-build.yml | 2 +- .github/workflows/ocaml.yaml | 2 +- .github/workflows/prd.yml | 2 +- .github/workflows/pyodide.yml | 2 +- .github/workflows/wasm-release.yml | 2 +- .github/workflows/wasm.yml | 2 +- .github/workflows/wip.yml | 2 +- 12 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/Windows.yml b/.github/workflows/Windows.yml index 74eb04d15..5cdaeb67e 100644 --- a/.github/workflows/Windows.yml +++ b/.github/workflows/Windows.yml @@ -22,7 +22,7 @@ jobs: runs-on: windows-latest steps: - name: Checkout code - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Add msbuild to PATH uses: microsoft/setup-msbuild@v2 - run: | diff --git a/.github/workflows/android-build.yml b/.github/workflows/android-build.yml index 5419720ef..74948ece8 100644 --- a/.github/workflows/android-build.yml +++ b/.github/workflows/android-build.yml @@ -21,7 +21,7 @@ jobs: steps: - name: Checkout code - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Configure CMake and build run: | diff --git a/.github/workflows/cross-build.yml b/.github/workflows/cross-build.yml index 8745215d2..0bda0a980 100644 --- a/.github/workflows/cross-build.yml +++ b/.github/workflows/cross-build.yml @@ -19,7 +19,7 @@ jobs: steps: - name: Checkout code - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Install cross build tools run: apt update && apt install -y ninja-build cmake python3 g++-11-${{ matrix.arch }}-linux-gnu diff --git a/.github/workflows/labeller.yml b/.github/workflows/labeller.yml index c31c0223e..ebe7126cd 100644 --- a/.github/workflows/labeller.yml +++ b/.github/workflows/labeller.yml @@ -13,7 +13,7 @@ jobs: genai-issue-labeller: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v5 - uses: pelikhan/action-genai-issue-labeller@v0 with: github_token: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/msvc-static-build-clang-cl.yml b/.github/workflows/msvc-static-build-clang-cl.yml index 3ec266ee7..3b5caf465 100644 --- a/.github/workflows/msvc-static-build-clang-cl.yml +++ b/.github/workflows/msvc-static-build-clang-cl.yml @@ -14,7 +14,7 @@ jobs: BUILD_TYPE: Release steps: - name: Checkout Repo - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Build run: | diff --git a/.github/workflows/msvc-static-build.yml b/.github/workflows/msvc-static-build.yml index 50a45b634..e197b1b64 100644 --- a/.github/workflows/msvc-static-build.yml +++ b/.github/workflows/msvc-static-build.yml @@ -14,7 +14,7 @@ jobs: BUILD_TYPE: Release steps: - name: Checkout Repo - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Build run: | diff --git a/.github/workflows/ocaml.yaml b/.github/workflows/ocaml.yaml index 5adc75a82..9d0917fd4 100644 --- a/.github/workflows/ocaml.yaml +++ b/.github/workflows/ocaml.yaml @@ -17,7 +17,7 @@ jobs: steps: - name: Checkout code - uses: actions/checkout@v4 + uses: actions/checkout@v5 # Cache ccache (shared across runs) - name: Cache ccache diff --git a/.github/workflows/prd.yml b/.github/workflows/prd.yml index afee5a7f1..6a53af4f8 100644 --- a/.github/workflows/prd.yml +++ b/.github/workflows/prd.yml @@ -13,7 +13,7 @@ jobs: generate-pull-request-description: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v5 - uses: pelikhan/action-genai-pull-request-descriptor@v0 with: github_token: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/pyodide.yml b/.github/workflows/pyodide.yml index b5e1d6868..8ba9d2401 100644 --- a/.github/workflows/pyodide.yml +++ b/.github/workflows/pyodide.yml @@ -19,7 +19,7 @@ jobs: steps: - name: Checkout code - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Setup packages run: sudo apt-get update && sudo apt-get install -y python3-dev python3-pip python3-venv diff --git a/.github/workflows/wasm-release.yml b/.github/workflows/wasm-release.yml index ce7145703..55599c946 100644 --- a/.github/workflows/wasm-release.yml +++ b/.github/workflows/wasm-release.yml @@ -21,7 +21,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Setup node uses: actions/setup-node@v4 diff --git a/.github/workflows/wasm.yml b/.github/workflows/wasm.yml index 0ea9688f1..319b53fb6 100644 --- a/.github/workflows/wasm.yml +++ b/.github/workflows/wasm.yml @@ -21,7 +21,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout - uses: actions/checkout@v4 + uses: actions/checkout@v5 - name: Setup node uses: actions/setup-node@v4 diff --git a/.github/workflows/wip.yml b/.github/workflows/wip.yml index 5ed29a457..bbd90d185 100644 --- a/.github/workflows/wip.yml +++ b/.github/workflows/wip.yml @@ -15,7 +15,7 @@ jobs: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v5 - name: Configure CMake run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} From c8e866f5682ed4d01a54ae714ceedf50670f09ca Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Tue, 12 Aug 2025 22:37:30 -0700 Subject: [PATCH 04/28] Parallel solving (#7775) * very basic setup * very basic setup (#7741) * add score access and reset Signed-off-by: Nikolaj Bjorner * added notes Signed-off-by: Nikolaj Bjorner * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * add bash files for test runs * fix compilation Signed-off-by: Nikolaj Bjorner * more notes Signed-off-by: Nikolaj Bjorner * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * add top-k fixed-sized min-heap priority queue for top scoring literals * fixed-size min-heap for tracking top-k literals (#7752) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner * remove verbose output Signed-off-by: Nikolaj Bjorner * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: Nikolaj Bjorner Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * debugging * process cubes as lists of individual lits * Parallel solving (#7756) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner * remove verbose output Signed-off-by: Nikolaj Bjorner * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * process cubes as lists of individual lits --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: Nikolaj Bjorner Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> * snapshot Signed-off-by: Nikolaj Bjorner * pair programming Signed-off-by: Nikolaj Bjorner * pair programming Signed-off-by: Nikolaj Bjorner * merge * chipping away at the new code structure * Parallel solving (#7758) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner * remove verbose output Signed-off-by: Nikolaj Bjorner * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests 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> * chipping away at the new code structure --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: Nikolaj Bjorner Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * updates Signed-off-by: Nikolaj Bjorner * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * Parallel solving (#7759) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner * remove verbose output Signed-off-by: Nikolaj Bjorner * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests 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> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: Nikolaj Bjorner Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * updates Signed-off-by: Nikolaj Bjorner * simplify output Signed-off-by: Nikolaj Bjorner * merge * resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints * initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel? * Parallel solving (#7769) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner * remove verbose output Signed-off-by: Nikolaj Bjorner * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests 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> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * merge * resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints * initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel? --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: Nikolaj Bjorner Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback * Parallel solving (#7771) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner * remove verbose output Signed-off-by: Nikolaj Bjorner * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests 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> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * merge * fix #7603: race condition in Ctrl-C handling (#7755) * fix #7603: race condition in Ctrl-C handling * fix race in cancel_eh * fix build * add arithemtic saturation * add an option to register callback on quantifier instantiation Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation * missing new closure Signed-off-by: Nikolaj Bjorner * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner * add python file Signed-off-by: Lev Nachmanson * debug under defined calls Signed-off-by: Lev Nachmanson * more untangle params Signed-off-by: Lev Nachmanson * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson * remove a printout Signed-off-by: Lev Nachmanson * rename a Python file Signed-off-by: Lev Nachmanson * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner * register on_binding attribute Signed-off-by: Nikolaj Bjorner * fix java build for java bindings Signed-off-by: Nikolaj Bjorner * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner * remove ref to theory_str Signed-off-by: Nikolaj Bjorner * get the finest factorizations before project Signed-off-by: Lev Nachmanson * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson * resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints * initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel? * Update RELEASE_NOTES.md * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback --------- Signed-off-by: Nikolaj Bjorner Signed-off-by: Lev Nachmanson Signed-off-by: Lev Nachmanson Co-authored-by: Nikolaj Bjorner Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Lev Nachmanson * code and notes * add some debug prints and impelement internal polynomial fix * add some comments and debug m_assumptions_used * redo greedy->frugal strategy so we don't split on existing cubes in frugal at all (eliminate the incorrect/wasteful step by processing current batch first) * set up initial scaffolding for sharing clauses between threads and batch manager. needs some reworking/debug still * Parallel solving (#7774) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner * remove verbose output Signed-off-by: Nikolaj Bjorner * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests 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> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * merge * fix #7603: race condition in Ctrl-C handling (#7755) * fix #7603: race condition in Ctrl-C handling * fix race in cancel_eh * fix build * add arithemtic saturation * add an option to register callback on quantifier instantiation Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation * missing new closure Signed-off-by: Nikolaj Bjorner * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner * add python file Signed-off-by: Lev Nachmanson * debug under defined calls Signed-off-by: Lev Nachmanson * more untangle params Signed-off-by: Lev Nachmanson * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson * remove a printout Signed-off-by: Lev Nachmanson * rename a Python file Signed-off-by: Lev Nachmanson * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner * register on_binding attribute Signed-off-by: Nikolaj Bjorner * fix java build for java bindings Signed-off-by: Nikolaj Bjorner * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner * remove ref to theory_str Signed-off-by: Nikolaj Bjorner * get the finest factorizations before project Signed-off-by: Lev Nachmanson * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson * resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints * initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel? * Update RELEASE_NOTES.md * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback * remove unused square-free check Signed-off-by: Lev Nachmanson * add some debug prints and impelement internal polynomial fix * add some comments and debug m_assumptions_used * redo greedy->frugal strategy so we don't split on existing cubes in frugal at all (eliminate the incorrect/wasteful step by processing current batch first) * set up initial scaffolding for sharing clauses between threads and batch manager. needs some reworking/debug still --------- Signed-off-by: Nikolaj Bjorner Signed-off-by: Lev Nachmanson Signed-off-by: Lev Nachmanson Co-authored-by: Nikolaj Bjorner Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Lev Nachmanson * sign of life Signed-off-by: Nikolaj Bjorner * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner * turn off logging at level 0 for testing * add max thread conflicts backoff --------- Signed-off-by: Nikolaj Bjorner Signed-off-by: Lev Nachmanson Signed-off-by: Lev Nachmanson Co-authored-by: Nikolaj Bjorner Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Lev Nachmanson --- PARALLEL_PROJECT_NOTES.md | 218 ++++++++++ run_local_tests.sh | 32 ++ src/math/polynomial/polynomial.cpp | 3 + src/smt/priority_queue.h | 191 +++++++++ src/smt/smt_context.h | 24 ++ src/smt/smt_internalizer.cpp | 26 ++ src/smt/smt_lookahead.h | 4 +- src/smt/smt_parallel.cpp | 644 +++++++++++++++++++---------- src/smt/smt_parallel.h | 112 ++++- 9 files changed, 1042 insertions(+), 212 deletions(-) create mode 100644 PARALLEL_PROJECT_NOTES.md create mode 100755 run_local_tests.sh create mode 100644 src/smt/priority_queue.h diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md new file mode 100644 index 000000000..b60263e4e --- /dev/null +++ b/PARALLEL_PROJECT_NOTES.md @@ -0,0 +1,218 @@ +# Parallel project notes + + + +We track notes for updates to +[smt/parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/smt/smt_parallel.cpp) +and possibly +[solver/parallel_tactic.cpp](https://github.com/Z3Prover/z3/blob/master/src/solver/parallel_tactical.cpp). + + + + + +## Variable selection heuristics + + + +* Lookahead solvers: + * lookahead in the smt directory performs a simplistic lookahead search using unit propagation. + * lookahead in the sat directory uses custom lookahead solver based on MARCH. March is described in Handbook of SAT and Knuth volumne 4. + * They both proxy on a cost model where the most useful variable to branch on is the one that _minimizes_ the set of new clauses maximally + through unit propagation. In other words, if a literal _p_ is set to true, and _p_ occurs in clause $\neg p \vee q \vee r$, then it results in + reducing the clause from size 3 to 2 (because $\neg p$ will be false after propagating _p_). + * Selected references: SAT handbook, Knuth Volumne 4, Marijn's March solver on github, [implementation of march in z3](https://github.com/Z3Prover/z3/blob/master/src/sat/sat_lookahead.cpp) +* VSIDS: + * As referenced in Matteo and Antti's solvers. + * Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. + * VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT). + * VSIDS does not keep track of variable phases (if the variable was set to true or false). + * Selected refernces [DAC 2001](https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf) and [Biere Tutorial, slide 64 on Variable Scoring Schemes](https://alexeyignatiev.github.io/ssa-school-2019/slides/ab-satsmtar19-slides.pdf) +* Proof prefix: + * Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score. + * The weight function can be formulated to take into account clause sizes. + * The score assignment may also decay similar to VSIDS. + * We could also use a doubly linked list for literals used in conflicts and keep reinsert literals into the list when they are used. This would be a "Variable move to front" (VMTF) variant. + * Selected references: [Battleman et al](https://www.cs.cmu.edu/~mheule/publications/proofix-SAT25.pdf) +* From local search: + * Note also that local search solvers can be used to assign variable branch priorities. + * We are not going to directly run a local search solver in the mix up front, but let us consider this heuristic for completeness. + * The heuristic is documented in Biere and Cai's journal paper on integrating local search for CDCL. + * Roughly, it considers clauses that move from the UNSAT set to the SAT set of clauses. It then keeps track of the literals involved. + * Selected references: [Cai et al](https://www.jair.org/index.php/jair/article/download/13666/26833/) +* Assignment trails: + * We could also consider the assignments to variables during search. + * Variables that are always assigned to the same truth value could be considered to be safe to assign that truth value. + * The cubes resulting from such variables might be a direction towards finding satisfying solutions. + * Selected references: [Alex and Vadim](https://link.springer.com/chapter/10.1007/978-3-319-94144-8_7) and most recently [Robin et al](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9). + + +## Algorithms + +This section considers various possible algorithms. +In the following, $F$ refers to the original goal, $T$ is the number of CPU cores or CPU threads. + +### Base algorithm + +The existing algorithm in smt_parallel is as follows: + +1. Run a solver on $F$ with a bounded number of conflicts. +2. If the result is SAT/UNSAT, or UNKNOWN with an interrupt or timeout, return. If the maximal number of conflicts were reached continue. +3. Spawn $T$ solvers on $F$ with a bounded number of conflicts, wait until a thread returns UNSAT/SAT or all threads have reached a maximal number of conflicts. +4. Perform a similar check as in 2. +5. Share unit literals learned by each thread. +6. Compute unit cubes for each thread $T$. +7. Spawn $T$ solvers with $F \wedge \ell$, where $\ell$ is a unit literal determined by lookahead function in each thread. +8. Perform a similar check as in 2. But note that a thread can be UNSAT because the unit cube $\ell$ contradicted $F$. In this case learn the unit literal $\neg \ell$. +9. Shared unit literals learned by each thread, increase the maximal number of conflicts, go to 3. + +### Algorithm Variants + +* Instead of using lookahead solving to find unit cubes use the proof-prefix based scoring function. +* Instead of using independent unit cubes, perform a systematic (where systematic can mean many things) cube and conquer strategy. +* Spawn some threads to work in "SAT" mode, tuning to find models instead of short resolution proofs. +* Change the synchronization barrier discipline. +* [Future] Include in-processing + +### Cube and Conquer strategy + +We could maintain a global decomposition of the search space by maintaing a list of _cubes_. +Initially, the list of cubes has just one element, the cube with no literals $[ [] ]$. +By using a list of cubes instead of a _set_ of cubes we can refer to an ordering. +For example, cubes can be ordered by a suffix traversal of the _cube tree_ (the tree formed by +case splitting on the first literal, children of the _true_ branch are the cubes where the first +literal is true, children of the _false_ branch are the cubes where the first literal is false). + +The main question is going to be how the cube decomposition is created. + +#### Static cubing +We can aim for a static cube strategy that uses a few initial (concurrent) probes to find cube literals. +This strategy would be a parallel implementaiton of proof-prefix approach. The computed cubes are inserted +into the list of cubes and the list is consumed by a second round. + +#### Growing cubes on demand +Based on experiences with cubing so far, there is high variance in how easy cubes are to solve. +Some cubes will be harder than others to solve. For hard cubes, it is tempting to develop a recursive +cubing strategy. Ideally, a recursive cubing strategy is symmetric to top-level cubing. + +* The solver would have to identify hard cubes vs. easy cubes. +* It would have to know when to stop working on a hard cube and replace it in the list of cubes by + a new list of sub-cubes. + +* Ideally, we don't need any static cubing and cubing is grown on demand while all threads are utilized. + * If we spawn $T$ threads to initially work with empty cubes, we could extract up to $T$ indepenent cubes + by examining the proof-prefix of their traces. This can form the basis for the first, up to $2^T$ cubes. + * After a round of solving with each thread churning on some cubes, we may obtain more proof-prefixes from + _hard_ cubes. It is not obvious that we want to share cubes from different proof prefixes at this point. + But a starting point is to split a hard cube into two by using the proof-prefix from attempting to solve it. + * Suppose we take the proof-prefix sampling algorithm at heart: It says to start with some initial cube prefix + and then sample for other cube literals. If we translate it to the case where multiple cubes are being processed + in parallel, then an analogy is to share candidates for new cube literals among cubes that are close to each-other. + For example, if thread $t_1$ processes cube $a, b, c$ and $t_2$ processes $a,b, \neg c$. They are close. They are only + separated by Hamming distance 1. If $t_1$ finds cube literal $d$ and $t_2$ finds cube literal $e$, we could consider the cubes + $a, b, c, d, e$, and $a, b, c, d, \neg e$, $\ldots$, $a, b, \neg c, \neg d, \neg e$. + +#### Representing cubes implicitly + +We can represent a list of cubes by using intervals and only represent start and end-points of the intervals. + +#### Batching +Threads can work on more than one cube in a batch. + +### Synchronization + +* The first thread to time out or finish could kill other threads instead of joining on all threads to finish. +* Instead of synchronization barriers have threads continue concurrently without terminating. They synchronize on signals and new units. This is trickier to implement, but in some guises accomplished in [sat/sat_parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/sat/sat_parallel.cpp) + + +## Parameter tuning + +The idea is to have parallel threads try out different parameter settings and search the parameter space of an optimal parameter setting. + +Let us assume that there is a set of tunable parameters $P$. The set comprises of a set of named parameters with initial values. +$P = \{ (p_1, v_1), \ldots, (p_n, v_n) \}$. +With each parameter associate a set of mutation functions $+=, -=, *=$, such as increment, decrement, scale a parameter by a non-negative multiplier (which can be less than 1). +We will initialize a search space of parameter settings by parameters, values and mutation functions that have assigned reward values. The reward value is incremented +if a parameter mutation step results in an improvement, and decremented if a mutation step degrades performance. +$P = \{ (p_1, v_1, \{ (r_{11}, m_{11}), \ldots, (r_{1k_1}, m_{1k_1}) \}), \ldots, (p_n, v_n, \{ (r_{n1}, m_{n1}), \ldots, (r_{nk_n}, m_{nk_n})\}) \}$. +The initial values of reward functions is fixed (to 1) and the initial values of parameters are the defaults. + +* The batch manager maintains a set of candidate parameters $CP = \{ (P_1, r_1), \ldots, (P_n, r_n) \}$. +* A worker thread picks up a parameter $P_i$ from $CP$ from the batch manager. +* It picks one or more parameter settings within $P_i$ whose mutation function have non-zero reward functions and applies a mutation. +* It then runs with a batch of cubes. +* It measures the reward for the new parameter setting based in number of cubes, cube depth, number of timeouts, and completions with number of conflicts. +* If the new reward is an improvement over $(P_i, r_i)$ it inserts the new parameter setting $(P_i', r_i')$ into the batch manager. +* The batch manager discards the worst parameter settings keeping the top $K$ ($K = 5$) parameter settings. + +When picking among mutation steps with reward functions use a weighted sampling algorithm. +Weighted sampling works as follows: You are given a set of items with weights $(i_1, w_1), \ldots, (i_k, w_k)$. +Add $w = \sum_j w_j$. Pick a random number $w_0$ in the range $0\ldots w$. +Then you pick item $i_n$ such that $n$ is the smallest index with $\sum_{j = 1}^n w_j \geq w_0$. + +SMT parameters that could be tuned: + +
+
+  arith.bprop_on_pivoted_rows (bool) (default: true)
+  arith.branch_cut_ratio (unsigned int) (default: 2)
+  arith.eager_eq_axioms (bool) (default: true)
+  arith.enable_hnf (bool) (default: true)
+  arith.greatest_error_pivot (bool) (default: false)
+  arith.int_eq_branch (bool) (default: false)
+  arith.min (bool) (default: false)
+  arith.nl.branching (bool) (default: true)
+  arith.nl.cross_nested (bool) (default: true)
+  arith.nl.delay (unsigned int) (default: 10)
+  arith.nl.expensive_patching (bool) (default: false)
+  arith.nl.expp (bool) (default: false)
+  arith.nl.gr_q (unsigned int) (default: 10)
+  arith.nl.grobner (bool) (default: true)
+  arith.nl.grobner_cnfl_to_report (unsigned int) (default: 1)
+  arith.nl.grobner_eqs_growth (unsigned int) (default: 10)
+  arith.nl.grobner_expr_degree_growth (unsigned int) (default: 2)
+  arith.nl.grobner_expr_size_growth (unsigned int) (default: 2)
+  arith.nl.grobner_frequency (unsigned int) (default: 4)
+  arith.nl.grobner_max_simplified (unsigned int) (default: 10000)
+  arith.nl.grobner_row_length_limit (unsigned int) (default: 10)
+  arith.nl.grobner_subs_fixed (unsigned int) (default: 1)
+  arith.nl.horner (bool) (default: true)
+  arith.nl.horner_frequency (unsigned int) (default: 4)
+  arith.nl.horner_row_length_limit (unsigned int) (default: 10)
+  arith.nl.horner_subs_fixed (unsigned int) (default: 2)
+  arith.nl.nra (bool) (default: true)
+  arith.nl.optimize_bounds (bool) (default: true)
+  arith.nl.order (bool) (default: true)
+  arith.nl.propagate_linear_monomials (bool) (default: true)
+  arith.nl.rounds (unsigned int) (default: 1024)
+  arith.nl.tangents (bool) (default: true)
+  arith.propagate_eqs (bool) (default: true)
+  arith.propagation_mode (unsigned int) (default: 1)
+  arith.random_initial_value (bool) (default: false)
+  arith.rep_freq (unsigned int) (default: 0)
+  arith.simplex_strategy (unsigned int) (default: 0)
+  dack (unsigned int) (default: 1)
+  dack.eq (bool) (default: false)
+  dack.factor (double) (default: 0.1)
+  dack.gc (unsigned int) (default: 2000)
+  dack.gc_inv_decay (double) (default: 0.8)
+  dack.threshold (unsigned int) (default: 10)
+  delay_units (bool) (default: false)
+  delay_units_threshold (unsigned int) (default: 32)
+  dt_lazy_splits (unsigned int) (default: 1)
+  lemma_gc_strategy (unsigned int) (default: 0)
+  phase_caching_off (unsigned int) (default: 100)
+  phase_caching_on (unsigned int) (default: 400)
+  phase_selection (unsigned int) (default: 3)
+  qi.eager_threshold (double) (default: 10.0)
+  qi.lazy_threshold (double) (default: 20.0)
+  qi.quick_checker (unsigned int) (default: 0)
+  relevancy (unsigned int) (default: 2)
+  restart_factor (double) (default: 1.1)
+  restart_strategy (unsigned int) (default: 1)
+  seq.max_unfolding (unsigned int) (default: 1000000000)
+  seq.min_unfolding (unsigned int) (default: 1)
+  seq.split_w_len (bool) (default: true)
+
+ + diff --git a/run_local_tests.sh b/run_local_tests.sh new file mode 100755 index 000000000..e9bd45bad --- /dev/null +++ b/run_local_tests.sh @@ -0,0 +1,32 @@ +#!/bin/bash +# run from inside ./z3/build + +Z3=./z3 +OPTIONS="-v:0 -st smt.threads=4" +OUT_FILE="../z3_results.txt" +BASE_PATH="../../z3-poly-testing/inputs/" + +# List of relative test files (relative to BASE_PATH) +REL_TEST_FILES=( + "QF_NIA_small/Ton_Chanh_15__Singapore_v1_false-termination.c__p27381_terminationG_0.smt2" + "QF_UFDTLIA_SAT/52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2" +) + +# Clear output file +> "$OUT_FILE" + +# Loop through and run Z3 on each file +for rel_path in "${REL_TEST_FILES[@]}"; do + full_path="$BASE_PATH$rel_path" + test_name="$rel_path" + + echo "Running: $test_name" + echo "===== $test_name =====" | tee -a "$OUT_FILE" + + # Run Z3 and pipe output to both screen and file + $Z3 "$full_path" $OPTIONS 2>&1 | tee -a "$OUT_FILE" + + echo "" | tee -a "$OUT_FILE" +done + +echo "Results written to $OUT_FILE" diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 9a0f572dd..0ad9639f2 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -5153,6 +5153,8 @@ namespace polynomial { // unsigned sz = R->size(); for (unsigned i = 0; i < sz; i++) { + if (sz > 100 && i % 100 == 0) + checkpoint(); monomial * m = R->m(i); numeral const & a = R->a(i); if (m->degree_of(x) == deg_R) { @@ -5571,6 +5573,7 @@ namespace polynomial { h = mk_one(); while (true) { + checkpoint(); TRACE(resultant, tout << "A: " << A << "\nB: " << B << "\n";); degA = degree(A, x); degB = degree(B, x); diff --git a/src/smt/priority_queue.h b/src/smt/priority_queue.h new file mode 100644 index 000000000..39deab9bb --- /dev/null +++ b/src/smt/priority_queue.h @@ -0,0 +1,191 @@ +// SOURCE: https://github.com/Ten0/updatable_priority_queue/blob/master/updatable_priority_queue.h + +#include +#include + +namespace updatable_priority_queue { + template + struct priority_queue_node { + Priority priority; + Key key; + priority_queue_node(const Key& key, const Priority& priority) : priority(priority), key(key) {} + friend bool operator<(const priority_queue_node& pqn1, const priority_queue_node& pqn2) { + return pqn1.priority > pqn2.priority; + } + friend bool operator>(const priority_queue_node& pqn1, const priority_queue_node& pqn2) { + return pqn1.priority < pqn2.priority; + } + }; + + /** Key has to be an uint value (convertible to size_t) + * This is a max heap (max is on top), to match stl's pQ */ + template + class priority_queue { + protected: + std::vector id_to_heappos; + std::vector> heap; + std::size_t max_size = 4; // std::numeric_limits::max(); // Create a variable max_size that defaults to the largest size_t value possible + + public: + // priority_queue() {} + priority_queue(std::size_t max_size = std::numeric_limits::max()): max_size(max_size) {} + + // Returns a const reference to the internal heap storage + const std::vector>& get_heap() const { + return heap; + } + + bool empty() const { return heap.empty(); } + std::size_t size() const { return heap.size(); } + + /** first is priority, second is key */ + const priority_queue_node& top() const { return heap.front(); } + + void pop(bool remember_key=false) { + if(size() == 0) return; + id_to_heappos[heap.front().key] = -1-remember_key; + if(size() > 1) { + *heap.begin() = std::move(*(heap.end()-1)); + id_to_heappos[heap.front().key] = 0; + } + heap.pop_back(); + sift_down(0); + } + + priority_queue_node pop_value(bool remember_key=true) { + if(size() == 0) return priority_queue_node(-1, Priority()); + priority_queue_node ret = std::move(*heap.begin()); + id_to_heappos[ret.key] = -1-remember_key; + if(size() > 1) { + *heap.begin() = std::move(*(heap.end()-1)); + id_to_heappos[heap.front().key] = 0; + } + heap.pop_back(); + sift_down(0); + return ret; + } + + /** Sets the priority for the given key. If not present, it will be added, otherwise it will be updated + * Returns true if the priority was changed. + * */ + bool set(const Key& key, const Priority& priority, bool only_if_higher=false) { + if(key < id_to_heappos.size() && id_to_heappos[key] < ((size_t)-2)) // This key is already in the pQ + return update(key, priority, only_if_higher); + else + return push(key, priority, only_if_higher); + } + + std::pair get_priority(const Key& key) { + if(key < id_to_heappos.size()) { + size_t pos = id_to_heappos[key]; + if(pos < ((size_t)-2)) { + return {true, heap[pos].priority}; + } + } + return {false, 0}; + } + + /** Returns true if the key was not inside and was added, otherwise does nothing and returns false + * If the key was remembered and only_if_unknown is true, does nothing and returns false + * */ + bool push(const Key& key, const Priority& priority, bool only_if_unknown = false) { + extend_ids(key); + if (id_to_heappos[key] < ((size_t)-2)) return false; // already inside + if (only_if_unknown && id_to_heappos[key] == ((size_t)-2)) return false; // was evicted and only_if_unknown prevents re-adding + + if (heap.size() < max_size) { + // We have room: just add new element + size_t n = heap.size(); + id_to_heappos[key] = n; + heap.emplace_back(key, priority); + sift_up(n); + return true; + } else { + // Heap full: heap[0] is the smallest priority in the top-k (min-heap) + if (priority <= heap[0].priority) { + // New element priority too small or equal, discard it + return false; + } + // Evict smallest element at heap[0] + Key evicted_key = heap[0].key; + id_to_heappos[evicted_key] = -2; // Mark evicted + + heap[0] = priority_queue_node(key, priority); + id_to_heappos[key] = 0; + sift_down(0); // restore min-heap property + return true; + } + } + + + + /** Returns true if the key was already inside and was updated, otherwise does nothing and returns false */ + bool update(const Key& key, const Priority& new_priority, bool only_if_higher=false) { + if(key >= id_to_heappos.size()) return false; + size_t heappos = id_to_heappos[key]; + if(heappos >= ((size_t)-2)) return false; + Priority& priority = heap[heappos].priority; + if(new_priority > priority) { + priority = new_priority; + sift_up(heappos); + return true; + } + else if(!only_if_higher && new_priority < priority) { + priority = new_priority; + sift_down(heappos); + return true; + } + return false; + } + + void clear() { + heap.clear(); + id_to_heappos.clear(); + } + + + private: + void extend_ids(Key k) { + size_t new_size = k+1; + if(id_to_heappos.size() < new_size) + id_to_heappos.resize(new_size, -1); + } + + void sift_down(size_t heappos) { + size_t len = heap.size(); + size_t child = heappos*2+1; + if(len < 2 || child >= len) return; + if(child+1 < len && heap[child+1] > heap[child]) ++child; // Check whether second child is higher + if(!(heap[child] > heap[heappos])) return; // Already in heap order + + priority_queue_node val = std::move(heap[heappos]); + do { + heap[heappos] = std::move(heap[child]); + id_to_heappos[heap[heappos].key] = heappos; + heappos = child; + child = 2*child+1; + if(child >= len) break; + if(child+1 < len && heap[child+1] > heap[child]) ++child; + } while(heap[child] > val); + heap[heappos] = std::move(val); + id_to_heappos[heap[heappos].key] = heappos; + } + + void sift_up(size_t heappos) { + size_t len = heap.size(); + if(len < 2 || heappos <= 0) return; + size_t parent = (heappos-1)/2; + if(!(heap[heappos] > heap[parent])) return; + priority_queue_node val = std::move(heap[heappos]); + do { + heap[heappos] = std::move(heap[parent]); + id_to_heappos[heap[heappos].key] = heappos; + heappos = parent; + if(heappos <= 0) break; + parent = (parent-1)/2; + } while(val > heap[parent]); + heap[heappos] = std::move(val); + id_to_heappos[heap[heappos].key] = heappos; + } + }; +} \ No newline at end of file diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 2fbc1d705..63316a331 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -50,6 +50,8 @@ Revision History: #include "model/model.h" #include "solver/progress_callback.h" #include "solver/assertions/asserted_formulas.h" +#include "smt/priority_queue.h" +#include "util/dlist.h" #include // there is a significant space overhead with allocating 1000+ contexts in @@ -189,6 +191,17 @@ namespace smt { unsigned_vector m_lit_occs; //!< occurrence count of literals svector m_bdata; //!< mapping bool_var -> data svector m_activity; + updatable_priority_queue::priority_queue m_pq_scores; + + struct lit_node : dll_base { + literal lit; + lit_node(literal l) : lit(l) { init(this); } + }; + lit_node* m_dll_lits; + + // svector> m_lit_scores; + svector m_lit_scores[2]; + clause_vector m_aux_clauses; clause_vector m_lemmas; vector m_clauses_to_reinit; @@ -933,6 +946,17 @@ namespace smt { ast_pp_util m_lemma_visitor; void dump_lemma(unsigned n, literal const* lits); void dump_axiom(unsigned n, literal const* lits); + void add_scores(unsigned n, literal const* lits); + void reset_scores() { + for (auto& e : m_lit_scores[0]) + e = 0; + for (auto& e : m_lit_scores[1]) + e = 0; + m_pq_scores.clear(); // Clear the priority queue heap as well + } + double get_score(literal l) const { + return m_lit_scores[l.sign()][l.var()]; + } public: void ensure_internalized(expr* e); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 9aa6d68f4..c7e257fac 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -931,6 +931,10 @@ namespace smt { set_bool_var(id, v); m_bdata.reserve(v+1); m_activity.reserve(v+1); + m_lit_scores[0].reserve(v + 1); + m_lit_scores[1].reserve(v + 1); + + m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0; m_bool_var2expr.reserve(v+1); m_bool_var2expr[v] = n; literal l(v, false); @@ -1419,6 +1423,7 @@ namespace smt { break; case CLS_LEARNED: dump_lemma(num_lits, lits); + add_scores(num_lits, lits); break; default: break; @@ -1527,6 +1532,27 @@ namespace smt { }} } + // void context::add_scores(unsigned n, literal const* lits) { + // for (unsigned i = 0; i < n; ++i) { + // auto lit = lits[i]; + // unsigned v = lit.var(); + // m_lit_scores[v][lit.sign()] += 1.0 / n; + // } + // } + + void context::add_scores(unsigned n, literal const* lits) { + for (unsigned i = 0; i < n; ++i) { + auto lit = lits[i]; + unsigned v = lit.var(); // unique key per literal + + m_lit_scores[lit.sign()][v] += 1.0 / n; + + auto new_score = m_lit_scores[0][v] * m_lit_scores[1][v]; + m_pq_scores.set(v, new_score); + + } + } + void context::dump_axiom(unsigned n, literal const* lits) { if (m_fparams.m_axioms2files) { literal_buffer tmp; diff --git a/src/smt/smt_lookahead.h b/src/smt/smt_lookahead.h index 5deccad2c..d53af58e4 100644 --- a/src/smt/smt_lookahead.h +++ b/src/smt/smt_lookahead.h @@ -30,11 +30,13 @@ namespace smt { struct compare; - double get_score(); + // double get_score(); void choose_rec(expr_ref_vector& trail, expr_ref_vector& result, unsigned depth, unsigned budget); public: + double get_score(); + lookahead(context& ctx); expr_ref choose(unsigned budget = 2000); diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 4941e4df9..d08a7c045 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -36,237 +36,463 @@ namespace smt { #else #include +#include namespace smt { + + void parallel::worker::run() { + ast_translation g2l(p.ctx.m, m); // global to local context -- MUST USE p.ctx.m, not ctx->m, AS GLOBAL MANAGER!!! + ast_translation l2g(m, p.ctx.m); // local to global context + while (m.inc()) { // inc: increase the limit and check if it is canceled, vs m.limit().is_canceled() is readonly. the .limit() is also not necessary (m.inc() etc provides a convenience wrapper) + vector cubes; + b.get_cubes(g2l, cubes); + if (cubes.empty()) + return; + collect_shared_clauses(g2l); + for (auto& cube : cubes) { + if (!m.inc()) { + b.set_exception("context cancelled"); + return; + } + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n"); + lbool r = check_cube(cube); + if (m.limit().is_canceled()) { + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " context cancelled\n"); + return; + } + switch (r) { + case l_undef: { + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found undef cube\n"); + // return unprocessed cubes to the batch manager + // add a split literal to the batch manager. + // optionally process other cubes and delay sending back unprocessed cubes to batch manager. + vector returned_cubes; + returned_cubes.push_back(cube); + auto split_atoms = get_split_atoms(); + b.return_cubes(l2g, returned_cubes, split_atoms); + update_max_thread_conflicts(); + break; + } + case l_true: { + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found sat cube\n"); + model_ref mdl; + ctx->get_model(mdl); + b.set_sat(l2g, *mdl); + return; + } + case l_false: { + // if unsat core only contains (external) assumptions (i.e. all the unsat core are asms), then unsat and return as this does NOT depend on cubes + // otherwise, extract lemmas that can be shared (units (and unsat core?)). + // share with batch manager. + // process next cube. + expr_ref_vector const& unsat_core = ctx->unsat_core(); + IF_VERBOSE(1, verbose_stream() << "unsat core: " << unsat_core << "\n"); + // If the unsat core only contains assumptions, + // unsatisfiability does not depend on the current cube and the entire problem is unsat. + if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " determined formula unsat\n"); + b.set_unsat(l2g, unsat_core); + return; + } + for (expr* e : unsat_core) + if (asms.contains(e)) + b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core + + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found unsat cube\n"); + b.collect_clause(l2g, id, mk_not(mk_and(unsat_core))); + break; + } + } + } + share_units(l2g); + } + } + + parallel::worker::worker(unsigned id, parallel& p, expr_ref_vector const& _asms): id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m) { + ast_translation g2l(p.ctx.m, m); + for (auto e : _asms) + asms.push_back(g2l(e)); + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " created with " << asms.size() << " assumptions\n"); + m_smt_params.m_preprocess = false; + ctx = alloc(context, m, m_smt_params, p.ctx.get_params()); + context::copy(p.ctx, *ctx, true); + ctx->set_random_seed(id + m_smt_params.m_random_seed); + + m_max_thread_conflicts = ctx->get_fparams().m_threads_max_conflicts; + m_max_conflicts = ctx->get_fparams().m_max_conflicts; + } + + void parallel::worker::share_units(ast_translation& l2g) { + // Collect new units learned locally by this worker and send to batch manager + unsigned sz = ctx->assigned_literals().size(); + for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync + literal lit = ctx->assigned_literals()[j]; + expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression + if (lit.sign()) + e = m.mk_not(e); // negate if literal is negative + b.collect_clause(l2g, id, e); + } + m_num_shared_units = sz; + } + + void parallel::batch_manager::collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause) { + std::scoped_lock lock(mux); + expr* g_clause = l2g(clause); + if (!shared_clause_set.contains(g_clause)) { + shared_clause_set.insert(g_clause); + shared_clause sc{source_worker_id, expr_ref(g_clause, m)}; + shared_clause_trail.push_back(sc); + } + } + + void parallel::worker::collect_shared_clauses(ast_translation& g2l) { + expr_ref_vector new_clauses = b.return_shared_clauses(g2l, m_shared_clause_limit, id); // get new clauses from the batch manager + // iterate over new clauses and assert them in the local context + for (expr* e : new_clauses) { + expr_ref local_clause(e, g2l.to()); // e was already translated to the local context in the batch manager!! + ctx->assert_expr(local_clause); // assert the clause in the local context + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n"); + } + } + + // get new clauses from the batch manager and assert them in the local context + expr_ref_vector parallel::batch_manager::return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id) { + std::scoped_lock lock(mux); + expr_ref_vector result(g2l.to()); + for (unsigned i = worker_limit; i < shared_clause_trail.size(); ++i) { + if (shared_clause_trail[i].source_worker_id == worker_id) + continue; // skip clauses from the requesting worker + result.push_back(g2l(shared_clause_trail[i].clause.get())); + } + worker_limit = shared_clause_trail.size(); // update the worker limit to the end of the current trail + return result; + } + + lbool parallel::worker::check_cube(expr_ref_vector const& cube) { + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " checking cube\n";); + for (auto& atom : cube) + asms.push_back(atom); + lbool r = l_undef; + + ctx->get_fparams().m_max_conflicts = std::min(m_max_thread_conflicts, m_max_conflicts); + try { + r = ctx->check(asms.size(), asms.data()); + } + catch (z3_error& err) { + b.set_exception(err.error_code()); + } + catch (z3_exception& ex) { + b.set_exception(ex.what()); + } + catch (...) { + b.set_exception("unknown exception"); + } + asms.shrink(asms.size() - cube.size()); + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " DONE checking cube " << r << "\n";); + return r; + } + + void parallel::batch_manager::get_cubes(ast_translation& g2l, vector& cubes) { + std::scoped_lock lock(mux); + if (m_cubes.size() == 1 && m_cubes[0].size() == 0) { + // special initialization: the first cube is emtpy, have the worker work on an empty cube. + cubes.push_back(expr_ref_vector(g2l.to())); + return; + } + + for (unsigned i = 0; i < std::min(m_max_batch_size / p.num_threads, (unsigned)m_cubes.size()) && !m_cubes.empty(); ++i) { + auto& cube = m_cubes.back(); + expr_ref_vector l_cube(g2l.to()); + for (auto& e : cube) { + l_cube.push_back(g2l(e)); + } + cubes.push_back(l_cube); + m_cubes.pop_back(); + } + } + + void parallel::batch_manager::set_sat(ast_translation& l2g, model& m) { + std::scoped_lock lock(mux); + if (m_state != state::is_running) + return; + m_state = state::is_sat; + p.ctx.set_model(m.translate(l2g)); + cancel_workers(); + } + + void parallel::batch_manager::set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core) { + std::scoped_lock lock(mux); + if (m_state != state::is_running) + return; + m_state = state::is_unsat; + + // every time we do a check_sat call, don't want to have old info coming from a prev check_sat call + // the unsat core gets reset internally in the context after each check_sat, so we assert this property here + // takeaway: each call to check_sat needs to have a fresh unsat core + SASSERT(p.ctx.m_unsat_core.empty()); + for (expr* e : unsat_core) + p.ctx.m_unsat_core.push_back(l2g(e)); + cancel_workers(); + } + + void parallel::batch_manager::set_exception(unsigned error_code) { + std::scoped_lock lock(mux); + if (m_state != state::is_running) + return; + m_state = state::is_exception_code; + m_exception_code = error_code; + cancel_workers(); + } + + void parallel::batch_manager::set_exception(std::string const& msg) { + std::scoped_lock lock(mux); + if (m_state != state::is_running || m.limit().is_canceled()) + return; + m_state = state::is_exception_msg; + m_exception_msg = msg; + cancel_workers(); + } + + void parallel::batch_manager::report_assumption_used(ast_translation& l2g, expr* assumption) { + std::scoped_lock lock(mux); + p.m_assumptions_used.insert(l2g(assumption)); + } + + lbool parallel::batch_manager::get_result() const { + if (m.limit().is_canceled()) + return l_undef; // the main context was cancelled, so we return undef. + switch (m_state) { + case state::is_running: // batch manager is still running, but all threads have processed their cubes, which means all cubes were unsat + if (!m_cubes.empty()) + throw default_exception("inconsistent end state"); + if (!p.m_assumptions_used.empty()) { + // collect unsat core from assumptions used, if any --> case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core + SASSERT(p.ctx.m_unsat_core.empty()); + for (auto a : p.m_assumptions_used) + p.ctx.m_unsat_core.push_back(a); + } + return l_false; + case state::is_unsat: + return l_false; + case state::is_sat: + return l_true; + case state::is_exception_msg: + throw default_exception(m_exception_msg.c_str()); + case state::is_exception_code: + throw z3_error(m_exception_code); + default: + UNREACHABLE(); + return l_undef; + } + } + + /* + Batch manager maintains C_batch, A_batch. + C_batch - set of cubes + A_batch - set of split atoms. + return_cubes is called with C_batch A_batch C A. + C_worker - one or more cubes + A_worker - split atoms form the worker thread. - lbool parallel::operator()(expr_ref_vector const& asms) { + Assumption: A_worker does not occur in C_worker. + + ------------------------------------------------------------------------------------------------------------------------------------------------------------ + Greedy strategy: + For each returned cube c from the worker, you split it on all split atoms not in it (i.e., A_batch \ atoms(c)), plus any new atoms from A_worker. + For each existing cube in the batch, you also split it on the new atoms from A_worker. + + return_cubes C_batch A_batch C_worker A_worker: + C_batch <- { cube * 2^(A_worker u (A_batch \ atoms(cube)) | cube in C_worker } u + { cube * 2^(A_worker \ A_batch) | cube in C_batch } + = + let C_batch' = C_batch u { cube * 2^(A_batch \ atoms(cube)) | cube in C_worker } + in { cube * 2^(A_worker \ A_batch) | cube in C_batch' } + A_batch <- A_batch u A_worker + + ------------------------------------------------------------------------------------------------------------------------------------------------------------ + Frugal strategy: only split on worker cubes + + case 1: thread returns no cubes, just atoms: just create 2^k cubes from all combinations of atoms so far. + return_cubes C_batch A_batch [[]] A_worker: + C_batch <- C_batch u 2^(A_worker u A_batch), + A_batch <- A_batch u A_worker + + case 2: thread returns both cubes and atoms + Only the returned cubes get split by the newly discovered atoms (A_worker). Existing cubes are not touched. + return_cubes C_batch A_batch C_worker A_worker: + C_batch <- C_batch u { cube * 2^A_worker | cube in C_worker }. + A_batch <- A_batch u A_worker + + This means: + Only the returned cubes get split by the newly discovered atoms (A_worker). + Existing cubes are not touched. + + ------------------------------------------------------------------------------------------------------------------------------------------------------------ + Hybrid: Between Frugal and Greedy: (generalizes the first case of empty cube returned by worker) -- don't focus on this approach + i.e. Expand only the returned cubes, but allow them to be split on both new and old atoms not already in them. + + C_batch <- C_batch u { cube * 2^(A_worker u (A_batch \ atoms(cube)) | cube in C_worker } + A_batch <- A_batch u A_worker + + ------------------------------------------------------------------------------------------------------------------------------------------------------------ + Final thought (do this!): use greedy strategy by a policy when C_batch, A_batch, A_worker are "small". -- want to do this. switch to frugal strategy after reaching size limit + */ - lbool result = l_undef; - unsigned num_threads = std::min((unsigned) std::thread::hardware_concurrency(), ctx.get_fparams().m_threads); - flet _nt(ctx.m_fparams.m_threads, 1); - unsigned thread_max_conflicts = ctx.get_fparams().m_threads_max_conflicts; - unsigned max_conflicts = ctx.get_fparams().m_max_conflicts; - - // try first sequential with a low conflict budget to make super easy problems cheap - unsigned max_c = std::min(thread_max_conflicts, 40u); - flet _mc(ctx.get_fparams().m_max_conflicts, max_c); - result = ctx.check(asms.size(), asms.data()); - if (result != l_undef || ctx.m_num_conflicts < max_c) { - return result; - } - - enum par_exception_kind { - DEFAULT_EX, - ERROR_EX + // currenly, the code just implements the greedy strategy + void parallel::batch_manager::return_cubes(ast_translation& l2g, vectorconst& C_worker, expr_ref_vector const& A_worker) { + auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) { + return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); }); }; - vector smt_params; - scoped_ptr_vector pms; - scoped_ptr_vector pctxs; - vector pasms; + auto add_split_atom = [&](expr* atom, unsigned start) { + unsigned stop = m_cubes.size(); + for (unsigned i = start; i < stop; ++i) { + m_cubes.push_back(m_cubes[i]); + m_cubes.back().push_back(m.mk_not(atom)); + m_cubes[i].push_back(atom); + } + }; + std::scoped_lock lock(mux); + unsigned max_cubes = 1000; + bool greedy_mode = (m_cubes.size() <= max_cubes); + unsigned a_worker_start_idx = 0; + + // + // --- Phase 1: Greedy split of *existing* cubes on new A_worker atoms (greedy) --- + // + if (greedy_mode) { + for (; a_worker_start_idx < A_worker.size(); ++a_worker_start_idx) { + expr_ref g_atom(l2g(A_worker[a_worker_start_idx]), l2g.to()); + if (m_split_atoms.contains(g_atom)) + continue; + m_split_atoms.push_back(g_atom); + + add_split_atom(g_atom, 0); // split all *existing* cubes + if (m_cubes.size() > max_cubes) { + greedy_mode = false; + ++a_worker_start_idx; // start frugal from here + break; + } + } + } + + unsigned initial_m_cubes_size = m_cubes.size(); // where to start processing the worker cubes after splitting the EXISTING cubes on the new worker atoms + + // --- Phase 2: Process worker cubes (greedy) --- + for (auto& c : C_worker) { + expr_ref_vector g_cube(l2g.to()); + for (auto& atom : c) + g_cube.push_back(l2g(atom)); + + unsigned start = m_cubes.size(); // update start after adding each cube so we only process the current cube being added + m_cubes.push_back(g_cube); + + if (greedy_mode) { + // Split new cube on all existing m_split_atoms not in it + for (auto g_atom : m_split_atoms) { + if (!atom_in_cube(g_cube, g_atom)) { + add_split_atom(g_atom, start); + if (m_cubes.size() > max_cubes) { + greedy_mode = false; + break; + } + } + } + } + } + + // --- Phase 3: Frugal fallback: only process NEW worker cubes with NEW atoms --- + if (!greedy_mode) { + for (unsigned i = a_worker_start_idx; i < A_worker.size(); ++i) { + expr_ref g_atom(l2g(A_worker[i]), l2g.to()); + if (!m_split_atoms.contains(g_atom)) + m_split_atoms.push_back(g_atom); + add_split_atom(g_atom, initial_m_cubes_size); + } + } + } + + expr_ref_vector parallel::worker::get_split_atoms() { + unsigned k = 2; + + auto candidates = ctx->m_pq_scores.get_heap(); + + std::sort(candidates.begin(), candidates.end(), + [](const auto& a, const auto& b) { return a.priority > b.priority; }); + + expr_ref_vector top_lits(m); + for (const auto& node: candidates) { + if (ctx->get_assignment(node.key) != l_undef) + continue; + + expr* e = ctx->bool_var2expr(node.key); + if (!e) + continue; + + top_lits.push_back(expr_ref(e, m)); + if (top_lits.size() >= k) + break; + } + IF_VERBOSE(1, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_pq_scores.size() << " num vars " << ctx->get_num_bool_vars() << "\n"); + return top_lits; + } + + void parallel::batch_manager::initialize() { + m_state = state::is_running; + m_cubes.reset(); + m_cubes.push_back(expr_ref_vector(m)); // push empty cube + m_split_atoms.reset(); + } + + lbool parallel::operator()(expr_ref_vector const& asms) { ast_manager& m = ctx.m; - scoped_limits sl(m.limit()); - unsigned finished_id = UINT_MAX; - std::string ex_msg; - par_exception_kind ex_kind = DEFAULT_EX; - unsigned error_code = 0; - bool done = false; - unsigned num_rounds = 0; + if (m.has_trace_stream()) throw default_exception("trace streams have to be off in parallel mode"); - - params_ref params = ctx.get_params(); - for (unsigned i = 0; i < num_threads; ++i) { - smt_params.push_back(ctx.get_fparams()); - smt_params.back().m_preprocess = false; - } - - for (unsigned i = 0; i < num_threads; ++i) { - ast_manager* new_m = alloc(ast_manager, m, true); - pms.push_back(new_m); - pctxs.push_back(alloc(context, *new_m, smt_params[i], params)); - context& new_ctx = *pctxs.back(); - context::copy(ctx, new_ctx, true); - new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed); - ast_translation tr(m, *new_m); - pasms.push_back(tr(asms)); - sl.push_child(&(new_m->limit())); - } - - auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) { - lookahead lh(ctx); - c = lh.choose(); - if (c) { - if ((ctx.get_random_value() % 2) == 0) - c = c.get_manager().mk_not(c); - lasms.push_back(c); - } + struct scoped_clear_table { + obj_hashtable& ht; + scoped_clear_table(obj_hashtable& ht) : ht(ht) {} // Constructor: Takes a reference to a hash table when the object is created and saves it. + ~scoped_clear_table() { ht.reset(); } // Destructor: When the scoped_clear_table object goes out of scope, it automatically calls reset() on that hash table, clearing it }; + scoped_clear_table clear(m_assumptions_used); // creates a scoped_clear_table named clear, bound to m_assumptions_used - obj_hashtable unit_set; - expr_ref_vector unit_trail(ctx.m); - unsigned_vector unit_lim; - for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0); - - std::function collect_units = [&,this]() { - //return; -- has overhead - for (unsigned i = 0; i < num_threads; ++i) { - context& pctx = *pctxs[i]; - pctx.pop_to_base_lvl(); - ast_translation tr(pctx.m, ctx.m); - unsigned sz = pctx.assigned_literals().size(); - for (unsigned j = unit_lim[i]; j < sz; ++j) { - literal lit = pctx.assigned_literals()[j]; - //IF_VERBOSE(0, verbose_stream() << "(smt.thread " << i << " :unit " << lit << " " << pctx.is_relevant(lit.var()) << ")\n";); - if (!pctx.is_relevant(lit.var())) - continue; - expr_ref e(pctx.bool_var2expr(lit.var()), pctx.m); - if (lit.sign()) e = pctx.m.mk_not(e); - expr_ref ce(tr(e.get()), ctx.m); - if (!unit_set.contains(ce)) { - unit_set.insert(ce); - unit_trail.push_back(ce); - } - } - } - - unsigned sz = unit_trail.size(); - for (unsigned i = 0; i < num_threads; ++i) { - context& pctx = *pctxs[i]; - ast_translation tr(ctx.m, pctx.m); - for (unsigned j = unit_lim[i]; j < sz; ++j) { - expr_ref src(ctx.m), dst(pctx.m); - dst = tr(unit_trail.get(j)); - pctx.assert_expr(dst); - } - unit_lim[i] = pctx.assigned_literals().size(); - } - IF_VERBOSE(1, verbose_stream() << "(smt.thread :units " << sz << ")\n"); - }; - - std::mutex mux; - - auto worker_thread = [&](int i) { - try { - context& pctx = *pctxs[i]; - ast_manager& pm = *pms[i]; - expr_ref_vector lasms(pasms[i]); - expr_ref c(pm); - - pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts); - if (num_rounds > 0 && (num_rounds % pctx.get_fparams().m_threads_cube_frequency) == 0) - cube(pctx, lasms, c); - IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; - if (num_rounds > 0) verbose_stream() << " :round " << num_rounds; - if (c) verbose_stream() << " :cube " << mk_bounded_pp(c, pm, 3); - verbose_stream() << ")\n";); - lbool r = pctx.check(lasms.size(), lasms.data()); - - if (r == l_undef && pctx.m_num_conflicts >= max_conflicts) - ; // no-op - else if (r == l_undef && pctx.m_num_conflicts >= thread_max_conflicts) - return; - else if (r == l_false && pctx.unsat_core().contains(c)) { - IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i << " :learn " << mk_bounded_pp(c, pm, 3) << ")"); - pctx.assert_expr(mk_not(mk_and(pctx.unsat_core()))); - return; - } + { + m_batch_manager.initialize(); + m_workers.reset(); + scoped_limits sl(m.limit()); + flet _nt(ctx.m_fparams.m_threads, 1); + SASSERT(num_threads > 1); + for (unsigned i = 0; i < num_threads; ++i) + m_workers.push_back(alloc(worker, i, *this, asms)); // i.e. "new worker(i, *this, asms)" + // THIS WILL ALLOW YOU TO CANCEL ALL THE CHILD THREADS + // within the lexical scope of the code block, creates a data structure that allows you to push children + // objects to the limit object, so if someone cancels the parent object, the cancellation propagates to the children + // and that cancellation has the lifetime of the scope + // even if this code doesn't expliclty kill the main thread, still applies bc if you e.g. Ctrl+C the main thread, the children threads need to be cancelled + for (auto w : m_workers) + sl.push_child(&(w->limit())); - bool first = false; - { - std::lock_guard lock(mux); - if (finished_id == UINT_MAX) { - finished_id = i; - first = true; - result = r; - done = true; - } - if (!first && r != l_undef && result == l_undef) { - finished_id = i; - result = r; - } - else if (!first) return; - } - - for (ast_manager* m : pms) { - if (m != &pm) m->limit().cancel(); - } - - } - catch (z3_error & err) { - if (finished_id == UINT_MAX) { - error_code = err.error_code(); - ex_kind = ERROR_EX; - done = true; - } - } - catch (z3_exception & ex) { - if (finished_id == UINT_MAX) { - ex_msg = ex.what(); - ex_kind = DEFAULT_EX; - done = true; - } - } - catch (...) { - if (finished_id == UINT_MAX) { - ex_msg = "unknown exception"; - ex_kind = ERROR_EX; - done = true; - } - } - }; - - // for debugging: num_threads = 1; - - while (true) { + // Launch threads vector threads(num_threads); for (unsigned i = 0; i < num_threads; ++i) { - threads[i] = std::thread([&, i]() { worker_thread(i); }); + threads[i] = std::thread([&, i]() { + m_workers[i]->run(); + }); } - for (auto & th : threads) { + + // Wait for all threads to finish + for (auto& th : threads) th.join(); - } - if (done) break; - collect_units(); - ++num_rounds; - max_conflicts = (max_conflicts < thread_max_conflicts) ? 0 : (max_conflicts - thread_max_conflicts); - thread_max_conflicts *= 2; + for (auto w : m_workers) + w->collect_statistics(ctx.m_aux_stats); } - for (context* c : pctxs) { - c->collect_statistics(ctx.m_aux_stats); - } - - if (finished_id == UINT_MAX) { - switch (ex_kind) { - case ERROR_EX: throw z3_error(error_code); - default: throw default_exception(std::move(ex_msg)); - } - } - - model_ref mdl; - context& pctx = *pctxs[finished_id]; - ast_translation tr(*pms[finished_id], m); - switch (result) { - case l_true: - pctx.get_model(mdl); - if (mdl) - ctx.set_model(mdl->translate(tr)); - break; - case l_false: - ctx.m_unsat_core.reset(); - for (expr* e : pctx.unsat_core()) - ctx.m_unsat_core.push_back(tr(e)); - break; - default: - break; - } - - return result; + m_workers.clear(); + return m_batch_manager.get_result(); // i.e. all threads have finished all of their cubes -- so if state::is_running is still true, means the entire formula is unsat (otherwise a thread would have returned l_undef) } } diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 07b04019d..b337d5e45 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -19,16 +19,124 @@ Revision History: #pragma once #include "smt/smt_context.h" +#include namespace smt { class parallel { context& ctx; + unsigned num_threads; + + struct shared_clause { + unsigned source_worker_id; + expr_ref clause; + }; + + class batch_manager { + enum state { + is_running, + is_sat, + is_unsat, + is_exception_msg, + is_exception_code + }; + + ast_manager& m; + parallel& p; + std::mutex mux; + state m_state = state::is_running; + expr_ref_vector m_split_atoms; // atoms to split on + vector m_cubes; + unsigned m_max_batch_size = 10; + unsigned m_exception_code = 0; + std::string m_exception_msg; + vector shared_clause_trail; // store all shared clauses with worker IDs + obj_hashtable shared_clause_set; // for duplicate filtering on per-thread clause expressions + + // called from batch manager to cancel other workers if we've reached a verdict + void cancel_workers() { + IF_VERBOSE(1, verbose_stream() << "Canceling workers\n"); + for (auto& w : p.m_workers) + w->cancel(); + } + + public: + batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_split_atoms(m) { } + + void initialize(); + + void set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core); + void set_sat(ast_translation& l2g, model& m); + void set_exception(std::string const& msg); + void set_exception(unsigned error_code); + + // + // worker threads ask the batch manager for a supply of cubes to check. + // they pass in a translation function from the global context to local context (ast-manager). It is called g2l. + // The batch manager returns a list of cubes to solve. + // + void get_cubes(ast_translation& g2l, vector& cubes); + + // + // worker threads return unprocessed cubes to the batch manager together with split literal candidates. + // the batch manager re-enqueues unprocessed cubes and optionally splits them using the split_atoms returned by this and workers. + // + void return_cubes(ast_translation& l2g, vectorconst& cubes, expr_ref_vector const& split_atoms); + void report_assumption_used(ast_translation& l2g, expr* assumption); + void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* e); + expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id); + lbool get_result() const; + }; + + class worker { + unsigned id; // unique identifier for the worker + parallel& p; + batch_manager& b; + ast_manager m; + expr_ref_vector asms; + smt_params m_smt_params; + scoped_ptr ctx; + unsigned m_max_conflicts = 800; // the global budget for all work this worker can do across cubes in the current run. + unsigned m_max_thread_conflicts = 100; // the per-cube limit for how many conflicts the worker can spend on a single cube before timing out on it and moving on + unsigned m_num_shared_units = 0; + unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share + void share_units(ast_translation& l2g); + lbool check_cube(expr_ref_vector const& cube); + void update_max_thread_conflicts() { + m_max_thread_conflicts *= 2; + } // allow for backoff scheme of conflicts within the thread for cube timeouts. + public: + worker(unsigned id, parallel& p, expr_ref_vector const& _asms); + void run(); + expr_ref_vector get_split_atoms(); + void collect_shared_clauses(ast_translation& g2l); + + void cancel() { + IF_VERBOSE(1, verbose_stream() << "Worker " << id << " canceling\n"); + m.limit().cancel(); + } + void collect_statistics(::statistics& st) const { + IF_VERBOSE(1, verbose_stream() << "Collecting statistics for worker " << id << "\n"); + ctx->collect_statistics(st); + } + reslimit& limit() { + return m.limit(); + } + }; + + obj_hashtable m_assumptions_used; // assumptions used in unsat cores, to be used in final core + batch_manager m_batch_manager; + ptr_vector m_workers; + public: - parallel(context& ctx): ctx(ctx) {} + parallel(context& ctx) : + ctx(ctx), + num_threads(std::min( + (unsigned)std::thread::hardware_concurrency(), + ctx.get_fparams().m_threads)), + m_batch_manager(ctx.m, *this) {} lbool operator()(expr_ref_vector const& asms); - }; } From 3abb09133617ec988e978ad1442ea513921773a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Aug 2025 10:23:51 -0700 Subject: [PATCH 05/28] fix #7776 --- src/api/api_solver.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index dad3bc126..c9ce1f5cc 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -146,6 +146,8 @@ extern "C" { bool proofs_enabled = true, models_enabled = true, unsat_core_enabled = false; params_ref p = s->m_params; mk_c(c)->params().get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled); + if (!s->m_solver_factory) + s->m_solver_factory = mk_smt_solver_factory(); s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); param_descrs r; From 57a60c832bafedfaf2a4b51a5b3beeeb9dfd02d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Aug 2025 10:24:12 -0700 Subject: [PATCH 06/28] add > operator as shorthand for Array --- src/api/python/z3/z3.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 16cc45de2..9a9fe5e4a 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -653,6 +653,10 @@ class SortRef(AstRef): """ return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast) + def __gt__(self, other): + """Create the function space Array(self, other)""" + return ArraySort(self, other) + def __hash__(self): """ Hash code. """ return AstRef.__hash__(self) From 237891c901ef3a49ed5c64e9b6bc6a616b44dde3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Aug 2025 10:24:36 -0700 Subject: [PATCH 07/28] updates to euf completion --- src/ast/euf/euf_arith_plugin.cpp | 26 ++++++++++++++++++++++++++ src/ast/simplifiers/euf_completion.cpp | 5 +++++ 2 files changed, 31 insertions(+) diff --git a/src/ast/euf/euf_arith_plugin.cpp b/src/ast/euf/euf_arith_plugin.cpp index df9207a3b..487cc1392 100644 --- a/src/ast/euf/euf_arith_plugin.cpp +++ b/src/ast/euf/euf_arith_plugin.cpp @@ -56,6 +56,32 @@ namespace euf { TRACE(plugin, tout << g.bpp(n) << "\n"); m_add.register_node(n); m_mul.register_node(n); + expr* e = n->get_expr(), * x, * y; + // x - y = x + (* -1 y) + if (a.is_sub(e, x, y)) { + auto& m = g.get_manager(); + auto e1 = a.mk_numeral(rational(-1), a.is_int(x)); + auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr); + auto e2 = a.mk_mul(e1, y); + enode* es1[2] = { n1, g.find(y)}; + auto mul = g.find(e2) ? g.find(e2) : g.mk(e2, 0, 2, es1); + enode* es2[2] = { g.find(x), mul }; + expr* e_add = a.mk_add(x, e2); + auto add = g.find(e_add) ? g.find(e_add): g.mk(e_add, 0, 2, es2); + push_merge(n, add); + } + // c1 * c2 = c1*c2 + rational r1, r2; + if (a.is_mul(e, x, y) && a.is_numeral(x, r1) && a.is_numeral(y, r2)) { + rational r = r1 * r2; + auto e1 = a.mk_numeral(r, a.is_int(x)); + auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr); + push_merge(n, n1); + } + if (a.is_uminus(e, x)) { + NOT_IMPLEMENTED_YET(); + } + } void arith_plugin::merge_eh(enode* n1, enode* n2) { diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index 1a32a1bd5..cea801ae7 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -359,6 +359,11 @@ namespace euf { IF_VERBOSE(1, verbose_stream() << "not: " << nf << "\n"); } else { + expr_ref f1(f, m); + if (!m.is_implies(f) && !is_quantifier(f)) { + m_rewriter(f1); + f = f1; + } enode* n = mk_enode(f); if (m.is_true(n->get_root()->get_expr())) return; From eb7fd9efaae5b235f7792702edc9d6de5a35ef17 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 14 Aug 2025 11:54:34 -0700 Subject: [PATCH 08/28] Add virtual translate method to solver_factory class (#7780) * Initial plan * Add virtual translate method to solver_factory base class and all implementations Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add documentation for the translate method in solver_factory 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> --- src/smt/smt_solver.cpp | 4 ++++ src/solver/combined_solver.cpp | 6 ++++++ src/solver/solver.h | 5 +++++ src/solver/tactic2solver.cpp | 9 +++++++++ src/tactic/portfolio/smt_strategic_solver.cpp | 8 ++++++++ 5 files changed, 32 insertions(+) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 05bcc00ba..1d38c0685 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -527,6 +527,10 @@ public: solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override { return mk_smt_solver(m, p, logic); } + + solver_factory* translate(ast_manager& m) override { + return alloc(smt_solver_factory); + } }; } diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index aacb2b1cc..9f489124f 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -424,6 +424,12 @@ public: (*m_f2)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic), p); } + + solver_factory* translate(ast_manager& m) override { + solver_factory* translated_f1 = m_f1->translate(m); + solver_factory* translated_f2 = m_f2->translate(m); + return alloc(combined_solver_factory, translated_f1, translated_f2); + } }; solver_factory * mk_combined_solver_factory(solver_factory * f1, solver_factory * f2) { diff --git a/src/solver/solver.h b/src/solver/solver.h index 3ddd0b11f..b45f4f347 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -32,6 +32,11 @@ class solver_factory { public: virtual ~solver_factory() = default; virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) = 0; + /** + \brief Create a clone of the solver factory for the given ast_manager. + The clone should be functionally equivalent but associated with the target manager. + */ + virtual solver_factory* translate(ast_manager& m) = 0; }; solver_factory * mk_smt_strategic_solver_factory(symbol const & logic = symbol::null); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 7c4542451..af5442b77 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -390,6 +390,11 @@ public: solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override { return mk_tactic2solver(m, m_tactic.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, logic); } + + solver_factory* translate(ast_manager& m) override { + tactic* translated_tactic = m_tactic->translate(m); + return alloc(tactic2solver_factory, translated_tactic); + } }; class tactic_factory2solver_factory : public solver_factory { @@ -402,6 +407,10 @@ public: tactic * t = (*m_factory)(m, p); return mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic); } + + solver_factory* translate(ast_manager& m) override { + return alloc(tactic_factory2solver_factory, m_factory); + } }; } diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 5257a70b5..ffd6450b3 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -60,6 +60,10 @@ public: auto s = mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic); return s; } + + solver_factory* translate(ast_manager& m) override { + return alloc(smt_nested_solver_factory); + } }; tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) { @@ -185,6 +189,10 @@ public: mk_solver_for_logic(m, p, l), p); } + + solver_factory* translate(ast_manager& m) override { + return alloc(smt_strategic_solver_factory, m_logic); + } }; solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) { From 6df8b39718a6ae53844138439e403cd0c69dafb0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Aug 2025 09:52:58 -0700 Subject: [PATCH 09/28] Update seq_rewriter.cpp --- src/ast/rewriter/seq_rewriter.cpp | 53 +++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 4e8eca949..c5ef8d9ed 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1450,6 +1450,59 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) { result = m_autil.mk_int(0); return BR_DONE; } + + if (str().is_empty(b)) { + result = str().mk_length(a); + return BR_DONE; + } + + expr_ref_vector as(m()), bs(m()); + str().get_concat_units(a, as); + str().get_concat_units(b, bs); + + auto is_suffix = [&](expr_ref_vector const& as, expr_ref_vector const& bs) { + if (as.size() < bs.size()) + return l_undef; + for (unsigned j = 0; j < bs.size(); ++j) { + auto a = as.get(as.size() - j - 1); + auto b = bs.get(bs.size() - j - 1); + if (m().are_equal(a, b)) + continue; + if (m().are_distinct(a, b)) + return l_false; + return l_undef; + } + return l_true; + }; + + switch (compare_lengths(as, bs)) { + case shorter_c: + result = minus_one(); + return BR_DONE; + case same_length_c: + result = m().mk_ite(m().mk_eq(a, b), zero(), minus_one()); + return BR_REWRITE_FULL; + case longer_c: { + unsigned i = as.size(); + while (i >= bs.size()) { + switch (is_suffix(as, bs)) { + case l_undef: + return BR_FAILED; + case l_true: + result = m_autil.mk_sub(str().mk_length(a), m_autil.mk_int(bs.size() - i)); + return BR_REWRITE3; + case l_false: + as.pop_back(); + --i; + break; + } + } + break; + } + default: + break; + } + return BR_FAILED; } From 174d64c4d953e8158c12286376ebaab7d387dce5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Aug 2025 14:43:13 -0700 Subject: [PATCH 10/28] fix releaseNotesSource to inline Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 932fc778e..c4b65c08d 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -471,7 +471,7 @@ stages: tagSource: 'userSpecifiedTag' tag: 'Nightly' title: 'Nightly' - releaseNotesSource: 'input' + releaseNotesSource: 'inline' releaseNotes: 'nightly build' assets: 'tmp/*' assetUploadMode: 'replace' From 1e7832a391d6935aa7356e9e30737ca0a3ae1af0 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 14 Aug 2025 18:13:23 -0700 Subject: [PATCH 11/28] Use solver factory translate method in Z3_solver_translate (#7782) * Initial plan * Fix Z3_solver_translate to use solver factory translate method 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> --- src/api/api_solver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index c9ce1f5cc..05b93d38b 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -276,7 +276,11 @@ extern "C" { LOG_Z3_solver_translate(c, s, target); RESET_ERROR_CODE(); params_ref const& p = to_solver(s)->m_params; - Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), (solver_factory *)nullptr); + solver_factory* translated_factory = nullptr; + if (to_solver(s)->m_solver_factory.get()) { + translated_factory = to_solver(s)->m_solver_factory->translate(mk_c(target)->m()); + } + Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), translated_factory); init_solver(c, s); sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p); mk_c(target)->save_object(sr); From e24a5b66241a0ed8a80bf4913f07e4770cf0549f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Aug 2025 18:16:35 -0700 Subject: [PATCH 12/28] Revert "Parallel solving (#7775)" (#7777) This reverts commit c8e866f5682ed4d01a54ae714ceedf50670f09ca. --- PARALLEL_PROJECT_NOTES.md | 218 ---------- run_local_tests.sh | 32 -- src/math/polynomial/polynomial.cpp | 3 - src/smt/priority_queue.h | 191 --------- src/smt/smt_context.h | 24 -- src/smt/smt_internalizer.cpp | 26 -- src/smt/smt_lookahead.h | 4 +- src/smt/smt_parallel.cpp | 668 ++++++++++------------------- src/smt/smt_parallel.h | 112 +---- 9 files changed, 224 insertions(+), 1054 deletions(-) delete mode 100644 PARALLEL_PROJECT_NOTES.md delete mode 100755 run_local_tests.sh delete mode 100644 src/smt/priority_queue.h diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md deleted file mode 100644 index b60263e4e..000000000 --- a/PARALLEL_PROJECT_NOTES.md +++ /dev/null @@ -1,218 +0,0 @@ -# Parallel project notes - - - -We track notes for updates to -[smt/parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/smt/smt_parallel.cpp) -and possibly -[solver/parallel_tactic.cpp](https://github.com/Z3Prover/z3/blob/master/src/solver/parallel_tactical.cpp). - - - - - -## Variable selection heuristics - - - -* Lookahead solvers: - * lookahead in the smt directory performs a simplistic lookahead search using unit propagation. - * lookahead in the sat directory uses custom lookahead solver based on MARCH. March is described in Handbook of SAT and Knuth volumne 4. - * They both proxy on a cost model where the most useful variable to branch on is the one that _minimizes_ the set of new clauses maximally - through unit propagation. In other words, if a literal _p_ is set to true, and _p_ occurs in clause $\neg p \vee q \vee r$, then it results in - reducing the clause from size 3 to 2 (because $\neg p$ will be false after propagating _p_). - * Selected references: SAT handbook, Knuth Volumne 4, Marijn's March solver on github, [implementation of march in z3](https://github.com/Z3Prover/z3/blob/master/src/sat/sat_lookahead.cpp) -* VSIDS: - * As referenced in Matteo and Antti's solvers. - * Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. - * VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT). - * VSIDS does not keep track of variable phases (if the variable was set to true or false). - * Selected refernces [DAC 2001](https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf) and [Biere Tutorial, slide 64 on Variable Scoring Schemes](https://alexeyignatiev.github.io/ssa-school-2019/slides/ab-satsmtar19-slides.pdf) -* Proof prefix: - * Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score. - * The weight function can be formulated to take into account clause sizes. - * The score assignment may also decay similar to VSIDS. - * We could also use a doubly linked list for literals used in conflicts and keep reinsert literals into the list when they are used. This would be a "Variable move to front" (VMTF) variant. - * Selected references: [Battleman et al](https://www.cs.cmu.edu/~mheule/publications/proofix-SAT25.pdf) -* From local search: - * Note also that local search solvers can be used to assign variable branch priorities. - * We are not going to directly run a local search solver in the mix up front, but let us consider this heuristic for completeness. - * The heuristic is documented in Biere and Cai's journal paper on integrating local search for CDCL. - * Roughly, it considers clauses that move from the UNSAT set to the SAT set of clauses. It then keeps track of the literals involved. - * Selected references: [Cai et al](https://www.jair.org/index.php/jair/article/download/13666/26833/) -* Assignment trails: - * We could also consider the assignments to variables during search. - * Variables that are always assigned to the same truth value could be considered to be safe to assign that truth value. - * The cubes resulting from such variables might be a direction towards finding satisfying solutions. - * Selected references: [Alex and Vadim](https://link.springer.com/chapter/10.1007/978-3-319-94144-8_7) and most recently [Robin et al](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9). - - -## Algorithms - -This section considers various possible algorithms. -In the following, $F$ refers to the original goal, $T$ is the number of CPU cores or CPU threads. - -### Base algorithm - -The existing algorithm in smt_parallel is as follows: - -1. Run a solver on $F$ with a bounded number of conflicts. -2. If the result is SAT/UNSAT, or UNKNOWN with an interrupt or timeout, return. If the maximal number of conflicts were reached continue. -3. Spawn $T$ solvers on $F$ with a bounded number of conflicts, wait until a thread returns UNSAT/SAT or all threads have reached a maximal number of conflicts. -4. Perform a similar check as in 2. -5. Share unit literals learned by each thread. -6. Compute unit cubes for each thread $T$. -7. Spawn $T$ solvers with $F \wedge \ell$, where $\ell$ is a unit literal determined by lookahead function in each thread. -8. Perform a similar check as in 2. But note that a thread can be UNSAT because the unit cube $\ell$ contradicted $F$. In this case learn the unit literal $\neg \ell$. -9. Shared unit literals learned by each thread, increase the maximal number of conflicts, go to 3. - -### Algorithm Variants - -* Instead of using lookahead solving to find unit cubes use the proof-prefix based scoring function. -* Instead of using independent unit cubes, perform a systematic (where systematic can mean many things) cube and conquer strategy. -* Spawn some threads to work in "SAT" mode, tuning to find models instead of short resolution proofs. -* Change the synchronization barrier discipline. -* [Future] Include in-processing - -### Cube and Conquer strategy - -We could maintain a global decomposition of the search space by maintaing a list of _cubes_. -Initially, the list of cubes has just one element, the cube with no literals $[ [] ]$. -By using a list of cubes instead of a _set_ of cubes we can refer to an ordering. -For example, cubes can be ordered by a suffix traversal of the _cube tree_ (the tree formed by -case splitting on the first literal, children of the _true_ branch are the cubes where the first -literal is true, children of the _false_ branch are the cubes where the first literal is false). - -The main question is going to be how the cube decomposition is created. - -#### Static cubing -We can aim for a static cube strategy that uses a few initial (concurrent) probes to find cube literals. -This strategy would be a parallel implementaiton of proof-prefix approach. The computed cubes are inserted -into the list of cubes and the list is consumed by a second round. - -#### Growing cubes on demand -Based on experiences with cubing so far, there is high variance in how easy cubes are to solve. -Some cubes will be harder than others to solve. For hard cubes, it is tempting to develop a recursive -cubing strategy. Ideally, a recursive cubing strategy is symmetric to top-level cubing. - -* The solver would have to identify hard cubes vs. easy cubes. -* It would have to know when to stop working on a hard cube and replace it in the list of cubes by - a new list of sub-cubes. - -* Ideally, we don't need any static cubing and cubing is grown on demand while all threads are utilized. - * If we spawn $T$ threads to initially work with empty cubes, we could extract up to $T$ indepenent cubes - by examining the proof-prefix of their traces. This can form the basis for the first, up to $2^T$ cubes. - * After a round of solving with each thread churning on some cubes, we may obtain more proof-prefixes from - _hard_ cubes. It is not obvious that we want to share cubes from different proof prefixes at this point. - But a starting point is to split a hard cube into two by using the proof-prefix from attempting to solve it. - * Suppose we take the proof-prefix sampling algorithm at heart: It says to start with some initial cube prefix - and then sample for other cube literals. If we translate it to the case where multiple cubes are being processed - in parallel, then an analogy is to share candidates for new cube literals among cubes that are close to each-other. - For example, if thread $t_1$ processes cube $a, b, c$ and $t_2$ processes $a,b, \neg c$. They are close. They are only - separated by Hamming distance 1. If $t_1$ finds cube literal $d$ and $t_2$ finds cube literal $e$, we could consider the cubes - $a, b, c, d, e$, and $a, b, c, d, \neg e$, $\ldots$, $a, b, \neg c, \neg d, \neg e$. - -#### Representing cubes implicitly - -We can represent a list of cubes by using intervals and only represent start and end-points of the intervals. - -#### Batching -Threads can work on more than one cube in a batch. - -### Synchronization - -* The first thread to time out or finish could kill other threads instead of joining on all threads to finish. -* Instead of synchronization barriers have threads continue concurrently without terminating. They synchronize on signals and new units. This is trickier to implement, but in some guises accomplished in [sat/sat_parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/sat/sat_parallel.cpp) - - -## Parameter tuning - -The idea is to have parallel threads try out different parameter settings and search the parameter space of an optimal parameter setting. - -Let us assume that there is a set of tunable parameters $P$. The set comprises of a set of named parameters with initial values. -$P = \{ (p_1, v_1), \ldots, (p_n, v_n) \}$. -With each parameter associate a set of mutation functions $+=, -=, *=$, such as increment, decrement, scale a parameter by a non-negative multiplier (which can be less than 1). -We will initialize a search space of parameter settings by parameters, values and mutation functions that have assigned reward values. The reward value is incremented -if a parameter mutation step results in an improvement, and decremented if a mutation step degrades performance. -$P = \{ (p_1, v_1, \{ (r_{11}, m_{11}), \ldots, (r_{1k_1}, m_{1k_1}) \}), \ldots, (p_n, v_n, \{ (r_{n1}, m_{n1}), \ldots, (r_{nk_n}, m_{nk_n})\}) \}$. -The initial values of reward functions is fixed (to 1) and the initial values of parameters are the defaults. - -* The batch manager maintains a set of candidate parameters $CP = \{ (P_1, r_1), \ldots, (P_n, r_n) \}$. -* A worker thread picks up a parameter $P_i$ from $CP$ from the batch manager. -* It picks one or more parameter settings within $P_i$ whose mutation function have non-zero reward functions and applies a mutation. -* It then runs with a batch of cubes. -* It measures the reward for the new parameter setting based in number of cubes, cube depth, number of timeouts, and completions with number of conflicts. -* If the new reward is an improvement over $(P_i, r_i)$ it inserts the new parameter setting $(P_i', r_i')$ into the batch manager. -* The batch manager discards the worst parameter settings keeping the top $K$ ($K = 5$) parameter settings. - -When picking among mutation steps with reward functions use a weighted sampling algorithm. -Weighted sampling works as follows: You are given a set of items with weights $(i_1, w_1), \ldots, (i_k, w_k)$. -Add $w = \sum_j w_j$. Pick a random number $w_0$ in the range $0\ldots w$. -Then you pick item $i_n$ such that $n$ is the smallest index with $\sum_{j = 1}^n w_j \geq w_0$. - -SMT parameters that could be tuned: - -
-
-  arith.bprop_on_pivoted_rows (bool) (default: true)
-  arith.branch_cut_ratio (unsigned int) (default: 2)
-  arith.eager_eq_axioms (bool) (default: true)
-  arith.enable_hnf (bool) (default: true)
-  arith.greatest_error_pivot (bool) (default: false)
-  arith.int_eq_branch (bool) (default: false)
-  arith.min (bool) (default: false)
-  arith.nl.branching (bool) (default: true)
-  arith.nl.cross_nested (bool) (default: true)
-  arith.nl.delay (unsigned int) (default: 10)
-  arith.nl.expensive_patching (bool) (default: false)
-  arith.nl.expp (bool) (default: false)
-  arith.nl.gr_q (unsigned int) (default: 10)
-  arith.nl.grobner (bool) (default: true)
-  arith.nl.grobner_cnfl_to_report (unsigned int) (default: 1)
-  arith.nl.grobner_eqs_growth (unsigned int) (default: 10)
-  arith.nl.grobner_expr_degree_growth (unsigned int) (default: 2)
-  arith.nl.grobner_expr_size_growth (unsigned int) (default: 2)
-  arith.nl.grobner_frequency (unsigned int) (default: 4)
-  arith.nl.grobner_max_simplified (unsigned int) (default: 10000)
-  arith.nl.grobner_row_length_limit (unsigned int) (default: 10)
-  arith.nl.grobner_subs_fixed (unsigned int) (default: 1)
-  arith.nl.horner (bool) (default: true)
-  arith.nl.horner_frequency (unsigned int) (default: 4)
-  arith.nl.horner_row_length_limit (unsigned int) (default: 10)
-  arith.nl.horner_subs_fixed (unsigned int) (default: 2)
-  arith.nl.nra (bool) (default: true)
-  arith.nl.optimize_bounds (bool) (default: true)
-  arith.nl.order (bool) (default: true)
-  arith.nl.propagate_linear_monomials (bool) (default: true)
-  arith.nl.rounds (unsigned int) (default: 1024)
-  arith.nl.tangents (bool) (default: true)
-  arith.propagate_eqs (bool) (default: true)
-  arith.propagation_mode (unsigned int) (default: 1)
-  arith.random_initial_value (bool) (default: false)
-  arith.rep_freq (unsigned int) (default: 0)
-  arith.simplex_strategy (unsigned int) (default: 0)
-  dack (unsigned int) (default: 1)
-  dack.eq (bool) (default: false)
-  dack.factor (double) (default: 0.1)
-  dack.gc (unsigned int) (default: 2000)
-  dack.gc_inv_decay (double) (default: 0.8)
-  dack.threshold (unsigned int) (default: 10)
-  delay_units (bool) (default: false)
-  delay_units_threshold (unsigned int) (default: 32)
-  dt_lazy_splits (unsigned int) (default: 1)
-  lemma_gc_strategy (unsigned int) (default: 0)
-  phase_caching_off (unsigned int) (default: 100)
-  phase_caching_on (unsigned int) (default: 400)
-  phase_selection (unsigned int) (default: 3)
-  qi.eager_threshold (double) (default: 10.0)
-  qi.lazy_threshold (double) (default: 20.0)
-  qi.quick_checker (unsigned int) (default: 0)
-  relevancy (unsigned int) (default: 2)
-  restart_factor (double) (default: 1.1)
-  restart_strategy (unsigned int) (default: 1)
-  seq.max_unfolding (unsigned int) (default: 1000000000)
-  seq.min_unfolding (unsigned int) (default: 1)
-  seq.split_w_len (bool) (default: true)
-
- - diff --git a/run_local_tests.sh b/run_local_tests.sh deleted file mode 100755 index e9bd45bad..000000000 --- a/run_local_tests.sh +++ /dev/null @@ -1,32 +0,0 @@ -#!/bin/bash -# run from inside ./z3/build - -Z3=./z3 -OPTIONS="-v:0 -st smt.threads=4" -OUT_FILE="../z3_results.txt" -BASE_PATH="../../z3-poly-testing/inputs/" - -# List of relative test files (relative to BASE_PATH) -REL_TEST_FILES=( - "QF_NIA_small/Ton_Chanh_15__Singapore_v1_false-termination.c__p27381_terminationG_0.smt2" - "QF_UFDTLIA_SAT/52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2" -) - -# Clear output file -> "$OUT_FILE" - -# Loop through and run Z3 on each file -for rel_path in "${REL_TEST_FILES[@]}"; do - full_path="$BASE_PATH$rel_path" - test_name="$rel_path" - - echo "Running: $test_name" - echo "===== $test_name =====" | tee -a "$OUT_FILE" - - # Run Z3 and pipe output to both screen and file - $Z3 "$full_path" $OPTIONS 2>&1 | tee -a "$OUT_FILE" - - echo "" | tee -a "$OUT_FILE" -done - -echo "Results written to $OUT_FILE" diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 0ad9639f2..9a0f572dd 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -5153,8 +5153,6 @@ namespace polynomial { // unsigned sz = R->size(); for (unsigned i = 0; i < sz; i++) { - if (sz > 100 && i % 100 == 0) - checkpoint(); monomial * m = R->m(i); numeral const & a = R->a(i); if (m->degree_of(x) == deg_R) { @@ -5573,7 +5571,6 @@ namespace polynomial { h = mk_one(); while (true) { - checkpoint(); TRACE(resultant, tout << "A: " << A << "\nB: " << B << "\n";); degA = degree(A, x); degB = degree(B, x); diff --git a/src/smt/priority_queue.h b/src/smt/priority_queue.h deleted file mode 100644 index 39deab9bb..000000000 --- a/src/smt/priority_queue.h +++ /dev/null @@ -1,191 +0,0 @@ -// SOURCE: https://github.com/Ten0/updatable_priority_queue/blob/master/updatable_priority_queue.h - -#include -#include - -namespace updatable_priority_queue { - template - struct priority_queue_node { - Priority priority; - Key key; - priority_queue_node(const Key& key, const Priority& priority) : priority(priority), key(key) {} - friend bool operator<(const priority_queue_node& pqn1, const priority_queue_node& pqn2) { - return pqn1.priority > pqn2.priority; - } - friend bool operator>(const priority_queue_node& pqn1, const priority_queue_node& pqn2) { - return pqn1.priority < pqn2.priority; - } - }; - - /** Key has to be an uint value (convertible to size_t) - * This is a max heap (max is on top), to match stl's pQ */ - template - class priority_queue { - protected: - std::vector id_to_heappos; - std::vector> heap; - std::size_t max_size = 4; // std::numeric_limits::max(); // Create a variable max_size that defaults to the largest size_t value possible - - public: - // priority_queue() {} - priority_queue(std::size_t max_size = std::numeric_limits::max()): max_size(max_size) {} - - // Returns a const reference to the internal heap storage - const std::vector>& get_heap() const { - return heap; - } - - bool empty() const { return heap.empty(); } - std::size_t size() const { return heap.size(); } - - /** first is priority, second is key */ - const priority_queue_node& top() const { return heap.front(); } - - void pop(bool remember_key=false) { - if(size() == 0) return; - id_to_heappos[heap.front().key] = -1-remember_key; - if(size() > 1) { - *heap.begin() = std::move(*(heap.end()-1)); - id_to_heappos[heap.front().key] = 0; - } - heap.pop_back(); - sift_down(0); - } - - priority_queue_node pop_value(bool remember_key=true) { - if(size() == 0) return priority_queue_node(-1, Priority()); - priority_queue_node ret = std::move(*heap.begin()); - id_to_heappos[ret.key] = -1-remember_key; - if(size() > 1) { - *heap.begin() = std::move(*(heap.end()-1)); - id_to_heappos[heap.front().key] = 0; - } - heap.pop_back(); - sift_down(0); - return ret; - } - - /** Sets the priority for the given key. If not present, it will be added, otherwise it will be updated - * Returns true if the priority was changed. - * */ - bool set(const Key& key, const Priority& priority, bool only_if_higher=false) { - if(key < id_to_heappos.size() && id_to_heappos[key] < ((size_t)-2)) // This key is already in the pQ - return update(key, priority, only_if_higher); - else - return push(key, priority, only_if_higher); - } - - std::pair get_priority(const Key& key) { - if(key < id_to_heappos.size()) { - size_t pos = id_to_heappos[key]; - if(pos < ((size_t)-2)) { - return {true, heap[pos].priority}; - } - } - return {false, 0}; - } - - /** Returns true if the key was not inside and was added, otherwise does nothing and returns false - * If the key was remembered and only_if_unknown is true, does nothing and returns false - * */ - bool push(const Key& key, const Priority& priority, bool only_if_unknown = false) { - extend_ids(key); - if (id_to_heappos[key] < ((size_t)-2)) return false; // already inside - if (only_if_unknown && id_to_heappos[key] == ((size_t)-2)) return false; // was evicted and only_if_unknown prevents re-adding - - if (heap.size() < max_size) { - // We have room: just add new element - size_t n = heap.size(); - id_to_heappos[key] = n; - heap.emplace_back(key, priority); - sift_up(n); - return true; - } else { - // Heap full: heap[0] is the smallest priority in the top-k (min-heap) - if (priority <= heap[0].priority) { - // New element priority too small or equal, discard it - return false; - } - // Evict smallest element at heap[0] - Key evicted_key = heap[0].key; - id_to_heappos[evicted_key] = -2; // Mark evicted - - heap[0] = priority_queue_node(key, priority); - id_to_heappos[key] = 0; - sift_down(0); // restore min-heap property - return true; - } - } - - - - /** Returns true if the key was already inside and was updated, otherwise does nothing and returns false */ - bool update(const Key& key, const Priority& new_priority, bool only_if_higher=false) { - if(key >= id_to_heappos.size()) return false; - size_t heappos = id_to_heappos[key]; - if(heappos >= ((size_t)-2)) return false; - Priority& priority = heap[heappos].priority; - if(new_priority > priority) { - priority = new_priority; - sift_up(heappos); - return true; - } - else if(!only_if_higher && new_priority < priority) { - priority = new_priority; - sift_down(heappos); - return true; - } - return false; - } - - void clear() { - heap.clear(); - id_to_heappos.clear(); - } - - - private: - void extend_ids(Key k) { - size_t new_size = k+1; - if(id_to_heappos.size() < new_size) - id_to_heappos.resize(new_size, -1); - } - - void sift_down(size_t heappos) { - size_t len = heap.size(); - size_t child = heappos*2+1; - if(len < 2 || child >= len) return; - if(child+1 < len && heap[child+1] > heap[child]) ++child; // Check whether second child is higher - if(!(heap[child] > heap[heappos])) return; // Already in heap order - - priority_queue_node val = std::move(heap[heappos]); - do { - heap[heappos] = std::move(heap[child]); - id_to_heappos[heap[heappos].key] = heappos; - heappos = child; - child = 2*child+1; - if(child >= len) break; - if(child+1 < len && heap[child+1] > heap[child]) ++child; - } while(heap[child] > val); - heap[heappos] = std::move(val); - id_to_heappos[heap[heappos].key] = heappos; - } - - void sift_up(size_t heappos) { - size_t len = heap.size(); - if(len < 2 || heappos <= 0) return; - size_t parent = (heappos-1)/2; - if(!(heap[heappos] > heap[parent])) return; - priority_queue_node val = std::move(heap[heappos]); - do { - heap[heappos] = std::move(heap[parent]); - id_to_heappos[heap[heappos].key] = heappos; - heappos = parent; - if(heappos <= 0) break; - parent = (parent-1)/2; - } while(val > heap[parent]); - heap[heappos] = std::move(val); - id_to_heappos[heap[heappos].key] = heappos; - } - }; -} \ No newline at end of file diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 63316a331..2fbc1d705 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -50,8 +50,6 @@ Revision History: #include "model/model.h" #include "solver/progress_callback.h" #include "solver/assertions/asserted_formulas.h" -#include "smt/priority_queue.h" -#include "util/dlist.h" #include // there is a significant space overhead with allocating 1000+ contexts in @@ -191,17 +189,6 @@ namespace smt { unsigned_vector m_lit_occs; //!< occurrence count of literals svector m_bdata; //!< mapping bool_var -> data svector m_activity; - updatable_priority_queue::priority_queue m_pq_scores; - - struct lit_node : dll_base { - literal lit; - lit_node(literal l) : lit(l) { init(this); } - }; - lit_node* m_dll_lits; - - // svector> m_lit_scores; - svector m_lit_scores[2]; - clause_vector m_aux_clauses; clause_vector m_lemmas; vector m_clauses_to_reinit; @@ -946,17 +933,6 @@ namespace smt { ast_pp_util m_lemma_visitor; void dump_lemma(unsigned n, literal const* lits); void dump_axiom(unsigned n, literal const* lits); - void add_scores(unsigned n, literal const* lits); - void reset_scores() { - for (auto& e : m_lit_scores[0]) - e = 0; - for (auto& e : m_lit_scores[1]) - e = 0; - m_pq_scores.clear(); // Clear the priority queue heap as well - } - double get_score(literal l) const { - return m_lit_scores[l.sign()][l.var()]; - } public: void ensure_internalized(expr* e); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index c7e257fac..9aa6d68f4 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -931,10 +931,6 @@ namespace smt { set_bool_var(id, v); m_bdata.reserve(v+1); m_activity.reserve(v+1); - m_lit_scores[0].reserve(v + 1); - m_lit_scores[1].reserve(v + 1); - - m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0; m_bool_var2expr.reserve(v+1); m_bool_var2expr[v] = n; literal l(v, false); @@ -1423,7 +1419,6 @@ namespace smt { break; case CLS_LEARNED: dump_lemma(num_lits, lits); - add_scores(num_lits, lits); break; default: break; @@ -1532,27 +1527,6 @@ namespace smt { }} } - // void context::add_scores(unsigned n, literal const* lits) { - // for (unsigned i = 0; i < n; ++i) { - // auto lit = lits[i]; - // unsigned v = lit.var(); - // m_lit_scores[v][lit.sign()] += 1.0 / n; - // } - // } - - void context::add_scores(unsigned n, literal const* lits) { - for (unsigned i = 0; i < n; ++i) { - auto lit = lits[i]; - unsigned v = lit.var(); // unique key per literal - - m_lit_scores[lit.sign()][v] += 1.0 / n; - - auto new_score = m_lit_scores[0][v] * m_lit_scores[1][v]; - m_pq_scores.set(v, new_score); - - } - } - void context::dump_axiom(unsigned n, literal const* lits) { if (m_fparams.m_axioms2files) { literal_buffer tmp; diff --git a/src/smt/smt_lookahead.h b/src/smt/smt_lookahead.h index d53af58e4..5deccad2c 100644 --- a/src/smt/smt_lookahead.h +++ b/src/smt/smt_lookahead.h @@ -30,13 +30,11 @@ namespace smt { struct compare; - // double get_score(); + double get_score(); void choose_rec(expr_ref_vector& trail, expr_ref_vector& result, unsigned depth, unsigned budget); public: - double get_score(); - lookahead(context& ctx); expr_ref choose(unsigned budget = 2000); diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index d08a7c045..4941e4df9 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -36,463 +36,237 @@ namespace smt { #else #include -#include namespace smt { - - void parallel::worker::run() { - ast_translation g2l(p.ctx.m, m); // global to local context -- MUST USE p.ctx.m, not ctx->m, AS GLOBAL MANAGER!!! - ast_translation l2g(m, p.ctx.m); // local to global context - while (m.inc()) { // inc: increase the limit and check if it is canceled, vs m.limit().is_canceled() is readonly. the .limit() is also not necessary (m.inc() etc provides a convenience wrapper) - vector cubes; - b.get_cubes(g2l, cubes); - if (cubes.empty()) - return; - collect_shared_clauses(g2l); - for (auto& cube : cubes) { - if (!m.inc()) { - b.set_exception("context cancelled"); - return; - } - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n"); - lbool r = check_cube(cube); - if (m.limit().is_canceled()) { - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " context cancelled\n"); - return; - } - switch (r) { - case l_undef: { - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found undef cube\n"); - // return unprocessed cubes to the batch manager - // add a split literal to the batch manager. - // optionally process other cubes and delay sending back unprocessed cubes to batch manager. - vector returned_cubes; - returned_cubes.push_back(cube); - auto split_atoms = get_split_atoms(); - b.return_cubes(l2g, returned_cubes, split_atoms); - update_max_thread_conflicts(); - break; - } - case l_true: { - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found sat cube\n"); - model_ref mdl; - ctx->get_model(mdl); - b.set_sat(l2g, *mdl); - return; - } - case l_false: { - // if unsat core only contains (external) assumptions (i.e. all the unsat core are asms), then unsat and return as this does NOT depend on cubes - // otherwise, extract lemmas that can be shared (units (and unsat core?)). - // share with batch manager. - // process next cube. - expr_ref_vector const& unsat_core = ctx->unsat_core(); - IF_VERBOSE(1, verbose_stream() << "unsat core: " << unsat_core << "\n"); - // If the unsat core only contains assumptions, - // unsatisfiability does not depend on the current cube and the entire problem is unsat. - if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " determined formula unsat\n"); - b.set_unsat(l2g, unsat_core); - return; - } - for (expr* e : unsat_core) - if (asms.contains(e)) - b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core - - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found unsat cube\n"); - b.collect_clause(l2g, id, mk_not(mk_and(unsat_core))); - break; - } - } - } - share_units(l2g); - } - } - - parallel::worker::worker(unsigned id, parallel& p, expr_ref_vector const& _asms): id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m) { - ast_translation g2l(p.ctx.m, m); - for (auto e : _asms) - asms.push_back(g2l(e)); - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " created with " << asms.size() << " assumptions\n"); - m_smt_params.m_preprocess = false; - ctx = alloc(context, m, m_smt_params, p.ctx.get_params()); - context::copy(p.ctx, *ctx, true); - ctx->set_random_seed(id + m_smt_params.m_random_seed); - - m_max_thread_conflicts = ctx->get_fparams().m_threads_max_conflicts; - m_max_conflicts = ctx->get_fparams().m_max_conflicts; - } - - void parallel::worker::share_units(ast_translation& l2g) { - // Collect new units learned locally by this worker and send to batch manager - unsigned sz = ctx->assigned_literals().size(); - for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync - literal lit = ctx->assigned_literals()[j]; - expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression - if (lit.sign()) - e = m.mk_not(e); // negate if literal is negative - b.collect_clause(l2g, id, e); - } - m_num_shared_units = sz; - } - - void parallel::batch_manager::collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause) { - std::scoped_lock lock(mux); - expr* g_clause = l2g(clause); - if (!shared_clause_set.contains(g_clause)) { - shared_clause_set.insert(g_clause); - shared_clause sc{source_worker_id, expr_ref(g_clause, m)}; - shared_clause_trail.push_back(sc); - } - } - - void parallel::worker::collect_shared_clauses(ast_translation& g2l) { - expr_ref_vector new_clauses = b.return_shared_clauses(g2l, m_shared_clause_limit, id); // get new clauses from the batch manager - // iterate over new clauses and assert them in the local context - for (expr* e : new_clauses) { - expr_ref local_clause(e, g2l.to()); // e was already translated to the local context in the batch manager!! - ctx->assert_expr(local_clause); // assert the clause in the local context - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n"); - } - } - - // get new clauses from the batch manager and assert them in the local context - expr_ref_vector parallel::batch_manager::return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id) { - std::scoped_lock lock(mux); - expr_ref_vector result(g2l.to()); - for (unsigned i = worker_limit; i < shared_clause_trail.size(); ++i) { - if (shared_clause_trail[i].source_worker_id == worker_id) - continue; // skip clauses from the requesting worker - result.push_back(g2l(shared_clause_trail[i].clause.get())); - } - worker_limit = shared_clause_trail.size(); // update the worker limit to the end of the current trail - return result; - } - - lbool parallel::worker::check_cube(expr_ref_vector const& cube) { - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " checking cube\n";); - for (auto& atom : cube) - asms.push_back(atom); - lbool r = l_undef; - - ctx->get_fparams().m_max_conflicts = std::min(m_max_thread_conflicts, m_max_conflicts); - try { - r = ctx->check(asms.size(), asms.data()); - } - catch (z3_error& err) { - b.set_exception(err.error_code()); - } - catch (z3_exception& ex) { - b.set_exception(ex.what()); - } - catch (...) { - b.set_exception("unknown exception"); - } - asms.shrink(asms.size() - cube.size()); - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " DONE checking cube " << r << "\n";); - return r; - } - - void parallel::batch_manager::get_cubes(ast_translation& g2l, vector& cubes) { - std::scoped_lock lock(mux); - if (m_cubes.size() == 1 && m_cubes[0].size() == 0) { - // special initialization: the first cube is emtpy, have the worker work on an empty cube. - cubes.push_back(expr_ref_vector(g2l.to())); - return; - } - - for (unsigned i = 0; i < std::min(m_max_batch_size / p.num_threads, (unsigned)m_cubes.size()) && !m_cubes.empty(); ++i) { - auto& cube = m_cubes.back(); - expr_ref_vector l_cube(g2l.to()); - for (auto& e : cube) { - l_cube.push_back(g2l(e)); - } - cubes.push_back(l_cube); - m_cubes.pop_back(); - } - } - - void parallel::batch_manager::set_sat(ast_translation& l2g, model& m) { - std::scoped_lock lock(mux); - if (m_state != state::is_running) - return; - m_state = state::is_sat; - p.ctx.set_model(m.translate(l2g)); - cancel_workers(); - } - - void parallel::batch_manager::set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core) { - std::scoped_lock lock(mux); - if (m_state != state::is_running) - return; - m_state = state::is_unsat; - - // every time we do a check_sat call, don't want to have old info coming from a prev check_sat call - // the unsat core gets reset internally in the context after each check_sat, so we assert this property here - // takeaway: each call to check_sat needs to have a fresh unsat core - SASSERT(p.ctx.m_unsat_core.empty()); - for (expr* e : unsat_core) - p.ctx.m_unsat_core.push_back(l2g(e)); - cancel_workers(); - } - - void parallel::batch_manager::set_exception(unsigned error_code) { - std::scoped_lock lock(mux); - if (m_state != state::is_running) - return; - m_state = state::is_exception_code; - m_exception_code = error_code; - cancel_workers(); - } - - void parallel::batch_manager::set_exception(std::string const& msg) { - std::scoped_lock lock(mux); - if (m_state != state::is_running || m.limit().is_canceled()) - return; - m_state = state::is_exception_msg; - m_exception_msg = msg; - cancel_workers(); - } - - void parallel::batch_manager::report_assumption_used(ast_translation& l2g, expr* assumption) { - std::scoped_lock lock(mux); - p.m_assumptions_used.insert(l2g(assumption)); - } - - lbool parallel::batch_manager::get_result() const { - if (m.limit().is_canceled()) - return l_undef; // the main context was cancelled, so we return undef. - switch (m_state) { - case state::is_running: // batch manager is still running, but all threads have processed their cubes, which means all cubes were unsat - if (!m_cubes.empty()) - throw default_exception("inconsistent end state"); - if (!p.m_assumptions_used.empty()) { - // collect unsat core from assumptions used, if any --> case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core - SASSERT(p.ctx.m_unsat_core.empty()); - for (auto a : p.m_assumptions_used) - p.ctx.m_unsat_core.push_back(a); - } - return l_false; - case state::is_unsat: - return l_false; - case state::is_sat: - return l_true; - case state::is_exception_msg: - throw default_exception(m_exception_msg.c_str()); - case state::is_exception_code: - throw z3_error(m_exception_code); - default: - UNREACHABLE(); - return l_undef; - } - } - - /* - Batch manager maintains C_batch, A_batch. - C_batch - set of cubes - A_batch - set of split atoms. - return_cubes is called with C_batch A_batch C A. - C_worker - one or more cubes - A_worker - split atoms form the worker thread. - Assumption: A_worker does not occur in C_worker. - - ------------------------------------------------------------------------------------------------------------------------------------------------------------ - Greedy strategy: - For each returned cube c from the worker, you split it on all split atoms not in it (i.e., A_batch \ atoms(c)), plus any new atoms from A_worker. - For each existing cube in the batch, you also split it on the new atoms from A_worker. - - return_cubes C_batch A_batch C_worker A_worker: - C_batch <- { cube * 2^(A_worker u (A_batch \ atoms(cube)) | cube in C_worker } u - { cube * 2^(A_worker \ A_batch) | cube in C_batch } - = - let C_batch' = C_batch u { cube * 2^(A_batch \ atoms(cube)) | cube in C_worker } - in { cube * 2^(A_worker \ A_batch) | cube in C_batch' } - A_batch <- A_batch u A_worker - - ------------------------------------------------------------------------------------------------------------------------------------------------------------ - Frugal strategy: only split on worker cubes - - case 1: thread returns no cubes, just atoms: just create 2^k cubes from all combinations of atoms so far. - return_cubes C_batch A_batch [[]] A_worker: - C_batch <- C_batch u 2^(A_worker u A_batch), - A_batch <- A_batch u A_worker - - case 2: thread returns both cubes and atoms - Only the returned cubes get split by the newly discovered atoms (A_worker). Existing cubes are not touched. - return_cubes C_batch A_batch C_worker A_worker: - C_batch <- C_batch u { cube * 2^A_worker | cube in C_worker }. - A_batch <- A_batch u A_worker - - This means: - Only the returned cubes get split by the newly discovered atoms (A_worker). - Existing cubes are not touched. - - ------------------------------------------------------------------------------------------------------------------------------------------------------------ - Hybrid: Between Frugal and Greedy: (generalizes the first case of empty cube returned by worker) -- don't focus on this approach - i.e. Expand only the returned cubes, but allow them to be split on both new and old atoms not already in them. - - C_batch <- C_batch u { cube * 2^(A_worker u (A_batch \ atoms(cube)) | cube in C_worker } - A_batch <- A_batch u A_worker - - ------------------------------------------------------------------------------------------------------------------------------------------------------------ - Final thought (do this!): use greedy strategy by a policy when C_batch, A_batch, A_worker are "small". -- want to do this. switch to frugal strategy after reaching size limit - */ - - // currenly, the code just implements the greedy strategy - void parallel::batch_manager::return_cubes(ast_translation& l2g, vectorconst& C_worker, expr_ref_vector const& A_worker) { - auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) { - return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); }); - }; - - auto add_split_atom = [&](expr* atom, unsigned start) { - unsigned stop = m_cubes.size(); - for (unsigned i = start; i < stop; ++i) { - m_cubes.push_back(m_cubes[i]); - m_cubes.back().push_back(m.mk_not(atom)); - m_cubes[i].push_back(atom); - } - }; - - std::scoped_lock lock(mux); - unsigned max_cubes = 1000; - bool greedy_mode = (m_cubes.size() <= max_cubes); - unsigned a_worker_start_idx = 0; - - // - // --- Phase 1: Greedy split of *existing* cubes on new A_worker atoms (greedy) --- - // - if (greedy_mode) { - for (; a_worker_start_idx < A_worker.size(); ++a_worker_start_idx) { - expr_ref g_atom(l2g(A_worker[a_worker_start_idx]), l2g.to()); - if (m_split_atoms.contains(g_atom)) - continue; - m_split_atoms.push_back(g_atom); - - add_split_atom(g_atom, 0); // split all *existing* cubes - if (m_cubes.size() > max_cubes) { - greedy_mode = false; - ++a_worker_start_idx; // start frugal from here - break; - } - } - } - - unsigned initial_m_cubes_size = m_cubes.size(); // where to start processing the worker cubes after splitting the EXISTING cubes on the new worker atoms - - // --- Phase 2: Process worker cubes (greedy) --- - for (auto& c : C_worker) { - expr_ref_vector g_cube(l2g.to()); - for (auto& atom : c) - g_cube.push_back(l2g(atom)); - - unsigned start = m_cubes.size(); // update start after adding each cube so we only process the current cube being added - m_cubes.push_back(g_cube); - - if (greedy_mode) { - // Split new cube on all existing m_split_atoms not in it - for (auto g_atom : m_split_atoms) { - if (!atom_in_cube(g_cube, g_atom)) { - add_split_atom(g_atom, start); - if (m_cubes.size() > max_cubes) { - greedy_mode = false; - break; - } - } - } - } - } - - // --- Phase 3: Frugal fallback: only process NEW worker cubes with NEW atoms --- - if (!greedy_mode) { - for (unsigned i = a_worker_start_idx; i < A_worker.size(); ++i) { - expr_ref g_atom(l2g(A_worker[i]), l2g.to()); - if (!m_split_atoms.contains(g_atom)) - m_split_atoms.push_back(g_atom); - add_split_atom(g_atom, initial_m_cubes_size); - } - } - } - - expr_ref_vector parallel::worker::get_split_atoms() { - unsigned k = 2; - - auto candidates = ctx->m_pq_scores.get_heap(); - - std::sort(candidates.begin(), candidates.end(), - [](const auto& a, const auto& b) { return a.priority > b.priority; }); - - expr_ref_vector top_lits(m); - for (const auto& node: candidates) { - if (ctx->get_assignment(node.key) != l_undef) - continue; - - expr* e = ctx->bool_var2expr(node.key); - if (!e) - continue; - - top_lits.push_back(expr_ref(e, m)); - if (top_lits.size() >= k) - break; - } - IF_VERBOSE(1, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_pq_scores.size() << " num vars " << ctx->get_num_bool_vars() << "\n"); - return top_lits; - } - - void parallel::batch_manager::initialize() { - m_state = state::is_running; - m_cubes.reset(); - m_cubes.push_back(expr_ref_vector(m)); // push empty cube - m_split_atoms.reset(); - } - lbool parallel::operator()(expr_ref_vector const& asms) { - ast_manager& m = ctx.m; + lbool result = l_undef; + unsigned num_threads = std::min((unsigned) std::thread::hardware_concurrency(), ctx.get_fparams().m_threads); + flet _nt(ctx.m_fparams.m_threads, 1); + unsigned thread_max_conflicts = ctx.get_fparams().m_threads_max_conflicts; + unsigned max_conflicts = ctx.get_fparams().m_max_conflicts; + + // try first sequential with a low conflict budget to make super easy problems cheap + unsigned max_c = std::min(thread_max_conflicts, 40u); + flet _mc(ctx.get_fparams().m_max_conflicts, max_c); + result = ctx.check(asms.size(), asms.data()); + if (result != l_undef || ctx.m_num_conflicts < max_c) { + return result; + } + + enum par_exception_kind { + DEFAULT_EX, + ERROR_EX + }; + + vector smt_params; + scoped_ptr_vector pms; + scoped_ptr_vector pctxs; + vector pasms; + + ast_manager& m = ctx.m; + scoped_limits sl(m.limit()); + unsigned finished_id = UINT_MAX; + std::string ex_msg; + par_exception_kind ex_kind = DEFAULT_EX; + unsigned error_code = 0; + bool done = false; + unsigned num_rounds = 0; if (m.has_trace_stream()) throw default_exception("trace streams have to be off in parallel mode"); + - struct scoped_clear_table { - obj_hashtable& ht; - scoped_clear_table(obj_hashtable& ht) : ht(ht) {} // Constructor: Takes a reference to a hash table when the object is created and saves it. - ~scoped_clear_table() { ht.reset(); } // Destructor: When the scoped_clear_table object goes out of scope, it automatically calls reset() on that hash table, clearing it - }; - scoped_clear_table clear(m_assumptions_used); // creates a scoped_clear_table named clear, bound to m_assumptions_used - - { - m_batch_manager.initialize(); - m_workers.reset(); - scoped_limits sl(m.limit()); - flet _nt(ctx.m_fparams.m_threads, 1); - SASSERT(num_threads > 1); - for (unsigned i = 0; i < num_threads; ++i) - m_workers.push_back(alloc(worker, i, *this, asms)); // i.e. "new worker(i, *this, asms)" - - // THIS WILL ALLOW YOU TO CANCEL ALL THE CHILD THREADS - // within the lexical scope of the code block, creates a data structure that allows you to push children - // objects to the limit object, so if someone cancels the parent object, the cancellation propagates to the children - // and that cancellation has the lifetime of the scope - // even if this code doesn't expliclty kill the main thread, still applies bc if you e.g. Ctrl+C the main thread, the children threads need to be cancelled - for (auto w : m_workers) - sl.push_child(&(w->limit())); - - // Launch threads - vector threads(num_threads); - for (unsigned i = 0; i < num_threads; ++i) { - threads[i] = std::thread([&, i]() { - m_workers[i]->run(); - }); - } - - // Wait for all threads to finish - for (auto& th : threads) - th.join(); - - for (auto w : m_workers) - w->collect_statistics(ctx.m_aux_stats); + params_ref params = ctx.get_params(); + for (unsigned i = 0; i < num_threads; ++i) { + smt_params.push_back(ctx.get_fparams()); + smt_params.back().m_preprocess = false; + } + + for (unsigned i = 0; i < num_threads; ++i) { + ast_manager* new_m = alloc(ast_manager, m, true); + pms.push_back(new_m); + pctxs.push_back(alloc(context, *new_m, smt_params[i], params)); + context& new_ctx = *pctxs.back(); + context::copy(ctx, new_ctx, true); + new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed); + ast_translation tr(m, *new_m); + pasms.push_back(tr(asms)); + sl.push_child(&(new_m->limit())); } - m_workers.clear(); - return m_batch_manager.get_result(); // i.e. all threads have finished all of their cubes -- so if state::is_running is still true, means the entire formula is unsat (otherwise a thread would have returned l_undef) + auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) { + lookahead lh(ctx); + c = lh.choose(); + if (c) { + if ((ctx.get_random_value() % 2) == 0) + c = c.get_manager().mk_not(c); + lasms.push_back(c); + } + }; + + obj_hashtable unit_set; + expr_ref_vector unit_trail(ctx.m); + unsigned_vector unit_lim; + for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0); + + std::function collect_units = [&,this]() { + //return; -- has overhead + for (unsigned i = 0; i < num_threads; ++i) { + context& pctx = *pctxs[i]; + pctx.pop_to_base_lvl(); + ast_translation tr(pctx.m, ctx.m); + unsigned sz = pctx.assigned_literals().size(); + for (unsigned j = unit_lim[i]; j < sz; ++j) { + literal lit = pctx.assigned_literals()[j]; + //IF_VERBOSE(0, verbose_stream() << "(smt.thread " << i << " :unit " << lit << " " << pctx.is_relevant(lit.var()) << ")\n";); + if (!pctx.is_relevant(lit.var())) + continue; + expr_ref e(pctx.bool_var2expr(lit.var()), pctx.m); + if (lit.sign()) e = pctx.m.mk_not(e); + expr_ref ce(tr(e.get()), ctx.m); + if (!unit_set.contains(ce)) { + unit_set.insert(ce); + unit_trail.push_back(ce); + } + } + } + + unsigned sz = unit_trail.size(); + for (unsigned i = 0; i < num_threads; ++i) { + context& pctx = *pctxs[i]; + ast_translation tr(ctx.m, pctx.m); + for (unsigned j = unit_lim[i]; j < sz; ++j) { + expr_ref src(ctx.m), dst(pctx.m); + dst = tr(unit_trail.get(j)); + pctx.assert_expr(dst); + } + unit_lim[i] = pctx.assigned_literals().size(); + } + IF_VERBOSE(1, verbose_stream() << "(smt.thread :units " << sz << ")\n"); + }; + + std::mutex mux; + + auto worker_thread = [&](int i) { + try { + context& pctx = *pctxs[i]; + ast_manager& pm = *pms[i]; + expr_ref_vector lasms(pasms[i]); + expr_ref c(pm); + + pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts); + if (num_rounds > 0 && (num_rounds % pctx.get_fparams().m_threads_cube_frequency) == 0) + cube(pctx, lasms, c); + IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; + if (num_rounds > 0) verbose_stream() << " :round " << num_rounds; + if (c) verbose_stream() << " :cube " << mk_bounded_pp(c, pm, 3); + verbose_stream() << ")\n";); + lbool r = pctx.check(lasms.size(), lasms.data()); + + if (r == l_undef && pctx.m_num_conflicts >= max_conflicts) + ; // no-op + else if (r == l_undef && pctx.m_num_conflicts >= thread_max_conflicts) + return; + else if (r == l_false && pctx.unsat_core().contains(c)) { + IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i << " :learn " << mk_bounded_pp(c, pm, 3) << ")"); + pctx.assert_expr(mk_not(mk_and(pctx.unsat_core()))); + return; + } + + + bool first = false; + { + std::lock_guard lock(mux); + if (finished_id == UINT_MAX) { + finished_id = i; + first = true; + result = r; + done = true; + } + if (!first && r != l_undef && result == l_undef) { + finished_id = i; + result = r; + } + else if (!first) return; + } + + for (ast_manager* m : pms) { + if (m != &pm) m->limit().cancel(); + } + + } + catch (z3_error & err) { + if (finished_id == UINT_MAX) { + error_code = err.error_code(); + ex_kind = ERROR_EX; + done = true; + } + } + catch (z3_exception & ex) { + if (finished_id == UINT_MAX) { + ex_msg = ex.what(); + ex_kind = DEFAULT_EX; + done = true; + } + } + catch (...) { + if (finished_id == UINT_MAX) { + ex_msg = "unknown exception"; + ex_kind = ERROR_EX; + done = true; + } + } + }; + + // for debugging: num_threads = 1; + + while (true) { + vector threads(num_threads); + for (unsigned i = 0; i < num_threads; ++i) { + threads[i] = std::thread([&, i]() { worker_thread(i); }); + } + for (auto & th : threads) { + th.join(); + } + if (done) break; + + collect_units(); + ++num_rounds; + max_conflicts = (max_conflicts < thread_max_conflicts) ? 0 : (max_conflicts - thread_max_conflicts); + thread_max_conflicts *= 2; + } + + for (context* c : pctxs) { + c->collect_statistics(ctx.m_aux_stats); + } + + if (finished_id == UINT_MAX) { + switch (ex_kind) { + case ERROR_EX: throw z3_error(error_code); + default: throw default_exception(std::move(ex_msg)); + } + } + + model_ref mdl; + context& pctx = *pctxs[finished_id]; + ast_translation tr(*pms[finished_id], m); + switch (result) { + case l_true: + pctx.get_model(mdl); + if (mdl) + ctx.set_model(mdl->translate(tr)); + break; + case l_false: + ctx.m_unsat_core.reset(); + for (expr* e : pctx.unsat_core()) + ctx.m_unsat_core.push_back(tr(e)); + break; + default: + break; + } + + return result; } } diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index b337d5e45..07b04019d 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -19,124 +19,16 @@ Revision History: #pragma once #include "smt/smt_context.h" -#include namespace smt { class parallel { context& ctx; - unsigned num_threads; - - struct shared_clause { - unsigned source_worker_id; - expr_ref clause; - }; - - class batch_manager { - enum state { - is_running, - is_sat, - is_unsat, - is_exception_msg, - is_exception_code - }; - - ast_manager& m; - parallel& p; - std::mutex mux; - state m_state = state::is_running; - expr_ref_vector m_split_atoms; // atoms to split on - vector m_cubes; - unsigned m_max_batch_size = 10; - unsigned m_exception_code = 0; - std::string m_exception_msg; - vector shared_clause_trail; // store all shared clauses with worker IDs - obj_hashtable shared_clause_set; // for duplicate filtering on per-thread clause expressions - - // called from batch manager to cancel other workers if we've reached a verdict - void cancel_workers() { - IF_VERBOSE(1, verbose_stream() << "Canceling workers\n"); - for (auto& w : p.m_workers) - w->cancel(); - } - - public: - batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_split_atoms(m) { } - - void initialize(); - - void set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core); - void set_sat(ast_translation& l2g, model& m); - void set_exception(std::string const& msg); - void set_exception(unsigned error_code); - - // - // worker threads ask the batch manager for a supply of cubes to check. - // they pass in a translation function from the global context to local context (ast-manager). It is called g2l. - // The batch manager returns a list of cubes to solve. - // - void get_cubes(ast_translation& g2l, vector& cubes); - - // - // worker threads return unprocessed cubes to the batch manager together with split literal candidates. - // the batch manager re-enqueues unprocessed cubes and optionally splits them using the split_atoms returned by this and workers. - // - void return_cubes(ast_translation& l2g, vectorconst& cubes, expr_ref_vector const& split_atoms); - void report_assumption_used(ast_translation& l2g, expr* assumption); - void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* e); - expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id); - lbool get_result() const; - }; - - class worker { - unsigned id; // unique identifier for the worker - parallel& p; - batch_manager& b; - ast_manager m; - expr_ref_vector asms; - smt_params m_smt_params; - scoped_ptr ctx; - unsigned m_max_conflicts = 800; // the global budget for all work this worker can do across cubes in the current run. - unsigned m_max_thread_conflicts = 100; // the per-cube limit for how many conflicts the worker can spend on a single cube before timing out on it and moving on - unsigned m_num_shared_units = 0; - unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share - void share_units(ast_translation& l2g); - lbool check_cube(expr_ref_vector const& cube); - void update_max_thread_conflicts() { - m_max_thread_conflicts *= 2; - } // allow for backoff scheme of conflicts within the thread for cube timeouts. - public: - worker(unsigned id, parallel& p, expr_ref_vector const& _asms); - void run(); - expr_ref_vector get_split_atoms(); - void collect_shared_clauses(ast_translation& g2l); - - void cancel() { - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " canceling\n"); - m.limit().cancel(); - } - void collect_statistics(::statistics& st) const { - IF_VERBOSE(1, verbose_stream() << "Collecting statistics for worker " << id << "\n"); - ctx->collect_statistics(st); - } - reslimit& limit() { - return m.limit(); - } - }; - - obj_hashtable m_assumptions_used; // assumptions used in unsat cores, to be used in final core - batch_manager m_batch_manager; - ptr_vector m_workers; - public: - parallel(context& ctx) : - ctx(ctx), - num_threads(std::min( - (unsigned)std::thread::hardware_concurrency(), - ctx.get_fparams().m_threads)), - m_batch_manager(ctx.m, *this) {} + parallel(context& ctx): ctx(ctx) {} lbool operator()(expr_ref_vector const& asms); + }; } From 7422d819a3fec495dc8f41a33c4b6d6e221a0d37 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Aug 2025 09:49:47 -0700 Subject: [PATCH 13/28] remove upload artifact for azure-pipeline Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 9 --------- 1 file changed, 9 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 180ad7437..6368afdb4 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -56,15 +56,6 @@ jobs: - script: "pip install build git+https://github.com/rhelmot/auditwheel" - script: "cd src/api/python && python -m build && AUDITWHEEL_PLAT= auditwheel repair --best-plat dist/*.whl && cd ../../.." - script: "pip install ./src/api/python/wheelhouse/*.whl && python - Date: Fri, 15 Aug 2025 09:50:45 -0700 Subject: [PATCH 14/28] Fix compilation warning: add missing is_passive_eq case to switch statement (#7785) * Initial plan * Fix compilation warning: add missing is_passive_eq case to switch statement 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> --- src/ast/euf/euf_ac_plugin.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp index ce0134439..e89f18d58 100644 --- a/src/ast/euf/euf_ac_plugin.cpp +++ b/src/ast/euf/euf_ac_plugin.cpp @@ -686,6 +686,7 @@ namespace euf { case eq_status::is_processed_eq: case eq_status::is_reducing_eq: case eq_status::is_dead_eq: + case eq_status::is_passive_eq: m_to_simplify_todo.remove(id); break; case eq_status::is_to_simplify_eq: From 7b8482a093a6202cc0ec1be5d387c7450d560ffd Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Fri, 15 Aug 2025 09:51:25 -0700 Subject: [PATCH 15/28] Remove NugetPublishNightly stage from nightly.yaml (#7787) * Initial plan * Remove NugetPublishNightly stage from nightly.yaml 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> --- scripts/nightly.yaml | 39 +-------------------------------------- 1 file changed, 1 insertion(+), 38 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index c4b65c08d..93a7baa77 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -478,42 +478,5 @@ stages: isDraft: false isPreRelease: true -- stage: NugetPublishNightly - jobs: - # Publish to nightly feed on Azure - - job: NuGetPublishNightly - displayName: "Push nuget packages to Azure Feed" - steps: - - task: NuGetAuthenticate@0 - displayName: 'NuGet Authenticate' - - task: NuGetToolInstaller@0 - inputs: - versionSpec: 5.x - checkLatest: false - - task: DownloadPipelineArtifact@2 - displayName: 'Download NuGet x86 Package' - inputs: - artifact: 'NuGet32' - path: $(Agent.TempDirectory)/x86 - - task: DownloadPipelineArtifact@2 - displayName: 'Download NuGet x64 Package' - inputs: - artifact: 'NuGet' - path: $(Agent.TempDirectory)/x64 - - task: NuGetCommand@2 - displayName: 'NuGet Nightly x64 push' - inputs: - command: push - publishVstsFeed: 'Z3Build/Z3-Nightly-Builds' - packagesToPush: $(Agent.TempDirectory)/x64/*.nupkg - allowPackageConflicts: true - - task: NuGetCommand@2 - displayName: 'NuGet Nightly x86 push' - inputs: - command: push - publishVstsFeed: 'Z3Build/Z3-Nightly-Builds' - packagesToPush: $(Agent.TempDirectory)/x86/*.nupkg - allowPackageConflicts: true - - + # TBD: run regression tests on generated binaries. From a121e6c6e95c60f50d1561f03762805dabc969e1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Aug 2025 16:09:26 -0700 Subject: [PATCH 16/28] enable pypi public Signed-off-by: Nikolaj Bjorner --- scripts/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index 946b002f3..0aaef56da 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -492,7 +492,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(0,1) + condition: eq(1,1) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From d8bf0e047faa35a4196b66f6671522a4d843a602 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 17 Aug 2025 10:25:51 -0700 Subject: [PATCH 17/28] Fix nullptr dereference in pp_symbol when handling null symbol names (#7790) * Initial plan * Fix nullptr dereference in pp_symbol with null symbol names 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> --- src/model/model_smt2_pp.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp index 489209851..f26b67797 100644 --- a/src/model/model_smt2_pp.cpp +++ b/src/model/model_smt2_pp.cpp @@ -42,8 +42,13 @@ static unsigned pp_symbol(std::ostream & out, symbol const & s) { return static_cast(str.length()); } else { - out << s.bare_str(); - return static_cast(strlen(s.bare_str())); + if (s.is_null()) { + out << "null"; + return 4; // length of "null" + } else { + out << s.bare_str(); + return static_cast(strlen(s.bare_str())); + } } } From c75b8ec752c89abf6f726d2a9567efa45bee6204 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 16:47:23 -0700 Subject: [PATCH 18/28] add option to control epsilon #7791 #7791 reports on using model values during lex optimization that break soft constraints. This is an artifact of using optimization where optimal values can be arbitrarily close to a rational. In a way it is by design, but we give the user now an option to control the starting point for epsilon when converting infinitesimals into rationals. --- src/math/lp/lar_solver.cpp | 6 +++--- src/math/lp/lp_settings.cpp | 2 ++ src/math/lp/lp_settings.h | 1 + src/params/smt_params_helper.pyg | 1 + src/params/theory_arith_params.cpp | 3 +++ src/params/theory_arith_params.h | 2 ++ src/smt/theory_arith_core.h | 3 ++- 7 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 5fbde7f42..e65e0a80a 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1523,7 +1523,7 @@ namespace lp { if (!m_imp->m_columns_with_changed_bounds.empty()) return false; - m_imp->m_delta = get_core_solver().find_delta_for_strict_bounds(mpq(1)); + m_imp->m_delta = get_core_solver().find_delta_for_strict_bounds(m_imp->m_settings.m_epsilon); unsigned j; unsigned n = get_core_solver().r_x().size(); do { @@ -1545,7 +1545,7 @@ namespace lp { } void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map& variable_values) const { - mpq delta = get_core_solver().find_delta_for_strict_bounds(mpq(1)); + mpq delta = get_core_solver().find_delta_for_strict_bounds(m_imp->m_settings.m_epsilon); for (unsigned i = 0; i < get_core_solver().r_x().size(); i++) { const impq& rp = get_core_solver().r_x(i); variable_values[i] = rp.x + delta * rp.y; @@ -1569,7 +1569,7 @@ namespace lp { } if (y_is_zero) return; - mpq delta = get_core_solver().find_delta_for_strict_bounds(mpq(1)); + mpq delta = get_core_solver().find_delta_for_strict_bounds(m_imp->m_settings.m_epsilon); for (unsigned j = 0; j < number_of_vars(); j++) { auto& v = get_core_solver().r_x(j); if (!v.y.is_zero()) { diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 48b064567..a89707e45 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -34,6 +34,8 @@ void lp::lp_settings::updt_params(params_ref const& _p) { report_frequency = p.arith_rep_freq(); m_simplex_strategy = static_cast(p.arith_simplex_strategy()); m_nlsat_delay = p.arith_nl_delay(); + auto eps = p.arith_epsilon(); + m_epsilon = rational(std::max(1, (int)(100000*eps)), 100000); m_dio = lp_p.dio(); m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory(); m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf(); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index a7a2d96dd..ef71d37da 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -242,6 +242,7 @@ private: public: unsigned limit_on_rows_for_hnf_cutter = 75; unsigned limit_on_columns_for_hnf_cutter = 150; + mpq m_epsilon = mpq(1); private: unsigned m_nlsat_delay = 0; bool m_enable_hnf = true; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 39a737829..d5af57ef2 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -86,6 +86,7 @@ def_module_params(module_name='smt', ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), + ('arith.epsilon', DOUBLE, 1.0, 'initial value of epsilon used for model generation of infinitesimals'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), diff --git a/src/params/theory_arith_params.cpp b/src/params/theory_arith_params.cpp index fdb7a71b4..27a8949b0 100644 --- a/src/params/theory_arith_params.cpp +++ b/src/params/theory_arith_params.cpp @@ -41,6 +41,8 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials(); m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds(); m_nl_arith_cross_nested = p.arith_nl_cross_nested(); + auto eps = p.arith_epsilon(); + m_arith_epsilon = rational(std::max(1, (int)(100000*eps)), 100000); arith_rewriter_params ap(_p); m_arith_eq2ineq = ap.eq2ineq(); @@ -99,4 +101,5 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nl_arith_cross_nested); DISPLAY_PARAM(m_arith_validate); DISPLAY_PARAM(m_arith_dump_lemmas); + DISPLAY_PARAM(m_arith_epsilon); } diff --git a/src/params/theory_arith_params.h b/src/params/theory_arith_params.h index 26dadef58..8329ae1fd 100644 --- a/src/params/theory_arith_params.h +++ b/src/params/theory_arith_params.h @@ -20,6 +20,7 @@ Revision History: #include #include "util/params.h" +#include "util/rational.h" enum class arith_solver_id { AS_NO_ARITH, // 0 @@ -76,6 +77,7 @@ struct theory_arith_params { unsigned m_arith_branch_cut_ratio = 2; bool m_arith_int_eq_branching = false; bool m_arith_enum_const_mod = false; + rational m_arith_epsilon = rational::one(); bool m_arith_gcd_test = true; bool m_arith_eager_gcd = false; diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 6f40cab0f..0a90495c7 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3174,7 +3174,8 @@ namespace smt { template void theory_arith::compute_epsilon() { - m_epsilon = numeral(1); + auto eps = ctx.get_fparams().m_arith_epsilon; + m_epsilon = numeral(eps); theory_var num = get_num_vars(); for (theory_var v = 0; v < num; v++) { bound * l = lower(v); From 4082e4e56adc19bd3eb45ca7c80a0df33936f334 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 16:48:41 -0700 Subject: [PATCH 19/28] update on euf --- src/ast/simplifiers/euf_completion.cpp | 34 ++++++++++++++++++++++---- src/ast/simplifiers/euf_completion.h | 4 +++ 2 files changed, 33 insertions(+), 5 deletions(-) diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index cea801ae7..a78338226 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -244,7 +244,7 @@ namespace euf { unsigned sz = qtail(); for (unsigned i = qhead(); i < sz; ++i) { auto [f, p, d] = m_fmls[i](); - if (is_app(f) && to_app(f)->get_num_args() == 1 && symbol("congruences") == to_app(f)->get_decl()->get_name()) + if (is_congruences(f)) map_congruence(to_app(f)->get_arg(0)); } } @@ -255,6 +255,11 @@ namespace euf { return; expr_ref_vector args(m); expr_mark visited; + proof_ref pr(m); + expr_dependency_ref dep(m); + auto canon = get_canonical(n->get_expr(), pr, dep); + args.push_back(canon); + visited.mark(canon); for (auto s : enode_class(n)) { expr_ref r(s->get_expr(), m); m_rewriter(r); @@ -329,6 +334,12 @@ namespace euf { if (a->get_root() == b->get_root()) return; + expr_ref x1(x, m); + m_rewriter(x1); +// enode* a1 = mk_enode(x1); +// if (a->get_root() != a1->get_root()) +// m_egraph.merge(a, a1, nullptr); + TRACE(euf, tout << "merge and propagate\n"); add_children(a); add_children(b); @@ -344,6 +355,7 @@ namespace euf { else if (m.is_not(f, nf)) { expr_ref f1(nf, m); m_rewriter(f1); + enode* n = mk_enode(f1); if (m.is_false(n->get_root()->get_expr())) return; @@ -351,6 +363,9 @@ namespace euf { auto n_false = mk_enode(m.mk_false()); auto j = to_ptr(push_pr_dep(pr, d)); m_egraph.merge(n, n_false, j); + if (nf != f1) + m_egraph.merge(n, mk_enode(nf), nullptr); + m_egraph.propagate(); add_children(n); m_should_propagate = true; @@ -358,6 +373,15 @@ namespace euf { m_side_condition_solver->add_constraint(f, pr, d); IF_VERBOSE(1, verbose_stream() << "not: " << nf << "\n"); } + else if (is_congruences(f)) { + auto t = to_app(f)->get_arg(0); + expr_ref r(t, m); + m_rewriter(r); + auto a = mk_enode(t); + auto b = mk_enode(r); + m_egraph.merge(a, b, nullptr); + m_egraph.propagate(); + } else { expr_ref f1(f, m); if (!m.is_implies(f) && !is_quantifier(f)) { @@ -1104,7 +1128,6 @@ namespace euf { } else UNREACHABLE(); - } enode* n = m_egraph.find(f); if (!n) n = mk_enode(f); @@ -1113,10 +1136,11 @@ namespace euf { d = m.mk_join(d, m_deps.get(r->get_id(), nullptr)); if (m.proofs_enabled()) { pr = prove_eq(n, r); - if (get_canonical_proof(r)) - pr = m.mk_transitivity(pr, get_canonical_proof(r)); + if (get_canonical_proof(r)) + pr = m.mk_transitivity(pr, get_canonical_proof(r)); } - SASSERT(m_canonical.get(r->get_id())); + if (!m_canonical.get(r->get_id())) + m_canonical.setx(r->get_id(), r->get_expr()); return expr_ref(m_canonical.get(r->get_id()), m); } diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h index 02366ee7d..ecf258986 100644 --- a/src/ast/simplifiers/euf_completion.h +++ b/src/ast/simplifiers/euf_completion.h @@ -175,6 +175,10 @@ namespace euf { void map_congruence(expr* t); void add_consequence(expr* t); + bool is_congruences(expr* f) const { + return is_app(f) && to_app(f)->get_num_args() == 1 && symbol("congruences") == to_app(f)->get_decl()->get_name(); + } + // Enable equality propagation inside of quantifiers // add quantifier bodies as closure terms to the E-graph. // use fresh variables for bound variables, but such that the fresh variables are From ff74af7eaa8f419a36be355ed68a9b5c5cc984cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 16:50:28 -0700 Subject: [PATCH 20/28] check for internalized in solve_for --- src/smt/theory_lra.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f3d9a5169..5eba2eba1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1296,10 +1296,14 @@ public: // q = 0 or p = (p mod q) + q * (p div q) // q = 0 or (p mod q) >= 0 // q = 0 or (p mod q) < abs(q) + // q >= 0 or (p mod q) = (p mod -q) mk_axiom(eqz, eq); mk_axiom(eqz, mod_ge_0); mk_axiom(eqz, mod_lt_q); +// if (!a.is_uminus(q)) +// mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q))))); + m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p)); if (a.is_zero(p)) { @@ -3732,6 +3736,8 @@ public: unsigned_vector vars; unsigned j = 0; for (auto [e, t, g] : solutions) { + if (!ctx().e_internalized(e)) + continue; auto n = get_enode(e); if (!n) { solutions[j++] = { e, t, g }; From 7ff0b246e8e108d4649e0e1b302e9c9d87b01e73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 17:08:27 -0700 Subject: [PATCH 21/28] fix #7792 add missing revert operations --- src/ast/simplifiers/model_reconstruction_trail.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 85b22475f..3520b1ca0 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -80,6 +80,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt add_vars(v, free_vars); st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr)); } + m_trail_stack.push(value_trail(t->m_active)); t->m_active = false; continue; } @@ -90,6 +91,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt TRACE(simplifier, tout << "replay removed " << r << "\n"); st.add(r); } + m_trail_stack.push(value_trail(t->m_active)); t->m_active = false; continue; } From 4542fc0b3b942f9c971362348e2482adb4dfcd66 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 17:09:56 -0700 Subject: [PATCH 22/28] update version number to 4.15.4 Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- MODULE.bazel | 2 +- scripts/mk_project.py | 2 +- scripts/nightly.yaml | 2 +- scripts/release.yml | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 25751040e..9841e3a68 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.16) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.15.3.0 LANGUAGES CXX) +project(Z3 VERSION 4.15.4.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/MODULE.bazel b/MODULE.bazel index a585d07c2..d9c0ac876 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -1,6 +1,6 @@ module( name = "z3", - version = "4.15.3", + version = "4.15.4", bazel_compatibility = [">=7.0.0"], ) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index f3e350ed1..6b6bef438 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 15, 3, 0) # express a default build version or pick up ci build version + set_version(4, 15, 4, 0) # express a default build version or pick up ci build version # Z3 Project definition def init_project_def(): diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 93a7baa77..898745c1e 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,7 +1,7 @@ variables: Major: '4' Minor: '15' - Patch: '3' + Patch: '4' ReleaseVersion: $(Major).$(Minor).$(Patch) AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId) NightlyVersion: $(AssemblyVersion)-$(Build.buildId) diff --git a/scripts/release.yml b/scripts/release.yml index 0aaef56da..b923b7285 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.15.3' + ReleaseVersion: '4.15.4' stages: From 21e31684211bc76c5d69e52af3a34fc5db1eba2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 17:20:10 -0700 Subject: [PATCH 23/28] fix #7753 --- src/sat/smt/arith_axioms.cpp | 3 +++ src/smt/theory_lra.cpp | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index e594b8bc6..49736e4c3 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -168,6 +168,9 @@ namespace arith { add_clause(eqz, mod_ge_0); add_clause(eqz, mod_lt_q); + if (!a.is_uminus(q)) + add_clause(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q))))); + #if 0 /*literal div_ge_0 = */ mk_literal(a.mk_ge(div, zero)); /*literal div_le_0 = */ mk_literal(a.mk_le(div, zero)); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5eba2eba1..8c6dbead1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1301,8 +1301,8 @@ public: mk_axiom(eqz, eq); mk_axiom(eqz, mod_ge_0); mk_axiom(eqz, mod_lt_q); -// if (!a.is_uminus(q)) -// mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q))))); + if (!a.is_uminus(q)) + mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q))))); m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p)); From debe04350cf620c3e54b6ed84c43c75e62c619a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Aug 2025 09:30:03 -0700 Subject: [PATCH 24/28] fix #7796 Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/extract_eqs.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp index ffc8c7cb7..8789fa569 100644 --- a/src/ast/simplifiers/extract_eqs.cpp +++ b/src/ast/simplifiers/extract_eqs.cpp @@ -115,7 +115,7 @@ namespace euf { if (is_eq_of(x2, y1, z, s, t) && is_complementary(x1, y2)) eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x1, s, t), m), d)); } - if (m.is_and(f, x1, y1) && m.is_or(x, x1, x2) && m.is_or(y1, y1, y2)) { + if (m.is_and(f, x1, y1) && m.is_or(x1, x1, x2) && m.is_or(y1, y1, y2)) { expr* z = nullptr, *t = nullptr, *s = nullptr; if (is_eq_of(x1, y1, z, s, t) && is_complementary(x2, y2)) eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y2, s, t), m), d)); From 265265a68c4514a4ead7272d6c37135f1c416fb2 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 20 Aug 2025 09:12:33 -0700 Subject: [PATCH 25/28] Create centralized version management with VERSION.txt (#7802) * Initial plan * Create VERSION.txt and update CMakeLists.txt to read version from file Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete centralized version management system Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix version update script and finalize implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Create centralized version management with VERSION.txt 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> --- CMakeLists.txt | 7 +- MODULE.bazel | 2 +- VERSION.txt | 1 + scripts/mk_project.py | 15 +++- scripts/nightly.yaml | 6 +- scripts/release.yml | 2 +- scripts/update_version.py | 139 ++++++++++++++++++++++++++++++++++++++ 7 files changed, 166 insertions(+), 6 deletions(-) create mode 100644 VERSION.txt create mode 100755 scripts/update_version.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 9841e3a68..d1cfa8ee3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,12 @@ cmake_minimum_required(VERSION 3.16) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.15.4.0 LANGUAGES CXX) + +# Read version from VERSION.txt file +file(READ "${CMAKE_CURRENT_SOURCE_DIR}/VERSION.txt" Z3_VERSION_FROM_FILE) +string(STRIP "${Z3_VERSION_FROM_FILE}" Z3_VERSION_FROM_FILE) + +project(Z3 VERSION ${Z3_VERSION_FROM_FILE} LANGUAGES CXX) ################################################################################ # Project version diff --git a/MODULE.bazel b/MODULE.bazel index d9c0ac876..c368221da 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -1,6 +1,6 @@ module( name = "z3", - version = "4.15.4", + version = "4.16.0", # TODO: Read from VERSION.txt - currently manual sync required bazel_compatibility = [">=7.0.0"], ) diff --git a/VERSION.txt b/VERSION.txt new file mode 100644 index 000000000..6baf7570c --- /dev/null +++ b/VERSION.txt @@ -0,0 +1 @@ +4.15.4.0 diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6b6bef438..da73e2daf 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,20 @@ from mk_util import * def init_version(): - set_version(4, 15, 4, 0) # express a default build version or pick up ci build version + # Read version from VERSION.txt file + version_file_path = os.path.join(os.path.dirname(os.path.dirname(__file__)), 'VERSION.txt') + try: + with open(version_file_path, 'r') as f: + version_str = f.read().strip() + version_parts = version_str.split('.') + if len(version_parts) >= 4: + major, minor, build, tweak = int(version_parts[0]), int(version_parts[1]), int(version_parts[2]), int(version_parts[3]) + else: + major, minor, build, tweak = int(version_parts[0]), int(version_parts[1]), int(version_parts[2]), 0 + set_version(major, minor, build, tweak) + except (IOError, ValueError) as e: + print(f"Warning: Could not read version from VERSION.txt: {e}") + set_version(4, 15, 4, 0) # fallback to default version # Z3 Project definition def init_project_def(): diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 898745c1e..5323f8bc0 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,10 +1,12 @@ variables: + # Version components read from VERSION.txt (updated manually when VERSION.txt changes) Major: '4' - Minor: '15' - Patch: '4' + Minor: '16' + Patch: '0' ReleaseVersion: $(Major).$(Minor).$(Patch) AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId) NightlyVersion: $(AssemblyVersion)-$(Build.buildId) + # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better stages: - stage: Build diff --git a/scripts/release.yml b/scripts/release.yml index b923b7285..2a6cd363d 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.15.4' + ReleaseVersion: '4.16.0' # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better stages: diff --git a/scripts/update_version.py b/scripts/update_version.py new file mode 100755 index 000000000..fcc3c5576 --- /dev/null +++ b/scripts/update_version.py @@ -0,0 +1,139 @@ +#!/usr/bin/env python3 +""" +Helper script to update version in all Z3 files when VERSION.txt changes. + +This script reads VERSION.txt and updates the remaining hardcoded version references +that cannot be automatically read from VERSION.txt due to limitations in their +respective build systems. + +Usage: python scripts/update_version.py +""" + +import os +import re +import sys + +def read_version(): + """Read version from VERSION.txt file.""" + script_dir = os.path.dirname(os.path.abspath(__file__)) + version_file = os.path.join(os.path.dirname(script_dir), 'VERSION.txt') + + try: + with open(version_file, 'r') as f: + version = f.read().strip() + return version + except IOError as e: + print(f"Error reading VERSION.txt: {e}") + sys.exit(1) + +def update_bazel_module(version): + """Update MODULE.bazel with the version.""" + script_dir = os.path.dirname(os.path.abspath(__file__)) + module_file = os.path.join(os.path.dirname(script_dir), 'MODULE.bazel') + + # Extract major.minor.patch from major.minor.patch.tweak + version_parts = version.split('.') + if len(version_parts) >= 3: + bazel_version = f"{version_parts[0]}.{version_parts[1]}.{version_parts[2]}" + else: + bazel_version = version + + try: + with open(module_file, 'r') as f: + content = f.read() + + # Update version line in module() block only + content = re.sub( + r'(module\([^)]*?\s+version\s*=\s*")[^"]*(".*?)', + r'\g<1>' + bazel_version + r'\g<2>', + content, + flags=re.DOTALL + ) + + with open(module_file, 'w') as f: + f.write(content) + + print(f"Updated MODULE.bazel version to {bazel_version}") + except IOError as e: + print(f"Error updating MODULE.bazel: {e}") + +def update_nightly_yaml(version): + """Update scripts/nightly.yaml with the version.""" + script_dir = os.path.dirname(os.path.abspath(__file__)) + nightly_file = os.path.join(script_dir, 'nightly.yaml') + + version_parts = version.split('.') + if len(version_parts) >= 3: + major, minor, patch = version_parts[0], version_parts[1], version_parts[2] + else: + print(f"Warning: Invalid version format in VERSION.txt: {version}") + return + + try: + with open(nightly_file, 'r') as f: + content = f.read() + + # Update Major, Minor, Patch variables + content = re.sub(r"(\s+Major:\s*')[^']*('.*)", r"\g<1>" + major + r"\g<2>", content) + content = re.sub(r"(\s+Minor:\s*')[^']*('.*)", r"\g<1>" + minor + r"\g<2>", content) + content = re.sub(r"(\s+Patch:\s*')[^']*('.*)", r"\g<1>" + patch + r"\g<2>", content) + + with open(nightly_file, 'w') as f: + f.write(content) + + print(f"Updated nightly.yaml version to {major}.{minor}.{patch}") + except IOError as e: + print(f"Error updating nightly.yaml: {e}") + +def update_release_yml(version): + """Update scripts/release.yml with the version.""" + script_dir = os.path.dirname(os.path.abspath(__file__)) + release_file = os.path.join(script_dir, 'release.yml') + + # Extract major.minor.patch from major.minor.patch.tweak + version_parts = version.split('.') + if len(version_parts) >= 3: + release_version = f"{version_parts[0]}.{version_parts[1]}.{version_parts[2]}" + else: + release_version = version + + try: + with open(release_file, 'r') as f: + content = f.read() + + # Update ReleaseVersion variable + content = re.sub( + r"(\s+ReleaseVersion:\s*')[^']*('.*)", + r"\g<1>" + release_version + r"\g<2>", + content + ) + + with open(release_file, 'w') as f: + f.write(content) + + print(f"Updated release.yml version to {release_version}") + except IOError as e: + print(f"Error updating release.yml: {e}") + +def main(): + """Main function.""" + print("Z3 Version Update Script") + print("========================") + + version = read_version() + print(f"Read version from VERSION.txt: {version}") + + print("\nUpdating files that cannot auto-read VERSION.txt...") + + update_bazel_module(version) + update_nightly_yaml(version) + update_release_yml(version) + + print("\nUpdate complete!") + print("\nNote: The following files automatically read from VERSION.txt:") + print(" - CMakeLists.txt") + print(" - scripts/mk_project.py") + print("\nThese do not need manual updates.") + +if __name__ == "__main__": + main() \ No newline at end of file From 72655637deebe5d3a79d7725287c634ac261b6fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Aug 2025 09:24:58 -0700 Subject: [PATCH 26/28] read version from VERSION.txt Signed-off-by: Nikolaj Bjorner --- src/api/python/setup.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 4d26367b3..ab4953977 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -114,11 +114,11 @@ def _clean_native_build(): def _z3_version(): post = os.getenv('Z3_VERSION_SUFFIX', '') if RELEASE_DIR is None: - fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py') + fn = os.path.join(ROOT_DIR, 'VERSION.txt') if os.path.exists(fn): with open(fn) as f: for line in f: - n = re.match(r".*set_version\((.*), (.*), (.*), (.*)\).*", line) + n = re.match(r"(.*), (.*), (.*), (.*)", line) if not n is None: return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post return "?.?.?.?" From 02f195a380afe1c36885fae53361d6a691566377 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Aug 2025 09:39:36 -0700 Subject: [PATCH 27/28] fix version parse Signed-off-by: Nikolaj Bjorner --- src/api/python/setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index ab4953977..fe3473cb2 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -118,7 +118,7 @@ def _z3_version(): if os.path.exists(fn): with open(fn) as f: for line in f: - n = re.match(r"(.*), (.*), (.*), (.*)", line) + n = re.match(r"(.*)\.(.*)\.(.*)\.(.*)", line) if not n is None: return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post return "?.?.?.?" From fa0f9c97bc0149eb7e98194f7793415165796fc1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Aug 2025 09:45:06 -0700 Subject: [PATCH 28/28] fix parsing of version Signed-off-by: Nikolaj Bjorner --- src/api/python/setup.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index fe3473cb2..6b400c7d4 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -114,7 +114,7 @@ def _clean_native_build(): def _z3_version(): post = os.getenv('Z3_VERSION_SUFFIX', '') if RELEASE_DIR is None: - fn = os.path.join(ROOT_DIR, 'VERSION.txt') + fn = os.path.join(SRC_DIR_REPO, 'VERSION.txt') if os.path.exists(fn): with open(fn) as f: for line in f: @@ -284,7 +284,7 @@ class sdist(_sdist): # The Azure Dev Ops pipelines use internal OS version tagging that don't correspond # to releases. -internal_build_re = re.compile("(.+)\_7") +internal_build_re = re.compile("(.+)_7") class bdist_wheel(_bdist_wheel):