EFSMT - A wrapper for solving exists-forall formulae


EFSMT is a prototypical C library for answering queries containing existential and universal variables with only one quantifier alternation. It is built on top of the Yices2 SMT solver (as a wrapper). The tool (excluding Yices2 and related Yices2 header files) is released under the Modified BSD license. 


EFSMT enables to answer problems of the following "shape", via the alternation of two solvers

$\exists x_1, \ldots, x_m\; \forall y_1, \ldots, y_n: \phi(x_1, \ldots, x_m, y_1, \ldots, y_n)$

Download & Install (Linux & MacOS)

Input format

EFSMT is designed to be used as a library. Still, now we offer basic input format support, allowing users to mix REAL, INT, and BOOL (no need to add definition).

 % Example using the simple format

Exists(x) REALForall(y) INTForall(z)Assumption([y>0] && [y<10])Assumption(!z)Guarantee([2*x-3*y <= 7])Guarantee([y + 100 >= 0])
\exists x\in \mathbf{R}\,\forall y \in \mathbf{Z}, z \in \mathbf{B}: ((y &gt; 0 \wedge y&lt;10) \wedge \neg z) \rightarrow ((2x-3y &lt;7) \wedge  (y+100&gt;0))

Currently, there are two restrictions in the parser:


Chih-Hong Cheng (ABB Research)

Natarajan Shankar (SRI international)