{"owner":"Z3Prover","repo":"z3","hasSkills":true,"hasMcp":false,"mcpConfig":null,"found":[".github/copilot-instructions.md"],"skills":{".github/copilot-instructions.md":"# Z3 Theorem Prover Development Guide\n\nAlways reference these instructions first and fallback to search or bash commands only when you encounter unexpected information that does not match the info here.\n\n## Working Effectively\n\n### Bootstrap and Build the Repository\n\nZ3 supports multiple build systems. **ALWAYS** use one of these validated approaches:\n\n#### Option 1: Python Build System (Recommended for most use cases)\n- `python scripts/mk_make.py` -- takes 7 seconds to configure\n- `cd build && make -j$(nproc)` -- takes 15 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Option 2: CMake Build System (Recommended for integration)\n- Clean source tree first if you previously used Python build: `git clean -fx src/`\n- `mkdir build && cd build`\n- `cmake ..` -- takes 1 second to configure\n- `make -j$(nproc)` -- takes 17 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Dependencies and Requirements\n- Python 3.x (required for both build systems)\n- C++20 capable compiler (g++ or clang++)\n- GNU Make\n- Git (for version information)\n\n### Test the Repository\n\n**Python Build System:**\n- Build unit tests: `make test` -- takes 3.5 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**CMake Build System:**\n- Build unit tests: `make test-z3` -- takes 4 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**Test basic Z3 functionality:**\n```bash\n./z3 --version\necho \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\" | ./z3 -in\n```\n\n### Validation Scenarios\n\n**ALWAYS** test these scenarios after making changes:\n\n#### Basic SMT Solving\n```bash\ncd build\necho \"(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n(get-model)\" | ./z3 -in\n```\nExpected output: `sat` followed by a model showing `x = 1` or similar.\n\n#### Python Bindings\n```bash\ncd build/python\npython3 -c \"import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())\"\n```\nExpected output: `Result: sat` and `Model: [x = 1]` or similar.\n\n#### Command Line Help\n```bash\n./z3 --help | head -10\n```\nShould display version and usage information.\n\n## Build System Details\n\n### Python Build System\n- Configuration: `python scripts/mk_make.py` (7 seconds)\n- Main build: `cd build && make -j$(nproc)` (15 minutes)\n- Test build: `make test` (3.5 minutes)\n- Generates build files in `build/` directory\n- Creates Python bindings in `build/python/`\n- **Warning**: Generates files in source tree that must be cleaned before using CMake\n\n### CMake Build System  \n- Clean first: `git clean -fx src/` (if switching from Python build)\n- Configuration: `cmake ..` (1 second)\n- Main build: `make -j$(nproc)` (17 minutes)\n- **Advantages**: Clean build tree, no source pollution, better for integration\n- **Recommended for**: IDE integration, package management, deployment\n\n### Critical Timing and Timeout Requirements\n\n**NEVER CANCEL these operations**:\n- `make -j$(nproc)` builds: 15-17 minutes. **Set timeout to 30+ minutes minimum**.\n- `make test` or `make test-z3` compilation: 3.5-4 minutes. **Set timeout to 10+ minutes**.\n- Unit test execution: 16 seconds. **Set timeout to 5+ minutes**.\n\n**Always wait for completion**. Z3 is a complex theorem prover with extensive code generation and builds may appear to hang but are actually progressing.\n\n## Repository Structure\n\n### Key Directories\n- `src/` - Main source code organized by components (ast, smt, sat, etc.)\n- `examples/` - Language binding examples (C, C++, Python, Java, .NET, etc.)\n- `scripts/` - Build scripts and utilities\n- `.github/workflows/` - CI/CD pipeline definitions\n- `cmake/` - CMake configuration files\n\n### Important Files\n- `README.md` - Main documentation and build instructions\n- `README-CMake.md` - Detailed CMake build documentation  \n- `configure` - Wrapper script around `scripts/mk_make.py`\n- `CMakeLists.txt` - Main CMake configuration\n- `scripts/mk_make.py` - Python build system entry point\n\n## Common Tasks and Validation\n\n### Pre-commit Validation\nBefore committing changes:\n1. **Build successfully**: Use one of the validated build commands above\n2. **Run unit tests**: `./test-z3 /a` must pass\n3. **Test basic functionality**: Run validation scenarios above\n4. **Test affected language bindings**: If modifying API, test relevant examples\n\n### Working with Language Bindings\n- **Python**: Located in `build/python/`, test with validation scenario above\n- **C/C++**: Examples in `examples/c/` and `examples/c++/`\n  - Compile C++ example: `g++ -I src/api -I src/api/c++ examples/c++/example.cpp -L build -lz3 -o test_example`\n  - Run with: `LD_LIBRARY_PATH=build ./test_example`\n- **Java**: Build with `python scripts/mk_make.py --java`, examples in `examples/java/`\n- **C#/.NET**: Build with `python scripts/mk_make.py --dotnet`, examples in `examples/dotnet/`\n\n### Performance Testing\nFor performance-sensitive changes:\n- Build optimized: `python scripts/mk_make.py` (Release mode by default)\n- Test with realistic SMT problems from `examples/SMT-LIB2/`\n- Use Z3's built-in statistics: `z3 -st problem.smt2`\n\n## Common Issues and Solutions\n\n### Build System Conflicts\n- **Error**: CMake complains about polluted source tree\n- **Solution**: Run `git clean -fx src/` to remove Python build artifacts\n\n### Python Import Errors\n- **Error**: `import z3` fails\n- **Solution**: Ensure you're in `build/python/` directory or add it to `PYTHONPATH`\n\n### Missing Dependencies\n- **Error**: Compiler not found or version too old\n- **Solution**: Z3 requires C++20. Install g++ 10+ or clang++ 10+\n\n### Long Build Times\n- **Normal**: 15-17 minute builds are expected for Z3\n- **Never cancel**: Set timeouts appropriately and wait for completion\n- **Optimization**: Use `make -j$(nproc)` for parallel compilation\n\n## Key Projects in Codebase\n\nZ3 is organized into several key components:\n\n- **Core SMT**: `src/smt/` - Main SMT solver engine\n- **SAT Solver**: `src/sat/` - Underlying boolean satisfiability solver  \n- **Theories**: Various theory solvers (arithmetic, arrays, bit-vectors, etc.)\n- **Abstract Syntax Trees**: `src/ast/` - Expression representation and manipulation\n- **Tactics**: `src/tactic/` - Configurable solving strategies\n- **API**: `src/api/` - Public C API and language bindings\n- **Parsers**: SMT-LIB2, Dimacs, and other input format parsers\n- **Model Generation**: Creating and manipulating satisfying assignments\n\nThe architecture is modular with clean separation between the core solver, theory plugins, and user interfaces."},"files":{".github/copilot-instructions.md":"# Z3 Theorem Prover Development Guide\n\nAlways reference these instructions first and fallback to search or bash commands only when you encounter unexpected information that does not match the info here.\n\n## Working Effectively\n\n### Bootstrap and Build the Repository\n\nZ3 supports multiple build systems. **ALWAYS** use one of these validated approaches:\n\n#### Option 1: Python Build System (Recommended for most use cases)\n- `python scripts/mk_make.py` -- takes 7 seconds to configure\n- `cd build && make -j$(nproc)` -- takes 15 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Option 2: CMake Build System (Recommended for integration)\n- Clean source tree first if you previously used Python build: `git clean -fx src/`\n- `mkdir build && cd build`\n- `cmake ..` -- takes 1 second to configure\n- `make -j$(nproc)` -- takes 17 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Dependencies and Requirements\n- Python 3.x (required for both build systems)\n- C++20 capable compiler (g++ or clang++)\n- GNU Make\n- Git (for version information)\n\n### Test the Repository\n\n**Python Build System:**\n- Build unit tests: `make test` -- takes 3.5 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**CMake Build System:**\n- Build unit tests: `make test-z3` -- takes 4 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**Test basic Z3 functionality:**\n```bash\n./z3 --version\necho \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\" | ./z3 -in\n```\n\n### Validation Scenarios\n\n**ALWAYS** test these scenarios after making changes:\n\n#### Basic SMT Solving\n```bash\ncd build\necho \"(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n(get-model)\" | ./z3 -in\n```\nExpected output: `sat` followed by a model showing `x = 1` or similar.\n\n#### Python Bindings\n```bash\ncd build/python\npython3 -c \"import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())\"\n```\nExpected output: `Result: sat` and `Model: [x = 1]` or similar.\n\n#### Command Line Help\n```bash\n./z3 --help | head -10\n```\nShould display version and usage information.\n\n## Build System Details\n\n### Python Build System\n- Configuration: `python scripts/mk_make.py` (7 seconds)\n- Main build: `cd build && make -j$(nproc)` (15 minutes)\n- Test build: `make test` (3.5 minutes)\n- Generates build files in `build/` directory\n- Creates Python bindings in `build/python/`\n- **Warning**: Generates files in source tree that must be cleaned before using CMake\n\n### CMake Build System  \n- Clean first: `git clean -fx src/` (if switching from Python build)\n- Configuration: `cmake ..` (1 second)\n- Main build: `make -j$(nproc)` (17 minutes)\n- **Advantages**: Clean build tree, no source pollution, better for integration\n- **Recommended for**: IDE integration, package management, deployment\n\n### Critical Timing and Timeout Requirements\n\n**NEVER CANCEL these operations**:\n- `make -j$(nproc)` builds: 15-17 minutes. **Set timeout to 30+ minutes minimum**.\n- `make test` or `make test-z3` compilation: 3.5-4 minutes. **Set timeout to 10+ minutes**.\n- Unit test execution: 16 seconds. **Set timeout to 5+ minutes**.\n\n**Always wait for completion**. Z3 is a complex theorem prover with extensive code generation and builds may appear to hang but are actually progressing.\n\n## Repository Structure\n\n### Key Directories\n- `src/` - Main source code organized by components (ast, smt, sat, etc.)\n- `examples/` - Language binding examples (C, C++, Python, Java, .NET, etc.)\n- `scripts/` - Build scripts and utilities\n- `.github/workflows/` - CI/CD pipeline definitions\n- `cmake/` - CMake configuration files\n\n### Important Files\n- `README.md` - Main documentation and build instructions\n- `README-CMake.md` - Detailed CMake build documentation  \n- `configure` - Wrapper script around `scripts/mk_make.py`\n- `CMakeLists.txt` - Main CMake configuration\n- `scripts/mk_make.py` - Python build system entry point\n\n## Common Tasks and Validation\n\n### Pre-commit Validation\nBefore committing changes:\n1. **Build successfully**: Use one of the validated build commands above\n2. **Run unit tests**: `./test-z3 /a` must pass\n3. **Test basic functionality**: Run validation scenarios above\n4. **Test affected language bindings**: If modifying API, test relevant examples\n\n### Working with Language Bindings\n- **Python**: Located in `build/python/`, test with validation scenario above\n- **C/C++**: Examples in `examples/c/` and `examples/c++/`\n  - Compile C++ example: `g++ -I src/api -I src/api/c++ examples/c++/example.cpp -L build -lz3 -o test_example`\n  - Run with: `LD_LIBRARY_PATH=build ./test_example`\n- **Java**: Build with `python scripts/mk_make.py --java`, examples in `examples/java/`\n- **C#/.NET**: Build with `python scripts/mk_make.py --dotnet`, examples in `examples/dotnet/`\n\n### Performance Testing\nFor performance-sensitive changes:\n- Build optimized: `python scripts/mk_make.py` (Release mode by default)\n- Test with realistic SMT problems from `examples/SMT-LIB2/`\n- Use Z3's built-in statistics: `z3 -st problem.smt2`\n\n## Common Issues and Solutions\n\n### Build System Conflicts\n- **Error**: CMake complains about polluted source tree\n- **Solution**: Run `git clean -fx src/` to remove Python build artifacts\n\n### Python Import Errors\n- **Error**: `import z3` fails\n- **Solution**: Ensure you're in `build/python/` directory or add it to `PYTHONPATH`\n\n### Missing Dependencies\n- **Error**: Compiler not found or version too old\n- **Solution**: Z3 requires C++20. Install g++ 10+ or clang++ 10+\n\n### Long Build Times\n- **Normal**: 15-17 minute builds are expected for Z3\n- **Never cancel**: Set timeouts appropriately and wait for completion\n- **Optimization**: Use `make -j$(nproc)` for parallel compilation\n\n## Key Projects in Codebase\n\nZ3 is organized into several key components:\n\n- **Core SMT**: `src/smt/` - Main SMT solver engine\n- **SAT Solver**: `src/sat/` - Underlying boolean satisfiability solver  \n- **Theories**: Various theory solvers (arithmetic, arrays, bit-vectors, etc.)\n- **Abstract Syntax Trees**: `src/ast/` - Expression representation and manipulation\n- **Tactics**: `src/tactic/` - Configurable solving strategies\n- **API**: `src/api/` - Public C API and language bindings\n- **Parsers**: SMT-LIB2, Dimacs, and other input format parsers\n- **Model Generation**: Creating and manipulating satisfying assignments\n\nThe architecture is modular with clean separation between the core solver, theory plugins, and user interfaces."},"items":[{"name":"copilot-instructions.md","path":".github/copilot-instructions.md","title":"copilot-instructions.md","content":"# Z3 Theorem Prover Development Guide\n\nAlways reference these instructions first and fallback to search or bash commands only when you encounter unexpected information that does not match the info here.\n\n## Working Effectively\n\n### Bootstrap and Build the Repository\n\nZ3 supports multiple build systems. **ALWAYS** use one of these validated approaches:\n\n#### Option 1: Python Build System (Recommended for most use cases)\n- `python scripts/mk_make.py` -- takes 7 seconds to configure\n- `cd build && make -j$(nproc)` -- takes 15 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Option 2: CMake Build System (Recommended for integration)\n- Clean source tree first if you previously used Python build: `git clean -fx src/`\n- `mkdir build && cd build`\n- `cmake ..` -- takes 1 second to configure\n- `make -j$(nproc)` -- takes 17 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Dependencies and Requirements\n- Python 3.x (required for both build systems)\n- C++20 capable compiler (g++ or clang++)\n- GNU Make\n- Git (for version information)\n\n### Test the Repository\n\n**Python Build System:**\n- Build unit tests: `make test` -- takes 3.5 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**CMake Build System:**\n- Build unit tests: `make test-z3` -- takes 4 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**Test basic Z3 functionality:**\n```bash\n./z3 --version\necho \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\" | ./z3 -in\n```\n\n### Validation Scenarios\n\n**ALWAYS** test these scenarios after making changes:\n\n#### Basic SMT Solving\n```bash\ncd build\necho \"(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n(get-model)\" | ./z3 -in\n```\nExpected output: `sat` followed by a model showing `x = 1` or similar.\n\n#### Python Bindings\n```bash\ncd build/python\npython3 -c \"import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())\"\n```\nExpected output: `Result: sat` and `Model: [x = 1]` or similar.\n\n#### Command Line Help\n```bash\n./z3 --help | head -10\n```\nShould display version and usage information.\n\n## Build System Details\n\n### Python Build System\n- Configuration: `python scripts/mk_make.py` (7 seconds)\n- Main build: `cd build && make -j$(nproc)` (15 minutes)\n- Test build: `make test` (3.5 minutes)\n- Generates build files in `build/` directory\n- Creates Python bindings in `build/python/`\n- **Warning**: Generates files in source tree that must be cleaned before using CMake\n\n### CMake Build System  \n- Clean first: `git clean -fx src/` (if switching from Python build)\n- Configuration: `cmake ..` (1 second)\n- Main build: `make -j$(nproc)` (17 minutes)\n- **Advantages**: Clean build tree, no source pollution, better for integration\n- **Recommended for**: IDE integration, package management, deployment\n\n### Critical Timing and Timeout Requirements\n\n**NEVER CANCEL these operations**:\n- `make -j$(nproc)` builds: 15-17 minutes. **Set timeout to 30+ minutes minimum**.\n- `make test` or `make test-z3` compilation: 3.5-4 minutes. **Set timeout to 10+ minutes**.\n- Unit test execution: 16 seconds. **Set timeout to 5+ minutes**.\n\n**Always wait for completion**. Z3 is a complex theorem prover with extensive code generation and builds may appear to hang but are actually progressing.\n\n## Repository Structure\n\n### Key Directories\n- `src/` - Main source code organized by components (ast, smt, sat, etc.)\n- `examples/` - Language binding examples (C, C++, Python, Java, .NET, etc.)\n- `scripts/` - Build scripts and utilities\n- `.github/workflows/` - CI/CD pipeline definitions\n- `cmake/` - CMake configuration files\n\n### Important Files\n- `README.md` - Main documentation and build instructions\n- `README-CMake.md` - Detailed CMake build documentation  \n- `configure` - Wrapper script around `scripts/mk_make.py`\n- `CMakeLists.txt` - Main CMake configuration\n- `scripts/mk_make.py` - Python build system entry point\n\n## Common Tasks and Validation\n\n### Pre-commit Validation\nBefore committing changes:\n1. **Build successfully**: Use one of the validated build commands above\n2. **Run unit tests**: `./test-z3 /a` must pass\n3. **Test basic functionality**: Run validation scenarios above\n4. **Test affected language bindings**: If modifying API, test relevant examples\n\n### Working with Language Bindings\n- **Python**: Located in `build/python/`, test with validation scenario above\n- **C/C++**: Examples in `examples/c/` and `examples/c++/`\n  - Compile C++ example: `g++ -I src/api -I src/api/c++ examples/c++/example.cpp -L build -lz3 -o test_example`\n  - Run with: `LD_LIBRARY_PATH=build ./test_example`\n- **Java**: Build with `python scripts/mk_make.py --java`, examples in `examples/java/`\n- **C#/.NET**: Build with `python scripts/mk_make.py --dotnet`, examples in `examples/dotnet/`\n\n### Performance Testing\nFor performance-sensitive changes:\n- Build optimized: `python scripts/mk_make.py` (Release mode by default)\n- Test with realistic SMT problems from `examples/SMT-LIB2/`\n- Use Z3's built-in statistics: `z3 -st problem.smt2`\n\n## Common Issues and Solutions\n\n### Build System Conflicts\n- **Error**: CMake complains about polluted source tree\n- **Solution**: Run `git clean -fx src/` to remove Python build artifacts\n\n### Python Import Errors\n- **Error**: `import z3` fails\n- **Solution**: Ensure you're in `build/python/` directory or add it to `PYTHONPATH`\n\n### Missing Dependencies\n- **Error**: Compiler not found or version too old\n- **Solution**: Z3 requires C++20. Install g++ 10+ or clang++ 10+\n\n### Long Build Times\n- **Normal**: 15-17 minute builds are expected for Z3\n- **Never cancel**: Set timeouts appropriately and wait for completion\n- **Optimization**: Use `make -j$(nproc)` for parallel compilation\n\n## Key Projects in Codebase\n\nZ3 is organized into several key components:\n\n- **Core SMT**: `src/smt/` - Main SMT solver engine\n- **SAT Solver**: `src/sat/` - Underlying boolean satisfiability solver  \n- **Theories**: Various theory solvers (arithmetic, arrays, bit-vectors, etc.)\n- **Abstract Syntax Trees**: `src/ast/` - Expression representation and manipulation\n- **Tactics**: `src/tactic/` - Configurable solving strategies\n- **API**: `src/api/` - Public C API and language bindings\n- **Parsers**: SMT-LIB2, Dimacs, and other input format parsers\n- **Model Generation**: Creating and manipulating satisfying assignments\n\nThe architecture is modular with clean separation between the core solver, theory plugins, and user interfaces.","category":".github","tokens":1678}]}