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
|
/*-----------------------------------------------------------------------
File : ccl_f_generality.h
Author: Stephan Schulz (schulz@eprover.org)
Contents
Code for computing the generality of function/predicate symbols
using a generalize SinE approach, counting occurences in terms,
literals, clauses, and formulas.
Copyright 2010 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> Wed Jun 30 23:30:02 CEST 2010
New
-----------------------------------------------------------------------*/
#ifndef CCL_F_GENERALITY
#define CCL_F_GENERALITY
#include <ccl_formulasets.h>
#include <ccl_clausesets.h>
#include <che_axfilter.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/* How often does a give f_code occur in certain substructures? */
typedef struct fun_gen_cell
{
FunCode f_code;
long term_freq;
long fc_freq;
}FunGenCell, *FunGen_p;
/* Distribution of the above... */
typedef struct gen_distrib_cell
{
Sig_p sig;
long size;
FunGen_p dist_array;
long *f_distrib;
}GenDistribCell, *GenDistrib_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define GenDistribCellAlloc() (GenDistribCell*)SizeMalloc(sizeof(GenDistribCell))
#define GenDistribCellFree(junk) SizeFree(junk, sizeof(GenDistribCell))
GenDistrib_p GenDistribAlloc(Sig_p sig);
void GenDistribFree(GenDistrib_p junk);
void GenDistribSizeAdjust(GenDistrib_p gd, Sig_p sig);
void GenDistribAddClause(GenDistrib_p dist, Clause_p clause,
short factor);
void GenDistribAddClauseSet(GenDistrib_p dist, ClauseSet_p set,
short factor);
void GenDistribAddFormula(GenDistrib_p dist, WFormula_p form,
short factor);
void GenDistribAddFormulaSet(GenDistrib_p dist,
FormulaSet_p set,
short factor);
void GenDistribAddClauseSetStack(GenDistrib_p dist,
PStack_p stack,
PStackPointer start,
short factor);
void GenDistribAddFormulaSetStack(GenDistrib_p dist,
PStack_p stack,
PStackPointer start,
short factor);
#define GenDistribAddClauseSets(dist, stack) \
GenDistribAddClauseSetStack((dist), (stack), 0, 1)
#define GenDistribAddFormulaSets(dist, stack) \
GenDistribAddFormulaSetStack((dist), (stack), 0, 1)
#define GenDistribBacktrackClauseSets(dist, stack, sp) \
GenDistribAddClauseSetStack((dist), (stack), (sp), -1)
#define GenDistribBacktrackFormulaSets(dist, stack, sp) \
GenDistribAddFormulaSetStack((dist), (stack), (sp), -1)
void GenDistPrint(FILE* out, GenDistrib_p dist);
int FunGenTGCmp(const FunGen_p fg1, const FunGen_p fg2);
int FunGenCGCmp(const FunGen_p fg1, const FunGen_p fg2);
void ClauseComputeDRel(GenDistrib_p generality,
GeneralityMeasure gentype,
double benevolence,
long generosity,
Clause_p clause,
PStack_p res);
void FormulaComputeDRel(GenDistrib_p generality,
GeneralityMeasure gentype,
double benevolence,
long generosity,
WFormula_p form,
PStack_p res);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
