1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2% Copyright 2009-10, Ullrich Hustadt, University of Liverpool
    3%
    4%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    5
    6:- use_module(library(system)).    7:- ensure_loaded([
    8       problems
    9   ]).   10
   11%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   12%
   13% testing(+ProblemClassId)
   14%
   15%     ProblemClassId is e.g. routine, routine_w_test, difficult; see
   16%     definition of problems. 
   17
   18testing(ProblemClassId) :-
   19    problems(ProblemClassId, ProblemList),
   20    test_problem_list(ProblemList).
   21
   22%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   23%
   24% test_problem_list(+OutputStream, +ProblemList)
   25%
   26%     ProblemList is a list of problem identifiers (see problems.pl)
   27
   28test_problem_list([]).
   29
   30test_problem_list([Problem|List]) :-
   31    test_problem(Problem),
   32    test_problem_list(List).
   33
   34%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   35%
   36% test_problem(+ProblemIdentifier)
   37
   38test_problem(ProblemId) :-
   39    write('Testing PDLProver (tree) on '), ttyflush,
   40    shell(hostname), ttyflush,
   41    write('Problem '), print( ProblemId), nl,
   42    ttyflush,
   43    problem(ProblemId, Expected, _Result),
   44    write('Expected Result   '), print(Expected), nl.
   45
   46
   47%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   48
   49validate(yes, unsatisfiable, unsatisfiable) :- !,
   50    write(', WARNING conflict !').
   51
   52validate(no, unsatisfiable, satisfiable) :- !,
   53    write(', WARNING conflict !').
   54
   55validate(no, satisfiable, unsatisfiable) :- !,
   56    write(', WARNING conflict !').
   57
   58validate( _, _, _).
   59
   60%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   61
   62systemCall(CallPredicate,Command) :-
   63        once(systemCall(Command,[],CallPredicate)),
   64        !.
   65systemCall(_CallPredicate,Command) :-
   66        write('SystemCall of '),
   67        write(Command),
   68        write(' failed.'),
   69        nl,
   70        !.
   71
   72systemCall([],CommandString,_) :-
   73        atom_chars(Command,CommandString),
   74        !,
   75        shell(Command).
   76systemCall([],CommandString,shell(Result)) :-
   77        atom_chars(Command,CommandString),
   78        !,
   79        shell(Command,Result).
   80systemCall([A|L],CommandString1,CallPredicate) :-
   81        (number(A) ->
   82            number_chars(A,AC)
   83        ;
   84            (atomic(A) ->
   85                atom_chars(A,AC)
   86            ;
   87                AC = A
   88            )
   89        ),
   90        append(CommandString1,AC,CommandString2),
   91        systemCall(L,CommandString2,CallPredicate).
   92
   93generateSourceFilename(ProblemId,File) :-
   94        generateAtom(['/var/tmp/','pdl-',ProblemId],[],File).
   95
   96generateFilename(Base,Extension,ProblemId,File) :-
   97        generateAtom([Base,ProblemId,Extension],[],File).
   98
   99generateAtom([],AtomString,Atom) :-
  100        atom_chars(Atom,AtomString).
  101generateAtom([A|L],AtomString1,Atom) :-
  102        (number(A) ->
  103            number_chars(A,AC)
  104        ;
  105            (atomic(A) ->
  106                atom_chars(A,AC)
  107            ;
  108                AC = A
  109            )
  110        ),
  111        append(AtomString1,AC,AtomString2),
  112        generateAtom(L,AtomString2,Atom).
  113
  114%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  115
  116prove([],Formula,Result) :-
  117	prove(Formula,Result).
  118prove([_|_],_,_) :-
  119	write('Problem uses axioms.'), nl.
  120
  121prove(Formula,Result) :-
  122	current_prolog_flag(pid,ProblemId),
  123        generateFilename('/var/tmp/pdlProver','.in', ProblemId,PDLProver_Input_File),
  124        generateFilename('/var/tmp/pdlProver','.out',ProblemId,PDLProver_Output_File),
  125	write('Writing PDLProver output to '), write(PDLProver_Output_File), nl,
  126        tell(PDLProver_Input_File),
  127        printFormulaPDLProver(Formula), 
  128	nl,
  129        told,
  130        !,
  131        systemCall(exec,['ulimit -t 1100; time cat ',PDLProver_Input_File,' | /users/lect/ullrich/provers/pdlProver/pdl tree verbose | tee ',PDLProver_Output_File]),
  132%        systemCall(system,['cat ',PDLProver_Output_File]),
  133	Result = unknown,
  134        ttyflush.
  135
  136printFormulaPDLProver(dia(P,A)) :-
  137        write('< '),
  138	printProgramPDLProver(P),
  139	write(' > '),
  140        printFormulaPDLProver(A).
  141printFormulaPDLProver(box(P,A)) :-
  142        write('[ '),
  143	printProgramPDLProver(P),
  144	write(' ] '),
  145        printFormulaPDLProver(A).
  146printFormulaPDLProver(and(A,B)) :-
  147        write('('),
  148        printFormulasPDLProver(' & ',[A,B]),
  149        write(')').
  150printFormulaPDLProver(equiv(A,B)) :-
  151        write('('),
  152        printFormulasPDLProver(' <=> ',[A,B]),
  153        write(')').
  154printFormulaPDLProver(implies(A,B)) :-
  155        write('('),
  156        printFormulasPDLProver(' => ',[A,B]),
  157        write(')').
  158printFormulaPDLProver(or(A,B)) :-
  159        write('('),
  160        printFormulasPDLProver(' | ',[A,B]),
  161        write(')').
  162printFormulaPDLProver(not(A)) :-
  163        write('~('),
  164        printFormulaPDLProver(A),
  165        write(')').
  166printFormulaPDLProver(true) :-
  167        write('True').
  168printFormulaPDLProver(false) :-
  169        write('False').
  170printFormulaPDLProver(A) :-
  171        atomic(A),
  172        write(A).
  173
  174printFormulasPDLProver(_Op,[T1]) :-
  175        printFormulaPDLProver(T1).
  176printFormulasPDLProver(Op,[T1,T2|TL]) :-
  177        printFormulaPDLProver(T1),
  178        write(' '),
  179        write(Op),
  180        write(' '),
  181        printFormulasPDLProver(Op,[T2|TL]).
  182
  183printProgramPDLProver(star(P)) :-
  184	write(' * ('),
  185	printProgramPDLProver(P),
  186	write(')').
  187printProgramPDLProver(plus(P)) :-
  188	printProgramPDLProver(comp(P,star(P))).
  189printProgramPDLProver(test(A)) :-
  190	write(' ? ('),
  191	printFormulaPDLProver(A),
  192	write(')').
  193printProgramPDLProver(comp(P,Q)) :-
  194	write('('),
  195	printProgramPDLProver(P),
  196	write(' ; '),
  197	printProgramPDLProver(Q),
  198	write(')').
  199printProgramPDLProver(or(P,Q)) :-
  200	write('('),
  201	printProgramPDLProver(P),
  202	write(' + '),
  203	printProgramPDLProver(Q),
  204	write(')').
  205printProgramPDLProver(id) :-
  206	write('? True').
  207printProgramPDLProver(P) :-
  208	atomic(P),
  209	write(P)