1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%
    3% Copyright 2003, Renate Schmidt, University of Manchester
    4%
    5%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    6
    7%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    8%
    9% testing(+ProblemClassId)
   10%
   11%     ProblemClassId is e.g. routine, routine_w_test, difficult; see
   12%     definition of problems. 
   13
   14testing(ProblemClassId) :-
   15    problems(ProblemClassId, ProblemList),
   16    create_test_output_file,
   17    test_problem_list(test_output, ProblemList),
   18    close(test_output).
   19
   20%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   21%
   22% test_problem_list(+OutputStream, +ProblemList)
   23%
   24%     ProblemList is a list of problem identifiers (see problems.pl)
   25
   26test_problem_list(_, []).
   27
   28test_problem_list(Output, [Problem|List]) :-
   29    test_problem(Output, Problem),
   30    test_problem_list(Output, List).
   31
   32%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   33%
   34% test_problem(+ProblemIdentifier)
   35
   36test_problem(ProblemId) :-
   37    current_output(Output),
   38    test_problem(Output, ProblemId).
   39
   40test_problem(Output, ProblemId) :-
   41    nl(Output),
   42    write(Output, 'pdl-tableau Version 1.1'), nl(Output),
   43    write('Testing on '), ttyflush,
   44    unix(system(hostname)), ttyflush,
   45    write(Output, 'Problem '), print(Output, ProblemId), nl(Output),
   46    write('Problem '), print(ProblemId),
   47    getRuntime(T0),
   48    problem(ProblemId, Expected, Result),
   49    getRuntime(T1),
   50    T is T1 - T0,
   51    write(Output, 'Result   '), print(Output, Result), nl(Output),
   52    write('Result   '), print(Result), nl,
   53    get_proof_steps_counter(StepsNumber),
   54    writef('Inference steps required: %4r', [StepsNumber]), nl,
   55    format('Runtime                 : ~3f~n', [T/1000]),
   56    get_sat_reuse_counter(SatReuseNumber),
   57    predicate_property(consistent(_,_,_),number_of_clauses(SatStoreNumber)),
   58    writef('Sat   sets stored: %4r', [SatStoreNumber]), nl,
   59    writef('Sat   set  reuse : %4r times', [SatReuseNumber]), nl,
   60    get_unsat_reuse_counter(UnsatReuseNumber),
   61    predicate_property(inconsistent(_),number_of_clauses(UnsatStoreNumber)),
   62    writef('Unsat sets stored: %4r', [UnsatStoreNumber]), nl,
   63    writef('Unsat set  reuse : %4r times', [UnsatReuseNumber]), nl,
   64    write(Output, 'Expected '), 
   65    get_negate_first(Flag),
   66    (Flag = yes ->
   67         write(Output, 'unknown  --  ')
   68         ;
   69         true
   70    ),
   71    print(Output, Expected), 
   72    validate(Output, Flag, Result, Expected),
   73    nl(Output), nl(Output),
   74    write('Expected '), 
   75    get_negate_first(Flag),
   76    (Flag = yes ->
   77         write('unknown  --  ')
   78         ;
   79         true
   80    ),
   81    print(Expected), 
   82    validate(Flag, Result, Expected),
   83    nl, nl.
   84
   85
   86%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   87
   88validate(Output, yes, unsatisfiable, unsatisfiable) :- !,
   89    write(Output, ', WARNING conflict !').
   90
   91validate(Output, no, unsatisfiable, satisfiable) :- !,
   92    write(Output, ', WARNING conflict !').
   93
   94validate(Output, no, satisfiable, unsatisfiable) :- !,
   95    write(Output, ', WARNING conflict !').
   96
   97validate(_, _, _, _).
   98
   99%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  100
  101validate(yes, unsatisfiable, unsatisfiable) :- !,
  102    write(', WARNING conflict !').
  103
  104validate(no, unsatisfiable, satisfiable) :- !,
  105    write(', WARNING conflict !').
  106
  107validate(no, satisfiable, unsatisfiable) :- !,
  108    write(', WARNING conflict !').
  109
  110validate(_, _, _).
  111
  112%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  113
  114test_formula(Formula) :-
  115    write('pdl-tableau 1.1'), nl,
  116    getRuntime(T0),
  117    satisfiable(Formula,Result),
  118    getRuntime(T1),
  119    T is T1 - T0,
  120    write('Result   '), print(Result), nl,
  121    get_proof_steps_counter(StepsNumber),
  122    writef('Inference steps required: %4r', [StepsNumber]), nl,
  123    format('Runtime                 : ~3f~n', [T/1000]),
  124    get_sat_reuse_counter(SatReuseNumber),
  125    predicate_property(consistent(_,_,_),number_of_clauses(SatStoreNumber)),
  126    writef('Sat   sets stored: %4r', [SatStoreNumber]), nl,
  127    writef('Sat   set  reuse : %4r times', [SatReuseNumber]), nl,
  128    get_unsat_reuse_counter(UnsatReuseNumber),
  129    predicate_property(inconsistent(_),number_of_clauses(UnsatStoreNumber)),
  130    writef('Unsat sets stored: %4r', [UnsatStoreNumber]), nl,
  131    writef('Unsat set  reuse : %4r times', [UnsatReuseNumber]), nl,
  132    nl, !.
  133
  134%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  135
  136test_file(File) :-
  137    write('pdl-tableau 1.1'), nl,
  138    see(File),
  139    read(Formula),
  140    seen,
  141    getRuntime(T0),
  142    satisfiable(Formula,Result),
  143    getRuntime(T1),
  144    T is T1 - T0,
  145    write('Result   '), print(Result), nl,
  146    get_proof_steps_counter(StepsNumber),
  147    writef('Inference steps required: %4r', [StepsNumber]), nl,
  148    format('Runtime                 : ~3f~n', [T/1000]),
  149    get_sat_reuse_counter(SatReuseNumber),
  150    predicate_property(consistent(_,_,_),number_of_clauses(SatStoreNumber)),
  151    writef('Sat   sets stored: %4r', [SatStoreNumber]), nl,
  152    writef('Sat   set  reuse : %4r times', [SatReuseNumber]), nl,
  153    get_unsat_reuse_counter(UnsatReuseNumber),
  154    predicate_property(inconsistent(_),number_of_clauses(UnsatStoreNumber)),
  155    writef('Unsat sets stored: %4r', [UnsatStoreNumber]), nl,
  156    writef('Unsat set  reuse : %4r times', [UnsatReuseNumber]), nl,
  157    nl, !.
  158
  159
  160%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  161
  162list_difference([], _, []).
  163
  164list_difference(List, [], List).
  165
  166list_difference(ListA, [Eliminate|ListB], ListDiff) :-
  167    select(Eliminate, ListA, ListAminus), !,
  168    list_difference(ListAminus,ListB, ListDiff).
  169    
  170list_difference(ListA, [_|ListB], ListDiff) :-
  171    list_difference(ListA, ListB, ListDiff).
  172
  173%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  174% getRuntime(-RT)
  175% RT is the runtime used so far by the process
  176
  177getRuntime(RT) :-
  178        system:statistics(cputime,RT0),
  179        RT is integer(RT0*1000)