- Daniel Kroening
- SMT Lists/Sets/Maps
- Google groups:
SMT-LIB Format for
Finite Lists, Sets, and Maps
Sets, lists, and maps are elementary data structures used in most programs. Program analysis tools therefore need to decide verification conditions containing variables of such types. We propose a new theory for the SMT-Lib standard as the standard format for such formulae.
We provide:
- A document formalizing the theory (PDF).
- A formalization of the concrete syntax for the upcoming SMT-LIB version 2.
- A converter (below) from SMT-LIB 2 to SMT-LIB 1.
- A version of CBMC (below) with preliminary support for SMT-LIB 2.
- An initial set of benchmarks, currently generated from the Event-B filesystem case study. We are working on a more comprehensive benchmark collection.
For questions about the theories or the converter, contact Philipp Ruemmer.
SMT-LIB 2 Converter
To ease the adoption of the new theories and allow experiments, we have developed a preliminary axiomatisation of the theories in the SMT-LIB 1 language, together with a converter that translates SMT-LIB 2 problems into the SMT-LIB 1 format. Although the converter still has certain restrictions (that we will eliminate as soon as possible), it supports most parts of the SMT-LIB 2 format, all of the proposed list/set/map theories, comes with full type checking, and provides a good impression of how the theories can be used in practice.
The parser of the converter is written using the
BNF Converter
tool (in the source distributions below, the grammar is defined in the file
src/smtlib.cf
). This grammar can be used to generate
SMT-LIB 2 parsers for various languages, including C, C++ (the language
of the converter), Java, and OCaml.
Releases
- 2009-09-08 (source, Windows binary): Fixed two bugs
- 2009-08-26 (source, Windows binary): Several small changes to make the converter compile under Visual C++. The provided Windows binary needs some Visual Studio libraries to run.
- 2009-08-24 (source): Support for type synonyms and user-defined functions (macros).
- 2009-08-21 (source):
Support for the
let
operator in terms (and not only in formulae). - 2009-08-20 (source):
Added multiary operators (like
and
,or
with more than two arguments); added thedistinct
operator; cleaned up example directory; some bugfixes. - 2009-08-01 (source): Initial release
CBMC for SMT-LIB Version 2
We also provide a version of CBMC with prototypical support for generating formulas in the SMT-LIB version 2 format. Use the command line options
--smt2 --outfile dest
to write the
verification conditions in SMT-LIB version 2 format into the file
dest
. The CBMC manual is here.