:- use_module(library(random)),
   use_module(library(lists)).

:- op(400,fy,-),
   op(100,fy,transfer),
   op(650,xfy,->),
   op(600,xfy,and),
   op(610,xfy,or),
   op(700,xfy,<).

generatePropVars(1,[p]).
generatePropVars(2,[p,q]).
generatePropVars(3,[p,q,r]).
generatePropVars(4,[p,q,r,t]).
generatePropVars(5,[p,q,r,t,p1]).
generatePropVars(6,[p,q,r,t,p1,p2]).
generatePropVars(7,[p,q,r,t,p1,p2,p3]).
generatePropVars(8,[p,q,r,t,p1,p2,p3,p4]).

generateFormula(PropVars,0,Formula) :- length(PropVars,Length), random(0,Length,Position),nth0(Position,PropVars,Formula),!.
generateFormula(PropVars,Depth,Formula):- random(1,14,Random), NewDepth is Depth - 1, generateFormulaIn(PropVars,Random,NewDepth,Formula).

/*
    15% -A
    15% A and B
    15% A or B
    15% A -> B
    15% A < B
    7% true
    7% false
    7% propositional variable
*/

generateFormulaIn(PropVars,1,Depth,-(A)):- generateFormula(PropVars,Depth,A).
generateFormulaIn(PropVars,2,Depth,-(A)):- generateFormula(PropVars,Depth,A).
generateFormulaIn(PropVars,3,Depth,((A) and (B))):- generateFormula(PropVars,Depth,A),generateFormula(PropVars,Depth,B).
generateFormulaIn(PropVars,4,Depth,((A) and (B))):- generateFormula(PropVars,Depth,A),generateFormula(PropVars,Depth,B).
generateFormulaIn(PropVars,5,Depth,((A) or (B))):- generateFormula(PropVars,Depth,A), generateFormula(PropVars,Depth,B).
generateFormulaIn(PropVars,6,Depth,((A) or (B))):- generateFormula(PropVars,Depth,A), generateFormula(PropVars,Depth,B).
generateFormulaIn(PropVars,7,Depth,((A) -> (B))) :- generateFormula(PropVars,Depth,A), generateFormula(PropVars,Depth,B).
generateFormulaIn(PropVars,8,Depth,((A) -> (B))) :- generateFormula(PropVars,Depth,A), generateFormula(PropVars,Depth,B).
generateFormulaIn(PropVars,9,Depth,((A) < (B))) :- generateFormula(PropVars,Depth,A), generateFormula(PropVars,Depth,B).
generateFormulaIn(PropVars,10,Depth,((A) < (B))) :- generateFormula(PropVars,Depth,A), generateFormula(PropVars,Depth,B).
generateFormulaIn(_,11,_,true).
generateFormulaIn(_,12,_,false).
generateFormulaIn(PropVars,13,_,PropVar) :- length(PropVars,Length),random(0,Length,Position),nth0(Position,PropVars,PropVar).

generateInstanceAxiomSchema(1,PropVars,Depth, ((A) < ((A) or (B))) or ((B) < ((A) or (B)))):-  NewDepth is Depth - 3, generateFormula(PropVars,NewDepth,A), generateFormula(PropVars,NewDepth,B).
generateInstanceAxiomSchema(2,PropVars,Depth, ((A) < (B)) and ((B) < (C)) -> ((A) < (C))) :- NewDepth is Depth - 3, generateFormula(PropVars,NewDepth,A), generateFormula(PropVars,NewDepth,B),generateFormula(PropVars,NewDepth,C).
generateInstanceAxiomSchema(3,PropVars,Depth,((A) < (B)) or ((B) < (A))) :- NewDepth is Depth - 2, generateFormula(PropVars,NewDepth,A), generateFormula(PropVars,NewDepth,B).
generateInstanceAxiomSchema(4,PropVars,Depth,(false < -(A))-> (A)) :- NewDepth is Depth - 3,generateFormula(PropVars,NewDepth,A).
generateInstanceAxiomSchema(5,PropVars,Depth, -(false < (A)) -> (false < (false < (A)))) :- NewDepth is Depth - 3,generateFormula(PropVars,NewDepth,A).
generateInstanceAxiomSchema(6,PropVars,Depth,(false < -(A)) -> (false < -(false < -(A)))) :- NewDepth is Depth - 5,generateFormula(PropVars,NewDepth,A).
generateInstanceAxiomSchema(7,PropVars,Depth,((A) -> ((A) < true))) :- NewDepth is Depth - 2, generateFormula(PropVars,NewDepth,A).
generateInstanceAxiomSchema(8,PropVars,Depth,((A) < true) -> (A)) :- NewDepth is Depth - 2, generateFormula(PropVars,NewDepth,A).
generateInstanceAxiomSchema(9,PropVars,Depth,((A)< (B)) -> (false < -((A) < (B)))):- NewDepth is Depth - 4, generateFormula(PropVars,NewDepth,A),generateFormula(PropVars,NewDepth,B).
generateInstanceAxiomSchema(10,PropVars,Depth,-((A) < (B)) -> (false < ((A) < (B)))) :- NewDepth is Depth -3, generateFormula(PropVars,NewDepth,A),generateFormula(PropVars,NewDepth,B).

chooseAxiomSchema(vtu,Random) :- random(1,7,Random).
chooseAxiomSchema(vwu,7).
chooseAxiomSchema(vcu,8).
chooseAxiomSchema(vta,Random) :- random(9,11,Random).


testValidFormulasIn(_,_,_,0,_) :- timeouts(T), write("Timeouts: "), writeln(T),!.
testValidFormulasIn(Logic,NumVars,Depth,NumFormulas,TimeOutLimit):-
    generatePropVars(NumVars,PropVars),
    chooseAxiomSchema(Logic,Random),
    generateInstanceAxiomSchema(Random,PropVars,Depth,Formula),
    writeln(Formula),
    catch(
    (call_with_time_limit(TimeOutLimit,prova(Formula))),
    time_limit_exceeded,
    (timeouts(T), T2 is T + 1, retractall(timeouts(_)), assert(timeouts(T2)),writeln("Timeout."))),
    NewNumFormulas is NumFormulas - 1,
    testValidFormulasIn(Logic,NumVars,Depth,NewNumFormulas,TimeOutLimit).

testValidFormulas(Logic,NumVars,Depth,NumFormulas,TimeOutLimit) :-
    retractall(timeouts(_)),
    assert(timeouts(0)),
    testValidFormulasIn(Logic,NumVars,Depth,NumFormulas,TimeOutLimit).



