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@cs.unipr.it