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
|
/*-----------------------------------------------------------------------
File : cto_orderings.h
Author: Stephan Schulz
Contents
Generic Interface to the term comparison routines.
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 May 4 23:24:41 MET DST 1998
New
-----------------------------------------------------------------------*/
#ifndef CTO_ORDERINGS
#define CTO_ORDERINGS
#include <cto_lpo.h>
#include <cto_lpo_debug.h>
/* #include <cto_rpo.h> */
#include <cto_kbo.h>
#include <cto_kbolin.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
bool TOGreater(OCB_p ocb, Term_p s, Term_p t, DerefType
deref_s, DerefType deref_t);
CompareResult TOCompare(OCB_p ocb, Term_p s, Term_p t, DerefType
deref_s, DerefType deref_t);
CompareResult TOCompareSymbolParse(Scanner_p in);
PStackPointer TOSymbolComparisonChainParse(Scanner_p in, OCB_p ocb);
PStackPointer TOPrecedenceParse(Scanner_p in, OCB_p ocb);
void TOSymbolWeightParse(Scanner_p in, OCB_p ocb);
long TOWeightsParse(Scanner_p in, OCB_p ocb);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
