Library SMTLIB.Domain

• Building a Model's Domain
  • The Two Passes
  • The Agreement
  • The Equations
  • Inhabitation

Library SMTLIB.Eval: Evaluation of SMT-LIB Terms

• Valuations
• The Evaluation Relation
• Inversion Principles
• Basic Facts About Evaluation
• Transporting an Evaluation
  • Agreement on Free Variables
  • Weakening
  • Strengthening
  • Across Signatures That Agree Except on Sorts
• Sort Uniqueness
• Determinism
• Renaming and Substitution
  • Renaming a Free Variable
  • Alpha-Renaming One Binder
  • Substitution
  • Alpha-Renaming the Variable a Context Was Extended At
  • Alpha-Renaming a Binder List
• Totality
• Satisfaction

Library SMTLIB.Signature: Signatures, their Construction and Composition

• Signatures
• Monomorphic Ranks
• Algebraic Datatypes
• Signature Expansion
• Rank Extension
• Signature Composition
  • Composability
  • The Composed Signature
  • What Composition Preserves
• Adding Sorts to a Signature
  • Datatype Sorts Across the Two Constructions

Library SMTLIB.Sorting: Well-Sortedness of SMT-LIB Terms

• The Sorting Judgment
• Extensionality
• Weakening and Strengthening
• Local Closure
• Declared Variables
• Sort Parameters
• Renaming and Substitution

Library SMTLIB.Symbols: Symbols, Identifiers and Sorts

• Symbols
• Identifiers & Indices
  • Boolean Equality
• Sorts
  • Induction and Recursion Principles
  • Decidable Equality and Countability
  • Operations on Sorts
  • Well-Formedness
• Elementary Sorts
• Sort Parameters
• Monomorphic Sorts
• Sort Substitution
• Instantiation

Library SMTLIB.Term: Syntax of SMT-LIB Terms

• Patterns
• Terms
• Size
• Free Variables
• Opening, Closing, Substitution & Local Closure
  • Facts about term_open
  • Facts about term_close
  • Interaction of term_open and term_close
  • Facts about term_subst
  • Facts about lc
  • Facts about lc_at
  • Substitution under opening
  • Opening and closing round-trips
• Sort Parameters and Sort Substitution

Library SMTLIB.Theory: Structures & Theories

• Interpretations and Heterogeneous Lists
  • Operations on hlist
• Ground Terms
  • Elimination
  • Reading a Sort Off a Term
• Structures
  • Moving Between the Domain and the Term Algebra
  • Crossing a Constructor's Argument List
  • The Selector and Tester Conditions
  • The Constructor Condition
  • Consequences of the Structure Axioms
  • What a Consumer of the Datatype Condition Needs
• Theories
• Model Construction
  • Building an Interpretation

Library SMTLIB.Utils: General-Purpose Helpers

• Type Casts
• Heterogeneous Equality
• Options
• Lists
  • Contiguous Sublists
  • Type-Valued "Every Element"
  • Decidable List Equality
  • Deciding Forall From Elementwise Decisions
  • Projecting Forall
• Lists into Finite Maps and Sets
• Strings
• Reading Back a Rendering
  • Taking a Rendering Apart
• Fresh Strings

Library SMTLIB.Tests.TestTheory: A Theory and a Model to Test Against

• A Signature with an Uninterpreted Symbol
• The Theory
• The Domain
• The Interpretation
• Consistency
• A Higher-Order Test Theory

Library SMTLIB.Tests.UnitTests: The Semantics on Four Small Examples

• 1 + 1 = 2 holds in every model
• Excluded middle holds in every model
• 0 / 0 is underspecified
• f 0 = 4 holds in some model, for an uninterpreted f
• 1 = 2 is unsatisfiable
• Excluded middle at Int, and a universal that is false
• Equality at a map sort
• Congruence, in a theory that can apply a function
• A formula with a sort parameter
• Refutation fails for a formula with a sort parameter

Library SMTLIB.Theory.Core

Library SMTLIB.Theory.HO_Core

Library SMTLIB.Theory.Reals_Ints

• • Reading a Literal Back

Library SMTLIB.Theory.Seq

• Datatypes Nested Under Sequences
  • Elimination
  • Size
  • Moving Between the Domain and the Term Algebra
  • How the Two Read Off Each Constructor
  • The Two Round Trips
  • Crossing a Constructor's Argument List
  • The Datatype Conditions, Read Through Sequences
  • What a Consumer Gets Out of Them
  • Closing a Pretheory with the Extended Reading
  • Interpreting the Datatype Symbols

Library SMTLIB.Theory.Strings

• • String constants
  • Reading a Constant Back