System Announcement: EZSMT

EZSMT: SMT-based constraint answer set programming solver

By Yuliya Lierler, University of Nebraska, USA

https://www.unomaha.edu/college-of-information-science-and-technology/natural-language-processing-and-knowledge-representation-lab/software/ezsmt.php

 

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.