User:Realazthat/Projects wishlist/LLVM/Algorithm Synthesis

Using an SMT solver, do the following:

Have an interpreter of language L.

So, for example, Interpret(X,A) will interpret X, which is of language L, and execute it with input A, and return the result, and a weight W representing the time taken to execute it.

Create a function, F in language L to accomplish a task T. So F would be executed as follows:

Interpret( F, T )

Assert that there is no other function, say G, that is equivalent to F, that will have a lower weight.

//G is input from user
constrain( Interpret(G,T).r == Interpret(F,T).r )
assert( Interpret(G,T).w < Interpret(F,T) )

All of this should be converted to SMT, the assertion declared to result true, the formula declared unsatisfiable, and hopefully the assertion proven false with a counter example.

References:

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-15.pdf