-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathTAGS
More file actions
11650 lines (11032 loc) · 375 KB
/
TAGS
File metadata and controls
11650 lines (11032 loc) · 375 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
ANALYSIS/can_clausestats.c,291
ClauseStats_p ClauseStatsCopy(61,1826
void ClauseStatsParseInto(88,2568
ClauseStats_p ClauseStatsParse(126,3658
void ClauseStatsPrint(146,4090
void ClauseStatsPrintNormalized(172,4689
long ClauseSetInfoParse(236,6405
long ClauseSetInfoPrint(270,7252
void ClauseStatTreeFree(305,8043
ANALYSIS/can_clausestore.c,327
long dummy;32,826
void CompClauseFree(63,1834
void CompClauseAddTerms(86,2354
void CompClauseRemoveTerms(121,3289
CompClause_p PackClause(146,3968
Clause_p UnpackClause(176,4692
CompClause_p CompactifyClause(206,5402
Clause_p UnCompactifyClause(227,5854
void CompClausePrint(248,6357
void CompClausePCLPrint(271,6908
ANALYSIS/can_treeanalyze.c,330
static long select_examples_from_proof(56,1648
static long select_examples_from_non_proof(120,3103
long ProofMarkProofClauses(162,4175
void ProofSetClauseStatistics(223,5562
void ProofComputeParentNumbers(257,6523
void ProofComputeDistance(325,8425
long ProofDistanceDistrib(374,9683
long InfStateSelectExamples(416,10893
BASICS/clb_ddarrays.c,181
DDArray_p DDArrayAlloc(61,1907
void DDArrayFree(91,2573
void DDArayEnlarge(113,3041
void DDArrayDebugPrint(142,3763
void DDArrayAdd(171,4406
double DDArraySelectPart(201,5077
BASICS/clb_dstacks.c,252
static void push(57,1788
DStack_p DStackAlloc(94,2815
void DStackFree(119,3321
void DStackReset(141,3776
void DStackPush(158,4115
double DStackPop(175,4470
double DStackTop(196,4888
double DStackBelowTop(217,5322
double DStackElement(237,5718
BASICS/clb_dstrings.c,484
char NullStr[NullStr30,808
DStr_p DStrAlloc(60,1804
void DStrFree(85,2335
char* DStrAppendStr(114,2847
char* DStrAppendChar(161,4013
char* DStrAppendBuffer(190,4711
char* DStrAppendInt(219,5268
char* DStrAppendStrArray(240,5742
char DStrDeleteLastChar(271,6383
char* DStrView(303,7208
char* DStrAddress(328,7697
char* DStrCopy(352,8211
char* DStrCopyCore(386,9087
char* DStrSet(414,9654
long DStrLen(438,10123
void DStrReset(459,10568
void DStrMinimize(483,11010
BASICS/clb_error.c,519
char ErrStr[ErrStr35,905
int TmpErrno;39,991
char* ProgName 43,1037
char* EmptyString 49,1208
#define E_SC_PAGE_SIZE 70,2005
#define E_SC_PAGE_SIZE 72,2070
long GetSystemPageSize(88,2452
#define MEM_PHRASE 119,3108
long GetSystemPhysMemory(121,3157
void InitError(199,5076
VOLATILE void Error(218,5489
VOLATILE void SysError(244,6153
void Warning(270,6686
void SysWarning(295,7328
double GetTotalCPUTime(323,7956
void PrintRusage(350,8518
void StrideMemory(405,10280
bool CheckLetterString(439,11020
BASICS/clb_fixdarrays.c,142
FixedDArray_p FixedDArrayAlloc(60,1779
void FixedDArrayFree(83,2275
FixedDArray_p FixedDArrayCopy(105,2736
void FixedDArrayPrint(137,3347
BASICS/clb_floattrees.c,328
static FloatTree_p splay_tree(57,1633
FloatTree_p FloatTreeCellAllocEmpty(154,3786
void FloatTreeFree(177,4359
FloatTree_p FloatTreeInsert(217,5241
bool FloatTreeStore(264,6232
FloatTree_p FloatTreeFind(298,6923
FloatTree_p FloatTreeExtractEntry(327,7578
bool FloatTreeDeleteEntry(368,8417
long FloatTreeNodes(394,8921
BASICS/clb_intmap.c,469
static bool switch_to_array(57,1635
static bool switch_to_tree(83,2237
static NumTree_p add_new_tree_node(109,2916
static void array_to_tree(138,3581
static void tree_to_array(183,4661
IntMap_p IntMapAlloc(232,6043
void IntMapFree(254,6477
void* IntMapGetVal(289,7181
void** IntMapGetRef(345,8424
void IntMapAssign(459,11786
void* IntMapDelKey(486,12388
IntMapIter_p IntMapIterAlloc(569,14708
void IntMapIterFree(617,15932
void IntMapDebugPrint(654,16678
BASICS/clb_memory.c,673
bool MemIsLow 43,1461
Mem_p free_mem_list[free_mem_list45,1485
long size_malloc_mem 48,1555
long size_malloc_count 49,1581
long size_free_mem 50,1609
long size_free_count 51,1633
long clb_free_count 52,1659
long secure_malloc_count 53,1684
long secure_malloc_mem 54,1714
long secure_realloc_count 55,1742
long secure_realloc_m_count 56,1773
long secure_realloc_f_count 57,1806
static long free_list_size(80,2386
void MemFlushFreeList(114,3252
void* SecureMalloc(148,4151
void* SecureRealloc(199,5393
char* SecureStrdup(260,6750
char* SecureStrndup(284,7353
long* IntArrayAlloc(323,8046
void MemDebugPrintStats(355,8639
void MemFreeListPrint(397,10092
BASICS/clb_newmem.c,662
bool MemIsLow 39,1404
Mem_p free_mem_list[free_mem_list42,1429
long size_malloc_mem 45,1499
long size_malloc_count 46,1525
long size_free_mem 47,1553
long size_free_count 48,1577
long clb_free_count 49,1603
long secure_malloc_count 50,1628
long secure_malloc_mem 51,1658
long secure_realloc_count 52,1686
long secure_realloc_m_count 53,1717
long secure_realloc_f_count 54,1750
void MemFlushFreeList(78,2512
void* SecureMalloc(98,3145
void* SecureRealloc(142,4222
void* SizeMallocReal(190,5409
void SizeFreeReal(253,7053
void MemAddNewChunk(298,8232
char* SecureStrdup(332,9065
long* IntArrayAlloc(355,9555
void MemDebugPrintStats(387,10148
BASICS/clb_numtrees.c,496
static long numtree_print(58,1736
static NumTree_p splay_tree(112,3072
NumTree_p NumTreeCellAllocEmpty(209,5239
void NumTreeFree(232,5800
NumTree_p NumTreeInsert(272,6682
bool NumTreeStore(319,7711
long NumTreeDebugPrint(350,8370
NumTree_p NumTreeFind(372,8902
NumTree_p NumTreeExtractEntry(401,9547
NumTree_p NumTreeExtractRoot(443,10386
bool NumTreeDeleteEntry(465,10863
long NumTreeNodes(491,11351
NumTree_p NumTreeMaxNode(527,12066
PStack_p NumTreeLimitedTraverseInit(553,12584
BASICS/clb_numxtrees.c,442
static NumXTree_p splay_tree(55,1649
NumXTree_p NumXTreeCellAllocEmpty(152,3822
void NumXTreeFree(179,4419
NumXTree_p NumXTreeInsert(219,5305
bool NumXTreeStore(266,6373
NumXTree_p NumXTreeFind(299,7072
NumXTree_p NumXTreeExtractEntry(328,7721
NumXTree_p NumXTreeExtractRoot(370,8566
bool NumXTreeDeleteEntry(392,9049
long NumXTreeNodes(418,9543
NumXTree_p NumXTreeMaxNode(454,10261
PStack_p NumXTreeLimitedTraverseInit(480,10783
BASICS/clb_objtrees.c,420
static PObjTree_p splay_tree(54,1585
PObjTree_p PTreeObjInsert(151,3469
void* PTreeObjStore(202,4566
PObjTree_p PTreeObjFind(233,5230
void* PTreeObjFindObj(260,5804
PObjTree_p PTreeObjFindBinary(287,6409
PObjTree_p PTreeObjExtractEntry(328,7208
void* PTreeObjExtractObject(371,8130
void* PTreeObjExtractRootObject(399,8796
void PTreeObjMerge(423,9345
void PObjTreeFree(459,10155
long PObjTreeNodes(483,10656
BASICS/clb_os_wrapper.c,284
RLimResult SetSoftRlimit(66,1981
void SetSoftRlimitErr(103,2837
void SetMemoryLimit(150,3884
rlim_t GetSoftRlimit(175,4437
void IncreaseMaxStackSize(203,5076
long long GetUSecTime(237,5856
long long GetUSecClock(258,6278
FILE* SecureFOpen(278,6689
void SecureFClose(304,7180
BASICS/clb_partial_orderings.c,46
char* POCompareSymbol[POCompareSymbol32,853
BASICS/clb_pdarrays.c,446
PDArray_p PDArrayAlloc(61,1873
PDArray_p PDIntArrayAlloc(93,2671
void PDArrayFree(125,3373
void PDArrayEnlarge(147,3844
PDArray_p PDArrayCopy(195,4942
void PDArrayElementDeleteP(221,5513
void PDArrayElementDeleteInt(242,5996
long PDArrayMembers(263,6426
long PDArrayFirstUnused(293,6971
long PDArrayStore(324,7594
long PDArrayStoreP(349,8120
long PDArrayStoreInt(372,8600
void PDArrayAdd(395,9116
long PDArrayElementIncInt(420,9685
BASICS/clb_pdrangearrays.c,457
static long range_arr_size(57,1603
static void range_arr_expand_down(89,2284
static void range_arr_expand_up(135,3465
PDRangeArr_p PDRangeArrAlloc(185,4827
PDRangeArr_p PDIntRangeArrAlloc(218,5639
void PDRangeArrFree(251,6359
void PDRangeArrEnlarge(273,6845
PDRangeArr_p PDRangeArrCopy(301,7551
void PDRangeArrElementDeleteP(326,8183
void PDRangeArrElementDeleteInt(347,8697
long PDRangeArrMembers(368,9158
long PDRangeArrElementIncInt(398,9721
BASICS/clb_plist.c,219
PList_p PListAlloc(60,1750
void PListFree(82,2150
void PListInsert(104,2564
void PListStore(125,3010
void PListStoreP(146,3420
void PListStoreInt(167,3804
PList_p PListExtract(188,4192
void PListDelete(215,4788
BASICS/clb_pqueue.c,149
void PQueueGrow(59,1768
long PQueueCardinality(94,2555
IntOrP PQueueElement(123,3143
long PQueueTailIndex(142,3562
long PQueueIncIndex(164,4058
BASICS/clb_pstacks.c,182
IntOrP* PStackTopAddr(60,1811
double PStackComputeAverage(83,2327
void PStackSort(135,3272
void PStackMerge(152,3703
void PStackPushStack(200,4705
void PStackPrintInt(224,5209
BASICS/clb_ptrees.c,672
static PTree_p splay_ptree(54,1559
PTree_p PTreeCellAllocEmpty(152,3474
void PTreeFree(174,3963
PTree_p PTreeInsert(214,4783
bool PTreeStore(262,5784
PTree_p PTreeFind(292,6380
PTree_p PTreeFindBinary(319,6945
PTree_p PTreeExtractEntry(359,7695
void* PTreeExtractKey(401,8532
void* PTreeExtractRootKey(428,9128
bool PTreeDeleteEntry(450,9645
bool PTreeMerge(478,10246
void PTreeInsertTree(521,11024
long PTreeNodes(553,11645
long PTreeDebugPrint(589,12323
long PStackToPTree(632,13201
long PTreeToPStack(661,13795
void* PTreeSharedElement(701,14746
PTree_p PTreeIntersection(741,15547
long PTreeDestrIntersection(779,16405
PTree_p PTreeCopy(815,17061
BASICS/clb_quadtrees.c,294
static QuadTree_p splay_tree(55,1638
int DoubleKeyCmp(148,3345
int QuadKeyCmp(174,3775
void QuadTreeFree(201,4383
QuadTree_p QuadTreeInsert(241,5215
bool QuadTreeStore(291,6273
QuadTree_p QuadTreeFind(325,7045
QuadTree_p QuadTreeExtractEntry(355,7709
bool QuadTreeDeleteEntry(397,8592
BASICS/clb_regmem.c,180
static PTree_p reg_mem_tree 37,1160
void* RegMemAlloc(66,2169
void* RegMemRealloc(88,2598
void RegMemFree(112,3090
void* RegMemProvide(136,3811
void RegMemCleanUp(169,4479
BASICS/clb_simple_stuff.c,202
int WeightedObjectCompareFun(60,1790
int StringIndex(88,2379
#define LOG_2 115,2830
double Log2(117,2875
long Log2Ceil(134,3226
double sqrt(168,3855
double pow(207,4550
char* IndentStr(235,5044
BASICS/clb_stringtrees.c,279
static StrTree_p splay_tree(58,1768
StrTree_p StrTreeCellAllocEmpty(154,3923
void StrTreeFree(177,4487
StrTree_p StrTreeInsert(204,5068
StrTree_p StrTreeStore(251,6121
StrTree_p StrTreeFind(285,6841
StrTree_p StrTreeExtractEntry(314,7499
bool StrTreeDeleteEntry(355,8338
BASICS/clb_sysdate.c,27
void SysDatePrint(62,1800
BASICS/clb_verbose.c,20
int Verbose 32,821
CLAUSES/ccl_axiomsorter.c,116
WAxiom_p WAxiomAlloc(61,1798
void WAxiomAddRelEval(95,2544
int WAxiomCmp(149,3677
int WAxiomCmpWrapper(182,4277
CLAUSES/ccl_clausecpos.c,207
CompactPos PackTermPos(61,1774
CompactPos PackClausePos(101,2535
void UnpackTermPos(139,3288
void UnpackClausePosInto(180,4162
ClausePos_p UnpackClausePos(228,5190
Term_p ClauseCPosGetSubterm(251,5772
CLAUSES/ccl_clausefunc.c,501
static int clause_canon_compare(55,1627
static int clause_canon_compare_wrapper(75,2075
void ClauseRemoveLiteralRef(102,2898
void ClauseRemoveLiteral(137,3703
void ClauseFlipLiteralSign(162,4260
void ClauseKillChildren(190,4827
int ClauseRemoveSuperfluousLiterals(222,5652
long ClauseSetRemoveSuperfluousLiterals(278,6862
void ClauseSetCanonize(306,7515
int ClauseRemoveACResolved(334,8176
bool ClauseUnitSimplifyTest(374,9174
void ClauseArchive(420,10249
void ClauseSetArchive(452,11132
CLAUSES/ccl_clauseinfo.c,105
ClauseInfo_p ClauseInfoAlloc(66,2085
void ClauseInfoFree(102,2977
void ClauseSourceInfoPrint(132,3548
CLAUSES/ccl_clausepos.c,337
void ClausePosPrint(62,1770
Eqn_p ClausePosFindPosLiteral(93,2485
Eqn_p ClausePosFindMaxLiteral(123,3167
Term_p ClausePosFindFirstMaximalSide(153,3874
Term_p ClausePosFindNextMaximalSide(182,4592
Term_p ClausePosFindFirstMaximalSubterm(224,5544
Term_p ClausePosFindNextMaximalSubterm(255,6152
bool TermComputeRWSequence(289,6977
CLAUSES/ccl_clausepos_tree.c,377
static void clause_tpos_free_wrapper(54,1610
ClauseTPos_p ClauseTPosAlloc(77,2221
void ClauseTPosFree(101,2734
void ClauseTPosTreeFree(120,3122
int CmpClauseTPosCells(139,3529
void ClauseTPosTreeFreeWrapper(161,4080
void ClauseTPosTreeInsertPos(179,4472
void ClauseTPosTreeDeletePos(210,5238
void ClauseTPosTreeDeleteClause(244,6128
void ClauseTPosTreePrint(270,6732
CLAUSES/ccl_clauses.c,2666
bool ClausesHaveLocalVariables 37,923
bool ClausesHaveDisjointVariables 44,1170
static long global_clause_counter 49,1298
long ClauseIdentCounter 54,1435
static long clause_perm_ident_counter 58,1547
static bool foundEqLitLater(87,2646
static bool term_query_var_prop(118,3352
Clause_p clause_copy_meta(167,4302
void TSTPSkipSource(210,5540
void ClauseSetTPTPType(231,5980
Clause_p ClauseCellAlloc(251,6474
Clause_p EmptyClauseAlloc(276,7001
Clause_p ClauseAlloc(317,8102
void ClauseRecomputeLitCounts(363,9084
bool ClauseHasMaxPosEqLit(400,9758
Clause_p ClauseSortLiterals(430,10415
Clause_p ClauseCanonize(473,11607
bool ClauseIsSorted(500,12178
int ClauseStructWeightCompareWrapper(539,12985
int ClauseStructWeightCompare(566,13831
int ClauseStructWeightLexCompare(636,15226
bool ClauseIsACRedundant(674,16180
void ClauseFree(701,16838
bool ClauseIsSemFalse(728,17417
bool ClauseIsSemEmpty(755,17960
bool ClauseIsRangeRestricted(788,18714
bool ClauseIsAntiRangeRestricted(851,20235
bool ClauseIsTPTPRangeRestricted(915,21838
bool ClauseIsStronglyRangeRestricted(976,23354
EqnSide ClauseIsEqDefinition(1053,25018
Clause_p ClauseCopy(1081,25764
Clause_p ClauseFlatCopy(1104,26287
Clause_p ClauseCopyOpt(1126,26803
Clause_p ClauseCopyDisjoint(1147,27279
Clause_p ClauseSkolemize(1169,27741
void ClausePrintList(1201,28450
void ClausePrintAxiom(1221,29032
void ClausePrintRule(1272,30145
void ClausePrintGoal(1304,30876
void ClausePrintQuery(1325,31426
void ClausePrintTPTPFormat(1346,31937
void ClausePrintLOPFormat(1398,33107
void ClausePrint(1425,33778
void ClausePCLPrint(1470,34682
void ClauseTSTPCorePrint(1518,35916
void ClauseTSTPPrint(1546,36550
bool ClauseStartsMaybe(1610,38018
ClauseProperties ClauseTypeParse(1638,38623
Clause_p ClauseParse(1695,39794
Clause_p ClausePCLParse(1849,44133
void ClauseMarkMaximalTerms(1885,44977
bool ClauseParentsAreSubset(1906,45484
void ClauseDetachParents(1951,46362
void ClauseRegisterChild(1983,47094
void ClauseAddEvalCell(2003,47656
void ClauseRemoveEvaluations(2022,48122
double ClauseWeight(2041,48593
double ClauseFunWeight(2072,49441
double ClauseNonLinearWeight(2107,50431
double ClauseSymTypeWeight(2142,51355
double ClauseStandardWeight(2174,52210
double ClauseOrientWeight(2199,52798
bool ClauseNotGreaterEqual(2244,54006
int ClauseCompareFun(2324,55940
int ClauseCmpById(2368,56866
int ClauseCmpByPermId(2398,57492
int ClauseCmpByPermIdR(2426,58125
int ClauseCmpByStructWeight(2455,58733
int ClauseCmpByPtr(2476,59287
Clause_p ClauseNormalizeVars(2497,59781
long ClauseCollectSubterms(2537,60761
long ClauseReturnFCodes(2569,61518
CLAUSES/ccl_clausesets.c,2572
static void print_var_pattern(54,1574
static void eq_func_axiom_print(91,2309
static void eq_pred_axiom_print(137,3407
static void tptp_eq_func_axiom_print(178,4360
static void tptp_eq_pred_axiom_print(224,5533
static void clause_set_extract_entry(269,6639
ClauseSet_p ClauseSetAlloc(323,8045
void ClauseSetFreeClauses(358,8851
void ClauseSetFree(384,9333
long ClauseSetStackCardinality(418,10013
void ClauseSetGCMarkTerms(446,10589
void ClauseSetInsert(469,11098
long ClauseSetInsertSet(515,12215
void ClauseSetPDTIndexedInsert(542,12781
void ClauseSetIndexedInsert(583,13841
void ClauseSetIndexedInsertClause(614,14547
Clause_p ClauseSetExtractEntry(634,15083
Clause_p ClauseSetExtractFirst(680,16215
void ClauseSetDeleteEntry(708,16783
Clause_p ClauseSetFindBest(729,17250
void ClauseSetPrint(764,18004
void ClauseSetTSTPPrint(789,18584
void ClauseSetPrintPrefix(814,19205
void ClauseSetSort(846,19996
void ClauseSetSetProp(883,20829
void ClauseSetDelProp(907,21327
long ClauseSetMarkCopies(934,22024
long ClauseSetDeleteMarkedEntries(976,22913
long ClauseSetDeleteCopies(1015,23760
long ClauseSetDeleteNonUnits(1044,24328
long ClauseSetGetTermNodes(1081,25132
long ClauseSetMarkSOS(1107,25713
void ClauseSetTermSetProp(1142,26481
long ClauseSetTBTermPropDelCount(1165,27045
long ClauseSetGetSharedTermNodes(1190,27655
long ClauseSetParseList(1215,28250
void ClauseSetMarkMaximalTerms(1244,28876
void ClauseSetSortLiterals(1268,29388
SysDate ClauseSetListGetMaxDate(1293,29989
Clause_p ClauseSetFind(1321,30669
Clause_p ClauseSetFindById(1355,31340
void ClauseSetRemoveEvaluations(1387,31992
long ClauseSetFilterTrivial(1417,32710
long ClauseSetFilterTautologies(1457,33516
Clause_p ClauseSetFindMaxStandardWeight(1496,34371
ClausePos_p ClauseSetFindEqDefinition(1532,35179
void ClauseSetDocInital(1580,36215
void ClauseSetPropDocQuote(1609,36844
bool ClauseSetVerifyDemod(1642,37615
bool PDTreeVerifyIndex(1676,38326
void EqAxiomsPrint(1758,40234
void ClauseSetAddSymbolDistribution(1832,41993
void ClauseSetAddConjSymbolDistribution(1856,42571
void ClauseSetComputeFunctionRanks(1884,43230
FunCode ClauseSetFindFreqSymbol(1910,43882
long ClauseSetMaxVarNumber(1955,44968
long ClauseSetFindCharFreqVectors(1986,45704
PermVector_p PermVectorCompute(2027,46823
long ClauseSetFVIndexify(2081,48212
long ClauseSetNewTerms(2116,49000
long ClauseSetSplitConjectures(2154,49888
long long ClauseSetStandardWeight(2189,50675
void ClauseSetDerivationStackStatistics(2218,51280
long ClauseSetPushClauses(2260,52362
CLAUSES/ccl_condensation.c,120
long CondensationAttempts 30,758
long CondensationSuccesses 31,789
bool CondenseOnce(63,1879
bool Condense(126,3606
CLAUSES/ccl_context_sr.c,90
int ClauseContextualSimplifyReflect(61,1882
long ClauseSetFindContextSRClauses(119,3442
CLAUSES/ccl_def_handling.c,201
DefStore_p DefStoreAlloc(64,2060
void DefStoreFree(91,2714
Eqn_p GenDefLit(112,3183
Clause_p GetClauseDefinition(166,4577
WFormula_p GetFormulaDefinition(199,5416
FunCode GetDefinitions(250,6906
CLAUSES/ccl_derivation.c,912
ProofObjectType BuildProofObject 32,840
char *opids[opids34,880
char *optheory optheory70,1334
char *opstatus opstatus107,1862
static void derived_free_wrapper(167,3022
int derived_compare(185,3411
PStack_p derived_get_derivation(210,4056
void ClausePushDerivation(243,4925
void ClausePushACResDerivation(282,5965
void WFormulaPushDerivation(309,6720
long DerivStackExtractParents(353,7908
Derived_p DerivedAlloc(434,9812
long get_clauseform_id(461,10321
void DerivationStackPCLPrint(521,11609
void DerivationStackTSTPPrint(631,14413
void DerivedPCLPrint(753,17682
void DerivedTSTPPrint(818,19498
Derivation_p DerivationAlloc(885,21150
void DerivationFree(910,21729
Derived_p DerivationGetDerived(935,22349
long DerivationExtract(976,23275
long DerivationTopoSort(1057,25554
void DerivationRenumber(1155,28213
Derivation_p DerivationCompute(1191,29037
void DerivationPrint(1225,29850
CLAUSES/ccl_eqn.c,2488
bool EqnUseInfix 35,920
bool EqnFullEquationalRep 36,945
IOFormat OutputFormat 37,980
static CompareResult compare_pos_eqns(113,3702
static CompareResult compare_poseqn_negeqn(180,6146
#define BOOL_TERM_NORMALIZE(244,8094
static bool eqn_parse_infix(266,8637
static bool eqn_parse_prefix(347,11017
static bool eqn_parse_mixfix(403,12343
bool eqn_parse_real(427,12959
Eqn_p EqnAlloc(505,14993
void EqnFree(566,16629
Eqn_p EqnParse(591,17319
Eqn_p EqnFOFParse(618,17873
Term_p EqnTermsTBTermEncode(645,18528
Eqn_p EqnTBTermDecode(689,19529
Term_p EqnTBTermParse(719,20232
void EqnPrint(749,20953
void EqnFOFPrint(853,23143
void EqnTSTPPrint(929,24736
void EqnSwapSidesSimple(970,25769
void EqnSwapSides(993,26249
Eqn_p EqnCopy(1018,26925
Eqn_p EqnFlatCopy(1050,27668
Eqn_p EqnCopyRepl(1082,28364
Eqn_p EqnCopyOpt(1113,29234
Eqn_p EqnCopyDisjoint(1145,30029
bool EqnIsACTrivial(1177,30761
bool EqnTermsAreDistinct(1196,31209
bool EqnIsTrue(1224,32008
bool EqnIsFalse(1246,32458
bool EqnHasUnboundVars(1271,32938
EqnSide EqnIsDefinition(1305,33812
int EqnSubsumeQOrderCompare(1342,34807
int EqnSubsumeInverseCompareRef(1379,35627
int EqnSubsumeInverseRefinedCompareRef(1404,36272
int EqnSubsumeCompare(1448,37330
Eqn_p EqnCanonize(1471,37972
int EqnStructWeightCompare(1505,38743
int EqnCanonCompare(1553,39686
int EqnStructWeightLexCompare(1574,40152
bool EqnEqualDirected(1606,40868
bool EqnEqual(1632,41467
bool EqnSubsumeDirected(1663,42279
bool EqnSubsume(1701,43227
bool EqnSubsumeP(1735,44043
bool LiteralSubsumeP(1760,44614
bool EqnUnifyDirected(1787,45315
bool EqnUnify(1823,46152
bool EqnUnifyP(1851,46778
bool LiteralUnifyOneWay(1876,47405
bool EqnOrient(1921,48336
CompareResult EqnCompare(1988,49774
bool EqnGreater(2009,50218
CompareResult LiteralCompare(2051,51349
bool LiteralGreater(2120,52821
FunCode SubstNormEqn(2143,53392
double EqnWeight(2167,53936
double EqnFunWeight(2200,54645
double EqnNonLinearWeight(2237,55681
double EqnSymTypeWeight(2270,56467
double EqnMaxWeight(2304,57312
double EqnCorrectedWeight(2327,57974
double EqnCorrectedNonLinearWeight(2369,58957
long EqnMaxTermPositions(2413,59918
long EqnInferencePositions(2438,60469
double LiteralWeight(2466,61237
double LiteralFunWeight(2504,62123
double LiteralNonLinearWeight(2547,63368
double LiteralSymTypeWeight(2590,64521
int LiteralCompareFun(2627,65317
void EqnAddSymbolFeatures(2663,66058
long EqnCollectSubterms(2686,66795
CLAUSES/ccl_eqnlist.c,1942
EqnRef eqn_list_find_last(55,1601
void EqnListFree(81,2224
void EqnListGCMarkTerms(106,2676
int EqnListSetProp(129,3128
int EqnListDelProp(156,3641
int EqnListFlipProp(183,4155
int EqnListQueryPropNumber(209,4635
int EqnListLength(238,5127
Eqn_p EqnListFromArray(262,5537
PStack_p EqnListToStack(292,6151
Eqn_p EqnListExtractElement(318,6667
Eqn_p EqnListExtractByProps(342,7179
void EqnListDeleteElement(374,7855
void EqnListInsertElement(396,8303
Eqn_p EqnListAppend(415,8686
Eqn_p EqnListFlatCopy(440,9195
Eqn_p EqnListCopy(470,9835
Eqn_p EqnListCopyExcept(501,10535
Eqn_p EqnListCopyOpt(534,11233
Eqn_p EqnListCopyOptExcept(565,11897
Eqn_p EqnListCopyDisjoint(598,12557
Eqn_p EqnListCopyRepl(630,13230
Eqn_p EqnListNegateEqns(661,13845
int EqnListRemoveDuplicates(688,14419
int EqnListRemoveResolved(726,15129
int EqnListRemoveACResolved(758,15712
int EqnListRemoveSimpleAnswers(791,16318
Eqn_p EqnListFindNegPureVarLit(825,16944
Eqn_p EqnListFindTrue(852,17456
bool EqnListIsTrivial(879,17982
bool EqnListIsACTrivial(918,18707
bool EqnListIsGround(944,19211
bool EqnListIsEquational(973,19718
bool EqnListIsPureEquational(999,20201
int EqnListOrient(1026,20758
int EqnListMaximalLiterals(1057,21415
bool EqnListEqnIsMaximal(1111,22756
bool EqnListEqnIsStrictlyMaximal(1153,23763
void EqnListDeleteTermProperties(1194,24682
void EqnListPrint(1220,25378
void EqnListTSTPPrint(1250,26021
Eqn_p EqnListParse(1280,26666
FunCode NormSubstEqnListExcept(1322,27785
long EqnListDepth(1352,28424
void EqnListAddSymbolDistribution(1382,29112
void EqnListAddSymbolDistExist(1407,29797
void EqnListAddSymbolFeatures(1429,30299
void EqnListComputeFunctionRanks(1452,30817
long EqnListCollectVariables(1475,31358
long EqnListAddFunOccs(1502,31945
void EqnListTermSetProp(1530,32513
long EqnListTBTermDelPropCount(1553,33014
long EqnListTermDelProp(1579,33570
long EqnListCollectSubterms(1606,34228
CLAUSES/ccl_eqnresolution.c,156
bool EqResOnMaximalLiteralsOnly 32,835
Clause_p ComputeEqRes(62,1908
Eqn_p ClausePosFirstEqResLiteral(103,3046
Eqn_p ClausePosNextEqResLiteral(134,3766
CLAUSES/ccl_f_generality.c,742
static void init_fun_gen_cell(54,1594
static void gd_merge_single_res(74,2026
static int fun_gen_tg_cmp_wrapper(104,2758
static int fun_gen_cg_cmp_wrapper(125,3274
static long extract_generality(147,3805
static void compute_d_rel(180,4506
GenDistrib_p GenDistribAlloc(271,7285
void GenDistribFree(303,8086
void GenDistribSizeAdjust(324,8588
void GenDistribAddClause(358,9425
void GenDistribAddClauseSet(390,10212
void GenDistribAddFormula(417,10811
void GenDistribAddFormulaSet(448,11611
void GenDistribAddClauseSetStack(475,12229
void GenDistribAddFormulaSetStack(502,12930
void GenDistPrint(528,13543
int FunGenTGCmp(557,14294
int FunGenCGCmp(589,14929
void ClauseComputeDRel(620,15504
void FormulaComputeDRel(658,16648
CLAUSES/ccl_factor.c,381
Eqn_p find_next_potential_eq_factor_partner(59,1735
Eqn_p find_first_eq_factor_partner(87,2495
Clause_p ComputeOrderedFactor(125,3636
Eqn_p ClausePosFirstOrderedFactorLiterals(184,5309
Eqn_p ClausePosNextOrderedFactorLiterals(224,6415
Clause_p ComputeEqualityFactor(269,7532
Eqn_p ClausePosFirstEqualityFactorSides(330,9630
Eqn_p ClausePosNextEqualityFactorSides(365,10437
CLAUSES/ccl_fcvindexing.c,476
FVIndexParmsCell FVIDefaultParameters 34,849
static FVIndex_p insert_empty_node(104,2230
void FVIndexParmsInit(143,3281
FVIndexParms_p FVIndexParmsAlloc(160,3680
FVIndex_p FVIndexAlloc(182,4131
void FVIndexFree(208,4705
FVIAnchor_p FVIAnchorAlloc(247,5523
void FVIAnchorFree(273,6077
FVIndex_p FVIndexGetNextNonEmptyNode(305,6865
void FVIndexInsert(333,7446
bool FVIndexDelete(384,8776
long FVIndexCountNodes(428,9907
FVPackedClause_p FVIndexPackClause(479,10961
CLAUSES/ccl_findex.c,454
static void findex_add_instance(55,1569
static void findex_remove_instance(76,2064
FIndex_p FIndexAlloc(103,2746
void FIndexFree(125,3149
void FIndexAddClause(152,3663
void FIndexRemoveClause(180,4271
void FIndexAddClauseSet(210,4893
void FIndexAddPLClause(235,5444
void FIndexRemovePLClause(266,6097
void FIndexAddPLClauseSet(296,6746
void FIndexAddPLFormula(323,7285
void FIndexRemovePLFormula(354,7946
void FIndexAddPLFormulaSet(384,8597
CLAUSES/ccl_formula_wrapper.c,526
long global_formula_counter 32,797
long FormulaDefLimit 33,837
WFormula_p DefaultWFormulaAlloc(63,1931
WFormula_p WTFormulaAlloc(93,2712
void WFormulaFree(117,3241
WFormula_p WFormulaFlatCopy(147,3879
void WFormulaGCMarkCells(172,4449
void WFormulaMarkPolarity(189,4849
WFormula_p WFormulaTPTPParse(206,5238
void WFormulaTPTPPrint(270,6843
WFormula_p WFormulaTSTPParse(324,7948
void WFormulaTSTPPrint(395,10107
WFormula_p WFormulaParse(465,11615
void WFormulaPrint(505,12563
long WFormulaReturnFCodes(537,13330
CLAUSES/ccl_formulafunc.c,740
TFormula_p answer_lit_alloc(59,1725
Clause_p tformula_collect_clause(89,2503
static bool verify_name(151,4187
static void check_all_found(182,4892
bool WFormulaConjectureNegate(247,6688
TFormula_p TFormulaAnnotateQuestion(280,7774
bool WFormulaAnnotateQuestion(327,9128
long FormulaSetPreprocConjectures(367,10525
bool WFormulaSimplify(408,11545
long WFormulaCNF(437,12268
long FormulaSetSimplify(459,12926
long FormulaSetCNF(505,14049
long FormulaAndClauseSetParse(566,15782
long TFormulaToCNF(679,19284
void TFormulaSetDelTermpProp(730,20695
void TFormulaSetFindDefs(757,21388
long TFormulaApplyDefs(792,22481
long TFormulaSetIntroduceDefs(850,24345
void FormulaSetArchive(933,27240
void FormulaSetDocInital(966,28050
CLAUSES/ccl_formulasets.c,532
FormulaSet_p FormulaSetAlloc(61,1784
void FormulaSetFreeFormulas(85,2315
void FormulaSetFree(107,2780
long FormulaSetStackCardinality(130,3287
void FormulaSetGCMarkCells(158,3897
void FormulaSetMarkPolarity(183,4410
void FormulaSetInsert(209,4900
long FormulaSetInsertSet(237,5546
WFormula_p FormulaSetExtractEntry(265,6122
WFormula_p FormulaSetExtractFirst(293,6727
void FormulaSetDeleteEntry(317,7197
void FormulaSetPrint(339,7604
long FormulaSetSplitConjectures(368,8298
long long FormulaSetStandardWeight(404,9093
CLAUSES/ccl_freqvectors.c,889
int tuple3_compare_23lex(56,1712
static void gather_feature_vec(102,2551
PermVector_p PermVectorComputeInternal(172,4532
FreqVector_p FreqVectorAlloc(239,6210
void FreqVectorFreeReal(264,6800
void FreqVectorInitialize(292,7339
void FreqVectorPrint(314,7757
void VarFreqVectorAddVals(351,8523
FreqVector_p VarFreqVectorCompute(445,11071
FreqVector_p OptimizedVarFreqVectorCompute(489,12233
void FVCollectInit(539,13436
FVCollect_p FVCollectAlloc(597,15385
void FVCollectFree(649,17065
FreqVector_p FVCollectFreqVectorCompute(669,17515
FVCollect_p BillFeaturesCollectAlloc(732,19145
FVCollect_p BillPlusFeaturesCollectAlloc(818,21258
FVPackedClause_p FVPackClause(896,23180
Clause_p FVUnpackClause(926,23871
void FVPackedClauseFreeReal(951,24323
void FreqVectorAdd(975,24878
void FreqVectorMulAdd(1004,25582
void FreqVectorMax(1032,26193
void FreqVectorMin(1059,26773
CLAUSES/ccl_g_lithash.c,221
void lit_tree_free(56,1698
int LitDescCompare(99,2722
LitHash_p LitHashAlloc(120,3231
void LitHashFree(151,3922
void LitHashInsertEqn(179,4590
void LitHashInsertClause(222,5619
void LitHashInsertClauseSet(245,6149
CLAUSES/ccl_garbage_coll.c,229
GCAdmin_p GCAdminAlloc(60,1831
void GCAdminFree(87,2363
void GCRegisterFormulaSet(110,2833
void GCRegisterClauseSet(130,3286
void GCDeregisterFormulaSet(150,3750
void GCDeregisterClauseSet(169,4220
long GCCollect(188,4640
CLAUSES/ccl_global_indices.c,264
void GlobalIndicesNull(63,1849
void GlobalIndicesInit(84,2364
void GlobalIndicesFreeIndices(132,3848
void GlobalIndicesReset(169,4719
void GlobalIndicesInsertClause(193,5346
void GlobalIndicesDeleteClause(237,6556
void GlobalIndicesInsertClauseSet(280,7761
CLAUSES/ccl_groundconstr.c,432
LitOccTable_p LitOccTableAlloc(64,1999
void LitOccTableFree(101,2954
bool LitPosGetConstrState(135,3685
void LitPosSetConstrState(158,4249
PTree_p LitPosGetConstraints(182,4879
bool LitPosAddConstraint(207,5560
void LitOccAddLitAlt(237,6209
void LitOccAddClauseAlt(275,6933
void LitOccAddClauseSetAlt(300,7498
long SigCollectConstantTerms(329,8260
void EqnCollectVarConstr(386,9672
void ClauseCollectVarConstr(439,10868
CLAUSES/ccl_grounding.c,1007
long clause_get_max_lit(57,1754
void varsetinstapply(83,2341
void varsetinstclear(112,3114
bool varsetinstinitialize(136,3658
double varinstestimate(166,4272
bool varsetinstnext(193,4862
void ground_set_print_unit(223,5496
int ClauseCmpByLen(255,6502
bool EqnEqlitRecode(282,7227
bool ClauseEqlitRecode(316,8066
long ClauseSetEqlitRecode(342,8626
VarSetInst_p VarSetInstAlloc(372,9251
void VarSetInstFree(414,10155
VarSetInst_p VarSetConstrInstAlloc(447,10825
void VarSetConstrInstFree(513,12427
void PrintDimacsHeader(550,13141
void ClausePrintDimacs(572,13598
void ClauseSetPrintDimacs(611,14456
GroundSet_p GroundSetAlloc(635,14972
void GroundSetFree(665,15672
long GroundSetMaxVar(691,16339
bool GroundSetInsert(729,17107
void GroundSetPrint(788,18477
void GroundSetPrintDimacs(823,19284
bool GroundSetUnitSimplifyClause(864,20289
bool ClauseCreateGroundInstances(928,21556
bool ClauseSetCreateGroundInstances(1005,23348
bool ClauseSetCreateConstrGroundInstances(1088,25335
CLAUSES/ccl_inferencedoc.c,1903
OutputFormatType DocOutputFormat 33,834
bool PCLFullTerms 34,883
bool PCLStepCompact 35,923
int PCLShellLevel 36,964
char* PCLTypeStr(61,1838
static void pcl_print_start(96,2492
static void pcl_print_end(119,3092
static void tstp_print_end(150,3826
static void print_initial(180,4476
static void print_paramod(216,5366
static void print_eres(255,6360
static void print_des_eres(291,7275
static void print_efactor(327,8178
static void print_factor(363,9079
static void print_split(401,9997
static void print_simplify_reflect(439,10986
static void print_context_simplify_reflect(476,11972
static void print_ac_res(515,12965
static void print_minimize(571,14409
static void print_condense(608,15374
static void print_eval_answer(644,16390
static void print_rewrite(679,17346
static void print_eq_unfold(750,19224
static void pcl_formula_print_start(813,20790
static void pcl_formula_print_end(837,21427
static void tstp_formula_print_end(859,21899
static void print_formula_initial(881,22337
static void print_fof_intro_def(916,23209
static void print_fof_split_equiv(952,24077
static void print_fof_simpl(990,25048
static void print_neg_conj(1024,25954
static void print_fof_nnf(1058,26844
static void print_shift_quantors(1093,27783
static void print_skolemize(1128,28676
static void print_distribute(1162,29566
static void print_annotate_question(1195,30477
static void print_var_rename(1231,31404
void DocClauseCreation(1272,32594
void DocClauseFromForm(1339,34388
void DocClauseModification(1383,35662
void DocClauseQuote(1462,37888
void DocClauseRewrite(1531,39525
void DocClauseEqUnfold(1562,40352
void DocFormulaCreation(1590,41080
void DocFormulaModification(1636,42299
void DocFormulaIntroDefs(1690,43807
void DocIntroSplitDef(1755,45716
void DocIntroSplitDefRest(1784,46420
void DocClauseApplyDefs(1829,47731
CLAUSES/ccl_neweval.c,700
long EvaluationCounter 30,835
static Eval_p evals_alloc_raw(54,1628
static Eval_p splay_tree(77,2102
Eval_p EvalsAlloc(172,4449
void EvalsFree(195,4924
void EvalPrint(217,5360