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
|
/*-----------------------------------------------------------------------
File : cte_replace.h
Author: Stephan Schulz
Contents
Functions for replacing and rewriting of terms.
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> Mon Jan 12 17:50:21 MET 1998
New
-----------------------------------------------------------------------*/
#ifndef CTE_REPLACE
#define CTE_REPLACE
#include <clb_pqueue.h>
#include <cte_termcpos.h>
#include <cio_output.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/** Can a term be rewritten, rewritten if not protected, or always
** rewritten? */
typedef enum
{
RWNotRewritable = 0,
RWLimitedRewritable = 1,
RWAlwaysRewritable = 2,
}RWResultType;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
void TermAddRWLink(Term_p term, Term_p replace,
struct clause_cell *demod,
bool sos, RWResultType type);
void TermDeleteRWLink(Term_p term);
Term_p TermFollowRWChain(Term_p term);
Term_p TBTermPosReplace(TB_p bank, Term_p repl, TermPos_p pos,
DerefType deref, int remains, Term_p orig);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
