# \[ANN\] Satisfiability.jl: a simple interface to theorem provers using the SMT-LIB standard
**URL:** https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984
**Category:** Package Announcements
**Tags:** package, announcement
**Created:** [August 19, 2023, 4:38pm UTC](https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984 "2023-08-19T16:38:42Z")
**Posts on this page:** 5
**Page:** 1
### Author:  [@elsoroka](https://discourse.julialang.org/u/elsoroka)
#### Post date: [August 19, 2023, 4:38pm UTC](https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984/1 "2023-08-19T16:38:42Z")
[Satisfiability.jl](https://github.com/elsoroka/Satisfiability.jl) is a package for representing satisfiability modulo theories (SMT) problems in Julia.
SMT is used in formal verification and synthesis. You can use it to find satisfying assignments for logical statements (finding a set of values that make the statement true), or to prove that no satisfying assignment exists. More practically, you can verify software correctness (some good examples are in Chapter 5 of “SAT/SMT by Example”), find a set of inputs for which a system crashes, or prove your Amazon EC2 instance is secure (Amazon’s IAM access analyzer uses SMT).
**Satisfiability.jl is not a theorem prover.** It is a simple interface to existing provers (Z3, cvc5, etc) using the [SMT-LIB language](http://smtlib.cs.uiowa.edu/language.shtml). Currently, the theories of propositional logic, Integers, Reals and fixed-size BitVectors are supported. We plan to add support for the remaining SMT-LIB standard theories: IEEE floating points, Arrays, and Strings.
If you’re familiar with PySMT, Satisfiability.jl seeks to fill the same niche in the Julia ecosystem. Our inspirations for the package interface are JuMP and Convex.jl
## What Satisfiability.jl does
- Provides a high-level interface to specify single-valued or vector-valued SMT expressions using Julia’s built-in capabilities.
- Generates files in the SMT-LIB specification language.
- Interacts with any solver that follows the SMT-LIB standard.
## Examples
These are from the package documentation, linked in the respository!
### Proving a bitwise version of de Morgan’s law.
Verify there is NO possible value of x and y such that de Morgan’s bitwise law doesn’t hold.
```julia-auto
@satvariable(x, BitVector, 64)
@satvariable(y, BitVector, 64)
expr = not((~x & ~y) == ~(x | y))
status = sat!(expr, solver=Z3())
println(status) # if status is UNSAT we proved it.
```
### Investigating rounding of real numbers
We want to find out if there exists a constant `a` and two real numbers `xR` and `yR` such that `round(xR) + round(yR) > a` while `xR + yR < a`.
```julia-auto
@satvariable(xR, Real)
@satvariable(yR, Real)
@satvariable(x, Int) # x represents a rounded version of xR
@satvariable(y, Int) # y represents a rounded version of yR
@satvariable(a, Int)
exprs = [xR + yR < a,
x + y > a,
or(x == xR, ((x < xR) ∧ (xR < x+1)), ((x-1 < xR) ∧ (xR < x))),
or(y == yR, ((y < yR) ∧ (yR < y+1)), ((y-1 < yR) ∧ (yR < y))),
]
status = sat!(exprs)
println("status = $status, xR=$(value(xR)), yR=$(value(yR)), a = $(value(a))")
```
There are! We get `status = SAT, xR=0.666, yR=-0.834, a = 0`.
## Previous work in Julia SMT
- Z3.jl provides bindings of the Z3 C++ API
- PicoSAT.jl provides bindings to the PicoSAT solver (using CNF format).
- SatisfiabilityInterface.jl was presented at JuliaCon 2021. It’s for “modelling discrete constraint satisfaction problems and encoding them to Boolean satisfiability (SAT) problems.”
## Try it out!
I haven’t registered the package yet, so you can install it with `using Pkg; Pkg.add(url="https://github.com/elsoroka/Satisfiability.jl/")`
You’ll also need a back-end solver. Both Z3 and cvc5 are available for free; the package documentation has instructions to install them.
If you do try it I’d love to hear feedback, ideas, or any issues you encountered!
---
### Author:  [@elsoroka](https://discourse.julialang.org/u/elsoroka)
#### Post date: [August 19, 2023, 4:39pm UTC](https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984/2 "2023-08-19T16:39:55Z")
Since I’m a new developer, I would specifically like to solicit feedback on the name Satisfiability.jl. It meets the package name guidelines but I want to ask people’s opinions on it. Thank you!
---
### Author:  [@Sukera](https://discourse.julialang.org/u/Sukera)
#### Post date: [August 27, 2023, 8:10am UTC](https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984/3 "2023-08-27T08:10:31Z")
> [@elsoroka](#):
>
> [GitHub - elsoroka/Satisfiability.jl: Specify satisfiability modulo theories problems in Julia and use the SMT-LIB format to interact with SMT solvers.](https://github.com/elsoroka/Satisfiability.jl/)
Fantastic stuff! For all those folks who liked [PropCheck.jl](https://discourse.julialang.org/t/ann-propcheck-jl/101481) (which is just a fancy fuzzer), _this_ is the mathematically correct theorem proving counterpart!
Do you have plans for depending (weakly) on Z3.jl or other solvers like cvc5, so that users don’t have to install the solver through their system package manager and instead can just use a JLL from Pkg?
As for the name - I think it’s fine, since this is more or less an interface package. Kind of like Tables.jl is an interface package.
---
### Author:  [@elsoroka](https://discourse.julialang.org/u/elsoroka)
#### Post date: [August 28, 2023, 5:24pm UTC](https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984/4 "2023-08-28T17:24:49Z")
Thank you! I haven’t seen PropCheck before so I will make a note to add it to a list of related packages.
> Do you have plans for depending (weakly) on Z3.jl or other solvers like cvc5, so that users don’t have to install the solver through their system package manager and instead can just use a JLL from Pkg?
Other Languages’ SMT Packages ([PySMT](https://github.com/pysmt/pysmt)) do this! It’s a good thing to put on a roadmap. Z3.jl (there seem to be 2 but I’m familiar with [this one](https://github.com/ahumenberger/Z3.jl)) My main concern is it’s not well documented, so although I’ve used it I’m not confident in understanding it well enough to interface with it.
I use Base.process to talk with solvers but have had difficulty with pipes which I think is related to Julia issue [#24717](https://github.com/JuliaLang/julia/issues/24717) and the state of [two-way communication with long-lived external processes](https://discourse.julialang.org/t/avoiding-readavailable-when-communicating-with-long-lived-external-program/61611/16). So other ways to interface with solvers are a good idea, especially if they allow all the dependencies to be Pkg installed.
---
### Author:  [@Sukera](https://discourse.julialang.org/u/Sukera)
#### Post date: [August 28, 2023, 5:37pm UTC](https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984/5 "2023-08-28T17:37:29Z")
> [@elsoroka](#):
>
> Z3.jl (there seem to be 2 but I’m familiar with [this one](https://github.com/ahumenberger/Z3.jl)) My main concern is it’s not well documented, so although I’ve used it I’m not confident in understanding it well enough to interface with it.
As far as I can tell, Z3.jl is the only package providing a Julia interface - [z3\_jll](https://juliahub.com/ui/Packages/General/z3_jll) is just the [BinaryBuilder.jl](https://docs.binarybuilder.org/stable/jll/) provided binary, built in CI for all platforms Julia (and the binary dependency in question) supports.
According to its README, the package is mostly autogenerated bindings to the C++ library, with the same names & functions as the original library.
> [@elsoroka](#):
>
> I use Base.process to talk with solvers but have had difficulty with pipes which I think is related to Julia issue [#24717](https://github.com/JuliaLang/julia/issues/24717) and the state of [two-way communication with long-lived external processes](https://discourse.julialang.org/t/avoiding-readavailable-when-communicating-with-long-lived-external-program/61611/16). So other ways to interface with solvers are a good idea, especially if they allow all the dependencies to be Pkg installed.
I’m not sure which issue in the linked discourse thread you’re referring to exactly, but `readavailable` doesn’t read in everything by default - the default `IOStream` does some internal (hidden…) buffering, which is what `readavailable` ultimately returns. I haven’t heard anything about long lived external processes being particularly problematic themselves though.