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

[J. Nunez Fontarnau]

Dear Enea

I would appreciate it to the more if you could shed some light on the following
problem. Given the logic program

p(0, X, X) :- !.

p(N, X, Y) :-

	X1 is 0.75*X+1,
	N1 is N - 1,
	p(N1, X1, Y).


such that recurses $N$ times over the expression $0.75*X+1$, find a fixpoint by
which no overflow in the $X$ and $Y$ arguments can be proved.

My proceeding on this includes the construction of two polyhedra: one for the
base case; the other for the inductive case. Then I (try to) calculate the
fixpoint using the program below. But a series of problem arise. For instance,
for the inductive constraints as shown below (note in particular $B =< 10000$),
the following abnormal halting error pops up, at the second fixpoint iteration:

ERROR: Unhandled exception: 'Integer_to_integer_term()'

Another constraints setting that produces the same error consists in removing
$A <= 100$ and $B =< 10000$, and querying the program with  ?- w(100).

I would be thankful if you could suggest some hints on how to get a fixpoint for
the program above. It might be that I do not declare enough constraints so that
sufficient information to assure convergence is included.

Many Thanks.

  Ciao,
Javier

----------------------


In this program, argument $K$ corresponds to the bounds for triggering a
widening operator (in this case the standard: H79).


verbosity(1).

w(K) :-

	make_vars(6, [A, B, C, D, E, F]),

	% Base case
	ppl_new_Polyhedron_from_dimension(c, 3, Base),
	ppl_Polyhedron_add_constraints(Base,
		[A = 0, B >= 0, C = B]),
	display_poly(['Base'],Base),

	% Inductive case
	ppl_new_Polyhedron_from_dimension(c, 6, Induc),
	ppl_Polyhedron_add_constraints(Induc,
		[A =< 100, A >= 0, B >= 0, B =< 10000,
		 C >= 0,
		 D >= A - 1, 4*E >= 3*B + 4,
		 C = F]),
	display_poly(['Inductive'],Induc),

	% Previous polyhedron
	ppl_new_Polyhedron_empty_from_dimension(c, 3,
		Previous),

	fixpoint(1, K, Induc, Previous, Base, Fixpoint, N),
	display_poly(['Fixpoint'],Fixpoint),
	display_message(['reached in',N,'iterations']).


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

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

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

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

	make_vars(6, [A, B, C, D, E, F]),

	ppl_delete_Polyhedron(Previous),
	ppl_new_Polyhedron_from_Polyhedron(c, Current,
		c, Previous1),
	ppl_delete_Polyhedron(Current),
	ppl_new_Polyhedron_from_Polyhedron(c, Induc,
		c, Current1),
	ppl_new_Polyhedron_from_dimension(c, 3, Aux),
	ppl_Polyhedron_concatenate_assign(Aux, Previous1),
	ppl_Polyhedron_intersection_assign(Current1, Aux),
	ppl_delete_Polyhedron(Aux),
	ppl_Polyhedron_remove_dimensions(Current1,[D,F,E]),
	ppl_Polyhedron_poly_hull_assign_and_minimize(
		Current1, Previous1),
	(N >= K, ppl_Polyhedron_H79_widening_assign(Current1,
		Previous1);
	 true),
	display_poly(['Iteration ', N],Current1),
	N1 is N+1,
	fixpoint(N1, K, Induc, Previous1, Current1,
		Fixpoint, M).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_poly(Message, Polyhedron) :-
	ppl_Polyhedron_get_constraints(Polyhedron,
		Constraints),
	display_message(Message),
	display_message(Constraints).

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

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