The SMT-LIBv2 Language and Tools: A Tutorial

The SMT-LIBv2 Language and Tools: A Tutorial
David R. Cok
GrammaTech, Inc.
Version 1.1
February 13, 2011
The most recent version is available at
.
Copyright (c) 2010-2011 by David R. Cok. Permission is granted to make and
distribute copies of this document for educational or research purposes, pro-
vided that the copyright notice and permission notice are preserved and ac-
knowledgment is given in publications. Modified versions of the document
may not be made. Incorporating this document within a larger collection, or
distributing it for commercial purposes, or including it as part or all of a prod-
uct for sale is allowed only by separate written permission from the author.






Contents
Preface 4
Version History 4
Note 4
1 Introduction 5
1.1 The SMT-LIB endeavor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.2 Purpose and Content . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.3 Mechanics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2 Quick Start 9
3 The SMT-LIB Language (v2) 14
3.1 Some logical concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3.1.1 Satisfiability and Validity . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3.1.2 Quantified formulas and SMT solvers . . . . . . . . . . . . . . . . . . . 15
3.1.3 Many-Sorted Logic . . . . . . . . . ...