diff --git a/.github/ISSUE_TEMPLATE/01-bug-report.yml b/.github/ISSUE_TEMPLATE/01-bug-report.yml new file mode 100644 index 000000000..a021d3aa6 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/01-bug-report.yml @@ -0,0 +1,140 @@ +name: 🐛 Bug Report +description: Report a bug or incorrect behavior in Z3 +title: "[Bug] " +labels: ["bug"] +body: + - type: markdown + attributes: + value: | + Thank you for reporting a bug! This helps make Z3 better. + + Please provide as much detail as possible to help us reproduce and fix the issue. + + - type: dropdown + id: bug-category + attributes: + label: Bug Category + description: What type of bug are you experiencing? + options: + - Crash/Assertion failure + - Incorrect result (SAT/UNSAT/Unknown) + - Performance regression + - Memory issue/leak + - API behavior + - Build/Installation issue + - Other + validations: + required: true + + - type: textarea + id: description + attributes: + label: Bug Description + description: A clear and concise description of the bug + placeholder: Describe what happens vs what you expected... + validations: + required: true + + - type: textarea + id: minimal-example + attributes: + label: Minimal Reproduction + description: Please provide the smallest possible example that reproduces the issue + placeholder: | + (set-logic QF_LIA) + (declare-fun x () Int) + (assert (> x 5)) + (check-sat) + render: smt2 + validations: + required: true + + - type: textarea + id: expected-behavior + attributes: + label: Expected Behavior + description: What did you expect to happen? + validations: + required: true + + - type: textarea + id: actual-behavior + attributes: + label: Actual Behavior + description: What actually happened? Include full error messages/output + validations: + required: true + + - type: input + id: version + attributes: + label: Z3 Version + description: What version of Z3 are you using? (run `z3 --version`) + placeholder: Z3 version 4.13.0 - 64 bit + validations: + required: true + + - type: dropdown + id: platform + attributes: + label: Platform + description: What platform are you running Z3 on? + options: + - Linux x86_64 + - macOS ARM64 (Apple Silicon) + - macOS Intel x86_64 + - Windows x86_64 + - Windows ARM64 + - Other (specify in additional context) + validations: + required: true + + - type: dropdown + id: interface + attributes: + label: Interface Used + description: How are you using Z3? + options: + - Command line (z3 executable) + - Python API + - C++ API + - C API + - Java API + - .NET API + - OCaml API + - JavaScript/WASM API + - Other (specify below) + validations: + required: true + + - type: textarea + id: installation-method + attributes: + label: Installation Method + description: How did you install Z3? + placeholder: "e.g., pip install z3-solver, built from source, downloaded from releases, package manager, etc." + + - type: textarea + id: additional-context + attributes: + label: Additional Context + description: Any other information that might be helpful (stack traces, related issues, workarounds, etc.) + + - type: checkboxes + id: regression + attributes: + label: Regression Check + description: Help us identify if this is a recent regression + options: + - label: This worked in a previous version of Z3 + required: false + - label: I can provide the last working version + required: false + + - type: markdown + attributes: + value: | + ### Before submitting + - [ ] I searched existing issues and couldn't find a duplicate + - [ ] I provided a minimal reproduction case + - [ ] I included the Z3 version and platform information \ No newline at end of file diff --git a/.github/ISSUE_TEMPLATE/02-performance-issue.yml b/.github/ISSUE_TEMPLATE/02-performance-issue.yml new file mode 100644 index 000000000..e9c09b43d --- /dev/null +++ b/.github/ISSUE_TEMPLATE/02-performance-issue.yml @@ -0,0 +1,163 @@ +name: ⚡ Performance Issue +description: Report performance problems or regressions in Z3 +title: "[Performance] " +labels: ["performance"] +body: + - type: markdown + attributes: + value: | + Thank you for reporting a performance issue! This helps us keep Z3 fast and efficient. + + - type: dropdown + id: performance-type + attributes: + label: Performance Issue Type + description: What kind of performance problem are you experiencing? + options: + - Slow solving (takes too long) + - Memory usage (uses too much memory) + - Timeout/infinite loop + - Regression (was faster in previous version) + - Scalability issue (doesn't scale well) + validations: + required: true + + - type: textarea + id: description + attributes: + label: Issue Description + description: Describe the performance problem + placeholder: Z3 takes much longer than expected to solve this formula... + validations: + required: true + + - type: textarea + id: formula + attributes: + label: Input Formula + description: Please provide the formula that exhibits the performance issue. For large files, consider attaching or linking to them. + placeholder: | + (set-logic QF_BV) + (declare-fun x () (_ BitVec 32)) + ; ... large formula here + render: smt2 + validations: + required: true + + - type: textarea + id: timing-info + attributes: + label: Performance Measurements + description: Provide timing and memory usage information + placeholder: | + Current behavior: Takes 300+ seconds, uses 8GB memory + Expected: Should complete in <10 seconds based on similar formulas + + Command used: z3 -smt2 formula.smt2 + System specs: Intel i7, 16GB RAM + value: | + **Current performance:** + - Time: + - Memory: + - Command: + + **Expected performance:** + - + + **System specifications:** + - CPU: + - Memory: + - Other relevant specs: + validations: + required: true + + - type: input + id: version + attributes: + label: Z3 Version + description: What version of Z3 are you using? + placeholder: Z3 version 4.13.0 - 64 bit + validations: + required: true + + - type: dropdown + id: regression-info + attributes: + label: Is this a regression? + description: Did this work better in a previous version? + options: + - "No, this has always been slow" + - "Yes, this is slower than a previous version" + - "I don't know" + validations: + required: true + + - type: input + id: last-working-version + attributes: + label: Last Working Version (if regression) + description: If this is a regression, what was the last version that performed well? + placeholder: e.g., Z3 4.12.6 + + - type: dropdown + id: theory + attributes: + label: Primary Theory + description: What's the main theory used in your formula? + options: + - Linear Arithmetic (LIA/LRA) + - Bit-vectors (QF_BV) + - Arrays + - Strings + - Uninterpreted Functions + - Quantifiers + - Mixed/Multiple theories + - Other/Unknown + validations: + required: true + + - type: textarea + id: solver-options + attributes: + label: Solver Configuration + description: Are you using any specific solver options or tactics? + placeholder: | + Command line: z3 -smt2 -T:300 formula.smt2 + Options: sat.max_memory=4096 + Tactics: None / Custom tactic used + + - type: textarea + id: workarounds + attributes: + label: Workarounds Found + description: Have you found any parameter changes or tactics that improve performance? + placeholder: Setting rewriter.bv_sort_ac=true helps significantly + + - type: textarea + id: additional-context + attributes: + label: Additional Context + description: Any other details that might help (related formulas, use case, etc.) + + - type: checkboxes + id: testing + attributes: + label: Testing Information + description: Help us understand your testing approach + options: + - label: I tested with the latest Z3 version + required: false + - label: I can provide the input file separately if it's too large + required: false + - label: This is blocking my work/research + required: false + + - type: markdown + attributes: + value: | + ### Before submitting + - [ ] I searched existing performance issues + - [ ] I provided timing/memory measurements + - [ ] I specified the Z3 version and system specs + + For very large input files, consider uploading them separately or providing a link. \ No newline at end of file diff --git a/.github/ISSUE_TEMPLATE/03-feature-request.yml b/.github/ISSUE_TEMPLATE/03-feature-request.yml new file mode 100644 index 000000000..c09f671cf --- /dev/null +++ b/.github/ISSUE_TEMPLATE/03-feature-request.yml @@ -0,0 +1,147 @@ +name: ✨ Feature Request +description: Suggest a new feature or enhancement for Z3 +title: "[Feature] " +labels: ["enhancement"] +body: + - type: markdown + attributes: + value: | + Thank you for suggesting a new feature! This helps us understand what users need. + + - type: dropdown + id: feature-category + attributes: + label: Feature Category + description: What area does this feature request relate to? + options: + - New theory support + - API enhancement (Python/C++/Java/.NET/etc.) + - Solver tactics/strategies + - SMT-LIB2 standard compliance + - Build system/packaging + - Performance optimization + - Documentation + - Developer tools/workflow + - Other + validations: + required: true + + - type: textarea + id: summary + attributes: + label: Feature Summary + description: A clear and concise description of the feature you'd like to see + placeholder: I would like Z3 to support... + validations: + required: true + + - type: textarea + id: motivation + attributes: + label: Motivation and Use Case + description: Why do you need this feature? What problem does it solve? + placeholder: | + This feature would help with... + My use case is... + Currently, I have to work around this by... + validations: + required: true + + - type: textarea + id: proposed-solution + attributes: + label: Proposed Solution + description: How do you envision this feature working? + placeholder: | + I think this could be implemented by... + The API could look like... + An example usage would be... + + - type: textarea + id: example + attributes: + label: Example Usage + description: Show how you would use this feature (code examples, SMT-LIB2 syntax, etc.) + placeholder: | + // Python API example: + solver.set_option("new_feature", True) + + ; SMT-LIB2 example: + (set-option :new-feature true) + (assert ...) + render: python + + - type: textarea + id: alternatives + attributes: + label: Alternatives Considered + description: Have you considered any alternative solutions or workarounds? + placeholder: | + I tried using... but it doesn't work because... + Another approach would be... but it has the drawback of... + + - type: dropdown + id: priority + attributes: + label: Priority + description: How important is this feature for your work? + options: + - Low - Nice to have + - Medium - Would be helpful + - High - Important for my work + - Critical - Blocking my research/project + validations: + required: true + + - type: dropdown + id: implementation-help + attributes: + label: Implementation Help + description: Would you be willing to help implement this feature? + options: + - I would like to implement this myself + - I could help with implementation if guided + - I can help with testing/feedback + - I can only provide requirements/feedback + validations: + required: true + + - type: textarea + id: related-work + attributes: + label: Related Work + description: Are there similar features in other solvers, research papers, or standards? + placeholder: | + Similar to CVC5's feature... + Described in paper: ... + SMT-LIB2 standard section: ... + + - type: checkboxes + id: compatibility + attributes: + label: Compatibility Considerations + description: Please consider compatibility aspects + options: + - label: This feature should maintain backward compatibility + required: false + - label: This feature might require breaking API changes + required: false + - label: This feature affects SMT-LIB2 compliance + required: false + + - type: textarea + id: additional-context + attributes: + label: Additional Context + description: Any other information that might be helpful (screenshots, links, research papers, etc.) + + - type: markdown + attributes: + value: | + ### Before submitting + - [ ] I searched existing feature requests and issues + - [ ] I provided clear motivation and use cases + - [ ] I considered backward compatibility implications + + ### After submitting + Community discussion and maintainer feedback will help refine this feature request. Complex features may require design discussions before implementation begins. \ No newline at end of file diff --git a/.github/ISSUE_TEMPLATE/04-question.yml b/.github/ISSUE_TEMPLATE/04-question.yml new file mode 100644 index 000000000..c1d78fa3c --- /dev/null +++ b/.github/ISSUE_TEMPLATE/04-question.yml @@ -0,0 +1,111 @@ +name: ❓ Question +description: Ask a question about using Z3 or understanding its behavior +title: "[Question] " +labels: ["question"] +body: + - type: markdown + attributes: + value: | + ### ⚠️ Before asking a question + + For general Z3 usage questions, tutorials, and discussions, please consider using: + - **[GitHub Discussions](../../discussions)** - Best for open-ended discussions + - **[Stack Overflow](https://stackoverflow.com/questions/tagged/z3)** - Great for specific coding questions + - **[Z3 Guide](https://microsoft.github.io/z3guide/)** - Comprehensive tutorials and documentation + + Use this issue template only for questions that are: + - Specific to Z3's internal behavior or design decisions + - Related to undocumented behavior that might be a bug + - Questions that could lead to documentation improvements + + - type: dropdown + id: question-type + attributes: + label: Question Type + description: What kind of question is this? + options: + - Usage/API question + - Behavior clarification + - Theory/algorithm question + - Build/installation question + - Documentation gap + - Design/architectural question + validations: + required: true + + - type: textarea + id: question + attributes: + label: Question + description: What would you like to know? + placeholder: I'm trying to understand why Z3 behaves differently when... + validations: + required: true + + - type: textarea + id: context + attributes: + label: Context + description: Provide relevant background about what you're trying to achieve + placeholder: | + I'm working on... + My goal is to... + I expected... but saw... + + - type: textarea + id: example + attributes: + label: Example (if applicable) + description: If relevant, provide a minimal example that illustrates your question + placeholder: | + (set-logic QF_LIA) + (declare-fun x () Int) + (assert (> x 0)) + (check-sat) + ; Why does this return sat instead of unsat? + render: smt2 + + - type: input + id: version + attributes: + label: Z3 Version + description: What version are you using? + placeholder: Z3 version 4.13.0 - 64 bit + + - type: textarea + id: research-done + attributes: + label: Research Done + description: What have you already tried or looked at? + placeholder: | + I checked the documentation at... + I searched for similar questions and found... + I tried using the following approaches... + + - type: checkboxes + id: question-check + attributes: + label: Question Guidelines + description: Please confirm + options: + - label: This is specific to Z3's behavior/design and not a general SMT question + required: true + - label: I searched existing issues and discussions for similar questions + required: true + - label: I considered whether Stack Overflow or GitHub Discussions might be more appropriate + required: true + + - type: markdown + attributes: + value: | + ### Alternative places for questions: + + - 💬 **[GitHub Discussions](../../discussions)** - For open-ended discussions about Z3 usage, best practices, and community Q&A + - 📚 **[Stack Overflow (z3 tag)](https://stackoverflow.com/questions/tagged/z3)** - For specific programming questions with Z3 APIs + - 📖 **[Z3 Guide](https://microsoft.github.io/z3guide/)** - For tutorials and comprehensive documentation + - 📝 **[Z3 API Documentation](https://z3prover.github.io/api/html/index.html)** - For API reference + + Questions asked here should ideally lead to: + - Documentation improvements + - Bug reports (if the behavior is unexpected) + - Feature requests (if functionality is missing) \ No newline at end of file diff --git a/.github/ISSUE_TEMPLATE/05-build-installation.yml b/.github/ISSUE_TEMPLATE/05-build-installation.yml new file mode 100644 index 000000000..f31aa201f --- /dev/null +++ b/.github/ISSUE_TEMPLATE/05-build-installation.yml @@ -0,0 +1,160 @@ +name: 🔧 Build/Installation Issue +description: Report problems with building or installing Z3 +title: "[Build] " +labels: ["build/release"] +body: + - type: markdown + attributes: + value: | + Thank you for reporting a build or installation issue! + + - type: dropdown + id: build-type + attributes: + label: Build/Installation Method + description: How are you trying to build or install Z3? + options: + - Building from source (CMake) + - Building from source (Python scripts) + - pip install z3-solver + - Package manager (apt, brew, vcpkg, etc.) + - Pre-built binaries from releases + - Building language bindings (Java, .NET, OCaml) + - Other + validations: + required: true + + - type: dropdown + id: platform + attributes: + label: Platform + description: What platform are you building on? + options: + - Linux (Ubuntu/Debian) + - Linux (RedHat/CentOS/Fedora) + - Linux (other distribution) + - macOS (Intel) + - macOS (Apple Silicon) + - Windows (MSVC) + - Windows (MinGW/MSYS2) + - Windows (Cygwin) + - Other Unix-like system + - Other + validations: + required: true + + - type: textarea + id: description + attributes: + label: Issue Description + description: Describe what went wrong during build/installation + placeholder: The build fails with error... / Installation doesn't work because... + validations: + required: true + + - type: textarea + id: build-commands + attributes: + label: Build Commands + description: Show the exact commands you used + placeholder: | + mkdir build + cd build + cmake .. + make + render: bash + validations: + required: true + + - type: textarea + id: error-output + attributes: + label: Error Output + description: Paste the complete error message or build failure output + placeholder: | + -- Configuring done + CMake Error: ... + make: *** [target] Error 1 + render: text + validations: + required: true + + - type: textarea + id: system-info + attributes: + label: System Information + description: Provide details about your build environment + placeholder: | + OS: Ubuntu 22.04 + Compiler: gcc 11.4.0 + CMake: 3.22.1 + Python: 3.10.12 + Java: OpenJDK 11.0.16 (if building Java bindings) + value: | + **Operating System:** + **Compiler:** + **CMake version:** + **Python version:** + **Other relevant tools:** + validations: + required: true + + - type: textarea + id: cmake-options + attributes: + label: CMake Configuration (if applicable) + description: What CMake options or configuration did you use? + placeholder: | + cmake -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_PYTHON_BINDINGS=ON .. + render: bash + + - type: textarea + id: dependencies + attributes: + label: Dependencies + description: What dependencies do you have installed? Any missing? + placeholder: | + Installed: build-essential, cmake, python3-dev + Missing: Not sure what's missing + + - type: textarea + id: workarounds + attributes: + label: Workarounds Tried + description: What have you tried to fix this issue? + placeholder: | + - Tried different CMake options + - Reinstalled dependencies + - Checked similar issues + + - type: checkboxes + id: build-info + attributes: + label: Additional Information + description: Help us understand your build environment + options: + - label: This worked in a previous version of Z3 + required: false + - label: This is a fresh/clean build (not incremental) + required: false + - label: I can provide more detailed logs if needed + required: false + + - type: textarea + id: additional-context + attributes: + label: Additional Context + description: Any other relevant information (Docker, CI environment, cross-compilation, etc.) + + - type: markdown + attributes: + value: | + ### Before submitting + - [ ] I searched existing build-related issues + - [ ] I provided the complete error output + - [ ] I included my system/environment details + + ### Common build documentation: + - [CMake build instructions](https://github.com/Z3Prover/z3/blob/master/README-CMake.md) + - [Main README](https://github.com/Z3Prover/z3/blob/master/README.md) + - [Python API installation](https://pypi.org/project/z3-solver/) \ No newline at end of file diff --git a/.github/ISSUE_TEMPLATE/06-other.yml b/.github/ISSUE_TEMPLATE/06-other.yml new file mode 100644 index 000000000..69a46b220 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/06-other.yml @@ -0,0 +1,65 @@ +name: 📋 Other Issue +description: For issues that don't fit other categories +title: "[Other] " +labels: [] +body: + - type: markdown + attributes: + value: | + Please use this template only if your issue doesn't fit any of the other specific categories. + + Consider whether your issue might be: + - **Bug Report** - Z3 crashes, gives wrong results, or behaves unexpectedly + - **Performance Issue** - Z3 is slower than expected or uses too much memory + - **Feature Request** - You need functionality that doesn't exist yet + - **Build/Installation** - Problems compiling or installing Z3 + - **Question** - You need help understanding Z3's behavior + + - type: dropdown + id: issue-category + attributes: + label: Issue Category + description: What type of issue is this? + options: + - Documentation problem + - Website/repository maintenance + - Security concern + - License question + - Community/governance + - CI/Testing infrastructure + - Release process + - Other (please specify) + validations: + required: true + + - type: textarea + id: description + attributes: + label: Description + description: Please describe your issue in detail + validations: + required: true + + - type: textarea + id: context + attributes: + label: Context + description: Additional context that might be helpful + placeholder: | + Related documentation: + Affected pages/sections: + Relevant links: + + - type: textarea + id: proposed-solution + attributes: + label: Proposed Solution (if any) + description: If you have ideas on how to address this issue + + - type: markdown + attributes: + value: | + ### Before submitting + - [ ] I confirmed this doesn't fit other issue categories + - [ ] I searched for existing similar issues + - [ ] I provided sufficient detail for maintainers to understand the issue \ No newline at end of file diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml new file mode 100644 index 000000000..2dc37611d --- /dev/null +++ b/.github/ISSUE_TEMPLATE/config.yml @@ -0,0 +1,17 @@ +blank_issues_enabled: false +contact_links: + - name: 💬 GitHub Discussions + url: https://github.com/Z3Prover/z3/discussions + about: For general questions, usage help, and community discussions + - name: 📚 Stack Overflow + url: https://stackoverflow.com/questions/tagged/z3 + about: For specific programming questions and code examples with Z3 APIs + - name: 📖 Z3 Guide + url: https://microsoft.github.io/z3guide/ + about: Comprehensive tutorials and documentation for learning Z3 + - name: 📝 API Documentation + url: https://z3prover.github.io/api/html/index.html + about: Complete API reference for all Z3 language bindings + - name: 🔬 Z3 Theory and Research + url: https://theory.stanford.edu/~nikolaj/programmingz3.html + about: Academic resources and theory behind Z3's algorithms \ No newline at end of file