DescriptionEFSMT 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. UsageEFSMT enables to answer problems of the following "shape", via the alternation of two solvers 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 formatEFSMT 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).
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.
DevelopmentChih-Hong Cheng (ABB Research) Natarajan Shankar (SRI international) |