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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
/*-----------------------------------------------------------------------
File : ccl_propclauses.h
Author: Stephan Schulz
Contents
Definitions for propositional clauses (for eground) which can be
stored much more compactly than ordinary clauses - at the price of
less functionality and flexibility.
Copyright 1998-2011 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
Created: Sun Dec 16 16:29:02 CET 2001
-----------------------------------------------------------------------*/
#ifndef CCL_PROPCLAUSES
#define CCL_PROPCLAUSES
#include <ccl_clauses.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct proplitcell
{
EqnProperties properties;
Term_p lit;
}PropLitCell, *PropLit_p;
typedef struct propclausecell
{
int lit_no;
PropLit_p literals;
struct propclausecell *next; /* For linear lists == PropClauseSets */
}PropClauseCell, *PropClause_p;
typedef struct propclausesetcell
{
long members;
long literals;
long empty_clauses;
PropClause_p list; /* List of clauses */
PropClause_p *inspos; /* Points to next field of last clause, so we
can keep inserted clauses in order - I
believe giving propositional provers small
clauses first may be beneficial */
}PropClauseSetCell, *PropClauseSet_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define PropClauseCellAlloc() (PropClauseCell*)SizeMalloc(sizeof(PropClauseCell))
#define PropClauseCellFree(junk) SizeFree(junk, sizeof(PropClauseCell))
PropClause_p PropClauseAlloc(Clause_p clause);
void PropClauseFree(PropClause_p clause);
Clause_p PropClauseToClause(TB_p bank, PropClause_p clause);
void PropClausePrint(FILE* out, TB_p bank, PropClause_p
clause);
long PropClauseMaxVar(PropClause_p clause);
#define PropClauseSetCellAlloc() (PropClauseSetCell*)SizeMalloc(sizeof(PropClauseSetCell))
#define PropClauseSetCellFree(junk) SizeFree(junk, sizeof(PropClauseSetCell))
PropClauseSet_p PropClauseSetAlloc(void);
void PropClauseSetFree(PropClauseSet_p set);
long PropClauseSetInsertPropClause(PropClauseSet_p set,
PropClause_p clause);
long PropClauseSetInsertClause(PropClauseSet_p set,
Clause_p clause);
void PropClauseSetPrint(FILE* out, TB_p bank,
PropClauseSet_p set);
long PropClauseSetMaxVar(PropClauseSet_p set);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
