[m-rev.] for review: new termination analyser (part 2 of 6)

[Julien Fischer]

On Sat, 2 Apr 2005, Mark Brown wrote:

> On 24-Mar-2005, Julien Fischer <juliensf at cs.mu.OZ.AU> wrote:
> >
> > ===================================================================
> > RCS file: compiler/lp_rational.m
> > diff -N compiler/lp_rational.m
> > --- /dev/null	1 Jan 1970 00:00:00 -0000
> > +++ compiler/lp_rational.m	23 Mar 2005 22:47:32 -0000
>
> > +%-----------------------------------------------------------------------------%
> > +%
> > +% file: lp_rational.m
> > +% main authors: conway, juliensf, vjteag.
> > +%
> > +% This module contains code for creating and manipulating systems of rational
> > +% linear arithmetic constraints.  It provides the following operations:
> > +%
> > +% * optimization (using the simplex method)
> > +%
> > +% * projection (using Fourier elimination).
> > +%
> > +% * an entailment test (using the above linear optimizer above.)
>
> Remove one of the "above"s.
>
Done.

> > +:- func lp_rational.simplify_constraints(constraints) = constraints.
>
> This needs documentation.
>
Ok.

> > +    % substitute_vars(VarsA, VarsB, Constraints0) = Constraints.
> > +    % If length(VarsA) \= length(VarsB) then an exception is thrown.
>
> You should state what the function does (that is, do occurrences of VarsA
> get replaced with VarsB or vice-versa).
>
Yes, variables in VarsA get replaced with the corresponding element
in VarsB.  I've modified the comment to mention that fact.

> > +    % NOTE: this does does not always detect that a constraint
> > +    % set is inconsistent, so callers to this procedure may need
> > +    % to do a consistency check on the result if they require
> > +    % the resulting system of constraints to be consistent.
>
> s/does does/does/
>
Done.

> > +%------------------------------------------------------------------------------%
> > +%
> > +% Entailment.
> > +%
> > +
> > +:- type entailment_result
> > +    --->    entailed
> > +    ;       not_entailed
> > +    ;       inconsistent.
> > +
> > +    % entailed(Vars , Vars):
>
> The arguments here aren't right.
>
Fixed.

> > +    % Determines if the constraint `C' is implied by the set of
> > +    % constraints `Cs'. Uses the simplex method to find the point `P'
> > +    % satisfying `Cs' which maximizes (if `C' contains '=<') or minimizes
> > +    % (if `C' contains '>=') a function parallel to `C'.
> > +    % Then tests if `P' satisfies `C'.
> > +    % This assumes that all the variables are non-negative.
> > +    % Throws an exception if `Cs' is inconsistent.
> > +    %
> > +:- pred lp_rational.entailed(lp_varset::in, constraints::in,
> > +    constraint::in) is semidet.
> > +
> > +:- func lp_rational.entailed(lp_varset, constraints, constraint) =
> > +    entailment_result.
>
> The function needs a comment.  Does it ever return 'inconsistent', or
> throw an exception?
>
The former not the latter (barring bugs in the linear solver).  The
predicate declarations are in the wrong order and the comment is also
wrong.  The det version of this was a last minute change to a bug that
was found using the declarative debugger (and which I'm sure that Ian will
be delighted to tell you about ;-) ).  I evidentally forgot to update the
documentation here.  It's now fixed.

> > +%------------------------------------------------------------------------------%
> > +%
> > +% Stuff for intermodule optimization.
> > +%
> > +
> > +    % A function that converts an lp_var into a string.
> > +    %
> > +:- type output_var == (func(lp_var) = string).
> > +:- inst output_var == (func(in) = out is det).
> > +
> > +    % Write out the constraints in a form we can read in using the
> > +    % term parser from the standard library.
> > +    %
> > +:- pred lp_rational.output_constraints(output_var::in(output_var),
> > +    constraints::in, io::di, io::uo) is det.
>
> You may no longer need the output_var inst, since it is the default.
>
Ok.

> > +nonneg_constr(lte([_ - (-rat.one)], rat.zero)).
> > +nonneg_constr(gte(_, _)) :-
> > +    throw("nonneg_constr/1: get.").
>
> s/get/gte encountered/
Fixed.

>
> > +    % Sort the list of terms in ascending order by variable
> > +    % and then multiply through so that the first term has a
> > +    % coefficient of one or negative one.  If the first argument
> > +    % is `yes' then we multiply through by the reciprocal of the
> > +    % absolute value of the coefficient, otherwise we multiply through
> > +    % by the value.
>
> s/by the value/by the reciprocal of the value/
>
Fixed.

> > +%------------------------------------------------------------------------------%
> > +%
> > +% Predicates for eliminating equations from the constraints.
> > +% (Gaussian elimination)
> > +%
> > +
> > +% Split the constraints into a set of inequalities and a set of
> > +% equalities.  For every variable in the set of target variables (ie.
> > +% those we are eliminating), check if there is at least one equality
> > +% that contains that variable.  If then substitute the value of that
> > +% variable into the other constraints.
>
> s/If then/If so then/
>
Fixed.

> You should state what happens if there are no equalities containing that
> variable.
>
I've added a sentence mentioning that the set of variables returned by
this predicate are the ones that do not occur in any equality.

> > +    % The `Flag' argument is `yes' if a one or more substitutions was made,
>
> s/if a one/if one/
> s/was/were/
>
Fixed.


> > +fourier_elimination([], _, _, _, Matrix, yes(Matrix)).
> > +fourier_elimination(Vars @ [Var0 | Vars0], Varset, MaybeThreshold, !.Step,
> > +        Matrix0, Result) :-
> > +    %
> > +    % Use Duffin's heuristic to try and find a "nice" variable eliminate.
>
> s/variable eliminate/variable to eliminate/
>
Fixed.

> > +    % normalize_vector(Var, Terms0, Const0, Terms, Const).
> > +    % Converts a vector, broken up into `Terms0' and `Const0', into a
> > +    % parallel one where the coefficient of `Var' is +/- one.
> > +    % Throws an exception if the map contains a zero coefficient for `Var'.
>
> This comment is a bit misleading.  You should reword it to be more like the
> comment above normalize_constraint/3.
Ok.

>
> > +%------------------------------------------------------------------------------%
> > +%------------------------------------------------------------------------------%
> > +%
> > +% Entailment test.
> > +%
> > +
> > +    % entailed(C, Cs, Vars).
>
> The arguments aren't right here, either.
>
> > +    % Determines if the constraint `C' is implied by the set of
> > +    % constraints `Cs'.  Uses the simplex method to find the point `P'
> > +    % satisfying `Cs' which maximizes (or minimizes if `C' contains `>=' )
> > +    % a function parallel to `C'.  Then tests whether `P' satisfies `C'.
> > +    % This assumes that all the variables are non-negative.
>
> This whole comment should be merged with the one in the interface.
>
Done.

Julien.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------