Chapter 16SMT Solving

Given a Σ-algebra A and a quantifier-free (QF) formula φ with variables Y , we say that φ is satisfiable (resp. valid) in A iff there is an assignment map a : Y A such that A,aφ (resp. for all maps a : Y A, A,aφ). Note that φ is valid in A iff ¬φ is unsatisfiable in A. We say that satisfiability in A is decidable iff we have an algorithm such that given any QF Σ-formula φ it can answer whether or not φ is satisfiable in A. Of course, this also means that it can answer whether or not φ is valid in A.

Assuming that all sorts in Σ are nonempty, i.e., TΣ,s for each sort s, we can view the equational unification methods for theories (Σ,G) explained in Chapters 13 and 14 , where G can be either a set of axioms Ax, or a set of FVP equations E Ax, as providing a decision procedure for satisfiability in the initial algebra TΣ∕G for any positive (i.e., having no negations) QF Σ-formula φ. This is so because any such positive φ can be put in disjunctive normal form as φ iI Qi, with each Qi the conjunction of a set of equations Qi. Then φ is satisfiable in TΣ∕G iff there exists a j I such that Qj has at least one G-unifier, which we can decide in Maude by asking for the first unifier of the system of equations Qj.

In this chapter we broaden the picture about satisfiability begun in Chapters 13 and 14 by explaining how satisfiability of QF formulas for several concrete Σ-algebras of interest is directly supported in Core Maude by special modules and an interface of commands that makes accessible to Maude users part of the functionality of the CVC4 and Yices2 SMT solvers. The reader should note that the only way of selecting one of the two SMT solvers within Maude is to use a different Maude binary executable file, maude-CVC4 or maude-Yices2, both available at the official website. In Section 16.6 we also briefly explain how satisfiability in initial algebras of the form TΣ∕EAx, where (Σ,E Ax) is FVP and satisfies one additional requirement, is also supported by algorithms written in Maude that use the variant unification algorithm from Chapter 14 as a subroutine.

The most basic type of satisfiability is that of formulas in propositional logic, that is, of Boolean expressions, in the two-element Boolean algebra 𝔹. This is called the SAT problem, and decision procedures solving it are called SAT solvers. By definition, a Boolean expression β with propositional variables X is satisfiable in 𝔹 iff there is an assignment a : X 𝔹 of Boolean values for the propositional variables X of β such that β is true under the assignment a.

But note that such a propositional SAT-solving problem for β in 𝔹 is equivalent to the first-order satisfiability in the initial algebra 𝔹 of the equational theory of the Booleans—as specified, for example, in the BOOL-OPS functional module of Chapter 7.1—of the equation β = true. In fact, Maude provides three different methods for solving the SAT problem: (1) the BOOL-OPS module can decide if β is satisfiable in 𝔹: it is so iff its canonical form in BOOL-OPS is different from false;1 (2) the LTL SAT solver described in Section 12.4, since propositional formulas are a special case of LTL formulas; and (3) the connections to the CVC4 and Yices SAT solvers explained in this chapter, which is of course the most efficient method among those three.

Satisfiability modulo theories (SMT) solvers provide satisfiability procedures both for SAT-solving and for various first-order theories T of interest. The theories discussed in this chapter are all theories T associated to specific data types of interest in the following, precise sense: given a Σ-algebra A its first-order theory th(A) is the theory th(A) = (Σ,Γ(A)), where Γ(A) = {φAφ}. Specifically, we will consider satisfiability procedures for QF formulas in theories of the form th(A) of A: (i) Presburger arithmetic on the integers (,0,1,+,>,), (ii) linear arithmetic on the rationals (,Q,+,>,), where Q is the (infinite) set of rational numbers interpreted by themselves as constants of the algebra ;2 and (iii) linear arithmetic for both the integers and the rationals, corresponding, essentially, to a subsort inclusion . Therefore, the intended model in this last case is in essence the linear arithmetic fragment of the initial algebra of the theory RAT of rationals described in Section 7.6, which contains the sort Int as a subsort. SMT solvers are called this way because they exploit the Boolean structure of QF first-order formulas to perform SAT solving at the Boolean level in order to achieve more efficient versions of satisfiability procedures for the theories T supported by the solver, using the so-called DPLL(T) approach [114].

To make SMT solving for the above-described theories available to Maude users, we have integrated within Maude, and have provided access to some of the decision procedures and functionality of, two state-of-the-art SMT solvers, namely, CVC43 and Yices24 . Maude’s connection to both CVC4 and Yices2 relies on the standard SMT-LIB notation5 accepted by both SMT solvers and allows for more connections to other SMT solvers to be added in the future. As already mentioned, the specific theories currently supported in Maude are: (i) SAT-solving for the Booleans, (ii) Presburger arithmetic for the integers, (iii) linear arithmetic for the rationals; and (iv) linear arithmetic for both the integers and the rationals. We describe below the corresponding Maude modules allowing definition of QF formulas in those four theories.

