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

[Enea Zaffanella]

Dear Javier,

J. Nunez Fontarnau wrote:
> 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

[...]

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

I guess that here you have to revert the order of arguments in the 
containment test. In an upward iteration sequence, it is always the case 
that the Current polyhedron contains the Previous one. As a side note, I 
would have placed the cut immediately after the containment test.

> % 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),

?

I guess that this is not the computation that you want to perform.
You are using poly-hull where an intersection should be used.
Moreover, you are not implementing the renaming apart of variables.
For a hint of how things could be done, see our tests/append1.cc C++ 
example.

Very briefly, Previous and Current should be 3-dim polyhedra, whereas 
Induc is a 6-dim polyhedron. In order to correctly compose them, you 
should first extend Current1 (the copy of Current) to be a 6-dim 
polyhedron using the "concatenation" method (that is, implement the 
renaming apart operation). Then you should intersect it with Induc (that 
is, compute the conjunction of the results of the recursive call with 
the constraints in the body of this clause). Finally, you have to remove 
the last three variables (that is, project the result on the clause's 
head variables).

Hoping that this is helpful enough.

Ciao,
Enea.