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
|
/*-----------------------------------------------------------------------
File : che_wfcb.c
Author: Stephan Schulz (schulz@eprover.org)
Contents
Functions for evaluation function control blocks.
Copyright 1998-2018 by the authors (see DOC/CONTRIBUTORS).
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: Fri Jun 5 22:05:39 MET DST 1998
-----------------------------------------------------------------------*/
#include "che_wfcb.h"
/*---------------------------------------------------------------------*/
/* Global Variables */
/*---------------------------------------------------------------------*/
/*---------------------------------------------------------------------*/
/* Forward Declarations */
/*---------------------------------------------------------------------*/
/*---------------------------------------------------------------------*/
/* Internal Functions */
/*---------------------------------------------------------------------*/
/*---------------------------------------------------------------------*/
/* Exported Functions */
/*---------------------------------------------------------------------*/
/*-----------------------------------------------------------------------
//
// Function: WFCBAlloc()
//
// Create and return an initialized WFCB-block.
//
// Global Variables: -
//
// Side Effects : Memory operations
//
/----------------------------------------------------------------------*/
WFCB_p WFCBAlloc(ClauseEvalFun wfcb_eval, ClausePrioFun prio_fun,
GenericExitFun wfcb_exit, void* data)
{
WFCB_p handle = WFCBCellAlloc();
handle->wfcb_eval = wfcb_eval;
handle->wfcb_priority = prio_fun;
handle->wfcb_exit = wfcb_exit;
handle->data = data;
return handle;
}
/*-----------------------------------------------------------------------
//
// Function: WFCBFree()
//
// Free a WFCB.
//
// Global Variables: -
//
// Side Effects : Memory operations
//
/----------------------------------------------------------------------*/
void WFCBFree(WFCB_p junk)
{
assert(junk);
if(junk->data)
{
junk->wfcb_exit(junk->data);
}
WFCBCellFree(junk);
}
/*-----------------------------------------------------------------------
//
// Function: ClauseAddEvaluation()
//
// Given a clause and a wfcb, add an evaluation to the clause.
//
// Global Variables: -
//
// Side Effects : Adds evaluation, by calling wfcb->compute_eval()
//
/----------------------------------------------------------------------*/
void ClauseAddEvaluation(WFCB_p wfcb, Clause_p clause, int pos, bool empty)
{
assert(clause->evaluations);
clause->evaluations->evals[pos].heuristic = wfcb->wfcb_eval(wfcb->data, clause);
if(empty)
{
clause->evaluations->evals[pos].priority = PrioBest;
}
else
{
clause->evaluations->evals[pos].priority = wfcb->wfcb_priority(clause);
}
}
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
