Merge pull request #53 from elsoroka/documentation-fixes

Update issue templates

.github/ISSUE_TEMPLATE/bug_report.md

@@ -0,0 +1,28 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: "[BUG]"
+labels: ''
+assignees: ''
+
+---
+
+**Describe the bug**
+A clear and concise description of what the bug is.
+
+**Please provide the steps to reproduce the bug, including a minimal code demo if possible.**
+
+
+**What is the expected behavior?**
+
+
+**Please tell us about your environment.**
+  A simple way to do this: open Julia and type
+  ```
+  using InteractiveUtils
+  versioninfo()
+  ```
+  Paste the output of `versioninfo()` into your bug report.
+
+
+**Other information** (e.g. detailed explanation, stacktraces, related issues, suggestions on how to fix it)

.github/ISSUE_TEMPLATE/feature_request.md

@@ -0,0 +1,15 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**If this request is about a new feature, please describe what you would like to see implemented.**
+
+**If this request is about an existing feature, what is the current behavior and what is the use case for changing the behavior?**
+
+**Additional context**
+Add any other context or screenshots about the feature request here.

README.md

@@ -50,13 +50,26 @@ An uninterpreted function is a function where the input-to-output mapping isn't
 @satvariable(y, Bool)
 @uninterpreted(f, Bool, Bool)
 
-# Yices requires setting the logic manually. Here we set it to "QF_UFLIA" - "Quantifier free uninterpreted functions, linear integer arithmetic".
-status = sat!(distinct(x,y), f(x) == y, f(f(x)) == x, solver=Yices(), logic="QF_UFLIA")
-println("status = \$status")
+status = sat!(distinct(x,y), f(x) == y, f(f(x)) == x, solver=Z3())
+println("status = $status")
 ```
 
 The problem is `:SAT`, so there is such a function! Since the satisfying assignment for an uninterpreted function is itself a function, Satisfiability.jl sets the value of `f` to this function. Now calling `f(value)` returns the value of this satisfying assignment.
 
+### Using a different solver
+Now let's suppose we want to use Yices, another SMT solver. Unlike Z3, Yices requires setting the logic manually. Here we set it to "QF_UFLIA" - "Quantifier free uninterpreted functions, linear integer arithmetic".
+
+```julia
+@satvariable(x, Bool)
+@satvariable(y, Bool)
+@uninterpreted(f, Bool, Bool)
+
+status = sat!(distinct(x,y), f(x) == y, f(f(x)) == x, solver=Yices(), logic="QF_UFLIA")
+println("status = $status")
+```
+
+We see this yields the same result.
+
 ```julia
 println(f(x.value))               # prints 0
 println(f(x.value) == y.value)    # true
@@ -76,4 +89,7 @@ println(status) # if status is UNSAT we proved it.
 ```
 
 ## Development status
-Release 0.1.1 is out! You can install it with the command `using Pkg; Pkg.add("Satisfiability")`. Please help make the Julia ecosystem better for everyone by opening a GitHub issue if you have feedback or find a bug.
+Release 0.1.2 is out! You can install it with the command `using Pkg; Pkg.add("Satisfiability")`. Please help make the Julia ecosystem better for everyone by opening a GitHub issue if you have feedback or find a bug.
+
+## Contributing
+Contribution guidelines are [here](https://elsoroka.github.io/Satisfiability.jl/dev/contributing/). If you're not sure how to get started, take a look at the [Roadmap](https://github.com/elsoroka/Satisfiability.jl/issues/46) and anything tagged [help wanted](https://github.com/elsoroka/Satisfiability.jl/issues?q=is%3Aissue+is%3Aopen+label%3A%22help+wanted%22).

docs/make.jl

@@ -34,6 +34,7 @@ pages = [
         "Library" => [
         "functions.md"
         ],
+        "contributing.md",
         "release_notes.md"
     ],
 format=fmt,

docs/src/contributing.md

@@ -0,0 +1,16 @@
+# Contributing
+
+You can contribute to Satisfiability.jl! (Yes, even if you've never made an open source contribution before.)
+
+## Getting started
+* Please make sure to follow the [Julia community standards](https://julialang.org/community/standards) in all interactions.
+* Here's a [guide to making your first pull request](https://docs.github.com/en/get-started/exploring-projects-on-github/contributing-to-a-project)
+* Here's some more Julia-specific tips by Katharine Hyatt on [Making your first Julia pull request](https://kshyatt.github.io/post/firstjuliapr/).
+* If you're not sure how to fix the bug or add the feature you're interested in (or not sure how it fits into our roadmap), **start an issue to discuss it**.
+
+## What should I work on?
+If you want to contribute, but aren't sure where to begin:
+
+* Look for issues tagged [good first issue](https://github.com/elsoroka/Satisfiability.jl/labels/good%20first%20issue).
+
+* Help add more examples to our [documentation](https://elsoroka.github.io/Satisfiability.jl/dev/) or improve the documentation itself.

docs/src/installation.md

@@ -4,48 +4,62 @@ Pages = ["installation.md"]
 Depth = 3
 ```
 
