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
|
/*-----------------------------------------------------------------------
File : che_diversityweight.h
Author: Stephan Schulz
Contents
Evaluation of a clause by refined diversity clause weight, using
weight penalty factors for maximal terms and literals, and penalties
for clauses with many different function symbols and variables.
Copyright 2019 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 May 27 00:55:33 CEST 2019
-----------------------------------------------------------------------*/
#ifndef CHE_DIVERSITYWEIGHT
#define CHE_DIVERSITYWEIGHT
#include <che_clauseweight.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
#define DEFAULT_MAX_MULT 1.5
typedef struct diversityweightparamcell
{
OCB_p ocb;
double max_term_multiplier;
double max_literal_multiplier;
double pos_multiplier;
double app_var_mult;
long vweight;
long fweight;
double fdiff1weight;
double fdiff2weight;
double vdiff1weight;
double vdiff2weight;
}DiversityWeightParamCell, *DiversityWeightParam_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define DiversityWeightParamCellAlloc() (DiversityWeightParamCell*) \
SizeMalloc(sizeof(DiversityWeightParamCell))
#define DiversityWeightParamCellFree(junk) \
SizeFree(junk, sizeof(DiversityWeightParamCell))
WFCB_p DiversityWeightInit(ClausePrioFun prio_fun, int fweight,
int vweight, OCB_p ocb,
double max_term_multiplier,
double max_literal_multiplier,
double pos_multiplier,
double fdiff1weight,
double fdiff2weight,
double vdiff1weight,
double vdiff2weight,
double app_var_mult);
WFCB_p DiversityWeightParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double DiversityWeightCompute(void* data, Clause_p clause);
void DiversityWeightExit(void* data);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
