During the last month or so I had to work on some assignments regarding problems to be solved using a SMT solver.

SMT solvers are very interesting piece of machinery and one of the most simple thing to explain to the not introduced.

Let’s say you have a boolean formula, like in “not a and b”, and you want to know if there is a pair of True/False values that is able to make the formula “not a and b” true.

Obviously you could substitute a and b with predicates such as tall, short-hair, italian and wonder if there is someone that fits the description. If you could have a list of people along with their heigth, length of hair and nationality you could feed it to a computer and be done with your search in minutes.

There is another problem with our approach to the problem, we are using natural language and this can lead to ambiguity. “not a and b” is “not (a and b)” or “(not a) and b”? The precedence matter and the solution to the two problems is indeed different.

This time syntax and semantics have to go hand in hand.

Every SMT solver with a name has the decency of accepting some standard syntax called, wait for it, SMT-lib standard. As long as you can write this lispy syntax to specify your problems you can go and use every respectable solver (z3, yices and many others).

Obviously we can do logic programming in Scheme and it would be some fun but I had to get serious and one of the requirements of my assignments was to use a SMT solver from the list. Too bad.

Moreover this assignment was not something that could be done by hand. Writing 10 assertions and 40 variables by hand is not fun, not even once, so I had to program the computer to output the problem statements in this funky strange syntax.

Obviously the syntax is based on S-expression, and is optimized for parsing. What they don’t say is that it’s also optimized for generating from some languages ;)

So the choice was now between Rust and Scheme. As I was not aware of the Rust library there was no real choice here but it’s always good to look at prior arts (note to self for the future).

I already knew some Scheme but I did not have any chance to prove my teeth at a problem with it; I did most of the exercises in The Scheme Programming Language but that was it. The book is sitting in my shelf, the exercises are done but I could not find a use case. Not that I tried too much, mostly it was in the background but this time it was prepotently front and center.

The result of this excursus is my first module, guile-smt, and maybe a good mark on my assignment.

In the end I think that this was a fun experiment and now I must say that I grasp better all this symbol manipulation. It’s been a learning experience like no other, maybe I will need more often my fix of Scheme. It’s addictive as nothing else.