From 92a8c6440104d59f51671bb26fedd52e33637385 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Sat, 8 Feb 2025 19:58:30 +0000 Subject: [PATCH] Update README.md with how to install at least one solver (Closes #164) --- README.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/README.md b/README.md index 4cf2578a..42cbb57c 100644 --- a/README.md +++ b/README.md @@ -23,6 +23,28 @@ Then install encoding: opam install smtml ``` +### Installing a Solver + +Smt.ml uses optional dependencies (known as `depopts` in opam) to integrate +with different SMT solvers. By default, Smt.ml installs without a solver, but +you can enable support for a specific solver by installing it with opam. +For example, to install smtml with Z3: + +```sh +opam install smtml z3 +``` + +Alternatively, if you've already installed Smt.ml through opam, you can simply +install the solver of your choice and opam will recompile smtml for you. +For example, to install Z3 after installing smtml: + +```sh +opam install z3 +``` + +See the [Supported Solvers](#supported-solvers) section below for a complete +list of available solvers. + ### Build from source Clone the repo and install the dependencies: