% ------------------------------------------------------------------------------------------------------
% Test the Prova Rule Engine
%
% In tree(n,k) a0 is at the root of a k-branching tree of depth n
% in which every literal occurs once. The test is a propositional LP
%
% tree(n,k) = rule(a0,n,k)
% 
% where, if p is a literal, n>0, r is a new unique label, 
% and a1,a2,...,ak are new unique literal:
%
% rules(p,n,k) = 
% p :- a1,a2,...,ak.
% rules(a1,n-1,k)
% rules(a2,n-1,k)
% ...
% rules(ak,n-1,k)
%
% and: rules(p,0,k) = p
%
% A query a0? will use every rule and fact. With goal memoization
% ------------------------------------------------------------------------------------------------------

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

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


a111().
a112().
a11() :- cache(a111()), cache(a112()), cache(a113()).
a113().
a121().
a122().
a12() :- cache(a121()), cache(a122()), cache(a123()).
a123().
a1() :- cache(a11()), cache(a12()), cache(a13()).
a131().
a132().
a13() :- cache(a131()), cache(a132()), cache(a133()).
a133().
a211().
a212().
a21() :- cache(a211()), cache(a212()), cache(a213()).
a213().
a221().
a222().
a22() :- cache(a221()), cache(a222()), cache(a223()).
a223().
a2() :- cache(a21()), cache(a22()), cache(a23()).
a231().
a232().
a23() :- cache(a231()), cache(a232()), cache(a233()).
a233().
a0() :- cache(a1()), cache(a2()), cache(a3()).
a311().
a312().
a31() :- cache(a311()), cache(a312()), cache(a313()).
a313().
a321().
a322().
a32() :- cache(a321()), cache(a322()), cache(a323()).
a323().
a3() :- cache(a31()), cache(a32()), cache(a33()).
a331().
a332().
a33() :- cache(a331()), cache(a332()), cache(a333()).
a333().



% Tests


testTrees() :-
println(["Test propositional Tree 1: depth n = 3  width k = 3 variables v=1 with goal memoization"]),
println(["----------------------------"]),
C1=rbsla.utils.WebsiteAvailable.getDate(),
T1=C1.getTimeInMillis(),


a0(),

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(testTrees()).
:-solve(testTrees()).
:-solve(testTrees()).
:-solve(testTrees()).
:-solve(testTrees()).
:-solve(testTrees()).
