User:Realazthat/Projects wishlist/LLVM/Algorithm Synthesis: Difference between revisions
(Created page with " 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 e...") |
No edit summary |
||
| Line 1: | Line 1: | ||
Using an SMT solver, do the following: |
Using an SMT solver, do the following: |
||
| Line 14: | Line 13: | ||
<pre> |
<pre> |
||
//G is input from user |
//G is input from user |
||
constrain( Interpret(G,T).r == Interpret(F,T).r ) |
constrain( Interpret(G,T).r == Interpret(F,T).r ) ///the results must always be equal |
||
assert( Interpret(G,T).w < Interpret(F,T) ) |
assert( !(Interpret(G,T).w < Interpret(F,T)) ) ///w must always be less. We assert that this is false, hoping for a counter example. |
||
</pre> |
</pre> |
||
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. |
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. |
||
Rinse and repeat, using the resulting G as the next F until unsatisfiable is true (in which case it is the optimal algorithm). |
|||
Notes: |
|||
'''w''' should probably be calculated, or compared asymptotically. |
|||
There should be a memory constraint as well, as a huge constant array with precomputed results will probably yeild the lowest '''w'''. The memory should probably be constrained to a constant times the size of the input, again, asymptotically. |
|||
For the weight, one would probably give |
|||
Revision as of 05:42, 26 November 2010
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 ) ///the results must always be equal assert( !(Interpret(G,T).w < Interpret(F,T)) ) ///w must always be less. We assert that this is false, hoping for a counter example.
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.
Rinse and repeat, using the resulting G as the next F until unsatisfiable is true (in which case it is the optimal algorithm).
Notes: w should probably be calculated, or compared asymptotically. There should be a memory constraint as well, as a huge constant array with precomputed results will probably yeild the lowest w. The memory should probably be constrained to a constant times the size of the input, again, asymptotically.
For the weight, one would probably give
References: