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
Download & Install (Linux & MacOS)
Installation is simple - install Yices2 first (one might need GMP library), then make the project. See README for details.
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
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.
Chih-Hong Cheng (ABB Research)
Natarajan Shankar (SRI international)