1
/* Copyright (C) 2006, 2007 William McCune
3
This file is part of the LADR Deduction Library.
5
The LADR Deduction Library is free software; you can redistribute it
6
and/or modify it under the terms of the GNU General Public License,
9
The LADR Deduction Library is distributed in the hope that it will be
10
useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
11
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12
GNU General Public License for more details.
14
You should have received a copy of the GNU General Public License
15
along with the LADR Deduction Library; if not, write to the Free Software
16
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
19
#ifndef TP_TERMORDER_H
20
#define TP_TERMORDER_H
27
/* Public definitions */
29
/* Term ordering method */
31
typedef enum { LRPO_METHOD,
37
/* End of public definitions */
39
/* Public function prototypes from termorder.c */
41
void assign_order_method(Order_method method);
43
Ordertype term_compare_basic(Term t1, Term t2);
45
Ordertype term_compare_ncv(Term t1, Term t2);
47
Ordertype term_compare_vcp(Term t1, Term t2);
49
Ordertype term_compare_vr(Term t1, Term t2);
51
Ordertype flatterm_compare_vr(Flatterm a, Flatterm b);
53
BOOL lrpo_multiset(Term t1, Term t2, BOOL lex_order_vars);
55
BOOL lrpo(Term s, Term t, BOOL lex_order_vars);
57
void init_kbo_weights(Plist weights);
59
int kbo_weight(Term t);
61
BOOL kbo(Term alpha, Term beta, BOOL lex_order_vars);
63
BOOL term_greater(Term alpha, Term beta, BOOL lex_order_vars);
65
Ordertype term_order(Term alpha, Term beta);
67
int flat_kbo_weight(Flatterm f);
69
BOOL flat_lrpo(Flatterm s, Flatterm t, BOOL lex_order_vars);
71
BOOL flat_greater(Flatterm alpha, Flatterm beta, BOOL lex_order_vars);
73
BOOL greater_multiset_current_ordering(Term t1, Term t2);
75
#endif /* conditional compilation of whole file */