\myheading{List of SMT-solvers}

\leveldown{}

\begin{itemize}

\item Yices\footnote{\url{http://yices.csl.sri.com/}}, created by Bruno Dutertre et al.
Logics Yices 2.6.2 supports\footnote{Grep'ed from its test suite}:

ALL, BV, LIA, LRA, QF\_ABV, QF\_ALIA, QF\_ALIRA, QF\_AUFBV, QF\_AUFLIA, QF\_AUFLIRA, QF\_BV, QF\_IDL,
QF\_LIA, QF\_LIRA, QF\_LRA, QF\_NIA, QF\_NIRA, QF\_NRA, QF\_RDL, QF\_UF, QF\_UFBV, QF\_UFIDL,
QF\_UFLIA, QF\_UFLRA, QF\_UFNIA, QF\_UFNRA, UF.

\item Z3\footnote{\url{https://github.com/Z3Prover/z3}},
developed by Leonardo de Moura, Nikolaj Bjorner, Christoph M. Wintersteiger, Lev Nachmanson.
Has its own state-of-art SAT solver.

Many examples here uses Python 2.x API for Z3 (AKA Z3Py).
Installation instructions (Ubuntu):

\begin{lstlisting}
sudo apt-get install python3-pip
sudo pip3 install z3-solver
\end{lstlisting}

Or compile the latest on Ubuntu:

\begin{lstlisting}
git clone https://github.com/Z3Prover/z3.git
cd z3
git tag
git checkout z3-4.12.0	# or newer version
python3 scripts/mk_make.py --python
cd build
make -j8
sudo make install
\end{lstlisting}

Python modules goes to \verb|/usr/lib/python3.x/site-packages/z3|.
If you have trouble with this, you can install Python modules to your \verb|$HOME|:

\begin{lstlisting}
python3 scripts/mk_make.py --prefix=$HOME --python --pypkgdir=$HOME/.local/lib/python3.8/site-packages
\end{lstlisting}

(Unofficial) bindings:
Haskell\footnote{\url{http://hackage.haskell.org/package/z3}, \url{http://leventerkok.github.io/sbv/}},
Racket\footnote{\url{https://github.com/philnguyen/z3-rkt}, \url{https://github.com/sunshowers/z3.rkt}},
Rust\footnote{\url{https://github.com/prove-rs/z3.rs}}.

Fun story: \href{https://www.cs.utexas.edu/~bornholt/post/z3-iphone.html}{SMT Solving on an iPhone}.

The first version of solver was called 'Zapatho', the second 'Zap2', the third 'Z3'\footnote{
\url{https://github.com/Z3Prover/z3/issues/2321},
\url{https://stackoverflow.com/questions/49963012/what-is-the-meaning-of-the-name-of-the-z3-smt-solver}}
Go figure how the fourth and fifth versions would be called.

Logics Z3 4.8.x supports\footnote{Grep'ed from its test suite}:

ABV, ALL, AUFBV, AUFLIA, AUFNIRA, BV, HORN, LIA, NRA, QF\_AUFLIA, QF\_AUFLIRA, QF\_BV, QF\_BVFP, QF\_FD, QF\_FP,
QF\_FP, QF\_FPA, QF\_FPBV, QF\_IDL, QF\_LIA, QF\_LRA, QF\_NIA, QF\_NRA, QF\_NRA, QF\_RDL, QF\_S, QF\_UF, QF\_UFBV,
QF\_UFLIA, UFBV, UFLIA.

\item STP\footnote{\url{https://github.com/stp/stp}}, used in KLEE.

Logics STP 2.3.3 supports\footnote{Grep'ed from its test suite}:
QF\_ABV, QF\_AUFBV, QF\_BV.

\item CVC3/CVC4\footnote{\url{http://cvc4.stanford.edu/} AKA \textit{A Cooperating Validity Checker},
Also available online: \url{https://cvc4.github.io/app/},
See also: \url{http://cvc4.cs.stanford.edu/wiki/}.}.

Newest version is CVC5: \url{https://github.com/cvc5/cvc5}.

Logics CVC 1.9 supports\footnote{Grep'ed from its test suite}:

ABV, ALL, ALL\_SUPPORTED, ASLIA, AUFBV, AUFBVDTLIRA, AUFBVDTNIRA, AUFDTLIA, AUFLIA, AUFLIAFS, AUFLIRA, AUFNIA, AUFNIRA, BV,
FP, LIA, LIRA, LRA, NIA, NIRA, NIRAT, NRA, QF\_ABV, QF\_ALIA, QF\_ALL, QF\_ALL\_SUPPORTED, QF\_ANIA,
QF\_AUF, QF\_AUFBV, QF\_AUFBVLIA, QF\_AUFBVLRA, QF\_AUFLIA, QF\_AUFLIRA, QF\_AUFNIA, QF\_AUFNIRA, QF\_AUFNRA, QF\_AX,
QF\_BV, QF\_BVDTLIAFS, QF\_BVFP, QF\_BVFS, QF\_BVLIA, QF\_DT, QF\_DTLIA, QF\_FP, QF\_FPLRA, QF\_IDL, QF\_LIA, QF\_LIRA,
QF\_LIRAFS, QF\_LRA, QF\_NIA, QF\_NIRA, QF\_NRA, QF\_NRAT, QF\_RDL, QF\_S, QF\_SAT, QF\_SEP\_LIA, QF\_SLIA, QF\_UF, QF\_UFBV,
QF\_UFBVFS, QF\_UFC, QF\_UFDTLIA, QF\_UFIDL, QF\_UFLIA, QF\_UFLIAFS, QF\_UFLIRA, QF\_UFLIRAFS, QF\_UFLRA, QF\_UFLRAFS, QF\_UFNIA,
QF\_UFNIRA, QF\_UFNRA, QF\_UFNRAT, QF\_UFSLIA, SAT, SLIA, UF, UFBV, UFC, UFDT, UFDTLIA, UFDTLIRA, UFDTSLIA, UFFS, UFIDL,
UFLIA, UFLIRA, UFNIA, UFNIRA, UFNRAT.

\item Boolector\footnote{\url{http://fmv.jku.at/boolector/}}, developed by Aina Niemetz, Mathias Preiner and Armin Biere.
Known as the fastest bitvector solver.

Logics Boolector 3.2.1 supports:
BV, QF\_ABV, QF\_AUFBV, QF\_BV, QF\_UFBV.

\item Alt-Ergo\footnote{\url{https://alt-ergo.ocamlpro.com/}}, used in Frama-C.

\item MathSAT\footnote{\url{http://mathsat.fbk.eu/}}. Developed by Alberto Griggio, Alessandro Cimatti and Roberto Sebastiani.

Logics MathSAT 5.6.5 supports:

QF\_ABV, QF\_ALIA, QF\_AUFBV, QF\_AUFLIA, QF\_AX, QF\_BV, QF\_BVFP, QF\_FP, QF\_FPBV, QF\_LIA, QF\_LRA,
QF\_UF, QF\_UFBV, QF\_UFLIA, QF\_UFLRA.

\item veriT\footnote{\url{http://www.verit-solver.org/}}.
Developed by David Déharbe, Pascal Fontaine, Haniel Barbosa.
Lacks bitvectors.

\item toysolver\footnote{\url{https://github.com/msakai/toysolver}} by Masahiro Sakai, written in Haskell.

\item MK85\footnote{\url{https://smt.st/MK85/}}.
Created by the author, as a toy bit-blaster, supports only booleans and bitvectors.

\item dReal: ``An SMT Solver for Nonlinear Theories of the Reals''
\footnote{\url{http://dreal.cs.cmu.edu}, \url{https://github.com/dreal}}.

\end{itemize}

Something else:

\begin{itemize}

\item PySMT: unified Python interface to many SMT solvers
\footnote{\url{https://pysmt.readthedocs.io/en/latest/},
\url{https://github.com/pysmt/pysmt},
\url{http://smt2015.csl.sri.com/wp-content/uploads/2015/06/2015-Gario-Micheli-PySMT-a-Solver-Agnostic-Library-for-Fast-Prototyping-of-SMT-Based-Algorithms.pdf}
\url{http://fmv.jku.at/avm15/slides/gario.pdf}}.

\item JavaSMT -- Unified Java API for SMT solvers: \url{https://github.com/sosy-lab/java-smt}

\item jSMTLIB -- Another Java API for SMT solvers: \url{http://smtlib.github.io/jSMTLIB/}

\item SBV: SMT Based Verification in Haskell: \url{http://leventerkok.github.io/sbv/}

\end{itemize}

\myheading{Boolector}

Boolector can generate CNF file instead of handing it out to SAT solver:

\begin{lstlisting}
boolector --smt2 --dump-dimacs filename.smt > filename.cnf
\end{lstlisting}

Just keep in mind that if Boolector calls a SAT solver several times, all these CNFs would be dumped to stdout, like:

\begin{lstlisting}
c CNF dump 1 start
c Boolector version
p cnf 13325 36769
1 0
2 0

...

-13325 0
c CNF dump 1 end
c CNF dump 2 start
c Boolector version
p cnf 15421 40065
1 0
2 0

...

15421 0
c CNF dump 2 end
c CNF dump 3 start
c Boolector version
p cnf 15488 40267
1 0
2 0
...
\end{lstlisting}

This is useful: you can try other SAT solvers, proof checkers, etc...

\levelup{}