Overview

At an intuitive level, SMT solvers are general-purpose problem solving tools. They are somewhat similar to calculators, in that the user provides the problem of interest, and the tool does some calculation to produce an answer. However, they are much more powerful than a simple calculator.

SMT solvers reason symbolically, as is done in grade school algebra. The user provides a set of assertions that describe constraints to be satisfied, and the solver produces a solution satisfying all of the constraints, if there is one. Consider the following simple example, mimicking a typical algebra word problem.

Example 1. In 10 years, Alice will be twice as old as Bob is now, but in 22 years, Bob will be twice as old as Alice is now. How old are Alice and Bob?

First, let’s see how to solve this using Python.

examples/Example1.py

1from cvc5.pythonic import *
2a, b = Ints('a b')
3solve(a + 10 == 2 * b, b + 22 == 2 * a)

The Pythonic API is designed to be as simple and intuitive as possible. We introduce the symbols we are using (SMT solvers always require that symbols be introduced before they are used), and then we call solve, passing in the two equations in much the same way we would write them naturally. The output is a simple representation of the solution as a Python list.

[a = 18, b = 14]

Alternatively, SMT solvers can take as input a script written in the SMT- LIB language [R5], a standard developed by the SMT community whose syntax is similar to that of LISP. Below is the same example written in SMT-LIB.

examples/Example1.smt2

 1(set-logic QF_LIA)
 2(set-option :produce-models true)
 3
 4(declare-const a Int)
 5(declare-const b Int)
 6
 7(assert (= (+ a 10) (* 2 b)))
 8(assert (= (+ b 22) (* 2 a)))
 9
10(check-sat)
11(get-model)

The result is:

sat
(
(define-fun a () Int 18)
(define-fun b () Int 14)
)

Notice that the solver replies sat before giving the solution. This is short for “satisfiable,” a word meaning that there is at least one solution. SMT solvers can also identify when a set of assertions has no solution. In this case, the solver replies unsat, which is short for “unsatisfiable.”

Let’s take a closer look at the SMT-LIB input file, which is a sequence of commands. The command in the first line tells the solver which logic we are working in. In this case, we are using QF_LIA which stands for quantifier-free linear integer arithmetic. We explain more about logics in SMT Theories. The second line tells the solver to produce models. A model assigns a concrete meaning to every user-declared symbol. Without turning this option on, a solver will still respond with sat or unsat, but it may not be able to provide a model. The next two lines declare two uninterpreted constants called a and b. Informally, we often refer to these as variables, because they play the same role that variables do in math. However, in the automated reasoning literature, a variable typically refers to a symbol that is bound by a quantifier, whereas an uninterpreted constant is a symbol whose value is determined by a model. SMT-LIB follows the the latter terminology. The next two lines create assertions. An assertion is a way of telling the solver about a formula that we would like to be true in the model that is produced. Note that the formulas too are specified in a LISP-like prefix syntax. Finally, the command (check-sat) tells the solver to check whether the set of assertions made so far is satisfiable, and the command (get-model) (which is only legal if the solver returns sat) prints values for each uninterpreted constant, with the guarantee that assigning these values to the constants makes all the assertions true. The values are printed using legal SMT-LIB syntax in case the user wants to copy and paste them into a new SMT-LIB script.

Exercise 1. Consider a modification of Example 1. The first assertion will stay the same, but for the second, let’s assert that Bob will be twice as old as Alice in only 20 years. Modify the Python program or SMT-LIB script to reflect the new set of constraints. What output does the SMT solver give?

Solution to Exercise 1

So far, we have seen the most basic use of an SMT solver. Given a set of assertions, determine whether there is a solution for them. We now show that this basic capability can be used to answer several similar questions.

Suppose we have a set \(X\) of assumptions about the world, and we want to know whether some hypothetical \(Y\) is possible under those assumptions. If we can express \(X\) and \(Y\) as SMT formulas, then an SMT solver can answer the question. In fact, we simply assert each assumption in \(X\) as well as the formula representing \(Y\) and check whether this set of assertions is satisfiable.

Example 2. Let \(x\) and \(y\) be 32-bit integers, with \(x\) a multiple of 2. Is it possible for the machine arithmetic product of \(x\) and \(y\) to be 1?

