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
|
/*-----------------------------------------------------------------------
File : che_simweight.h
Author: Stephan Schulz
Contents
Evaluation of a clause by similarity of terms (equations with
similar terms have low weight).
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.
Changes
<1> Sun Jun 28 18:18:00 MET DST 1998
New
-----------------------------------------------------------------------*/
#ifndef CHE_SIMWEIGHT
#define CHE_SIMWEIGHT
#include <che_wfcb.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct simparamcell
{
double equal_weight;
double var_var_clash;
double var_term_clash;
double term_term_clash;
double app_var_mult;
}SimParamCell, *SimParam_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define SimParamCellAlloc() (SimParamCell*) \
SizeMalloc(sizeof(SimParamCell))
#define SimParamCellFree(junk) \
SizeFree(junk, sizeof(SimParamCell))
WFCB_p SimWeightInit(ClausePrioFun prio_fun, double equal_weight,
double var_var_clash, double var_term_clash,
double term_term_clash, double app_var_mult);
WFCB_p SimWeightParse(Scanner_p in, OCB_p ocb, ProofState_p state);
double SimWeightCompute(void* data, Clause_p clause);
void SimWeightExit(void* data);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
