Simple SMT solver for use in an optimizing compiler
Posted on December 31, 2014This is a second blog post in a series about engineering optimizing compilers; the previous was Quasi-quoting DSLs for free. In this blog we will see how we might write a very simple SMT solver that will allow us to write an optimization pass that can turn something like
if a == 0 then
if !(a == 0) && b == 1 then
write 1
else
write 2
else
write 3
into
if a == 0 then
write 2
else
write 3
without much effort at all. Read more at well-typed.com