A tool and method for automatically producing near-optimal code sequences are
particularly
useful for generating near-optimal code sequences in inner loops, crucial subroutines,
and device drivers. As a novel functional and architectural strategy, the invention
contemplates applying technologies that would be normally in automatic theorem
proving to the problem of automatic code generation. The aspect of the automatic
theorem proving is realized by matching followed by planning with satisfiability
search. Notably also, the present invention targets a goal-oriented, cycle budget
limited code sequence in producing the near-optimal code sequence.