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).