A Generic Parser for SMT-LIB v2

Alberto Griggio <griggio[AT]fbk.eu>

 Open Source

This is a (complete, I think) parser/lexer for the SMT-LIB v2 language, implemented in Flex, Bison and C99, released under the MIT license. Besides a grammar and an abstract interface for implementing backends, a sample implementation using the Yices 1 solver is provided. The implementation is not 100% complete, but it should be enough for understanding how the interface is supposed to work.

DOWNLOAD:

REQUIREMENTS:

For compiling, copy Makefile.in to Makefile, edit the compilation flags and the YICES_DIR variable, and run make

LICENSE:

Copyright (C) 2010-2013 Alberto Griggio

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.

CONTENTS:

LICENSE.txt:
the license file
Makefile.in:
Makefile template
smtlib2parserinterface.h:
abstract interface for implementing backends to the parser
smtlib2abstractparser.h, smtlib2abstractparser.c:
an abstract implementation of the parser interface, providing default implementation for the callbacks and support for parsing terms
smtlib2abstractparser_private.h:
"protected" part of the abstract parser
smtlib2bisonparser.y:
Bison grammar for the SMT-LIB v2 language, defining a re-entrant parser
smtlib2flexlexer.l:
Flex definitions for a re-entrant SMT-LIB v2 lexical scanner
smtlib2termparser.c, smtlib2termparser.h:
helper class for parsing terms and managing let bindings and definitions
smtlib2charbuf.h, smtlib2charbuf.c, smtlib2genvector.h, smtlib2hashtable.c, smtlib2hashtable.h, smtlib2scanner.c, smtlib2scanner.h, smtlib2stream.c, smtlib2stream.h, smtlib2types.h, smtlib2utils.c, smtlib2utils.h, smtlib2vector.c, smtlib2vector.h:
several utility data structures and functions
smtlib2yices.c, smtlib2yices.h, main.c:
example backend using the Yices 1 SMT solver
test1.smt2, test2.smt2, test3.smt2, test4.smt2, test5.smt2, test6.smt2:
small test inputs for the Yices backend