1 /*-----------------------------------------------------------------------
2
3 File : che_clausefeatures.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Functions for determining features of clauses.
10
11 Copyright 1998, 1999 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Mon Sep 28 19:17:50 MET DST 1998
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "che_clausefeatures.h"
25
26
27
28 /*---------------------------------------------------------------------*/
29 /* Global Variables */
30 /*---------------------------------------------------------------------*/
31
32
33 /*---------------------------------------------------------------------*/
34 /* Forward Declarations */
35 /*---------------------------------------------------------------------*/
36
37
38 /*---------------------------------------------------------------------*/
39 /* Internal Functions */
40 /*---------------------------------------------------------------------*/
41
42
43 /*-----------------------------------------------------------------------
44 //
45 // Function: term_depth_info_add()
46 //
47 // Change term depth to depthsum, adapt depthmax, increase count by
48 // one. Return the new max.
49 //
50 // Global Variables: -
51 //
52 // Side Effects : -
53 //
54 /----------------------------------------------------------------------*/
55
term_depth_info_add(Term_p term,long * depthmax,long * depthsum,long * count)56 static long term_depth_info_add(Term_p term, long* depthmax, long*
57 depthsum, long* count)
58 {
59 long depth = TermDepth(term);
60
61 (*depthsum)+=depth;
62 (*count)++;
63 if(depth > *depthmax)
64 {
65 (*depthmax) = depth;
66 }
67 return *depthmax;
68 }
69
70
71 /*-----------------------------------------------------------------------
72 //
73 // Function: eqn_tptp_depth_info_add()
74 //
75 // Add term depth info according to TPTP interpretation (all
76 // literals are conventional, equations are interpreted as equal(t1,
77 // t2)).
78 //
79 // Global Variables: -
80 //
81 // Side Effects : -
82 //
83 /----------------------------------------------------------------------*/
84
eqn_tptp_depth_info_add(Eqn_p eqn,long * depthmax,long * depthsum,long * count)85 static long eqn_tptp_depth_info_add(Eqn_p eqn, long* depthmax, long*
86 depthsum, long* count)
87 {
88 if(EqnIsEquLit(eqn))
89 {
90 term_depth_info_add(eqn->lterm, depthmax, depthsum, count);
91 term_depth_info_add(eqn->rterm, depthmax, depthsum, count);
92 }
93 else
94 {
95 int i;
96 for(i=0; i<eqn->lterm->arity; i++)
97 {
98 term_depth_info_add(eqn->lterm->args[i], depthmax, depthsum,
99 count);
100 }
101 }
102 return *depthmax;
103 }
104
105
106
107 /*---------------------------------------------------------------------*/
108 /* Exported Functions */
109 /*---------------------------------------------------------------------*/
110
111 /*-----------------------------------------------------------------------
112 //
113 // Function: ClauseCountExtSymbols()
114 //
115 // Return the number of different external function symbols in
116 // clause.
117 //
118 // Global Variables: -
119 //
120 // Side Effects : -
121 //
122 /----------------------------------------------------------------------*/
123
ClauseCountExtSymbols(Clause_p clause,Sig_p sig,long min_arity)124 int ClauseCountExtSymbols(Clause_p clause, Sig_p sig, long min_arity)
125 {
126 long *dist_array = SizeMalloc((sig->f_count+1)*sizeof(long));
127 FunCode i;
128 int res =0;
129
130 for(i=0; i<=sig->f_count; i++)
131 {
132 dist_array[i] = 0;
133 }
134 ClauseAddSymbolDistribution(clause, dist_array);
135
136 for(i=sig->internal_symbols+1; i<=sig->f_count; i++)
137 {
138 if((SigFindArity(sig, i)>=min_arity) && dist_array[i])
139 {
140 res++;
141 }
142 }
143 SizeFree(dist_array, (sig->f_count+1)*sizeof(long));
144
145 return res;
146 }
147
148 /*-----------------------------------------------------------------------
149 //
150 // Function: TermAddVarDistribution()
151 //
152 // Count the variable occurences in term. Return the largest
153 // (negated) variable f_count.
154 //
155 // Global Variables: -
156 //
157 // Side Effects : -
158 //
159 /----------------------------------------------------------------------*/
160
TermAddVarDistribution(Term_p term,PDArray_p dist_array)161 FunCode TermAddVarDistribution(Term_p term, PDArray_p dist_array)
162 {
163 PStack_p stack = PStackAlloc();
164 long count;
165 FunCode max_var = 0;
166 assert(term);
167
168 PStackPushP(stack, term);
169
170 while(!PStackEmpty(stack))
171 {
172 term = PStackPopP(stack);
173
174 if(!TermIsVar(term))
175 {
176 int i;
177
178 assert(term->f_code > 0);
179
180 for(i=0; i<term->arity; i++)
181 {
182 assert(term->args);
183 PStackPushP(stack, term->args[i]);
184 }
185 }
186 else
187 {
188 count = PDArrayElementInt(dist_array, -(term->f_code));
189 count++;
190 max_var = MAX(max_var, -(term->f_code));
191 PDArrayAssignInt(dist_array, -(term->f_code), count);
192 }
193 }
194 PStackFree(stack);
195
196 return max_var;
197 }
198
199
200 /*-----------------------------------------------------------------------
201 //
202 // Function: EqnAddVarDistribution()
203 //
204 // As TermAddVarDistribution(), but for equations.
205 //
206 // Global Variables: -
207 //
208 // Side Effects : -
209 //
210 /----------------------------------------------------------------------*/
211
EqnAddVarDistribution(Eqn_p eqn,PDArray_p dist_array)212 FunCode EqnAddVarDistribution(Eqn_p eqn, PDArray_p dist_array)
213 {
214 FunCode lvars, rvars;
215
216 lvars = TermAddVarDistribution(eqn->lterm, dist_array);
217 rvars = TermAddVarDistribution(eqn->rterm, dist_array);
218
219 return MAX(lvars, rvars);
220 }
221
222
223 /*-----------------------------------------------------------------------
224 //
225 // Function: EqnListAddVarDistribution()
226 //
227 // As TernAddVarDistribution, for lists of equations.
228 //
229 // Global Variables: -
230 //
231 // Side Effects : -
232 //
233 /----------------------------------------------------------------------*/
234
EqnListAddVarDistribution(Eqn_p list,PDArray_p dist_array)235 FunCode EqnListAddVarDistribution(Eqn_p list, PDArray_p dist_array)
236 {
237 FunCode max_var = 0, local;
238
239 while(list)
240 {
241 local = EqnAddVarDistribution(list, dist_array);
242 max_var = MAX(max_var, local);
243 list = list->next;
244 }
245 return max_var;
246 }
247
248
249 /*-----------------------------------------------------------------------
250 //
251 // Function: ClauseCountVariableSet()
252 //
253 // Return the number of different variables in
254 // clause.
255 //
256 // Global Variables: -
257 //
258 // Side Effects : -
259 //
260 /----------------------------------------------------------------------*/
261
ClauseCountVariableSet(Clause_p clause)262 long ClauseCountVariableSet(Clause_p clause)
263 {
264 PDArray_p dist_array = PDIntArrayAlloc(20,20);
265 FunCode max_var,i;
266 long res = 0;
267
268 max_var = ClauseAddVarDistribution(clause, dist_array);
269
270 for(i=1; i<=max_var; i++)
271 {
272 if(PDArrayElementInt(dist_array, i))
273 {
274 res++;
275 }
276 }
277 PDArrayFree(dist_array);
278 return res;
279 }
280
281
282 /*-----------------------------------------------------------------------
283 //
284 // Function: ClauseCountSingletonSet()
285 //
286 // Return the number of different singleton variables in
287 // clause.
288 //
289 // Global Variables: -
290 //
291 // Side Effects : -
292 //
293 /----------------------------------------------------------------------*/
294
ClauseCountSingletonSet(Clause_p clause)295 long ClauseCountSingletonSet(Clause_p clause)
296 {
297 PDArray_p dist_array = PDIntArrayAlloc(20,20);
298 FunCode max_var,i;
299 long res = 0;
300
301 max_var = ClauseAddVarDistribution(clause, dist_array);
302
303 for(i=1; i<=max_var; i++)
304 {
305 if(PDArrayElementInt(dist_array, i)==1)
306 {
307 res++;
308 }
309 }
310 PDArrayFree(dist_array);
311 return res;
312 }
313
314
315 /*-----------------------------------------------------------------------
316 //
317 // Function: ClauseCountMaximalTerms()
318 //
319 // Given an clause, return the number of maximal terms in maximal
320 // literals.
321 //
322 // Global Variables: -
323 //
324 // Side Effects : -
325 //
326 /----------------------------------------------------------------------*/
327
ClauseCountMaximalTerms(Clause_p clause)328 long ClauseCountMaximalTerms(Clause_p clause)
329 {
330 Eqn_p handle;
331 long res = 0;
332
333 for(handle=clause->literals; handle; handle = handle->next)
334 {
335 if(EqnIsMaximal(handle))
336 {
337 res+=EqnCountMaximalLiterals(handle);
338 }
339 }
340 return res;
341 }
342
343
344 /*-----------------------------------------------------------------------
345 //
346 // Function: ClauseCountMaximalLiterals()
347 //
348 // Given an clause, return the number of maximal literals.
349 //
350 // Global Variables: -
351 //
352 // Side Effects : -
353 //
354 /----------------------------------------------------------------------*/
355
ClauseCountMaximalLiterals(Clause_p clause)356 long ClauseCountMaximalLiterals(Clause_p clause)
357 {
358 Eqn_p handle;
359 long res = 0;
360
361 for(handle=clause->literals; handle; handle = handle->next)
362 {
363 if(EqnIsMaximal(handle))
364 {
365 res++;
366 }
367 }
368 return res;
369 }
370
371
372 /*-----------------------------------------------------------------------
373 //
374 // Function: ClauseCountUnorientableLiterals()
375 //
376 // Given an clause, return the number of unorientable literals.
377 //
378 // Global Variables: -
379 //
380 // Side Effects : -
381 //
382 /----------------------------------------------------------------------*/
383
ClauseCountUnorientableLiterals(Clause_p clause)384 long ClauseCountUnorientableLiterals(Clause_p clause)
385 {
386 Eqn_p handle;
387 long res = 0;
388
389 for(handle=clause->literals; handle; handle = handle->next)
390 {
391 if(!EqnIsOriented(handle))
392 {
393 res++;
394 }
395 }
396 return res;
397 }
398
399
400 /*-----------------------------------------------------------------------
401 //
402 // Function: ClauseTPTPDepthInfoAdd()
403 //
404 // Add the term depth information according to TPTP interpretation
405 // (see eqn_tptp_depth_info_add()).
406 //
407 // Global Variables: -
408 //
409 // Side Effects : -
410 //
411 /----------------------------------------------------------------------*/
412
ClauseTPTPDepthInfoAdd(Clause_p clause,long * depthmax,long * depthsum,long * count)413 long ClauseTPTPDepthInfoAdd(Clause_p clause, long* depthmax, long*
414 depthsum, long* count)
415 {
416 Eqn_p handle;
417
418 for(handle = clause->literals; handle; handle=handle->next)
419 {
420 eqn_tptp_depth_info_add(handle, depthmax, depthsum, count);
421 }
422 return *depthmax;
423 }
424
425 /*-----------------------------------------------------------------------
426 //
427 // Function: ClauseInfoPrint()
428 //
429 // Print a lot of information about clause in the form
430 // info(d0,...,dn) with
431 //
432 // d0: Clause ident (number)
433 // d1: Proof depth
434 // d2: Proof length
435 // d3: Symbol count
436 // d4: Clause depth
437 // d5: Literal number
438 // d6: Number of variable occurences
439 // d7: Number of different variables
440 //
441 // Global Variables: -
442 //
443 // Side Effects : -
444 //
445 /----------------------------------------------------------------------*/
446
ClauseInfoPrint(FILE * out,Clause_p clause)447 void ClauseInfoPrint(FILE* out, Clause_p clause)
448 {
449 fprintf(out, "info(%ld, %ld, %ld, %ld, %ld, %d, %ld, %ld)",
450 clause->ident,
451 clause->proof_depth,
452 clause->proof_size,
453 (long)ClauseWeight(clause, 1, 1, 1, 1, 1, false),
454 ClauseDepth(clause),
455 ClauseLiteralNumber(clause),
456 (long)ClauseWeight(clause, 0, 1, 1, 1, 1, false),
457 ClauseCountVariableSet(clause));
458 }
459
460
461 /*-----------------------------------------------------------------------
462 //
463 // Function: ClauseLinePrint()
464 //
465 // Print the clause and potential information on a single line.
466 //
467 // Global Variables: -
468 //
469 // Side Effects : Output
470 //
471 /----------------------------------------------------------------------*/
472
ClauseLinePrint(FILE * out,Clause_p clause,bool printinfo)473 void ClauseLinePrint(FILE* out, Clause_p clause, bool printinfo)
474 {
475 ClausePrint(out, clause, true);
476 if(printinfo)
477 {
478 fputs(" # ", out);
479 ClauseInfoPrint(out, clause);
480 }
481 fputc('\n', out);
482 }
483
484
485 /*-----------------------------------------------------------------------
486 //
487 // Function: ClausePropInfoPrint()
488 //
489 // Print a clause and certain statistical information about it as a
490 // comment.
491 //
492 // Global Variables: -
493 //
494 // Side Effects : Output
495 //
496 /----------------------------------------------------------------------*/
497
ClausePropInfoPrint(FILE * out,Clause_p clause)498 void ClausePropInfoPrint(FILE* out, Clause_p clause)
499 {
500 assert(clause);
501
502 fprintf(out, "# ");
503 ClausePCLPrint(out, clause, true);
504 fprintf(out,
505 "\n"
506 "# Standardweight: %6ld\n"
507 "# Symbol count : %6ld\n"
508 "# F. symbols : %6ld\n"
509 "# Variables : %6ld\n"
510 "# Constants : %6ld\n"
511 "# P. symbols : %6ld\n"
512 "# Depth : %6ld\n"
513 "# Literals : %6d\n"
514 "# ...positive: %6d\n"
515 "# ...negative: %6d\n",
516 (long)ClauseStandardWeight(clause),
517 (long)ClauseSymTypeWeight(clause, 1,1,1,1,1,1,1),
518 (long)ClauseSymTypeWeight(clause, 1,1,1,0,1,0,0),
519 (long)ClauseSymTypeWeight(clause, 1,1,1,1,0,0,0),
520 (long)ClauseSymTypeWeight(clause, 1,1,1,0,0,1,0),
521 (long)ClauseSymTypeWeight(clause, 1,1,1,0,0,0,1),
522 ClauseDepth(clause),
523 ClauseLiteralNumber(clause),
524 clause->pos_lit_no,
525 clause->neg_lit_no);
526 }
527
528
529 /*---------------------------------------------------------------------*/
530 /* End of File */
531 /*---------------------------------------------------------------------*/
532
533
534
535
536
537
538
539
540