Skip to content

Commit 1c89bd4

Browse files
committed
Update README.md with how to install at least one solver (Closes #164)
1 parent 062100a commit 1c89bd4

File tree

1 file changed

+22
-0
lines changed

1 file changed

+22
-0
lines changed

README.md

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,28 @@ Then install encoding:
2323
opam install smtml
2424
```
2525

26+
### Installing a Solver
27+
28+
Smt.ml uses optional dependencies (known as `depopts` in opam) to integrate
29+
with different SMT solvers. By default, Smt.ml installs without a solver, but
30+
you can enable support for a specific solver by installing it with opam.
31+
For example, to install smtml with Z3:
32+
33+
```sh
34+
opam install smtml z3
35+
```
36+
37+
Alternatively, if you've already installed Smt.ml through opam, you can simply
38+
install the solver of your choice and opam will recompile smtml for you.
39+
For example, to install Z3 after installing smtml:
40+
41+
```sh
42+
opam install z3
43+
```
44+
45+
See the [Supported Solvers](#supported-solvers) section below for a complete
46+
list of available solvers.
47+
2648
### Build from source
2749

2850
Clone the repo and install the dependencies:

0 commit comments

Comments
 (0)