I’m working on integrating two SMT solvers with Wenxin Feng, therefore it is necessary to understand the SMT-LIB 2.0 logic, which can be used as an input language for both solvers (AltErgo, CVC4). Part of the project is to classify formulas which can be solved by one solver, while not by the others. Therefore knowing how theories and logics are defined in SMT-LIB is also important.

SMT-LIB Logics

• \(\mathcal{S}\): Infinite set of sort symbols, containing \(\tt BOOL\).
• \(\mathcal{U}\): Infinite set of sort parameters
• \(\mathcal{X}\): Infinite set of variables
• \(\mathcal{F}\): Infinite set of function symbols
• \(\mathcal{B}\): Boolean values \(\tt \{true, false\}\)
• …

Sorts

Sorts over a set of sort symbols \(\mathcal{S}\) are defined as \(\tt Sort(\mathcal{S})\).

• \(\sigma \in \mathcal{S}\) of arity 0 is a sort
• \(\sigma \sigma_1, \sigma_2, \sigma_3, \ldots, \sigma_n\) is a sort if \(\sigma \in \mathcal{S}\) of arity \(n\), \(\sigma_1\) to \(\sigma_n\) are sorts

Signature

Baiscly, \(\Sigma\) defines sort symbols and arities, function symbols and ranks, some variables and their sorts.

• \(\Sigma^\mathcal{S} \subset \mathcal{S}\): sort symbols, containing \(\tt BOOL\)
• \(\Sigma^\mathcal{F} \subset \mathcal{F}\): function symbols, containing equality, conjunction, and negation
• \(\Sigma^\mathcal{S}\) to \(\mathbb{N}\): a total mapping from sort symbol to its arity, including \(\tt BOOL \Rightarrow 0\)
• \(\Sigma^\mathcal{F}\) to \(\tt Sort(\Sigma^\mathcal{S})+\): a left total mapping from a function symbol to its rank, containing \(=(\sigma, \sigma, {\tt BOOL} )\), \(\neg({\tt BOOL},{\tt BOOL})\), \(\wedge ({\tt BOOL}, {\tt BOOL}, {\tt BOOL})\).
• \(\mathcal{X}\) to \(\tt Sort(\Sigma^\mathcal{S})\): a partial mapping from a variable to its sort.

Formulas

Well sorted terms of sort \(\tt BOOL\) over \(\Sigma\)

Structure

\(\bf A\) can be regarded as a model.

• \(A\): the universe (of values) of \(\bf A\), including \(\tt BOOL^{\bf A} = \{true, false\}\).
• \(\sigma^{\bf A} \subset A\): give the sort \(\sigma \in \tt Sort(\Sigma^\mathcal{S})\) a universe \(\sigma^{\bf A} \subset A\). For example, \(\tt BOOL^{\bf A}\) is \(\{true, false\} \subset \rm A\). \(\tt INT^{\bf A}\) could be all the integers \(\mathbb{Z} \subset A\).
• \((f:\sigma)^{\bf A} \in \sigma^{\bf A}\): give the constant symbol \(f:\sigma\) a value in the universe of $\sigma$
• \((f:\sigma_1,\sigma_2,\ldots,\sigma_n,\sigma)^{\bf A}\): define the function symbol as a relation from \((\sigma_1,\sigma_2,…,\sigma_n)^{\bf A}\) to \(\sigma^{\bf A}\). This must include the equality relations (or identity predicate over \(\sigma^{\bf A}\), that is \(\tt = (\sigma, \sigma, BOOL)\) as standard equality relations from \((\sigma^{\bf A}, \sigma^{\bf A})\) to \(\{true, false\}\)).

\(\sigma^{\bf A}\) is called the extension of \(\sigma\) in \(\bf A\).

Valuation and Interpretation

• Valuations \(v\): a partial mapping \(v\) from \(\mathcal{X} \times \tt Sort(\Sigma^\mathcal{S})\) to \(\sigma^{\bf A}\). That is to give variable \(x\) of sort \(\sigma\) a value in \(\sigma^{\bf A}\).
• Interpretation \(\mathcal{I}\): \(\mathcal{I} = ({\bf A}, v)\), that is the structure together with the valuations make the \(\Sigma\)-interpretation.
• Semantics: \(\mathcal{I}\) will assign a meaning to well-sorted terms by uniquely mapping them into the \(\bf A\).
• Satisfiability: if \(\varphi\) is mapped to \(\tt true\) by some \(\mathcal{I}\), then it is satisfiable.
  • if \(\varphi\) is not closed, we say \(\mathcal{I} = ({\bf A}, v)\) makes true \(\varphi\)
  • if \(\varphi\) is closed, we say the structure \(\bf A\) makes true \(\varphi\). (Since it doesn’t matter what valuation it is.)
  • if \(\varphi\) is closed, we say the structure \(\bf A\) a model of \(\varphi\).

Theories

• Traditionally, its a set of axioms
• Here it consists of three parts
  • Signature: \(\Sigma\)
  • Axioms:
    • I think this part is left for the people who implement solvers. Take \(\tt INT\) theory as an example, since we have the plus sign in our signature (we just denote it as \(\tt ADD\), so that you know it is only a symbol, not the actual operation), we will have an axiom like \(\forall x:{\tt INT}. y:{\tt INT}. \exists z:{\tt INT}. {\tt ADD}(x,y,z) \leftrightarrow x + y = z\). Therefore, our model (or structure) must contain the correct relations to map \(\tt ADD\) to the actual addition operation to satisfy this axiom.
    • Also, some theories like \(\tt REAL\) include those axioms as plain text, like associativity, commutativity, etc.
  • Models: A set of \(\Sigma\)-structures, all of which are models of the theory.

Logics

• Sublogic: it is a sublogic of SMT-LIB logic
• Restrictions:
  • fixing a signature \(\Sigma\) and its theory \(\mathcal{T}\)
  • restricting structures to the models of \(\mathcal{T}\)
  • restricting input sentences as subset of \(\Sigma\)-sentences