From 4a1a19b72a7cc8fa2f84fc784113ae823b98eeb0 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 3 Oct 2022 23:05:12 +0200 Subject: [PATCH] update Readme with new solver CVC5. --- README.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index cc55ee0ae9..13b717ae29 100644 --- a/README.md +++ b/README.md @@ -60,8 +60,9 @@ Currently JavaSMT supports several SMT solvers (see [Getting Started](doc/Gettin | --- |:---:|:---:|:---:|:--- | | [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: | | | | +| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | new! | | [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | | | -| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | same as MathSAT5, but with support for optimization | +| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | based on MathSAT5, with support for optimization | | [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | | [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver | | [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | [soon](https://github.com/sosy-lab/java-smt/pull/215) | | | @@ -87,6 +88,7 @@ If something specific is missing, please [look for or file an issue](https://git | --- |:---:|:---:| | [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | :heavy_check_mark: | +| [CVC5](https://cvc4.github.io/) | :heavy_check_mark: | | | [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | | | [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | | @@ -95,10 +97,10 @@ If something specific is missing, please [look for or file an issue](https://git | [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | | Interruption using a [ShutdownNotifier][] may be used to interrupt a -a solver from any thread. +a solver from any thread. Formulas are translatable in between contexts/provers/threads using _FormulaManager.translateFrom()_. -¹ Multiple contexts, but all operations on each context only from a single thread. +¹ Multiple contexts, but all operations on each context only from a single thread. ² Multiple provers on one or more contexts, with each prover using its own thread. #### Garbage Collection in Native Solvers