EFSMT - A wrapper for solving exists-forall formulae

Description

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.

Usage

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)

  • Version efsmt_20150419.tar.gz

  • Installation is simple - install Yices2 first (one might need GMP library), then make the project. See README for details.

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:

  • "-" is always viewed as minus, not the unary negation. Therefore, [-2*x + y > 0] will create syntax error. Use [2*x - y < 0] instead.

  • "!" negation should be close to (Pseudo) Boolean variables. Therefore, !(a && b) will create syntax error. Use (!a || !b) instead.

Development

Chih-Hong Cheng (ABB Research)

Natarajan Shankar (SRI international)