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
|
/*-----------------------------------------------------------------------
File : che_axfilter.h
Author: Stephan Schulz (schulz@eprover.org)
Contents
Definitions dealing with the description of axiom set filters based
on relevancy/SinE principles. This only deals with their parameters
and specifications. The real code is (for now) in CONTROL and knows
nothing about this ;-).
Copyright 2011 by the author.
This code is released under the GNU General Public Licence.
See the file COPYING in the main CLIB directory for details.
Run "eprover -h" for contact information.
Changes
<1> Wed Feb 23 00:17:20 CET 2011
New
-----------------------------------------------------------------------*/
#ifndef CHE_AXFILTER
#define CHE_AXFILTER
#include <clb_simple_stuff.h>
#include <cio_basicparser.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef enum
{
AFNoFilter = 0,
AFGSinE, /* Generalized SinE */
AFThreshold /* Pass all formulas if less then N */
}AxFilterType;
/* Type of generality measure: Number of occurences in terms or in
* formulas (and possibly later in equations). */
typedef enum
{
GMNoMeasure,
GMTerms,
GMLiterals,
GMFormulas,
GMPosFormula,
GMPosLiteral,
GMPosTerms,
GMNegFormula,
GMNegLiteral,
GMNegTerms
}GeneralityMeasure;
/* Parameters for a single Axiom filter */
typedef struct
{
char* name;
AxFilterType type;
GeneralityMeasure gen_measure;
bool use_hypotheses;
double benevolence;
long generosity;
long max_recursion_depth;
long long max_set_size;
long threshold;
double max_set_fraction;
bool add_no_symbol_axioms;
}AxFilterCell, *AxFilter_p;
/* Sets of AxFilters */
typedef struct
{
PStack_p set;
}AxFilterSetCell, *AxFilterSet_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
extern char* AxFilterDefaultSet;
#define AxFilterCellAlloc() (AxFilterCell*)SizeMalloc(sizeof(AxFilterCell))
#define AxFilterCellFree(junk) SizeFree(junk, sizeof(AxFilterCell))
AxFilter_p AxFilterAlloc(void);
void AxFilterFree(AxFilter_p junk);
AxFilter_p AxFilterParse(Scanner_p in);
AxFilter_p AxFilterDefParse(Scanner_p in);
bool AxFilterPrintBuf(char* buf, int buflen, AxFilter_p filter);
void AxFilterPrint(FILE* out, AxFilter_p filter);
void AxFilterDefPrint(FILE* out, AxFilter_p filter);
#define AxFilterSetCellAlloc() (AxFilterSetCell*)SizeMalloc(sizeof(AxFilterSetCell))
#define AxFilterSetCellFree(junk) SizeFree(junk, sizeof(AxFilterSetCell))
AxFilterSet_p AxFilterSetAlloc(void);
void AxFilterSetFree(AxFilterSet_p junk);
long AxFilterSetParse(Scanner_p in, AxFilterSet_p set);
AxFilterSet_p AxFilterSetCreateInternal(char* str);
void AxFilterSetPrint(FILE* out, AxFilterSet_p set);
#define AxFilterSetElements(s) PStackGetSP((s)->set)
#define AxFilterSetGetFilter(s, i) ((AxFilter_p)PStackElementP((s)->set,(i)))
#define AxFilterSetAddFilter(s, f) PStackPushP((s)->set, (f))
AxFilter_p AxFilterSetFindFilter(AxFilterSet_p set, char* name);
void AxFilterSetAddNames(DStr_p res, AxFilterSet_p filters);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
