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_INDEX_LITS_H
20
#define TP_INDEX_LITS_H
22
#include "../ladr/clock.h"
23
#include "../ladr/subsume.h"
24
#include "../ladr/di_tree.h"
29
/* Public definitions */
31
/* End of public definitions */
33
/* Public function prototypes from index_lits.c */
35
void init_literals_index(void);
37
void destroy_literals_index(void);
39
void index_literals(Topform c, Indexop op, Clock clock, BOOL no_fapl);
41
void index_denial(Topform c, Indexop op, Clock clock);
43
void unit_conflict(Topform c, void (*empty_proc) (Topform));
45
void unit_deletion(Topform c);
47
Plist back_unit_deletable(Topform c);
49
Topform forward_subsumption(Topform d);
51
Plist back_subsumption(Topform c);
53
void lits_idx_report(void);
55
#endif /* conditional compilation of whole file */