Merge pull request #67 from elsoroka/main

merge main INTO joss-paper but I don't think this is necessary

.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.

.github/workflows/ci.yml

@@ -14,21 +14,24 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@master
-      
+
       - name: Setup z3
         run: sudo apt-get -y install z3
-
+
+      - name: Setup Yices
+        run: sudo add-apt-repository ppa:sri-csl/formal-methods; sudo apt-get update; sudo apt-get install yices2
+
       - name: Set up Julia latest version
         uses: julia-actions/setup-julia@latest
-      - uses: julia-actions/cache@v1
-      
+      - uses: julia-actions/cache@v2
+
       - name: Run tests
         uses: julia-actions/julia-buildpkg@v1
       - uses: julia-actions/julia-runtest@v1
       - uses: julia-actions/julia-processcoverage@v1
       - name: Upload coverage reports to Codecov
-        uses: codecov/codecov-action@v4 
+        uses: codecov/codecov-action@v4
         env:
           CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}
         with:
-          file: lcov.info  # https://github.com/julia-actions/julia-processcoverage
+          file: lcov.info # https://github.com/julia-actions/julia-processcoverage

.github/workflows/docs.yml

@@ -16,8 +16,10 @@ jobs:
       steps:
         - name: Setup z3
           run: sudo apt-get -y install z3
+        - name: Setup Yices
+          run: sudo add-apt-repository ppa:sri-csl/formal-methods; sudo apt-get update; sudo apt-get install yices2
         - uses: actions/checkout@v4
-        - uses: julia-actions/cache@v1
+        - uses: julia-actions/cache@v2
         - uses: julia-actions/julia-buildpkg@v1
         - uses: julia-actions/julia-docdeploy@v1
           env:

.github/workflows/draft-pdf.yml

@@ -14,7 +14,7 @@ jobs:
           # This should be the path to the paper within your repo.
           paper-path: joss-paper/paper.md
       - name: Upload
-        uses: actions/upload-artifact@v1
+        uses: actions/upload-artifact@v4
         with:
           name: paper
           # This is the output path where Pandoc will write the compiled

Project.toml

@@ -1,10 +1,11 @@
 name = "Satisfiability"
 uuid = "160ab843-0bc6-4ba4-9585-b7478b70f443"
 authors = ["Emi Soroka <[email protected]>, Mykel Kochenderfer, Sanjay Lall"]
-version = "0.1.1"
+version = "0.2.0"
 
 [compat]
 julia = "1"
+z3_jll = "4.13"
 
 [extras]
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
@@ -14,3 +15,5 @@ test = ["Test"]
 
 [deps]
 Logging = "56ddb016-857b-54e1-b83d-db4d58db5568"
+z3_jll = "1bc4e1ec-7839-5212-8f2f-0d16b7bd09bc"
+Unicode = "4ec0a83e-493e-50e2-b9ac-8f72acf5a8f5"

README.md

