5
6:- use_module(library(system)). 7:- ensure_loaded([
8 problems
9 ]). 10
17
18testing(ProblemClassId) :-
19 problems(ProblemClassId, ProblemList),
20 test_problem_list(ProblemList).
21
27
28test_problem_list([]).
29
30test_problem_list([Problem|List]) :-
31 test_problem(Problem),
32 test_problem_list(List).
33
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
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
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
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]),
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)