[PPL-devel] Re: Fixpoint + Widening in PPL

[J. Nunez Fontarnau]

This is the code I am using to obtain a fixpoint for append. Note that no
widening is applied: so far the code is aimed at producing a (possibly) infinite
'iteration'. Though so it does, the polyhedra produced are always the same. Note
also that a query to 'fixpoint' will terminate in the base case. (?) Only by
changing the order of occurrence of the inductive and base 'fixpoint' clauses,
infinite recursive calls are obtained.

Please help.
Javier

% Iteration to Post-Fixpoint for Append.

%verbosity(0).
verbosity(1).

wappend :-

	% Base case
	make_vars(6, [A, B, C, D, E, F]),
	ppl_new_Polyhedron_from_dimension(c, 6, Base),
	ppl_Polyhedron_add_constraints(Base,
		[A = 0, B >= 0, C = B]),
	ppl_Polyhedron_get_constraints(Base, BConstr),
	display_message(['Base constraints ...']),
	display_message(BConstr),

	% Inductive case
	ppl_new_Polyhedron_from_dimension(c, 6, Induc),
	ppl_Polyhedron_add_constraints(Induc,
		[A + F = C + D, B = E, C + D >= A,
		 D >= 0, B >= 0, A >= D + 1]),
	ppl_Polyhedron_get_constraints(Induc, IConstr),
	display_message(['Inductive constraints ...']),
	display_message(IConstr),

	% Empty polyhedron
	ppl_new_Polyhedron_empty_from_dimension(c, 6, Empty),

	display_message(['Querying fixpoint/4 ...']),

	fixpoint(Induc, Empty, Base, Fixpoint),
	ppl_Polyhedron_get_constraints(Fixpoint, FConstr),
	display_message(['Post-Fixpoint ...']),
	display_message(FConstr),

	display_message(['Deleting Base ...']),
	ppl_delete_Polyhedron(Base),
	display_message(['Deleting Induc ...']),
	ppl_delete_Polyhedron(Induc),
	display_message(['Deleting Empty ...']),
	ppl_delete_Polyhedron(Empty).



%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Post-fixpoint calculation

% Base case
fixpoint(_, Previous, Current, Fixpoint) :-

	ppl_Polyhedron_contains_Polyhedron(Current,
		Previous),
	ppl_Polyhedron_get_constraints(Current, FCurrent),
	display_message(['Base case: Current ...']),
	display_message(FCurrent),
	ppl_Polyhedron_get_constraints(Previous, FPrevious),
	display_message(['Base case: Previous ...']),
	display_message(FPrevious),

	ppl_new_Polyhedron_from_Polyhedron(c, Current,
		c, Fixpoint),
	!.

% Inductive case
fixpoint(Induc, Previous, Current, Fixpoint) :-

	ppl_delete_Polyhedron(Previous),
	ppl_new_Polyhedron_from_Polyhedron(c, Current,
		c, Current1),
	ppl_Polyhedron_get_constraints(Current1, FCurrent1),
	display_message(['Inductive case: Current 1 ...']),
	display_message(FCurrent1),
	ppl_Polyhedron_get_constraints(Induc, FInduc),
	display_message(['Inductive case: Induc ...']),
	display_message(FInduc),

	% computations over current1
	ppl_Polyhedron_poly_hull_assign(Current1, Induc),
	ppl_Polyhedron_get_constraints(Current1, FCurrent1a),
	display_message(['Current 1 after convex hull ...']),
	display_message(FCurrent1a),

	ppl_Polyhedron_get_constraints(CS_P, Current1),
	ppl_Polyhedra_get_constraints(CS_Q, Induc),
	widen_extrapolation_init(P, CS_P, Topology),
	widen_extrapolation_init(Q, CS_Q, Topology),
	ppl_Polyhedron_H79_widening_assign(P, Q),

	display_message(['Recursive query to fixpoint ...']),

	fixpoint(Induc, Current, Current1, Fixpoint).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% make_var_list(+I,+Dimension,?VariableList)
% constructs a list of variables with indices from I to Dimension - 1.
% It is assumed that I =< Dimension.

make_vars(Dim, VarList):-
  make_var_list(0, Dim, VarList).
make_var_list(Dim,Dim,[]):- !.
make_var_list(I,Dim,['$VAR'(I)|VarList]):-
  I1 is I + 1,
  make_var_list(I1,Dim,VarList).


%%%%%%%%%%%%%%%%%%
% Output messages.

display_message(Message):-
   verbosity(1), !,
   nl, write_all(Message), nl.
display_message(_).

write_all([]).
write_all([Phrase|Phrases]):-
   write(Phrase),
   write(' '),
   write_all(Phrases).




> On Tue, 7 Sep 2004 10:10:06 +0100 (BST), P M Hill wrote
> > Hi Javier,
> >
> > Have a look in ppl/interfaces/Prolog/pl_check.pl
> >
> > There are tests for the ppl Prolog widening predicates
> > such as ppl_Polyhedron_H79_widening_assign/2.
> >
> > I have written some longer code that uses the widening to ensure
> > convergence in some analysis but it will not be in the ppl sources.
> >
> > I'll see if I can find it.
> >
> > Pat
> > On Tue, 7 Sep 2004, Enea Zaffanella wrote:
> >
> > > J. Nunez Fontarnau wrote:
> > > > Hi Enea
> > > > How are you ?
> > > >
> > > > I need to ask you about fixpoint calculations and widenings in PPL. As
> you are
> > > > the expertise in all the implementation stuff, I would like to ask
> whether there
> > > > is any examples on fixpoint calculation with PPL and widening for
> Prolog (not
> > > > C++). I've noticed a file append?.cc that calculates the fixpoint for
> append. I
> > > > am trying to rewrite it in Prolog, but I am a bit lost with
> the 'reassignment'
> > > > of polyhedra 'Previous' and 'Current'
> > >  >
> > >  > Any suggestions on how to implement this in Prolog would be very much
> > >  > appreciated.
> > >  >
> > >  > Thanks,
> > >  > Javier
> > >
> > > Dear Javier,
> > >
> > > I am not sure I have understood your question.
> > > As I see it, you are going in the wrong direction, since it seems that
> > > you want to repeat the iterative control flow of append*.cc into your
> > > Prolog program, whereas I would suggest to go for a more canonical
> > > recursive solution.
> > >
> > > Namely, your solution sould be something similar to the following
> pattern:
> > >
> > > %% base case
> > > upward_iteration_sequence(Previous, Current, Inductive, Current) :-
> > >    ppl_Polyhedron_contains_Polyhedron(Previous, Current),
> > >    !.
> > >
> > > %% inductive case.
> > > upward_iteration_sequence(Previous, Current, Inductive, Result) :-
> > >    ppl_delete_Polyhedron(Previous),
> > >    ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Current1),
> > >    %% perform the required computation modifying Current1.
> > >    ....,
> > >    upward_iteration_sequence(Current, Current1, Inductive, Result).
> > >
> > >
> > > I hope this is enough. Anyway, Pat is much more expert than me on the
> > > Prolog interface of PPL.
> > >
> > > Ciao,
> > > Enea.
> > >
> > >
>
>
> --
> Prof. Roberto Bagnara
> Computer Science Group
> Department of Mathematics, University of Parma, Italy
> http://www.cs.unipr.it/~bagnara/
> mailto:bagnara at cs.unipr.it
>
>

-- 
Javier Nunez Fontarnau, School of Computing, Phone: (+44) 113 3431075
University of Leeds, LS2 9JT, Leeds, UK.     Fax: (+44) 113 3435468
                                             http://www.comp.leeds.ac.uk/javier