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
|
/*-----------------------------------------------------------------------
File : pcl_propanalysis.h
Author: Stephan Schulz
Contents
Functions for computing various properties of the clauses in a PCL
protocol.
Copyright 2002 by the author.
This code is released under the GNU General Public Licence and
the GNU Lesser General Public License.
See the file COPYING in the main E directory for details..
Run "eprover -h" for contact information.
Changes
<1> Thu Feb 28 16:27:34 MET 2002
New
-----------------------------------------------------------------------*/
#ifndef PCL_PROPANALYIS
#define PCL_PROPANALYIS
#include <che_clausefeatures.h>
#include <pcl_protocol.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct pcl_propdata_cell
{
long fof_formulae;
long pos_clauses;
long neg_clauses;
long mix_clauses;
long pos_clause_literals;
long neg_clause_literals;
long mix_clause_literals;
long pos_literals;
long neg_literals;
long const_count;
long func_count;
long pred_count;
long var_count;
PCLStep_p longest_clause;
PCLStep_p max_symbol_clause;
PCLStep_p max_standard_weight_clause;
PCLStep_p max_depth_clause;
}PCLPropDataCell, *PCLPropData_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
typedef int (*PCLCmpFunType)(const PCLStep_p, const PCLStep_p);
PCLStep_p PCLProtFindMaxStep(PCLProt_p prot, PCLCmpFunType cmp);
void PCLProtPropAnalyse(PCLProt_p prot, PCLPropData_p data);
void PCLProtPropDataPrint(FILE* out, PCLPropData_p data);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
