1 /*-----------------------------------------------------------------------
2
3 File : che_clausesetfeatures.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Functions for calculating certain features of clause sets.
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> Tue Sep 29 02:50:34 MET DST 1998
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "che_clausesetfeatures.h"
25
26
27 /*---------------------------------------------------------------------*/
28 /* Global Variables */
29 /*---------------------------------------------------------------------*/
30
31
32 /*---------------------------------------------------------------------*/
33 /* Forward Declarations */
34 /*---------------------------------------------------------------------*/
35
36
37 /*---------------------------------------------------------------------*/
38 /* Internal Functions */
39 /*---------------------------------------------------------------------*/
40
41
42
43 /*---------------------------------------------------------------------*/
44 /* Exported Functions */
45 /*---------------------------------------------------------------------*/
46
47 /*-----------------------------------------------------------------------
48 //
49 // Function: SpecLimitsAlloc()
50 //
51 // Allocate an initialized SpecLimitsCell.
52 //
53 // Global Variables: -
54 //
55 // Side Effects : Memory operations
56 //
57 /----------------------------------------------------------------------*/
58
SpecLimitsAlloc(void)59 SpecLimits_p SpecLimitsAlloc(void)
60 {
61 SpecLimits_p handle = SpecLimitsCellAlloc();
62
63 handle->ngu_absolute = NGU_ABSOLUTE;
64 if(NGU_ABSOLUTE)
65 {
66 handle->ngu_few_limit = NGU_FEW_ABSDEFAULT;
67 handle->ngu_many_limit = NGU_MANY_ABSDEFAULT;
68 }
69 else
70 {
71 handle->ngu_few_limit = NGU_FEW_DEFAULT;
72 handle->ngu_many_limit = NGU_MANY_DEFAULT;
73 }
74 handle->gpc_absolute = GPC_ABSOLUTE;
75 if(GPC_ABSOLUTE)
76 {
77 handle->gpc_few_limit = GPC_FEW_ABSDEFAULT;
78 handle->gpc_many_limit = GPC_MANY_ABSDEFAULT;
79 }
80 else
81 {
82 handle->gpc_few_limit = GPC_FEW_DEFAULT;
83 handle->gpc_many_limit = GPC_MANY_DEFAULT;
84 }
85 handle->ax_some_limit = AX_SOME_DEFAULT ;
86 handle->ax_many_limit = AX_MANY_DEFAULT ;
87 handle->lit_some_limit = LIT_SOME_DEFAULT ;
88 handle->lit_many_limit = LIT_MANY_DEFAULT ;
89 handle->term_medium_limit = TERM_MED_DEFAULT ;
90 handle->term_large_limit = TERM_LARGE_DEFAULT ;
91 handle->far_sum_medium_limit = FAR_SUM_MED_DEFAULT ;
92 handle->far_sum_large_limit = FAR_SUM_LARGE_DEFAULT;
93 handle->depth_medium_limit = DEPTH_MEDIUM_DEFAULT;
94 handle->depth_deep_limit = DEPTH_DEEP_DEFAULT;
95 handle->symbols_medium_limit = SYMBOLS_MEDIUM_DEFAULT;
96 handle->symbols_large_limit = SYMBOLS_LARGE_DEFAULT;
97
98 handle->predc_medium_limit = PREDC_MEDIUM_DEFAULT;
99 handle->predc_large_limit = PREDC_LARGE_DEFAULT;
100 handle->pred_medium_limit = PRED_MEDIUM_DEFAULT;
101 handle->pred_large_limit = PRED_LARGE_DEFAULT;
102 handle->func_medium_limit = FUNC_MEDIUM_DEFAULT;
103 handle->func_large_limit = FUNC_LARGE_DEFAULT;
104 handle->fun_medium_limit = FUN_MEDIUM_DEFAULT;
105 handle->fun_large_limit = FUN_LARGE_DEFAULT;
106
107 return handle;
108 }
109
110 /*-----------------------------------------------------------------------
111 //
112 // Function: ClauseSetCountGoals()
113 //
114 // Count number of goal clauses.
115 //
116 // Global Variables: -
117 //
118 // Side Effects : -
119 //
120 /----------------------------------------------------------------------*/
121
ClauseSetCountGoals(ClauseSet_p set)122 long ClauseSetCountGoals(ClauseSet_p set)
123 {
124 long res = 0;
125 Clause_p handle;
126
127 for(handle = set->anchor->succ; handle!=set->anchor; handle =
128 handle->succ)
129 {
130 if(ClauseIsGoal(handle))
131 {
132 res++;
133 }
134 }
135 return res;
136 }
137
138 /*-----------------------------------------------------------------------
139 //
140 // Function: ClauseSetCountUnit()
141 //
142 // Count the unit clauses in set.
143 //
144 // Global Variables: -
145 //
146 // Side Effects : -
147 //
148 /----------------------------------------------------------------------*/
149
ClauseSetCountUnit(ClauseSet_p set)150 long ClauseSetCountUnit(ClauseSet_p set)
151 {
152 long res = 0;
153 Clause_p handle;
154
155 for(handle = set->anchor->succ; handle!=set->anchor; handle =
156 handle->succ)
157 {
158 if(ClauseIsUnit(handle))
159 {
160 res++;
161 }
162 }
163 return res;
164 }
165
166
167 /*-----------------------------------------------------------------------
168 //
169 // Function: ClauseSetCountUnitGoals()
170 //
171 // Count the unit goal clauses in set.
172 //
173 // Global Variables: -
174 //
175 // Side Effects : -
176 //
177 /----------------------------------------------------------------------*/
178
ClauseSetCountUnitGoals(ClauseSet_p set)179 long ClauseSetCountUnitGoals(ClauseSet_p set)
180 {
181 long res = 0;
182 Clause_p handle;
183
184 for(handle = set->anchor->succ; handle!=set->anchor; handle =
185 handle->succ)
186 {
187 if(ClauseIsUnit(handle)&&ClauseIsGoal(handle))
188 {
189 res++;
190 }
191 }
192 return res;
193 }
194
195
196 /*-----------------------------------------------------------------------
197 //
198 // Function: ClauseSetCountHorn()
199 //
200 // Count the unit clauses in set.
201 //
202 // Global Variables: -
203 //
204 // Side Effects : -
205 //
206 /----------------------------------------------------------------------*/
207
ClauseSetCountHorn(ClauseSet_p set)208 long ClauseSetCountHorn(ClauseSet_p set)
209 {
210 long res = 0;
211 Clause_p handle;
212
213 for(handle = set->anchor->succ; handle!=set->anchor; handle =
214 handle->succ)
215 {
216 if(ClauseIsHorn(handle))
217 {
218 res++;
219 }
220 }
221 return res;
222 }
223
224 /*-----------------------------------------------------------------------
225 //
226 // Function: ClauseSetCountHornGoals()
227 //
228 // Count the unit clauses in set.
229 //
230 // Global Variables: -
231 //
232 // Side Effects : -
233 //
234 /----------------------------------------------------------------------*/
235
ClauseSetCountHornGoals(ClauseSet_p set)236 long ClauseSetCountHornGoals(ClauseSet_p set)
237 {
238 long res = 0;
239 Clause_p handle;
240
241 for(handle = set->anchor->succ; handle!=set->anchor; handle =
242 handle->succ)
243 {
244 if(ClauseIsHorn(handle)&&ClauseIsGoal(handle))
245 {
246 res++;
247 }
248 }
249 return res;
250 }
251
252
253 /*-----------------------------------------------------------------------
254 //
255 // Function: ClauseSetCountEquational()
256 //
257 // Count number of clauses with at least one equational literal.
258 //
259 // Global Variables: -
260 //
261 // Side Effects : -
262 //
263 /----------------------------------------------------------------------*/
264
ClauseSetCountEquational(ClauseSet_p set)265 long ClauseSetCountEquational(ClauseSet_p set)
266 {
267 long res = 0;
268 Clause_p handle;
269
270 for(handle = set->anchor->succ; handle!=set->anchor; handle =
271 handle->succ)
272 {
273 if(ClauseIsEquational(handle))
274 {
275 res++;
276 }
277 }
278 return res;
279 }
280
281 /*-----------------------------------------------------------------------
282 //
283 // Function: ClauseSetCountPureEquational()
284 //
285 // Count number of clauses which have only equational literals.
286 //
287 // Global Variables: -
288 //
289 // Side Effects : -
290 //
291 /----------------------------------------------------------------------*/
292
ClauseSetCountPureEquational(ClauseSet_p set)293 long ClauseSetCountPureEquational(ClauseSet_p set)
294 {
295 long res = 0;
296 Clause_p handle;
297
298 for(handle = set->anchor->succ; handle!=set->anchor; handle =
299 handle->succ)
300 {
301 if(ClauseIsPureEquational(handle))
302 {
303 res++;
304 }
305 }
306 return res;
307 }
308
309
310 /*-----------------------------------------------------------------------
311 //
312 // Function: ClauseSetCountPosUnits()
313 //
314 // Count number of positive unit clauses.
315 //
316 // Global Variables: -
317 //
318 // Side Effects : -
319 //
320 /----------------------------------------------------------------------*/
321
ClauseSetCountPosUnits(ClauseSet_p set)322 long ClauseSetCountPosUnits(ClauseSet_p set)
323 {
324 long res = 0;
325 Clause_p handle;
326
327 for(handle = set->anchor->succ; handle!=set->anchor; handle =
328 handle->succ)
329 {
330 if(ClauseIsDemodulator(handle))
331 {
332 res++;
333 }
334 }
335 return res;
336 }
337
338
339 /*-----------------------------------------------------------------------
340 //
341 // Function: ClauseSetCountGroundGoals()
342 //
343 // Count number of ground goal clauses.
344 //
345 // Global Variables: -
346 //
347 // Side Effects : -
348 //
349 /----------------------------------------------------------------------*/
350
ClauseSetCountGroundGoals(ClauseSet_p set)351 long ClauseSetCountGroundGoals(ClauseSet_p set)
352 {
353 long res = 0;
354 Clause_p handle;
355
356 for(handle = set->anchor->succ; handle!=set->anchor; handle =
357 handle->succ)
358 {
359 if(ClauseIsGoal(handle) && ClauseIsGround(handle))
360 {
361 res++;
362 }
363 }
364 return res;
365 }
366
367
368 /*-----------------------------------------------------------------------
369 //
370 // Function: ClauseSetCountGround()
371 //
372 // Count number of ground clauses.
373 //
374 // Global Variables: -
375 //
376 // Side Effects : -
377 //
378 /----------------------------------------------------------------------*/
379
ClauseSetCountGround(ClauseSet_p set)380 long ClauseSetCountGround(ClauseSet_p set)
381 {
382 long res = 0;
383 Clause_p handle;
384
385 for(handle = set->anchor->succ; handle!=set->anchor; handle =
386 handle->succ)
387 {
388 if(ClauseIsGround(handle))
389 {
390 res++;
391 }
392 }
393 return res;
394 }
395
396
397 /*-----------------------------------------------------------------------
398 //
399 // Function: ClauseSetCountGroundUnitAxioms()
400 //
401 // Count number of positive ground unit clauses.
402 //
403 // Global Variables: -
404 //
405 // Side Effects : -
406 //
407 /----------------------------------------------------------------------*/
408
ClauseSetCountGroundUnitAxioms(ClauseSet_p set)409 long ClauseSetCountGroundUnitAxioms(ClauseSet_p set)
410 {
411 long res = 0;
412 Clause_p handle;
413
414 for(handle = set->anchor->succ; handle!=set->anchor; handle =
415 handle->succ)
416 {
417 if(ClauseIsDemodulator(handle) && ClauseIsGround(handle))
418 {
419 res++;
420 }
421 }
422 return res;
423 }
424
425
426 /*-----------------------------------------------------------------------
427 //
428 // Function: ClauseSetCountGroundPositiveAxioms()
429 //
430 // Count number of positive ground clauses.
431 //
432 // Global Variables: -
433 //
434 // Side Effects : -
435 //
436 /----------------------------------------------------------------------*/
437
ClauseSetCountGroundPositiveAxioms(ClauseSet_p set)438 long ClauseSetCountGroundPositiveAxioms(ClauseSet_p set)
439 {
440 long res = 0;
441 Clause_p handle;
442
443 for(handle = set->anchor->succ; handle!=set->anchor; handle =
444 handle->succ)
445 {
446 if(ClauseIsPositive(handle) && ClauseIsGround(handle))
447 {
448 res++;
449 }
450 }
451 return res;
452 }
453
454
455 /*-----------------------------------------------------------------------
456 //
457 // Function: ClauseSetCountPositiveAxioms()
458 //
459 // Count number of positive ground clauses.
460 //
461 // Global Variables: -
462 //
463 // Side Effects : -
464 //
465 /----------------------------------------------------------------------*/
466
ClauseSetCountPositiveAxioms(ClauseSet_p set)467 long ClauseSetCountPositiveAxioms(ClauseSet_p set)
468 {
469 long res = 0;
470 Clause_p handle;
471
472 for(handle = set->anchor->succ; handle!=set->anchor; handle =
473 handle->succ)
474 {
475 if(ClauseIsPositive(handle))
476 {
477 res++;
478 }
479 }
480 return res;
481 }
482
483
484 /*-----------------------------------------------------------------------
485 //
486 // Function: ClauseSetCountTPTPRangeRestricted()
487 //
488 // Count number of positive ground clauses.
489 //
490 // Global Variables: -
491 //
492 // Side Effects : -
493 //
494 /----------------------------------------------------------------------*/
495
ClauseSetCountTPTPRangeRestricted(ClauseSet_p set)496 long ClauseSetCountTPTPRangeRestricted(ClauseSet_p set)
497 {
498 long res = 0;
499 Clause_p handle;
500
501 for(handle = set->anchor->succ; handle!=set->anchor; handle =
502 handle->succ)
503 {
504 if(ClauseIsTPTPRangeRestricted(handle))
505 {
506 res++;
507 }
508 }
509 return res;
510 }
511
512
513 /*-----------------------------------------------------------------------
514 //
515 // Function: ClauseSetNonGoundAxiomPart()
516 //
517 // Return the percentage of non-ground clauses among the unit
518 // clauses (0 if no unit clauses exist).
519 //
520 // Global Variables: -
521 //
522 // Side Effects : -
523 //
524 /----------------------------------------------------------------------*/
525
ClauseSetNonGoundAxiomPart(ClauseSet_p set)526 double ClauseSetNonGoundAxiomPart(ClauseSet_p set)
527 {
528 long tmp = ClauseSetCountUnitAxioms(set);
529
530 if(tmp == 0)
531 {
532 return 0.0;
533 }
534 return (tmp-ClauseSetCountGroundUnitAxioms(set))/(double)tmp;
535 }
536
537
538 /*-----------------------------------------------------------------------
539 //
540 // Function: ClauseSetCollectArityInformation()
541 //
542 // Collect information about the arities of function and predicate
543 // symbol arities. Average and sum for function symbols does not
544 // include constants, it does for predicate symbols. Equality is not
545 // counted, Returns number of function symbol constants.
546 //
547 // Global Variables: -
548 //
549 // Side Effects : Memory operations
550 //
551 /----------------------------------------------------------------------*/
552
ClauseSetCollectArityInformation(ClauseSet_p set,Sig_p sig,int * max_fun_arity,int * avg_fun_arity,int * sum_fun_arity,int * max_pred_arity,int * avg_pred_arity,int * sum_pred_arity,int * non_const_funs,int * non_const_preds)553 long ClauseSetCollectArityInformation(ClauseSet_p set, Sig_p sig,
554 int *max_fun_arity,
555 int *avg_fun_arity,
556 int *sum_fun_arity,
557 int *max_pred_arity,
558 int *avg_pred_arity,
559 int *sum_pred_arity,
560 int *non_const_funs,
561 int *non_const_preds)
562 {
563 int max_f_arity = 0,
564 sum_f_arity = 0,
565 f_count = 0,
566 c_count = 0,
567 non_const_p = 0;
568 int max_p_arity = 0,
569 sum_p_arity = 0,
570 p_count = 0;
571 long array_size = sizeof(long)*(sig->f_count+1);
572 long *dist_array = SizeMalloc(array_size);
573 FunCode i;
574
575 for(i=1; i<= sig->f_count; i++)
576 {
577 dist_array[i] = 0;
578 }
579 ClauseSetAddSymbolDistribution(set, dist_array);
580
581 for(i=1; i<= sig->f_count; i++)
582 {
583 if(!SigIsSpecial(sig, i)&&dist_array[i])
584 {
585 short arity = SigFindArity(sig, i);
586 if(SigIsPredicate(sig, i))
587 {
588 max_p_arity = MAX(arity, max_p_arity);
589 sum_p_arity += arity;
590 p_count++;
591 if(arity)
592 {
593 non_const_p++;
594 }
595 }
596 else
597 {
598 if(arity)
599 {
600 max_f_arity = MAX(arity, max_f_arity);
601 sum_f_arity += arity;
602 f_count++;
603 }
604 else
605 {
606 c_count++;
607 }
608 }
609 }
610 }
611 SizeFree(dist_array, array_size);
612
613 *max_fun_arity = max_f_arity;
614 *avg_fun_arity = f_count?sum_f_arity/f_count:0;
615 *sum_fun_arity = sum_f_arity;
616 *max_pred_arity = max_p_arity;
617 *avg_pred_arity = p_count?sum_p_arity/p_count:0;
618 *sum_pred_arity = sum_p_arity;
619 *non_const_funs = f_count;
620 *non_const_preds = non_const_p;
621
622 return c_count;
623 }
624
625
626 /*-----------------------------------------------------------------------
627 //
628 // Function: ClauseSetCountMaximalTerms()
629 //
630 // Count the number of maximal terms in maximal literals in clauses
631 // in set.
632 //
633 // Global Variables: -
634 //
635 // Side Effects : -
636 //
637 /----------------------------------------------------------------------*/
638
ClauseSetCountMaximalTerms(ClauseSet_p set)639 long ClauseSetCountMaximalTerms(ClauseSet_p set)
640 {
641 Clause_p handle;
642 long res = 0;
643
644 for(handle = set->anchor->succ; handle!=set->anchor; handle =
645 handle->succ)
646 {
647 res += ClauseCountMaximalTerms(handle);
648 }
649 return res;
650 }
651
652 /*-----------------------------------------------------------------------
653 //
654 // Function: ClauseSetCountMaximalLiterals()
655 //
656 // Count the number of maximal literals in clauses in set.
657 //
658 // Global Variables: -
659 //
660 // Side Effects : -
661 //
662 /----------------------------------------------------------------------*/
663
ClauseSetCountMaximalLiterals(ClauseSet_p set)664 long ClauseSetCountMaximalLiterals(ClauseSet_p set)
665 {
666 Clause_p handle;
667 long res = 0;
668
669 for(handle = set->anchor->succ; handle!=set->anchor; handle =
670 handle->succ)
671 {
672 res += ClauseCountMaximalLiterals(handle);
673 }
674 return res;
675 }
676
677
678 /*-----------------------------------------------------------------------
679 //
680 // Function: ClauseSetCountVariables()
681 //
682 // Count the number of variables in a clause set, where variables in
683 // different clauses are considered to be distinct.
684 //
685 // Global Variables: -
686 //
687 // Side Effects : By calling ClauseCountVariableSet
688 //
689 /----------------------------------------------------------------------*/
690
ClauseSetCountVariables(ClauseSet_p set)691 long ClauseSetCountVariables(ClauseSet_p set)
692 {
693 Clause_p handle;
694 long res = 0;
695
696 for(handle = set->anchor->succ; handle!=set->anchor; handle =
697 handle->succ)
698 {
699 res += ClauseCountVariableSet(handle);
700 }
701 return res;
702 }
703
704
705 /*-----------------------------------------------------------------------
706 //
707 // Function: ClauseSetCountSingletons()
708 //
709 // Count the number of singletons in a clause set, where variables in
710 // different clauses are considered to be distinct.
711 //
712 // Global Variables: -
713 //
714 // Side Effects : By calling ClauseCountSingletonSet
715 //
716 /----------------------------------------------------------------------*/
717
ClauseSetCountSingletons(ClauseSet_p set)718 long ClauseSetCountSingletons(ClauseSet_p set)
719 {
720 Clause_p handle;
721 long res = 0;
722
723 for(handle = set->anchor->succ; handle!=set->anchor; handle =
724 handle->succ)
725 {
726 res += ClauseCountSingletonSet(handle);
727 }
728 return res;
729 }
730
731
732 /*-----------------------------------------------------------------------
733 //
734 // Function: ClauseSetTPTPDepthInfoAdd()
735 //
736 // Add the depth information in TPTP interpretation to the
737 // variables. See che_clausefeatures.c for more.
738 //
739 // Global Variables:
740 //
741 // Side Effects :
742 //
743 /----------------------------------------------------------------------*/
744
ClauseSetTPTPDepthInfoAdd(ClauseSet_p set,long * depthmax,long * depthsum,long * count)745 long ClauseSetTPTPDepthInfoAdd(ClauseSet_p set, long* depthmax, long*
746 depthsum, long* count)
747 {
748 Clause_p handle;
749
750 for(handle = set->anchor->succ; handle!=set->anchor; handle =
751 handle->succ)
752 {
753 ClauseTPTPDepthInfoAdd(handle, depthmax, depthsum, count);
754 }
755 return *depthmax;
756 }
757
758
759 /*-----------------------------------------------------------------------
760 //
761 // Function: ClauseSetCountUnorientableLiterals()
762 //
763 // Count the number of Unorientable literals in clauses in set.
764 //
765 // Global Variables: -
766 //
767 // Side Effects : -
768 //
769 /----------------------------------------------------------------------*/
770
ClauseSetCountUnorientableLiterals(ClauseSet_p set)771 long ClauseSetCountUnorientableLiterals(ClauseSet_p set)
772 {
773 Clause_p handle;
774 long res = 0;
775
776 for(handle = set->anchor->succ; handle!=set->anchor; handle =
777 handle->succ)
778 {
779 res += ClauseCountUnorientableLiterals(handle);
780 }
781 return res;
782 }
783
784 /*-----------------------------------------------------------------------
785 //
786 // Function: ClauseSetCountEqnLiterals()
787 //
788 // Count the number of equational literals in clauses in set.
789 //
790 // Global Variables: -
791 //
792 // Side Effects : -
793 //
794 /----------------------------------------------------------------------*/
795
ClauseSetCountEqnLiterals(ClauseSet_p set)796 long ClauseSetCountEqnLiterals(ClauseSet_p set)
797 {
798 Clause_p handle;
799 long res = 0;
800
801 for(handle = set->anchor->succ; handle!=set->anchor; handle =
802 handle->succ)
803 {
804 res += ClausePropLitNumber(handle, EPIsEquLiteral);
805 }
806 return res;
807 }
808
809
810 /*-----------------------------------------------------------------------
811 //
812 // Function: ClauseSetMaxStandardWeight()
813 //
814 // Return the standard weight of the largest clause in set (or -1 if
815 // set is empty).
816 //
817 // Global Variables: -
818 //
819 // Side Effects : -
820 //
821 /----------------------------------------------------------------------*/
822
ClauseSetMaxStandardWeight(ClauseSet_p set)823 long ClauseSetMaxStandardWeight(ClauseSet_p set)
824 {
825 long res = -1;
826 Clause_p handle = ClauseSetFindMaxStandardWeight(set);
827
828 if(handle)
829 {
830 res = ClauseStandardWeight(handle);
831 }
832 return res;
833 }
834
835
836 /*-----------------------------------------------------------------------
837 //
838 // Function: ClauseSetTermCells()
839 //
840 // Return the number of term positions in the clause set.
841 //
842 // Global Variables: -
843 //
844 // Side Effects : -
845 //
846 /----------------------------------------------------------------------*/
847
ClauseSetTermCells(ClauseSet_p set)848 long ClauseSetTermCells(ClauseSet_p set)
849 {
850 Clause_p handle;
851 long res = 0;
852
853 for(handle = set->anchor->succ; handle!=set->anchor; handle =
854 handle->succ)
855 {
856 res += ClauseWeight(handle, 1, 1, 1, 1, 1, false);
857 }
858 return res;
859 }
860
861
862 /*-----------------------------------------------------------------------
863 //
864 // Function: ClauseSetMaxLiteralNumber()
865 //
866 // Return the length of the longest clause.
867 //
868 // Global Variables: -
869 //
870 // Side Effects : -
871 //
872 /----------------------------------------------------------------------*/
873
ClauseSetMaxLiteralNumber(ClauseSet_p set)874 long ClauseSetMaxLiteralNumber(ClauseSet_p set)
875 {
876 Clause_p handle;
877 long res = 0;
878
879 for(handle = set->anchor->succ; handle!=set->anchor; handle =
880 handle->succ)
881 {
882 res = MAX(res, ClauseLiteralNumber(handle));
883 }
884 return res;
885 }
886
887
888 /*-----------------------------------------------------------------------
889 //
890 // Function: SpecFeaturesCompute()
891 //
892 // Compute all relevant features for a set of clauses.
893 //
894 // Global Variables: -
895 //
896 // Side Effects : -
897 //
898 /----------------------------------------------------------------------*/
899
SpecFeaturesCompute(SpecFeature_p features,ClauseSet_p set,Sig_p sig)900 void SpecFeaturesCompute(SpecFeature_p features, ClauseSet_p set,
901 Sig_p sig)
902 {
903 long tmp, count;
904
905 features->clauses = set->members;
906 features->goals = ClauseSetCountGoals(set);
907 features->axioms = features->clauses-features->goals;
908
909 features->literals = set->literals;
910 features->term_cells = ClauseSetTermCells(set);
911
912 tmp = 0;
913 count = 0;
914 features->clause_max_depth = 0;
915 ClauseSetTPTPDepthInfoAdd(set,
916 &(features->clause_max_depth),
917 &tmp,
918 &count);
919 features->clause_avg_depth = count?tmp/count:0;
920
921 features->unit = ClauseSetCountUnit(set);
922 features->unitgoals = ClauseSetCountUnitGoals(set);
923 features->unitaxioms = features->unit-features->unitgoals;
924
925 features->horn = ClauseSetCountHorn(set);
926 features->horngoals = ClauseSetCountHornGoals(set);
927 features->hornaxioms = features->horn-features->horngoals;
928
929 features->eq_clauses = ClauseSetCountEquational(set);
930 features->peq_clauses = ClauseSetCountPureEquational(set);
931 features->groundunitaxioms = ClauseSetCountGroundUnitAxioms(set);
932 features->groundgoals = ClauseSetCountGroundGoals(set);
933 features->positiveaxioms = ClauseSetCountPositiveAxioms(set);
934 features->groundpositiveaxioms = ClauseSetCountGroundPositiveAxioms(set);
935 features->fun_const_count =
936 ClauseSetCollectArityInformation(set, sig,
937 &(features->max_fun_arity),
938 &(features->avg_fun_arity),
939 &(features->sum_fun_arity),
940 &(features->max_pred_arity),
941 &(features->avg_pred_arity),
942 &(features->sum_pred_arity),
943 &(features->fun_nonconst_count),
944 &(features->pred_nonconst_count));
945
946 features->goals_are_ground = (features->groundgoals ==
947 features->goals);
948
949 if(features->unitaxioms == features->axioms)
950 {
951 features->axiomtypes = SpecUnit;
952 }
953 else if(features->hornaxioms == features->axioms)
954 {
955 features->axiomtypes = SpecHorn;
956 }
957 else
958 {
959 features->axiomtypes = SpecGeneral;
960 }
961
962 if(features->unitgoals == features->goals)
963 {
964 features->goaltypes = SpecUnit;
965 }
966 else if(features->horngoals == features->goals)
967 {
968 features->goaltypes = SpecHorn;
969 }
970 else
971 {
972 features->goaltypes = SpecGeneral;
973 }
974
975 if(features->peq_clauses == features->clauses)
976 {
977 features->eq_content = SpecPureEq;
978 }
979 else if(features->eq_clauses)
980 {
981 features->eq_content = SpecSomeEq;
982 }
983 else
984 {
985 features->eq_content = SpecNoEq;
986 }
987
988 switch(features->max_fun_arity)
989 {
990 case 0:
991 features->max_fun_ar_class = SpecArity0;
992 break;
993 case 1:
994 features->max_fun_ar_class = SpecArity1;
995 break;
996 case 2:
997 features->max_fun_ar_class = SpecArity2;
998 break;
999 default:
1000 features->max_fun_ar_class = SpecArity3Plus;
1001 break;
1002 }
1003 switch(features->avg_fun_arity)
1004 {
1005 case 0:
1006 features->avg_fun_ar_class = SpecArity0;
1007 break;
1008 case 1:
1009 features->avg_fun_ar_class = SpecArity1;
1010 break;
1011 case 2:
1012 features->avg_fun_ar_class = SpecArity2;
1013 break;
1014 default:
1015 features->avg_fun_ar_class = SpecArity3Plus;
1016 break;
1017 }
1018 features->ng_unit_axioms_part = features->unitaxioms?
1019 ((double)(features->unitaxioms-features->groundunitaxioms)/
1020 (double)(features->unitaxioms))
1021 :0.0;
1022
1023 features->ground_positive_axioms_part = features->positiveaxioms?
1024 ((double)(features->groundpositiveaxioms)/
1025 (double)(features->positiveaxioms))
1026 :0.0;
1027
1028
1029 }
1030
1031
1032 /*-----------------------------------------------------------------------
1033 //
1034 // Function: SpecFeaturesAddEval()
1035 //
1036 // Add the cheap, subjective things to a SpecFeatureCell.
1037 //
1038 // Global Variables: -
1039 //
1040 // Side Effects : -
1041 //
1042 /----------------------------------------------------------------------*/
1043
SpecFeaturesAddEval(SpecFeature_p features,SpecLimits_p limits)1044 void SpecFeaturesAddEval(SpecFeature_p features, SpecLimits_p limits)
1045 {
1046
1047 features->goals_are_ground = (features->groundgoals ==
1048 features->goals);
1049
1050 if(limits->ngu_absolute)
1051 {
1052 features->ng_unit_content = SpecFewPosNonGroundUnits;
1053 if((features->unitaxioms-features->groundunitaxioms)>
1054 limits->ngu_few_limit)
1055 {
1056 features->ng_unit_content = SpecSomePosNonGroundUnits;
1057 }
1058 if((features->unitaxioms-features->groundunitaxioms)>
1059 limits->ngu_many_limit)
1060 {
1061 features->ng_unit_content = SpecManyPosNonGroundUnits;
1062 }
1063 }
1064 else
1065 {
1066 if(features->ng_unit_axioms_part<=limits->ngu_few_limit)
1067 {
1068 features->ng_unit_content = SpecFewPosNonGroundUnits;
1069 }
1070 else if(features->ng_unit_axioms_part>=limits->ngu_many_limit)
1071 {
1072 features->ng_unit_content = SpecManyPosNonGroundUnits;
1073 }
1074 else
1075 {
1076 features->ng_unit_content = SpecSomePosNonGroundUnits;
1077 }
1078 }
1079
1080 if(limits->gpc_absolute)
1081 {
1082 features->ground_positive_content = SpecFewPosGround;
1083 if(features->groundpositiveaxioms > limits->gpc_few_limit)
1084 {
1085 features->ground_positive_content = SpecSomePosGround;
1086 }
1087 if(features->groundpositiveaxioms > limits->gpc_many_limit)
1088 {
1089 features->ground_positive_content = SpecManyPosGround;
1090 }
1091 }
1092 else
1093 {
1094 if(features->ground_positive_axioms_part<=limits->gpc_few_limit)
1095 {
1096 features->ground_positive_content = SpecFewPosGround;
1097 }
1098 else if(features->ground_positive_axioms_part>=limits->gpc_many_limit)
1099 {
1100 features->ground_positive_content = SpecManyPosGround;
1101 }
1102 else
1103 {
1104 features->ground_positive_content = SpecSomePosGround;
1105 }
1106 }
1107
1108 if(features->clauses < limits->ax_some_limit)
1109 {
1110 features->set_clause_size = SpecFewAxioms;
1111 }
1112 else if(features->clauses < limits->ax_many_limit)
1113 {
1114 features->set_clause_size = SpecSomeAxioms;
1115 }
1116 else
1117 {
1118 features->set_clause_size = SpecManyAxioms;
1119 }
1120
1121 if(features->literals < limits->lit_some_limit)
1122 {
1123 features->set_literal_size = SpecFewLiterals;
1124 }
1125 else if(features->literals < limits->lit_many_limit)
1126 {
1127 features->set_literal_size = SpecSomeLiterals;
1128 }
1129 else
1130 {
1131 features->set_literal_size = SpecManyLiterals;
1132 }
1133
1134 if(features->term_cells < limits->term_medium_limit)
1135 {
1136 features->set_termcell_size = SpecSmallTerms;
1137 }
1138 else if(features->term_cells < limits->term_large_limit)
1139 {
1140 features->set_termcell_size = SpecMediumTerms;
1141 }
1142 else
1143 {
1144 features->set_termcell_size = SpecLargeTerms;
1145 }
1146
1147 switch(features->max_fun_arity)
1148 {
1149 case 0:
1150 features->max_fun_ar_class = SpecArity0;
1151 break;
1152 case 1:
1153 features->max_fun_ar_class = SpecArity1;
1154 break;
1155 case 2:
1156 features->max_fun_ar_class = SpecArity2;
1157 break;
1158 default:
1159 features->max_fun_ar_class = SpecArity3Plus;
1160 break;
1161 }
1162 switch(features->avg_fun_arity)
1163 {
1164 case 0:
1165 features->avg_fun_ar_class = SpecArity0;
1166 break;
1167 case 1:
1168 features->avg_fun_ar_class = SpecArity1;
1169 break;
1170 case 2:
1171 features->avg_fun_ar_class = SpecArity2;
1172 break;
1173 default:
1174 features->avg_fun_ar_class = SpecArity3Plus;
1175 break;
1176 }
1177 features->ng_unit_axioms_part = features->unitaxioms?
1178 ((double)(features->unitaxioms-features->groundunitaxioms)/
1179 (double)(features->unitaxioms))
1180 :0.0;
1181
1182 features->ground_positive_axioms_part = features->positiveaxioms?
1183 ((double)(features->groundpositiveaxioms)/
1184 (double)(features->positiveaxioms))
1185 :0.0;
1186 if(features->sum_fun_arity < limits->far_sum_medium_limit)
1187 {
1188 features->sum_fun_ar_class = SpecAritySumSmall;
1189 }
1190 else if(features->sum_fun_arity < limits->far_sum_large_limit)
1191 {
1192 features->sum_fun_ar_class = SpecAritySumMedium;
1193 }
1194 else
1195 {
1196 features->sum_fun_ar_class = SpecAritySumLarge;
1197 }
1198
1199 if(features->clause_max_depth < limits->depth_medium_limit)
1200 {
1201 features->max_depth_class = SpecDepthShallow;
1202 /* printf("Shallow %ld %ld\n", features->clause_max_depth, limits->depth_medium_limit);*/
1203 }
1204 else if(features->clause_max_depth < limits->depth_deep_limit)
1205 {
1206 features->max_depth_class = SpecDepthMedium;
1207 /* printf("Medium %ld %ld\n", features->clause_max_depth, limits->depth_medium_limit);*/
1208 }
1209 else
1210 {
1211 features->max_depth_class = SpecDepthDeep;
1212 /* printf("Deep %ld %ld\n", features->clause_max_depth, limits->depth_medium_limit);*/
1213 }
1214 }
1215
1216
1217
1218
1219 /*-----------------------------------------------------------------------
1220 //
1221 // Function: SpecFeaturesPrint()
1222 //
1223 // Print the feature vector.
1224 //
1225 // Global Variables: -
1226 //
1227 // Side Effects : Outpur
1228 //
1229 /----------------------------------------------------------------------*/
1230
SpecFeaturesPrint(FILE * out,SpecFeature_p features)1231 void SpecFeaturesPrint(FILE* out, SpecFeature_p features)
1232 {
1233 assert(features);
1234
1235 fprintf(out,
1236 "( %3ld, %3ld, %3ld, %3ld, %3ld, %3ld, %3ld, %3ld, %3ld,"
1237 " %3ld, %3ld, %3ld, %3ld, %3ld, %3ld, %8.6f, %8.6f,"
1238 " %3d, %3d, %3d, %3ld, %3ld )",
1239 features->goals,
1240 features->axioms,
1241 features->clauses,
1242 features->literals,
1243 features->term_cells,
1244 features->unitgoals,
1245 features->unitaxioms,
1246 features->horngoals,
1247 features->hornaxioms,
1248 features->eq_clauses,
1249 features->peq_clauses,
1250 features->groundunitaxioms,
1251 features->groundgoals,
1252 features->groundpositiveaxioms,
1253 features->positiveaxioms,
1254 features->ng_unit_axioms_part,
1255 features->ground_positive_axioms_part,
1256 features->max_fun_arity,
1257 features->avg_fun_arity,
1258 features->sum_fun_arity,
1259 features->clause_max_depth,
1260 features->clause_avg_depth
1261 );
1262 }
1263
1264
1265 /*-----------------------------------------------------------------------
1266 //
1267 // Function: SpecFeaturesParse()
1268 //
1269 // Parse the relevant (i.e. currently used and printed) parts of a
1270 // spec features cell from in into a caller-provided structure. Also
1271 // parse the type and extract the invariant parts from it.
1272 //
1273 // Global Variables: -
1274 //
1275 // Side Effects : Input
1276 //
1277 /----------------------------------------------------------------------*/
1278
SpecFeaturesParse(Scanner_p in,SpecFeature_p features)1279 void SpecFeaturesParse(Scanner_p in, SpecFeature_p features)
1280 {
1281 char *class;
1282
1283 AcceptInpTok(in, OpenBracket);
1284 features->goals = ParseInt(in);
1285 AcceptInpTok(in, Comma);
1286 features->axioms = ParseInt(in);
1287 AcceptInpTok(in, Comma);
1288 features->clauses = ParseInt(in);
1289 AcceptInpTok(in, Comma);
1290 features->literals = ParseInt(in);
1291 AcceptInpTok(in, Comma);
1292 features->term_cells = ParseInt(in);
1293 AcceptInpTok(in, Comma);
1294 features->unitgoals = ParseInt(in);
1295 AcceptInpTok(in, Comma);
1296 features->unitaxioms = ParseInt(in);
1297 AcceptInpTok(in, Comma);
1298 features->horngoals = ParseInt(in);
1299 AcceptInpTok(in, Comma);
1300 features->hornaxioms = ParseInt(in);
1301 AcceptInpTok(in, Comma);
1302 features->eq_clauses = ParseInt(in);
1303 AcceptInpTok(in, Comma);
1304 features->peq_clauses = ParseInt(in);
1305 AcceptInpTok(in, Comma);
1306 features->groundunitaxioms = ParseInt(in);
1307 AcceptInpTok(in, Comma);
1308 features->groundgoals = ParseInt(in);
1309 AcceptInpTok(in, Comma);
1310 features->groundpositiveaxioms = ParseInt(in);
1311 AcceptInpTok(in, Comma);
1312 features->positiveaxioms = ParseInt(in);
1313 AcceptInpTok(in, Comma);
1314 features->ng_unit_axioms_part = ParseFloat(in);
1315 AcceptInpTok(in, Comma);
1316 features->ground_positive_axioms_part = ParseFloat(in);
1317 AcceptInpTok(in, Comma);
1318 features->max_fun_arity = ParseInt(in);
1319 AcceptInpTok(in, Comma);
1320 features->avg_fun_arity = ParseInt(in);
1321 AcceptInpTok(in, Comma);
1322 features->sum_fun_arity = ParseInt(in);
1323 AcceptInpTok(in, Comma);
1324 features->clause_max_depth = ParseInt(in);
1325 AcceptInpTok(in, Comma);
1326 features->clause_avg_depth = ParseInt(in);
1327 AcceptInpTok(in, CloseBracket);
1328 AcceptInpTok(in, Colon);
1329
1330 class = ParsePlainFilename(in);
1331 if(strlen(class) < 5)
1332 {
1333 Error("Insufficient class information in class name(s) (to short)", SYNTAX_ERROR);
1334 }
1335 switch(class[0])
1336 {
1337 case 'G':
1338 features->axiomtypes = SpecGeneral;
1339 break;
1340 case 'H':
1341 features->axiomtypes = SpecHorn;
1342 break;
1343 case 'U':
1344 features->axiomtypes = SpecUnit;
1345 break;
1346 default:
1347 Error("Insufficient class information in class name(s)", SYNTAX_ERROR);
1348 break;
1349 }
1350 switch(class[1])
1351 {
1352 case 'H':
1353 features->goaltypes = SpecHorn;
1354 break;
1355 case 'U':
1356 features->goaltypes = SpecUnit;
1357 break;
1358 default:
1359 Error("Insufficient class information in class name(s)", SYNTAX_ERROR);
1360 break;
1361 }
1362 switch(class[2])
1363 {
1364 case 'N':
1365 features->eq_content = SpecNoEq;
1366 break;
1367 case 'S':
1368 features->eq_content = SpecSomeEq;
1369 break;
1370 case 'P':
1371 features->eq_content = SpecPureEq;
1372 break;
1373 default:
1374 Error("Insufficient class information in class name(s)", SYNTAX_ERROR);
1375 break;
1376 }
1377 /* class[3] information is recovered from numeric features */
1378 switch(class[4])
1379 {
1380 case 'G':
1381 features->goals_are_ground = true;
1382 break;
1383 case 'N':
1384 features->goals_are_ground = false;
1385 break;
1386 default:
1387 Error("Insufficient class information in class name(s)", SYNTAX_ERROR);
1388 break;
1389 }
1390
1391
1392 FREE(class);
1393 }
1394
1395
1396 /*-----------------------------------------------------------------------
1397 //
1398 // Function: SpecTypePrint()
1399 //
1400 // Print the type of the problem as a n-letter code.
1401 // 1) Axioms are [U]nit, [H]orn, [General]
1402 // 2) Goals are [U]nit, [H]orn, [General]
1403 // 3) [N]o equality, [S]ome equality, [P]ure equality
1404 // 4) [F]ew, [S]ome, [M]any non-ground facts
1405 // 5) [G]round goals or [N]on-ground goals
1406 //
1407 // Global Variables: -
1408 //
1409 // Side Effects : -
1410 //
1411 /----------------------------------------------------------------------*/
1412
SpecTypePrint(FILE * out,SpecFeature_p features,char * mask)1413 void SpecTypePrint(FILE* out, SpecFeature_p features, char* mask)
1414 {
1415 const char encoding[]="UHGNSPFSMFSMFSMFSMSML0123SMLSMD";
1416 char result[14]; /* Big enough for the '\0'!!!*/
1417 int i, limit;
1418
1419 assert(features);
1420 assert(mask && (strlen(mask)==13));
1421 limit = strlen(mask);
1422
1423 sprintf(result, "%c%c%c%c%c%c%c%c%c%c%c%c%c",
1424 encoding[features->axiomtypes],
1425 encoding[features->goaltypes],
1426 encoding[features->eq_content],
1427 encoding[features->ng_unit_content],
1428 features->goals_are_ground?'G':'N',
1429 encoding[features->set_clause_size],
1430 encoding[features->set_literal_size],
1431 encoding[features->set_termcell_size],
1432 encoding[features->ground_positive_content],
1433 encoding[features->max_fun_ar_class],
1434 encoding[features->avg_fun_ar_class],
1435 encoding[features->sum_fun_ar_class],
1436 encoding[features->max_depth_class]);
1437 for(i=0; i<limit; i++)
1438 {
1439 if(mask[i]=='-')
1440 {
1441 result[i]= '-';
1442 }
1443 }
1444 fputs(result, out);
1445 }
1446
1447 /*-----------------------------------------------------------------------
1448 //
1449 // Function: ClauseSetPrintPosUnits()
1450 //
1451 // Print the positive unit clauses from set.
1452 //
1453 // Global Variables: -
1454 //
1455 // Side Effects : Output
1456 //
1457 /----------------------------------------------------------------------*/
1458
ClauseSetPrintPosUnits(FILE * out,ClauseSet_p set,bool printinfo)1459 void ClauseSetPrintPosUnits(FILE* out, ClauseSet_p set, bool
1460 printinfo)
1461 {
1462 Clause_p handle;
1463
1464 for(handle = set->anchor->succ; handle!=set->anchor; handle =
1465 handle->succ)
1466 {
1467 if(ClauseIsDemodulator(handle))
1468 {
1469 ClauseLinePrint(out, handle, printinfo);
1470 }
1471 }
1472 }
1473
1474 /*-----------------------------------------------------------------------
1475 //
1476 // Function: ClauseSetPrintNegUnits()
1477 //
1478 // Print the negative unit clauses from set.
1479 //
1480 // Global Variables: -
1481 //
1482 // Side Effects : Output
1483 //
1484 /----------------------------------------------------------------------*/
1485
ClauseSetPrintNegUnits(FILE * out,ClauseSet_p set,bool printinfo)1486 void ClauseSetPrintNegUnits(FILE* out, ClauseSet_p set, bool
1487 printinfo)
1488 {
1489 Clause_p handle;
1490
1491 for(handle = set->anchor->succ; handle!=set->anchor; handle =
1492 handle->succ)
1493 {
1494 if(ClauseIsUnit(handle)&&ClauseIsGoal(handle))
1495 {
1496 ClauseLinePrint(out, handle, printinfo);
1497 }
1498 }
1499 }
1500
1501
1502 /*-----------------------------------------------------------------------
1503 //
1504 // Function: ClauseSetPrintNonUnits()
1505 //
1506 // Print the non-unit clauses from set.
1507 //
1508 // Global Variables: -
1509 //
1510 // Side Effects : Output
1511 //
1512 /----------------------------------------------------------------------*/
1513
ClauseSetPrintNonUnits(FILE * out,ClauseSet_p set,bool printinfo)1514 void ClauseSetPrintNonUnits(FILE* out, ClauseSet_p set, bool
1515 printinfo)
1516 {
1517 Clause_p handle;
1518
1519 for(handle = set->anchor->succ; handle!=set->anchor; handle =
1520 handle->succ)
1521 {
1522 if(!ClauseIsUnit(handle))
1523 {
1524 ClauseLinePrint(out, handle, printinfo);
1525 }
1526 }
1527 }
1528
1529
1530 /*-----------------------------------------------------------------------
1531 //
1532 // Function: ProofStatePrintSelective()
1533 //
1534 // Print parts of the proof state to the given stream. Descriptor
1535 // controls which parts.
1536 //
1537 // Global Variables: -
1538 //
1539 // Side Effects : Output
1540 //
1541 /----------------------------------------------------------------------*/
1542
ProofStatePrintSelective(FILE * out,ProofState_p state,char * descriptor,bool printinfo)1543 void ProofStatePrintSelective(FILE* out, ProofState_p state, char*
1544 descriptor, bool printinfo)
1545 {
1546 char* current = descriptor;
1547
1548 while(*current)
1549 {
1550 switch(*current)
1551 {
1552 case 'e':
1553 fprintf(out, "# Processed positive unit clauses:\n");
1554 ClauseSetPrintPosUnits(out, state->processed_pos_rules,
1555 printinfo);
1556 ClauseSetPrintPosUnits(out, state->processed_pos_eqns,
1557 printinfo);
1558 fputc('\n', out);
1559 break;
1560 case 'i':
1561 fprintf(out, "# Processed negative unit clauses:\n");
1562 ClauseSetPrintNegUnits(out, state->processed_neg_units,
1563 printinfo);
1564 fputc('\n', out);
1565 break;
1566 case 'g':
1567 fprintf(out, "# Processed non-unit clauses:\n");
1568 ClauseSetPrintNonUnits(out, state->processed_non_units,
1569 printinfo);
1570 fputc('\n', out);
1571 break;
1572 case 'E':
1573 fprintf(out, "# Unprocessed positive unit clauses:\n");
1574 ClauseSetPrintPosUnits(out, state->unprocessed,
1575 printinfo);
1576 fputc('\n', out);
1577 break;
1578 case 'I':
1579 fprintf(out, "# Unprocessed negative unit clauses:\n");
1580 ClauseSetPrintNegUnits(out, state->unprocessed,
1581 printinfo);
1582 fputc('\n', out);
1583 break;
1584 case 'G':
1585 fprintf(out, "# Unprocessed non-unit clauses:\n");
1586 ClauseSetPrintNonUnits(out, state->unprocessed,
1587 printinfo);
1588 fputc('\n', out);
1589 break;
1590 case 'a':
1591 if(ClauseSetIsEquational(state->axioms))
1592 {
1593 fprintf(out, "# Equality axioms:\n");
1594 EqAxiomsPrint(out, state->signature, true);
1595 }
1596 else
1597 {
1598 fprintf(out, "# No equality axioms required.\n");
1599 }
1600
1601 break;
1602 case 'A':
1603 if(ClauseSetIsEquational(state->axioms))
1604 {
1605 fprintf(out, "# Equality axioms:\n");
1606 EqAxiomsPrint(out, state->signature, false);
1607 }
1608 else
1609 {
1610 fprintf(out, "# No equality axioms required.\n");
1611 }
1612 break;
1613 default:
1614 assert(false && "Illegal character in descriptor string");
1615 break;
1616 }
1617 current++;
1618 }
1619 }
1620
1621
1622 /*-----------------------------------------------------------------------
1623 //
1624 // Function: CreateDefaultSpecLimits()
1625 //
1626 // Return a SpecLimits cell initialized with the default limits for
1627 // Auto-Mode problem classification.
1628 //
1629 // Global Variables:
1630 //
1631 // Side Effects :
1632 //
1633 /----------------------------------------------------------------------*/
CreateDefaultSpecLimits(void)1634 SpecLimits_p CreateDefaultSpecLimits(void)
1635 {
1636 SpecLimits_p limits = SpecLimitsAlloc();
1637
1638 limits->ax_some_limit = 1000;
1639 limits->ax_many_limit = 100000;
1640 limits->lit_some_limit = 400;
1641 limits->lit_many_limit = 4000;
1642 limits->term_medium_limit = 200;
1643 limits->term_large_limit = 1500;
1644 limits->far_sum_medium_limit = 4;
1645 limits->far_sum_large_limit = 29;
1646 limits->depth_medium_limit = 4;
1647 limits->depth_deep_limit = 7;
1648 limits->gpc_absolute = true;
1649 limits->gpc_few_limit = 2;
1650 limits->gpc_many_limit = 5;
1651 limits->ngu_absolute = true;
1652 limits->ngu_few_limit = 1;
1653 limits->ngu_many_limit = 3;
1654
1655 return limits;
1656 }
1657
1658
1659 /*---------------------------------------------------------------------*/
1660 /* End of File */
1661 /*---------------------------------------------------------------------*/
1662
1663
1664