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
|
/*-----------------------------------------------------------------------
File : ccl_factor.h
Author: Stephan Schulz
Contents
Functions for ordered factorisation.
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> Sun May 31 19:12:41 MET DST 1998
New
-----------------------------------------------------------------------*/
#ifndef CCL_FACTOR
#define CCL_FACTOR
#include <ccl_clausesets.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
Clause_p ComputeOrderedFactor(TB_p bank, OCB_p ocb, ClausePos_p pos1,
ClausePos_p pos2, VarBank_p freshvars);
Eqn_p ClausePosFirstOrderedFactorLiterals(Clause_p clause,
ClausePos_p pos1,
ClausePos_p pos2);
Eqn_p ClausePosNextOrderedFactorLiterals(ClausePos_p pos1,
ClausePos_p pos2);
Clause_p ComputeEqualityFactor(TB_p bank, OCB_p ocb, ClausePos_p pos1,
ClausePos_p pos2, VarBank_p freshvars);
Eqn_p ClausePosFirstEqualityFactorSides(Clause_p clause,
ClausePos_p pos1,
ClausePos_p pos2);
Eqn_p ClausePosNextEqualityFactorSides(ClausePos_p pos1,
ClausePos_p pos2);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
