This lecture will be about SMT resolving, and we will say something about the syntax and the tools. We already saw that SAT is satisfiability that is about propositional formulas, that is, composed from Boolean variables and operators, negation, disjunction, conjunction, implication, and bifurcation. SMT means satisfiability modulo theories, and it is about SAT extended by extra theory. Here, we focus on the theory of linear inequalities, either on real numbers or integers, but they deal with numbers. Again a formula is satisfiable, abbreviated to SAT, if it is possible to give values to the variables such that a formula yields true. And the mapping of the variables to these values situated to formula yields true, that's satisfying assignment. Let's give an example. Here, we have a formula on integer variables a, b, c, and d. Two a is greater than b plus c, 2b is greater than c plus d, 2c is greater than 3d, and 3d is greater than a plus c. While you might try to find a solution by yourself, but you will see that it is not that easy, it has a solution. It is satisfiable with satisfying assignment, a is 30, b is 27, c is 32, and d is 21, and in fact, this is the smallest solution. There are tools to solve this kind of problems. For checking satisfiability, we have several powerful tools, SMT solvers like Z3, YICES, and CVC4. For non-commercial use, they are free to download and free to use. You can see further instructions how to do this. You can also google them and find also how to do this. Most of them have their own syntax, but luckily they all accept the syntax of the SMT- LIB standard. In fact, there are also competitions and if you do a competition on several tools, of course, they should have a common syntax. In this lecture, we show how to use the syntax of SMT-LIB Version 2. There was an earlier Version 1.2 and it was slightly different. But now, the focus is on Version 2. The tools allow to be used interactively, but we want to apply them on big formulas. And a big formula you do not want to type in yourself, but you want to have a file. Typically, we have a program generating this formula in a file. If the file is called, let's say file, then we will call the tool by typing the name of the tool and maybe some flex in some command-line interface, and that is how we use the tools. The general ingredients of a file in the syntax are as follows. It starts by set-logic or set-options, where you can define which logic to use or which option to use. Most times they have a default, so they can be left away if you just want to take the default. Next, you have the declarations. You can declare variables, you can declare functions, and you do that by declare-const and declare-fun. Next, we have the actual formula, and this is put in assert with parentheses around it. Between the opening parenthesis and the closing parenthesis, we have the formula that may be very big. Next, we have the command check-sat to do the actual sat solving. In case of satisfiability, we want to show the satisfying assignment, we should continue by get-model. All operators in this syntax: greater than, less than, equality, greater or equal, less or equal, plus, times, and, or, not, all operators are written in prefix notation. That means, always first we start by parenthesis open, then we have the operator, then the arguments, and then parenthesis closed. So in these notations, the expression 2a is written as, (* 2 a), and b plus c is written as, (+ b c). The full formula, 2a greater than b plus c, is written as follows. We simply take these two ingredients and we put parentheses open greater than around it and we conclude by parenthesis closed. The operators plus and an or may have any number of arguments, not only two, and that's often convenient if you want to add a great amount of numbers or if you have the conjunction of a great number of requirements, you only need to put a single one, plus at the start or a single end at the start. For linearity, star always has two arguments, and one of which should be a number. Otherwise, the expression is not linear and then typically, the tools do not accept it or are very poor. So, our problem of solving 2a greater than b plus c and so on can be expressed by the following formula. First, we have the declarations of a, b, c, and d, all being integers. Next, we have the assert of the whole formula, which is an Int of the four requirements, each expressing such an equality. Then, check-sat and then get-model. If we put this text in a file called file, for instance, by doing cut and paste from the examples document, then we call Z3 with the flag minus smt2, to state that we need this smt2 syntax and then the name of the file. Then within a fraction of a second, we get the output sat and the model stating that b has value 27, a the value 30, c the value of 32, d the value 21, indeed containing the values as just mentioned. The same can be done by one function f, instead of four separate variables a,b,c,d. Just by replacing a by f(1), b by f(2), c by f(3) and d by f(4). Then, it looks as follows. First, remember that f(1) is written in the SMT syntax (f 1). It follows the same prefix format all by starting by, parentheses open, then the name of the operator, then the arguments, and then parentheses closed, and the full formula then reads as follows. If we apply Z3 on it, we get the solutions, but now for f1, f2, f3, and f4. Well, here we have an example in propositional SAT. We want to check satisfiability of some big formula containing Int, an or, a negation, an implication and by implication, and four boolean variables a, b, c, and d. Well, in the syntax implication is written as, implies and by implication by iff. Then the formula reads as follows, we declare a constant of type Bool a and the same for B, C, and D. We have an assert, and there we simply express the formula as given on top. We conclude by check-sat and get-model, and indeed this gives the solution. SMT solvers can also deal with very big numbers. For instance, if we want to compute 87 times a very big odd number plus 93 times a very big other odd number, and we want to divide it by 2. Well, which is possible, since both parts are also the same as even. So, dividing by two is possible. So, this should be an integer. If we want to compute this by the SMT solver, we can do this by the following formula. We declare A to keep the value, the first big number, we declare B to keep the value of the second big number, and C for the answer. We just say 87 times A plus 93 times B should be equal to C plus C. If we do check-sat and get-model, we get the result C is indeed the result of this computation. A convenient operation is the if-then-else, abbreviated do ite. It always has three arguments. The first one is the condition, which should be a boolean. The second one is the result in case the condition is true, and the third one is the result in case the condition is false. Let's give an example, Ite less a b 13 and then and so on. What does this mean? Well, this yields the value 13, in case a is less than b, and otherwise it yields the value 3a. Another application is as follows. We can do ite p 1 0. What does this mean? Well, p is a boolean variable, and in case this has the value true, it yields one and otherwise it yields zero. So this transforms true to one and false to zero. If we do this for p,q, r and add all results, this just counts the number of variables among p,q,r that are true. This kind of things is convenient to use and will often be used in examples. Summarizing, we saw how SAT can be extended to SMT, to deal with linear inequalities, and the SMT solvers like Z3, YICES, and CVC4 accept formula in the SMT-LIB syntax and we saw a number of examples of this. In next lectures, we will give several applications, but you may start by playing around right now. Good luck.