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_UTILITIES_H
20
#define TP_UTILITIES_H
22
#include "search-structures.h"
27
/* Public definitions */
29
/* End of public definitions */
31
/* Public function prototypes from utilities.c */
33
void print_memory_stats(FILE *fp);
35
void fsym_report(Ilist fsyms, Plist clauses);
37
BOOL inverse_order(Clist clauses);
39
void p_sym_list(Ilist syms);
41
void symbol_order(Clist usable, Clist sos, Clist demods, BOOL echo);
43
Ilist unary_symbols(Ilist a);
45
void auto_kbo_weights(Clist usable, Clist sos);
47
int neg_pos_depth_difference(Plist sos);
49
void structure_of_clauses(Clist clauses);
51
int plist_size_of_diff(Plist a, Plist b);
53
void structure_of_variables(Clist clauses);
55
Ordertype clause_compare_m4(Topform a, Topform b);
59
Topform first_negative_clause(Plist proof);
61
Plist neg_clauses_and_descendants(Plist proof,
62
Clist a_list, Clist b_list, Clist c_list);
64
Plist neg_descendants(Topform top_neg,
65
Clist a_list, Clist b_list, Clist c_list);
68
void check_constant_sharing(Plist clauses);
70
#endif /* conditional compilation of whole file */
added
removed
provers.src/utilities.h.bak