For this problem, we’ll use bit-vectors. SMT solvers use bit-vectors to model machine arithmetic and other operations on fixed-size vectors of bits. The SMT-LIB encoding and a corresponding Python script are shown below. This time, we use the Python API in a way that more closely resembles the SMT-LIB script.

examples/Example2.smt2

 1(set-logic QF_BV)
 2
 3(declare-const x (_ BitVec 32))
 4(declare-const y (_ BitVec 32))
 5(declare-const z (_ BitVec 32))
 6
 7(assert (= x (bvmul z (_ bv2 32))))
 8(assert (= (bvmul x y) (_ bv1 32)))
 9
10(check-sat)

We use the logic QF_BV which stands for quantifier-free bit-vectors. The underscore symbol _ is used in SMT-LIB to indicate that the next symbol is indexed by the following argument. It is used to specify the bit-vector size in this example. The bvmul symbol represents bit-vector multiplication, and the notation bvX is the bit-vector constant whose value, in decimal notation, is X. Constant z names the value we must multiply by 2 to get x. There is no solution because an even number does not have a multiplicative inverse in machine arithmetic (i.e., when doing arithmetic modulo a power of 2). The output of cvc5 is shown below.

Exercise 2. Find the multiplicative inverse of 5 (mod \(2^8\)).

Solution to Exercise 2

Another common situation is when we have a set \(X\) of assumptions, and we want to know whether some \(Y\) must hold as a consequence. If so, we say that \(Y\) is implied or entailed by \(X\). Again, assuming we can represent \(X\) and \(Y\) using formulas, we can start by asserting the formulas representing \(X\). At this point, however, we do not assert the formula for \(Y\) . Instead, we assert its negation. If the result is unsat, then \(Y\) must follow from \(X\). The reasoning is that if it is not possible for the negation of \(Y\) to be true when \(X\) is true, then \(Y\) itself must be true. Let’s look at a version of the well-known syllogism about Socrates.

Example 3. If all humans are mortal, and Socrates is a human, then must Socrates be mortal?

The SMT-LIB and Python versions are as follows.

examples/socrates.smt2

 1(set-logic UF)
 2
 3(declare-sort S 0)
 4(declare-fun Human (S) Bool)
 5(declare-fun Mortal (S) Bool)
 6(declare-const Socrates S)
 7
 8(assert (forall ((x S)) (=> (Human x) (Mortal x))))
 9(assert (Human Socrates))
10(assert (not (Mortal Socrates)))
11
12(check-sat)

This problem illustrates a few new encoding tools. First, we use the logic UF which stands for “uninterpreted functions.” This logic allows us to declare new function symbols. Note that it is also missing the QF prefix we’ve used above, which means that quantifiers are also allowed. We declare a new uninterpreted sort S. A sort is like a type in programming languages. We use an uninterpreted sort to represent a class of individual objects that cannot be modeled with the predefined sorts provided by SMT-LIB, (so far, we’ve seen the predefined sorts for integers and bit-vectors). Next, we declare two functions, Human and Mortal, each of which takes a single argument of sort S and returns a Bool, the SMT-LIB Boolean sort. A function returning a Boolean is also called a predicate. We then declare an uninterpreted constant called Socrates of sort S. Now, we are ready to encode the first fact, namely that all humans are mortal. To do so, we use the universal quantifier (forall in SMT-LIB, ForAll in Python). The assertion states that for every individual x of sort S, if the predicate Human holds for that individual, then the predicate Mortal also holds. The next assertion states that the Human predicate holds for Socrates. Finally, we want to see whether the fact that Socrates is mortal necessarily follows from the assumptions. To do this, we assert the negation of the statement and check for satisfiability. Running the example confirms that the result is unsatisfiable and thus, indeed, this statement is entailed. The output of cvc5 is shown below.

What we have presented so far should provide a good high-level idea of what is possible with SMT solvers.[1] We cover these ideas in more detail in the following. In Formal Foundations, we briefly describe the formal foundations for SMT. Next, in SMT Theories, we catalog the different theories supported by SMT solvers and provide examples of how to use them. We cover the different outputs produced by SMT solvers, including models and proofs, in SMT Solver Outputs, and conclude in Conclusion with pointers to additional resources.