Tools for quantifier elimination in linear integer arithmetic
-
13-06-2021 - |
Domanda
Are there any other available (and still supported) SMT tools that perform quantifier elimination for linear integer arithmetic besides Z3?
Thanks.
Soluzione
You can try Princess, by Philipp Rümmer. It supports quantifier-elimination and is actively maintained.
Autorizzato sotto: CC-BY-SA insieme a attribuzione
Non affiliato a StackOverflow