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.
23
#include "termorder.h"
28
/* Public definitions */
30
enum { /* how to check for maximal literals */
35
/* End of public definitions */
37
/* Public function prototypes from maximal.c */
39
void init_maximal(void);
41
BOOL max_lit_test(Literals lits, Literals lit);
43
BOOL max_signed_lit_test(Literals lits, Literals lit);
45
void mark_maximal_literals(Literals lits);
47
BOOL maximal_literal(Literals lits, Literals lit, int check);
49
BOOL maximal_signed_literal(Literals lits, Literals lit, int check);
51
int number_of_maximal_literals(Literals lits, int check);
53
void mark_selected_literal(Literals lit);
55
void mark_selected_literals(Literals lits, char *selection);
57
BOOL selected_literal(Literals lit);
59
BOOL exists_selected_literal(Literals lits);
61
void copy_selected_literal_marks(Literals a, Literals b);
63
#endif /* conditional compilation of whole file */