1 /*-----------------------------------------------------------------------
2 
3 File  : can_clausestore.h
4 
5 Author: Stephan Schulz
6 
7 Contents
8 
9   Data type for compact storing of clauses, indexed by identifier, for
10   analysis purposes.
11 
12   Copyright 1998, 1999 by the author.
13   This code is released under the GNU General Public Licence and
14   the GNU Lesser General Public License.
15   See the file COPYING in the main E directory for details..
16   Run "eprover -h" for contact information.
17 
18 Changes
19 
20 <1> Sat Jul  5 02:28:25 MET DST 1997
21     New
22 
23 -----------------------------------------------------------------------*/
24 
25 #ifndef CAN_CLAUSESTORE
26 
27 #define CAN_CLAUSESTORE
28 
29 #include <ccl_clauses.h>
30 #include <can_clausestats.h>
31 
32 
33 /*---------------------------------------------------------------------*/
34 /*                    Data type declarations                           */
35 /*---------------------------------------------------------------------*/
36 
37 /* Represent a clause as compact as possible for analysis
38    purposes. You need some context to interprete this, in particular
39    the term bank. */
40 
41 typedef struct compact_clause_cell
42 {
43    FormulaProperties properties;
44    long              ident;
45    long              ext_ident;   /* Ident of the current version of
46                                      the clause for PCL generation */
47    short            literal_no;
48    short            *sign; /* For literals */
49    Term_p           *lit_terms; /* Literals are just pairs of terms */
50    PTree_p          g_parents; /* Generating parents */
51    PTree_p          s_parents; /* Simplifying parents */
52    ClauseStatsCell  stats;
53 }CompClauseCell, *CompClause_p;
54 
55 
56 
57 
58 /*---------------------------------------------------------------------*/
59 /*                Exported Functions and Variables                     */
60 /*---------------------------------------------------------------------*/
61 
62 #define CompClauseCellAlloc()\
63         (CompClauseCell*)SizeMalloc(sizeof(CompClauseCell))
64 #define CompClauseCellFree(junk)\
65         SizeFree(junk, sizeof(CompClauseCell))
66 
67 void         CompClauseFree(CompClause_p clause, TB_p bank);
68 
69 void CompClauseAddTerms(CompClause_p clause, Clause_p term_clause);
70 void CompClauseRemoveTerms(CompClause_p clause, TB_p bank);
71 
72 CompClause_p PackClause(Clause_p clause);
73 Clause_p     UnpackClause(CompClause_p clause, TB_p bank);
74 
75 CompClause_p CompactifyClause(Clause_p clause);
76 Clause_p     UnCompactifyClause(CompClause_p clause, TB_p bank);
77 
78 void CompClausePrint(FILE* out, CompClause_p compact, TB_p bank, bool
79            full_terms);
80 
81 void CompClausePCLPrint(FILE* out, CompClause_p compact, TB_p bank);
82 
83 #endif
84 
85 /*---------------------------------------------------------------------*/
86 /*                        End of File                                  */
87 /*---------------------------------------------------------------------*/
88