provide more solver information on starting page.
@@ -49,13 +49,17 @@ JavaSMT can express formulas in the following theories:
- Uninterpreted Function
Currently JavaSMT support several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation):
- - [Boolector](https://boolector.github.io/)
- - [CVC4](https://cvc4.github.io/)
- - [MathSAT5](http://mathsat.fbk.eu/) and [OptiMathSAT](http://optimathsat.disi.unitn.it/)
- - [Princess](http://www.philipp.ruemmer.org/princess.shtml)
- - [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/)
- - [Yices2](https://yices.csl.sri.com/)
- - [Z3](https://github.com/Z3Prover/z3)
+
+| SMT Solver | Linux64 | Windows64 | MacOS | Description |
+| --- |:---:|:---:|:---:|:--- |
+| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | a fast solver for bitvector logic, misses formula introspection |
+| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | |
+| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | | |
+| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | same a MathSAT5, but with support for optimization |
+| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | |
+| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | |
+| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | [soon](https://github.com/sosy-lab/java-smt/pull/215) | | |
+| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
The following features are supported (depending on the used SMT solver):
@@ -69,6 +73,9 @@ The following features are supported (depending on the used SMT solver):
- Formula transformation using built-in tactics
- Formula introspection using visitors
+We aim for supporting more important features, more SMT solvers, and more systems.
+If something specific is missing, please [look for or file an issue](https://github.com/sosy-lab/java-smt/issues).
+
#### Multithreading Support
The solvers Z3(w and w/o Optimization), SMTInterpol, Princess, MathSAT5, Boolector and CVC4 support multithreading,
provided that different threads use different contexts,
