Yes, although it's hard to make it scale in every case. What you're talking about sounds like the field of program synthesis[1], which uses SMT solvers (among other technologies) to generate code to some specification. I worked on a system[2] that used this sort of technique to optimize code for a weird architecture (GreenArrays' Forth-based chip[3]) and it was certainly much easier to implement than a classical optimizing compiler.

Perhaps the most relevant example project here would be Rosette[4], which is basically a framework for easily writing synthesizers for different tasks. It would let you implement a description of your machine in Scheme (ie write a simple interpreter) and automatically generate a synthesizer for it that could compile programs in your language to formulas in a solver of some sort.

[1]: http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-...

[2]: http://jelv.is/chlorophyll.pdf

[3]: http://www.greenarraychips.com/

[4]: http://homes.cs.washington.edu/~emina/rosette/