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
|
/*-----------------------------------------------------------------------
File : che_learning.h
Author: Stephan Schulz
Contents
Evaluation of a clause by tsm-based learning algorithms
Copyright 1998, 1999 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.
Created: Mon Aug 30 19:17:53 MET DST 1999
-----------------------------------------------------------------------*/
#ifndef CHE_LEARNING
#define CHE_LEARNING
#include <che_wfcb.h>
#include <cle_tsmio.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
#define DEFAULT_POS_MULT 1
/* As it is fairly expensive to create a suitable TSM (about 10-40
seconds) we only want to create it when we really need to use
it. Therefore we hack this as follows: All relevant data is stored
in the parameter cell, and the TSM is created if the
evaluation function is called for the first time. */
typedef struct tsmparamcell
{
long fweight;
long vweight;
double max_term_multiplier; /* For TSWRWeight only */
double max_literal_multiplier; /* For TSWRWeight only */
double pos_multiplier; /* For TSWRWeight only */
bool flat_clauses;
double learnweight;
char* kb;
ProofState_p state;
long sel_no;
double set_part;
double dist_part;
IndexType indextype;
TSMType tsmtype;
long depth;
double e_weights[ANNOTATION_DEFAULT_SIZE-1];
double eval_base;
double eval_scale;
PatternSubst_p pat_subst;
TSMAdmin_p tsmadmin;
}TSMParamCell, *TSMParam_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define TSMParamCellAlloc() (TSMParamCell*) \
SizeMalloc(sizeof(TSMParamCell))
#define TSMParamCellFree(junk) \
SizeFree(junk, sizeof(TSMParamCell))
WFCB_p TSMWeightInit(ClausePrioFun prio_fun, int fweight,
int vweight, bool flat_clauses, double
learnweight, char* kb, ProofState_p state, long
sel_no, double set_part, double dist_part,
IndexType indextype, TSMType tsmtype, long depth,
double proofs_w, double dist_w, double p_simp_w,
double f_simp_w, double p_gen_w, double f_gen_w);
WFCB_p TSMWeightParse(Scanner_p in, OCB_p ocb, ProofState_p state);
double TSMWeightCompute(void* data, Clause_p clause);
WFCB_p TSMRWeightInit(ClausePrioFun prio_fun, int fweight,
int vweight, double max_term_multiplier, double
max_literal_multiplier, double pos_multiplier,
bool flat_clauses, double
learnweight, char* kb, ProofState_p state, long
sel_no, double set_part, double dist_part,
IndexType indextype, TSMType tsmtype, long depth,
double proofs_w, double dist_w, double p_simp_w,
double f_simp_w, double p_gen_w, double f_gen_w);
WFCB_p TSMRWeightParse(Scanner_p in, OCB_p ocb, ProofState_p state);
double TSMRWeightCompute(void* data, Clause_p clause);
void TSMWeightExit(void* data);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
