System Announcement: EZSMT

EZSMT: SMT-based constraint answer set programming solver


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.