16.1Boolean formulas

The SMT interface is accessed by loading the file smt.maude. The SMT-LIB Core theory is represented by the following signature.

``` fmod BOOLEAN is  sort Boolean .  op true : -> Boolean [special (id-hook SMT_Symbol (true))] .  op false : -> Boolean [special (id-hook SMT_Symbol (false))] .   op not_ : Boolean -> Boolean    [prec 53 special (id-hook SMT_Symbol (not))] .  op _and_ : Boolean Boolean -> Boolean    [gather (E e) prec 55 special (id-hook SMT_Symbol (and))] .  op _xor_ : Boolean Boolean -> Boolean    [gather (E e) prec 57 special (id-hook SMT_Symbol (xor))] .  op _or_ : Boolean Boolean -> Boolean    [gather (E e) prec 59 special (id-hook SMT_Symbol (or))] .  op _implies_ : Boolean Boolean -> Boolean    [gather (e E) prec 61 special (id-hook SMT_Symbol (implies))] .   op _===_ : Boolean Boolean -> Boolean    [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] .  op _=/==_ : Boolean Boolean -> Boolean    [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] .  op _?_:_ : Boolean Boolean Boolean -> Boolean    [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] . endfm
```

Here a different sort Boolean and constants true and false are used for true and false to avoid immediately ambiguity with Maude’s Bool sort and its constants true and false. All of the operators are inert at the Maude level, i.e., they have no built-in semantics in Maude. The _?_:_ operator is the if-then-else operation and _===_ and _=/==_ are used to represent equality and inequality, again to minimize syntactic ambiguity with Maude’s standard symbols.

16.2Formulas using integer linear arithmetic

The SMT-LIB Ints theory is represented by the following signature.

``` fmod INTEGER is  protecting BOOLEAN .  sort Integer .  op <Integers> : -> Integer [special (id-hook SMT_NumberSymbol (integers))] .   op -_ : Integer -> Integer    [special (id-hook SMT_Symbol (-))] .  op _+_ : Integer Integer -> Integer    [gather (E e) prec 33 special (id-hook SMT_Symbol (+))] .  op _*_ : Integer Integer -> Integer    [gather (E e) prec 31 special (id-hook SMT_Symbol (*))] .  op _-_ : Integer Integer -> Integer    [gather (E e) prec 33 special (id-hook SMT_Symbol (-))] .  op _div_ : Integer Integer -> Integer    [gather (E e) prec 31 special (id-hook SMT_Symbol (div))] .  op _mod_ : Integer Integer -> Integer    [gather (E e) prec 31 special (id-hook SMT_Symbol (mod))] .   op _<_ : Integer Integer -> Boolean    [prec 37 special (id-hook SMT_Symbol (<))] .  op _<=_ : Integer Integer -> Boolean    [prec 37 special (id-hook SMT_Symbol (<=))] .  op _>_ : Integer Integer -> Boolean    [prec 37 special (id-hook SMT_Symbol (>))] .  op _>=_ : Integer Integer -> Boolean    [prec 37 special (id-hook SMT_Symbol (>=))] .   op _===_ : Integer Integer -> Boolean    [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] .  op _=/==_ : Integer Integer -> Boolean    [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] .  op _?_:_ : Boolean Integer Integer -> Integer    [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] .   op _divisible_ : Integer Integer -> Boolean    [prec 51 special (id-hook SMT_Symbol (divisible))] . endfm
```

Here a different sort Integer is given for the integer constants ,2,1,0,1,2, to avoid ambiguity with the integer constants of Maude’s Int sort. Note that _divisible_ has the opposite argument order to Maude’s _divides_ operator on Int but it follows the SMT-LIB convention.

16.3Formulas using rational linear arithmetic

The SMT-LIB Reals theory is represented by the following signature:

