
tst:- [tests].

rtest(I):- 
    randF(C),!,
    F = and(C,not(C)),
    concat(problem,I,PFile),
    tell(PFile),
    write(F),
    told,!,
    concat('dimacs_file',I,File),
    rewrite(F,File),!.


randF(F):-
    T is random(5),
    symType(T,Type,R),
    S is random(R),
    sym(Type,S,Sym),
    rnd(0,Type,Sym,F),!.


rnd(_,p,P,P):-!.

rnd(D,u,U,Res):-
    T is random(5),
    modify(D,T,TT),
    symType(TT,Type,R),
    S is random(R),
    sym(Type,S,Sym),
    DD is D + 1,
    rnd(DD,Type,Sym,A0),
    Res =.. [U,A0],!.

rnd(D,m,M,Res):-
    T is random(5),    
    modify(D,T,TT),
    symType(TT,Type,R),
    S is random(R),
    sym(Type,S,Sym),
    DD is D + 1,
    rnd(DD,Type,Sym,A0),
    Res =.. [M,r,A0],!.

rnd(D,b,B,Res):-
    T is random(5),   
    modify(D,T,TT),
    symType(TT,Type,R),
    S is random(R),
    sym(Type,S,Sym),
    DD is D + 1,
    rnd(DD,Type,Sym,A0),

    T1 is random(5),   
    modify(D,T1,TT1),
    symType(TT1,Type1,R1),
    S1 is random(R1),
    sym(Type1,S1,Sym1),
    rnd(DD,Type1,Sym1,A1),

    Res =.. [B,A0,A1],!.


modify(D,_,1):-
    D > 8,!.
modify(D,_,2):-
    D > 6,!.
modify(D,_,3):-
    D > 4,!.
modify(_,X,X).


symType(0,p,2).
symType(1,p,2).
symType(2,m,2).
symType(3,u,2).
symType(4,b,3).


sym(m,0,all).
sym(m,1,some).
sym(u,0,not).
sym(u,1,not).
sym(b,0,and).
sym(b,1,or).
sym(b,2,implies).
sym(p,0,u).
sym(p,1,v).

test:- F = and(implies(u, some(r, not(not(all(r, and(not(not(all(r, some(r, v)))), not(not(some(r, some(r, v)))))))))), not(implies(u, some(r, not(not(all(r, and(not(not(all(r, some(r, v)))), not(not(some(r, some(r, v)))))))))))),
	write(F),
	rewrite(F,'dimacs_file').

test1:- F = and(all(r,all(r,or(p,q))),and(some(r,all(r,or(s,t))),and(some(r,some(r,or(u,v))),all(r,some(r,or(a,b)))))),
	write(F),
	rewrite(F,'dimacs_file').

test2:- F = and(all(eats,implies(veg,not(meat))),and(some(eats,veg),and(all(eats,and(some(drinks,wine),all(drinks,not(beer)))),some(eats,or(all(eats,meat),some(drinks,beer)))))),
	write(F),
	rewrite(F,'dimacs_file').

test(a):- F = and(all(r,all(r,or(p,q))),some(r,some(r,some(r,or(u,v))))),
	write(F),
	rewrite(F,'dimacs_file').

test(b):- F = and(all(r,some(r,or(p,q))),some(r,some(r,some(r,or(u,v))))),
	write(F),
	rewrite(F,'dimacs_file').

test(c):- F = and(some(r,some(r,or(p,q))),some(r,some(r,some(r,or(u,v))))),
	write(F),
	rewrite(F,'dimacs_file').

test(d):- F = and(some(r,all(r,or(p,q))),some(r,some(r,some(r,or(u,v))))),
	write(F),
	rewrite(F,'dimacs_file').

test(1):- F = and(all(r,all(r,all(r,or(p,q)))),and(some(r,all(r,all(r,or(a,b)))),some(r,some(r,some(r,or(u,v)))))),
	write(F),
	rewrite(F,'dimacs_file').

test(2):- F = and(all(r,all(r,some(r,or(p,q)))),and(some(r,all(r,some(r,or(a,b)))),some(r,some(r,some(r,or(u,v)))))),
	write(F),
	rewrite(F,'dimacs_file').

test(3):- F = and(all(r,some(r,some(r,or(p,q)))),and(some(r,some(r,some(r,or(a,b)))),some(r,some(r,some(r,or(u,v)))))),
	write(F),
	rewrite(F,'dimacs_file').

test(4):- F = and(all(r,some(r,all(r,or(p,q)))),and(some(r,some(r,all(r,or(a,b)))),some(r,some(r,some(r,or(u,v)))))),
	write(F),
	rewrite(F,'dimacs_file').


test(5):- F = and(all(r,some(r,p)),some(r,all(r,not(p)))),
	write(F),
	rewrite(F,'dimacs_file').

