1 /*-----------------------------------------------------------------------
2 
3 File  : ccl_clauseinfo.h
4 
5 Author: Stephan Schulz (schulz@eprover.org)
6 
7 Contents
8 
9   Datatype and basic functions for storing and handling clause
10   information that few clauses carry (probably just input
11   clauses). This is not stored in the clause (or formula) data types,
12   because it would eat  up to much memory (remember, there are
13   millions of clauses)
14 
15   Copyright 2004-1017 by the authors.
16   This code is released under the GNU General Public Licence and
17   the GNU Lesser General Public License.
18   See the file COPYING in the main E directory for details..
19   Run "eprover -h" for contact information.
20 
21 Changes
22 
23 
24 -----------------------------------------------------------------------*/
25 
26 #ifndef CCL_CLAUSEINFO
27 
28 #define CCL_CLAUSEINFO
29 
30 #include <clb_memory.h>
31 #include <clb_dstrings.h>
32 
33 
34 /*---------------------------------------------------------------------*/
35 /*                    Data type declarations                           */
36 /*---------------------------------------------------------------------*/
37 
38 typedef struct clause_info_cell
39 {
40    char *name;   /* In the input file, if any */
41    char *source; /* File name, if any */
42    long line;
43    long column;
44 }ClauseInfoCell, *ClauseInfo_p;
45 
46 
47 
48 /*---------------------------------------------------------------------*/
49 /*                Exported Functions and Variables                     */
50 /*---------------------------------------------------------------------*/
51 
52 #define ClauseInfoCellAlloc()    (ClauseInfoCell*)SizeMalloc(sizeof(ClauseInfoCell))
53 #define ClauseInfoCellFree(junk) SizeFree(junk, sizeof(ClauseInfoCell))
54 
55 ClauseInfo_p ClauseInfoAlloc(char* name, char* source, long line, long column);
56 #define      ClauseInfoAllocEmpty() ClauseInfoAlloc(NULL, NULL, -1, -1)
57 void         ClauseInfoFree(ClauseInfo_p info);
58 void         ClauseSourceInfoPrint(FILE* out, ClauseInfo_p info,
59                                    char *inf_lit, char* delim);
60 #define ClauseSourceInfoPrintTSTP(out, info) \
61         ClauseSourceInfoPrint((out), (info), "file", "'")
62 
63 #define ClauseSourceInfoPrintPCL(out, info) \
64         ClauseSourceInfoPrint((out), (info), "initial", "\"")
65 long    ClauseInfoGetIdNameSpace(ClauseInfo_p info);
66 long    ClauseInfoGetIdCounter(ClauseInfo_p info);
67 
68 
69 #endif
70 
71 /*---------------------------------------------------------------------*/
72 /*                        End of File                                  */
73 /*---------------------------------------------------------------------*/
74