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.
29
/* Public definitions */
31
/* End of public definitions */
33
/* Public function prototypes from subsume.c */
35
int nonunit_subsumption_tests(void);
37
BOOL subsumes(Topform c, Topform d);
39
BOOL subsumes_bt(Topform c, Topform d);
41
Topform forward_subsume(Topform d, Lindex idx);
43
Plist back_subsume(Topform c, Lindex idx);
45
Topform back_subsume_one(Topform c, Lindex idx);
47
void unit_conflict_by_index(Topform c, Lindex idx, void (*empty_proc) (Topform));
49
Topform try_unit_conflict(Topform a, Topform b);
51
void unit_delete(Topform c, Lindex idx);
53
Plist back_unit_del_by_index(Topform unit, Lindex idx);
55
void simplify_literals(Topform c);
57
BOOL eq_removable_literal(Topform c, Literals lit);
59
void simplify_literals2(Topform c);
61
#endif /* conditional compilation of whole file */