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
|
/*-----------------------------------------------------------------------
File : pcl_positions.h
Author: Stephan Schulz
Contents
Positions in PCL2 clauses.
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> Wed Mar 22 19:32:20 MET 2000
New
-----------------------------------------------------------------------*/
#ifndef PCL_POSITIONS
#define PCL_POSITIONS
#include <ccl_eqn.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/* Position is literal, side, position in term. Except for the
position, everything is optional. Empty term position is expressed
by both termposlen==0 and termpos==NULL, unless I decide otherwise
;-) */
typedef struct pcl2poscell
{
long literal;
EqnSide side;
long termposlen; /* Might take a stack here, but stacks will */
PDArray_p termpos; /* be, on average, much to large */
}PCL2PosCell, *PCL2Pos_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define PCL2PosCellAlloc() (PCL2PosCell*)SizeMalloc(sizeof(PCL2PosCell))
#define PCL2PosCellFree(junk) SizeFree(junk, sizeof(PCL2PosCell))
PCL2Pos_p PCL2PosAlloc(void);
void PCL2PosFree(PCL2Pos_p pos);
PCL2Pos_p PCL2PosParse(Scanner_p in);
void PCL2PosPrint(FILE* out, PCL2Pos_p pos);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
