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 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}} diff --git a/CMakeLists.txt b/CMakeLists.txt index 25751040e..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.3.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 a585d07c2..c368221da 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -1,6 +1,6 @@ module( name = "z3", - version = "4.15.3", + 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/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 - MAX_EXAMPLES: + break + if not benchmark.endswith(".smt2"): + continue + + filepath = os.path.join(bench_dir, benchmark) + print(f"Running {filepath}\n") + + scores = {} + for n, v in params: + s = z3.SimpleSolver() + s.from_file(filepath) + + s.set("smt.auto_config", False) + s.set(n, v) + s.set("smt.max_conflicts", MAX_CONFLICTS) + + r = s.check() + st = s.statistics() + + try: + conf = st.get_key_value('conflicts') + except: + try: + conf = st.num_conflicts() + except AttributeError: + conf = None + + scores[(n, v)] = conf + + num_examples += 1 + + print(f"Scores for {benchmark}: {scores}") diff --git a/scripts/mk_project.py b/scripts/mk_project.py index f3e350ed1..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, 3, 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 932fc778e..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: '3' + 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 @@ -471,49 +473,12 @@ stages: tagSource: 'userSpecifiedTag' tag: 'Nightly' title: 'Nightly' - releaseNotesSource: 'input' + releaseNotesSource: 'inline' releaseNotes: 'nightly build' assets: 'tmp/*' assetUploadMode: 'replace' 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. diff --git a/scripts/release.yml b/scripts/release.yml index 946b002f3..2a6cd363d 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.15.3' + ReleaseVersion: '4.16.0' # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better stages: @@ -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" 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 diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index dad3bc126..05b93d38b 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; @@ -274,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); diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 4d26367b3..6b400c7d4 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(SRC_DIR_REPO, '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 "?.?.?.?" @@ -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): 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) 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: 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/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; } diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index 1a32a1bd5..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,7 +373,21 @@ 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)) { + m_rewriter(f1); + f = f1; + } enode* n = mk_enode(f); if (m.is_true(n->get_root()->get_expr())) return; @@ -1099,7 +1128,6 @@ namespace euf { } else UNREACHABLE(); - } enode* n = m_egraph.find(f); if (!n) n = mk_enode(f); @@ -1108,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 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)); 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; } 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 c8e2cf862..42d6d8ef6 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 e3ee2344d..d86b7d70e 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -245,6 +245,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/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())); + } } } 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); 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/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/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/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); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4b544fc20..b9c804b3e 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)) { @@ -3734,6 +3738,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 }; 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) {