| 摘要 |
<p>A method which determines by an optimizing compiler whether any variable in the given program equals to the given acyclic mathematical function f(x,y,...) applied to the given variables x, y, ... in the program. In one embodiment, the method includes expressing the bits of the value of the function f(x,y,..) as a Boolean function of the bits of the inputs x, y, ...; expressing, for every variable v and program statement s, the value taken by v when s is executed as a Boolean function V(s,v)(x, y, ...) of the bits of x, y, ...; and expressing, for every statement s, the condition under which the statement is executed as a Boolean function C(s)(x, y, ...) of the bits of the inputs x, y, .... Finally, a determination is made using a Boolean satisfiability oracle of whether, for the given variable v and program statement s, the following Boolean expression holds: C(s)(x,y,...) P> V(s,v)(x,y...)=f(x,y,...). In a second embodiment, the method includes expressing the value of f(x,y,...) as a plurality of functions f <SUB>j</SUB>(x,y,..) having the corresponding predicate P<SUB>j</SUB>(x,y,..); expressing, for every variable v and program statement s, the value taken by v when s is executed as a plurality of functions V<SUB>j</SUB>(s,v)(x,y,...), one for each predicate P<SUB>j</SUB>(x,y,..); and expressing, for every statement s, the condition under which the statement is executed as a plurality of functions C<SUB>j</SUB>(s)(x,y,...), one for each predicate P<SUB>j</SUB>(x,y,..). Finally, a determination is of whether for the given variable v and program statement s, V<SUB>j</SUB>(s,v)(x,y,...)=f<SUB>j</SUB>(x,y,..) whenever the predicate P<SUB>j</SUB>(x,y,..) and the condition C<SUB>j</SUB>(s)(x,y,...) are true.</p> |
