Tools for quantifier elimination in linear integer arithmetic

StackOverflow https://stackoverflow.com/questions/10961259

  •  13-06-2021
  •  | 
  •  

题

Are there any other available (and still supported) SMT tools that perform quantifier elimination for linear integer arithmetic besides Z3?

Thanks.

有帮助吗？

解决方案

You can try Princess, by Philipp Rümmer. It supports quantifier-elimination and is actively maintained.

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top