Package

# purescript-z3

Repository
gbagan/purescript-z3
MIT AND ISC
pacchettibotti
Published on
2023-05-07T15:55:35Z

PureScript FFI bindings for the Z3 theorem prover

### Documentation

Documentation is published on Pursuit

### Install

``````spago install z3
npm install z3-solver
``````

The npm repository is not up to date. Use the github repository to be able to use all features. https://github.com/Z3Prover/z3/tree/master/src/api/js

### Example

```sudoku :: Array Int
sudoku =
[ 0, 0, 0, 0, 9, 4, 0, 3, 0
, 0, 0, 0, 5, 1, 0, 0, 0, 7
, 0, 8, 9, 0, 0, 0, 0, 4, 0
, 0, 0, 0, 0, 0, 0, 2, 0, 8
, 0, 6, 0, 2, 0, 1, 0, 5, 0
, 1, 0, 2, 0, 0, 0, 0, 0, 0
, 0, 7, 0, 0, 0, 0, 5, 2, 0
, 9, 0, 0, 0, 6, 5, 0, 0, 0
, 0, 4, 0, 9, 7, 0, 0, 0, 0
]

for2_ :: ∀a b m. Applicative m ⇒ Array a → Array b → (a → b → m Unit) → m Unit
for2_ t1 t2 f = sequence_ (zipWith f t1 t2)

idx :: forall a. Array a -> Int -> a
idx t i = unsafePartial \$ unsafeIndex t i

solveSudoku :: Aff Unit
solveSudoku = Z3.run do
vars ← Z3.intVector 81
for2_ vars sudoku \var val → do
if val == 0 then do
Z3.assert \$ var `ge` 1
Z3.assert \$ var `le` 9
else
Z3.assert \$ var `eq` val

for_ (0..8) \i -> do
Z3.assert \$ Z3.distinct \$ (0..8) <#> \j -> idx vars (i * 9 + j)
Z3.assert \$ Z3.distinct \$ (0..8) <#> \j -> idx vars (j * 9 + i)
Z3.assert \$ Z3.distinct \$ (0..8) <#> \j -> idx vars (i / 3 * 27 + i `mod` 3 * 3 + j / 3 * 9 + j `mod` 3)

m ← Z3.withModel \$ flip Z3.eval vars
liftEffect \$ logShow m```

### Another example (Optimization)

```petersen :: Array (Tuple Int Int)
petersen =
[ 0 /\ 1, 1 /\ 2, 2 /\ 3, 3 /\ 4, 4 /\ 0
, 5 /\ 7, 7 /\ 9, 9 /\ 6, 6 /\ 8, 8 /\ 5
, 0 /\ 5, 1 /\ 6, 2 /\ 7, 3 /\ 8, 4 /\ 9
]

graphColoring :: Aff Unit
graphColoring = Z3.run do
res ← Z3.runOpt do
m ← Z3.int
colors ← Z3.intVector 10
for_ colors \c → do
Z3.assertAll [c `ge` 1, c `le` m]
for_ petersen \(u /\ v) →
Z3.assert \$ idx colors u `neq` idx colors v
Z3.minimize m
Z3.withModel (flip Z3.eval m)
liftEffect \$ logShow \$ m```

### More examples

https://github.com/gbagan/purescript-z3/blob/main/test/Main.purs

Modules
Z3
Z3.Internal
Z3.Types
Dependencies