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
|
/*-----------------------------------------------------------------------
File : ccl_neweval.h
Author: Stephan Schulz
Contents
Data type for representing evaluations of clauses.
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> Thu Apr 9 02:00:51 MET DST 1998
New
<2> Thu Jan 28 00:58:19 MET 1999
Replaced AVL trees with Splay-Trees
<3> Thu Apr 20 00:32:11 CEST 2006
Imported code and history for new, more efficient evaluations for
ccl_evaluations.h
-----------------------------------------------------------------------*/
#ifndef CCL_NEWEVAL
#define CCL_NEWEVAL
#include <clb_avlgeneric.h>
#include <clb_ptrees.h>
#include <clb_sysdate.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef long EvalPriority;
#define PrioBest 0
#define PrioPrefer 30
#define PrioNormal 40
#define PrioDefer 50
#define PrioLargestReasonable MEGA
typedef struct simple_eval_cell
{
EvalPriority priority; /* Technical considerations */
float heuristic; /* Heuristical evaluation */
struct eval_cell* lson; /* Successors in ordered tree */
struct eval_cell* rson;
}SimpleEvalCell, *SimpleEval_p;
typedef struct eval_cell
{
int eval_no; /* Number of simple evaluations */
long eval_count; /* Evaluation cell count, used as
FIFO tiebreaker */
void* object; /* Evaluated object.*/
SimpleEvalCell evals[];
}EvalCell, *Eval_p;
/*---------------------------------------------------------------------*/
/* Macros for a common interface with old evaluations */
/*---------------------------------------------------------------------*/
//#define EvalsFree(eval) EvalsFree(eval)
//#define EvalTreeFindSmallestWrap(root, pos) EvalTreeFindSmallest((root), (pos))
//#define EvalTreePrintInOrderWrap(file, root, pos) EvalTreePrintInOrder(file, root, pos)
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
extern long EvaluationCounter;
#define EVAL_SIZE(eval_no) (sizeof(EvalCell)+((eval_no)*sizeof(SimpleEvalCell)))
#define EvalCellAlloc(eval_no) (EvalCell*)SizeMalloc(EVAL_SIZE(eval_no))
#define EvalCellFree(junk, eval_no) SizeFree(junk, EVAL_SIZE(eval_no))
#ifdef CONSTANT_MEM_ESTIMATE
#define EVAL_MEM(eval_no) (32+(4*(eval_no)))
#else
#define EVAL_MEM(eval_no) (MEMSIZE(EvalCell)+(EVAL_SIZE((eval_no))))
#endif
Eval_p EvalsAlloc(int eval_no);
void EvalsFree(Eval_p junk);
void EvalPrint(FILE* out, Eval_p list, int pos);
void EvalPrintComment(FILE* out, Eval_p list, int pos);
void EvalListPrint(FILE* out, Eval_p list);
void EvalListPrintComment(FILE* out, Eval_p list);
void EvalSetPriority(Eval_p list, EvalPriority priority);
void EvalListChangePriority(Eval_p list, EvalPriority diff);
bool EvalGreater(Eval_p ev1, Eval_p ev2, int pos);
long EvalCompare(Eval_p ev1, Eval_p ev2, int pos);
Eval_p EvalTreeInsert(Eval_p *root, Eval_p newnode, int pos);
Eval_p EvalTreeFind(Eval_p *root, Eval_p key, int pos);
Eval_p EvalTreeExtractEntry(Eval_p *root, Eval_p key, int pos);
bool EvalTreeDeleteEntry(Eval_p *root, Eval_p key, int pos);
Eval_p EvalTreeFindSmallest(Eval_p root, int pos);
/* AVL_TRAVERSE_DECLARATION(EvalTree,Eval_p) */
#define EvalTreeTraverseExit(stack) PStackFree(stack)
PStack_p EvalTreeTraverseInit(Eval_p root, int pos);
Eval_p EvalTreeTraverseNext(PStack_p state, int pos);
void EvalTreePrintInOrder(FILE* out, Eval_p tree, int pos);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
