How could an SMT solver be implemented as simple as possible?

Question

I'm trying to figure out how an SMT solver works as simple as possible. Let's assume we have a simple input program with symbolic values x and y. E.g.

if (x+y < 20) {
   if (x > 10) {
      if (y > 10) {
        assume(false);
      }
   }
}

Here we have different paths, depending on the conditions. To reach assume(false) each condition has to be true, so our outcoming formula is:

$x+y < 20 \,\,\,\,\,\wedge \,\,\,\,\, x > 10 \,\,\,\,\, \wedge \,\,\,\,\, y > 10$

So far, so good. What happens next, step by step?

I would like to implement, as simple as possible, a solver which gets as input something like the formula above and delivers specific output to reach the end of the path - here assume(false), i.e. x = 2147483647, y = 2147483647 (jfi: x+y would be -2) - for overflow detection or similar.

I know there are a lot of SMT solvers on the internet, but I couldn't find a really simple self-explaining one. Looking forward to a suggestion.

Answer 1

What happens next is that we invoke a SMT solver to try to check whether the formula

$$x+y < 20 \quad \land \quad x > 10 \quad \land \quad y > 10$$

is satisfiable. The solver tries to find values for $x,y$ that make this formula true. If it finds such a value, then it knows the assume(false) statement is reachable. (I am guessing you meant to write assert(false), not assume(false).) If the formula is not satisfiable, then that statement is not reachable.

So basically you are asking: how do SMT solvers work? That is too broad for this site, but there are lots of places that explain how SAT solvers and SMT solvers work. I would suggest doing some research; you will find many explanations. You could start with the DPLL algorithm for SAT.

There is little point in implementing your own solver. Your solver will probably perform far worse than existing tools. There has been a lot of research into building effective solvers, and the techniques required are non-trivial. Instead, I'd recommend you simply use an existing solver, such as Z3.

If you just want to implement one for fun, the most straightforward approach is probably to bit-blast to SAT: treat each bit of (the binary representation of) $x,y$ as a boolean variable, then write down a boolean formula (on those boolean variables) that expresses the requirement that $x+y<20$. How can you do that? Write a boolean circuit that computes $x+y$ and compares the sum to 20, then convert that circuit from CircuitSAT to SAT. Finally, invoke an off-the-shelf SAT solver to check satisfiability of this boolean formula. You'll need to do some research to understand each of these steps, but there's a lot written on how to do that.

Answer 2

You may not need a general SMT solver. In this case, you have a bunch of inequalities conjoined together, which you can solve as a linear program.

A simpler alternative to an SMT solver is to implement the theory as an add-on to a logic program. Most decent Prolog implementations, for example, have a CLP(R) or CLP(Q) library which can solve equality and inequality constraints over reals or rationals.