@@ -16,11 +16,12 @@ You can read the documentation [here](https://elsoroka.github.io/Satisfiability.
 ### Solving the vector-valued Boolean problem
 (x1 ∧ y1) ∨ (¬x1 ∧ y1) ∧ ... ∧ (xn ∧ yn) ∨ (¬xn ∧ yn)
 ```julia
+n = 10
 @satvariable(x[1:n], Bool)
 @satvariable(y[1:n], Bool)
 expr = (x .∧ y) .∨ (¬x .∧ y)
 status = sat!(expr, solver=Z3())
-println("x = $(value(x)), y = $(value(y))”)
+println("x = $(value(x)), y = $(value(y))")
 ```
 
 ### Investigating rounding of real numbers
@@ -49,18 +50,28 @@ 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")
+
 println(f(x.value))               # prints 0
 println(f(x.value) == y.value)    # true
 println(f(f(x.value)) == x.value) # true
 ```
+We see this yields the same result.
 
 ### Proving a bitwise version of de Morgan's law.
 In this example we want to show there is NO possible value of x and y such that de Morgan's bitwise law doesn't hold.
@@ -75,4 +86,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

@@ -7,12 +7,11 @@ using Satisfiability
 fmt = Documenter.Writers.HTMLWriter.HTML(edit_link="main")
 
 makedocs(sitename="Satisfiability.jl",
-#repo = Documenter.Remotes.GitHub("elsoroka", "Satisfiability.jl"),
 clean=true,
 draft=false,
-checkdocs=:none,
 source  = "src",
 workdir=pwd(),
+warnonly = Documenter.except(:doctest, :docs_block, :parse_error, :example_block, :linkcheck, :cross_references),
 modules = [Satisfiability],
 pages = [
         "index.md",
@@ -27,13 +26,15 @@ pages = [
         "Examples" => [
             "example_scheduling.md",
             "example_job_shop.md",
+            "example_bv_mini.md",
             "example_bv_lcg.md",
             "example_graph_coloring.md",
             "example_bad_assertions.md",
         ],
         "Library" => [
         "functions.md"
         ],
+        "contributing.md",
         "release_notes.md"
     ],
 format=fmt,

docs/src/advanced.md

@@ -50,7 +50,8 @@ If you just want to use an SMT solver interactively, for example by `push`ing or
 In the SMT-LIB specification, after entering a problem and issuing the command `(check-sat)` the solver will be in either `sat` or `unsat` mode. The solver mode determines which commands are valid: for example, `(get-unsat-core)` is only valid in `unsat` mode and `(get-model)` is only valid in `sat` mode. You can find descriptions of modes and listings of valid commands in the latest [SMT-LIB Standard](http://www.smtlib.org/).
 
 Here's an example.
-```julia
+```jldoctest; output = false
+using Satisfiability
 @satvariable(x[1:2], Bool)
 expr = (x[1] ∧ ¬x[1]) ∧ or(x) # unsat
 
@@ -71,6 +72,12 @@ println(response)
 
 # it's good form to clean up your open solver process
 close(interactive_solver)
+
+# output
+
+status = unsat
+
+()
 ```
 
 When using this functionality, you are responsible for keeping track of the solver mode and parsing the result of `send_command`. For convenience, `parse_model(model::String)` can parse the result of the SMT-LIB command `(get-model)`, returning a dictionary with variable names as keys and satisfying assignments as values.

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/example_bad_assertions.md

@@ -2,40 +2,41 @@
 In this problem we have some expressions we need to satisfy, and some that we would like to satisfy (but we can't satisfy them all).
 We want to figure out which expressions we can satisfy using push() and pop() to assert and remove them as necessary.
 
-```julia
+```jldoctest label1; output = false
 using Satisfiability
 @satvariable(x, Bool)
 @satvariable(y, Bool)
 @satvariable(z, Bool)
 necessary_exprs = or(and(not(x), y, z), and(not(y), x, z))
 
 interactive_solver = open(Z3())
-```
-We assert this at the first level, since we always have to have it.
-```julia
+
+# We assert this at the first level, since we always have to have it.
 assert!(interactive_solver, necessary_exprs)
+
+# output
+
+
 ```
 
 Here are some conflicting expressions. One of them is satisfiable when `necessary_exprs` is true; the others are not.
-```julia
+```jldoctest label1; output = false
 conflicting_exprs = [
     not(z),
     and(not(x), not(y)),
     not(x),
     and(x,y),
 ]
-```
 
-We'll use `push` and `pop` to add and remove them one at a time.
-```julia
+# We'll use `push` and `pop` to add and remove them one at a time.
+
 for e in conflicting_exprs
     # Push one assertion level on the stack
     push!(interactive_solver)
 
     # Now assert an expression that might make the problem unsatisfiable
     assert!(interactive_solver, e)
-    # Note: logic here is NONE meaning only propositional logic. This arises because we used Yices, which requires setting the logic.
-    status, assignment = sat!(interactive_solver, logic="NONE")
+    status, assignment = sat!(interactive_solver)
 
     if status == :SAT
         println("We found it! Expr \n$e \nis satisfiable.")
@@ -46,16 +47,28 @@ for e in conflicting_exprs
         pop!(interactive_solver)
     end
 end
+
+# output
+
+We found it! Expr 
+not_53b20e3050918288
+ | x
+ 
+is satisfiable.
 ```
 
 ### Another way to do this.
 Let's reset the solver so we can try another way to do the same thing. This command clears all assertions, including the first one we made at level 1.
-```julia
+```jldoctest label1
 reset_assertions!(interactive_solver)
+
+# output
+
+
 ```
 
 This time, we use `sat!(solver, exprs...)` which is equivalent to the SMT-LIB command `(check-sat-assuming exprs...)`. Thus the expression is not asserted but is assumed within the scope of the `sat!` call.
-```julia
+```jldoctest label1
 assert!(interactive_solver, necessary_exprs)
 # Here's an equivalent way to do this by passing exprs into sat!. This is equivalent to the SMT-LIB syntax "(check-sat-assuming (exprs...))", which does not (assert) the expressions but assumes they should be satisfied.
 for e in conflicting_exprs
@@ -70,4 +83,16 @@ end
 
 # We're done, so don't forget to clean up.
 close(interactive_solver)
+
+# output
+
+status = ERROR
+status = UNSAT
+status = SAT
+We found it! Expr 
+not_53b20e3050918288 = true
+ | x = false
+ 
+is satisfiable.
+status = UNSAT
 ```