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
|
/*-----------------------------------------------------------------------
File : pcl_lemmas.h
Author: Stephan Schulz
Contents
Definition for dealing with lemmas in PCL protocols.
Copyright 1998-2011 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> Sun Jun 15 22:47:43 CEST 2003
New
-----------------------------------------------------------------------*/
#ifndef PCL_LEMMAS
#define PCL_LEMMAS
#include <pcl_protocol.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/* Lemma rating is as follows:
size = StandardWeight(lemma)
actpm = references as active partner in paramod
o_gen = references from other generating inferences
act_simpl = references from active simplification
pas_simpl = references from being simplified
subsum = references from subsumption (will probably not always be
available)
proof_tree = size of proof tree (unfolded)
proof_dag = size of proof tree seen as a dag
(1+
actpm*actpm_w +
o_gen*o_gen_w +
act_simpl*act_simpl_w +
pas_simpl*pas_simpl_w +
subsum*subsum_w)
*
(1+
proof_tree*proof_tree_w+
proof_dag*proof_dag_w)
/
1+size*size_w
Large is good! */
typedef struct lemma_param_cell
{
long tree_base_weight;
double act_pm_w;
double o_gen_w;
double act_simpl_w;
double pas_simpl_w;
double proof_tree_w;
double proof_dag_w;
long size_base_weight;
double horn_bonus;
}LemmaParamCell, *LemmaParam_p;
#define LEMMA_TREE_BASE_W 1
#define LEMMA_ACT_PM_W 2.0
#define LEMMA_O_GEN_W 1.0
#define LEMMA_ACT_SIMPL_W 2.0
#define LEMMA_PAS_SIMPL_W 1.0
#define LEMMA_PROOF_TREE_W 1.0
#define LEMMA_PROOF_DAG_W 0.0 /* Don't know how to efficiently compute
* DAG size at the moment */
#define LEMMA_SIZE_BASE_W 1
#define LEMMA_HORN_BONUS_W 2.0
typedef long InferenceWeightType[PCLOpMaxOp];
typedef InferenceWeightType *InferenceWeight_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define LemmaParamCellAlloc() (LemmaParamCell*)SizeMalloc(sizeof(LemmaParamCell))
#define LemmaParamCellFree(junk) SizeFree(junk, sizeof(LemmaParamCell))
LemmaParam_p LemmaParamAlloc(void);
#define LemmaParamFree(cell) LemmaParamCellFree(cell)
#define InferenceWeightCellAlloc()\
(InferenceWeight_p)SizeMalloc(sizeof(InferenceWeightType))
#define InferenceWeightCellFree(junk) \
SizeFree(junk, sizeof(InferenceWeightType))
InferenceWeight_p InferenceWeightsAlloc(void);
#define InferenceWeightsFree(junk) InferenceWeightCellFree(junk)
void PCLExprUpdateRefs(PCLProt_p prot, PCLExpr_p expr);
void PCLStepUpdateRefs(PCLProt_p prot, PCLStep_p step);
void PCLProtUpdateRefs(PCLProt_p prot);
int PCLStepLemmaCmpWrapper(const void* s1, const void* s2);
int PCLStepLemmaCmp(PCLStep_p step1, PCLStep_p step2);
long PCLExprProofSize(PCLProt_p prot, PCLExpr_p expr, InferenceWeight_p iw,
bool use_lemmas);
long PCLStepProofSize(PCLProt_p prot, PCLStep_p step, InferenceWeight_p iw,
bool use_lemmas);
void PCLProtComputeProofSize(PCLProt_p prot, InferenceWeight_p iw,
bool use_lemmas);
float PCLStepComputeLemmaWeight(PCLProt_p prot, PCLStep_p step,
LemmaParam_p params);
PCLStep_p PCLProtComputeLemmaWeights(PCLProt_p prot, LemmaParam_p params);
long PCLProtSeqFindLemmas(PCLProt_p prot, LemmaParam_p params,
InferenceWeight_p iw, long max_number,
float quality_limit);
long PCLProtRecFindLemmas(PCLProt_p prot, LemmaParam_p params,
InferenceWeight_p iw, long max_number,
float quality_limit);
long PCLProtFlatFindLemmas(PCLProt_p prot, LemmaParam_p params,
InferenceWeight_p iw, long max_number,
float quality_limit);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
