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
99
100
101
102
103
104
|
/*-----------------------------------------------------------------------
File : ccl_splitting.h
Author: Stephan Schulz
Contents
Implements functions for destructive splitting of clauses with at
least two non-propositional variable disjoint subsets of literals.
Copyright 1998, 1999 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
<1> Wed Apr 18 18:24:18 MET DST 2001
New
-----------------------------------------------------------------------*/
#ifndef CCL_SPLITTING
#define CCL_SPLITTING
#include <ccl_def_handling.h>
typedef enum
{
SplitGroundNone = 0, /* Combine ground literals with first
subclause */
SplitGroundOne = 1, /* Split off (at most) _one_ ground subclause
containing all ground literals */
SplitGroundFull = 2 /* Split off individual ground literals */
}SplitType;
/* Describes which clauses should be split. Note that this currently
is not orthogonal at all. The functions using this are in
CONTROL/cco_clausesplitting.c, but we need the data type for the
control block later on. */
typedef enum
{
SplitNone = 0,
SplitHorn = 1,
SplitNonHorn = 2,
SplitNegative = 4,
SplitPositive = 8,
SplitMixed = 16,
SplitAll = 7
}SplitClassType;
#define QuerySplitClass(var, prop) ((var)&(prop))
#define SetSplitClass(var, prop) (var) = ((var)|(prop))
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct lit_split_desc
{
Eqn_p literal;
int part;
PTree_p varset; /* Initially: Varset of literal, later either
empty (in subsequent literals) or varset of
partition (for first literal of partition) */
}LitSplitDescCell, *LitSplitDesc_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
bool ClauseHasSplitLiteral(Clause_p clause);
int ClauseSplit(DefStore_p store, Clause_p clause, ClauseSet_p set,
SplitType how, bool fresh_defs);
long ClauseSetSplitClauses(DefStore_p store, ClauseSet_p from_set,
ClauseSet_p to_set, SplitType how,
bool fresh_defs);
long ClauseSetSplitClausesGeneral(DefStore_p store, bool fresh_defs,
ClauseSet_p from_set,
ClauseSet_p to_set, long tries);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
