2021-04-11 10:34:02 (CEST) cTI start

% cTI_lt 0.25 using 23.619 MLIPS SICStus 3.8.5 (x86-linux-glibc2.1): Mon Oct 30 16:34:14 CET 2000.
% cTI: Rt=648ms, Wt=1144ms, GC=4ms. NTI: Rt=12ms, Wt=8ms at most 84 inferences for useful informations.
% NTI summary: 15 cases unresolved, 3 predicates have been ignored: [!/0,;/2,sort/2]

append(A,B,C)terminates_if b(A);b(C).
    % optimal. loops found: [append([A|_],x,[A|_])]. NTI took    0ms,72i,72i
find_all_vars(A,B)terminates_if b(A).
    % optimal. loops found: [find_all_vars([[]=_|_],x)]. NTI took    0ms,77i,77i WARNING: ignored predicates: [sort/2]
find_all_vars2(A,B)terminates_if b(A).
    % optimal. loops found: [find_all_vars2([[]=_|_],_),find_all_vars2([[]=_|_],y)]. NTI took    0ms,73i,73i
get_query(A,B)terminates_if true.
init_vars(A,B,C,D)terminates_if false.
    % optimal. loops found: [init_vars([],[],_,x),init_vars([],[],y,x)]. NTI took    0ms,84i,84i WARNING: ignored predicates: [sort/2,!/0]
init_vars2(A,B,C)terminates_if b(A).
    % optimal. loops found: [init_vars2([_|_],x,x)]. NTI took    0ms,73i,73i WARNING: ignored predicates: [sort/2]
init_vars3(A,B,C)terminates_if b(A);b(C).
    % optimal. loops found: [init_vars3([A|_],x,[[A]=[unbound]|_])]. NTI took    0ms,72i,72i
intersect(A,B,C,D,E)terminates_if b(A),b(B);b(A),b(D);b(B),b(E);b(C),b(D),b(E).
    % 15 unresolved: [intersect(b,f,b,f,b),intersect(b,f,b,f,f),intersect(b,f,f,f,b),intersect(b,f,f,f,f),intersect(f,b,b,b,f),intersect(f,b,b,f,f),intersect(f,b,f,b,f),intersect(f,b,f,f,f),intersect(f,f,b,b,f),intersect(f,f,b,f,b),intersect(f,f,b,f,f),intersect(f,f,f,b,b),intersect(f,f,f,b,f),intersect(f,f,f,f,b),intersect(f,f,f,f,f)].
    %  NTI took    0ms, 0i,71i WARNING: ignored predicates: [!/0,;/2]

% Comparison with termination analyzers
% A termination analyser of identical power would verify
% with the following 21 proofs the 8 inferred conditions:

append(f, f, b).
    % ==> termination proof established
append(b, f, f).
    % ==> termination proof established
append(f, b, f).
    % ==> no proof found
find_all_vars(b, f).
    % ==> termination proof established
find_all_vars(f, b).
    % ==> no proof found
find_all_vars2(b, f).
    % ==> termination proof established
find_all_vars2(f, b).
    % ==> no proof found
get_query(f, f).
    % ==> termination proof established
init_vars(b, b, b, b).
    % ==> no proof found
init_vars2(b, f, f).
    % ==> termination proof established
init_vars2(f, b, b).
    % ==> no proof found
init_vars3(f, f, b).
    % ==> termination proof established
init_vars3(b, f, f).
    % ==> termination proof established
init_vars3(f, b, f).
    % ==> no proof found
intersect(f, b, f, f, b).
    % ==> termination proof established
intersect(b, f, f, b, f).
    % ==> termination proof established
intersect(b, b, f, f, f).
    % ==> termination proof established
intersect(f, f, b, b, b).
    % ==> termination proof established
intersect(b, f, b, f, b).
    % ==> no proof found
intersect(f, b, b, b, f).
    % ==> no proof found
intersect(f, f, f, b, b).
    % ==> no proof found

Tooltip: You can skip this comparison with termination analyzers by selecting "Comp. skipped" above

Analyzed program located at URL http://www.complang.tuwien.ac.at/cti/bench/maria/aiakl.pl:

/*-----------------------------------------------------------------------------
	Program: initialization for abstract unification in AKL analyzer
	Author:  Dan Sahlin and Thomas Sjoland
	Date:	 March, 1993

-----------------------------------------------------------------------------*/

%:- entry(init_vars(E1,E2,E1in,E2in),[share([[E1in],[E2in]]),free([E1in,E2in])]).

init_vars(E1,E2,E1init,E2init) :-
	find_all_vars(E1,Vars1),
	find_all_vars(E2,Vars2),
	intersect(Vars1,Vars2,_X,Notin1,Notin2),
	init_vars2(Notin1,E1,E1init),
	init_vars2(Notin2,E2,E2init).

find_all_vars(E,Vars) :-
	find_all_vars2(E,Vars0),
	sort(Vars0,Vars).

find_all_vars2([],[]).
find_all_vars2([Vars=_Values|Es],AllVars) :-
	append(Vars,AllVars1,AllVars),
	find_all_vars2(Es,AllVars1).

init_vars2(Notin,E,Einit) :-
	init_vars3(Notin,E,Einit0),
	sort(Einit0,Einit).

init_vars3([],E,E).
init_vars3([Var|Vars],E,[[Var]=[unbound]|Es]) :-
	init_vars3(Vars,E,Es).

append([],A,A).   % tid 5. 2.9%
append([A|B],C,[A|D]) :-
	append(B,C,D).

intersect(As,[],[],[],As) :- !.
intersect([],Bs,[],Bs,[]) :- !.
intersect([A|As],[B|Bs],Cs,Ds,Es) :-
	(A=B ->
		Cs = [A|Cs2],
		intersect(As,Bs,Cs2,Ds,Es)
	;A@<B ->
		Es = [A|Es2],
		intersect(As,[B|Bs],Cs,Ds,Es2)
	;       Ds = [B|Ds2],
		intersect([A|As],Bs,Cs,Ds2,Es)
	).
/*
:- noparallelize.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%         This piece has been included for the simulation process    %

no_trace_main:- 
	get_query(E1,E2),
	time(_),
	init_vars(E1,E2,E1init,E2init),
	time(T),
	write('Executed in '), write(T), write(' mS.'), nl,
	write('Result '), write(E1init), write(' '), write(E2init), nl.

trace_main(Eventfile):-
	get_query(E1,E2),
	start_event_trace, 
	init_vars(E1,E2,E1init,E2init),
	stop_event_trace,
	save_trace(Eventfile),
	write('Result '), write(E1init), write(' '), write(E2init), nl.

save_trace(X) :-
	write('Saving trace in file '), write(X), write('... '), 
	open(X,write,Y),
	save_event_trace(Y),
	close(X),
	write('done.'), nl.
*/
get_query(E1,E2):- 
	E1 = [X = [a], X = [a],X = [a], X = [a]],
	E2 = [Y = [a], Y = [a],Y = [a], Y = [a]],
	X = [5,7,8,3,2,4,1,6,9,15,17,18,13,12,14,11,16,19,25,27,28,23,22,24,
             21,26,29],
	Y = [15,17,18,13,12,14,11,16,19,35,37,38,33,32,34,5,7,8,3,2,4,1,6,9,
             31,36,39].
/*
time(T) :- statistics(runtime,[_,T]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/