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.
26
This package deals with clash structures, which are used for
27
binary resolution, hyperresolution, and UR-resolution.
28
The inference rule sets up a clash list (corresponding
29
to the nucleus), and then calls clash() to compute all of the
33
/* Public definitions */
35
typedef struct clash * Clash;
40
BOOL flipped; /* Is nuc_lit or sat_lit a flipped equality? */
50
/* End of public definitions */
52
/* Public function prototypes from clash.c */
54
void fprint_clash_mem(FILE *fp, BOOL heading);
58
Clash append_clash(Clash p);
60
void zap_clash(Clash p);
62
Literals atom_to_literal(Term atom);
64
Literals apply_lit(Literals lit, Context c);
67
BOOL (*sat_test) (Literals),
69
void (*proc_proc) (Topform));
71
#endif /* conditional compilation of whole file */