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
|
/*-----------------------------------------------------------------------
File : ccl_clausecpos.h
Author: Stephan Schulz
Contents
Positions of subterms in clauses (and in equations) using compact
(i.e. single integer) positions.
Copyright 2010 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> Thu Feb 18 01:31:48 EET 2010
New
-----------------------------------------------------------------------*/
#ifndef CCL_CLAUSECPOS
#define CCL_CLAUSECPOS
#include <ccl_clausepos.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef long CompactPos;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
CompactPos PackTermPos(TermPos_p pos);
CompactPos PackClausePos(ClausePos_p pos);
void UnpackTermPos(TermPos_p pos, Term_p t, CompactPos cpos);
void UnpackClausePosInto(CompactPos cpos, Clause_p clause,
ClausePos_p pos);
ClausePos_p UnpackClausePos(CompactPos cpos, Clause_p clause);
Term_p ClauseCPosGetSubterm(Clause_p clause, CompactPos cpos);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
