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.