EZSMT: SMT-based constraint answer set programming solver
By Yuliya Lierler, University of Nebraska, USA
EZSMT version 2.0 offers some unique features. For example, it can process nontight programs with constraints over mixed integer and real domains; over integers; and over reals. It also accepts some nonlinear constraints. Currently, it uses such SMT solvers as CVC4, Yices, and Z3 for search.
Also, a collection of benchmarks encoded in the language accepted by EZSMT is linked to the system’s website. The posted paper on EZSMT presents comparative analysis with other constraint answer set solvers.