Hi, Javier.
J. Nunez Fontarnau wrote:
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()'
This seems to be caused by the call to the output function, since the Prolog system you are using (i.e., ... ?) cannot handle arbitrary precision integers. If you comment away all the calls to display_poly/2 but the last one printing the fixpoint, then you won't get the exception.
I tested your program using ppl_pl (after commenting all but the last polyhedra output). Note that the choice of k=17 is arbitrary ... just to let you see that the ppl core is not throwing an exception.
============================== [zaffanella@spark somepath]$ ppl_pl Welcome to SWI-Prolog (Multi-threaded, Version 5.2.13) Copyright (c) 1990-2003 University of Amsterdam. SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software, and you are welcome to redistribute it under certain conditions. Please visit http://www.swi-prolog.org for details.
For help, use ?- help(Topic). or ?- apropos(Word).
?- consult(fixpoint). Warning: (/somepath/fixpoint.pl:43): Singleton variables: [A, B, C] % fixpoint compiled 0.00 sec, 4,720 bytes
Yes ?- w(17).
Fixpoint
1*A>=0 1*B>=0
reached in 19 iterations
Yes ?- ==============================
Mmmmmhhhh ... not a really interesting invariant. I may be missing something, but I guess that you are doing something wrong. For instance, why using the non-strict inequalities
D >= A - 1, 4*E >= 3*B + 4,
to approximate the built-ins
X1 is 0.75*X+1, N1 is N - 1,
?
I would have used equalities instead. If you do this, you would obtain the following stronger invariant:
============================== ?- w(3).
Fixpoint
2499*A+ -1*B+1*C>=0 1*A+1*B+ -1*C>=0 1*B>=0
reached in 5 iterations
Yes ?- ==============================
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
You now have the post-fixpoint. Note though that I have not fully understood the link between your original program and the kind of analysis you are performing. For instance, where do the bounds A <= 100 and B <= 10000 come from?
Anyway, in order to improve the fixpoint you can use the limited_h79_extrapolation_assign (which is a widening, if you ensure that you will always call it by passing the same constraint system), or you can conclude your abstract computation by adding one (or more) steps of a downward iteration sequence.
Cheers, Enea.