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
|
/*-----------------------------------------------------------------------
File : ccl_clauseinfo.h
Author: Stephan Schulz (schulz@eprover.org)
Contents
Datatype and basic functions for storing and handling clause
information that few clauses carry (probably just input
clauses). This is not stored in the clause (or formula) data types,
because it would eat up to much memory (remember, there are
millions of clauses)
Copyright 2004-1017 by the authors.
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
-----------------------------------------------------------------------*/
#ifndef CCL_CLAUSEINFO
#define CCL_CLAUSEINFO
#include <clb_memory.h>
#include <clb_dstrings.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct clause_info_cell
{
char *name; /* In the input file, if any */
char *source; /* File name, if any */
long line;
long column;
}ClauseInfoCell, *ClauseInfo_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define ClauseInfoCellAlloc() (ClauseInfoCell*)SizeMalloc(sizeof(ClauseInfoCell))
#define ClauseInfoCellFree(junk) SizeFree(junk, sizeof(ClauseInfoCell))
ClauseInfo_p ClauseInfoAlloc(char* name, char* source, long line, long column);
#define ClauseInfoAllocEmpty() ClauseInfoAlloc(NULL, NULL, -1, -1)
void ClauseInfoFree(ClauseInfo_p info);
void ClauseSourceInfoPrint(FILE* out, ClauseInfo_p info,
char *inf_lit, char* delim);
#define ClauseSourceInfoPrintTSTP(out, info) \
ClauseSourceInfoPrint((out), (info), "file", "'")
#define ClauseSourceInfoPrintPCL(out, info) \
ClauseSourceInfoPrint((out), (info), "initial", "\"")
long ClauseInfoGetIdNameSpace(ClauseInfo_p info);
long ClauseInfoGetIdCounter(ClauseInfo_p info);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
