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