System Announcement: EZSMT

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.