% ------------------------------------------------------------------------------------------------------
% Test the Prova Rule Engine
%
% In dag(n,k,v) (directed acyclic graph) a0 is at the root of a k-branching tree
% of depth n in which every literal occurs k times and which has v variables. 
% The test is datalog with 
% goal memoization
%
% dag(n,k,v) =
% a0(X1,..Xv) :- a1(X1,..Xv), a2(X1,..Xv), ..., ak(X1,..Xv).
% a1(X1,..Xv) :- a2(X1,..Xv), a3(X1,..Xv), ..., ak+1(X1,..Xv).
%     ...
% ank(X1,..Xv) :- ank+1(X1,..Xv), ank+2(X1,..Xv), ..., ank+k(X1,..Xv). % rules
%
% ank+1(x1,..xv). ank+2(x1,..xv). ... ank+k(x1,..xv).  % facts
%
% A query a0? will use and memorize every rule and fact.
% ------------------------------------------------------------------------------------------------------

% include basic predicates
:-eval(consult('ContractLog/math.prova')).

% set up cache localy (memorize subgoals for one query)
cacheTimeout(0).


a0(Y) :- cache(a1(Y)), cache(a2(Y)), cache(a3(Y)).
a1(Y) :- cache(a2(Y)),cache(a3(Y)),cache(a4(Y)).
a2(Y) :- cache(a3(Y)),cache(a4(Y)),cache(a5(Y)).
a3(Y) :- cache(a4(Y)),cache(a5(Y)),cache(a6(Y)).
a4(Y) :- cache(a5(Y)),cache(a6(Y)),cache(a7(Y)).
a5(Y) :- cache(a6(Y)),cache(a7(Y)),cache(a8(Y)).
a6(Y) :- cache(a7(Y)),cache(a8(Y)),cache(a9(Y)).
a7(Y) :- cache(a8(Y)),cache(a9(Y)),cache(a10(Y)).
a8(Y) :- cache(a9(Y)), cache(a10(Y)),cache(a11(Y)).
a9(Y) :- cache(a10(Y)), cache(a11(Y)),cache(a12(Y)).
a10(Y).
a11(Y).
a12(Y).

% Tests


testDag(Y) :-
println(["TestDAG 1: depth n = 3  width k = 3 with goal memoization and one variable"]),
println(["----------------------------"]),
C1=rbsla.utils.WebsiteAvailable.getDate(),
T1=C1.getTimeInMillis(),


a0(Y),

C2=rbsla.utils.WebsiteAvailable.getDate(),
T2=C2.getTimeInMillis(),
math_sub(T2,T1,DIF),
println(["Duration:",DIF]),
println(["-----------------------------"]).

% 6 Experiments in a row - First is only for garbage removal of parsing

:-solve(testDag(Y)).
:-solve(testDag(Y)).
:-solve(testDag(Y)).
:-solve(testDag(Y)).
:-solve(testDag(Y)).
:-solve(testDag(Y)).
