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
|
/*-----------------------------------------------------------------------
File : ccl_eqnresolution.h
Author: Stephan Schulz
Contents
Routines for performing (ordered) equality resolution.
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> Fri Jun 5 18:36:46 MET DST 1998
New
-----------------------------------------------------------------------*/
#ifndef CCL_EQNRESOLUTION
#define CCL_EQNRESOLUTION
#include <ccl_clausesets.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
extern bool EqResOnMaximalLiteralsOnly;
Clause_p ComputeEqRes(TB_p bank, ClausePos_p pos, VarBank_p
freshvars);
Eqn_p ClausePosFirstEqResLiteral(Clause_p clause, ClausePos_p
pos);
Eqn_p ClausePosNextEqResLiteral(ClausePos_p pos);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