``` fmod REAL is  protecting BOOLEAN .  sort Real .  op <Reals> : -> Real [special (id-hook SMT_NumberSymbol (reals))] .   op -_ : Real -> Real [special (id-hook SMT_Symbol (-))] .  op _+_ : Real Real -> Real    [gather (E e) prec 33 special (id-hook SMT_Symbol (+))] .  op _*_ : Real Real -> Real    [gather (E e) prec 31 special (id-hook SMT_Symbol (*))] .  op _-_ : Real Real -> Real    [gather (E e) prec 33 special (id-hook SMT_Symbol (-))] .  op _/_ : Real Real -> Real    [gather (E e) prec 31 special (id-hook SMT_Symbol (/))] .   op _<_ : Real Real -> Boolean    [prec 37 special (id-hook SMT_Symbol (<))] .  op _<=_ : Real Real -> Boolean    [prec 37 special (id-hook SMT_Symbol (<=))] .  op _>_ : Real Real -> Boolean    [prec 37 special (id-hook SMT_Symbol (>))] .  op _>=_ : Real Real -> Boolean    [prec 37 special (id-hook SMT_Symbol (>=))] .   op _===_ : Real Real -> Boolean    [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] .  op _=/==_ : Real Real -> Boolean    [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] .  op _?_:_ : Boolean Real Real -> Real    [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] . endfm
```

Here a different sort Real is given for the rational constants that look like 11, 3100, 01, 73, to avoid ambiguity with the rational constants of Maude’s Rat sort. The symbol is mandatory and servers to distinguish the reals from the integers (which are completely different types in SMT-LIB). Again all of the operators are inert, although currently, rational constants are canonicalized (this may change).

16.4Formulas using rational and integer linear arithmetic

Finally, the SMT-LIB Reals-Ints theory is represented by the following signature:

``` fmod REAL-INTEGER is  protecting INTEGER .  protecting REAL .   op toReal : Integer -> Real [special (id-hook SMT_Symbol (toReal))] .  op toInteger : Real -> Integer [special (id-hook SMT_Symbol (toInteger))] .  op isInteger : Real -> Boolean [special (id-hook SMT_Symbol (isInteger))] . endfm
```

16.5Satisfiability of formulas

The SMT solver is invoked internally using the check command. The syntax of this command is:

``` check [ in ⟨ModId⟩ : ] ⟨Term⟩ .
```

where Term must only contain the constants and operators from the appropriate signatures above, together with variables from the three sorts, Boolean, Integer and Real when these are available. Adding any super or subsorts to these three sorts (or subsort relations between them) will cause inconsistency issues, as will adding any additional operators.

Maude responds with whatever the SMT solver returns, typically sat for satisfiable or unsat for unsatisfiable. Note that the current implementation is quite brittle. There is only a cursory attempt to check that the query to the SMT solver makes sense and no attempt to catch exceptions. Consider the following example.

``` fmod TEST-RI is  protecting REAL-INTEGER .  vars W X Y Z : Boolean .  vars I J K L : Integer .  vars P Q R S : Real . endfm
```

``` Maude> check toInteger(R) + toInteger(P) === toInteger(R + P) . Result from sat solver is: sat  Maude> check not(toInteger(R) + toInteger(P) === toInteger(R + P)) . Result from sat solver is: sat  Maude> check -2 < I and -2 * I > -1 and I =/== -1 . Result from sat solver is: sat  Maude> check -2 < I and -2 * I > -1 and I =/== -1 and I - I =/== I . Result from sat solver is: unsat
```

16.6A brief introduction to variant satisfiability

A current limitation of SMT solvers is that they only provide domain-specific satisfiability procedures for a fixed family T1,,Tn of theories and their so-called Nelson-Oppen combinations [113]. To verify programs in a conventional programming language with a fixed set of data types this is quite reasonable. But in a language like Maude, where order-sorted data types are user-definable as the initial models of functional modules, it would be highly desirable to have theory-generic decision procedures for an infinite class of user-definable theories of the form th(TΣ∕EAx), that is, for the theory of all inductive theorems true in the initial algebra TΣ∕EAx, where (Σ,E Ax) belongs to an infinite class of theories specifiable as functional modules in Maude. Specifically, such a class consists of equational theories that: (i) are FVP and (ii) protect a constructor subspecification (Ω,EΩ AxΩ) satisfying the OS-compactness property [108]. The OS-compactness requirement is quite mild in practice. For example, all constructor theories where the constructors are free modulo axioms, i.e., of the form (Ω,AxΩ), and where any associativity axiom in AxΩ has a corresponding commutative axiom also in AxΩ is OS-compact, and so are as well various parameterized theories of interest for lists, compact lists, multisets, sets, and hereditarily finite sets [108]. The theory-generic satisfiability algorithm for theories in this class is called variant satisfiability [108]. Detailed algorithms for variant satisfiability and its associated auxiliary functions (which invoke variant unification as a subroutine) as well as a Maude prototype tool are described in [129]. This is a quite active area of research with many applications. In the near future two important research objectives are to: (i) improve and document the current variant satisfiability prototype; and (ii) combine within Maude: (a) domain-specific decision procedures from state-of-the-art SMT solvers, (b) order-sorted congruence closure modulo axioms [107], and (c) variant satisfiability.