-**NOTE: To successfully use this package you will need to install a back-end solver.** [Z3](https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/) and [cvc5](https://cvc5.github.io/) are currently supported. You should be able to [use other solvers](advanced.md#Custom-solver-options-and-using-other-solvers) as long as they implement the SMT-LIB standard.
+**NOTE: To successfully use this package you need a back-end solver installed.** [Z3](https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/) will automatically be installed using `z3_jll`.
+
+You can also use [cvc5](https://cvc5.github.io/) (although you will have to install it yourself). To use other solvers that implement the SMT-LIB standard, [check this page](advanced.md#Custom-solver-options-and-using-other-solvers) for guidelines.
 
 ## Installing Satisfiability
 The usual way! `using Pkg; Pkg.add("Satisfiability")`
+Satisfiability will automatically install Z3 on your system if it isn't already installed.
 
-## Installing a Solver
-Satisfiability uses Julia's Base.Process library to interact with solvers. Thus to successfully install a solver for this package, all you need to do is make sure the appropriate command works in your machine's terminal.
+## Installing other Solvers
+Satisfiability uses Julia's Base.Process library to interact with solvers. To successfully install a solver for this package, all you need to do is make sure the appropriate command works in your machine's terminal.
 
 ### Debian Linux
-**To install Z3**, use `sudo apt-get install z3`.
-If you can launch Z3 from the command line by typing `z3 -smt2 -in`, your installation is correct.
 
 **To install CVC5:**
 * Download the appropriate binary [here](https://cvc5.github.io/downloads.html) and save it as `cvc5`. (Note: if you already have `cvc5` installed under the name `cvc5-linux`, make a symlink to the name `cvc5` or [customize your solver command](advanced.md#Custom-solver-options-and-using-other-solvers) to use the name `cvc5-linux`.)
 * Set the executable permission: `chmod +x ./cvc5`.
 * Most users should move the binary to `/usr/local/bin`. This allows it to be found from the command line.
 If you can launch CVC5 from the command line by typing `cvc5 --interactive --produce-models`, your installation is correct.
 
+**To install Z3 manually** (you shouldn't need to do this), use `sudo apt-get install z3`.
+If you can launch Z3 from the command line by typing `z3 -smt2 -in`, your installation is correct.
+
 ### MacOS
-**To install Z3**
-* Download the appropriate zip file for the [latest Z3 release](https://github.com/Z3Prover/z3/releases) and install following the instructions on that page.
-* If you can open your Terminal and launch z3 by typing `z3 -smt2 -in`, your installation is correct.
 
 **To install CVC5**
 * Download the appropriate binary [here](https://cvc5.github.io/downloads.html) and save it as `cvc5`. (Note: if you already have `cvc5` installed under another name, make a symlink to the name `cvc5` or [customize your solver command](advanced.md#Custom-solver-options-and-using-other-solvers) to use the name you already have.)
 * Most users should move the binary to `/usr/local/bin`. This allows it to be found from the command line.
 * If you can open your Terminal and launch CVC5 by typing `cvc5 --interactive --produce-models`, your installation is correct.
 
+
+**To install Z3 manually** (you shouldn't need to do this):
+
+* `brew install z3` should work if you have Homebrew installed.
+
+Alternatively:
+
+* Download the appropriate zip file for the [latest Z3 release](https://github.com/Z3Prover/z3/releases) and install following the instructions on that page.
+* If you can open your Terminal and launch z3 by typing `z3 -smt2 -in`, your installation is correct.
+
+
 ### Windows
-**To install Z3**
-* Download the appropriate zip file for the [latest Z3 release](https://github.com/Z3Prover/z3/releases).
-* Unzip the file and put it in your applications folder.
-* Find z3.exe. Typically this will be in a bin file in your unzipped folder. Don't move it, but make a note of this file path.
-* Add the z3.exe file path to your PATH environment variable ([here's how to do this](https://helpdeskgeek.com/windows-10/add-windows-path-environment-variable/)).
-If you can open the WIndows command line and launch z3 by typing `z3.exe -smt2 -in`, your installation is correct.
 
 **To install cvc5**
 * Download the [latest release](https://github.com/cvc5/cvc5/releases/) of cvc5. Make sure you save the exe file as `cvc5.exe`, not `cvc5-Win64.exe` or anything else.
 * Make a note of the file path where you put cvc5.exe.
 * Add the cvc5.exe file path to your PATH environment variable ([here's how to do this](https://helpdeskgeek.com/windows-10/add-windows-path-environment-variable/)).
 If you can open the Windows command line and launch cvc5 by typing `cvc5 --interactive --produce-models`, your installation is correct.
 
+**To install Z3 manually** (you shouldn't need to do this):
+* Download the appropriate zip file for the [latest Z3 release](https://github.com/Z3Prover/z3/releases).
+* Unzip the file and put it in your applications folder.
+* Find z3.exe. Typically this will be in a bin file in your unzipped folder. Don't move it, but make a note of this file path.
+* Add the z3.exe file path to your PATH environment variable ([here's how to do this](https://helpdeskgeek.com/windows-10/add-windows-path-environment-variable/)).
+If you can open the WIndows command line and launch z3 by typing `z3.exe -smt2 -in`, your installation is correct.
+
+
 ### Installing Yices
 Please follow the [official instructions](https://yices.csl.sri.com/).
 

docs/src/release_notes.md

@@ -3,6 +3,10 @@
 Pages = ["release_notes.md"]
 Depth = 3
 ```
+
+# Version 0.1.3 (May 23, 2024)
+* Automatically download Z3 using `z3_jll` when Satisfiability.jl is installed.
+
 # Version 0.1.1 (December 15, 2023)
 * Fixed bugs in issues #21 and #26.
 * Added remaining operators defined in SMT-LIB QF_BV (bitvector) specification (issue #22)